Cleanup.
HOL-OCL/Isabelle_DOF/Isabelle2018 There was a failure building this commit
Details
HOL-OCL/Isabelle_DOF/Isabelle2018 There was a failure building this commit
Details
This commit is contained in:
parent
bbfe6b1a2c
commit
f971a8e018
|
|
@ -1,52 +0,0 @@
|
|||
(* Author: Tobias Nipkow
|
||||
Copyright 1998 TUM
|
||||
*)
|
||||
|
||||
section "Automata based scanner"
|
||||
|
||||
theory AutoMaxChop
|
||||
imports DA MaxChop
|
||||
begin
|
||||
|
||||
primrec auto_split :: "('a,'s)da \<Rightarrow> 's \<Rightarrow> 'a list * 'a list \<Rightarrow> 'a list \<Rightarrow> 'a splitter" where
|
||||
"auto_split A q res ps [] = (if fin A q then (ps,[]) else res)" |
|
||||
"auto_split A q res ps (x#xs) =
|
||||
auto_split A (next A x q) (if fin A q then (ps,x#xs) else res) (ps@[x]) xs"
|
||||
|
||||
definition
|
||||
auto_chop :: "('a,'s)da \<Rightarrow> 'a chopper" where
|
||||
"auto_chop A = chop (\<lambda>xs. auto_split A (start A) ([],xs) [] xs)"
|
||||
|
||||
|
||||
lemma delta_snoc: "delta A (xs@[y]) q = next A y (delta A xs q)"
|
||||
by simp
|
||||
|
||||
lemma auto_split_lemma:
|
||||
"\<And>q ps res. auto_split A (delta A ps q) res ps xs =
|
||||
maxsplit (\<lambda>ys. fin A (delta A ys q)) res ps xs"
|
||||
apply (induct xs)
|
||||
apply simp
|
||||
apply (simp add: delta_snoc[symmetric] del: delta_append)
|
||||
done
|
||||
|
||||
lemma auto_split_is_maxsplit:
|
||||
"auto_split A (start A) res [] xs = maxsplit (accepts A) res [] xs"
|
||||
apply (unfold accepts_def)
|
||||
apply (subst delta_Nil[where ?s = "start A", symmetric])
|
||||
apply (subst auto_split_lemma)
|
||||
apply simp
|
||||
done
|
||||
|
||||
lemma is_maxsplitter_auto_split:
|
||||
"is_maxsplitter (accepts A) (\<lambda>xs. auto_split A (start A) ([],xs) [] xs)"
|
||||
by (simp add: auto_split_is_maxsplit is_maxsplitter_maxsplit)
|
||||
|
||||
|
||||
lemma is_maxchopper_auto_chop:
|
||||
"is_maxchopper (accepts A) (auto_chop A)"
|
||||
apply (unfold auto_chop_def)
|
||||
apply (rule is_maxchopper_chop)
|
||||
apply (rule is_maxsplitter_auto_split)
|
||||
done
|
||||
|
||||
end
|
||||
|
|
@ -1,29 +0,0 @@
|
|||
(* Author: Tobias Nipkow
|
||||
Copyright 1998 TUM
|
||||
|
||||
Is there an optimal order of arguments for `next'?
|
||||
Currently we can have laws like `delta A (a#w) = delta A w o delta A a'
|
||||
Otherwise we could have `acceps A == fin A o delta A (start A)'
|
||||
and use foldl instead of foldl2.
|
||||
*)
|
||||
|
||||
section "Projection functions for automata"
|
||||
|
||||
theory AutoProj
|
||||
imports Main
|
||||
begin
|
||||
|
||||
definition start :: "'a * 'b * 'c \<Rightarrow> 'a" where "start A = fst A"
|
||||
definition "next" :: "'a * 'b * 'c \<Rightarrow> 'b" where "next A = fst(snd(A))"
|
||||
definition fin :: "'a * 'b * 'c \<Rightarrow> 'c" where "fin A = snd(snd(A))"
|
||||
|
||||
lemma [simp]: "start(q,d,f) = q"
|
||||
by(simp add:start_def)
|
||||
|
||||
lemma [simp]: "next(q,d,f) = d"
|
||||
by(simp add:next_def)
|
||||
|
||||
lemma [simp]: "fin(q,d,f) = f"
|
||||
by(simp add:fin_def)
|
||||
|
||||
end
|
||||
|
|
@ -1,17 +0,0 @@
|
|||
(* Author: Tobias Nipkow
|
||||
Copyright 1998 TUM
|
||||
*)
|
||||
|
||||
section "Combining automata and regular expressions"
|
||||
|
||||
theory AutoRegExp
|
||||
imports Automata RegExp2NA RegExp2NAe
|
||||
begin
|
||||
|
||||
theorem "DA.accepts (na2da(rexp2na r)) w = (w : lang r)"
|
||||
by (simp add: NA_DA_equiv[THEN sym] accepts_rexp2na)
|
||||
|
||||
theorem "DA.accepts (nae2da(rexp2nae r)) w = (w : lang r)"
|
||||
by (simp add: NAe_DA_equiv accepts_rexp2nae)
|
||||
|
||||
end
|
||||
|
|
@ -1,55 +0,0 @@
|
|||
(* Author: Tobias Nipkow
|
||||
Copyright 1998 TUM
|
||||
*)
|
||||
|
||||
section "Conversions between automata"
|
||||
|
||||
theory Automata
|
||||
imports DA NAe
|
||||
begin
|
||||
|
||||
definition
|
||||
na2da :: "('a,'s)na \<Rightarrow> ('a,'s set)da" where
|
||||
"na2da A = ({start A}, \<lambda>a Q. Union(next A a ` Q), \<lambda>Q. \<exists>q\<in>Q. fin A q)"
|
||||
|
||||
definition
|
||||
nae2da :: "('a,'s)nae \<Rightarrow> ('a,'s set)da" where
|
||||
"nae2da A = ({start A},
|
||||
\<lambda>a Q. Union(next A (Some a) ` ((eps A)\<^sup>* `` Q)),
|
||||
\<lambda>Q. \<exists>p \<in> (eps A)\<^sup>* `` Q. fin A p)"
|
||||
|
||||
(*** Equivalence of NA and DA ***)
|
||||
|
||||
lemma DA_delta_is_lift_NA_delta:
|
||||
"\<And>Q. DA.delta (na2da A) w Q = Union(NA.delta A w ` Q)"
|
||||
by (induct w)(auto simp:na2da_def)
|
||||
|
||||
lemma NA_DA_equiv:
|
||||
"NA.accepts A w = DA.accepts (na2da A) w"
|
||||
apply (simp add: DA.accepts_def NA.accepts_def DA_delta_is_lift_NA_delta)
|
||||
apply (simp add: na2da_def)
|
||||
done
|
||||
|
||||
(*** Direct equivalence of NAe and DA ***)
|
||||
|
||||
lemma espclosure_DA_delta_is_steps:
|
||||
"\<And>Q. (eps A)\<^sup>* `` (DA.delta (nae2da A) w Q) = steps A w `` Q"
|
||||
apply (induct w)
|
||||
apply(simp)
|
||||
apply (simp add: step_def nae2da_def)
|
||||
apply (blast)
|
||||
done
|
||||
|
||||
lemma NAe_DA_equiv:
|
||||
"DA.accepts (nae2da A) w = NAe.accepts A w"
|
||||
proof -
|
||||
have "\<And>Q. fin (nae2da A) Q = (\<exists>q \<in> (eps A)\<^sup>* `` Q. fin A q)"
|
||||
by(simp add:nae2da_def)
|
||||
thus ?thesis
|
||||
apply(simp add:espclosure_DA_delta_is_steps NAe.accepts_def DA.accepts_def)
|
||||
apply(simp add:nae2da_def)
|
||||
apply blast
|
||||
done
|
||||
qed
|
||||
|
||||
end
|
||||
|
|
@ -1,38 +0,0 @@
|
|||
(* Author: Tobias Nipkow
|
||||
Copyright 1998 TUM
|
||||
*)
|
||||
|
||||
section "Deterministic automata"
|
||||
|
||||
theory DA
|
||||
imports AutoProj
|
||||
begin
|
||||
|
||||
type_synonym ('a,'s)da = "'s * ('a \<Rightarrow> 's \<Rightarrow> 's) * ('s \<Rightarrow> bool)"
|
||||
|
||||
definition
|
||||
foldl2 :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a list \<Rightarrow> 'b \<Rightarrow> 'b" where
|
||||
"foldl2 f xs a = foldl (\<lambda>a b. f b a) a xs"
|
||||
|
||||
definition
|
||||
delta :: "('a,'s)da \<Rightarrow> 'a list \<Rightarrow> 's \<Rightarrow> 's" where
|
||||
"delta A = foldl2 (next A)"
|
||||
|
||||
definition
|
||||
accepts :: "('a,'s)da \<Rightarrow> 'a list \<Rightarrow> bool" where
|
||||
"accepts A = (\<lambda>w. fin A (delta A w (start A)))"
|
||||
|
||||
lemma [simp]: "foldl2 f [] a = a \<and> 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]:
|
||||
"\<And>q ys. delta A (xs@ys) q = delta A ys (delta A xs q)"
|
||||
by(induct xs) simp_all
|
||||
|
||||
end
|
||||
|
|
@ -1,20 +0,0 @@
|
|||
(* Author: Lukas Bulwahn, TUM 2011 *)
|
||||
|
||||
section \<open>Executing Automata and membership of Regular Expressions\<close>
|
||||
|
||||
theory Execute
|
||||
imports AutoRegExp
|
||||
begin
|
||||
|
||||
subsection \<open>Example\<close>
|
||||
|
||||
definition example_expression
|
||||
where
|
||||
"example_expression = (let r0 = Atom (0::nat); r1 = Atom (1::nat)
|
||||
in Times (Star (Plus (Times r1 r1) r0)) (Star (Plus (Times r0 r0) r1)))"
|
||||
|
||||
value "NA.accepts (rexp2na example_expression) [0,1,1,0,0,1]"
|
||||
|
||||
value "DA.accepts (na2da (rexp2na example_expression)) [0,1,1,0,0,1]"
|
||||
|
||||
end
|
||||
|
|
@ -1,5 +0,0 @@
|
|||
theory Functional_Automata
|
||||
imports AutoRegExp AutoMaxChop RegSet_of_nat_DA Execute
|
||||
begin
|
||||
|
||||
end
|
||||
|
|
@ -1,120 +0,0 @@
|
|||
(* Author: Tobias Nipkow
|
||||
Copyright 1998 TUM
|
||||
*)
|
||||
|
||||
section "Generic scanner"
|
||||
|
||||
theory MaxChop
|
||||
imports MaxPrefix
|
||||
begin
|
||||
|
||||
type_synonym 'a chopper = "'a list \<Rightarrow> 'a list list * 'a list"
|
||||
|
||||
definition
|
||||
is_maxchopper :: "('a list \<Rightarrow> bool) \<Rightarrow> 'a chopper \<Rightarrow> bool" where
|
||||
"is_maxchopper P chopper =
|
||||
(\<forall>xs zs yss.
|
||||
(chopper(xs) = (yss,zs)) =
|
||||
(xs = concat yss @ zs \<and> (\<forall>ys \<in> set yss. ys \<noteq> []) \<and>
|
||||
(case yss of
|
||||
[] \<Rightarrow> is_maxpref P [] xs
|
||||
| us#uss \<Rightarrow> is_maxpref P us xs \<and> chopper(concat(uss)@zs) = (uss,zs))))"
|
||||
|
||||
definition
|
||||
reducing :: "'a splitter \<Rightarrow> bool" where
|
||||
"reducing splitf =
|
||||
(\<forall>xs ys zs. splitf xs = (ys,zs) \<and> ys \<noteq> [] \<longrightarrow> length zs < length xs)"
|
||||
|
||||
function chop :: "'a splitter \<Rightarrow> 'a list \<Rightarrow> 'a list list \<times> 'a list" where
|
||||
[simp del]: "chop splitf xs = (if reducing splitf
|
||||
then let pp = splitf xs
|
||||
in if fst pp = [] then ([], xs)
|
||||
else let qq = chop splitf (snd pp)
|
||||
in (fst pp # fst qq, snd qq)
|
||||
else undefined)"
|
||||
by pat_completeness auto
|
||||
|
||||
termination apply (relation "measure (length \<circ> snd)")
|
||||
apply (auto simp: reducing_def)
|
||||
apply (case_tac "splitf xs")
|
||||
apply auto
|
||||
done
|
||||
|
||||
lemma chop_rule: "reducing splitf \<Longrightarrow>
|
||||
chop splitf xs = (let (pre, post) = splitf xs
|
||||
in if pre = [] then ([], xs)
|
||||
else let (xss, zs) = chop splitf post
|
||||
in (pre # xss,zs))"
|
||||
apply (simp add: chop.simps)
|
||||
apply (simp add: Let_def split: prod.split)
|
||||
done
|
||||
|
||||
lemma reducing_maxsplit: "reducing(\<lambda>qs. maxsplit P ([],qs) [] qs)"
|
||||
by (simp add: reducing_def maxsplit_eq)
|
||||
|
||||
lemma is_maxsplitter_reducing:
|
||||
"is_maxsplitter P splitf \<Longrightarrow> reducing splitf"
|
||||
by(simp add:is_maxsplitter_def reducing_def)
|
||||
|
||||
lemma chop_concat[rule_format]: "is_maxsplitter P splitf \<Longrightarrow>
|
||||
(\<forall>yss zs. chop splitf xs = (yss,zs) \<longrightarrow> xs = concat yss @ zs)"
|
||||
apply (induct xs rule:length_induct)
|
||||
apply (simp (no_asm_simp) split del: if_split
|
||||
add: chop_rule[OF is_maxsplitter_reducing])
|
||||
apply (simp add: Let_def is_maxsplitter_def split: prod.split)
|
||||
done
|
||||
|
||||
lemma chop_nonempty: "is_maxsplitter P splitf \<Longrightarrow>
|
||||
\<forall>yss zs. chop splitf xs = (yss,zs) \<longrightarrow> (\<forall>ys \<in> set yss. ys \<noteq> [])"
|
||||
apply (induct xs rule:length_induct)
|
||||
apply (simp (no_asm_simp) add: chop_rule is_maxsplitter_reducing)
|
||||
apply (simp add: Let_def is_maxsplitter_def split: prod.split)
|
||||
apply (intro allI impI)
|
||||
apply (rule ballI)
|
||||
apply (erule exE)
|
||||
apply (erule allE)
|
||||
apply auto
|
||||
done
|
||||
|
||||
lemma is_maxchopper_chop:
|
||||
assumes prem: "is_maxsplitter P splitf" shows "is_maxchopper P (chop splitf)"
|
||||
apply(unfold is_maxchopper_def)
|
||||
apply clarify
|
||||
apply (rule iffI)
|
||||
apply (rule conjI)
|
||||
apply (erule chop_concat[OF prem])
|
||||
apply (rule conjI)
|
||||
apply (erule prem[THEN chop_nonempty[THEN spec, THEN spec, THEN mp]])
|
||||
apply (erule rev_mp)
|
||||
apply (subst prem[THEN is_maxsplitter_reducing[THEN chop_rule]])
|
||||
apply (simp add: Let_def prem[simplified is_maxsplitter_def]
|
||||
split: prod.split)
|
||||
apply clarify
|
||||
apply (rule conjI)
|
||||
apply (clarify)
|
||||
apply (clarify)
|
||||
apply simp
|
||||
apply (frule chop_concat[OF prem])
|
||||
apply (clarify)
|
||||
apply (subst prem[THEN is_maxsplitter_reducing, THEN chop_rule])
|
||||
apply (simp add: Let_def prem[simplified is_maxsplitter_def]
|
||||
split: prod.split)
|
||||
apply (clarify)
|
||||
apply (rename_tac xs1 ys1 xss1 ys)
|
||||
apply (simp split: list.split_asm)
|
||||
apply (simp add: is_maxpref_def)
|
||||
apply (blast intro: prefix_append[THEN iffD2])
|
||||
apply (rule conjI)
|
||||
apply (clarify)
|
||||
apply (simp (no_asm_use) add: is_maxpref_def)
|
||||
apply (blast intro: prefix_append[THEN iffD2])
|
||||
apply (clarify)
|
||||
apply (rename_tac us uss)
|
||||
apply (subgoal_tac "xs1=us")
|
||||
apply simp
|
||||
apply simp
|
||||
apply (simp (no_asm_use) add: is_maxpref_def)
|
||||
apply (blast intro: prefix_append[THEN iffD2] prefix_order.antisym)
|
||||
done
|
||||
|
||||
end
|
||||
|
|
@ -1,92 +0,0 @@
|
|||
(* Author: Tobias Nipkow
|
||||
Copyright 1998 TUM
|
||||
*)
|
||||
|
||||
section "Maximal prefix"
|
||||
|
||||
theory MaxPrefix
|
||||
imports "HOL-Library.Sublist"
|
||||
begin
|
||||
|
||||
definition
|
||||
is_maxpref :: "('a list \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> bool" where
|
||||
"is_maxpref P xs ys =
|
||||
(prefix xs ys \<and> (xs=[] \<or> P xs) \<and> (\<forall>zs. prefix zs ys \<and> P zs \<longrightarrow> prefix zs xs))"
|
||||
|
||||
type_synonym 'a splitter = "'a list \<Rightarrow> 'a list * 'a list"
|
||||
|
||||
definition
|
||||
is_maxsplitter :: "('a list \<Rightarrow> bool) \<Rightarrow> 'a splitter \<Rightarrow> bool" where
|
||||
"is_maxsplitter P f =
|
||||
(\<forall>xs ps qs. f xs = (ps,qs) = (xs=ps@qs \<and> is_maxpref P ps xs))"
|
||||
|
||||
fun maxsplit :: "('a list \<Rightarrow> bool) \<Rightarrow> 'a list * 'a list \<Rightarrow> 'a list \<Rightarrow> 'a splitter" where
|
||||
"maxsplit P res ps [] = (if P ps then (ps,[]) else res)" |
|
||||
"maxsplit P res ps (q#qs) = maxsplit P (if P ps then (ps,q#qs) else res)
|
||||
(ps@[q]) qs"
|
||||
|
||||
declare if_split[split del]
|
||||
|
||||
lemma maxsplit_lemma: "(maxsplit P res ps qs = (xs,ys)) =
|
||||
(if \<exists>us. prefix us qs \<and> P(ps@us) then xs@ys=ps@qs \<and> is_maxpref P xs (ps@qs)
|
||||
else (xs,ys)=res)"
|
||||
proof (induction P res ps qs rule: maxsplit.induct)
|
||||
case 1
|
||||
thus ?case by (auto simp: is_maxpref_def split: if_splits)
|
||||
next
|
||||
case (2 P res ps q qs)
|
||||
show ?case
|
||||
proof (cases "\<exists>us. prefix us qs \<and> P ((ps @ [q]) @ us)")
|
||||
case True
|
||||
note ex1 = this
|
||||
then guess us by (elim exE conjE) note us = this
|
||||
hence ex2: "\<exists>us. prefix us (q # qs) \<and> P (ps @ us)"
|
||||
by (intro exI[of _ "q#us"]) auto
|
||||
with ex1 and 2 show ?thesis by simp
|
||||
next
|
||||
case False
|
||||
note ex1 = this
|
||||
show ?thesis
|
||||
proof (cases "\<exists>us. prefix us (q#qs) \<and> P (ps @ us)")
|
||||
case False
|
||||
from 2 show ?thesis
|
||||
by (simp only: ex1 False) (insert ex1 False, auto simp: prefix_Cons)
|
||||
next
|
||||
case True
|
||||
note ex2 = this
|
||||
show ?thesis
|
||||
proof (cases "P ps")
|
||||
case True
|
||||
with 2 have "(maxsplit P (ps, q # qs) (ps @ [q]) qs = (xs, ys)) \<longleftrightarrow> (xs = ps \<and> ys = q # qs)"
|
||||
by (simp only: ex1 ex2) simp_all
|
||||
also have "\<dots> \<longleftrightarrow> (xs @ ys = ps @ q # qs \<and> is_maxpref P xs (ps @ q # qs))"
|
||||
using ex1 True
|
||||
by (auto simp: is_maxpref_def prefix_append prefix_Cons append_eq_append_conv2)
|
||||
finally show ?thesis using True by (simp only: ex1 ex2) simp_all
|
||||
next
|
||||
case False
|
||||
with 2 have "(maxsplit P res (ps @ [q]) qs = (xs, ys)) \<longleftrightarrow> ((xs, ys) = res)"
|
||||
by (simp only: ex1 ex2) simp
|
||||
also have "\<dots> \<longleftrightarrow> (xs @ ys = ps @ q # qs \<and> is_maxpref P xs (ps @ q # qs))"
|
||||
using ex1 ex2 False
|
||||
by (auto simp: append_eq_append_conv2 is_maxpref_def prefix_Cons)
|
||||
finally show ?thesis
|
||||
using False by (simp only: ex1 ex2) simp
|
||||
qed
|
||||
qed
|
||||
qed
|
||||
qed
|
||||
|
||||
declare if_split[split]
|
||||
|
||||
lemma is_maxpref_Nil[simp]:
|
||||
"\<not>(\<exists>us. prefix us xs \<and> P us) \<Longrightarrow> is_maxpref P ps xs = (ps = [])"
|
||||
by (auto simp: is_maxpref_def)
|
||||
|
||||
lemma is_maxsplitter_maxsplit:
|
||||
"is_maxsplitter P (\<lambda>xs. maxsplit P ([],xs) [] xs)"
|
||||
by (auto simp: maxsplit_lemma is_maxsplitter_def)
|
||||
|
||||
lemmas maxsplit_eq = is_maxsplitter_maxsplit[simplified is_maxsplitter_def]
|
||||
|
||||
end
|
||||
|
|
@ -1,50 +0,0 @@
|
|||
(* Author: Tobias Nipkow
|
||||
Copyright 1998 TUM
|
||||
*)
|
||||
|
||||
section "Nondeterministic automata"
|
||||
|
||||
theory NA
|
||||
imports AutoProj
|
||||
begin
|
||||
|
||||
type_synonym ('a,'s) na = "'s * ('a \<Rightarrow> 's \<Rightarrow> 's set) * ('s \<Rightarrow> bool)"
|
||||
|
||||
primrec delta :: "('a,'s)na \<Rightarrow> 'a list \<Rightarrow> 's \<Rightarrow> 's set" where
|
||||
"delta A [] p = {p}" |
|
||||
"delta A (a#w) p = Union(delta A w ` next A a p)"
|
||||
|
||||
definition
|
||||
accepts :: "('a,'s)na \<Rightarrow> 'a list \<Rightarrow> bool" where
|
||||
"accepts A w = (\<exists>q \<in> delta A w (start A). fin A q)"
|
||||
|
||||
definition
|
||||
step :: "('a,'s)na \<Rightarrow> 'a \<Rightarrow> ('s * 's)set" where
|
||||
"step A a = {(p,q) . q : next A a p}"
|
||||
|
||||
primrec steps :: "('a,'s)na \<Rightarrow> 'a list \<Rightarrow> ('s * 's)set" where
|
||||
"steps A [] = Id" |
|
||||
"steps A (a#w) = step A a O steps A w"
|
||||
|
||||
lemma steps_append[simp]:
|
||||
"steps A (v@w) = steps A v O steps A w"
|
||||
by(induct v, simp_all add:O_assoc)
|
||||
|
||||
lemma in_steps_append[iff]:
|
||||
"(p,r) : steps A (v@w) = ((p,r) : (steps A v O steps A w))"
|
||||
apply(rule steps_append[THEN equalityE])
|
||||
apply blast
|
||||
done
|
||||
|
||||
lemma delta_conv_steps: "\<And>p. delta A w p = {q. (p,q) : steps A w}"
|
||||
by(induct w)(auto simp:step_def)
|
||||
|
||||
lemma accepts_conv_steps:
|
||||
"accepts A w = (\<exists>q. (start A,q) \<in> steps A w \<and> fin A q)"
|
||||
by(simp add: delta_conv_steps accepts_def)
|
||||
|
||||
abbreviation
|
||||
Cons_syn :: "'a \<Rightarrow> 'a list set \<Rightarrow> 'a list set" (infixr "##" 65) where
|
||||
"x ## S \<equiv> Cons x ` S"
|
||||
|
||||
end
|
||||
|
|
@ -1,72 +0,0 @@
|
|||
(* Author: Tobias Nipkow
|
||||
Copyright 1998 TUM
|
||||
*)
|
||||
|
||||
section "Nondeterministic automata with epsilon transitions"
|
||||
|
||||
theory NAe
|
||||
imports NA
|
||||
begin
|
||||
|
||||
type_synonym ('a,'s)nae = "('a option,'s)na"
|
||||
|
||||
abbreviation
|
||||
eps :: "('a,'s)nae \<Rightarrow> ('s * 's)set" where
|
||||
"eps A \<equiv> step A None"
|
||||
|
||||
primrec steps :: "('a,'s)nae \<Rightarrow> 'a list \<Rightarrow> ('s * 's)set" where
|
||||
"steps A [] = (eps A)\<^sup>*" |
|
||||
"steps A (a#w) = (eps A)\<^sup>* O step A (Some a) O steps A w"
|
||||
|
||||
definition
|
||||
accepts :: "('a,'s)nae \<Rightarrow> 'a list \<Rightarrow> bool" where
|
||||
"accepts A w = (\<exists>q. (start A,q) \<in> steps A w \<and> fin A q)"
|
||||
|
||||
(* not really used:
|
||||
consts delta :: "('a,'s)nae \<Rightarrow> 'a list \<Rightarrow> 's \<Rightarrow> 's set"
|
||||
primrec
|
||||
"delta A [] s = (eps A)\<^sup>* `` {s}"
|
||||
"delta A (a#w) s = lift(delta A w) (lift(next A (Some a)) ((eps A)\<^sup>* `` {s}))"
|
||||
*)
|
||||
|
||||
lemma steps_epsclosure[simp]: "(eps A)\<^sup>* O steps A w = steps A w"
|
||||
by (cases w) (simp_all add: O_assoc[symmetric])
|
||||
|
||||
lemma in_steps_epsclosure:
|
||||
"[| (p,q) : (eps A)\<^sup>*; (q,r) : steps A w |] ==> (p,r) : steps A w"
|
||||
apply(rule steps_epsclosure[THEN equalityE])
|
||||
apply blast
|
||||
done
|
||||
|
||||
lemma epsclosure_steps: "steps A w O (eps A)\<^sup>* = steps A w"
|
||||
apply(induct w)
|
||||
apply simp
|
||||
apply(simp add:O_assoc)
|
||||
done
|
||||
|
||||
lemma in_epsclosure_steps:
|
||||
"[| (p,q) : steps A w; (q,r) : (eps A)\<^sup>* |] ==> (p,r) : steps A w"
|
||||
apply(rule epsclosure_steps[THEN equalityE])
|
||||
apply blast
|
||||
done
|
||||
|
||||
lemma steps_append[simp]: "steps A (v@w) = steps A v O steps A w"
|
||||
by(induct v)(simp_all add:O_assoc[symmetric])
|
||||
|
||||
lemma in_steps_append[iff]:
|
||||
"(p,r) : steps A (v@w) = ((p,r) : (steps A v O steps A w))"
|
||||
apply(rule steps_append[THEN equalityE])
|
||||
apply blast
|
||||
done
|
||||
|
||||
(* Equivalence of steps and delta
|
||||
* Use "(\<exists>x \<in> f ` A. P x) = (\<exists>a\<in>A. P(f x))" ?? *
|
||||
Goal "\<forall>p. (p,q) : steps A w = (q : delta A w p)";
|
||||
by (induct_tac "w" 1);
|
||||
by (Simp_tac 1);
|
||||
by (asm_simp_tac (simpset() addsimps [comp_def,step_def]) 1);
|
||||
by (Blast_tac 1);
|
||||
qed_spec_mp "steps_equiv_delta";
|
||||
*)
|
||||
|
||||
end
|
||||
|
|
@ -1,11 +0,0 @@
|
|||
chapter AFP
|
||||
|
||||
session "Functional-Automata" (AFP) = "HOL-Library" +
|
||||
options [timeout = 600]
|
||||
sessions
|
||||
"Regular-Sets"
|
||||
theories
|
||||
Functional_Automata
|
||||
document_files
|
||||
"root.bib"
|
||||
"root.tex"
|
||||
|
|
@ -1,442 +0,0 @@
|
|||
(* Author: Tobias Nipkow
|
||||
Copyright 1998 TUM
|
||||
*)
|
||||
|
||||
section "From regular expressions directly to nondeterministic automata"
|
||||
|
||||
theory RegExp2NA
|
||||
imports "Regular-Sets.Regular_Exp" NA
|
||||
begin
|
||||
|
||||
type_synonym 'a bitsNA = "('a,bool list)na"
|
||||
|
||||
definition
|
||||
"atom" :: "'a \<Rightarrow> 'a bitsNA" where
|
||||
"atom a = ([True],
|
||||
\<lambda>b s. if s=[True] \<and> b=a then {[False]} else {},
|
||||
\<lambda>s. s=[False])"
|
||||
|
||||
definition
|
||||
or :: "'a bitsNA \<Rightarrow> 'a bitsNA \<Rightarrow> 'a bitsNA" where
|
||||
"or = (\<lambda>(ql,dl,fl)(qr,dr,fr).
|
||||
([],
|
||||
\<lambda>a s. case s of
|
||||
[] \<Rightarrow> (True ## dl a ql) \<union> (False ## dr a qr)
|
||||
| left#s \<Rightarrow> if left then True ## dl a s
|
||||
else False ## dr a s,
|
||||
\<lambda>s. case s of [] \<Rightarrow> (fl ql | fr qr)
|
||||
| left#s \<Rightarrow> if left then fl s else fr s))"
|
||||
|
||||
definition
|
||||
conc :: "'a bitsNA \<Rightarrow> 'a bitsNA \<Rightarrow> 'a bitsNA" where
|
||||
"conc = (\<lambda>(ql,dl,fl)(qr,dr,fr).
|
||||
(True#ql,
|
||||
\<lambda>a s. case s of
|
||||
[] \<Rightarrow> {}
|
||||
| left#s \<Rightarrow> if left then (True ## dl a s) \<union>
|
||||
(if fl s then False ## dr a qr else {})
|
||||
else False ## dr a s,
|
||||
\<lambda>s. case s of [] \<Rightarrow> False | left#s \<Rightarrow> left \<and> fl s \<and> fr qr | \<not>left \<and> fr s))"
|
||||
|
||||
definition
|
||||
epsilon :: "'a bitsNA" where
|
||||
"epsilon = ([],\<lambda>a s. {}, \<lambda>s. s=[])"
|
||||
|
||||
definition
|
||||
plus :: "'a bitsNA \<Rightarrow> 'a bitsNA" where
|
||||
"plus = (\<lambda>(q,d,f). (q, \<lambda>a s. d a s \<union> (if f s then d a q else {}), f))"
|
||||
|
||||
definition
|
||||
star :: "'a bitsNA \<Rightarrow> 'a bitsNA" where
|
||||
"star A = or epsilon (plus A)"
|
||||
|
||||
primrec rexp2na :: "'a rexp \<Rightarrow> 'a bitsNA" where
|
||||
"rexp2na Zero = ([], \<lambda>a s. {}, \<lambda>s. False)" |
|
||||
"rexp2na One = epsilon" |
|
||||
"rexp2na(Atom a) = atom a" |
|
||||
"rexp2na(Plus r s) = or (rexp2na r) (rexp2na s)" |
|
||||
"rexp2na(Times r s) = conc (rexp2na r) (rexp2na s)" |
|
||||
"rexp2na(Star r) = star (rexp2na r)"
|
||||
|
||||
declare split_paired_all[simp]
|
||||
|
||||
(******************************************************)
|
||||
(* atom *)
|
||||
(******************************************************)
|
||||
|
||||
lemma fin_atom: "(fin (atom a) q) = (q = [False])"
|
||||
by(simp add:atom_def)
|
||||
|
||||
lemma start_atom: "start (atom a) = [True]"
|
||||
by(simp add:atom_def)
|
||||
|
||||
lemma in_step_atom_Some[simp]:
|
||||
"(p,q) : step (atom a) b = (p=[True] \<and> q=[False] \<and> b=a)"
|
||||
by (simp add: atom_def step_def)
|
||||
|
||||
lemma False_False_in_steps_atom:
|
||||
"([False],[False]) : steps (atom a) w = (w = [])"
|
||||
apply (induct "w")
|
||||
apply simp
|
||||
apply (simp add: relcomp_unfold)
|
||||
done
|
||||
|
||||
lemma start_fin_in_steps_atom:
|
||||
"(start (atom a), [False]) : steps (atom a) w = (w = [a])"
|
||||
apply (induct "w")
|
||||
apply (simp add: start_atom)
|
||||
apply (simp add: False_False_in_steps_atom relcomp_unfold start_atom)
|
||||
done
|
||||
|
||||
lemma accepts_atom:
|
||||
"accepts (atom a) w = (w = [a])"
|
||||
by (simp add: accepts_conv_steps start_fin_in_steps_atom fin_atom)
|
||||
|
||||
(******************************************************)
|
||||
(* or *)
|
||||
(******************************************************)
|
||||
|
||||
(***** lift True/False over fin *****)
|
||||
|
||||
lemma fin_or_True[iff]:
|
||||
"\<And>L R. fin (or L R) (True#p) = fin L p"
|
||||
by(simp add:or_def)
|
||||
|
||||
lemma fin_or_False[iff]:
|
||||
"\<And>L R. fin (or L R) (False#p) = fin R p"
|
||||
by(simp add:or_def)
|
||||
|
||||
(***** lift True/False over step *****)
|
||||
|
||||
lemma True_in_step_or[iff]:
|
||||
"\<And>L R. (True#p,q) : step (or L R) a = (\<exists>r. q = True#r \<and> (p,r) \<in> step L a)"
|
||||
apply (simp add:or_def step_def)
|
||||
apply blast
|
||||
done
|
||||
|
||||
lemma False_in_step_or[iff]:
|
||||
"\<And>L R. (False#p,q) : step (or L R) a = (\<exists>r. q = False#r \<and> (p,r) \<in> step R a)"
|
||||
apply (simp add:or_def step_def)
|
||||
apply blast
|
||||
done
|
||||
|
||||
|
||||
(***** lift True/False over steps *****)
|
||||
|
||||
lemma lift_True_over_steps_or[iff]:
|
||||
"\<And>p. (True#p,q)\<in>steps (or L R) w = (\<exists>r. q = True # r \<and> (p,r) \<in> steps L w)"
|
||||
apply (induct "w")
|
||||
apply force
|
||||
apply force
|
||||
done
|
||||
|
||||
lemma lift_False_over_steps_or[iff]:
|
||||
"\<And>p. (False#p,q)\<in>steps (or L R) w = (\<exists>r. q = False#r \<and> (p,r)\<in>steps R w)"
|
||||
apply (induct "w")
|
||||
apply force
|
||||
apply force
|
||||
done
|
||||
|
||||
(** From the start **)
|
||||
|
||||
lemma start_step_or[iff]:
|
||||
"\<And>L R. (start(or L R),q) : step(or L R) a =
|
||||
(\<exists>p. (q = True#p \<and> (start L,p) : step L a) |
|
||||
(q = False#p \<and> (start R,p) : step R a))"
|
||||
apply (simp add:or_def step_def)
|
||||
apply blast
|
||||
done
|
||||
|
||||
lemma steps_or:
|
||||
"(start(or L R), q) : steps (or L R) w =
|
||||
( (w = [] \<and> q = start(or L R)) |
|
||||
(w \<noteq> [] \<and> (\<exists>p. q = True # p \<and> (start L,p) : steps L w |
|
||||
q = False # p \<and> (start R,p) : steps R w)))"
|
||||
apply (case_tac "w")
|
||||
apply (simp)
|
||||
apply blast
|
||||
apply (simp)
|
||||
apply blast
|
||||
done
|
||||
|
||||
lemma fin_start_or[iff]:
|
||||
"\<And>L R. fin (or L R) (start(or L R)) = (fin L (start L) | fin R (start R))"
|
||||
by (simp add:or_def)
|
||||
|
||||
lemma accepts_or[iff]:
|
||||
"accepts (or L R) w = (accepts L w | accepts R w)"
|
||||
apply (simp add: accepts_conv_steps steps_or)
|
||||
(* get rid of case_tac: *)
|
||||
apply (case_tac "w = []")
|
||||
apply auto
|
||||
done
|
||||
|
||||
(******************************************************)
|
||||
(* conc *)
|
||||
(******************************************************)
|
||||
|
||||
(** True/False in fin **)
|
||||
|
||||
lemma fin_conc_True[iff]:
|
||||
"\<And>L R. fin (conc L R) (True#p) = (fin L p \<and> fin R (start R))"
|
||||
by(simp add:conc_def)
|
||||
|
||||
lemma fin_conc_False[iff]:
|
||||
"\<And>L R. fin (conc L R) (False#p) = fin R p"
|
||||
by(simp add:conc_def)
|
||||
|
||||
|
||||
(** True/False in step **)
|
||||
|
||||
lemma True_step_conc[iff]:
|
||||
"\<And>L R. (True#p,q) : step (conc L R) a =
|
||||
((\<exists>r. q=True#r \<and> (p,r): step L a) |
|
||||
(fin L p \<and> (\<exists>r. q=False#r \<and> (start R,r) : step R a)))"
|
||||
apply (simp add:conc_def step_def)
|
||||
apply blast
|
||||
done
|
||||
|
||||
lemma False_step_conc[iff]:
|
||||
"\<And>L R. (False#p,q) : step (conc L R) a =
|
||||
(\<exists>r. q = False#r \<and> (p,r) : step R a)"
|
||||
apply (simp add:conc_def step_def)
|
||||
apply blast
|
||||
done
|
||||
|
||||
(** False in steps **)
|
||||
|
||||
lemma False_steps_conc[iff]:
|
||||
"\<And>p. (False#p,q): steps (conc L R) w = (\<exists>r. q=False#r \<and> (p,r): steps R w)"
|
||||
apply (induct "w")
|
||||
apply fastforce
|
||||
apply force
|
||||
done
|
||||
|
||||
(** True in steps **)
|
||||
|
||||
lemma True_True_steps_concI:
|
||||
"\<And>L R p. (p,q) : steps L w \<Longrightarrow> (True#p,True#q) : steps (conc L R) w"
|
||||
apply (induct "w")
|
||||
apply simp
|
||||
apply simp
|
||||
apply fast
|
||||
done
|
||||
|
||||
lemma True_False_step_conc[iff]:
|
||||
"\<And>L R. (True#p,False#q) : step (conc L R) a =
|
||||
(fin L p \<and> (start R,q) : step R a)"
|
||||
by simp
|
||||
|
||||
lemma True_steps_concD[rule_format]:
|
||||
"\<forall>p. (True#p,q) : steps (conc L R) w \<longrightarrow>
|
||||
((\<exists>r. (p,r) : steps L w \<and> q = True#r) \<or>
|
||||
(\<exists>u a v. w = u@a#v \<and>
|
||||
(\<exists>r. (p,r) : steps L u \<and> fin L r \<and>
|
||||
(\<exists>s. (start R,s) : step R a \<and>
|
||||
(\<exists>t. (s,t) : steps R v \<and> q = False#t)))))"
|
||||
apply (induct "w")
|
||||
apply simp
|
||||
apply simp
|
||||
apply (clarify del:disjCI)
|
||||
apply (erule disjE)
|
||||
apply (clarify del:disjCI)
|
||||
apply (erule allE, erule impE, assumption)
|
||||
apply (erule disjE)
|
||||
apply blast
|
||||
apply (rule disjI2)
|
||||
apply (clarify)
|
||||
apply simp
|
||||
apply (rule_tac x = "a#u" in exI)
|
||||
apply simp
|
||||
apply blast
|
||||
apply (rule disjI2)
|
||||
apply (clarify)
|
||||
apply simp
|
||||
apply (rule_tac x = "[]" in exI)
|
||||
apply simp
|
||||
apply blast
|
||||
done
|
||||
|
||||
lemma True_steps_conc:
|
||||
"(True#p,q) : steps (conc L R) w =
|
||||
((\<exists>r. (p,r) : steps L w \<and> q = True#r) \<or>
|
||||
(\<exists>u a v. w = u@a#v \<and>
|
||||
(\<exists>r. (p,r) : steps L u \<and> fin L r \<and>
|
||||
(\<exists>s. (start R,s) : step R a \<and>
|
||||
(\<exists>t. (s,t) : steps R v \<and> q = False#t)))))"
|
||||
by(force dest!: True_steps_concD intro!: True_True_steps_concI)
|
||||
|
||||
(** starting from the start **)
|
||||
|
||||
lemma start_conc:
|
||||
"\<And>L R. start(conc L R) = True#start L"
|
||||
by (simp add:conc_def)
|
||||
|
||||
lemma final_conc:
|
||||
"\<And>L R. fin(conc L R) p = ((fin R (start R) \<and> (\<exists>s. p = True#s \<and> fin L s)) \<or>
|
||||
(\<exists>s. p = False#s \<and> fin R s))"
|
||||
apply (simp add:conc_def split: list.split)
|
||||
apply blast
|
||||
done
|
||||
|
||||
lemma accepts_conc:
|
||||
"accepts (conc L R) w = (\<exists>u v. w = u@v \<and> accepts L u \<and> accepts R v)"
|
||||
apply (simp add: accepts_conv_steps True_steps_conc final_conc start_conc)
|
||||
apply (rule iffI)
|
||||
apply (clarify)
|
||||
apply (erule disjE)
|
||||
apply (clarify)
|
||||
apply (erule disjE)
|
||||
apply (rule_tac x = "w" in exI)
|
||||
apply simp
|
||||
apply blast
|
||||
apply blast
|
||||
apply (erule disjE)
|
||||
apply blast
|
||||
apply (clarify)
|
||||
apply (rule_tac x = "u" in exI)
|
||||
apply simp
|
||||
apply blast
|
||||
apply (clarify)
|
||||
apply (case_tac "v")
|
||||
apply simp
|
||||
apply blast
|
||||
apply simp
|
||||
apply blast
|
||||
done
|
||||
|
||||
(******************************************************)
|
||||
(* epsilon *)
|
||||
(******************************************************)
|
||||
|
||||
lemma step_epsilon[simp]: "step epsilon a = {}"
|
||||
by(simp add:epsilon_def step_def)
|
||||
|
||||
lemma steps_epsilon: "((p,q) : steps epsilon w) = (w=[] \<and> p=q)"
|
||||
by (induct "w") auto
|
||||
|
||||
lemma accepts_epsilon[iff]: "accepts epsilon w = (w = [])"
|
||||
apply (simp add: steps_epsilon accepts_conv_steps)
|
||||
apply (simp add: epsilon_def)
|
||||
done
|
||||
|
||||
(******************************************************)
|
||||
(* plus *)
|
||||
(******************************************************)
|
||||
|
||||
lemma start_plus[simp]: "\<And>A. start (plus A) = start A"
|
||||
by(simp add:plus_def)
|
||||
|
||||
lemma fin_plus[iff]: "\<And>A. fin (plus A) = fin A"
|
||||
by(simp add:plus_def)
|
||||
|
||||
lemma step_plusI:
|
||||
"\<And>A. (p,q) : step A a \<Longrightarrow> (p,q) : step (plus A) a"
|
||||
by(simp add:plus_def step_def)
|
||||
|
||||
lemma steps_plusI: "\<And>p. (p,q) : steps A w \<Longrightarrow> (p,q) \<in> steps (plus A) w"
|
||||
apply (induct "w")
|
||||
apply simp
|
||||
apply simp
|
||||
apply (blast intro: step_plusI)
|
||||
done
|
||||
|
||||
lemma step_plus_conv[iff]:
|
||||
"\<And>A. (p,r): step (plus A) a =
|
||||
( (p,r): step A a | fin A p \<and> (start A,r) : step A a )"
|
||||
by(simp add:plus_def step_def)
|
||||
|
||||
lemma fin_steps_plusI:
|
||||
"[| (start A,q) : steps A u; u \<noteq> []; fin A p |]
|
||||
==> (p,q) : steps (plus A) u"
|
||||
apply (case_tac "u")
|
||||
apply blast
|
||||
apply simp
|
||||
apply (blast intro: steps_plusI)
|
||||
done
|
||||
|
||||
(* reverse list induction! Complicates matters for conc? *)
|
||||
lemma start_steps_plusD[rule_format]:
|
||||
"\<forall>r. (start A,r) \<in> steps (plus A) w \<longrightarrow>
|
||||
(\<exists>us v. w = concat us @ v \<and>
|
||||
(\<forall>u\<in>set us. accepts A u) \<and>
|
||||
(start A,r) \<in> steps A v)"
|
||||
apply (induct w rule: rev_induct)
|
||||
apply simp
|
||||
apply (rule_tac x = "[]" in exI)
|
||||
apply simp
|
||||
apply simp
|
||||
apply (clarify)
|
||||
apply (erule allE, erule impE, assumption)
|
||||
apply (clarify)
|
||||
apply (erule disjE)
|
||||
apply (rule_tac x = "us" in exI)
|
||||
apply (simp)
|
||||
apply blast
|
||||
apply (rule_tac x = "us@[v]" in exI)
|
||||
apply (simp add: accepts_conv_steps)
|
||||
apply blast
|
||||
done
|
||||
|
||||
lemma steps_star_cycle[rule_format]:
|
||||
"us \<noteq> [] \<longrightarrow> (\<forall>u \<in> set us. accepts A u) \<longrightarrow> accepts (plus A) (concat us)"
|
||||
apply (simp add: accepts_conv_steps)
|
||||
apply (induct us rule: rev_induct)
|
||||
apply simp
|
||||
apply (rename_tac u us)
|
||||
apply simp
|
||||
apply (clarify)
|
||||
apply (case_tac "us = []")
|
||||
apply (simp)
|
||||
apply (blast intro: steps_plusI fin_steps_plusI)
|
||||
apply (clarify)
|
||||
apply (case_tac "u = []")
|
||||
apply (simp)
|
||||
apply (blast intro: steps_plusI fin_steps_plusI)
|
||||
apply (blast intro: steps_plusI fin_steps_plusI)
|
||||
done
|
||||
|
||||
lemma accepts_plus[iff]:
|
||||
"accepts (plus A) w =
|
||||
(\<exists>us. us \<noteq> [] \<and> w = concat us \<and> (\<forall>u \<in> set us. accepts A u))"
|
||||
apply (rule iffI)
|
||||
apply (simp add: accepts_conv_steps)
|
||||
apply (clarify)
|
||||
apply (drule start_steps_plusD)
|
||||
apply (clarify)
|
||||
apply (rule_tac x = "us@[v]" in exI)
|
||||
apply (simp add: accepts_conv_steps)
|
||||
apply blast
|
||||
apply (blast intro: steps_star_cycle)
|
||||
done
|
||||
|
||||
(******************************************************)
|
||||
(* star *)
|
||||
(******************************************************)
|
||||
|
||||
lemma accepts_star:
|
||||
"accepts (star A) w = (\<exists>us. (\<forall>u \<in> set us. accepts A u) \<and> w = concat us)"
|
||||
apply(unfold star_def)
|
||||
apply (rule iffI)
|
||||
apply (clarify)
|
||||
apply (erule disjE)
|
||||
apply (rule_tac x = "[]" in exI)
|
||||
apply simp
|
||||
apply blast
|
||||
apply force
|
||||
done
|
||||
|
||||
(***** Correctness of r2n *****)
|
||||
|
||||
lemma accepts_rexp2na:
|
||||
"\<And>w. accepts (rexp2na r) w = (w : lang r)"
|
||||
apply (induct "r")
|
||||
apply (simp add: accepts_conv_steps)
|
||||
apply simp
|
||||
apply (simp add: accepts_atom)
|
||||
apply (simp)
|
||||
apply (simp add: accepts_conc Regular_Set.conc_def)
|
||||
apply (simp add: accepts_star in_star_iff_concat subset_iff Ball_def)
|
||||
done
|
||||
|
||||
end
|
||||
|
|
@ -1,641 +0,0 @@
|
|||
(* Author: Tobias Nipkow
|
||||
Copyright 1998 TUM
|
||||
*)
|
||||
|
||||
section "From regular expressions to nondeterministic automata with epsilon"
|
||||
|
||||
theory RegExp2NAe
|
||||
imports "Regular-Sets.Regular_Exp" NAe
|
||||
begin
|
||||
|
||||
type_synonym 'a bitsNAe = "('a,bool list)nae"
|
||||
|
||||
definition
|
||||
epsilon :: "'a bitsNAe" where
|
||||
"epsilon = ([],\<lambda>a s. {}, \<lambda>s. s=[])"
|
||||
|
||||
definition
|
||||
"atom" :: "'a \<Rightarrow> 'a bitsNAe" where
|
||||
"atom a = ([True],
|
||||
\<lambda>b s. if s=[True] \<and> b=Some a then {[False]} else {},
|
||||
\<lambda>s. s=[False])"
|
||||
|
||||
definition
|
||||
or :: "'a bitsNAe \<Rightarrow> 'a bitsNAe \<Rightarrow> 'a bitsNAe" where
|
||||
"or = (\<lambda>(ql,dl,fl)(qr,dr,fr).
|
||||
([],
|
||||
\<lambda>a s. case s of
|
||||
[] \<Rightarrow> if a=None then {True#ql,False#qr} else {}
|
||||
| left#s \<Rightarrow> if left then True ## dl a s
|
||||
else False ## dr a s,
|
||||
\<lambda>s. case s of [] \<Rightarrow> False | left#s \<Rightarrow> if left then fl s else fr s))"
|
||||
|
||||
definition
|
||||
conc :: "'a bitsNAe \<Rightarrow> 'a bitsNAe \<Rightarrow> 'a bitsNAe" where
|
||||
"conc = (\<lambda>(ql,dl,fl)(qr,dr,fr).
|
||||
(True#ql,
|
||||
\<lambda>a s. case s of
|
||||
[] \<Rightarrow> {}
|
||||
| left#s \<Rightarrow> if left then (True ## dl a s) \<union>
|
||||
(if fl s \<and> a=None then {False#qr} else {})
|
||||
else False ## dr a s,
|
||||
\<lambda>s. case s of [] \<Rightarrow> False | left#s \<Rightarrow> \<not>left \<and> fr s))"
|
||||
|
||||
definition
|
||||
star :: "'a bitsNAe \<Rightarrow> 'a bitsNAe" where
|
||||
"star = (\<lambda>(q,d,f).
|
||||
([],
|
||||
\<lambda>a s. case s of
|
||||
[] \<Rightarrow> if a=None then {True#q} else {}
|
||||
| left#s \<Rightarrow> if left then (True ## d a s) \<union>
|
||||
(if f s \<and> a=None then {True#q} else {})
|
||||
else {},
|
||||
\<lambda>s. case s of [] \<Rightarrow> True | left#s \<Rightarrow> left \<and> f s))"
|
||||
|
||||
primrec rexp2nae :: "'a rexp \<Rightarrow> 'a bitsNAe" where
|
||||
"rexp2nae Zero = ([], \<lambda>a s. {}, \<lambda>s. False)" |
|
||||
"rexp2nae One = epsilon" |
|
||||
"rexp2nae(Atom a) = atom a" |
|
||||
"rexp2nae(Plus r s) = or (rexp2nae r) (rexp2nae s)" |
|
||||
"rexp2nae(Times r s) = conc (rexp2nae r) (rexp2nae s)" |
|
||||
"rexp2nae(Star r) = star (rexp2nae r)"
|
||||
|
||||
declare split_paired_all[simp]
|
||||
|
||||
(******************************************************)
|
||||
(* epsilon *)
|
||||
(******************************************************)
|
||||
|
||||
lemma step_epsilon[simp]: "step epsilon a = {}"
|
||||
by(simp add:epsilon_def step_def)
|
||||
|
||||
lemma steps_epsilon: "((p,q) : steps epsilon w) = (w=[] \<and> p=q)"
|
||||
by (induct "w") auto
|
||||
|
||||
lemma accepts_epsilon[simp]: "accepts epsilon w = (w = [])"
|
||||
apply (simp add: steps_epsilon accepts_def)
|
||||
apply (simp add: epsilon_def)
|
||||
done
|
||||
|
||||
(******************************************************)
|
||||
(* atom *)
|
||||
(******************************************************)
|
||||
|
||||
lemma fin_atom: "(fin (atom a) q) = (q = [False])"
|
||||
by(simp add:atom_def)
|
||||
|
||||
lemma start_atom: "start (atom a) = [True]"
|
||||
by(simp add:atom_def)
|
||||
|
||||
(* Use {x. False} = {}? *)
|
||||
|
||||
lemma eps_atom[simp]:
|
||||
"eps(atom a) = {}"
|
||||
by (simp add:atom_def step_def)
|
||||
|
||||
lemma in_step_atom_Some[simp]:
|
||||
"(p,q) : step (atom a) (Some b) = (p=[True] \<and> q=[False] \<and> b=a)"
|
||||
by (simp add:atom_def step_def)
|
||||
|
||||
lemma False_False_in_steps_atom:
|
||||
"([False],[False]) : steps (atom a) w = (w = [])"
|
||||
apply (induct "w")
|
||||
apply (simp)
|
||||
apply (simp add: relcomp_unfold)
|
||||
done
|
||||
|
||||
lemma start_fin_in_steps_atom:
|
||||
"(start (atom a), [False]) : steps (atom a) w = (w = [a])"
|
||||
apply (induct "w")
|
||||
apply (simp add: start_atom rtrancl_empty)
|
||||
apply (simp add: False_False_in_steps_atom relcomp_unfold start_atom)
|
||||
done
|
||||
|
||||
lemma accepts_atom: "accepts (atom a) w = (w = [a])"
|
||||
by (simp add: accepts_def start_fin_in_steps_atom fin_atom)
|
||||
|
||||
|
||||
(******************************************************)
|
||||
(* or *)
|
||||
(******************************************************)
|
||||
|
||||
(***** lift True/False over fin *****)
|
||||
|
||||
lemma fin_or_True[iff]:
|
||||
"\<And>L R. fin (or L R) (True#p) = fin L p"
|
||||
by(simp add:or_def)
|
||||
|
||||
lemma fin_or_False[iff]:
|
||||
"\<And>L R. fin (or L R) (False#p) = fin R p"
|
||||
by(simp add:or_def)
|
||||
|
||||
(***** lift True/False over step *****)
|
||||
|
||||
lemma True_in_step_or[iff]:
|
||||
"\<And>L R. (True#p,q) : step (or L R) a = (\<exists>r. q = True#r \<and> (p,r) : step L a)"
|
||||
apply (simp add:or_def step_def)
|
||||
apply blast
|
||||
done
|
||||
|
||||
lemma False_in_step_or[iff]:
|
||||
"\<And>L R. (False#p,q) : step (or L R) a = (\<exists>r. q = False#r \<and> (p,r) : step R a)"
|
||||
apply (simp add:or_def step_def)
|
||||
apply blast
|
||||
done
|
||||
|
||||
|
||||
(***** lift True/False over epsclosure *****)
|
||||
|
||||
lemma lemma1a:
|
||||
"(tp,tq) : (eps(or L R))\<^sup>* \<Longrightarrow>
|
||||
(\<And>p. tp = True#p \<Longrightarrow> \<exists>q. (p,q) : (eps L)\<^sup>* \<and> tq = True#q)"
|
||||
apply (induct rule:rtrancl_induct)
|
||||
apply (blast)
|
||||
apply (clarify)
|
||||
apply (simp)
|
||||
apply (blast intro: rtrancl_into_rtrancl)
|
||||
done
|
||||
|
||||
lemma lemma1b:
|
||||
"(tp,tq) : (eps(or L R))\<^sup>* \<Longrightarrow>
|
||||
(\<And>p. tp = False#p \<Longrightarrow> \<exists>q. (p,q) : (eps R)\<^sup>* \<and> tq = False#q)"
|
||||
apply (induct rule:rtrancl_induct)
|
||||
apply (blast)
|
||||
apply (clarify)
|
||||
apply (simp)
|
||||
apply (blast intro: rtrancl_into_rtrancl)
|
||||
done
|
||||
|
||||
lemma lemma2a:
|
||||
"(p,q) : (eps L)\<^sup>* \<Longrightarrow> (True#p, True#q) : (eps(or L R))\<^sup>*"
|
||||
apply (induct rule: rtrancl_induct)
|
||||
apply (blast)
|
||||
apply (blast intro: rtrancl_into_rtrancl)
|
||||
done
|
||||
|
||||
lemma lemma2b:
|
||||
"(p,q) : (eps R)\<^sup>* \<Longrightarrow> (False#p, False#q) : (eps(or L R))\<^sup>*"
|
||||
apply (induct rule: rtrancl_induct)
|
||||
apply (blast)
|
||||
apply (blast intro: rtrancl_into_rtrancl)
|
||||
done
|
||||
|
||||
lemma True_epsclosure_or[iff]:
|
||||
"(True#p,q) : (eps(or L R))\<^sup>* = (\<exists>r. q = True#r \<and> (p,r) : (eps L)\<^sup>*)"
|
||||
by (blast dest: lemma1a lemma2a)
|
||||
|
||||
lemma False_epsclosure_or[iff]:
|
||||
"(False#p,q) : (eps(or L R))\<^sup>* = (\<exists>r. q = False#r \<and> (p,r) : (eps R)\<^sup>*)"
|
||||
by (blast dest: lemma1b lemma2b)
|
||||
|
||||
(***** lift True/False over steps *****)
|
||||
|
||||
lemma lift_True_over_steps_or[iff]:
|
||||
"\<And>p. (True#p,q):steps (or L R) w = (\<exists>r. q = True # r \<and> (p,r):steps L w)"
|
||||
apply (induct "w")
|
||||
apply auto
|
||||
apply force
|
||||
done
|
||||
|
||||
lemma lift_False_over_steps_or[iff]:
|
||||
"\<And>p. (False#p,q):steps (or L R) w = (\<exists>r. q = False#r \<and> (p,r):steps R w)"
|
||||
apply (induct "w")
|
||||
apply auto
|
||||
apply (force)
|
||||
done
|
||||
|
||||
(***** Epsilon closure of start state *****)
|
||||
|
||||
lemma unfold_rtrancl2:
|
||||
"R\<^sup>* = Id \<union> (R O R\<^sup>*)"
|
||||
apply (rule set_eqI)
|
||||
apply (simp)
|
||||
apply (rule iffI)
|
||||
apply (erule rtrancl_induct)
|
||||
apply (blast)
|
||||
apply (blast intro: rtrancl_into_rtrancl)
|
||||
apply (blast intro: converse_rtrancl_into_rtrancl)
|
||||
done
|
||||
|
||||
lemma in_unfold_rtrancl2:
|
||||
"(p,q) : R\<^sup>* = (q = p | (\<exists>r. (p,r) : R \<and> (r,q) : R\<^sup>*))"
|
||||
apply (rule unfold_rtrancl2[THEN equalityE])
|
||||
apply (blast)
|
||||
done
|
||||
|
||||
lemmas [iff] = in_unfold_rtrancl2[where ?p = "start(or L R)"] for L R
|
||||
|
||||
lemma start_eps_or[iff]:
|
||||
"\<And>L R. (start(or L R),q) : eps(or L R) =
|
||||
(q = True#start L | q = False#start R)"
|
||||
by (simp add:or_def step_def)
|
||||
|
||||
lemma not_start_step_or_Some[iff]:
|
||||
"\<And>L R. (start(or L R),q) \<notin> step (or L R) (Some a)"
|
||||
by (simp add:or_def step_def)
|
||||
|
||||
lemma steps_or:
|
||||
"(start(or L R), q) : steps (or L R) w =
|
||||
( (w = [] \<and> q = start(or L R)) |
|
||||
(\<exists>p. q = True # p \<and> (start L,p) : steps L w |
|
||||
q = False # p \<and> (start R,p) : steps R w) )"
|
||||
apply (case_tac "w")
|
||||
apply (simp)
|
||||
apply (blast)
|
||||
apply (simp)
|
||||
apply (blast)
|
||||
done
|
||||
|
||||
lemma start_or_not_final[iff]:
|
||||
"\<And>L R. \<not> fin (or L R) (start(or L R))"
|
||||
by (simp add:or_def)
|
||||
|
||||
lemma accepts_or:
|
||||
"accepts (or L R) w = (accepts L w | accepts R w)"
|
||||
apply (simp add:accepts_def steps_or)
|
||||
apply auto
|
||||
done
|
||||
|
||||
|
||||
(******************************************************)
|
||||
(* conc *)
|
||||
(******************************************************)
|
||||
|
||||
(** True/False in fin **)
|
||||
|
||||
lemma in_conc_True[iff]:
|
||||
"\<And>L R. fin (conc L R) (True#p) = False"
|
||||
by (simp add:conc_def)
|
||||
|
||||
lemma fin_conc_False[iff]:
|
||||
"\<And>L R. fin (conc L R) (False#p) = fin R p"
|
||||
by (simp add:conc_def)
|
||||
|
||||
(** True/False in step **)
|
||||
|
||||
lemma True_step_conc[iff]:
|
||||
"\<And>L R. (True#p,q) : step (conc L R) a =
|
||||
((\<exists>r. q=True#r \<and> (p,r): step L a) |
|
||||
(fin L p \<and> a=None \<and> q=False#start R))"
|
||||
by (simp add:conc_def step_def) (blast)
|
||||
|
||||
lemma False_step_conc[iff]:
|
||||
"\<And>L R. (False#p,q) : step (conc L R) a =
|
||||
(\<exists>r. q = False#r \<and> (p,r) : step R a)"
|
||||
by (simp add:conc_def step_def) (blast)
|
||||
|
||||
(** False in epsclosure **)
|
||||
|
||||
lemma lemma1b':
|
||||
"(tp,tq) : (eps(conc L R))\<^sup>* \<Longrightarrow>
|
||||
(\<And>p. tp = False#p \<Longrightarrow> \<exists>q. (p,q) : (eps R)\<^sup>* \<and> tq = False#q)"
|
||||
apply (induct rule: rtrancl_induct)
|
||||
apply (blast)
|
||||
apply (blast intro: rtrancl_into_rtrancl)
|
||||
done
|
||||
|
||||
lemma lemma2b':
|
||||
"(p,q) : (eps R)\<^sup>* \<Longrightarrow> (False#p, False#q) : (eps(conc L R))\<^sup>*"
|
||||
apply (induct rule: rtrancl_induct)
|
||||
apply (blast)
|
||||
apply (blast intro: rtrancl_into_rtrancl)
|
||||
done
|
||||
|
||||
lemma False_epsclosure_conc[iff]:
|
||||
"((False # p, q) : (eps (conc L R))\<^sup>*) =
|
||||
(\<exists>r. q = False # r \<and> (p, r) : (eps R)\<^sup>*)"
|
||||
apply (rule iffI)
|
||||
apply (blast dest: lemma1b')
|
||||
apply (blast dest: lemma2b')
|
||||
done
|
||||
|
||||
(** False in steps **)
|
||||
|
||||
lemma False_steps_conc[iff]:
|
||||
"\<And>p. (False#p,q): steps (conc L R) w = (\<exists>r. q=False#r \<and> (p,r): steps R w)"
|
||||
apply (induct "w")
|
||||
apply (simp)
|
||||
apply (simp)
|
||||
apply (fast) (*MUCH faster than blast*)
|
||||
done
|
||||
|
||||
(** True in epsclosure **)
|
||||
|
||||
lemma True_True_eps_concI:
|
||||
"(p,q): (eps L)\<^sup>* \<Longrightarrow> (True#p,True#q) : (eps(conc L R))\<^sup>*"
|
||||
apply (induct rule: rtrancl_induct)
|
||||
apply (blast)
|
||||
apply (blast intro: rtrancl_into_rtrancl)
|
||||
done
|
||||
|
||||
lemma True_True_steps_concI:
|
||||
"\<And>p. (p,q) : steps L w \<Longrightarrow> (True#p,True#q) : steps (conc L R) w"
|
||||
apply (induct "w")
|
||||
apply (simp add: True_True_eps_concI)
|
||||
apply (simp)
|
||||
apply (blast intro: True_True_eps_concI)
|
||||
done
|
||||
|
||||
lemma lemma1a':
|
||||
"(tp,tq) : (eps(conc L R))\<^sup>* \<Longrightarrow>
|
||||
(\<And>p. tp = True#p \<Longrightarrow>
|
||||
(\<exists>q. tq = True#q \<and> (p,q) : (eps L)\<^sup>*) |
|
||||
(\<exists>q r. tq = False#q \<and> (p,r):(eps L)\<^sup>* \<and> fin L r \<and> (start R,q) : (eps R)\<^sup>*))"
|
||||
apply (induct rule: rtrancl_induct)
|
||||
apply (blast)
|
||||
apply (blast intro: rtrancl_into_rtrancl)
|
||||
done
|
||||
|
||||
lemma lemma2a':
|
||||
"(p, q) : (eps L)\<^sup>* \<Longrightarrow> (True#p, True#q) : (eps(conc L R))\<^sup>*"
|
||||
apply (induct rule: rtrancl_induct)
|
||||
apply (blast)
|
||||
apply (blast intro: rtrancl_into_rtrancl)
|
||||
done
|
||||
|
||||
lemma lem:
|
||||
"\<And>L R. (p,q) : step R None \<Longrightarrow> (False#p, False#q) : step (conc L R) None"
|
||||
by(simp add: conc_def step_def)
|
||||
|
||||
lemma lemma2b'':
|
||||
"(p,q) : (eps R)\<^sup>* \<Longrightarrow> (False#p, False#q) : (eps(conc L R))\<^sup>*"
|
||||
apply (induct rule: rtrancl_induct)
|
||||
apply (blast)
|
||||
apply (drule lem)
|
||||
apply (blast intro: rtrancl_into_rtrancl)
|
||||
done
|
||||
|
||||
lemma True_False_eps_concI:
|
||||
"\<And>L R. fin L p \<Longrightarrow> (True#p, False#start R) : eps(conc L R)"
|
||||
by(simp add: conc_def step_def)
|
||||
|
||||
lemma True_epsclosure_conc[iff]:
|
||||
"((True#p,q) \<in> (eps(conc L R))\<^sup>*) =
|
||||
((\<exists>r. (p,r) \<in> (eps L)\<^sup>* \<and> q = True#r) \<or>
|
||||
(\<exists>r. (p,r) \<in> (eps L)\<^sup>* \<and> fin L r \<and>
|
||||
(\<exists>s. (start R, s) \<in> (eps R)\<^sup>* \<and> q = False#s)))"
|
||||
apply (rule iffI)
|
||||
apply (blast dest: lemma1a')
|
||||
apply (erule disjE)
|
||||
apply (blast intro: lemma2a')
|
||||
apply (clarify)
|
||||
apply (rule rtrancl_trans)
|
||||
apply (erule lemma2a')
|
||||
apply (rule converse_rtrancl_into_rtrancl)
|
||||
apply (erule True_False_eps_concI)
|
||||
apply (erule lemma2b'')
|
||||
done
|
||||
|
||||
(** True in steps **)
|
||||
|
||||
lemma True_steps_concD[rule_format]:
|
||||
"\<forall>p. (True#p,q) : steps (conc L R) w \<longrightarrow>
|
||||
((\<exists>r. (p,r) : steps L w \<and> q = True#r) \<or>
|
||||
(\<exists>u v. w = u@v \<and> (\<exists>r. (p,r) \<in> steps L u \<and> fin L r \<and>
|
||||
(\<exists>s. (start R,s) \<in> steps R v \<and> q = False#s))))"
|
||||
apply (induct "w")
|
||||
apply (simp)
|
||||
apply (simp)
|
||||
apply (clarify del: disjCI)
|
||||
apply (erule disjE)
|
||||
apply (clarify del: disjCI)
|
||||
apply (erule disjE)
|
||||
apply (clarify del: disjCI)
|
||||
apply (erule allE, erule impE, assumption)
|
||||
apply (erule disjE)
|
||||
apply (blast)
|
||||
apply (rule disjI2)
|
||||
apply (clarify)
|
||||
apply (simp)
|
||||
apply (rule_tac x = "a#u" in exI)
|
||||
apply (simp)
|
||||
apply (blast)
|
||||
apply (blast)
|
||||
apply (rule disjI2)
|
||||
apply (clarify)
|
||||
apply (simp)
|
||||
apply (rule_tac x = "[]" in exI)
|
||||
apply (simp)
|
||||
apply (blast)
|
||||
done
|
||||
|
||||
lemma True_steps_conc:
|
||||
"(True#p,q) \<in> steps (conc L R) w =
|
||||
((\<exists>r. (p,r) \<in> steps L w \<and> q = True#r) |
|
||||
(\<exists>u v. w = u@v \<and> (\<exists>r. (p,r) : steps L u \<and> fin L r \<and>
|
||||
(\<exists>s. (start R,s) : steps R v \<and> q = False#s))))"
|
||||
by (blast dest: True_steps_concD
|
||||
intro: True_True_steps_concI in_steps_epsclosure)
|
||||
|
||||
(** starting from the start **)
|
||||
|
||||
lemma start_conc:
|
||||
"\<And>L R. start(conc L R) = True#start L"
|
||||
by (simp add: conc_def)
|
||||
|
||||
lemma final_conc:
|
||||
"\<And>L R. fin(conc L R) p = (\<exists>s. p = False#s \<and> fin R s)"
|
||||
by (simp add:conc_def split: list.split)
|
||||
|
||||
lemma accepts_conc:
|
||||
"accepts (conc L R) w = (\<exists>u v. w = u@v \<and> accepts L u \<and> accepts R v)"
|
||||
apply (simp add: accepts_def True_steps_conc final_conc start_conc)
|
||||
apply (blast)
|
||||
done
|
||||
|
||||
(******************************************************)
|
||||
(* star *)
|
||||
(******************************************************)
|
||||
|
||||
lemma True_in_eps_star[iff]:
|
||||
"\<And>A. (True#p,q) \<in> eps(star A) =
|
||||
( (\<exists>r. q = True#r \<and> (p,r) \<in> eps A) \<or> (fin A p \<and> q = True#start A) )"
|
||||
by (simp add:star_def step_def) (blast)
|
||||
|
||||
lemma True_True_step_starI:
|
||||
"\<And>A. (p,q) : step A a \<Longrightarrow> (True#p, True#q) : step (star A) a"
|
||||
by (simp add:star_def step_def)
|
||||
|
||||
lemma True_True_eps_starI:
|
||||
"(p,r) : (eps A)\<^sup>* \<Longrightarrow> (True#p, True#r) : (eps(star A))\<^sup>*"
|
||||
apply (induct rule: rtrancl_induct)
|
||||
apply (blast)
|
||||
apply (blast intro: True_True_step_starI rtrancl_into_rtrancl)
|
||||
done
|
||||
|
||||
lemma True_start_eps_starI:
|
||||
"\<And>A. fin A p \<Longrightarrow> (True#p,True#start A) : eps(star A)"
|
||||
by (simp add:star_def step_def)
|
||||
|
||||
lemma lem':
|
||||
"(tp,s) : (eps(star A))\<^sup>* \<Longrightarrow> (\<forall>p. tp = True#p \<longrightarrow>
|
||||
(\<exists>r. ((p,r) \<in> (eps A)\<^sup>* \<or>
|
||||
(\<exists>q. (p,q) \<in> (eps A)\<^sup>* \<and> fin A q \<and> (start A,r) : (eps A)\<^sup>*)) \<and>
|
||||
s = True#r))"
|
||||
apply (induct rule: rtrancl_induct)
|
||||
apply (simp)
|
||||
apply (clarify)
|
||||
apply (simp)
|
||||
apply (blast intro: rtrancl_into_rtrancl)
|
||||
done
|
||||
|
||||
lemma True_eps_star[iff]:
|
||||
"((True#p,s) \<in> (eps(star A))\<^sup>*) =
|
||||
(\<exists>r. ((p,r) \<in> (eps A)\<^sup>* \<or>
|
||||
(\<exists>q. (p,q) : (eps A)\<^sup>* \<and> fin A q \<and> (start A,r) : (eps A)\<^sup>*)) \<and>
|
||||
s = True#r)"
|
||||
apply (rule iffI)
|
||||
apply (drule lem')
|
||||
apply (blast)
|
||||
(* Why can't blast do the rest? *)
|
||||
apply (clarify)
|
||||
apply (erule disjE)
|
||||
apply (erule True_True_eps_starI)
|
||||
apply (clarify)
|
||||
apply (rule rtrancl_trans)
|
||||
apply (erule True_True_eps_starI)
|
||||
apply (rule rtrancl_trans)
|
||||
apply (rule r_into_rtrancl)
|
||||
apply (erule True_start_eps_starI)
|
||||
apply (erule True_True_eps_starI)
|
||||
done
|
||||
|
||||
(** True in step Some **)
|
||||
|
||||
lemma True_step_star[iff]:
|
||||
"\<And>A. (True#p,r) \<in> step (star A) (Some a) =
|
||||
(\<exists>q. (p,q) \<in> step A (Some a) \<and> r=True#q)"
|
||||
by (simp add:star_def step_def) (blast)
|
||||
|
||||
|
||||
(** True in steps **)
|
||||
|
||||
(* reverse list induction! Complicates matters for conc? *)
|
||||
lemma True_start_steps_starD[rule_format]:
|
||||
"\<forall>rr. (True#start A,rr) \<in> steps (star A) w \<longrightarrow>
|
||||
(\<exists>us v. w = concat us @ v \<and>
|
||||
(\<forall>u\<in>set us. accepts A u) \<and>
|
||||
(\<exists>r. (start A,r) \<in> steps A v \<and> rr = True#r))"
|
||||
apply (induct w rule: rev_induct)
|
||||
apply (simp)
|
||||
apply (clarify)
|
||||
apply (rule_tac x = "[]" in exI)
|
||||
apply (erule disjE)
|
||||
apply (simp)
|
||||
apply (clarify)
|
||||
apply (simp)
|
||||
apply (simp add: O_assoc[symmetric] epsclosure_steps)
|
||||
apply (clarify)
|
||||
apply (erule allE, erule impE, assumption)
|
||||
apply (clarify)
|
||||
apply (erule disjE)
|
||||
apply (rule_tac x = "us" in exI)
|
||||
apply (rule_tac x = "v@[x]" in exI)
|
||||
apply (simp add: O_assoc[symmetric] epsclosure_steps)
|
||||
apply (blast)
|
||||
apply (clarify)
|
||||
apply (rule_tac x = "us@[v@[x]]" in exI)
|
||||
apply (rule_tac x = "[]" in exI)
|
||||
apply (simp add: accepts_def)
|
||||
apply (blast)
|
||||
done
|
||||
|
||||
lemma True_True_steps_starI:
|
||||
"\<And>p. (p,q) : steps A w \<Longrightarrow> (True#p,True#q) : steps (star A) w"
|
||||
apply (induct "w")
|
||||
apply (simp)
|
||||
apply (simp)
|
||||
apply (blast intro: True_True_eps_starI True_True_step_starI)
|
||||
done
|
||||
|
||||
lemma steps_star_cycle:
|
||||
"(\<forall>u \<in> set us. accepts A u) \<Longrightarrow>
|
||||
(True#start A,True#start A) \<in> steps (star A) (concat us)"
|
||||
apply (induct "us")
|
||||
apply (simp add:accepts_def)
|
||||
apply (simp add:accepts_def)
|
||||
by(blast intro: True_True_steps_starI True_start_eps_starI in_epsclosure_steps)
|
||||
|
||||
(* Better stated directly with start(star A)? Loop in star A back to start(star A)?*)
|
||||
lemma True_start_steps_star:
|
||||
"(True#start A,rr) : steps (star A) w =
|
||||
(\<exists>us v. w = concat us @ v \<and>
|
||||
(\<forall>u\<in>set us. accepts A u) \<and>
|
||||
(\<exists>r. (start A,r) \<in> steps A v \<and> rr = True#r))"
|
||||
apply (rule iffI)
|
||||
apply (erule True_start_steps_starD)
|
||||
apply (clarify)
|
||||
apply (blast intro: steps_star_cycle True_True_steps_starI)
|
||||
done
|
||||
|
||||
(** the start state **)
|
||||
|
||||
lemma start_step_star[iff]:
|
||||
"\<And>A. (start(star A),r) : step (star A) a = (a=None \<and> r = True#start A)"
|
||||
by (simp add:star_def step_def)
|
||||
|
||||
lemmas epsclosure_start_step_star =
|
||||
in_unfold_rtrancl2[where ?p = "start (star A)"] for A
|
||||
|
||||
lemma start_steps_star:
|
||||
"(start(star A),r) : steps (star A) w =
|
||||
((w=[] \<and> r= start(star A)) | (True#start A,r) : steps (star A) w)"
|
||||
apply (rule iffI)
|
||||
apply (case_tac "w")
|
||||
apply (simp add: epsclosure_start_step_star)
|
||||
apply (simp)
|
||||
apply (clarify)
|
||||
apply (simp add: epsclosure_start_step_star)
|
||||
apply (blast)
|
||||
apply (erule disjE)
|
||||
apply (simp)
|
||||
apply (blast intro: in_steps_epsclosure)
|
||||
done
|
||||
|
||||
lemma fin_star_True[iff]: "\<And>A. fin (star A) (True#p) = fin A p"
|
||||
by (simp add:star_def)
|
||||
|
||||
lemma fin_star_start[iff]: "\<And>A. fin (star A) (start(star A))"
|
||||
by (simp add:star_def)
|
||||
|
||||
(* too complex! Simpler if loop back to start(star A)? *)
|
||||
lemma accepts_star:
|
||||
"accepts (star A) w =
|
||||
(\<exists>us. (\<forall>u \<in> set(us). accepts A u) \<and> (w = concat us))"
|
||||
apply(unfold accepts_def)
|
||||
apply (simp add: start_steps_star True_start_steps_star)
|
||||
apply (rule iffI)
|
||||
apply (clarify)
|
||||
apply (erule disjE)
|
||||
apply (clarify)
|
||||
apply (simp)
|
||||
apply (rule_tac x = "[]" in exI)
|
||||
apply (simp)
|
||||
apply (clarify)
|
||||
apply (rule_tac x = "us@[v]" in exI)
|
||||
apply (simp add: accepts_def)
|
||||
apply (blast)
|
||||
apply (clarify)
|
||||
apply (rule_tac xs = "us" in rev_exhaust)
|
||||
apply (simp)
|
||||
apply (blast)
|
||||
apply (clarify)
|
||||
apply (simp add: accepts_def)
|
||||
apply (blast)
|
||||
done
|
||||
|
||||
|
||||
(***** Correctness of r2n *****)
|
||||
|
||||
lemma accepts_rexp2nae:
|
||||
"\<And>w. accepts (rexp2nae r) w = (w : lang r)"
|
||||
apply (induct "r")
|
||||
apply (simp add: accepts_def)
|
||||
apply simp
|
||||
apply (simp add: accepts_atom)
|
||||
apply (simp add: accepts_or)
|
||||
apply (simp add: accepts_conc Regular_Set.conc_def)
|
||||
apply (simp add: accepts_star in_star_iff_concat subset_iff Ball_def)
|
||||
done
|
||||
|
||||
end
|
||||
|
|
@ -1,233 +0,0 @@
|
|||
(* Author: Tobias Nipkow
|
||||
Copyright 1998 TUM
|
||||
|
||||
To generate a regular expression, the alphabet must be finite.
|
||||
regexp needs to be supplied with an 'a list for a unique order
|
||||
|
||||
add_Atom d i j r a = (if d a i = j then Union r (Atom a) else r)
|
||||
atoms d i j as = foldl (add_Atom d i j) Empty as
|
||||
|
||||
regexp as d i j 0 = (if i=j then Union (Star Empty) (atoms d i j as)
|
||||
else atoms d i j as
|
||||
*)
|
||||
|
||||
section "From deterministic automata to regular sets"
|
||||
|
||||
theory RegSet_of_nat_DA
|
||||
imports "Regular-Sets.Regular_Set" DA
|
||||
begin
|
||||
|
||||
type_synonym 'a nat_next = "'a \<Rightarrow> nat \<Rightarrow> nat"
|
||||
|
||||
abbreviation
|
||||
deltas :: "'a nat_next \<Rightarrow> 'a list \<Rightarrow> nat \<Rightarrow> nat" where
|
||||
"deltas \<equiv> foldl2"
|
||||
|
||||
primrec trace :: "'a nat_next \<Rightarrow> nat \<Rightarrow> 'a list \<Rightarrow> nat list" where
|
||||
"trace d i [] = []" |
|
||||
"trace d i (x#xs) = d x i # trace d (d x i) xs"
|
||||
|
||||
(* conversion a la Warshall *)
|
||||
|
||||
primrec regset :: "'a nat_next \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> 'a list set" where
|
||||
"regset d i j 0 = (if i=j then insert [] {[a] | a. d a i = j}
|
||||
else {[a] | a. d a i = j})" |
|
||||
"regset d i j (Suc k) =
|
||||
regset d i j k \<union>
|
||||
(regset d i k k) @@ (star(regset d k k k)) @@ (regset d k j k)"
|
||||
|
||||
definition
|
||||
regset_of_DA :: "('a,nat)da \<Rightarrow> nat \<Rightarrow> 'a list set" where
|
||||
"regset_of_DA A k = (\<Union>j\<in>{j. j<k \<and> fin A j}. regset (next A) (start A) j k)"
|
||||
|
||||
definition
|
||||
bounded :: "'a nat_next \<Rightarrow> nat \<Rightarrow> bool" where
|
||||
"bounded d k = (\<forall>n. n < k \<longrightarrow> (\<forall>x. d x n < k))"
|
||||
|
||||
declare
|
||||
in_set_butlast_appendI[simp,intro] less_SucI[simp] image_eqI[simp]
|
||||
|
||||
(* Lists *)
|
||||
|
||||
lemma butlast_empty[iff]:
|
||||
"(butlast xs = []) = (case xs of [] \<Rightarrow> True | y#ys \<Rightarrow> ys=[])"
|
||||
by (cases xs) simp_all
|
||||
|
||||
lemma in_set_butlast_concatI:
|
||||
"x:set(butlast xs) \<Longrightarrow> xs:set xss \<Longrightarrow> x:set(butlast(concat xss))"
|
||||
apply (induct "xss")
|
||||
apply simp
|
||||
apply (simp add: butlast_append del: ball_simps)
|
||||
apply (rule conjI)
|
||||
apply (clarify)
|
||||
apply (erule disjE)
|
||||
apply (blast)
|
||||
apply (subgoal_tac "xs=[]")
|
||||
apply simp
|
||||
apply (blast)
|
||||
apply (blast dest: in_set_butlastD)
|
||||
done
|
||||
|
||||
(* Regular sets *)
|
||||
|
||||
(* The main lemma:
|
||||
how to decompose a trace into a prefix, a list of loops and a suffix.
|
||||
*)
|
||||
lemma decompose[rule_format]:
|
||||
"\<forall>i. k \<in> set(trace d i xs) \<longrightarrow> (\<exists>pref mids suf.
|
||||
xs = pref @ concat mids @ suf \<and>
|
||||
deltas d pref i = k \<and> (\<forall>n\<in>set(butlast(trace d i pref)). n \<noteq> k) \<and>
|
||||
(\<forall>mid\<in>set mids. (deltas d mid k = k) \<and>
|
||||
(\<forall>n\<in>set(butlast(trace d k mid)). n \<noteq> k)) \<and>
|
||||
(\<forall>n\<in>set(butlast(trace d k suf)). n \<noteq> k))"
|
||||
apply (induct "xs")
|
||||
apply (simp)
|
||||
apply (rename_tac a as)
|
||||
apply (intro strip)
|
||||
apply (case_tac "d a i = k")
|
||||
apply (rule_tac x = "[a]" in exI)
|
||||
apply simp
|
||||
apply (case_tac "k : set(trace d (d a i) as)")
|
||||
apply (erule allE)
|
||||
apply (erule impE)
|
||||
apply (assumption)
|
||||
apply (erule exE)+
|
||||
apply (rule_tac x = "pref#mids" in exI)
|
||||
apply (rule_tac x = "suf" in exI)
|
||||
apply simp
|
||||
apply (rule_tac x = "[]" in exI)
|
||||
apply (rule_tac x = "as" in exI)
|
||||
apply simp
|
||||
apply (blast dest: in_set_butlastD)
|
||||
apply simp
|
||||
apply (erule allE)
|
||||
apply (erule impE)
|
||||
apply (assumption)
|
||||
apply (erule exE)+
|
||||
apply (rule_tac x = "a#pref" in exI)
|
||||
apply (rule_tac x = "mids" in exI)
|
||||
apply (rule_tac x = "suf" in exI)
|
||||
apply simp
|
||||
done
|
||||
|
||||
lemma length_trace[simp]: "\<And>i. length(trace d i xs) = length xs"
|
||||
by (induct "xs") simp_all
|
||||
|
||||
lemma deltas_append[simp]:
|
||||
"\<And>i. deltas d (xs@ys) i = deltas d ys (deltas d xs i)"
|
||||
by (induct "xs") simp_all
|
||||
|
||||
lemma trace_append[simp]:
|
||||
"\<And>i. trace d i (xs@ys) = trace d i xs @ trace d (deltas d xs i) ys"
|
||||
by (induct "xs") simp_all
|
||||
|
||||
lemma trace_concat[simp]:
|
||||
"(\<forall>xs \<in> set xss. deltas d xs i = i) \<Longrightarrow>
|
||||
trace d i (concat xss) = concat (map (trace d i) xss)"
|
||||
by (induct "xss") simp_all
|
||||
|
||||
lemma trace_is_Nil[simp]: "\<And>i. (trace d i xs = []) = (xs = [])"
|
||||
by (case_tac "xs") simp_all
|
||||
|
||||
lemma trace_is_Cons_conv[simp]:
|
||||
"(trace d i xs = n#ns) =
|
||||
(case xs of [] \<Rightarrow> False | y#ys \<Rightarrow> n = d y i \<and> ns = trace d n ys)"
|
||||
apply (case_tac "xs")
|
||||
apply simp_all
|
||||
apply (blast)
|
||||
done
|
||||
|
||||
lemma set_trace_conv:
|
||||
"\<And>i. set(trace d i xs) =
|
||||
(if xs=[] then {} else insert(deltas d xs i)(set(butlast(trace d i xs))))"
|
||||
apply (induct "xs")
|
||||
apply (simp)
|
||||
apply (simp add: insert_commute)
|
||||
done
|
||||
|
||||
lemma deltas_concat[simp]:
|
||||
"(\<forall>mid\<in>set mids. deltas d mid k = k) \<Longrightarrow> deltas d (concat mids) k = k"
|
||||
by (induct mids) simp_all
|
||||
|
||||
lemma lem: "[| n < Suc k; n \<noteq> k |] ==> n < k"
|
||||
by arith
|
||||
|
||||
lemma regset_spec:
|
||||
"\<And>i j xs. xs \<in> regset d i j k =
|
||||
((\<forall>n\<in>set(butlast(trace d i xs)). n < k) \<and> deltas d xs i = j)"
|
||||
apply (induct k)
|
||||
apply(simp split: list.split)
|
||||
apply(fastforce)
|
||||
apply (simp add: conc_def)
|
||||
apply (rule iffI)
|
||||
apply (erule disjE)
|
||||
apply simp
|
||||
apply (erule exE conjE)+
|
||||
apply simp
|
||||
apply (subgoal_tac
|
||||
"(\<forall>m\<in>set(butlast(trace d k xsb)). m < Suc k) \<and> deltas d xsb k = k")
|
||||
apply (simp add: set_trace_conv butlast_append ball_Un)
|
||||
apply (erule star_induct)
|
||||
apply (simp)
|
||||
apply (simp add: set_trace_conv butlast_append ball_Un)
|
||||
apply (case_tac "k : set(butlast(trace d i xs))")
|
||||
prefer 2 apply (rule disjI1)
|
||||
apply (blast intro:lem)
|
||||
apply (rule disjI2)
|
||||
apply (drule in_set_butlastD[THEN decompose])
|
||||
apply (clarify)
|
||||
apply (rule_tac x = "pref" in exI)
|
||||
apply simp
|
||||
apply (rule conjI)
|
||||
apply (rule ballI)
|
||||
apply (rule lem)
|
||||
prefer 2 apply simp
|
||||
apply (drule bspec) prefer 2 apply assumption
|
||||
apply simp
|
||||
apply (rule_tac x = "concat mids" in exI)
|
||||
apply (simp)
|
||||
apply (rule conjI)
|
||||
apply (rule concat_in_star)
|
||||
apply (clarsimp simp: subset_iff)
|
||||
apply (rule lem)
|
||||
prefer 2 apply simp
|
||||
apply (drule bspec) prefer 2 apply assumption
|
||||
apply (simp add: image_eqI in_set_butlast_concatI)
|
||||
apply (rule ballI)
|
||||
apply (rule lem)
|
||||
apply auto
|
||||
done
|
||||
|
||||
lemma trace_below:
|
||||
"bounded d k \<Longrightarrow> \<forall>i. i < k \<longrightarrow> (\<forall>n\<in>set(trace d i xs). n < k)"
|
||||
apply (unfold bounded_def)
|
||||
apply (induct "xs")
|
||||
apply simp
|
||||
apply (simp (no_asm))
|
||||
apply (blast)
|
||||
done
|
||||
|
||||
lemma regset_below:
|
||||
"[| bounded d k; i < k; j < k |] ==>
|
||||
regset d i j k = {xs. deltas d xs i = j}"
|
||||
apply (rule set_eqI)
|
||||
apply (simp add: regset_spec)
|
||||
apply (blast dest: trace_below in_set_butlastD)
|
||||
done
|
||||
|
||||
lemma deltas_below:
|
||||
"\<And>i. bounded d k \<Longrightarrow> i < k \<Longrightarrow> deltas d w i < k"
|
||||
apply (unfold bounded_def)
|
||||
apply (induct "w")
|
||||
apply simp_all
|
||||
done
|
||||
|
||||
lemma regset_DA_equiv:
|
||||
"[| bounded (next A) k; start A < k; j < k |] ==>
|
||||
w : regset_of_DA A k = accepts A w"
|
||||
apply(unfold regset_of_DA_def)
|
||||
apply (simp cong: conj_cong
|
||||
add: regset_below deltas_below accepts_def delta_def)
|
||||
done
|
||||
|
||||
end
|
||||
|
|
@ -1,6 +0,0 @@
|
|||
@inproceedings{Nipkow-TPHOLs98,author={Tobias Nipkow},
|
||||
title={Verified Lexical Analysis},
|
||||
booktitle={Theorem Proving in Higher Order Logics},
|
||||
editor={J. Grundy and M. Newey},
|
||||
publisher=Springer,series=LNCS,volume={1479},pages={1--15},year=1998,
|
||||
note={\url{http://www4.informatik.tu-muenchen.de/~nipkow/pubs/tphols98.html}}}
|
||||
|
|
@ -1,54 +0,0 @@
|
|||
|
||||
|
||||
\documentclass[11pt,a4paper]{article}
|
||||
\usepackage{isabelle,isabellesym}
|
||||
|
||||
|
||||
% this should be the last package used
|
||||
\usepackage{pdfsetup}
|
||||
|
||||
\begin{document}
|
||||
|
||||
\title{Functional Automata}
|
||||
\author{Tobias Nipkow}
|
||||
\maketitle
|
||||
|
||||
\begin{abstract}
|
||||
This theory defines deterministic and nondeterministic automata in a
|
||||
functional representation: the transition function/relation and the finality
|
||||
predicate are just functions. Hence the state space may be infinite. It is
|
||||
shown how to convert regular expressions into such automata. A scanner
|
||||
(generator) is implemented with the help of functional automata: the scanner
|
||||
chops the input up into longest recognized substrings. Finally we also show
|
||||
how to convert a certain subclass of functional automata (essentially the
|
||||
finite deterministic ones) into regular sets.
|
||||
\end{abstract}
|
||||
|
||||
\section{Overview}
|
||||
|
||||
The theories are structured as follows:
|
||||
\begin{itemize}
|
||||
\item Automata:
|
||||
\texttt{AutoProj}, \texttt{NA}, \texttt{NAe}, \texttt{DA}, \texttt{Automata}
|
||||
\item Conversion of regular expressions into automata:\\
|
||||
\texttt{RegExp2NA}, \texttt{RegExp2NAe}, \texttt{AutoRegExp}.
|
||||
\item Scanning: \texttt{MaxPrefix}, \texttt{MaxChop}, \texttt{AutoMaxChop}.
|
||||
\end{itemize}
|
||||
For a full description see \cite{Nipkow-TPHOLs98}.
|
||||
|
||||
In contrast to that paper, the latest version of the theories provides a
|
||||
fully executable scanner generator. The non-executable bits (transitive
|
||||
closure) have been eliminated by going from regular expressions directly to
|
||||
nondeterministic automata, thus bypassing epsilon-moves.
|
||||
|
||||
Not described in the paper is the conversion of certain functional automata
|
||||
(essentially the finite deterministic ones) into regular sets contained in
|
||||
\texttt{RegSet\_of\_nat\_DA}.
|
||||
|
||||
% include generated text of all theories
|
||||
\input{session}
|
||||
|
||||
\bibliographystyle{abbrv}
|
||||
\bibliography{root}
|
||||
|
||||
\end{document}
|
||||
Loading…
Reference in New Issue