diff --git a/AFP-contribs/Functional-Automata/AutoMaxChop.thy b/AFP-contribs/Functional-Automata/AutoMaxChop.thy new file mode 100644 index 0000000..78ceffb --- /dev/null +++ b/AFP-contribs/Functional-Automata/AutoMaxChop.thy @@ -0,0 +1,52 @@ +(* Author: Tobias Nipkow + Copyright 1998 TUM +*) + +section "Automata based scanner" + +theory AutoMaxChop +imports DA MaxChop +begin + +primrec auto_split :: "('a,'s)da => 's => 'a list * 'a list => 'a list => '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 => 'a chopper" where +"auto_chop A = chop (%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: + "!!q ps res. auto_split A (delta A ps q) res ps xs = + maxsplit (%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) (%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 diff --git a/AFP-contribs/Functional-Automata/AutoProj.thy b/AFP-contribs/Functional-Automata/AutoProj.thy new file mode 100644 index 0000000..7facc84 --- /dev/null +++ b/AFP-contribs/Functional-Automata/AutoProj.thy @@ -0,0 +1,29 @@ +(* 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 => 'a" where "start A = fst A" +definition "next" :: "'a * 'b * 'c => 'b" where "next A = fst(snd(A))" +definition fin :: "'a * 'b * 'c => '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 diff --git a/AFP-contribs/Functional-Automata/AutoRegExp.thy b/AFP-contribs/Functional-Automata/AutoRegExp.thy new file mode 100644 index 0000000..fe6612c --- /dev/null +++ b/AFP-contribs/Functional-Automata/AutoRegExp.thy @@ -0,0 +1,17 @@ +(* 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 diff --git a/AFP-contribs/Functional-Automata/Automata.thy b/AFP-contribs/Functional-Automata/Automata.thy new file mode 100644 index 0000000..d9ad882 --- /dev/null +++ b/AFP-contribs/Functional-Automata/Automata.thy @@ -0,0 +1,55 @@ +(* Author: Tobias Nipkow + Copyright 1998 TUM +*) + +section "Conversions between automata" + +theory Automata +imports DA NAe +begin + +definition + na2da :: "('a,'s)na => ('a,'s set)da" where +"na2da A = ({start A}, %a Q. Union(next A a ` Q), %Q. ? q:Q. fin A q)" + +definition + nae2da :: "('a,'s)nae => ('a,'s set)da" where +"nae2da A = ({start A}, + %a Q. Union(next A (Some a) ` ((eps A)^* `` Q)), + %Q. ? p: (eps A)^* `` Q. fin A p)" + +(*** Equivalence of NA and DA ***) + +lemma DA_delta_is_lift_NA_delta: + "!!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: + "!!Q. (eps A)^* `` (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 "!!Q. fin (nae2da A) Q = (EX q : (eps A)^* `` 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 diff --git a/AFP-contribs/Functional-Automata/DA.thy b/AFP-contribs/Functional-Automata/DA.thy new file mode 100644 index 0000000..b420b6a --- /dev/null +++ b/AFP-contribs/Functional-Automata/DA.thy @@ -0,0 +1,38 @@ +(* Author: Tobias Nipkow + Copyright 1998 TUM +*) + +section "Deterministic automata" + +theory DA +imports AutoProj +begin + +type_synonym ('a,'s)da = "'s * ('a => 's => 's) * ('s => bool)" + +definition + foldl2 :: "('a => 'b => 'b) => 'a list => 'b => 'b" where +"foldl2 f xs a = foldl (%a b. f b a) a xs" + +definition + delta :: "('a,'s)da => 'a list => 's => 's" where +"delta A = foldl2 (next A)" + +definition + accepts :: "('a,'s)da => 'a list => bool" where +"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 diff --git a/AFP-contribs/Functional-Automata/Execute.thy b/AFP-contribs/Functional-Automata/Execute.thy new file mode 100644 index 0000000..40b8e71 --- /dev/null +++ b/AFP-contribs/Functional-Automata/Execute.thy @@ -0,0 +1,20 @@ +(* Author: Lukas Bulwahn, TUM 2011 *) + +section {* Executing Automata and membership of Regular Expressions *} + +theory Execute +imports AutoRegExp +begin + +subsection {* Example *} + +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 diff --git a/AFP-contribs/Functional-Automata/Functional_Automata.thy b/AFP-contribs/Functional-Automata/Functional_Automata.thy new file mode 100644 index 0000000..8dd9c9f --- /dev/null +++ b/AFP-contribs/Functional-Automata/Functional_Automata.thy @@ -0,0 +1,5 @@ +theory Functional_Automata +imports AutoRegExp AutoMaxChop RegSet_of_nat_DA Execute +begin + +end diff --git a/AFP-contribs/Functional-Automata/MaxChop.thy b/AFP-contribs/Functional-Automata/MaxChop.thy new file mode 100644 index 0000000..ad272a7 --- /dev/null +++ b/AFP-contribs/Functional-Automata/MaxChop.thy @@ -0,0 +1,120 @@ +(* Author: Tobias Nipkow + Copyright 1998 TUM +*) + +section "Generic scanner" + +theory MaxChop +imports MaxPrefix +begin + +type_synonym 'a chopper = "'a list => 'a list list * 'a list" + +definition + is_maxchopper :: "('a list => bool) => 'a chopper => bool" where +"is_maxchopper P chopper = + (!xs zs yss. + (chopper(xs) = (yss,zs)) = + (xs = concat yss @ zs & (!ys : set yss. ys ~= []) & + (case yss of + [] => is_maxpref P [] xs + | us#uss => is_maxpref P us xs & chopper(concat(uss)@zs) = (uss,zs))))" + +definition + reducing :: "'a splitter => bool" where +"reducing splitf = + (!xs ys zs. splitf xs = (ys,zs) & ys ~= [] --> length zs < length xs)" + +function chop :: "'a splitter \ 'a list \ 'a list list \ '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 o snd)") +apply (auto simp: reducing_def) +apply (case_tac "splitf xs") +apply auto +done + +lemma chop_rule: "reducing splitf ==> + 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(%qs. maxsplit P ([],qs) [] qs)" +by (simp add: reducing_def maxsplit_eq) + +lemma is_maxsplitter_reducing: + "is_maxsplitter P splitf ==> reducing splitf" +by(simp add:is_maxsplitter_def reducing_def) + +lemma chop_concat[rule_format]: "is_maxsplitter P splitf ==> + (!yss zs. chop splitf xs = (yss,zs) --> 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 ==> + !yss zs. chop splitf xs = (yss,zs) --> (!ys : set yss. ys ~= [])" +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 diff --git a/AFP-contribs/Functional-Automata/MaxPrefix.thy b/AFP-contribs/Functional-Automata/MaxPrefix.thy new file mode 100644 index 0000000..a4c0534 --- /dev/null +++ b/AFP-contribs/Functional-Automata/MaxPrefix.thy @@ -0,0 +1,92 @@ +(* Author: Tobias Nipkow + Copyright 1998 TUM +*) + +section "Maximal prefix" + +theory MaxPrefix +imports "HOL-Library.Sublist" +begin + +definition + is_maxpref :: "('a list => bool) => 'a list => 'a list => bool" where +"is_maxpref P xs ys = + (prefix xs ys & (xs=[] | P xs) & (!zs. prefix zs ys & P zs --> prefix zs xs))" + +type_synonym 'a splitter = "'a list => 'a list * 'a list" + +definition + is_maxsplitter :: "('a list => bool) => 'a splitter => bool" where +"is_maxsplitter P f = + (!xs ps qs. f xs = (ps,qs) = (xs=ps@qs & is_maxpref P ps xs))" + +fun maxsplit :: "('a list => bool) => 'a list * 'a list => 'a list => '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 \us. prefix us qs \ P(ps@us) then xs@ys=ps@qs \ 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 "\us. prefix us qs & P ((ps @ [q]) @ us)") + case True + note ex1 = this + then guess us by (elim exE conjE) note us = this + hence ex2: "\us. prefix us (q # qs) & 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 "\us. prefix us (q#qs) & 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)) \ (xs = ps \ ys = q # qs)" + by (simp only: ex1 ex2) simp_all + also have "\ \ (xs @ ys = ps @ q # qs \ 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)) \ ((xs, ys) = res)" + by (simp only: ex1 ex2) simp + also have "\ \ (xs @ ys = ps @ q # qs \ 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]: + "\(\us. prefix us xs \ P us) \ is_maxpref P ps xs = (ps = [])" + by (auto simp: is_maxpref_def) + +lemma is_maxsplitter_maxsplit: + "is_maxsplitter P (%xs. maxsplit P ([],xs) [] xs)" + by (auto simp: maxsplit_lemma is_maxsplitter_def) + +lemmas maxsplit_eq = is_maxsplitter_maxsplit[simplified is_maxsplitter_def] + +end diff --git a/AFP-contribs/Functional-Automata/NA.thy b/AFP-contribs/Functional-Automata/NA.thy new file mode 100644 index 0000000..0c99f48 --- /dev/null +++ b/AFP-contribs/Functional-Automata/NA.thy @@ -0,0 +1,50 @@ +(* Author: Tobias Nipkow + Copyright 1998 TUM +*) + +section "Nondeterministic automata" + +theory NA +imports AutoProj +begin + +type_synonym ('a,'s) na = "'s * ('a => 's => 's set) * ('s => bool)" + +primrec delta :: "('a,'s)na => 'a list => 's => '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 => 'a list => bool" where +"accepts A w = (EX q : delta A w (start A). fin A q)" + +definition + step :: "('a,'s)na => 'a => ('s * 's)set" where +"step A a = {(p,q) . q : next A a p}" + +primrec steps :: "('a,'s)na => 'a list => ('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: "!!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 = (? q. (start A,q) : steps A w & fin A q)" +by(simp add: delta_conv_steps accepts_def) + +abbreviation + Cons_syn :: "'a => 'a list set => 'a list set" (infixr "##" 65) where + "x ## S == Cons x ` S" + +end diff --git a/AFP-contribs/Functional-Automata/NAe.thy b/AFP-contribs/Functional-Automata/NAe.thy new file mode 100644 index 0000000..72bb562 --- /dev/null +++ b/AFP-contribs/Functional-Automata/NAe.thy @@ -0,0 +1,72 @@ +(* 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 => ('s * 's)set" where + "eps A == step A None" + +primrec steps :: "('a,'s)nae => 'a list => ('s * 's)set" where +"steps A [] = (eps A)^*" | +"steps A (a#w) = (eps A)^* O step A (Some a) O steps A w" + +definition + accepts :: "('a,'s)nae => 'a list => bool" where +"accepts A w = (? q. (start A,q) : steps A w & fin A q)" + +(* not really used: +consts delta :: "('a,'s)nae => 'a list => 's => 's set" +primrec +"delta A [] s = (eps A)^* `` {s}" +"delta A (a#w) s = lift(delta A w) (lift(next A (Some a)) ((eps A)^* `` {s}))" +*) + +lemma steps_epsclosure[simp]: "(eps A)^* O steps A w = steps A w" +by (cases w) (simp_all add: O_assoc[symmetric]) + +lemma in_steps_epsclosure: + "[| (p,q) : (eps A)^*; (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)^* = 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)^* |] ==> (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 "(? x : f ` A. P x) = (? a:A. P(f x))" ?? * +Goal "!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 diff --git a/AFP-contribs/Functional-Automata/ROOT b/AFP-contribs/Functional-Automata/ROOT new file mode 100644 index 0000000..ad8c019 --- /dev/null +++ b/AFP-contribs/Functional-Automata/ROOT @@ -0,0 +1,13 @@ +chapter AFP + +session "Functional-Automata" (AFP) = "HOL-Library" + + options [timeout = 600] + sessions + "Regular-Sets" + theories [document = false] + "Regular-Sets.Regular_Exp" + theories + Functional_Automata + document_files + "root.bib" + "root.tex" diff --git a/AFP-contribs/Functional-Automata/RegExp2NA.thy b/AFP-contribs/Functional-Automata/RegExp2NA.thy new file mode 100644 index 0000000..0b9f149 --- /dev/null +++ b/AFP-contribs/Functional-Automata/RegExp2NA.thy @@ -0,0 +1,442 @@ +(* 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 => 'a bitsNA" where +"atom a = ([True], + %b s. if s=[True] & b=a then {[False]} else {}, + %s. s=[False])" + +definition + or :: "'a bitsNA => 'a bitsNA => 'a bitsNA" where +"or = (%(ql,dl,fl)(qr,dr,fr). + ([], + %a s. case s of + [] => (True ## dl a ql) Un (False ## dr a qr) + | left#s => if left then True ## dl a s + else False ## dr a s, + %s. case s of [] => (fl ql | fr qr) + | left#s => if left then fl s else fr s))" + +definition + conc :: "'a bitsNA => 'a bitsNA => 'a bitsNA" where +"conc = (%(ql,dl,fl)(qr,dr,fr). + (True#ql, + %a s. case s of + [] => {} + | left#s => if left then (True ## dl a s) Un + (if fl s then False ## dr a qr else {}) + else False ## dr a s, + %s. case s of [] => False | left#s => left & fl s & fr qr | ~left & fr s))" + +definition + epsilon :: "'a bitsNA" where +"epsilon = ([],%a s. {}, %s. s=[])" + +definition + plus :: "'a bitsNA => 'a bitsNA" where +"plus = (%(q,d,f). (q, %a s. d a s Un (if f s then d a q else {}), f))" + +definition + star :: "'a bitsNA => 'a bitsNA" where +"star A = or epsilon (plus A)" + +primrec rexp2na :: "'a rexp => 'a bitsNA" where +"rexp2na Zero = ([], %a s. {}, %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] & q=[False] & 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]: + "!!L R. fin (or L R) (True#p) = fin L p" +by(simp add:or_def) + +lemma fin_or_False[iff]: + "!!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]: +"!!L R. (True#p,q) : step (or L R) a = (? r. q = True#r & (p,r) : step L a)" +apply (simp add:or_def step_def) +apply blast +done + +lemma False_in_step_or[iff]: +"!!L R. (False#p,q) : step (or L R) a = (? r. q = False#r & (p,r) : 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]: + "!!p. (True#p,q):steps (or L R) w = (? r. q = True # r & (p,r):steps L w)" +apply (induct "w") + apply force +apply force +done + +lemma lift_False_over_steps_or[iff]: + "!!p. (False#p,q):steps (or L R) w = (? r. q = False#r & (p,r):steps R w)" +apply (induct "w") + apply force +apply force +done + +(** From the start **) + +lemma start_step_or[iff]: + "!!L R. (start(or L R),q) : step(or L R) a = + (? p. (q = True#p & (start L,p) : step L a) | + (q = False#p & (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 = [] & q = start(or L R)) | + (w ~= [] & (? p. q = True # p & (start L,p) : steps L w | + q = False # p & (start R,p) : steps R w)))" +apply (case_tac "w") + apply (simp) + apply blast +apply (simp) +apply blast +done + +lemma fin_start_or[iff]: + "!!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]: + "!!L R. fin (conc L R) (True#p) = (fin L p & fin R (start R))" +by(simp add:conc_def) + +lemma fin_conc_False[iff]: + "!!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]: + "!!L R. (True#p,q) : step (conc L R) a = + ((? r. q=True#r & (p,r): step L a) | + (fin L p & (? r. q=False#r & (start R,r) : step R a)))" +apply (simp add:conc_def step_def) +apply blast +done + +lemma False_step_conc[iff]: + "!!L R. (False#p,q) : step (conc L R) a = + (? r. q = False#r & (p,r) : step R a)" +apply (simp add:conc_def step_def) +apply blast +done + +(** False in steps **) + +lemma False_steps_conc[iff]: + "!!p. (False#p,q): steps (conc L R) w = (? r. q=False#r & (p,r): steps R w)" +apply (induct "w") + apply fastforce +apply force +done + +(** True in steps **) + +lemma True_True_steps_concI: + "!!L R p. (p,q) : steps L w ==> (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]: + "!!L R. (True#p,False#q) : step (conc L R) a = + (fin L p & (start R,q) : step R a)" +by simp + +lemma True_steps_concD[rule_format]: + "!p. (True#p,q) : steps (conc L R) w --> + ((? r. (p,r) : steps L w & q = True#r) | + (? u a v. w = u@a#v & + (? r. (p,r) : steps L u & fin L r & + (? s. (start R,s) : step R a & + (? t. (s,t) : steps R v & 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 = + ((? r. (p,r) : steps L w & q = True#r) | + (? u a v. w = u@a#v & + (? r. (p,r) : steps L u & fin L r & + (? s. (start R,s) : step R a & + (? t. (s,t) : steps R v & q = False#t)))))" +by(force dest!: True_steps_concD intro!: True_True_steps_concI) + +(** starting from the start **) + +lemma start_conc: + "!!L R. start(conc L R) = True#start L" +by (simp add:conc_def) + +lemma final_conc: + "!!L R. fin(conc L R) p = ((fin R (start R) & (? s. p = True#s & fin L s)) | + (? s. p = False#s & fin R s))" +apply (simp add:conc_def split: list.split) +apply blast +done + +lemma accepts_conc: + "accepts (conc L R) w = (? u v. w = u@v & accepts L u & 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=[] & 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]: "!!A. start (plus A) = start A" +by(simp add:plus_def) + +lemma fin_plus[iff]: "!!A. fin (plus A) = fin A" +by(simp add:plus_def) + +lemma step_plusI: + "!!A. (p,q) : step A a ==> (p,q) : step (plus A) a" +by(simp add:plus_def step_def) + +lemma steps_plusI: "!!p. (p,q) : steps A w ==> (p,q) : steps (plus A) w" +apply (induct "w") + apply simp +apply simp +apply (blast intro: step_plusI) +done + +lemma step_plus_conv[iff]: + "!!A. (p,r): step (plus A) a = + ( (p,r): step A a | fin A p & (start A,r) : step A a )" +by(simp add:plus_def step_def) + +lemma fin_steps_plusI: + "[| (start A,q) : steps A u; u ~= []; 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]: + "!r. (start A,r) : steps (plus A) w --> + (? us v. w = concat us @ v & + (!u:set us. accepts A u) & + (start A,r) : 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 ~= [] --> (!u : set us. accepts A u) --> 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 = + (? us. us ~= [] & w = concat us & (!u : 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 = (? us. (!u : set us. accepts A u) & 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: + "!!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 diff --git a/AFP-contribs/Functional-Automata/RegExp2NAe.thy b/AFP-contribs/Functional-Automata/RegExp2NAe.thy new file mode 100644 index 0000000..0dc669d --- /dev/null +++ b/AFP-contribs/Functional-Automata/RegExp2NAe.thy @@ -0,0 +1,641 @@ +(* 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 = ([],%a s. {}, %s. s=[])" + +definition +"atom" :: "'a => 'a bitsNAe" where +"atom a = ([True], + %b s. if s=[True] & b=Some a then {[False]} else {}, + %s. s=[False])" + +definition + or :: "'a bitsNAe => 'a bitsNAe => 'a bitsNAe" where +"or = (%(ql,dl,fl)(qr,dr,fr). + ([], + %a s. case s of + [] => if a=None then {True#ql,False#qr} else {} + | left#s => if left then True ## dl a s + else False ## dr a s, + %s. case s of [] => False | left#s => if left then fl s else fr s))" + +definition + conc :: "'a bitsNAe => 'a bitsNAe => 'a bitsNAe" where +"conc = (%(ql,dl,fl)(qr,dr,fr). + (True#ql, + %a s. case s of + [] => {} + | left#s => if left then (True ## dl a s) Un + (if fl s & a=None then {False#qr} else {}) + else False ## dr a s, + %s. case s of [] => False | left#s => ~left & fr s))" + +definition + star :: "'a bitsNAe => 'a bitsNAe" where +"star = (%(q,d,f). + ([], + %a s. case s of + [] => if a=None then {True#q} else {} + | left#s => if left then (True ## d a s) Un + (if f s & a=None then {True#q} else {}) + else {}, + %s. case s of [] => True | left#s => left & f s))" + +primrec rexp2nae :: "'a rexp => 'a bitsNAe" where +"rexp2nae Zero = ([], %a s. {}, %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=[] & 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] & q=[False] & 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]: + "!!L R. fin (or L R) (True#p) = fin L p" +by(simp add:or_def) + +lemma fin_or_False[iff]: + "!!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]: +"!!L R. (True#p,q) : step (or L R) a = (? r. q = True#r & (p,r) : step L a)" +apply (simp add:or_def step_def) +apply blast +done + +lemma False_in_step_or[iff]: +"!!L R. (False#p,q) : step (or L R) a = (? r. q = False#r & (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))^* ==> + (!!p. tp = True#p ==> ? q. (p,q) : (eps L)^* & 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))^* ==> + (!!p. tp = False#p ==> ? q. (p,q) : (eps R)^* & 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)^* ==> (True#p, True#q) : (eps(or L R))^*" +apply (induct rule: rtrancl_induct) + apply (blast) +apply (blast intro: rtrancl_into_rtrancl) +done + +lemma lemma2b: + "(p,q) : (eps R)^* ==> (False#p, False#q) : (eps(or L R))^*" +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))^* = (? r. q = True#r & (p,r) : (eps L)^*)" +by (blast dest: lemma1a lemma2a) + +lemma False_epsclosure_or[iff]: + "(False#p,q) : (eps(or L R))^* = (? r. q = False#r & (p,r) : (eps R)^*)" +by (blast dest: lemma1b lemma2b) + +(***** lift True/False over steps *****) + +lemma lift_True_over_steps_or[iff]: + "!!p. (True#p,q):steps (or L R) w = (? r. q = True # r & (p,r):steps L w)" +apply (induct "w") + apply auto +apply force +done + +lemma lift_False_over_steps_or[iff]: + "!!p. (False#p,q):steps (or L R) w = (? r. q = False#r & (p,r):steps R w)" +apply (induct "w") + apply auto +apply (force) +done + +(***** Epsilon closure of start state *****) + +lemma unfold_rtrancl2: + "R^* = Id Un (R O R^*)" +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^* = (q = p | (? r. (p,r) : R & (r,q) : R^*))" +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]: + "!!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]: + "!!L R. (start(or L R),q) ~: 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 = [] & q = start(or L R)) | + (? p. q = True # p & (start L,p) : steps L w | + q = False # p & (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]: + "!!L R. ~ 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]: + "!!L R. fin (conc L R) (True#p) = False" +by (simp add:conc_def) + +lemma fin_conc_False[iff]: + "!!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]: + "!!L R. (True#p,q) : step (conc L R) a = + ((? r. q=True#r & (p,r): step L a) | + (fin L p & a=None & q=False#start R))" +by (simp add:conc_def step_def) (blast) + +lemma False_step_conc[iff]: + "!!L R. (False#p,q) : step (conc L R) a = + (? r. q = False#r & (p,r) : step R a)" +by (simp add:conc_def step_def) (blast) + +(** False in epsclosure **) + +lemma lemma1b': + "(tp,tq) : (eps(conc L R))^* ==> + (!!p. tp = False#p ==> ? q. (p,q) : (eps R)^* & tq = False#q)" +apply (induct rule: rtrancl_induct) + apply (blast) +apply (blast intro: rtrancl_into_rtrancl) +done + +lemma lemma2b': + "(p,q) : (eps R)^* ==> (False#p, False#q) : (eps(conc L R))^*" +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))^*) = + (? r. q = False # r & (p, r) : (eps R)^*)" +apply (rule iffI) + apply (blast dest: lemma1b') +apply (blast dest: lemma2b') +done + +(** False in steps **) + +lemma False_steps_conc[iff]: + "!!p. (False#p,q): steps (conc L R) w = (? r. q=False#r & (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)^* ==> (True#p,True#q) : (eps(conc L R))^*" +apply (induct rule: rtrancl_induct) + apply (blast) +apply (blast intro: rtrancl_into_rtrancl) +done + +lemma True_True_steps_concI: + "!!p. (p,q) : steps L w ==> (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))^* ==> + (!!p. tp = True#p ==> + (? q. tq = True#q & (p,q) : (eps L)^*) | + (? q r. tq = False#q & (p,r):(eps L)^* & fin L r & (start R,q) : (eps R)^*))" +apply (induct rule: rtrancl_induct) + apply (blast) +apply (blast intro: rtrancl_into_rtrancl) +done + +lemma lemma2a': + "(p, q) : (eps L)^* ==> (True#p, True#q) : (eps(conc L R))^*" +apply (induct rule: rtrancl_induct) + apply (blast) +apply (blast intro: rtrancl_into_rtrancl) +done + +lemma lem: + "!!L R. (p,q) : step R None ==> (False#p, False#q) : step (conc L R) None" +by(simp add: conc_def step_def) + +lemma lemma2b'': + "(p,q) : (eps R)^* ==> (False#p, False#q) : (eps(conc L R))^*" +apply (induct rule: rtrancl_induct) + apply (blast) +apply (drule lem) +apply (blast intro: rtrancl_into_rtrancl) +done + +lemma True_False_eps_concI: + "!!L R. fin L p ==> (True#p, False#start R) : eps(conc L R)" +by(simp add: conc_def step_def) + +lemma True_epsclosure_conc[iff]: + "((True#p,q) : (eps(conc L R))^*) = + ((? r. (p,r) : (eps L)^* & q = True#r) | + (? r. (p,r) : (eps L)^* & fin L r & + (? s. (start R, s) : (eps R)^* & 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]: + "!p. (True#p,q) : steps (conc L R) w --> + ((? r. (p,r) : steps L w & q = True#r) | + (? u v. w = u@v & (? r. (p,r) : steps L u & fin L r & + (? s. (start R,s) : steps R v & 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) : steps (conc L R) w = + ((? r. (p,r) : steps L w & q = True#r) | + (? u v. w = u@v & (? r. (p,r) : steps L u & fin L r & + (? s. (start R,s) : steps R v & q = False#s))))" +by (blast dest: True_steps_concD + intro: True_True_steps_concI in_steps_epsclosure) + +(** starting from the start **) + +lemma start_conc: + "!!L R. start(conc L R) = True#start L" +by (simp add: conc_def) + +lemma final_conc: + "!!L R. fin(conc L R) p = (? s. p = False#s & fin R s)" +by (simp add:conc_def split: list.split) + +lemma accepts_conc: + "accepts (conc L R) w = (? u v. w = u@v & accepts L u & 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]: + "!!A. (True#p,q) : eps(star A) = + ( (? r. q = True#r & (p,r) : eps A) | (fin A p & q = True#start A) )" +by (simp add:star_def step_def) (blast) + +lemma True_True_step_starI: + "!!A. (p,q) : step A a ==> (True#p, True#q) : step (star A) a" +by (simp add:star_def step_def) + +lemma True_True_eps_starI: + "(p,r) : (eps A)^* ==> (True#p, True#r) : (eps(star A))^*" +apply (induct rule: rtrancl_induct) + apply (blast) +apply (blast intro: True_True_step_starI rtrancl_into_rtrancl) +done + +lemma True_start_eps_starI: + "!!A. fin A p ==> (True#p,True#start A) : eps(star A)" +by (simp add:star_def step_def) + +lemma lem': + "(tp,s) : (eps(star A))^* ==> (! p. tp = True#p --> + (? r. ((p,r) : (eps A)^* | + (? q. (p,q) : (eps A)^* & fin A q & (start A,r) : (eps A)^*)) & + 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) : (eps(star A))^*) = + (? r. ((p,r) : (eps A)^* | + (? q. (p,q) : (eps A)^* & fin A q & (start A,r) : (eps A)^*)) & + 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]: + "!!A. (True#p,r): step (star A) (Some a) = + (? q. (p,q): step A (Some a) & 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]: + "!rr. (True#start A,rr) : steps (star A) w --> + (? us v. w = concat us @ v & + (!u:set us. accepts A u) & + (? r. (start A,r) : steps A v & 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: + "!!p. (p,q) : steps A w ==> (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: + "(!u : set us. accepts A u) ==> + (True#start A,True#start A) : 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 = + (? us v. w = concat us @ v & + (!u:set us. accepts A u) & + (? r. (start A,r) : steps A v & 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]: + "!!A. (start(star A),r) : step (star A) a = (a=None & 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=[] & 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]: "!!A. fin (star A) (True#p) = fin A p" +by (simp add:star_def) + +lemma fin_star_start[iff]: "!!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 = + (? us. (!u : set(us). accepts A u) & (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: + "!!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 diff --git a/AFP-contribs/Functional-Automata/RegSet_of_nat_DA.thy b/AFP-contribs/Functional-Automata/RegSet_of_nat_DA.thy new file mode 100644 index 0000000..3674d0f --- /dev/null +++ b/AFP-contribs/Functional-Automata/RegSet_of_nat_DA.thy @@ -0,0 +1,233 @@ +(* 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 => nat => nat" + +abbreviation + deltas :: "'a nat_next => 'a list => nat => nat" where + "deltas == foldl2" + +primrec trace :: "'a nat_next => nat => 'a list => 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 => nat => nat => nat => '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 Un + (regset d i k k) @@ (star(regset d k k k)) @@ (regset d k j k)" + +definition + regset_of_DA :: "('a,nat)da => nat => 'a list set" where +"regset_of_DA A k = (UN j:{j. j nat => bool" where +"bounded d k = (!n. n < k --> (!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 [] => True | y#ys => ys=[])" +by (cases xs) simp_all + +lemma in_set_butlast_concatI: + "x:set(butlast xs) ==> xs:set xss ==> 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]: + "!i. k : set(trace d i xs) --> (EX pref mids suf. + xs = pref @ concat mids @ suf & + deltas d pref i = k & (!n:set(butlast(trace d i pref)). n ~= k) & + (!mid:set mids. (deltas d mid k = k) & + (!n:set(butlast(trace d k mid)). n ~= k)) & + (!n:set(butlast(trace d k suf)). n ~= 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]: "!!i. length(trace d i xs) = length xs" +by (induct "xs") simp_all + +lemma deltas_append[simp]: + "!!i. deltas d (xs@ys) i = deltas d ys (deltas d xs i)" +by (induct "xs") simp_all + +lemma trace_append[simp]: + "!!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]: + "(!xs: set xss. deltas d xs i = i) ==> + trace d i (concat xss) = concat (map (trace d i) xss)" +by (induct "xss") simp_all + +lemma trace_is_Nil[simp]: "!!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 [] => False | y#ys => n = d y i & ns = trace d n ys)" +apply (case_tac "xs") +apply simp_all +apply (blast) +done + +lemma set_trace_conv: + "!!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]: + "(!mid:set mids. deltas d mid k = k) ==> deltas d (concat mids) k = k" +by (induct mids) simp_all + +lemma lem: "[| n < Suc k; n ~= k |] ==> n < k" +by arith + +lemma regset_spec: + "!!i j xs. xs : regset d i j k = + ((!n:set(butlast(trace d i xs)). n < k) & 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 + "(!m:set(butlast(trace d k xsb)). m < Suc k) & 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 ==> !i. i < k --> (!n: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: + "!!i. bounded d k ==> i < k ==> 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 diff --git a/AFP-contribs/Functional-Automata/document/root.bib b/AFP-contribs/Functional-Automata/document/root.bib new file mode 100644 index 0000000..3a1992e --- /dev/null +++ b/AFP-contribs/Functional-Automata/document/root.bib @@ -0,0 +1,6 @@ +@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}}} diff --git a/AFP-contribs/Functional-Automata/document/root.tex b/AFP-contribs/Functional-Automata/document/root.tex new file mode 100644 index 0000000..b5421fb --- /dev/null +++ b/AFP-contribs/Functional-Automata/document/root.tex @@ -0,0 +1,54 @@ + + +\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} diff --git a/AFP-contribs/Regular-Sets/Derivatives.thy b/AFP-contribs/Regular-Sets/Derivatives.thy new file mode 100644 index 0000000..6cfde24 --- /dev/null +++ b/AFP-contribs/Regular-Sets/Derivatives.thy @@ -0,0 +1,375 @@ +section "Derivatives of regular expressions" + +(* Author: Christian Urban *) + +theory Derivatives +imports Regular_Exp +begin + +text\This theory is based on work by Brozowski \cite{Brzozowski64} and Antimirov \cite{Antimirov95}.\ + +subsection \Brzozowski's derivatives of regular expressions\ + +primrec + deriv :: "'a \ 'a rexp \ 'a rexp" +where + "deriv c (Zero) = Zero" +| "deriv c (One) = Zero" +| "deriv c (Atom c') = (if c = c' then One else Zero)" +| "deriv c (Plus r1 r2) = Plus (deriv c r1) (deriv c r2)" +| "deriv c (Times r1 r2) = + (if nullable r1 then Plus (Times (deriv c r1) r2) (deriv c r2) else Times (deriv c r1) r2)" +| "deriv c (Star r) = Times (deriv c r) (Star r)" + +primrec + derivs :: "'a list \ 'a rexp \ 'a rexp" +where + "derivs [] r = r" +| "derivs (c # s) r = derivs s (deriv c r)" + + +lemma atoms_deriv_subset: "atoms (deriv x r) \ atoms r" +by (induction r) (auto) + +lemma atoms_derivs_subset: "atoms (derivs w r) \ atoms r" +by (induction w arbitrary: r) (auto dest: atoms_deriv_subset[THEN subsetD]) + +lemma lang_deriv: "lang (deriv c r) = Deriv c (lang r)" +by (induct r) (simp_all add: nullable_iff) + +lemma lang_derivs: "lang (derivs s r) = Derivs s (lang r)" +by (induct s arbitrary: r) (simp_all add: lang_deriv) + +text \A regular expression matcher:\ + +definition matcher :: "'a rexp \ 'a list \ bool" where +"matcher r s = nullable (derivs s r)" + +lemma matcher_correctness: "matcher r s \ s \ lang r" +by (induct s arbitrary: r) + (simp_all add: nullable_iff lang_deriv matcher_def Deriv_def) + + +subsection \Antimirov's partial derivatives\ + +abbreviation + "Timess rs r \ (\r' \ rs. {Times r' r})" + +lemma Timess_eq_image: + "Timess rs r = (\r'. Times r' r) ` rs" + by auto + +primrec + pderiv :: "'a \ 'a rexp \ 'a rexp set" +where + "pderiv c Zero = {}" +| "pderiv c One = {}" +| "pderiv c (Atom c') = (if c = c' then {One} else {})" +| "pderiv c (Plus r1 r2) = (pderiv c r1) \ (pderiv c r2)" +| "pderiv c (Times r1 r2) = + (if nullable r1 then Timess (pderiv c r1) r2 \ pderiv c r2 else Timess (pderiv c r1) r2)" +| "pderiv c (Star r) = Timess (pderiv c r) (Star r)" + +primrec + pderivs :: "'a list \ 'a rexp \ ('a rexp) set" +where + "pderivs [] r = {r}" +| "pderivs (c # s) r = \ (pderivs s ` pderiv c r)" + +abbreviation + pderiv_set :: "'a \ 'a rexp set \ 'a rexp set" +where + "pderiv_set c rs \ \ (pderiv c ` rs)" + +abbreviation + pderivs_set :: "'a list \ 'a rexp set \ 'a rexp set" +where + "pderivs_set s rs \ \ (pderivs s ` rs)" + +lemma pderivs_append: + "pderivs (s1 @ s2) r = \ (pderivs s2 ` pderivs s1 r)" +by (induct s1 arbitrary: r) (simp_all) + +lemma pderivs_snoc: + shows "pderivs (s @ [c]) r = pderiv_set c (pderivs s r)" +by (simp add: pderivs_append) + +lemma pderivs_simps [simp]: + shows "pderivs s Zero = (if s = [] then {Zero} else {})" + and "pderivs s One = (if s = [] then {One} else {})" + and "pderivs s (Plus r1 r2) = (if s = [] then {Plus r1 r2} else (pderivs s r1) \ (pderivs s r2))" +by (induct s) (simp_all) + +lemma pderivs_Atom: + shows "pderivs s (Atom c) \ {Atom c, One}" +by (induct s) (simp_all) + +subsection \Relating left-quotients and partial derivatives\ + +lemma Deriv_pderiv: + shows "Deriv c (lang r) = \ (lang ` pderiv c r)" +by (induct r) (auto simp add: nullable_iff conc_UNION_distrib) + +lemma Derivs_pderivs: + shows "Derivs s (lang r) = \ (lang ` pderivs s r)" +proof (induct s arbitrary: r) + case (Cons c s) + have ih: "\r. Derivs s (lang r) = \ (lang ` pderivs s r)" by fact + have "Derivs (c # s) (lang r) = Derivs s (Deriv c (lang r))" by simp + also have "\ = Derivs s (\ (lang ` pderiv c r))" by (simp add: Deriv_pderiv) + also have "\ = Derivss s (lang ` (pderiv c r))" + by (auto simp add: Derivs_def) + also have "\ = \ (lang ` (pderivs_set s (pderiv c r)))" + using ih by auto + also have "\ = \ (lang ` (pderivs (c # s) r))" by simp + finally show "Derivs (c # s) (lang r) = \ (lang ` pderivs (c # s) r)" . +qed (simp add: Derivs_def) + +subsection \Relating derivatives and partial derivatives\ + +lemma deriv_pderiv: + shows "\ (lang ` (pderiv c r)) = lang (deriv c r)" +unfolding lang_deriv Deriv_pderiv by simp + +lemma derivs_pderivs: + shows "\ (lang ` (pderivs s r)) = lang (derivs s r)" +unfolding lang_derivs Derivs_pderivs by simp + + +subsection \Finiteness property of partial derivatives\ + +definition + pderivs_lang :: "'a lang \ 'a rexp \ 'a rexp set" +where + "pderivs_lang A r \ \x \ A. pderivs x r" + +lemma pderivs_lang_subsetI: + assumes "\s. s \ A \ pderivs s r \ C" + shows "pderivs_lang A r \ C" +using assms unfolding pderivs_lang_def by (rule UN_least) + +lemma pderivs_lang_union: + shows "pderivs_lang (A \ B) r = (pderivs_lang A r \ pderivs_lang B r)" +by (simp add: pderivs_lang_def) + +lemma pderivs_lang_subset: + shows "A \ B \ pderivs_lang A r \ pderivs_lang B r" +by (auto simp add: pderivs_lang_def) + +definition + "UNIV1 \ UNIV - {[]}" + +lemma pderivs_lang_Zero [simp]: + shows "pderivs_lang UNIV1 Zero = {}" +unfolding UNIV1_def pderivs_lang_def by auto + +lemma pderivs_lang_One [simp]: + shows "pderivs_lang UNIV1 One = {}" +unfolding UNIV1_def pderivs_lang_def by (auto split: if_splits) + +lemma pderivs_lang_Atom [simp]: + shows "pderivs_lang UNIV1 (Atom c) = {One}" +unfolding UNIV1_def pderivs_lang_def +apply(auto) +apply(frule rev_subsetD) +apply(rule pderivs_Atom) +apply(simp) +apply(case_tac xa) +apply(auto split: if_splits) +done + +lemma pderivs_lang_Plus [simp]: + shows "pderivs_lang UNIV1 (Plus r1 r2) = pderivs_lang UNIV1 r1 \ pderivs_lang UNIV1 r2" +unfolding UNIV1_def pderivs_lang_def by auto + + +text \Non-empty suffixes of a string (needed for the cases of @{const Times} and @{const Star} below)\ + +definition + "PSuf s \ {v. v \ [] \ (\u. u @ v = s)}" + +lemma PSuf_snoc: + shows "PSuf (s @ [c]) = (PSuf s) @@ {[c]} \ {[c]}" +unfolding PSuf_def conc_def +by (auto simp add: append_eq_append_conv2 append_eq_Cons_conv) + +lemma PSuf_Union: + shows "(\v \ PSuf s @@ {[c]}. f v) = (\v \ PSuf s. f (v @ [c]))" +by (auto simp add: conc_def) + +lemma pderivs_lang_snoc: + shows "pderivs_lang (PSuf s @@ {[c]}) r = (pderiv_set c (pderivs_lang (PSuf s) r))" +unfolding pderivs_lang_def +by (simp add: PSuf_Union pderivs_snoc) + +lemma pderivs_Times: + shows "pderivs s (Times r1 r2) \ Timess (pderivs s r1) r2 \ (pderivs_lang (PSuf s) r2)" +proof (induct s rule: rev_induct) + case (snoc c s) + have ih: "pderivs s (Times r1 r2) \ Timess (pderivs s r1) r2 \ (pderivs_lang (PSuf s) r2)" + by fact + have "pderivs (s @ [c]) (Times r1 r2) = pderiv_set c (pderivs s (Times r1 r2))" + by (simp add: pderivs_snoc) + also have "\ \ pderiv_set c (Timess (pderivs s r1) r2 \ (pderivs_lang (PSuf s) r2))" + using ih by fastforce + also have "\ = pderiv_set c (Timess (pderivs s r1) r2) \ pderiv_set c (pderivs_lang (PSuf s) r2)" + by (simp) + also have "\ = pderiv_set c (Timess (pderivs s r1) r2) \ pderivs_lang (PSuf s @@ {[c]}) r2" + by (simp add: pderivs_lang_snoc) + also + have "\ \ pderiv_set c (Timess (pderivs s r1) r2) \ pderiv c r2 \ pderivs_lang (PSuf s @@ {[c]}) r2" + by auto + also + have "\ \ Timess (pderiv_set c (pderivs s r1)) r2 \ pderiv c r2 \ pderivs_lang (PSuf s @@ {[c]}) r2" + by (auto simp add: if_splits) + also have "\ = Timess (pderivs (s @ [c]) r1) r2 \ pderiv c r2 \ pderivs_lang (PSuf s @@ {[c]}) r2" + by (simp add: pderivs_snoc) + also have "\ \ Timess (pderivs (s @ [c]) r1) r2 \ pderivs_lang (PSuf (s @ [c])) r2" + unfolding pderivs_lang_def by (auto simp add: PSuf_snoc) + finally show ?case . +qed (simp) + +lemma pderivs_lang_Times_aux1: + assumes a: "s \ UNIV1" + shows "pderivs_lang (PSuf s) r \ pderivs_lang UNIV1 r" +using a unfolding UNIV1_def PSuf_def pderivs_lang_def by auto + +lemma pderivs_lang_Times_aux2: + assumes a: "s \ UNIV1" + shows "Timess (pderivs s r1) r2 \ Timess (pderivs_lang UNIV1 r1) r2" +using a unfolding pderivs_lang_def by auto + +lemma pderivs_lang_Times: + shows "pderivs_lang UNIV1 (Times r1 r2) \ Timess (pderivs_lang UNIV1 r1) r2 \ pderivs_lang UNIV1 r2" +apply(rule pderivs_lang_subsetI) +apply(rule subset_trans) +apply(rule pderivs_Times) +using pderivs_lang_Times_aux1 pderivs_lang_Times_aux2 +apply auto +apply blast +done + +lemma pderivs_Star: + assumes a: "s \ []" + shows "pderivs s (Star r) \ Timess (pderivs_lang (PSuf s) r) (Star r)" +using a +proof (induct s rule: rev_induct) + case (snoc c s) + have ih: "s \ [] \ pderivs s (Star r) \ Timess (pderivs_lang (PSuf s) r) (Star r)" by fact + { assume asm: "s \ []" + have "pderivs (s @ [c]) (Star r) = pderiv_set c (pderivs s (Star r))" by (simp add: pderivs_snoc) + also have "\ \ pderiv_set c (Timess (pderivs_lang (PSuf s) r) (Star r))" + using ih[OF asm] by fast + also have "\ \ Timess (pderiv_set c (pderivs_lang (PSuf s) r)) (Star r) \ pderiv c (Star r)" + by (auto split: if_splits) + also have "\ \ Timess (pderivs_lang (PSuf (s @ [c])) r) (Star r) \ (Timess (pderiv c r) (Star r))" + by (simp only: PSuf_snoc pderivs_lang_snoc pderivs_lang_union) + (auto simp add: pderivs_lang_def) + also have "\ = Timess (pderivs_lang (PSuf (s @ [c])) r) (Star r)" + by (auto simp add: PSuf_snoc PSuf_Union pderivs_snoc pderivs_lang_def) + finally have ?case . + } + moreover + { assume asm: "s = []" + then have ?case by (auto simp add: pderivs_lang_def pderivs_snoc PSuf_def) + } + ultimately show ?case by blast +qed (simp) + +lemma pderivs_lang_Star: + shows "pderivs_lang UNIV1 (Star r) \ Timess (pderivs_lang UNIV1 r) (Star r)" +apply(rule pderivs_lang_subsetI) +apply(rule subset_trans) +apply(rule pderivs_Star) +apply(simp add: UNIV1_def) +apply(simp add: UNIV1_def PSuf_def) +apply(auto simp add: pderivs_lang_def) +done + +lemma finite_Timess [simp]: + assumes a: "finite A" + shows "finite (Timess A r)" +using a by auto + +lemma finite_pderivs_lang_UNIV1: + shows "finite (pderivs_lang UNIV1 r)" +apply(induct r) +apply(simp_all add: + finite_subset[OF pderivs_lang_Times] + finite_subset[OF pderivs_lang_Star]) +done + +lemma pderivs_lang_UNIV: + shows "pderivs_lang UNIV r = pderivs [] r \ pderivs_lang UNIV1 r" +unfolding UNIV1_def pderivs_lang_def +by blast + +lemma finite_pderivs_lang_UNIV: + shows "finite (pderivs_lang UNIV r)" +unfolding pderivs_lang_UNIV +by (simp add: finite_pderivs_lang_UNIV1) + +lemma finite_pderivs_lang: + shows "finite (pderivs_lang A r)" +by (metis finite_pderivs_lang_UNIV pderivs_lang_subset rev_finite_subset subset_UNIV) + + +text\The following relationship between the alphabetic width of regular expressions +(called @{text awidth} below) and the number of partial derivatives was proved +by Antimirov~\cite{Antimirov95} and formalized by Max Haslbeck.\ + +fun awidth :: "'a rexp \ nat" where +"awidth Zero = 0" | +"awidth One = 0" | +"awidth (Atom a) = 1" | +"awidth (Plus r1 r2) = awidth r1 + awidth r2" | +"awidth (Times r1 r2) = awidth r1 + awidth r2" | +"awidth (Star r1) = awidth r1" + +lemma card_Timess_pderivs_lang_le: + "card (Timess (pderivs_lang A r) s) \ card (pderivs_lang A r)" + using finite_pderivs_lang unfolding Timess_eq_image by (rule card_image_le) + +lemma card_pderivs_lang_UNIV1_le_awidth: "card (pderivs_lang UNIV1 r) \ awidth r" +proof (induction r) + case (Plus r1 r2) + have "card (pderivs_lang UNIV1 (Plus r1 r2)) = card (pderivs_lang UNIV1 r1 \ pderivs_lang UNIV1 r2)" by simp + also have "\ \ card (pderivs_lang UNIV1 r1) + card (pderivs_lang UNIV1 r2)" + by(simp add: card_Un_le) + also have "\ \ awidth (Plus r1 r2)" using Plus.IH by simp + finally show ?case . +next + case (Times r1 r2) + have "card (pderivs_lang UNIV1 (Times r1 r2)) \ card (Timess (pderivs_lang UNIV1 r1) r2 \ pderivs_lang UNIV1 r2)" + by (simp add: card_mono finite_pderivs_lang pderivs_lang_Times) + also have "\ \ card (Timess (pderivs_lang UNIV1 r1) r2) + card (pderivs_lang UNIV1 r2)" + by (simp add: card_Un_le) + also have "\ \ card (pderivs_lang UNIV1 r1) + card (pderivs_lang UNIV1 r2)" + by (simp add: card_Timess_pderivs_lang_le) + also have "\ \ awidth (Times r1 r2)" using Times.IH by simp + finally show ?case . +next + case (Star r) + have "card (pderivs_lang UNIV1 (Star r)) \ card (Timess (pderivs_lang UNIV1 r) (Star r))" + by (simp add: card_mono finite_pderivs_lang pderivs_lang_Star) + also have "\ \ card (pderivs_lang UNIV1 r)" by (rule card_Timess_pderivs_lang_le) + also have "\ \ awidth (Star r)" by (simp add: Star.IH) + finally show ?case . +qed (auto) + +text\Antimirov's Theorem 3.4:\ +theorem card_pderivs_lang_UNIV_le_awidth: "card (pderivs_lang UNIV r) \ awidth r + 1" +proof - + have "card (insert r (pderivs_lang UNIV1 r)) \ Suc (card (pderivs_lang UNIV1 r))" + by(auto simp: card_insert_if[OF finite_pderivs_lang_UNIV1]) + also have "\ \ Suc (awidth r)" by(simp add: card_pderivs_lang_UNIV1_le_awidth) + finally show ?thesis by(simp add: pderivs_lang_UNIV) +qed + +text\Antimirov's Corollary 3.5:\ +corollary card_pderivs_lang_le_awidth: "card (pderivs_lang A r) \ awidth r + 1" +by(rule order_trans[OF + card_mono[OF finite_pderivs_lang_UNIV pderivs_lang_subset[OF subset_UNIV]] + card_pderivs_lang_UNIV_le_awidth]) + +end diff --git a/AFP-contribs/Regular-Sets/Equivalence_Checking.thy b/AFP-contribs/Regular-Sets/Equivalence_Checking.thy new file mode 100644 index 0000000..1abcc85 --- /dev/null +++ b/AFP-contribs/Regular-Sets/Equivalence_Checking.thy @@ -0,0 +1,230 @@ +section \Deciding Regular Expression Equivalence\ + +theory Equivalence_Checking +imports + NDerivative + "HOL-Library.While_Combinator" +begin + + +subsection \Bisimulation between languages and regular expressions\ + +coinductive bisimilar :: "'a lang \ 'a lang \ bool" where +"([] \ K \ [] \ L) + \ (\x. bisimilar (Deriv x K) (Deriv x L)) + \ bisimilar K L" + +lemma equal_if_bisimilar: +assumes "bisimilar K L" shows "K = L" +proof (rule set_eqI) + fix w + from \bisimilar K L\ show "w \ K \ w \ L" + proof (induct w arbitrary: K L) + case Nil thus ?case by (auto elim: bisimilar.cases) + next + case (Cons a w K L) + from \bisimilar K L\ have "bisimilar (Deriv a K) (Deriv a L)" + by (auto elim: bisimilar.cases) + then have "w \ Deriv a K \ w \ Deriv a L" by (rule Cons(1)) + thus ?case by (auto simp: Deriv_def) + qed +qed + +lemma language_coinduct: +fixes R (infixl "\" 50) +assumes "K \ L" +assumes "\K L. K \ L \ ([] \ K \ [] \ L)" +assumes "\K L x. K \ L \ Deriv x K \ Deriv x L" +shows "K = L" +apply (rule equal_if_bisimilar) +apply (rule bisimilar.coinduct[of R, OF \K \ L\]) +apply (auto simp: assms) +done + +type_synonym 'a rexp_pair = "'a rexp * 'a rexp" +type_synonym 'a rexp_pairs = "'a rexp_pair list" + +definition is_bisimulation :: "'a::order list \ 'a rexp_pair set \ bool" +where +"is_bisimulation as R = + (\(r,s)\ R. (atoms r \ atoms s \ set as) \ (nullable r \ nullable s) \ + (\a\set as. (nderiv a r, nderiv a s) \ R))" + +lemma bisim_lang_eq: +assumes bisim: "is_bisimulation as ps" +assumes "(r, s) \ ps" +shows "lang r = lang s" +proof - + define ps' where "ps' = insert (Zero, Zero) ps" + from bisim have bisim': "is_bisimulation as ps'" + by (auto simp: ps'_def is_bisimulation_def) + let ?R = "\K L. (\(r,s)\ps'. K = lang r \ L = lang s)" + show ?thesis + proof (rule language_coinduct[where R="?R"]) + from \(r, s) \ ps\ + have "(r, s) \ ps'" by (auto simp: ps'_def) + thus "?R (lang r) (lang s)" by auto + next + fix K L assume "?R K L" + then obtain r s where rs: "(r, s) \ ps'" + and KL: "K = lang r" "L = lang s" by auto + with bisim' have "nullable r \ nullable s" + by (auto simp: is_bisimulation_def) + thus "[] \ K \ [] \ L" by (auto simp: nullable_iff KL) + fix a + show "?R (Deriv a K) (Deriv a L)" + proof cases + assume "a \ set as" + with rs bisim' + have "(nderiv a r, nderiv a s) \ ps'" + by (auto simp: is_bisimulation_def) + thus ?thesis by (force simp: KL lang_nderiv) + next + assume "a \ set as" + with bisim' rs + have "a \ atoms r" "a \ atoms s" by (auto simp: is_bisimulation_def) + then have "nderiv a r = Zero" "nderiv a s = Zero" + by (auto intro: deriv_no_occurrence) + then have "Deriv a K = lang Zero" + "Deriv a L = lang Zero" + unfolding KL lang_nderiv[symmetric] by auto + thus ?thesis by (auto simp: ps'_def) + qed + qed +qed + +subsection \Closure computation\ + +definition closure :: + "'a::order list \ 'a rexp_pair \ ('a rexp_pairs * 'a rexp_pair set) option" +where +"closure as = rtrancl_while (%(r,s). nullable r = nullable s) + (%(r,s). map (\a. (nderiv a r, nderiv a s)) as)" + +definition pre_bisim :: "'a::order list \ 'a rexp \ 'a rexp \ + 'a rexp_pairs * 'a rexp_pair set \ bool" +where +"pre_bisim as r s = (\(ws,R). + (r,s) \ R \ set ws \ R \ + (\(r,s)\ R. atoms r \ atoms s \ set as) \ + (\(r,s)\ R - set ws. (nullable r \ nullable s) \ + (\a\set as. (nderiv a r, nderiv a s) \ R)))" + +theorem closure_sound: +assumes result: "closure as (r,s) = Some([],R)" +and atoms: "atoms r \ atoms s \ set as" +shows "lang r = lang s" +proof- + let ?test = "While_Combinator.rtrancl_while_test (%(r,s). nullable r = nullable s)" + let ?step = "While_Combinator.rtrancl_while_step (%(r,s). map (\a. (nderiv a r, nderiv a s)) as)" + { fix st assume inv: "pre_bisim as r s st" and test: "?test st" + have "pre_bisim as r s (?step st)" + proof (cases st) + fix ws R assume "st = (ws, R)" + with test obtain r s t where st: "st = ((r, s) # t, R)" and "nullable r = nullable s" + by (cases ws) auto + with inv show ?thesis using atoms_nderiv[of _ r] atoms_nderiv[of _ s] + unfolding st rtrancl_while_test.simps rtrancl_while_step.simps pre_bisim_def Ball_def + by simp_all blast+ + qed + } + moreover + from atoms + have "pre_bisim as r s ([(r,s)],{(r,s)})" by (simp add: pre_bisim_def) + ultimately have pre_bisim_ps: "pre_bisim as r s ([],R)" + by (rule while_option_rule[OF _ result[unfolded closure_def rtrancl_while_def]]) + then have "is_bisimulation as R" "(r, s) \ R" + by (auto simp: pre_bisim_def is_bisimulation_def) + thus "lang r = lang s" by (rule bisim_lang_eq) +qed + +subsection \Bisimulation-free proof of closure computation\ + +text\The equivalence check can be viewed as the product construction +of two automata. The state space is the reflexive transitive closure of +the pair of next-state functions, i.e. derivatives.\ + +lemma rtrancl_nderiv_nderivs: defines "nderivs == foldl (%r a. nderiv a r)" +shows "{((r,s),(nderiv a r,nderiv a s))| r s a. a : A}^* = + {((r,s),(nderivs r w,nderivs s w))| r s w. w : lists A}" (is "?L = ?R") +proof- + note [simp] = nderivs_def + { fix r s r' s' + have "((r,s),(r',s')) : ?L \ ((r,s),(r',s')) : ?R" + proof(induction rule: converse_rtrancl_induct2) + case refl show ?case by (force intro!: foldl.simps(1)[symmetric]) + next + case step thus ?case by(force intro!: foldl.simps(2)[symmetric]) + qed + } moreover + { fix r s r' s' + { fix w have "\x\set w. x \ A \ ((r, s), nderivs r w, nderivs s w) :?L" + proof(induction w rule: rev_induct) + case Nil show ?case by simp + next + case snoc thus ?case by (auto elim!: rtrancl_into_rtrancl) + qed + } + hence "((r,s),(r',s')) : ?R \ ((r,s),(r',s')) : ?L" by auto + } ultimately show ?thesis by (auto simp: in_lists_conv_set) blast +qed + +lemma nullable_nderivs: + "nullable (foldl (%r a. nderiv a r) r w) = (w : lang r)" +by (induct w arbitrary: r) (simp_all add: nullable_iff lang_nderiv Deriv_def) + +theorem closure_sound_complete: +assumes result: "closure as (r,s) = Some(ws,R)" +and atoms: "set as = atoms r \ atoms s" +shows "ws = [] \ lang r = lang s" +proof - + have leq: "(lang r = lang s) = + (\(r',s') \ {((r0,s0),(nderiv a r0,nderiv a s0))| r0 s0 a. a : set as}^* `` {(r,s)}. + nullable r' = nullable s')" + by(simp add: atoms rtrancl_nderiv_nderivs Ball_def lang_eq_ext imp_ex nullable_nderivs + del:Un_iff) + have "{(x,y). y \ set ((\(p,q). map (\a. (nderiv a p, nderiv a q)) as) x)} = + {((r,s), nderiv a r, nderiv a s) |r s a. a \ set as}" + by auto + with atoms rtrancl_while_Some[OF result[unfolded closure_def]] + show ?thesis by (auto simp add: leq Ball_def split: if_splits) +qed + +subsection \The overall procedure\ + +primrec add_atoms :: "'a rexp \ 'a list \ 'a list" +where + "add_atoms Zero = id" +| "add_atoms One = id" +| "add_atoms (Atom a) = List.insert a" +| "add_atoms (Plus r s) = add_atoms s o add_atoms r" +| "add_atoms (Times r s) = add_atoms s o add_atoms r" +| "add_atoms (Star r) = add_atoms r" + +lemma set_add_atoms: "set (add_atoms r as) = atoms r \ set as" +by (induct r arbitrary: as) auto + + +definition check_eqv :: "nat rexp \ nat rexp \ bool" where +"check_eqv r s = + (let nr = norm r; ns = norm s; as = add_atoms nr (add_atoms ns []) + in case closure as (nr, ns) of + Some([],_) \ True | _ \ False)" + +lemma soundness: +assumes "check_eqv r s" shows "lang r = lang s" +proof - + let ?nr = "norm r" let ?ns = "norm s" + let ?as = "add_atoms ?nr (add_atoms ?ns [])" + obtain R where 1: "closure ?as (?nr,?ns) = Some([],R)" + using assms by (auto simp: check_eqv_def Let_def split:option.splits list.splits) + then have "lang (norm r) = lang (norm s)" + by (rule closure_sound) (auto simp: set_add_atoms dest!: subsetD[OF atoms_norm]) + thus "lang r = lang s" by simp +qed + +text\Test:\ +lemma "check_eqv (Plus One (Times (Atom 0) (Star(Atom 0)))) (Star(Atom 0))" +by eval + +end diff --git a/AFP-contribs/Regular-Sets/Equivalence_Checking2.thy b/AFP-contribs/Regular-Sets/Equivalence_Checking2.thy new file mode 100644 index 0000000..724a3cb --- /dev/null +++ b/AFP-contribs/Regular-Sets/Equivalence_Checking2.thy @@ -0,0 +1,318 @@ +section \Deciding Equivalence of Extended Regular Expressions\ + +theory Equivalence_Checking2 +imports Regular_Exp2 "HOL-Library.While_Combinator" +begin + +subsection \Term ordering\ + +fun le_rexp :: "nat rexp \ nat rexp \ bool" +where + "le_rexp Zero _ = True" +| "le_rexp _ Zero = False" +| "le_rexp One _ = True" +| "le_rexp _ One = False" +| "le_rexp (Atom a) (Atom b) = (a <= b)" +| "le_rexp (Atom _) _ = True" +| "le_rexp _ (Atom _) = False" +| "le_rexp (Star r) (Star s) = le_rexp r s" +| "le_rexp (Star _) _ = True" +| "le_rexp _ (Star _) = False" +| "le_rexp (Not r) (Not s) = le_rexp r s" +| "le_rexp (Not _) _ = True" +| "le_rexp _ (Not _) = False" +| "le_rexp (Plus r r') (Plus s s') = + (if r = s then le_rexp r' s' else le_rexp r s)" +| "le_rexp (Plus _ _) _ = True" +| "le_rexp _ (Plus _ _) = False" +| "le_rexp (Times r r') (Times s s') = + (if r = s then le_rexp r' s' else le_rexp r s)" +| "le_rexp (Times _ _) _ = True" +| "le_rexp _ (Times _ _) = False" +| "le_rexp (Inter r r') (Inter s s') = + (if r = s then le_rexp r' s' else le_rexp r s)" + +subsection \Normalizing operations\ + +text \associativity, commutativity, idempotence, zero\ + +fun nPlus :: "nat rexp \ nat rexp \ nat rexp" +where + "nPlus Zero r = r" +| "nPlus r Zero = r" +| "nPlus (Plus r s) t = nPlus r (nPlus s t)" +| "nPlus r (Plus s t) = + (if r = s then (Plus s t) + else if le_rexp r s then Plus r (Plus s t) + else Plus s (nPlus r t))" +| "nPlus r s = + (if r = s then r + else if le_rexp r s then Plus r s + else Plus s r)" + +lemma lang_nPlus[simp]: "lang S (nPlus r s) = lang S (Plus r s)" +by (induct r s rule: nPlus.induct) auto + +text \associativity, zero, one\ + +fun nTimes :: "nat rexp \ nat rexp \ nat rexp" +where + "nTimes Zero _ = Zero" +| "nTimes _ Zero = Zero" +| "nTimes One r = r" +| "nTimes r One = r" +| "nTimes (Times r s) t = Times r (nTimes s t)" +| "nTimes r s = Times r s" + +lemma lang_nTimes[simp]: "lang S (nTimes r s) = lang S (Times r s)" +by (induct r s rule: nTimes.induct) (auto simp: conc_assoc) + +text \more optimisations:\ + +fun nInter :: "nat rexp \ nat rexp \ nat rexp" +where + "nInter Zero _ = Zero" +| "nInter _ Zero = Zero" +| "nInter r s = Inter r s" + +lemma lang_nInter[simp]: "lang S (nInter r s) = lang S (Inter r s)" +by (induct r s rule: nInter.induct) (auto) + +primrec norm :: "nat rexp \ nat rexp" +where + "norm Zero = Zero" +| "norm One = One" +| "norm (Atom a) = Atom a" +| "norm (Plus r s) = nPlus (norm r) (norm s)" +| "norm (Times r s) = nTimes (norm r) (norm s)" +| "norm (Star r) = Star (norm r)" +| "norm (Not r) = Not (norm r)" +| "norm (Inter r1 r2) = nInter (norm r1) (norm r2)" + +lemma lang_norm[simp]: "lang S (norm r) = lang S r" +by (induct r) auto + + +subsection \Derivative\ + +primrec nderiv :: "nat \ nat rexp \ nat rexp" +where + "nderiv _ Zero = Zero" +| "nderiv _ One = Zero" +| "nderiv a (Atom b) = (if a = b then One else Zero)" +| "nderiv a (Plus r s) = nPlus (nderiv a r) (nderiv a s)" +| "nderiv a (Times r s) = + (let r's = nTimes (nderiv a r) s + in if nullable r then nPlus r's (nderiv a s) else r's)" +| "nderiv a (Star r) = nTimes (nderiv a r) (Star r)" +| "nderiv a (Not r) = Not (nderiv a r)" +| "nderiv a (Inter r1 r2) = nInter (nderiv a r1) (nderiv a r2)" + +lemma lang_nderiv: "a:S \ lang S (nderiv a r) = Deriv a (lang S r)" +by (induct r) (auto simp: Let_def nullable_iff[where S=S]) + +lemma atoms_nPlus[simp]: "atoms (nPlus r s) = atoms r \ atoms s" +by (induct r s rule: nPlus.induct) auto + +lemma atoms_nTimes: "atoms (nTimes r s) \ atoms r \ atoms s" +by (induct r s rule: nTimes.induct) auto + +lemma atoms_nInter: "atoms (nInter r s) \ atoms r \ atoms s" +by (induct r s rule: nInter.induct) auto + +lemma atoms_norm: "atoms (norm r) \ atoms r" +by (induct r) (auto dest!:subsetD[OF atoms_nTimes]subsetD[OF atoms_nInter]) + +lemma atoms_nderiv: "atoms (nderiv a r) \ atoms r" +by (induct r) (auto simp: Let_def dest!:subsetD[OF atoms_nTimes]subsetD[OF atoms_nInter]) + + +subsection \Bisimulation between languages and regular expressions\ + +context +fixes S :: "'a set" +begin + +coinductive bisimilar :: "'a lang \ 'a lang \ bool" where +"K \ lists S \ L \ lists S + \ ([] \ K \ [] \ L) + \ (\x. x:S \ bisimilar (Deriv x K) (Deriv x L)) + \ bisimilar K L" + +lemma equal_if_bisimilar: +assumes "K \ lists S" "L \ lists S" "bisimilar K L" shows "K = L" +proof (rule set_eqI) + fix w + from assms show "w \ K \ w \ L" + proof (induction w arbitrary: K L) + case Nil thus ?case by (auto elim: bisimilar.cases) + next + case (Cons a w K L) + show ?case + proof cases + assume "a : S" + with \bisimilar K L\ have "bisimilar (Deriv a K) (Deriv a L)" + by (auto elim: bisimilar.cases) + then have "w \ Deriv a K \ w \ Deriv a L" + by (metis Cons.IH bisimilar.cases) + thus ?case by (auto simp: Deriv_def) + next + assume "a \ S" + thus ?case using Cons.prems by auto + qed + qed +qed + +lemma language_coinduct: +fixes R (infixl "\" 50) +assumes "\K L. K \ L \ K \ lists S \ L \ lists S" +assumes "K \ L" +assumes "\K L. K \ L \ ([] \ K \ [] \ L)" +assumes "\K L x. K \ L \ x : S \ Deriv x K \ Deriv x L" +shows "K = L" +apply (rule equal_if_bisimilar) +apply (metis assms(1) assms(2)) +apply (metis assms(1) assms(2)) +apply (rule bisimilar.coinduct[of R, OF \K \ L\]) +apply (auto simp: assms) +done + +end + +type_synonym rexp_pair = "nat rexp * nat rexp" +type_synonym rexp_pairs = "rexp_pair list" + +definition is_bisimulation :: "nat list \ rexp_pairs \ bool" +where +"is_bisimulation as ps = + (\(r,s)\ set ps. (atoms r \ atoms s \ set as) \ (nullable r \ nullable s) \ + (\a\set as. (nderiv a r, nderiv a s) \ set ps))" + + +lemma bisim_lang_eq: +assumes bisim: "is_bisimulation as ps" +assumes "(r, s) \ set ps" +shows "lang (set as) r = lang (set as) s" +proof - + let ?R = "\K L. (\(r,s)\set ps. K = lang (set as) r \ L = lang (set as) s)" + show ?thesis + proof (rule language_coinduct[where R="?R" and S = "set as"]) + from \(r, s) \ set ps\ show "?R (lang (set as) r) (lang (set as) s)" + by auto + next + fix K L assume "?R K L" + then obtain r s where rs: "(r, s) \ set ps" + and KL: "K = lang (set as) r" "L = lang (set as) s" by auto + with bisim have "nullable r \ nullable s" + by (auto simp: is_bisimulation_def) + thus "[] \ K \ [] \ L" by (auto simp: nullable_iff[where S="set as"] KL) + txt\next case, but shared context\ + from bisim rs KL lang_subset_lists[of _ "set as"] + show "K \ lists (set as) \ L \ lists (set as)" + unfolding is_bisimulation_def by blast + txt\next case, but shared context\ + fix a assume "a \ set as" + with rs bisim + have "(nderiv a r, nderiv a s) \ set ps" + by (auto simp: is_bisimulation_def) + thus "?R (Deriv a K) (Deriv a L)" using \a \ set as\ + by (force simp: KL lang_nderiv) + qed +qed + +subsection \Closure computation\ + +fun test :: "rexp_pairs * rexp_pairs \ bool" +where "test (ws, ps) = (case ws of [] \ False | (p,q)#_ \ nullable p = nullable q)" + +fun step :: "nat list \ rexp_pairs * rexp_pairs \ rexp_pairs * rexp_pairs" +where "step as (ws,ps) = + (let + (r, s) = hd ws; + ps' = (r, s) # ps; + succs = map (\a. (nderiv a r, nderiv a s)) as; + new = filter (\p. p \ set ps' \ set ws) succs + in (new @ tl ws, ps'))" + +definition closure :: + "nat list \ rexp_pairs * rexp_pairs + \ (rexp_pairs * rexp_pairs) option" where +"closure as = while_option test (step as)" + +definition pre_bisim :: "nat list \ nat rexp \ nat rexp \ + rexp_pairs * rexp_pairs \ bool" +where +"pre_bisim as r s = (\(ws,ps). + ((r, s) \ set ws \ set ps) \ + (\(r,s)\ set ws \ set ps. atoms r \ atoms s \ set as) \ + (\(r,s)\ set ps. (nullable r \ nullable s) \ + (\a\set as. (nderiv a r, nderiv a s) \ set ps \ set ws)))" + +theorem closure_sound: +assumes result: "closure as ([(r,s)],[]) = Some([],ps)" +and atoms: "atoms r \ atoms s \ set as" +shows "lang (set as) r = lang (set as) s" +proof- + { fix st have "pre_bisim as r s st \ test st \ pre_bisim as r s (step as st)" + unfolding pre_bisim_def + by (cases st) (auto simp: split_def split: list.splits prod.splits + dest!: subsetD[OF atoms_nderiv]) } + moreover + from atoms + have "pre_bisim as r s ([(r,s)],[])" by (simp add: pre_bisim_def) + ultimately have pre_bisim_ps: "pre_bisim as r s ([],ps)" + by (rule while_option_rule[OF _ result[unfolded closure_def]]) + then have "is_bisimulation as ps" "(r, s) \ set ps" + by (auto simp: pre_bisim_def is_bisimulation_def) + thus "lang (set as) r = lang (set as) s" by (rule bisim_lang_eq) +qed + + +subsection \The overall procedure\ + +primrec add_atoms :: "nat rexp \ nat list \ nat list" +where + "add_atoms Zero = id" +| "add_atoms One = id" +| "add_atoms (Atom a) = List.insert a" +| "add_atoms (Plus r s) = add_atoms s o add_atoms r" +| "add_atoms (Times r s) = add_atoms s o add_atoms r" +| "add_atoms (Not r) = add_atoms r" +| "add_atoms (Inter r s) = add_atoms s o add_atoms r" +| "add_atoms (Star r) = add_atoms r" + +lemma set_add_atoms: "set (add_atoms r as) = atoms r \ set as" +by (induct r arbitrary: as) auto + +definition check_eqv :: "nat list \ nat rexp \ nat rexp \ bool" +where +"check_eqv as r s \ set(add_atoms r (add_atoms s [])) \ set as \ + (case closure as ([(norm r, norm s)], []) of + Some([],_) \ True | _ \ False)" + +lemma soundness: +assumes "check_eqv as r s" shows "lang (set as) r = lang (set as) s" +proof - + obtain ps where cl: "closure as ([(norm r,norm s)],[]) = Some([],ps)" + and at: "atoms r \ atoms s \ set as" + using assms + by (auto simp: check_eqv_def set_add_atoms split:option.splits list.splits) + hence "atoms(norm r) \ atoms(norm s) \ set as" + using atoms_norm by blast + hence "lang (set as) (norm r) = lang (set as) (norm s)" + by (rule closure_sound[OF cl]) + thus "lang (set as) r = lang (set as) s" by simp +qed + +lemma "check_eqv [0] (Plus One (Times (Atom 0) (Star(Atom 0)))) (Star(Atom 0))" +by eval + +lemma "check_eqv [0,1] (Not(Atom 0)) + (Plus One (Times (Plus (Atom 1) (Times (Atom 0) (Plus (Atom 0) (Atom 1)))) + (Star(Plus (Atom 0) (Atom 1)))))" +by eval + +lemma "check_eqv [0] (Atom 0) (Inter (Star (Atom 0)) (Atom 0))" +by eval + +end diff --git a/AFP-contribs/Regular-Sets/NDerivative.thy b/AFP-contribs/Regular-Sets/NDerivative.thy new file mode 100644 index 0000000..7a9ef1a --- /dev/null +++ b/AFP-contribs/Regular-Sets/NDerivative.thy @@ -0,0 +1,85 @@ +section \Normalizing Derivative\ + +theory NDerivative +imports + Regular_Exp +begin + +subsection \Normalizing operations\ + +text \associativity, commutativity, idempotence, zero\ + +fun nPlus :: "'a::order rexp \ 'a rexp \ 'a rexp" +where + "nPlus Zero r = r" +| "nPlus r Zero = r" +| "nPlus (Plus r s) t = nPlus r (nPlus s t)" +| "nPlus r (Plus s t) = + (if r = s then (Plus s t) + else if le_rexp r s then Plus r (Plus s t) + else Plus s (nPlus r t))" +| "nPlus r s = + (if r = s then r + else if le_rexp r s then Plus r s + else Plus s r)" + +lemma lang_nPlus[simp]: "lang (nPlus r s) = lang (Plus r s)" +by (induction r s rule: nPlus.induct) auto + +text \associativity, zero, one\ + +fun nTimes :: "'a::order rexp \ 'a rexp \ 'a rexp" +where + "nTimes Zero _ = Zero" +| "nTimes _ Zero = Zero" +| "nTimes One r = r" +| "nTimes r One = r" +| "nTimes (Times r s) t = Times r (nTimes s t)" +| "nTimes r s = Times r s" + +lemma lang_nTimes[simp]: "lang (nTimes r s) = lang (Times r s)" +by (induction r s rule: nTimes.induct) (auto simp: conc_assoc) + +primrec norm :: "'a::order rexp \ 'a rexp" +where + "norm Zero = Zero" +| "norm One = One" +| "norm (Atom a) = Atom a" +| "norm (Plus r s) = nPlus (norm r) (norm s)" +| "norm (Times r s) = nTimes (norm r) (norm s)" +| "norm (Star r) = Star (norm r)" + +lemma lang_norm[simp]: "lang (norm r) = lang r" +by (induct r) auto + +primrec nderiv :: "'a::order \ 'a rexp \ 'a rexp" +where + "nderiv _ Zero = Zero" +| "nderiv _ One = Zero" +| "nderiv a (Atom b) = (if a = b then One else Zero)" +| "nderiv a (Plus r s) = nPlus (nderiv a r) (nderiv a s)" +| "nderiv a (Times r s) = + (let r's = nTimes (nderiv a r) s + in if nullable r then nPlus r's (nderiv a s) else r's)" +| "nderiv a (Star r) = nTimes (nderiv a r) (Star r)" + +lemma lang_nderiv: "lang (nderiv a r) = Deriv a (lang r)" +by (induction r) (auto simp: Let_def nullable_iff) + +lemma deriv_no_occurrence: + "x \ atoms r \ nderiv x r = Zero" +by (induction r) auto + +lemma atoms_nPlus[simp]: "atoms (nPlus r s) = atoms r \ atoms s" +by (induction r s rule: nPlus.induct) auto + +lemma atoms_nTimes: "atoms (nTimes r s) \ atoms r \ atoms s" +by (induction r s rule: nTimes.induct) auto + +lemma atoms_norm: "atoms (norm r) \ atoms r" +by (induction r) (auto dest!:subsetD[OF atoms_nTimes]) + +lemma atoms_nderiv: "atoms (nderiv a r) \ atoms r" +by (induction r) (auto simp: Let_def dest!:subsetD[OF atoms_nTimes]) + +end diff --git a/AFP-contribs/Regular-Sets/ROOT b/AFP-contribs/Regular-Sets/ROOT new file mode 100644 index 0000000..423f5d3 --- /dev/null +++ b/AFP-contribs/Regular-Sets/ROOT @@ -0,0 +1,12 @@ +chapter AFP + +session "Regular-Sets" (AFP) = "HOL-Library" + + options [timeout = 600] + theories + Regexp_Method + Regexp_Constructions + pEquivalence_Checking + Equivalence_Checking2 + document_files + "root.bib" + "root.tex" diff --git a/AFP-contribs/Regular-Sets/Regexp_Constructions.thy b/AFP-contribs/Regular-Sets/Regexp_Constructions.thy new file mode 100644 index 0000000..2e2dceb --- /dev/null +++ b/AFP-contribs/Regular-Sets/Regexp_Constructions.thy @@ -0,0 +1,395 @@ +(* + File: Regexp_Constructions.thy + Author: Manuel Eberl + + Some simple constructions on regular expressions to illustrate closure properties of regular + languages: reversal, substitution, prefixes, suffixes, subwords ("fragments") +*) +section \Basic constructions on regular expressions\ +theory Regexp_Constructions +imports + Main + "HOL-Library.Sublist" + Regular_Exp +begin + +subsection \Reverse language\ + +lemma rev_conc [simp]: "rev ` (A @@ B) = rev ` B @@ rev ` A" + unfolding conc_def image_def by force + +lemma rev_compower [simp]: "rev ` (A ^^ n) = (rev ` A) ^^ n" + by (induction n) (simp_all add: conc_pow_comm) + +lemma rev_star [simp]: "rev ` star A = star (rev ` A)" + by (simp add: star_def image_UN) + + +subsection \Substituting characters in a language\ + +definition subst_word :: "('a \ 'b list) \ 'a list \ 'b list" where + "subst_word f xs = concat (map f xs)" + +lemma subst_word_Nil [simp]: "subst_word f [] = []" + by (simp add: subst_word_def) + +lemma subst_word_singleton [simp]: "subst_word f [x] = f x" + by (simp add: subst_word_def) + +lemma subst_word_append [simp]: "subst_word f (xs @ ys) = subst_word f xs @ subst_word f ys" + by (simp add: subst_word_def) + +lemma subst_word_Cons [simp]: "subst_word f (x # xs) = f x @ subst_word f xs" + by (simp add: subst_word_def) + +lemma subst_word_conc [simp]: "subst_word f ` (A @@ B) = subst_word f ` A @@ subst_word f ` B" + unfolding conc_def image_def by force + +lemma subst_word_compower [simp]: "subst_word f ` (A ^^ n) = (subst_word f ` A) ^^ n" + by (induction n) simp_all + +lemma subst_word_star [simp]: "subst_word f ` (star A) = star (subst_word f ` A)" + by (simp add: star_def image_UN) + + +text \Suffix language\ + +definition Suffixes :: "'a list set \ 'a list set" where + "Suffixes A = {w. \q. q @ w \ A}" + +lemma Suffixes_altdef [code]: "Suffixes A = (\w\A. set (suffixes w))" + unfolding Suffixes_def set_suffixes_eq suffix_def by blast + +lemma Nil_in_Suffixes_iff [simp]: "[] \ Suffixes A \ A \ {}" + by (auto simp: Suffixes_def) + +lemma Suffixes_empty [simp]: "Suffixes {} = {}" + by (auto simp: Suffixes_def) + +lemma Suffixes_empty_iff [simp]: "Suffixes A = {} \ A = {}" + by (auto simp: Suffixes_altdef) + +lemma Suffixes_singleton [simp]: "Suffixes {xs} = set (suffixes xs)" + by (auto simp: Suffixes_altdef) + +lemma Suffixes_insert: "Suffixes (insert xs A) = set (suffixes xs) \ Suffixes A" + by (simp add: Suffixes_altdef) + +lemma Suffixes_conc [simp]: "A \ {} \ Suffixes (A @@ B) = Suffixes B \ (Suffixes A @@ B)" + unfolding Suffixes_altdef conc_def by (force simp: suffix_append) + +lemma Suffixes_union [simp]: "Suffixes (A \ B) = Suffixes A \ Suffixes B" + by (auto simp: Suffixes_def) + +lemma Suffixes_UNION [simp]: "Suffixes (UNION A f) = UNION A (\x. Suffixes (f x))" + by (auto simp: Suffixes_def) + +lemma Suffixes_compower: + assumes "A \ {}" + shows "Suffixes (A ^^ n) = insert [] (Suffixes A @@ (\kk A ^^ n))" + by (simp_all add: assms conc_Un_distrib) + also have "(\k A ^^ n = (\k\insert n {.. {}" + shows "Suffixes (star A) = Suffixes A @@ star A" +proof - + have "star A = (\n. A ^^ n)" unfolding star_def .. + also have "Suffixes \ = (\x. Suffixes (A ^^ x))" by simp + also have "\ = (\n. insert [] (Suffixes A @@ (\k = insert [] (Suffixes A @@ (\n. (\kn. (\kn. A ^^ n)" by auto + also have "\ = star A" unfolding star_def .. + also have "insert [] (Suffixes A @@ star A) = Suffixes A @@ star A" + using assms by auto + finally show ?thesis . +qed + +text \Prefix language\ + +definition Prefixes :: "'a list set \ 'a list set" where + "Prefixes A = {w. \q. w @ q \ A}" + +lemma Prefixes_altdef [code]: "Prefixes A = (\w\A. set (prefixes w))" + unfolding Prefixes_def set_prefixes_eq prefix_def by blast + +lemma Nil_in_Prefixes_iff [simp]: "[] \ Prefixes A \ A \ {}" + by (auto simp: Prefixes_def) + +lemma Prefixes_empty [simp]: "Prefixes {} = {}" + by (auto simp: Prefixes_def) + +lemma Prefixes_empty_iff [simp]: "Prefixes A = {} \ A = {}" + by (auto simp: Prefixes_altdef) + +lemma Prefixes_singleton [simp]: "Prefixes {xs} = set (prefixes xs)" + by (auto simp: Prefixes_altdef) + +lemma Prefixes_insert: "Prefixes (insert xs A) = set (prefixes xs) \ Prefixes A" + by (simp add: Prefixes_altdef) + +lemma Prefixes_conc [simp]: "B \ {} \ Prefixes (A @@ B) = Prefixes A \ (A @@ Prefixes B)" + unfolding Prefixes_altdef conc_def by (force simp: prefix_append) + +lemma Prefixes_union [simp]: "Prefixes (A \ B) = Prefixes A \ Prefixes B" + by (auto simp: Prefixes_def) + +lemma Prefixes_UNION [simp]: "Prefixes (UNION A f) = UNION A (\x. Prefixes (f x))" + by (auto simp: Prefixes_def) + + +lemma Prefixes_rev: "Prefixes (rev ` A) = rev ` Suffixes A" + by (auto simp: Prefixes_altdef prefixes_rev Suffixes_altdef) + +lemma Suffixes_rev: "Suffixes (rev ` A) = rev ` Prefixes A" + by (auto simp: Prefixes_altdef suffixes_rev Suffixes_altdef) + + +lemma Prefixes_compower: + assumes "A \ {}" + shows "Prefixes (A ^^ n) = insert [] ((\k = insert [] ((\k {}" + shows "Prefixes (star A) = star A @@ Prefixes A" +proof - + have "star A = rev ` star (rev ` A)" by (simp add: image_image) + also have "Prefixes \ = star A @@ Prefixes A" + unfolding Prefixes_rev + by (subst Suffixes_star) (simp_all add: assms image_image Suffixes_rev) + finally show ?thesis . +qed + + +subsection \Subword language\ + +text \ + The language of all sub-words, i.e. all words that are a contiguous sublist of a word in + the original language. +\ +definition Sublists :: "'a list set \ 'a list set" where + "Sublists A = {w. \q\A. sublist w q}" + +lemma Sublists_altdef [code]: "Sublists A = (\w\A. set (sublists w))" + by (auto simp: Sublists_def) + +lemma Sublists_empty [simp]: "Sublists {} = {}" + by (auto simp: Sublists_def) + +lemma Sublists_singleton [simp]: "Sublists {w} = set (sublists w)" + by (auto simp: Sublists_altdef) + +lemma Sublists_insert: "Sublists (insert w A) = set (sublists w) \ Sublists A" + by (auto simp: Sublists_altdef) + +lemma Sublists_Un [simp]: "Sublists (A \ B) = Sublists A \ Sublists B" + by (auto simp: Sublists_altdef) + +lemma Sublists_UN [simp]: "Sublists (UNION A f) = UNION A (\x. Sublists (f x))" + by (auto simp: Sublists_altdef) + +lemma Sublists_conv_Prefixes: "Sublists A = Prefixes (Suffixes A)" + by (auto simp: Sublists_def Prefixes_def Suffixes_def sublist_def) + +lemma Sublists_conv_Suffixes: "Sublists A = Suffixes (Prefixes A)" + by (auto simp: Sublists_def Prefixes_def Suffixes_def sublist_def) + +lemma Sublists_conc [simp]: + assumes "A \ {}" "B \ {}" + shows "Sublists (A @@ B) = Sublists A \ Sublists B \ Suffixes A @@ Prefixes B" + using assms unfolding Sublists_conv_Suffixes by auto + +lemma star_not_empty [simp]: "star A \ {}" + by auto + +lemma Sublists_star: + "A \ {} \ Sublists (star A) = Sublists A \ Suffixes A @@ star A @@ Prefixes A" + by (simp add: Sublists_conv_Prefixes) + +lemma Prefixes_subset_Sublists: "Prefixes A \ Sublists A" + unfolding Prefixes_def Sublists_def by auto + +lemma Suffixes_subset_Sublists: "Suffixes A \ Sublists A" + unfolding Suffixes_def Sublists_def by auto + + +subsection \Fragment language\ + +text \ + The following is the fragment language of a given language, i.e. the set of all words that + are (not necessarily contiguous) sub-sequences of a word in the original language. +\ +definition Subseqs where "Subseqs A = (\w\A. set (subseqs w))" + +lemma Subseqs_empty [simp]: "Subseqs {} = {}" + by (simp add: Subseqs_def) + +lemma Subseqs_insert [simp]: "Subseqs (insert xs A) = set (subseqs xs) \ Subseqs A" + by (simp add: Subseqs_def) + +lemma Subseqs_singleton [simp]: "Subseqs {xs} = set (subseqs xs)" + by simp + +lemma Subseqs_Un [simp]: "Subseqs (A \ B) = Subseqs A \ Subseqs B" + by (simp add: Subseqs_def) + +lemma Subseqs_UNION [simp]: "Subseqs (UNION A f) = UNION A (\x. Subseqs (f x))" + by (simp add: Subseqs_def) + +lemma Subseqs_conc [simp]: "Subseqs (A @@ B) = Subseqs A @@ Subseqs B" +proof safe + fix xs assume "xs \ Subseqs (A @@ B)" + then obtain ys zs where *: "ys \ A" "zs \ B" "subseq xs (ys @ zs)" + by (auto simp: Subseqs_def conc_def) + from *(3) obtain xs1 xs2 where "xs = xs1 @ xs2" "subseq xs1 ys" "subseq xs2 zs" + by (rule subseq_appendE) + with *(1,2) show "xs \ Subseqs A @@ Subseqs B" by (auto simp: Subseqs_def set_subseqs_eq) +next + fix xs assume "xs \ Subseqs A @@ Subseqs B" + then obtain xs1 xs2 ys zs + where "xs = xs1 @ xs2" "subseq xs1 ys" "subseq xs2 zs" "ys \ A" "zs \ B" + by (auto simp: conc_def Subseqs_def) + thus "xs \ Subseqs (A @@ B)" by (force simp: Subseqs_def conc_def intro: list_emb_append_mono) +qed + +lemma Subseqs_compower [simp]: "Subseqs (A ^^ n) = Subseqs A ^^ n" + by (induction n) simp_all + +lemma Subseqs_star [simp]: "Subseqs (star A) = star (Subseqs A)" + by (simp add: star_def) + +lemma Sublists_subset_Subseqs: "Sublists A \ Subseqs A" + by (auto simp: Sublists_def Subseqs_def dest!: sublist_imp_subseq) + + +subsection \Various regular expression constructions\ + +text \A construction for language reversal of a regular expression:\ + +primrec rexp_rev where + "rexp_rev Zero = Zero" +| "rexp_rev One = One" +| "rexp_rev (Atom x) = Atom x" +| "rexp_rev (Plus r s) = Plus (rexp_rev r) (rexp_rev s)" +| "rexp_rev (Times r s) = Times (rexp_rev s) (rexp_rev r)" +| "rexp_rev (Star r) = Star (rexp_rev r)" + +lemma lang_rexp_rev [simp]: "lang (rexp_rev r) = rev ` lang r" + by (induction r) (simp_all add: image_Un) + + +text \The obvious construction for a singleton-language regular expression:\ + +fun rexp_of_word where + "rexp_of_word [] = One" +| "rexp_of_word [x] = Atom x" +| "rexp_of_word (x#xs) = Times (Atom x) (rexp_of_word xs)" + +lemma lang_rexp_of_word [simp]: "lang (rexp_of_word xs) = {xs}" + by (induction xs rule: rexp_of_word.induct) (simp_all add: conc_def) + +lemma size_rexp_of_word [simp]: "size (rexp_of_word xs) = Suc (2 * (length xs - 1))" + by (induction xs rule: rexp_of_word.induct) auto + + +text \Character substitution in a regular expression:\ + +primrec rexp_subst where + "rexp_subst f Zero = Zero" +| "rexp_subst f One = One" +| "rexp_subst f (Atom x) = rexp_of_word (f x)" +| "rexp_subst f (Plus r s) = Plus (rexp_subst f r) (rexp_subst f s)" +| "rexp_subst f (Times r s) = Times (rexp_subst f r) (rexp_subst f s)" +| "rexp_subst f (Star r) = Star (rexp_subst f r)" + +lemma lang_rexp_subst: "lang (rexp_subst f r) = subst_word f ` lang r" + by (induction r) (simp_all add: image_Un) + + +text \Suffix language of a regular expression:\ + +primrec suffix_rexp :: "'a rexp \ 'a rexp" where + "suffix_rexp Zero = Zero" +| "suffix_rexp One = One" +| "suffix_rexp (Atom a) = Plus (Atom a) One" +| "suffix_rexp (Plus r s) = Plus (suffix_rexp r) (suffix_rexp s)" +| "suffix_rexp (Times r s) = + (if rexp_empty r then Zero else Plus (Times (suffix_rexp r) s) (suffix_rexp s))" +| "suffix_rexp (Star r) = + (if rexp_empty r then One else Times (suffix_rexp r) (Star r))" + +theorem lang_suffix_rexp [simp]: + "lang (suffix_rexp r) = Suffixes (lang r)" + by (induction r) (auto simp: rexp_empty_iff) + + +text \Prefix language of a regular expression:\ + +primrec prefix_rexp :: "'a rexp \ 'a rexp" where + "prefix_rexp Zero = Zero" +| "prefix_rexp One = One" +| "prefix_rexp (Atom a) = Plus (Atom a) One" +| "prefix_rexp (Plus r s) = Plus (prefix_rexp r) (prefix_rexp s)" +| "prefix_rexp (Times r s) = + (if rexp_empty s then Zero else Plus (Times r (prefix_rexp s)) (prefix_rexp r))" +| "prefix_rexp (Star r) = + (if rexp_empty r then One else Times (Star r) (prefix_rexp r))" + +theorem lang_prefix_rexp [simp]: + "lang (prefix_rexp r) = Prefixes (lang r)" + by (induction r) (auto simp: rexp_empty_iff) + + +text \Sub-word language of a regular expression\ + +primrec sublist_rexp :: "'a rexp \ 'a rexp" where + "sublist_rexp Zero = Zero" +| "sublist_rexp One = One" +| "sublist_rexp (Atom a) = Plus (Atom a) One" +| "sublist_rexp (Plus r s) = Plus (sublist_rexp r) (sublist_rexp s)" +| "sublist_rexp (Times r s) = + (if rexp_empty r \ rexp_empty s then Zero else + Plus (sublist_rexp r) (Plus (sublist_rexp s) (Times (suffix_rexp r) (prefix_rexp s))))" +| "sublist_rexp (Star r) = + (if rexp_empty r then One else + Plus (sublist_rexp r) (Times (suffix_rexp r) (Times (Star r) (prefix_rexp r))))" + +theorem lang_sublist_rexp [simp]: + "lang (sublist_rexp r) = Sublists (lang r)" + by (induction r) (auto simp: rexp_empty_iff Sublists_star) + + +text \Fragment language of a regular expression:\ + +primrec subseqs_rexp :: "'a rexp \ 'a rexp" where + "subseqs_rexp Zero = Zero" +| "subseqs_rexp One = One" +| "subseqs_rexp (Atom x) = Plus (Atom x) One" +| "subseqs_rexp (Plus r s) = Plus (subseqs_rexp r) (subseqs_rexp s)" +| "subseqs_rexp (Times r s) = Times (subseqs_rexp r) (subseqs_rexp s)" +| "subseqs_rexp (Star r) = Star (subseqs_rexp r)" + +lemma lang_subseqs_rexp [simp]: "lang (subseqs_rexp r) = Subseqs (lang r)" + by (induction r) auto + + +text \Subword language of a regular expression\ + + +end diff --git a/AFP-contribs/Regular-Sets/Regexp_Method.thy b/AFP-contribs/Regular-Sets/Regexp_Method.thy new file mode 100644 index 0000000..c0ef10c --- /dev/null +++ b/AFP-contribs/Regular-Sets/Regexp_Method.thy @@ -0,0 +1,67 @@ +section \Proving Relation (In)equalities via Regular Expressions\ + +theory Regexp_Method +imports Equivalence_Checking Relation_Interpretation +begin + +primrec rel_of_regexp :: "('a * 'a) set list \ nat rexp \ ('a * 'a) set" where +"rel_of_regexp vs Zero = {}" | +"rel_of_regexp vs One = Id" | +"rel_of_regexp vs (Atom i) = vs ! i" | +"rel_of_regexp vs (Plus r s) = rel_of_regexp vs r \ rel_of_regexp vs s " | +"rel_of_regexp vs (Times r s) = rel_of_regexp vs r O rel_of_regexp vs s" | +"rel_of_regexp vs (Star r) = (rel_of_regexp vs r)^*" + +lemma rel_of_regexp_rel: "rel_of_regexp vs r = rel (\i. vs ! i) r" +by (induct r) auto + +primrec rel_eq where +"rel_eq (r, s) vs = (rel_of_regexp vs r = rel_of_regexp vs s)" + +lemma rel_eqI: "check_eqv r s \ rel_eq (r, s) vs" +unfolding rel_eq.simps rel_of_regexp_rel +by (rule Relation_Interpretation.soundness) + (rule Equivalence_Checking.soundness) + +lemmas regexp_reify = rel_of_regexp.simps rel_eq.simps +lemmas regexp_unfold = trancl_unfold_left subset_Un_eq + +ML \ +local + +fun check_eqv (ct, b) = Thm.mk_binop @{cterm "Pure.eq :: bool \ bool \ prop"} + ct (if b then @{cterm True} else @{cterm False}); + +val (_, check_eqv_oracle) = Context.>>> (Context.map_theory_result + (Thm.add_oracle (@{binding check_eqv}, check_eqv))); + +in + +val regexp_conv = + @{computation_conv bool terms: check_eqv datatypes: "nat rexp"} + (fn _ => fn b => fn ct => check_eqv_oracle (ct, b)) + +end +\ + +method_setup regexp = \ + Scan.succeed (fn ctxt => + SIMPLE_METHOD' ( + (TRY o eresolve_tac ctxt @{thms rev_subsetD}) + THEN' (Subgoal.FOCUS_PARAMS (fn {context = ctxt', ...} => + TRY (Local_Defs.unfold_tac ctxt' @{thms regexp_unfold}) + THEN Reification.tac ctxt' @{thms regexp_reify} NONE 1 + THEN resolve_tac ctxt' @{thms rel_eqI} 1 + THEN CONVERSION (HOLogic.Trueprop_conv (regexp_conv ctxt')) 1 + THEN resolve_tac ctxt' [TrueI] 1) ctxt))) +\ \decide relation equalities via regular expressions\ + +hide_const (open) le_rexp nPlus nTimes norm nullable bisimilar is_bisimulation closure + pre_bisim add_atoms check_eqv rel word_rel rel_eq + +text \Example:\ + +lemma "(r \ s^+)^* = (r \ s)^*" + by regexp + +end diff --git a/AFP-contribs/Regular-Sets/Regular_Exp.thy b/AFP-contribs/Regular-Sets/Regular_Exp.thy new file mode 100644 index 0000000..497ebe0 --- /dev/null +++ b/AFP-contribs/Regular-Sets/Regular_Exp.thy @@ -0,0 +1,176 @@ +(* Author: Tobias Nipkow *) + +section "Regular expressions" + +theory Regular_Exp +imports Regular_Set +begin + +datatype (atoms: 'a) rexp = + is_Zero: Zero | + is_One: One | + Atom 'a | + Plus "('a rexp)" "('a rexp)" | + Times "('a rexp)" "('a rexp)" | + Star "('a rexp)" + +primrec lang :: "'a rexp => 'a lang" where +"lang Zero = {}" | +"lang One = {[]}" | +"lang (Atom a) = {[a]}" | +"lang (Plus r s) = (lang r) Un (lang s)" | +"lang (Times r s) = conc (lang r) (lang s)" | +"lang (Star r) = star(lang r)" + +abbreviation (input) regular_lang where "regular_lang A \ (\r. lang r = A)" + +primrec nullable :: "'a rexp \ bool" where +"nullable Zero = False" | +"nullable One = True" | +"nullable (Atom c) = False" | +"nullable (Plus r1 r2) = (nullable r1 \ nullable r2)" | +"nullable (Times r1 r2) = (nullable r1 \ nullable r2)" | +"nullable (Star r) = True" + +lemma nullable_iff [code_abbrev]: "nullable r \ [] \ lang r" + by (induct r) (auto simp add: conc_def split: if_splits) + +primrec rexp_empty where + "rexp_empty Zero \ True" +| "rexp_empty One \ False" +| "rexp_empty (Atom a) \ False" +| "rexp_empty (Plus r s) \ rexp_empty r \ rexp_empty s" +| "rexp_empty (Times r s) \ rexp_empty r \ rexp_empty s" +| "rexp_empty (Star r) \ False" + +(* TODO Fixme: This code_abbrev rule does not work. Why? *) +lemma rexp_empty_iff [code_abbrev]: "rexp_empty r \ lang r = {}" + by (induction r) auto + + + +text\Composition on rhs usually complicates matters:\ +lemma map_map_rexp: + "map_rexp f (map_rexp g r) = map_rexp (\r. f (g r)) r" + unfolding rexp.map_comp o_def .. + +lemma map_rexp_ident[simp]: "map_rexp (\x. x) = (\r. r)" + unfolding id_def[symmetric] fun_eq_iff rexp.map_id id_apply by (intro allI refl) + +lemma atoms_lang: "w : lang r \ set w \ atoms r" +proof(induction r arbitrary: w) + case Times thus ?case by fastforce +next + case Star thus ?case by (fastforce simp add: star_conv_concat) +qed auto + +lemma lang_eq_ext: "(lang r = lang s) = + (\w \ lists(atoms r \ atoms s). w \ lang r \ w \ lang s)" + by (auto simp: atoms_lang[unfolded subset_iff]) + +lemma lang_eq_ext_Nil_fold_Deriv: + fixes r s + defines "\ \ {(fold Deriv w (lang r), fold Deriv w (lang s))| w. w\lists (atoms r \ atoms s)}" + shows "lang r = lang s \ (\(K, L) \ \. [] \ K \ [] \ L)" + unfolding lang_eq_ext \_def by (subst (1 2) in_fold_Deriv[of "[]", simplified, symmetric]) auto + + +subsection \Term ordering\ + +instantiation rexp :: (order) "{order}" +begin + +fun le_rexp :: "('a::order) rexp \ ('a::order) rexp \ bool" +where + "le_rexp Zero _ = True" +| "le_rexp _ Zero = False" +| "le_rexp One _ = True" +| "le_rexp _ One = False" +| "le_rexp (Atom a) (Atom b) = (a <= b)" +| "le_rexp (Atom _) _ = True" +| "le_rexp _ (Atom _) = False" +| "le_rexp (Star r) (Star s) = le_rexp r s" +| "le_rexp (Star _) _ = True" +| "le_rexp _ (Star _) = False" +| "le_rexp (Plus r r') (Plus s s') = + (if r = s then le_rexp r' s' else le_rexp r s)" +| "le_rexp (Plus _ _) _ = True" +| "le_rexp _ (Plus _ _) = False" +| "le_rexp (Times r r') (Times s s') = + (if r = s then le_rexp r' s' else le_rexp r s)" + +(* The class instance stuff is by Dmitriy Traytel *) + +definition less_eq_rexp where "r \ s \ le_rexp r s" +definition less_rexp where "r < s \ le_rexp r s \ r \ s" + +lemma le_rexp_Zero: "le_rexp r Zero \ r = Zero" +by (induction r) auto + +lemma le_rexp_refl: "le_rexp r r" +by (induction r) auto + +lemma le_rexp_antisym: "\le_rexp r s; le_rexp s r\ \ r = s" +by (induction r s rule: le_rexp.induct) (auto dest: le_rexp_Zero) + +lemma le_rexp_trans: "\le_rexp r s; le_rexp s t\ \ le_rexp r t" +proof (induction r s arbitrary: t rule: le_rexp.induct) + fix v t assume "le_rexp (Atom v) t" thus "le_rexp One t" by (cases t) auto +next + fix s1 s2 t assume "le_rexp (Plus s1 s2) t" thus "le_rexp One t" by (cases t) auto +next + fix s1 s2 t assume "le_rexp (Times s1 s2) t" thus "le_rexp One t" by (cases t) auto +next + fix s t assume "le_rexp (Star s) t" thus "le_rexp One t" by (cases t) auto +next + fix v u t assume "le_rexp (Atom v) (Atom u)" "le_rexp (Atom u) t" + thus "le_rexp (Atom v) t" by (cases t) auto +next + fix v s1 s2 t assume "le_rexp (Plus s1 s2) t" thus "le_rexp (Atom v) t" by (cases t) auto +next + fix v s1 s2 t assume "le_rexp (Times s1 s2) t" thus "le_rexp (Atom v) t" by (cases t) auto +next + fix v s t assume "le_rexp (Star s) t" thus "le_rexp (Atom v) t" by (cases t) auto +next + fix r s t + assume IH: "\t. le_rexp r s \ le_rexp s t \ le_rexp r t" + and "le_rexp (Star r) (Star s)" "le_rexp (Star s) t" + thus "le_rexp (Star r) t" by (cases t) auto +next + fix r s1 s2 t assume "le_rexp (Plus s1 s2) t" thus "le_rexp (Star r) t" by (cases t) auto +next + fix r s1 s2 t assume "le_rexp (Times s1 s2) t" thus "le_rexp (Star r) t" by (cases t) auto +next + fix r1 r2 s1 s2 t + assume "\t. r1 = s1 \ le_rexp r2 s2 \ le_rexp s2 t \ le_rexp r2 t" + "\t. r1 \ s1 \ le_rexp r1 s1 \ le_rexp s1 t \ le_rexp r1 t" + "le_rexp (Plus r1 r2) (Plus s1 s2)" "le_rexp (Plus s1 s2) t" + thus "le_rexp (Plus r1 r2) t" by (cases t) (auto split: if_split_asm intro: le_rexp_antisym) +next + fix r1 r2 s1 s2 t assume "le_rexp (Times s1 s2) t" thus "le_rexp (Plus r1 r2) t" by (cases t) auto +next + fix r1 r2 s1 s2 t + assume "\t. r1 = s1 \ le_rexp r2 s2 \ le_rexp s2 t \ le_rexp r2 t" + "\t. r1 \ s1 \ le_rexp r1 s1 \ le_rexp s1 t \ le_rexp r1 t" + "le_rexp (Times r1 r2) (Times s1 s2)" "le_rexp (Times s1 s2) t" + thus "le_rexp (Times r1 r2) t" by (cases t) (auto split: if_split_asm intro: le_rexp_antisym) +qed auto + +instance proof +qed (auto simp add: less_eq_rexp_def less_rexp_def + intro: le_rexp_refl le_rexp_antisym le_rexp_trans) + +end + +instantiation rexp :: (linorder) "{linorder}" +begin + +lemma le_rexp_total: "le_rexp (r :: 'a :: linorder rexp) s \ le_rexp s r" +by (induction r s rule: le_rexp.induct) auto + +instance proof +qed (unfold less_eq_rexp_def less_rexp_def, rule le_rexp_total) + +end + +end diff --git a/AFP-contribs/Regular-Sets/Regular_Exp2.thy b/AFP-contribs/Regular-Sets/Regular_Exp2.thy new file mode 100644 index 0000000..940138f --- /dev/null +++ b/AFP-contribs/Regular-Sets/Regular_Exp2.thy @@ -0,0 +1,51 @@ +(* Author: Tobias Nipkow *) + +section "Extended Regular Expressions" + +theory Regular_Exp2 +imports Regular_Set +begin + +datatype (atoms: 'a) rexp = + is_Zero: Zero | + is_One: One | + Atom 'a | + Plus "('a rexp)" "('a rexp)" | + Times "('a rexp)" "('a rexp)" | + Star "('a rexp)" | + Not "('a rexp)" | + Inter "('a rexp)" "('a rexp)" + +context +fixes S :: "'a set" +begin + +primrec lang :: "'a rexp => 'a lang" where +"lang Zero = {}" | +"lang One = {[]}" | +"lang (Atom a) = {[a]}" | +"lang (Plus r s) = (lang r) Un (lang s)" | +"lang (Times r s) = conc (lang r) (lang s)" | +"lang (Star r) = star(lang r)" | +"lang (Not r) = lists S - lang r" | +"lang (Inter r s) = (lang r Int lang s)" + +end + +lemma lang_subset_lists: "atoms r \ S \ lang S r \ lists S" +by(induction r)(auto simp: conc_subset_lists star_subset_lists) + +primrec nullable :: "'a rexp \ bool" where +"nullable Zero = False" | +"nullable One = True" | +"nullable (Atom c) = False" | +"nullable (Plus r1 r2) = (nullable r1 \ nullable r2)" | +"nullable (Times r1 r2) = (nullable r1 \ nullable r2)" | +"nullable (Star r) = True" | +"nullable (Not r) = (\ (nullable r))" | +"nullable (Inter r s) = (nullable r \ nullable s)" + +lemma nullable_iff: "nullable r \ [] \ lang S r" +by (induct r) (auto simp add: conc_def split: if_splits) + +end diff --git a/AFP-contribs/Regular-Sets/Regular_Set.thy b/AFP-contribs/Regular-Sets/Regular_Set.thy new file mode 100644 index 0000000..938929e --- /dev/null +++ b/AFP-contribs/Regular-Sets/Regular_Set.thy @@ -0,0 +1,457 @@ +(* Author: Tobias Nipkow, Alex Krauss, Christian Urban *) + +section "Regular sets" + +theory Regular_Set +imports Main +begin + +type_synonym 'a lang = "'a list set" + +definition conc :: "'a lang \ 'a lang \ 'a lang" (infixr "@@" 75) where +"A @@ B = {xs@ys | xs ys. xs:A & ys:B}" + +text \checks the code preprocessor for set comprehensions\ +export_code conc checking SML + +overloading lang_pow == "compow :: nat \ 'a lang \ 'a lang" +begin + primrec lang_pow :: "nat \ 'a lang \ 'a lang" where + "lang_pow 0 A = {[]}" | + "lang_pow (Suc n) A = A @@ (lang_pow n A)" +end + +text \for code generation\ + +definition lang_pow :: "nat \ 'a lang \ 'a lang" where + lang_pow_code_def [code_abbrev]: "lang_pow = compow" + +lemma [code]: + "lang_pow (Suc n) A = A @@ (lang_pow n A)" + "lang_pow 0 A = {[]}" + by (simp_all add: lang_pow_code_def) + +hide_const (open) lang_pow + +definition star :: "'a lang \ 'a lang" where +"star A = (\n. A ^^ n)" + + +subsection\@{term "op @@"}\ + +lemma concI[simp,intro]: "u : A \ v : B \ u@v : A @@ B" +by (auto simp add: conc_def) + +lemma concE[elim]: +assumes "w \ A @@ B" +obtains u v where "u \ A" "v \ B" "w = u@v" +using assms by (auto simp: conc_def) + +lemma conc_mono: "A \ C \ B \ D \ A @@ B \ C @@ D" +by (auto simp: conc_def) + +lemma conc_empty[simp]: shows "{} @@ A = {}" and "A @@ {} = {}" +by auto + +lemma conc_epsilon[simp]: shows "{[]} @@ A = A" and "A @@ {[]} = A" +by (simp_all add:conc_def) + +lemma conc_assoc: "(A @@ B) @@ C = A @@ (B @@ C)" +by (auto elim!: concE) (simp only: append_assoc[symmetric] concI) + +lemma conc_Un_distrib: +shows "A @@ (B \ C) = A @@ B \ A @@ C" +and "(A \ B) @@ C = A @@ C \ B @@ C" +by auto + +lemma conc_UNION_distrib: +shows "A @@ UNION I M = UNION I (%i. A @@ M i)" +and "UNION I M @@ A = UNION I (%i. M i @@ A)" +by auto + +lemma conc_subset_lists: "A \ lists S \ B \ lists S \ A @@ B \ lists S" +by(fastforce simp: conc_def in_lists_conv_set) + +lemma Nil_in_conc[simp]: "[] \ A @@ B \ [] \ A \ [] \ B" +by (metis append_is_Nil_conv concE concI) + +lemma concI_if_Nil1: "[] \ A \ xs : B \ xs \ A @@ B" +by (metis append_Nil concI) + +lemma conc_Diff_if_Nil1: "[] \ A \ A @@ B = (A - {[]}) @@ B \ B" +by (fastforce elim: concI_if_Nil1) + +lemma concI_if_Nil2: "[] \ B \ xs : A \ xs \ A @@ B" +by (metis append_Nil2 concI) + +lemma conc_Diff_if_Nil2: "[] \ B \ A @@ B = A @@ (B - {[]}) \ A" +by (fastforce elim: concI_if_Nil2) + +lemma singleton_in_conc: + "[x] : A @@ B \ [x] : A \ [] : B \ [] : A \ [x] : B" +by (fastforce simp: Cons_eq_append_conv append_eq_Cons_conv + conc_Diff_if_Nil1 conc_Diff_if_Nil2) + + +subsection\@{term "A ^^ n"}\ + +lemma lang_pow_add: "A ^^ (n + m) = A ^^ n @@ A ^^ m" +by (induct n) (auto simp: conc_assoc) + +lemma lang_pow_empty: "{} ^^ n = (if n = 0 then {[]} else {})" +by (induct n) auto + +lemma lang_pow_empty_Suc[simp]: "({}::'a lang) ^^ Suc n = {}" +by (simp add: lang_pow_empty) + +lemma conc_pow_comm: + shows "A @@ (A ^^ n) = (A ^^ n) @@ A" +by (induct n) (simp_all add: conc_assoc[symmetric]) + +lemma length_lang_pow_ub: + "ALL w : A. length w \ k \ w : A^^n \ length w \ k*n" +by(induct n arbitrary: w) (fastforce simp: conc_def)+ + +lemma length_lang_pow_lb: + "ALL w : A. length w \ k \ w : A^^n \ length w \ k*n" +by(induct n arbitrary: w) (fastforce simp: conc_def)+ + +lemma lang_pow_subset_lists: "A \ lists S \ A ^^ n \ lists S" +by(induct n)(auto simp: conc_subset_lists) + + +subsection\@{const star}\ + +lemma star_subset_lists: "A \ lists S \ star A \ lists S" +unfolding star_def by(blast dest: lang_pow_subset_lists) + +lemma star_if_lang_pow[simp]: "w : A ^^ n \ w : star A" +by (auto simp: star_def) + +lemma Nil_in_star[iff]: "[] : star A" +proof (rule star_if_lang_pow) + show "[] : A ^^ 0" by simp +qed + +lemma star_if_lang[simp]: assumes "w : A" shows "w : star A" +proof (rule star_if_lang_pow) + show "w : A ^^ 1" using \w : A\ by simp +qed + +lemma append_in_starI[simp]: +assumes "u : star A" and "v : star A" shows "u@v : star A" +proof - + from \u : star A\ obtain m where "u : A ^^ m" by (auto simp: star_def) + moreover + from \v : star A\ obtain n where "v : A ^^ n" by (auto simp: star_def) + ultimately have "u@v : A ^^ (m+n)" by (simp add: lang_pow_add) + thus ?thesis by simp +qed + +lemma conc_star_star: "star A @@ star A = star A" +by (auto simp: conc_def) + +lemma conc_star_comm: + shows "A @@ star A = star A @@ A" +unfolding star_def conc_pow_comm conc_UNION_distrib +by simp + +lemma star_induct[consumes 1, case_names Nil append, induct set: star]: +assumes "w : star A" + and "P []" + and step: "!!u v. u : A \ v : star A \ P v \ P (u@v)" +shows "P w" +proof - + { fix n have "w : A ^^ n \ P w" + by (induct n arbitrary: w) (auto intro: \P []\ step star_if_lang_pow) } + with \w : star A\ show "P w" by (auto simp: star_def) +qed + +lemma star_empty[simp]: "star {} = {[]}" +by (auto elim: star_induct) + +lemma star_epsilon[simp]: "star {[]} = {[]}" +by (auto elim: star_induct) + +lemma star_idemp[simp]: "star (star A) = star A" +by (auto elim: star_induct) + +lemma star_unfold_left: "star A = A @@ star A \ {[]}" (is "?L = ?R") +proof + show "?L \ ?R" by (rule, erule star_induct) auto +qed auto + +lemma concat_in_star: "set ws \ A \ concat ws : star A" +by (induct ws) simp_all + +lemma in_star_iff_concat: + "w : star A = (EX ws. set ws \ A & w = concat ws)" + (is "_ = (EX ws. ?R w ws)") +proof + assume "w : star A" thus "EX ws. ?R w ws" + proof induct + case Nil have "?R [] []" by simp + thus ?case .. + next + case (append u v) + moreover + then obtain ws where "set ws \ A \ v = concat ws" by blast + ultimately have "?R (u@v) (u#ws)" by auto + thus ?case .. + qed +next + assume "EX us. ?R w us" thus "w : star A" + by (auto simp: concat_in_star) +qed + +lemma star_conv_concat: "star A = {concat ws|ws. set ws \ A}" +by (fastforce simp: in_star_iff_concat) + +lemma star_insert_eps[simp]: "star (insert [] A) = star(A)" +proof- + { fix us + have "set us \ insert [] A \ EX vs. concat us = concat vs \ set vs \ A" + (is "?P \ EX vs. ?Q vs") + proof + let ?vs = "filter (%u. u \ []) us" + show "?P \ ?Q ?vs" by (induct us) auto + qed + } thus ?thesis by (auto simp: star_conv_concat) +qed + +lemma star_unfold_left_Nil: "star A = (A - {[]}) @@ (star A) \ {[]}" +by (metis insert_Diff_single star_insert_eps star_unfold_left) + +lemma star_Diff_Nil_fold: "(A - {[]}) @@ star A = star A - {[]}" +proof - + have "[] \ (A - {[]}) @@ star A" by simp + thus ?thesis using star_unfold_left_Nil by blast +qed + +lemma star_decom: + assumes a: "x \ star A" "x \ []" + shows "\a b. x = a @ b \ a \ [] \ a \ A \ b \ star A" +using a by (induct rule: star_induct) (blast)+ + + +subsection \Left-Quotients of languages\ + +definition Deriv :: "'a \ 'a lang \ 'a lang" + where "Deriv x A = { xs. x#xs \ A }" + +definition Derivs :: "'a list \ 'a lang \ 'a lang" +where "Derivs xs A = { ys. xs @ ys \ A }" + +abbreviation + Derivss :: "'a list \ 'a lang set \ 'a lang" +where + "Derivss s As \ \ (Derivs s ` As)" + + +lemma Deriv_empty[simp]: "Deriv a {} = {}" + and Deriv_epsilon[simp]: "Deriv a {[]} = {}" + and Deriv_char[simp]: "Deriv a {[b]} = (if a = b then {[]} else {})" + and Deriv_union[simp]: "Deriv a (A \ B) = Deriv a A \ Deriv a B" + and Deriv_inter[simp]: "Deriv a (A \ B) = Deriv a A \ Deriv a B" + and Deriv_compl[simp]: "Deriv a (-A) = - Deriv a A" + and Deriv_Union[simp]: "Deriv a (Union M) = Union(Deriv a ` M)" + and Deriv_UN[simp]: "Deriv a (UN x:I. S x) = (UN x:I. Deriv a (S x))" +by (auto simp: Deriv_def) + +lemma Der_conc [simp]: + shows "Deriv c (A @@ B) = (Deriv c A) @@ B \ (if [] \ A then Deriv c B else {})" +unfolding Deriv_def conc_def +by (auto simp add: Cons_eq_append_conv) + +lemma Deriv_star [simp]: + shows "Deriv c (star A) = (Deriv c A) @@ star A" +proof - + have "Deriv c (star A) = Deriv c ({[]} \ A @@ star A)" + by (metis star_unfold_left sup.commute) + also have "... = Deriv c (A @@ star A)" + unfolding Deriv_union by (simp) + also have "... = (Deriv c A) @@ (star A) \ (if [] \ A then Deriv c (star A) else {})" + by simp + also have "... = (Deriv c A) @@ star A" + unfolding conc_def Deriv_def + using star_decom by (force simp add: Cons_eq_append_conv) + finally show "Deriv c (star A) = (Deriv c A) @@ star A" . +qed + +lemma Deriv_diff[simp]: + shows "Deriv c (A - B) = Deriv c A - Deriv c B" +by(auto simp add: Deriv_def) + +lemma Deriv_lists[simp]: "c : S \ Deriv c (lists S) = lists S" +by(auto simp add: Deriv_def) + +lemma Derivs_simps [simp]: + shows "Derivs [] A = A" + and "Derivs (c # s) A = Derivs s (Deriv c A)" + and "Derivs (s1 @ s2) A = Derivs s2 (Derivs s1 A)" +unfolding Derivs_def Deriv_def by auto + +lemma in_fold_Deriv: "v \ fold Deriv w L \ w @ v \ L" + by (induct w arbitrary: L) (simp_all add: Deriv_def) + +lemma Derivs_alt_def [code]: "Derivs w L = fold Deriv w L" + by (induct w arbitrary: L) simp_all + +lemma Deriv_code [code]: + "Deriv x A = tl ` Set.filter (\xs. case xs of x' # _ \ x = x' | _ \ False) A" + by (auto simp: Deriv_def Set.filter_def image_iff tl_def split: list.splits) + +subsection \Shuffle product\ + +definition Shuffle (infixr "\" 80) where + "Shuffle A B = \{shuffle xs ys | xs ys. xs \ A \ ys \ B}" + +lemma Deriv_Shuffle[simp]: + "Deriv a (A \ B) = Deriv a A \ B \ A \ Deriv a B" + unfolding Shuffle_def Deriv_def by (fastforce simp: Cons_in_shuffle_iff neq_Nil_conv) + +lemma shuffle_subset_lists: + assumes "A \ lists S" "B \ lists S" + shows "A \ B \ lists S" +unfolding Shuffle_def proof safe + fix x and zs xs ys :: "'a list" + assume zs: "zs \ shuffle xs ys" "x \ set zs" and "xs \ A" "ys \ B" + with assms have "xs \ lists S" "ys \ lists S" by auto + with zs show "x \ S" by (induct xs ys arbitrary: zs rule: shuffle.induct) auto +qed + +lemma Nil_in_Shuffle[simp]: "[] \ A \ B \ [] \ A \ [] \ B" + unfolding Shuffle_def by force + +lemma shuffle_Un_distrib: +shows "A \ (B \ C) = A \ B \ A \ C" +and "A \ (B \ C) = A \ B \ A \ C" +unfolding Shuffle_def by fast+ + +lemma shuffle_UNION_distrib: +shows "A \ UNION I M = UNION I (%i. A \ M i)" +and "UNION I M \ A = UNION I (%i. M i \ A)" +unfolding Shuffle_def by fast+ + +lemma Shuffle_empty[simp]: + "A \ {} = {}" + "{} \ B = {}" + unfolding Shuffle_def by auto + +lemma Shuffle_eps[simp]: + "A \ {[]} = A" + "{[]} \ B = B" + unfolding Shuffle_def by auto + + +subsection \Arden's Lemma\ + +lemma arden_helper: + assumes eq: "X = A @@ X \ B" + shows "X = (A ^^ Suc n) @@ X \ (\m\n. (A ^^ m) @@ B)" +proof (induct n) + case 0 + show "X = (A ^^ Suc 0) @@ X \ (\m\0. (A ^^ m) @@ B)" + using eq by simp +next + case (Suc n) + have ih: "X = (A ^^ Suc n) @@ X \ (\m\n. (A ^^ m) @@ B)" by fact + also have "\ = (A ^^ Suc n) @@ (A @@ X \ B) \ (\m\n. (A ^^ m) @@ B)" using eq by simp + also have "\ = (A ^^ Suc (Suc n)) @@ X \ ((A ^^ Suc n) @@ B) \ (\m\n. (A ^^ m) @@ B)" + by (simp add: conc_Un_distrib conc_assoc[symmetric] conc_pow_comm) + also have "\ = (A ^^ Suc (Suc n)) @@ X \ (\m\Suc n. (A ^^ m) @@ B)" + by (auto simp add: atMost_Suc) + finally show "X = (A ^^ Suc (Suc n)) @@ X \ (\m\Suc n. (A ^^ m) @@ B)" . +qed + +lemma Arden: + assumes "[] \ A" + shows "X = A @@ X \ B \ X = star A @@ B" +proof + assume eq: "X = A @@ X \ B" + { fix w assume "w : X" + let ?n = "size w" + from \[] \ A\ have "ALL u : A. length u \ 1" + by (metis Suc_eq_plus1 add_leD2 le_0_eq length_0_conv not_less_eq_eq) + hence "ALL u : A^^(?n+1). length u \ ?n+1" + by (metis length_lang_pow_lb nat_mult_1) + hence "ALL u : A^^(?n+1)@@X. length u \ ?n+1" + by(auto simp only: conc_def length_append) + hence "w \ A^^(?n+1)@@X" by auto + hence "w : star A @@ B" using \w : X\ using arden_helper[OF eq, where n="?n"] + by (auto simp add: star_def conc_UNION_distrib) + } moreover + { fix w assume "w : star A @@ B" + hence "EX n. w : A^^n @@ B" by(auto simp: conc_def star_def) + hence "w : X" using arden_helper[OF eq] by blast + } ultimately show "X = star A @@ B" by blast +next + assume eq: "X = star A @@ B" + have "star A = A @@ star A \ {[]}" + by (rule star_unfold_left) + then have "star A @@ B = (A @@ star A \ {[]}) @@ B" + by metis + also have "\ = (A @@ star A) @@ B \ B" + unfolding conc_Un_distrib by simp + also have "\ = A @@ (star A @@ B) \ B" + by (simp only: conc_assoc) + finally show "X = A @@ X \ B" + using eq by blast +qed + + +lemma reversed_arden_helper: + assumes eq: "X = X @@ A \ B" + shows "X = X @@ (A ^^ Suc n) \ (\m\n. B @@ (A ^^ m))" +proof (induct n) + case 0 + show "X = X @@ (A ^^ Suc 0) \ (\m\0. B @@ (A ^^ m))" + using eq by simp +next + case (Suc n) + have ih: "X = X @@ (A ^^ Suc n) \ (\m\n. B @@ (A ^^ m))" by fact + also have "\ = (X @@ A \ B) @@ (A ^^ Suc n) \ (\m\n. B @@ (A ^^ m))" using eq by simp + also have "\ = X @@ (A ^^ Suc (Suc n)) \ (B @@ (A ^^ Suc n)) \ (\m\n. B @@ (A ^^ m))" + by (simp add: conc_Un_distrib conc_assoc) + also have "\ = X @@ (A ^^ Suc (Suc n)) \ (\m\Suc n. B @@ (A ^^ m))" + by (auto simp add: atMost_Suc) + finally show "X = X @@ (A ^^ Suc (Suc n)) \ (\m\Suc n. B @@ (A ^^ m))" . +qed + +theorem reversed_Arden: + assumes nemp: "[] \ A" + shows "X = X @@ A \ B \ X = B @@ star A" +proof + assume eq: "X = X @@ A \ B" + { fix w assume "w : X" + let ?n = "size w" + from \[] \ A\ have "ALL u : A. length u \ 1" + by (metis Suc_eq_plus1 add_leD2 le_0_eq length_0_conv not_less_eq_eq) + hence "ALL u : A^^(?n+1). length u \ ?n+1" + by (metis length_lang_pow_lb nat_mult_1) + hence "ALL u : X @@ A^^(?n+1). length u \ ?n+1" + by(auto simp only: conc_def length_append) + hence "w \ X @@ A^^(?n+1)" by auto + hence "w : B @@ star A" using \w : X\ using reversed_arden_helper[OF eq, where n="?n"] + by (auto simp add: star_def conc_UNION_distrib) + } moreover + { fix w assume "w : B @@ star A" + hence "EX n. w : B @@ A^^n" by (auto simp: conc_def star_def) + hence "w : X" using reversed_arden_helper[OF eq] by blast + } ultimately show "X = B @@ star A" by blast +next + assume eq: "X = B @@ star A" + have "star A = {[]} \ star A @@ A" + unfolding conc_star_comm[symmetric] + by(metis Un_commute star_unfold_left) + then have "B @@ star A = B @@ ({[]} \ star A @@ A)" + by metis + also have "\ = B \ B @@ (star A @@ A)" + unfolding conc_Un_distrib by simp + also have "\ = B \ (B @@ star A) @@ A" + by (simp only: conc_assoc) + finally show "X = X @@ A \ B" + using eq by blast +qed + +end diff --git a/AFP-contribs/Regular-Sets/Relation_Interpretation.thy b/AFP-contribs/Regular-Sets/Relation_Interpretation.thy new file mode 100644 index 0000000..41e71ce --- /dev/null +++ b/AFP-contribs/Regular-Sets/Relation_Interpretation.thy @@ -0,0 +1,53 @@ +section \Regular Expressions as Homogeneous Binary Relations\ + +theory Relation_Interpretation +imports Regular_Exp +begin + +primrec rel :: "('a \ ('b * 'b) set) \ 'a rexp \ ('b * 'b) set" +where + "rel v Zero = {}" | + "rel v One = Id" | + "rel v (Atom a) = v a" | + "rel v (Plus r s) = rel v r \ rel v s" | + "rel v (Times r s) = rel v r O rel v s" | + "rel v (Star r) = (rel v r)^*" + +primrec word_rel :: "('a \ ('b * 'b) set) \ 'a list \ ('b * 'b) set" +where + "word_rel v [] = Id" +| "word_rel v (a#as) = v a O word_rel v as" + +lemma word_rel_append: + "word_rel v w O word_rel v w' = word_rel v (w @ w')" +by (rule sym) (induct w, auto) + +lemma rel_word_rel: "rel v r = (\w\lang r. word_rel v w)" +proof (induct r) + case Times thus ?case + by (auto simp: rel_def word_rel_append conc_def relcomp_UNION_distrib relcomp_UNION_distrib2) +next + case (Star r) + { fix n + have "(rel v r) ^^ n = (\w \ lang r ^^ n. word_rel v w)" + proof (induct n) + case 0 show ?case by simp + next + case (Suc n) thus ?case + unfolding relpow.simps relpow_commute[symmetric] + by (auto simp add: Star conc_def word_rel_append + relcomp_UNION_distrib relcomp_UNION_distrib2) + qed } + + thus ?case unfolding rel.simps + by (force simp: rtrancl_power star_def) +qed auto + + +text \Soundness:\ + +lemma soundness: + "lang r = lang s \ rel v r = rel v s" +unfolding rel_word_rel by auto + +end diff --git a/AFP-contribs/Regular-Sets/document/root.bib b/AFP-contribs/Regular-Sets/document/root.bib new file mode 100644 index 0000000..8b5cb20 --- /dev/null +++ b/AFP-contribs/Regular-Sets/document/root.bib @@ -0,0 +1,36 @@ +@article{KraussN-JAR,author={Alexander Krauss and Tobias Nipkow}, +title={Proof Pearl: Regular Expression Equivalence and Relation Algebra}, +journal={J. Automated Reasoning},note={Online 2011, to appear in print}} + +@inproceedings{Rutten98, + author = {Jan J. M. M. Rutten}, + title = {Automata and Coinduction (An Exercise in Coalgebra)}, + editor = {Davide Sangiorgi and Robert de Simone}, + booktitle = {Concurrency Theory (CONCUR'98)}, + pages = {194--218}, + publisher = {Springer}, + series = {Lecture Notes in Computer Science}, + volume = {1466}, + year = {1998}, +} + +@article{Brzozowski64, + author = {J.~A.~Brzozowski}, + title = {{D}erivatives of {R}egular {E}xpressions}, + journal = {Journal of the ACM}, + volume = {11}, + issue = {4}, + year = {1964}, + pages = {481--494}, + publisher = {ACM} +} + +@ARTICLE{Antimirov95, + author = {V.~Antimirov}, + title = {{P}artial {D}erivatives of {R}egular {E}xpressions and + {F}inite {A}utomata {C}onstructions}, + journal = {Theoretical Computer Science}, + year = {1995}, + volume = {155}, + pages = {291--319} +} \ No newline at end of file diff --git a/AFP-contribs/Regular-Sets/document/root.tex b/AFP-contribs/Regular-Sets/document/root.tex new file mode 100644 index 0000000..cc5e5bd --- /dev/null +++ b/AFP-contribs/Regular-Sets/document/root.tex @@ -0,0 +1,47 @@ +\documentclass[11pt,a4paper]{article} +\usepackage{isabelle,isabellesym} +\usepackage{eufrak} + +% this should be the last package used +\usepackage{pdfsetup} + +% urls in roman style, theory text in math-similar italics +\urlstyle{rm} +\isabellestyle{it} + + +\begin{document} + +\title{Regular Sets, Expressions, Derivatives and Relation Algebra} +\author{Alexander Krauss, Tobias Nipkow,\\ + Chunhan Wu, Xingyuan Zhang and Christian Urban} +\maketitle + +\begin{abstract} +This is a library of constructions on regular expressions and languages. It +provides the operations of concatenation, Kleene star and left-quotients of +languages. A theory of derivatives and partial derivatives is +provided. Arden's lemma and finiteness of partial derivatives is +established. A simple regular expression matcher based on Brozowski's +derivatives is proved to be correct. An executable equivalence checker for +regular expressions is verified; it does not need automata but works directly +on regular expressions. By mapping regular expressions to binary relations, an +automatic and complete proof method for (in)equalities of binary relations +over union, concatenation and (reflexive) transitive closure is obtained. + +For an exposition of the equivalence checker for regular and relation +algebraic expressions see the paper by Krauss and Nipkow~\cite{KraussN-JAR}. + +Extended regular expressions with complement and intersection +are also defined and an equivalence checker is provided. +\end{abstract} + +\tableofcontents + +% include generated text of all theories +\input{session} + +\bibliographystyle{abbrv} +\bibliography{root} + +\end{document} diff --git a/AFP-contribs/Regular-Sets/pEquivalence_Checking.thy b/AFP-contribs/Regular-Sets/pEquivalence_Checking.thy new file mode 100644 index 0000000..05bf430 --- /dev/null +++ b/AFP-contribs/Regular-Sets/pEquivalence_Checking.thy @@ -0,0 +1,306 @@ +section \Deciding Regular Expression Equivalence (2)\ + +theory pEquivalence_Checking +imports Equivalence_Checking Derivatives +begin + +text\\noindent Similar to theory @{theory Equivalence_Checking}, but +with partial derivatives instead of derivatives.\ + +text\Lifting many notions to sets:\ + +definition "Lang R == UN r:R. lang r" +definition "Nullable R == EX r:R. nullable r" +definition "Pderiv a R == UN r:R. pderiv a r" +definition "Atoms R == UN r:R. atoms r" + +(* FIXME: rename pderiv_set in Derivatives to Pderiv and drop the one above *) + +lemma Atoms_pderiv: "Atoms(pderiv a r) \ atoms r" +apply (induct r) +apply (auto simp: Atoms_def UN_subset_iff) +apply (fastforce)+ +done + +lemma Atoms_Pderiv: "Atoms(Pderiv a R) \ Atoms R" +using Atoms_pderiv by (fastforce simp: Atoms_def Pderiv_def) + +lemma pderiv_no_occurrence: + "x \ atoms r \ pderiv x r = {}" +by (induct r) auto + +lemma Pderiv_no_occurrence: + "x \ Atoms R \ Pderiv x R = {}" +by(auto simp:pderiv_no_occurrence Atoms_def Pderiv_def) + +lemma Deriv_Lang: "Deriv c (Lang R) = Lang (Pderiv c R)" +by(auto simp: Deriv_pderiv Pderiv_def Lang_def) + +lemma Nullable_pderiv[simp]: "Nullable(pderivs w r) = (w : lang r)" +apply(induction w arbitrary: r) +apply (simp add: Nullable_def nullable_iff singleton_iff) +using eqset_imp_iff[OF Deriv_pderiv[where 'a = 'a]] +apply (simp add: Nullable_def Deriv_def) +done + + +type_synonym 'a Rexp_pair = "'a rexp set * 'a rexp set" +type_synonym 'a Rexp_pairs = "'a Rexp_pair list" + +definition is_Bisimulation :: "'a list \ 'a Rexp_pairs \ bool" +where +"is_Bisimulation as ps = + (\(R,S)\ set ps. Atoms R \ Atoms S \ set as \ + (Nullable R \ Nullable S) \ + (\a\set as. (Pderiv a R, Pderiv a S) \ set ps))" + +lemma Bisim_Lang_eq: +assumes Bisim: "is_Bisimulation as ps" +assumes "(R, S) \ set ps" +shows "Lang R = Lang S" +proof - + def ps' \ "({}, {}) # ps" + from Bisim have Bisim': "is_Bisimulation as ps'" + by (fastforce simp: ps'_def is_Bisimulation_def UN_subset_iff Pderiv_def Atoms_def) + let ?R = "\K L. (\(R,S)\set ps'. K = Lang R \ L = Lang S)" + show ?thesis + proof (rule language_coinduct[where R="?R"]) + from \(R,S) \ set ps\ + have "(R,S) \ set ps'" by (auto simp: ps'_def) + thus "?R (Lang R) (Lang S)" by auto + next + fix K L assume "?R K L" + then obtain R S where rs: "(R, S) \ set ps'" + and KL: "K = Lang R" "L = Lang S" by auto + with Bisim' have "Nullable R \ Nullable S" + by (auto simp: is_Bisimulation_def) + thus "[] \ K \ [] \ L" + by (auto simp: nullable_iff KL Nullable_def Lang_def) + fix a + show "?R (Deriv a K) (Deriv a L)" + proof cases + assume "a \ set as" + with rs Bisim' + have "(Pderiv a R, Pderiv a S) \ set ps'" + by (auto simp: is_Bisimulation_def) + thus ?thesis by (fastforce simp: KL Deriv_Lang) + next + assume "a \ set as" + with Bisim' rs + have "a \ Atoms R \ Atoms S" + by (fastforce simp: is_Bisimulation_def UN_subset_iff) + then have "Pderiv a R = {}" "Pderiv a S = {}" + by (metis Pderiv_no_occurrence Un_iff)+ + then have "Deriv a K = Lang {}" "Deriv a L = Lang {}" + unfolding KL Deriv_Lang by auto + thus ?thesis by (auto simp: ps'_def) + qed + qed +qed + + +subsection \Closure computation\ + +fun test :: "'a Rexp_pairs * 'a Rexp_pairs \ bool" where +"test (ws, ps) = (case ws of [] \ False | (R,S)#_ \ Nullable R = Nullable S)" + +fun step :: "'a list \ + 'a Rexp_pairs * 'a Rexp_pairs \ 'a Rexp_pairs * 'a Rexp_pairs" +where "step as (ws,ps) = + (let + (R,S) = hd ws; + ps' = (R,S) # ps; + succs = map (\a. (Pderiv a R, Pderiv a S)) as; + new = filter (\p. p \ set ps \ set ws) succs + in (remdups new @ tl ws, ps'))" + +definition closure :: + "'a list \ 'a Rexp_pairs * 'a Rexp_pairs + \ ('a Rexp_pairs * 'a Rexp_pairs) option" where +"closure as = while_option test (step as)" + +definition pre_Bisim :: "'a list \ 'a rexp set \ 'a rexp set \ + 'a Rexp_pairs * 'a Rexp_pairs \ bool" +where +"pre_Bisim as R S = (\(ws,ps). + ((R,S) \ set ws \ set ps) \ + (\(R,S)\ set ws \ set ps. Atoms R \ Atoms S \ set as) \ + (\(R,S)\ set ps. (Nullable R \ Nullable S) \ + (\a\set as. (Pderiv a R, Pderiv a S) \ set ps \ set ws)))" + +lemma step_set_eq: "\ test (ws,ps); step as (ws,ps) = (ws',ps') \ + \ set ws' \ set ps' = + set ws \ set ps + \ (\a\set as. {(Pderiv a (fst(hd ws)), Pderiv a (snd(hd ws)))})" +by(auto split: list.splits) + +theorem closure_sound: +assumes result: "closure as ([(R,S)],[]) = Some([],ps)" +and atoms: "Atoms R \ Atoms S \ set as" +shows "Lang R = Lang S" +proof- + { fix st + have "pre_Bisim as R S st \ test st \ pre_Bisim as R S (step as st)" + unfolding pre_Bisim_def + proof(split prod.splits, elim case_prodE conjE, intro allI impI conjI, goal_cases) + case 1 thus ?case by(auto split: list.splits) + next + case prems: (2 ws ps ws' ps') + note prems(2)[simp] + from \test st\ obtain wstl R S where [simp]: "ws = (R,S)#wstl" + by (auto split: list.splits) + from \step as st = (ws',ps')\ obtain P where [simp]: "ps' = (R,S) # ps" + and [simp]: "ws' = remdups(filter P (map (\a. (Pderiv a R, Pderiv a S)) as)) @ wstl" + by auto + have "\(R',S')\set wstl \ set ps'. Atoms R' \ Atoms S' \ set as" + using prems(4) by auto + moreover + have "\a\set as. Atoms(Pderiv a R) \ Atoms(Pderiv a S) \ set as" + using prems(4) by simp (metis (lifting) Atoms_Pderiv order_trans) + ultimately show ?case by simp blast + next + case 3 thus ?case + apply (clarsimp simp: image_iff split: prod.splits list.splits) + by hypsubst_thin metis + qed + } + moreover + from atoms + have "pre_Bisim as R S ([(R,S)],[])" by (simp add: pre_Bisim_def) + ultimately have pre_Bisim_ps: "pre_Bisim as R S ([],ps)" + by (rule while_option_rule[OF _ result[unfolded closure_def]]) + then have "is_Bisimulation as ps" "(R,S) \ set ps" + by (auto simp: pre_Bisim_def is_Bisimulation_def) + thus "Lang R = Lang S" by (rule Bisim_Lang_eq) +qed + + +subsection \The overall procedure\ + +definition check_eqv :: "'a rexp \ 'a rexp \ bool" +where +"check_eqv r s = + (case closure (add_atoms r (add_atoms s [])) ([({r}, {s})], []) of + Some([],_) \ True | _ \ False)" + +lemma soundness: assumes "check_eqv r s" shows "lang r = lang s" +proof - + let ?as = "add_atoms r (add_atoms s [])" + obtain ps where 1: "closure ?as ([({r},{s})],[]) = Some([],ps)" + using assms by (auto simp: check_eqv_def split:option.splits list.splits) + then have "lang r = lang s" + by(rule closure_sound[of _ "{r}" "{s}", simplified Lang_def, simplified]) + (auto simp: set_add_atoms Atoms_def) + thus "lang r = lang s" by simp +qed + +text\Test:\ +lemma "check_eqv + (Plus One (Times (Atom 0) (Star(Atom 0)))) + (Star(Atom(0::nat)))" +by eval + + +subsection "Termination and Completeness" + +definition PDERIVS :: "'a rexp set => 'a rexp set" where +"PDERIVS R = (UN r:R. pderivs_lang UNIV r)" + +lemma PDERIVS_incr[simp]: "R \ PDERIVS R" +apply(auto simp add: PDERIVS_def pderivs_lang_def) +by (metis pderivs.simps(1) insertI1) + +lemma Pderiv_PDERIVS: assumes "R' \ PDERIVS R" shows "Pderiv a R' \ PDERIVS R" +proof + fix r assume "r : Pderiv a R'" + then obtain r' where "r' : R'" "r : pderiv a r'" by(auto simp: Pderiv_def) + from \r' : R'\ \R' \ PDERIVS R\ obtain s w where "s : R" "r' : pderivs w s" + by(auto simp: PDERIVS_def pderivs_lang_def) + hence "r \ pderivs (w @ [a]) s" using \r : pderiv a r'\ by(auto simp add:pderivs_snoc) + thus "r : PDERIVS R" using \s : R\ by(auto simp: PDERIVS_def pderivs_lang_def) +qed + +lemma finite_PDERIVS: "finite R \ finite(PDERIVS R)" +by(simp add: PDERIVS_def finite_pderivs_lang_UNIV) + +lemma closure_Some: assumes "finite R0" "finite S0" shows "\p. closure as ([(R0,S0)],[]) = Some p" +proof(unfold closure_def) + let ?Inv = "%(ws,bs). distinct ws \ (ALL (R,S) : set ws. R \ PDERIVS R0 \ S \ PDERIVS S0 \ (R,S) \ set bs)" + let ?m1 = "%bs. Pow(PDERIVS R0) \ Pow(PDERIVS S0) - set bs" + let ?m2 = "%(ws,bs). card(?m1 bs)" + have Inv0: "?Inv ([(R0, S0)], [])" by simp + { fix s assume "test s" "?Inv s" + obtain ws bs where [simp]: "s = (ws,bs)" by fastforce + from \test s\ obtain R S ws' where [simp]: "ws = (R,S)#ws'" + by(auto split: prod.splits list.splits) + let ?bs' = "(R,S) # bs" + let ?succs = "map (\a. (Pderiv a R, Pderiv a S)) as" + let ?new = "filter (\p. p \ set bs \ set ws) ?succs" + let ?ws' = "remdups ?new @ ws'" + have *: "?Inv (step as s)" + proof - + from \?Inv s\ have "distinct ?ws'" by auto + have "ALL (R,S) : set ?ws'. R \ PDERIVS R0 \ S \ PDERIVS S0 \ (R,S) \ set ?bs'" using \?Inv s\ + by(simp add: Ball_def image_iff) (metis Pderiv_PDERIVS) + with \distinct ?ws'\ show ?thesis by(simp) + qed + have "?m2(step as s) < ?m2 s" + proof - + have "finite(?m1 bs)" + by(metis assms finite_Diff finite_PDERIVS finite_cartesian_product finite_Pow_iff) + moreover have "?m2(step as s) < ?m2 s" using \?Inv s\ + by(auto intro: psubset_card_mono[OF \finite(?m1 bs)\]) + then show ?thesis using \?Inv s\ by simp + qed + note * and this + } note step = this + show "\p. while_option test (step as) ([(R0, S0)], []) = Some p" + by(rule measure_while_option_Some [where P = ?Inv and f = ?m2, OF _ Inv0])(simp add: step) +qed + +theorem closure_Some_Inv: assumes "closure as ([({r},{s})],[]) = Some p" +shows "\(R,S)\set(fst p). \w. R = pderivs w r \ S = pderivs w s" (is "?Inv p") +proof- + from assms have 1: "while_option test (step as) ([({r},{s})],[]) = Some p" + by(simp add: closure_def) + have Inv0: "?Inv ([({r},{s})],[])" by simp (metis pderivs.simps(1)) + { fix p assume "?Inv p" "test p" + obtain ws bs where [simp]: "p = (ws,bs)" by fastforce + from \test p\ obtain R S ws' where [simp]: "ws = (R,S)#ws'" + by(auto split: prod.splits list.splits) + let ?succs = "map (\a. (Pderiv a R, Pderiv a S)) as" + let ?new = "filter (\p. p \ set bs \ set ws) ?succs" + let ?ws' = "remdups ?new @ ws'" + from \?Inv p\ obtain w where [simp]: "R = pderivs w r" "S = pderivs w s" + by auto + { fix x assume "x : set as" + have "EX w. Pderiv x R = pderivs w r \ Pderiv x S = pderivs w s" + by(rule_tac x="w@[x]" in exI)(simp add: pderivs_append Pderiv_def) + } + with \?Inv p\ have "?Inv (step as p)" by auto + } note Inv_step = this + show ?thesis + apply(rule while_option_rule[OF _ 1]) + apply(erule (1) Inv_step) + apply(rule Inv0) + done +qed + +lemma closure_complete: assumes "lang r = lang s" + shows "EX bs. closure as ([({r},{s})],[]) = Some([],bs)" (is ?C) +proof(rule ccontr) + assume "\ ?C" + then obtain R S ws bs + where cl: "closure as ([({r},{s})],[]) = Some((R,S)#ws,bs)" + using closure_Some[of "{r}" "{s}", simplified] + by (metis (hide_lams, no_types) list.exhaust prod.exhaust) + from assms closure_Some_Inv[OF this] + while_option_stop[OF cl[unfolded closure_def]] + show "False" by auto +qed + +corollary completeness: "lang r = lang s \ check_eqv r s" +by(auto simp add: check_eqv_def dest!: closure_complete + split: option.split list.split) + +end diff --git a/Isa_DOF.thy b/Isa_DOF.thy index 4977bcd..89034f8 100644 --- a/Isa_DOF.thy +++ b/Isa_DOF.thy @@ -16,6 +16,7 @@ theory Isa_DOF (* Isabelle Document Ontology Framework *) imports Main (* Isa_MOF *) RegExp Assert + keywords "+=" ":=" and "title*" "subtitle*" @@ -1377,7 +1378,7 @@ fun add_doc_class_cmd overloaded (raw_params, binding) raw_parent raw_fieldsNdef |> DOF_core.define_doc_class_global (params', binding) parent fieldsNterms' regexps |> (fn thy => gen_antiquotation binding (cid thy) thy) (* defines the ontology-checked text antiquotation to this document class *) - |> (Sign.add_consts_cmd [(binding, "doc_class RegExp.rexp", Mixfix.NoSyn)]) + |> (Sign.add_consts_cmd [(binding, "doc_class Regular_Exp.rexp", Mixfix.NoSyn)]) (* adding const symbol representing doc-class for Monitor-RegExps.*) end; @@ -1416,8 +1417,6 @@ writeln (DOF_core.toStringDocItemRef "scholarly_paper.introduction" "XX" []); \ *) -ML\ fold_aterms Term.add_free_names; - fold_aterms Term.add_var_names;\ end diff --git a/ROOT b/ROOT index aec2f99..9c69ed8 100644 --- a/ROOT +++ b/ROOT @@ -1,4 +1,4 @@ -session "Isabelle_DOF" = Main + +session "Isabelle_DOF" = "Functional-Automata" + options [document = pdf, document_output = "output"] theories [document = false] (* Foo *) diff --git a/ROOTS b/ROOTS new file mode 100644 index 0000000..1d506a0 --- /dev/null +++ b/ROOTS @@ -0,0 +1,3 @@ +AFP-contribs/Regular-Sets +AFP-contribs/Functional-Automata + diff --git a/RegExp.thy b/RegExp.thy index fa6a4af..3b8af21 100644 --- a/RegExp.thy +++ b/RegExp.thy @@ -1,25 +1,35 @@ theory RegExp -imports Main +imports "Functional-Automata.Execute" begin +term Atom +value "Star (Times(Plus (Atom(CHR ''a'')) (Atom(CHR ''b''))) (Atom(CHR ''c'')))" + +notation Star ("\(_)\\<^sup>*" [0]100) +notation Plus (infixr "||" 55) +notation Times (infixr "~~" 60) +notation Atom ("\_\" 65) + +(* datatype 'a rexp = Empty ("<>") | Atom 'a ("\_\" 65) | Alt "('a rexp)" "('a rexp)" (infixr "||" 55) | Conc "('a rexp)" "('a rexp)" (infixr "~~" 60) | Star "('a rexp)" ("\(_)\\<^sup>*" [0]100) +*) definition rep1 :: "'a rexp \ 'a rexp" ("\(_)\\<^sup>+") where "\A\\<^sup>+ \ A ~~ \A\\<^sup>*" definition opt :: "'a rexp \ 'a rexp" ("\(_)\") - where "\A\ \ A || <>" + where "\A\ \ A || Zero" value "Star (Conc(Alt (Atom(CHR ''a'')) (Atom(CHR ''b''))) (Atom(CHR ''c'')))" text{* or better equivalently: *} value "\(\CHR ''a''\ || \CHR ''b''\) ~~ \CHR ''c''\\\<^sup>*" - section{* Definition of a semantic function: the ``language'' of the regular expression *} +text\ This is just a reminder - already defined in @{theory Regular_Exp} as @{term lang}.\ text{* In the following, we give a semantics for our regular expressions, which so far have just been a term language (i.e. abstract syntax). The semantics is a ``denotational semantics'', @@ -27,93 +37,31 @@ i.e. we give a direct meaning for regular expressions in some universe of ``deno This universe of denotations is in our concrete case: *} -type_synonym 'a lang = "'a list set" - -inductive_set star :: "'a lang \ 'a lang" - for A:: "'a lang" -where NilI : "[] \ star A" - | ConsI : "[| a\A; as \ star A |] ==> a@as \ star A" - - -lemma NilI : "[] \ star A" -by(rule NilI) - - -lemma ConsI : "a\A \ as \ star A \ a@as \ star A" -apply(rule ConsI) -apply(assumption) -by(assumption) - -lemma epsilonExists: "star {[]} = {[]}" -apply(rule Set.set_eqI) -apply(rule iffI) -apply(erule star.induct) -apply(auto intro: NilI ) -done - -lemma epsilonAlt: "star {} = {[]}" -apply(rule Set.set_eqI) -apply(rule iffI) -apply(erule star.induct, simp,simp) -apply(auto intro: NilI ) -done - - - - -text{* ... and of course, we have the consequence : *} - -lemma epsilon': "star (star {[]}) = {[]}" -by(simp add: epsilonExists) - -lemma epsilon'': "star (star ((star {[]}))) = {[]}" -by(simp add: epsilonExists) - - text{* Now the denotational semantics for regular expression can be defined on a post-card: *} fun L :: "'a rexp => 'a lang" -where L_Emp : "L Empty = {}" - |L_Atom: "L (\a\) = {[a]}" - |L_Un: "L (el || er) = (L el) \ (L er)" - |L_Conc: "L (el ~~ er) = {xs@ys | xs ys. xs \ L el \ ys \ L er}" - |L_Star: "L (Star e) = star(L e)" + where L_Emp : "L Zero = {}" + |L_One: "L One = {[]}" + |L_Atom: "L (\a\) = {[a]}" + |L_Un: "L (el || er) = (L el) \ (L er)" + |L_Conc: "L (el ~~ er) = {xs@ys | xs ys. xs \ L el \ ys \ L er}" + |L_Star: "L (Star e) = Regular_Set.star(L e)" -fun L\<^sub>s\<^sub>u\<^sub>b :: "'a::order rexp => 'a lang" -where L\<^sub>s\<^sub>u\<^sub>b_Emp : "L\<^sub>s\<^sub>u\<^sub>b Empty = {}" - |L\<^sub>s\<^sub>u\<^sub>b_Atom: "L\<^sub>s\<^sub>u\<^sub>b (\a\) = {z . \x. x \ a \ z=[x]}" - |L\<^sub>s\<^sub>u\<^sub>b_Un: "L\<^sub>s\<^sub>u\<^sub>b (el || er) = (L\<^sub>s\<^sub>u\<^sub>b el) \ (L\<^sub>s\<^sub>u\<^sub>b er)" - |L\<^sub>s\<^sub>u\<^sub>b_Conc: "L\<^sub>s\<^sub>u\<^sub>b (el ~~ er) = {xs@ys | xs ys. xs \ L\<^sub>s\<^sub>u\<^sub>b el \ ys \ L\<^sub>s\<^sub>u\<^sub>b er}" - |L\<^sub>s\<^sub>u\<^sub>b_Star: "L\<^sub>s\<^sub>u\<^sub>b (Star e) = star(L\<^sub>s\<^sub>u\<^sub>b e)" +text\A more useful definition is the \ +fun L\<^sub>s\<^sub>u\<^sub>b :: "'a::order rexp => 'a lang" + where L\<^sub>s\<^sub>u\<^sub>b_Emp: "L\<^sub>s\<^sub>u\<^sub>b Zero = {}" + |L\<^sub>s\<^sub>u\<^sub>b_One: "L\<^sub>s\<^sub>u\<^sub>b One = {[]}" + |L\<^sub>s\<^sub>u\<^sub>b_Atom: "L\<^sub>s\<^sub>u\<^sub>b (\a\) = {z . \x. x \ a \ z=[x]}" + |L\<^sub>s\<^sub>u\<^sub>b_Un: "L\<^sub>s\<^sub>u\<^sub>b (el || er) = (L\<^sub>s\<^sub>u\<^sub>b el) \ (L\<^sub>s\<^sub>u\<^sub>b er)" + |L\<^sub>s\<^sub>u\<^sub>b_Conc: "L\<^sub>s\<^sub>u\<^sub>b (el ~~ er) = {xs@ys | xs ys. xs \ L\<^sub>s\<^sub>u\<^sub>b el \ ys \ L\<^sub>s\<^sub>u\<^sub>b er}" + |L\<^sub>s\<^sub>u\<^sub>b_Star: "L\<^sub>s\<^sub>u\<^sub>b (Star e) = Regular_Set.star(L\<^sub>s\<^sub>u\<^sub>b e)" +(* reminder from execute *) +value "NA.accepts (rexp2na example_expression) [0,1,1,0,0,1]" -schematic_goal WeCompute: "L(Star ((\CHR ''a''\ || \CHR ''b''\) ~~ \CHR ''c''\)) = ?X" -by simp - -thm WeCompute - - -text{* Well, an attempt to evaluate this turns out not to work too well ... *} - - -text{* Now let's reconsider our `obvious lemma' from above, this time by stating that - the alternative-operator produces \emph{semantically} equivalent ewpressions. *} - - - -lemma alt_commute' : "L((A::'a rexp) || B) = L(B || A)" -by auto - - -lemma mt_seq' : "L(Empty ~~ Empty) = {}" -by simp - - -lemma eps : "L (Star Empty) = {[]}" -by (simp add: epsilonAlt) - +value "DA.accepts (na2da (rexp2na example_expression)) [0,1,1,0,0,1]" no_notation Atom ("\_\") diff --git a/examples/cenelec/Example.thy b/examples/cenelec/Example.thy index f856747..7d4a667 100644 --- a/examples/cenelec/Example.thy +++ b/examples/cenelec/Example.thy @@ -74,10 +74,10 @@ print_doc_items section\ Text Antiquotation Infrastructure ... \ -text\ @{docref \lalala\} -- produces warning. \ -text\ @{docref (unchecked) \lalala\} -- produces no warning. \ +text\ @{docitem \lalala\} -- produces warning. \ +text\ @{docitem (unchecked) \lalala\} -- produces no warning. \ -text\ @{docref \ass122\} -- global reference to a text-item in another file. \ +text\ @{docitem \ass122\} -- global reference to a text-item in another file. \ text\ @{ec \ass122\} -- global reference to a exported constraint in another file. Note that the link is actually a srac, which, according to diff --git a/ontologies/Conceptual.thy b/ontologies/Conceptual.thy index 75a2c55..d74486a 100644 --- a/ontologies/Conceptual.thy +++ b/ontologies/Conceptual.thy @@ -1,5 +1,5 @@ theory Conceptual - imports "../Isa_DOF" + imports "../Isa_DOF" "../Isa_COL" begin doc_class A = diff --git a/ontologies/mathex_onto.thy b/ontologies/mathex_onto.thy index a58b073..31dfb3a 100644 --- a/ontologies/mathex_onto.thy +++ b/ontologies/mathex_onto.thy @@ -1,5 +1,5 @@ theory mathex_onto - imports "../Isa_DOF" + imports "../Isa_COL" begin (*<<*)