[f3dc84]: thys / Functional-Automata / DA.thy  Maximize  Restore  History

Download this file

36 lines (24 with data), 887 Bytes

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
(* ID: $Id: DA.thy,v 1.3.2.1 2004-05-21 00:14:35 lsf37 Exp $
Author: Tobias Nipkow
Copyright 1998 TUM
*)
header "Deterministic automata"
theory DA = AutoProj:
types ('a,'s)da = "'s * ('a => 's => 's) * ('s => bool)"
constdefs
foldl2 :: "('a => 'b => 'b) => 'a list => 'b => 'b"
"foldl2 f xs a == foldl (%a b. f b a) a xs"
delta :: "('a,'s)da => 'a list => 's => 's"
"delta A == foldl2 (next A)"
accepts :: "('a,'s)da => 'a list => bool"
"accepts A == %w. fin A (delta A w (start A))"
lemma [simp]: "foldl2 f [] a = a & foldl2 f (x#xs) a = foldl2 f xs (f x a)"
by(simp add:foldl2_def)
lemma delta_Nil[simp]: "delta A [] s = s"
by(simp add:delta_def)
lemma delta_Cons[simp]: "delta A (a#w) s = delta A w (next A a s)"
by(simp add:delta_def)
lemma delta_append[simp]:
"!!q ys. delta A (xs@ys) q = delta A ys (delta A xs q)"
by(induct xs, simp_all)
end

Get latest updates about Open Source Projects, Conferences and News.

Sign up for the SourceForge newsletter:





No, thanks