From 530727cccd0917fac258f56c88fab3d00b6a2b33 Mon Sep 17 00:00:00 2001 From: "Achim D. Brucker" Date: Sat, 5 Jan 2019 21:01:52 +0000 Subject: [PATCH] Removed local AFP entries. --- .../Functional-Automata/AutoMaxChop.thy | 52 -- AFP-contribs/Functional-Automata/AutoProj.thy | 29 - .../Functional-Automata/AutoRegExp.thy | 17 - AFP-contribs/Functional-Automata/Automata.thy | 55 -- AFP-contribs/Functional-Automata/DA.thy | 38 -- AFP-contribs/Functional-Automata/Execute.thy | 20 - .../Functional_Automata.thy | 5 - AFP-contribs/Functional-Automata/MaxChop.thy | 120 ---- .../Functional-Automata/MaxPrefix.thy | 92 --- AFP-contribs/Functional-Automata/NA.thy | 50 -- AFP-contribs/Functional-Automata/NAe.thy | 72 -- AFP-contribs/Functional-Automata/ROOT | 13 - .../Functional-Automata/RegExp2NA.thy | 442 ------------ .../Functional-Automata/RegExp2NAe.thy | 641 ------------------ .../Functional-Automata/RegSet_of_nat_DA.thy | 233 ------- .../Functional-Automata/document/root.bib | 6 - .../Functional-Automata/document/root.tex | 54 -- AFP-contribs/ROOTS | 2 - AFP-contribs/Regular-Sets/Derivatives.thy | 375 ---------- .../Regular-Sets/Equivalence_Checking.thy | 230 ------- .../Regular-Sets/Equivalence_Checking2.thy | 318 --------- AFP-contribs/Regular-Sets/NDerivative.thy | 85 --- AFP-contribs/Regular-Sets/ROOT | 12 - .../Regular-Sets/Regexp_Constructions.thy | 395 ----------- AFP-contribs/Regular-Sets/Regexp_Method.thy | 67 -- AFP-contribs/Regular-Sets/Regular_Exp.thy | 176 ----- AFP-contribs/Regular-Sets/Regular_Exp2.thy | 51 -- AFP-contribs/Regular-Sets/Regular_Set.thy | 457 ------------- .../Regular-Sets/Relation_Interpretation.thy | 53 -- AFP-contribs/Regular-Sets/document/root.bib | 36 - AFP-contribs/Regular-Sets/document/root.tex | 47 -- .../Regular-Sets/pEquivalence_Checking.thy | 306 --------- .../afp-Functional-Automata-2017-10-10.tar.gz | Bin 12261 -> 0 bytes .../afp-Regular-Sets-2017-10-10.tar.gz | Bin 22131 -> 0 bytes ROOTS | 1 - 35 files changed, 4550 deletions(-) delete mode 100644 AFP-contribs/Functional-Automata/AutoMaxChop.thy delete mode 100644 AFP-contribs/Functional-Automata/AutoProj.thy delete mode 100644 AFP-contribs/Functional-Automata/AutoRegExp.thy delete mode 100644 AFP-contribs/Functional-Automata/Automata.thy delete mode 100644 AFP-contribs/Functional-Automata/DA.thy delete mode 100644 AFP-contribs/Functional-Automata/Execute.thy delete mode 100644 AFP-contribs/Functional-Automata/Functional_Automata.thy delete mode 100644 AFP-contribs/Functional-Automata/MaxChop.thy delete mode 100644 AFP-contribs/Functional-Automata/MaxPrefix.thy delete mode 100644 AFP-contribs/Functional-Automata/NA.thy delete mode 100644 AFP-contribs/Functional-Automata/NAe.thy delete mode 100644 AFP-contribs/Functional-Automata/ROOT delete mode 100644 AFP-contribs/Functional-Automata/RegExp2NA.thy delete mode 100644 AFP-contribs/Functional-Automata/RegExp2NAe.thy delete mode 100644 AFP-contribs/Functional-Automata/RegSet_of_nat_DA.thy delete mode 100644 AFP-contribs/Functional-Automata/document/root.bib delete mode 100644 AFP-contribs/Functional-Automata/document/root.tex delete mode 100644 AFP-contribs/ROOTS delete mode 100644 AFP-contribs/Regular-Sets/Derivatives.thy delete mode 100644 AFP-contribs/Regular-Sets/Equivalence_Checking.thy delete mode 100644 AFP-contribs/Regular-Sets/Equivalence_Checking2.thy delete mode 100644 AFP-contribs/Regular-Sets/NDerivative.thy delete mode 100644 AFP-contribs/Regular-Sets/ROOT delete mode 100644 AFP-contribs/Regular-Sets/Regexp_Constructions.thy delete mode 100644 AFP-contribs/Regular-Sets/Regexp_Method.thy delete mode 100644 AFP-contribs/Regular-Sets/Regular_Exp.thy delete mode 100644 AFP-contribs/Regular-Sets/Regular_Exp2.thy delete mode 100644 AFP-contribs/Regular-Sets/Regular_Set.thy delete mode 100644 AFP-contribs/Regular-Sets/Relation_Interpretation.thy delete mode 100644 AFP-contribs/Regular-Sets/document/root.bib delete mode 100644 AFP-contribs/Regular-Sets/document/root.tex delete mode 100644 AFP-contribs/Regular-Sets/pEquivalence_Checking.thy delete mode 100644 AFP-contribs/afp-Functional-Automata-2017-10-10.tar.gz delete mode 100644 AFP-contribs/afp-Regular-Sets-2017-10-10.tar.gz diff --git a/AFP-contribs/Functional-Automata/AutoMaxChop.thy b/AFP-contribs/Functional-Automata/AutoMaxChop.thy deleted file mode 100644 index 78ceffb..0000000 --- a/AFP-contribs/Functional-Automata/AutoMaxChop.thy +++ /dev/null @@ -1,52 +0,0 @@ -(* Author: Tobias Nipkow - Copyright 1998 TUM -*) - -section "Automata based scanner" - -theory AutoMaxChop -imports DA MaxChop -begin - -primrec auto_split :: "('a,'s)da => '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 deleted file mode 100644 index 7facc84..0000000 --- a/AFP-contribs/Functional-Automata/AutoProj.thy +++ /dev/null @@ -1,29 +0,0 @@ -(* Author: Tobias Nipkow - Copyright 1998 TUM - -Is there an optimal order of arguments for `next'? -Currently we can have laws like `delta A (a#w) = delta A w o delta A a' -Otherwise we could have `acceps A == fin A o delta A (start A)' -and use foldl instead of foldl2. -*) - -section "Projection functions for automata" - -theory AutoProj -imports Main -begin - -definition start :: "'a * 'b * 'c => '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 deleted file mode 100644 index fe6612c..0000000 --- a/AFP-contribs/Functional-Automata/AutoRegExp.thy +++ /dev/null @@ -1,17 +0,0 @@ -(* Author: Tobias Nipkow - Copyright 1998 TUM -*) - -section "Combining automata and regular expressions" - -theory AutoRegExp -imports Automata RegExp2NA RegExp2NAe -begin - -theorem "DA.accepts (na2da(rexp2na r)) w = (w : lang r)" -by (simp add: NA_DA_equiv[THEN sym] accepts_rexp2na) - -theorem "DA.accepts (nae2da(rexp2nae r)) w = (w : lang r)" -by (simp add: NAe_DA_equiv accepts_rexp2nae) - -end diff --git a/AFP-contribs/Functional-Automata/Automata.thy b/AFP-contribs/Functional-Automata/Automata.thy deleted file mode 100644 index d9ad882..0000000 --- a/AFP-contribs/Functional-Automata/Automata.thy +++ /dev/null @@ -1,55 +0,0 @@ -(* Author: Tobias Nipkow - Copyright 1998 TUM -*) - -section "Conversions between automata" - -theory Automata -imports DA NAe -begin - -definition - na2da :: "('a,'s)na => ('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 deleted file mode 100644 index b420b6a..0000000 --- a/AFP-contribs/Functional-Automata/DA.thy +++ /dev/null @@ -1,38 +0,0 @@ -(* Author: Tobias Nipkow - Copyright 1998 TUM -*) - -section "Deterministic automata" - -theory DA -imports AutoProj -begin - -type_synonym ('a,'s)da = "'s * ('a => '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 deleted file mode 100644 index 40b8e71..0000000 --- a/AFP-contribs/Functional-Automata/Execute.thy +++ /dev/null @@ -1,20 +0,0 @@ -(* 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 deleted file mode 100644 index 8dd9c9f..0000000 --- a/AFP-contribs/Functional-Automata/Functional_Automata.thy +++ /dev/null @@ -1,5 +0,0 @@ -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 deleted file mode 100644 index ad272a7..0000000 --- a/AFP-contribs/Functional-Automata/MaxChop.thy +++ /dev/null @@ -1,120 +0,0 @@ -(* 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 deleted file mode 100644 index a4c0534..0000000 --- a/AFP-contribs/Functional-Automata/MaxPrefix.thy +++ /dev/null @@ -1,92 +0,0 @@ -(* Author: Tobias Nipkow - Copyright 1998 TUM -*) - -section "Maximal prefix" - -theory MaxPrefix -imports "HOL-Library.Sublist" -begin - -definition - is_maxpref :: "('a list => 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 deleted file mode 100644 index 0c99f48..0000000 --- a/AFP-contribs/Functional-Automata/NA.thy +++ /dev/null @@ -1,50 +0,0 @@ -(* Author: Tobias Nipkow - Copyright 1998 TUM -*) - -section "Nondeterministic automata" - -theory NA -imports AutoProj -begin - -type_synonym ('a,'s) na = "'s * ('a => '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 deleted file mode 100644 index 72bb562..0000000 --- a/AFP-contribs/Functional-Automata/NAe.thy +++ /dev/null @@ -1,72 +0,0 @@ -(* Author: Tobias Nipkow - Copyright 1998 TUM -*) - -section "Nondeterministic automata with epsilon transitions" - -theory NAe -imports NA -begin - -type_synonym ('a,'s)nae = "('a option,'s)na" - -abbreviation - eps :: "('a,'s)nae => ('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 deleted file mode 100644 index ad8c019..0000000 --- a/AFP-contribs/Functional-Automata/ROOT +++ /dev/null @@ -1,13 +0,0 @@ -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 deleted file mode 100644 index 0b9f149..0000000 --- a/AFP-contribs/Functional-Automata/RegExp2NA.thy +++ /dev/null @@ -1,442 +0,0 @@ -(* Author: Tobias Nipkow - Copyright 1998 TUM -*) - -section "From regular expressions directly to nondeterministic automata" - -theory RegExp2NA -imports "Regular-Sets.Regular_Exp" NA -begin - -type_synonym 'a bitsNA = "('a,bool list)na" - -definition -"atom" :: "'a => '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 deleted file mode 100644 index 0dc669d..0000000 --- a/AFP-contribs/Functional-Automata/RegExp2NAe.thy +++ /dev/null @@ -1,641 +0,0 @@ -(* Author: Tobias Nipkow - Copyright 1998 TUM -*) - -section "From regular expressions to nondeterministic automata with epsilon" - -theory RegExp2NAe -imports "Regular-Sets.Regular_Exp" NAe -begin - -type_synonym 'a bitsNAe = "('a,bool list)nae" - -definition - epsilon :: "'a bitsNAe" where -"epsilon = ([],%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 deleted file mode 100644 index 3674d0f..0000000 --- a/AFP-contribs/Functional-Automata/RegSet_of_nat_DA.thy +++ /dev/null @@ -1,233 +0,0 @@ -(* Author: Tobias Nipkow - Copyright 1998 TUM - -To generate a regular expression, the alphabet must be finite. -regexp needs to be supplied with an 'a list for a unique order - -add_Atom d i j r a = (if d a i = j then Union r (Atom a) else r) -atoms d i j as = foldl (add_Atom d i j) Empty as - -regexp as d i j 0 = (if i=j then Union (Star Empty) (atoms d i j as) - else atoms d i j as -*) - -section "From deterministic automata to regular sets" - -theory RegSet_of_nat_DA -imports "Regular-Sets.Regular_Set" DA -begin - -type_synonym 'a nat_next = "'a => 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 deleted file mode 100644 index 3a1992e..0000000 --- a/AFP-contribs/Functional-Automata/document/root.bib +++ /dev/null @@ -1,6 +0,0 @@ -@inproceedings{Nipkow-TPHOLs98,author={Tobias Nipkow}, -title={Verified Lexical Analysis}, -booktitle={Theorem Proving in Higher Order Logics}, -editor={J. Grundy and M. Newey}, -publisher=Springer,series=LNCS,volume={1479},pages={1--15},year=1998, -note={\url{http://www4.informatik.tu-muenchen.de/~nipkow/pubs/tphols98.html}}} diff --git a/AFP-contribs/Functional-Automata/document/root.tex b/AFP-contribs/Functional-Automata/document/root.tex deleted file mode 100644 index b5421fb..0000000 --- a/AFP-contribs/Functional-Automata/document/root.tex +++ /dev/null @@ -1,54 +0,0 @@ - - -\documentclass[11pt,a4paper]{article} -\usepackage{isabelle,isabellesym} - - -% this should be the last package used -\usepackage{pdfsetup} - -\begin{document} - -\title{Functional Automata} -\author{Tobias Nipkow} -\maketitle - -\begin{abstract} -This theory defines deterministic and nondeterministic automata in a -functional representation: the transition function/relation and the finality -predicate are just functions. Hence the state space may be infinite. It is -shown how to convert regular expressions into such automata. A scanner -(generator) is implemented with the help of functional automata: the scanner -chops the input up into longest recognized substrings. Finally we also show -how to convert a certain subclass of functional automata (essentially the -finite deterministic ones) into regular sets. -\end{abstract} - -\section{Overview} - -The theories are structured as follows: -\begin{itemize} -\item Automata: - \texttt{AutoProj}, \texttt{NA}, \texttt{NAe}, \texttt{DA}, \texttt{Automata} -\item Conversion of regular expressions into automata:\\ - \texttt{RegExp2NA}, \texttt{RegExp2NAe}, \texttt{AutoRegExp}. -\item Scanning: \texttt{MaxPrefix}, \texttt{MaxChop}, \texttt{AutoMaxChop}. -\end{itemize} -For a full description see \cite{Nipkow-TPHOLs98}. - -In contrast to that paper, the latest version of the theories provides a -fully executable scanner generator. The non-executable bits (transitive -closure) have been eliminated by going from regular expressions directly to -nondeterministic automata, thus bypassing epsilon-moves. - -Not described in the paper is the conversion of certain functional automata -(essentially the finite deterministic ones) into regular sets contained in -\texttt{RegSet\_of\_nat\_DA}. - -% include generated text of all theories -\input{session} - -\bibliographystyle{abbrv} -\bibliography{root} - -\end{document} diff --git a/AFP-contribs/ROOTS b/AFP-contribs/ROOTS deleted file mode 100644 index 05dd4f5..0000000 --- a/AFP-contribs/ROOTS +++ /dev/null @@ -1,2 +0,0 @@ -Regular-Sets -Functional-Automata diff --git a/AFP-contribs/Regular-Sets/Derivatives.thy b/AFP-contribs/Regular-Sets/Derivatives.thy deleted file mode 100644 index 6cfde24..0000000 --- a/AFP-contribs/Regular-Sets/Derivatives.thy +++ /dev/null @@ -1,375 +0,0 @@ -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 deleted file mode 100644 index 1abcc85..0000000 --- a/AFP-contribs/Regular-Sets/Equivalence_Checking.thy +++ /dev/null @@ -1,230 +0,0 @@ -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 deleted file mode 100644 index 724a3cb..0000000 --- a/AFP-contribs/Regular-Sets/Equivalence_Checking2.thy +++ /dev/null @@ -1,318 +0,0 @@ -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 deleted file mode 100644 index 7a9ef1a..0000000 --- a/AFP-contribs/Regular-Sets/NDerivative.thy +++ /dev/null @@ -1,85 +0,0 @@ -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 deleted file mode 100644 index 423f5d3..0000000 --- a/AFP-contribs/Regular-Sets/ROOT +++ /dev/null @@ -1,12 +0,0 @@ -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 deleted file mode 100644 index 2e2dceb..0000000 --- a/AFP-contribs/Regular-Sets/Regexp_Constructions.thy +++ /dev/null @@ -1,395 +0,0 @@ -(* - 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 deleted file mode 100644 index c0ef10c..0000000 --- a/AFP-contribs/Regular-Sets/Regexp_Method.thy +++ /dev/null @@ -1,67 +0,0 @@ -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 deleted file mode 100644 index 497ebe0..0000000 --- a/AFP-contribs/Regular-Sets/Regular_Exp.thy +++ /dev/null @@ -1,176 +0,0 @@ -(* 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 deleted file mode 100644 index 940138f..0000000 --- a/AFP-contribs/Regular-Sets/Regular_Exp2.thy +++ /dev/null @@ -1,51 +0,0 @@ -(* 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 deleted file mode 100644 index 938929e..0000000 --- a/AFP-contribs/Regular-Sets/Regular_Set.thy +++ /dev/null @@ -1,457 +0,0 @@ -(* 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 deleted file mode 100644 index 41e71ce..0000000 --- a/AFP-contribs/Regular-Sets/Relation_Interpretation.thy +++ /dev/null @@ -1,53 +0,0 @@ -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 deleted file mode 100644 index 8b5cb20..0000000 --- a/AFP-contribs/Regular-Sets/document/root.bib +++ /dev/null @@ -1,36 +0,0 @@ -@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 deleted file mode 100644 index cc5e5bd..0000000 --- a/AFP-contribs/Regular-Sets/document/root.tex +++ /dev/null @@ -1,47 +0,0 @@ -\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 deleted file mode 100644 index 05bf430..0000000 --- a/AFP-contribs/Regular-Sets/pEquivalence_Checking.thy +++ /dev/null @@ -1,306 +0,0 @@ -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/AFP-contribs/afp-Functional-Automata-2017-10-10.tar.gz b/AFP-contribs/afp-Functional-Automata-2017-10-10.tar.gz deleted file mode 100644 index 09e9e9af95d49d43adc19df921dc2639a4916a0d..0000000000000000000000000000000000000000 GIT binary patch literal 0 HcmV?d00001 literal 12261 zcmV2V{~b6ZeeUKL3MO*ZDDj_Eiy1MH!U$REio`I zbYXG;?S1`w)5fxJfA(LoI8Q<18aD|9?n&!H4$xEXLxBVBd++mxysm7o6M-$+lAJgv zP5<_HX7)q7tCj3PfO4+gr^J?4yR);i^R+XhpBBlmh|?sR+&Nej=`<>$@4mU_&o+D> z?Cs&--JP8s`n&yr{;JP6J9l^PKiJ-Ru)VkY&Gyc{-Q9cNu)S|S!)K8fQO4Le?rQ4VV> z!eN6b=OdO6qa@*3yVWXAc$%FvgPvOPbe3jC&Ym1Fb!otl4_e?ci3_xs`{bi1mJCw{k{*A~uQhg5B2NjEmwcbx;5l?CgYRywx_kJz#T|@tnqvvHizJpeml!7T3_9)*lga*nOTHv6NlmteWI%tO{gd|54mgfH>$lFdW^ z5aLNa2wr=1xP)<+IUsPv;ei;j+!7rR0bw4rL=11t-04#51DG9s3BFzCT?alSe)t08 z9v*cN5r?gEO4rTSh_@@%DecTMWfNaG5y2*d^+Vt77vf`s=5VF@MILWMrp!5GmZ1U zf)M9hgM5UK5D(}qCln2bdr* z-QLLmzp(soJh~E-_4nvj>m?3+7K6mZe$oZ(M(XKz z+PgUlyq**U<#U?D+-gP1h%Ml0+{Y6ZCwal65rRz@cDuH6gBwA9AIrTWrWMKUV(U5B zTq`-hM4;G6^`;c%On`z?90WJ$Fa!K&Cg>_Q1>Cw*kky(?m{xvL*&ax`x4Y(-WheqxNLLe+9lJbyMjx)42W?~?I#Ca zrK<%=v^$D|3%VHa0KsV?B8U4Y%uvkWg}RN}IRY%$oph_5g=9OE%V3|Lw-h;p`NDXt{i0;8 z2gFA!yq$(`SKTvZLmYs;uz%LhGOYGwKq-uHLgte=10rYK#VPk8mFKhJB+VBYF?u~R zm>08L z^lwO)=*J*UC$88Q{u?E>g*Qa}8@dNX1It&^YRgB*=!3`Mg>NVTp*;Ww#Re#)qw1NA zVBWs-7(J2%U5}*1W>0}DwE=fBip4f{jz}m^d^Ar6R{QN)+E;r3MKiB-A-sjT4L*_W)1>5|TtTb$|Bie92Y0tO{@>5?k$cgzhwCp-houM+s@2K~YBR~bm|rPur`qu9v)t48+O zF@KJ|WXJI+8_=|rLOWEhVnEqFyeiwZSa1XM`+w!2@#kGaN+53r6!*shxY7An9?BR% zv=%VxE=`6}fe*1q`1DQa2W*CY^dD1KXhHnhV;E+5Q>YrjFv>YSk&d+o7>p!4wx|tg&^D2UKt(9(x zVWGKv22dhGLl2KSB091DLqVfB+I+4;JmruWssa5qKCMO%G;cr3z6ExOTkK-=K(U}CkDuw_dvOUi#XG#ltSOos z6376(wJGUPC0t$k>h9Zz9u@1U}t6@pvy+l*P-ntGX)j*r^ zB$^6!Vwvv%L)k%bieGGaWRIvliXM@7_!hR*!{zz0dGyX`<0D{b3#p?Afu`~J$?lQO z3Dn}%t)0ck7C8^E6@&&sD75$mt<~LyjZ2L#Ouat_F(CUo912Xjj5<}r9%cYDKSG*D%7)_ zEVLfYewII);~Xt~&GZDvi=?#fR<6fYvT_ZZ(U*}+Ks2P|Rv!=MTVh(KHCpLOG}3*o z^pgnR9H!>ZG3!-?fuLmM+S)qQ7TA%}zqM&A@?8OKRe0yQSc1;E@*X0zZ-3xRz*_#} zqNKwGHGca;l#G64uMn68%z>svu?cb!WdoP;1G-ByrD@9{dxT0E!Y9op+|wp}!f&EL z?}e>T zTIA+KClnmYm%ID5fCY25g|iai5p)QaB))+*2>J5aAxyK++Vd??p#Xle?6A>UT$~WN zc-p=zks~4^nM${2OyX3|^`~f(*H6~$f-bCuW4X)hiKuPljLO(JOQ#OBddF$cP?}86 z_X#?B6w~FCoM%OOslyDyk~$tn1c`C=q}?Uf^WHV*&3xe4b4QlZE_s97t6Ys;8TD%J zZDcV_t+qjjdb2ay?QegWq{;DwkBiLkS&OrSncm4Lvs7nogHw4h2Xi!njizABph@W-(|3N6~FU3$jIyPB;X}LKj=X94v+2Two?H_4!=hL^Jesw_F;K zp)lcddp`&$5Q244Wss1EiW}A&dDfMeSv7#Rf(fs;w10(V#l2*srn0vFC97HTau?UF zW(5oyejP+%fOh#8|D}*^zxY0~U1tPm8MfF$Oan9dF{ojS%ThigM}!~GVLi;Xs47@O z7h}?YxnhshdC1Kg6BQLu)LU@8^Ja~O%AmI5;&HSnIC9f{4|AviYn9h#W0n7^ zH~xS3?t^=k`2UUl|Ml4aFVbYRA_d^Z)lvXhQkw%n$#>N}098Gz5|N+OMdV{gm8g7S zed0;{#q5$yOgqecrZeEo^fw)CK3gM-KUp)1|IA34^2G4hCNE;XlXpDIUqp<;MRV@- zzySsKUj(zxJY-!Ow4BwYfnbqN)ij^lL2`lM9(y(-)T(Q$-iHQ+y<}znn@&}rE0sWf z-O1^rGc#}Q)a|7V%|GpE&5zv8FZ)rRr^8aXCVgwHcsxF$q&UD%7P5Wjjv1&MK{@)% za%_DjFZ}sd-{iOE^F;*m@cgNEyNfI{^Ds}ODWDc5GYTRZDoapLUFF0X<6zk;nX7~3(9oo}gvaK!l21~+_DY1m@`lh|nIGW`@zg7ic zh5Wy}x9!${+Pk;AvyuN_z5JK{s#zX`UCN3qN^%lXxv3bG2_T>(H0T7Bf-hXpSa2#$ z#Km@nbyVaNuaiocA)*RKN#O%?;my*HJK~P5A@Fp{vsdnw3DGYV7`imTOG^;0R4w=w zbc?mwcngRG%wCppvdb4aAMLk*k%Iy3)3gE+jUMlh*I9GaySU6rC7l{AXO zKeV{kgMZJ0xvgiMu|JL|!p&7c&OC~RF|W0ii}D$*T$E$KG}fk99onr(V4Uxl(qF4s zR(w*@uMF%UMUPe@r37Xzq_`ujj}(u-$v#Zq3|HrolmZ;{vP4I&n=;uUgZ$zVRZNO%Xf6Hr_U{a}X}sf=BIC9RLlt0SK^xrGW)Mf4{ReO-p^w4V!UT(S0aBmc-`>V(JlUi0-?wE( z@SQij$lG*o3_4(pwT(yVkSc~^fdTaFA5|ad${+ow%bEEwwe;mLVucpbYkwS1WW#or zrbTxU58B4hf-l?uORYig{#RA^K1=-9?*04s9=P#e_wH}%zkN0K-%ohH@2U34MpQlv zbc!Mc17f9WoFOI|gx)zc`S#Vh1fCGDU=~Xjo9~2moj^+ruOtE=?w^ z27sQ?;1ExekLGCwl^4-ILWQQendKIx1mo$(|L=2>Tyb;empDT{dM*OG%_kxIEn$H;amA|{Ud_y?sXrJVI&X;-#4-I4NU(a!SHxKnp6p?A39|{Y zf^s|o*kI^!=0LLoCU`CvW5JVoCG!zO+^>v%dZ-!yh>9(^yXGQXT&{y(d#Q3DA2`he2FM5@>i)xUM8IBMcWN-OBw+2;pRG3JO#BH|DQ&fp1laLS!ji-$0O%b~=i$G9~&^{M- zzNr5A0iO^pX8(uKQTL$-KX63pIl#i_I0m}0sQ6+e7h@g@v%1GhVPhW5U_0v!NEB?B zeF^uV?hHC1LARm{>BgW=`skJ`&+AO1zwCEFVKAi>oh!*GBx?0VAaX=jIl-dG`r_Zx zn}UN>)xB>ky?$Jp2Uv6Sz^s=cD$gc#?eA zqz`>3Bw>0AW;gEC>OM}hJ~mX|zxItA&)I8PQxyP(AEDGIX7maKxc;2Y>^+%Ufm*6t z8oIe(YEpLmy0+t{dC~5+Cx%Vbf&wTK2nB#JoM3HbMW?d@2N9{69(l9)t&@l2O zzNeYPBkEke7WI38lQ>xoooHAA@AZd*w-U*@gJr67OsK{ta`)&7$(Vr>+53{asM(xV zaLu-uo{nt&oSijto^hHDdCUB6;+h~72yX(hM0qoe4#s8U*B=NXpqr673tF6fPYb(! z+Yya6k?3tCn79J7q!o))N|hR>fb-NeJ;N!8A)j|<7G;B0?5g5HId|j1*T#cLb04!O z)Vh@NNl%R#ZhLE4FnvWyPn6~-AFK$d#YkN|4S+mhGE2GwNORu1Z?>QN5-bNxUyVJ%QeaG7hB zn~POWA$RBC$XdnK%NZErw&x04wx+ZNIGZFc@qHiML}Z%M1nkc=?pfsw8M#_dc`#u@ z!sliPD`Q$~8h6Imu}c{Q*(&mopa|5h-VYXqD|((gB;veU)xppcyKqrUp0>MN(phCp zZEl%c(hfOzPC-GX1|Bl8FQM%MW^mdiLRmbDwoaj)C8Pb_EhN8tPWq+$K;A89pPRGy zv@Ni0r!d9*sf1Nvy$C~-39P-~s`v%fRT{vpx2@{je)EJ`8U$NB+g-Da3lRmCIKi`#Xlv2NJ;#^Nyv;4e#~RFE7{o-IJrW3h zJy4}>mEAhTOzP(f(#7rbZ%ecwqKRJuQRT&r{mNz+^-$Cemsv`^g`mQ`xv_2BRBRiG za?QSks#+pjVp1xqj#BDVP@;)m#!@daI-F4ulcV?u>5jQ|dO(f%JPhlN0AnR)8k4!! ztny}6z^(36uM-%W@z7GXD{^yDQW>sqsednwU$FLT>fg@#8W=VfFl?x_RVg3jHY%-^)Aq`zYdF|-8#C&_=hGbSUxo4$uV5;nESxBC;r1e%#ImdAg`or_#gjYypVOBVYWtH`6D+`OaweqOQC(vZF zo>mw-i@wNLth%R`BM!F4`WkyRcbvNRO4M#tm$8Iv40X*Tt^a^e=Pw1HsrZ*$pRCb` zwA7jkZaTaFW&=%>Ywl6so5`S7OCHJe4~MgbYwOj{=D89$)~58}zT8HiPQemUzMoFP zQq#wAEV>Z!TctUOK7x97;LwR%VVN*xRz&@91FwPMudsa_?=2orKTb1@^rhPW>6m4^ zZd8Nw!gHbHoRyO|W4fwuQg?K(OjYGtj|giFQO{!{xPa4&k?C&5wO>5(mCKxrw|6fxYcys*!z1^L?`<42yyPNmFe*N+P zO=165Zn!50fUlPXz?-uGxGxQWuM~pG`#SVfOEcF0 zT8R5fBwen=l^3GA4$k;%t%71FKExAjzAO%jbtfT#*JdPeHzk38Ku!W*nUug+WhL-R zS_0GRC^vHqxRYeS8*&p?JXoKez`sm>!sei%_Mkz*dMzgne&gV?95MVaNk9oiMT(21 zWEYo2Rpj0+i=9yCWljoQF$NGc$f~_pDe%g9E}}-wAiP?-%ZFvVTx+_E75n7Y_6z>IL+-_(m~{$WSW5@n zV-2ew9?b=G3S7*}^b5Q$YNDAHxt`-AH(8;VU|!)tbk?HSjC0%~{N1%@92Qr#T;pYb zMcS7?Y`!BVJGkOxRnCZiwy%xZs)*IU(sXwtQ?`~1WJUe5GVIquhj%J$y}5i4xPuC~ zuS;;%=3+){@RtLa*pyK%%}6D&cvOYLns}66Au0F-Oc=?yuQsb%SVyO+fy81+O`ud6 zl16_mECaP_;n$gXM`p}lI`7VaP(-!b_6~b0?Ip$DQ>hi!U4cL~Wdo?35f$MZAS%!ul9z`)MB&r6GT+)q6n+C= zZHu8om$m7Y#{M_sqUKJRG9aQPSrudKO{l9{SV>y+t+Y>J=dA?pPgh@3 zW$QVH-r$zU_|Y(y=Fcave?FZ(3r6AD4LW-@x&fY?GTt&>8 zL{w_OtfIWv>uMgA{+2T_By!q&SHZ;Y_(5 zda`W&JF3hcvl49sF|E?l_NUi=NeXO868>Zf!iERegSa*P9p0y^-koSo4(In~iA+b} zafbIw5TETn33XQF90}FrewtQIXIPm5X=f;xoAmQD%}6m#=D3EMJVRfIV&Pv?(9W#< zZj$e{tlpKw;(Zm?i*`Kq0vz%3MdgbKMFvnlYQJl-hq+fV`H7F3pJ1UT#DfpN-KT4n8A35g{mRH*S$IHE%6{d&k~dk_ z)8R~Ov-dh1>Enwo7$_~1f_;@2GKB+8<7NSdGTT;jqIHWetX+FS?oxjN21IPuz>*s3 zF*rw}D>AY@B^qi>r4`-Q1ol>6QdoJFV))l70%5l}eRQ~NOjciOa_fb(dGh3O^s1S) zmK|16c2^o^hB9pGS@jie>O9|i>wKWu-{9UBnvPHX2^*_wkl3tGmY1$?iyOGQk25)6 zWeqh=peqlpG-hsCHwWiU>YjxKM|Sw$geth|-#Kzj5&bkO-={^nv%*-EGkeIMr|C?v zWqM)EAR4~M1YEmSGruiO`xVT!_m^U=wLx2cp;Eh*8%tC8m(!H#rJb*W)qHj1O_8o- zy0u2exp`^)P|S%s`p;YwZC$NCx4E1J6YI6uTG3k?DjB|Y(DKwx($rKlwJJ5K1g)%R zlPsC1Hck3EX`}`x0*Uz&uxikUBK%D$yIkH)f4C%?#~Kii1jI zOj&Nk?U*Lk(6haS_1yxCE7Fu?_k zVMT#mdWE^gSDJJ9T_O)KZKd9s!h3})1g+(mnYF8FV>3` z^qK8z>QEnAyN1^mui@8Jy+)w%qsrFU4btr2y^PJ~bG`L{fDHQSxSvEt|H((c2DrKY z&(6Kw-5tCB&+hj2-MvlypTBVZpVqG_JLU<`P|=M%#eX`a4o8#ONi+b>e+p=31J0-- z2k*Av0jvj+a6Y0kL2xTy0JDj~$|2(>O0ZG{Ig?Py#AJ_nzThm)Mm%e^fEo3vuEU7M z>>bO5h74K*mduFZ`#Vwo;9I~gFH4H6U z3gk#VwJk@Cd)8Q@wgWvDiX7l_nEK)y1eV>{Q)8*7k`mxgEkI6hRyT?%SsQspNhSEv zW>0G0tBidle2MR9mxYbsiu?m(MuP!}?>G_#SMXrIi1gc4%V&So>uPr(i-CYmB%kcb zHQ6^ZEs7ezU7vE#UM~{T=UEX+4H^d#| zB6Q&v=@EC4T%Q~e;;?WR;3phKYhg-0c>uiwu6}#L-tAw!>#}!0yw|5A?=HJ)9s#X~ zHdgSP2c|)~NJhYv>emq~i)lbq^O1nzM$%;o`vHE4GO)`o5f@zwjXE#F^u{R+76mG) zebBr>VR}aOBsygG9kB_p);=tVxO&9mX>`mnm#wS{!=3|ba--OV>W``)lzxXmUKi^3 z;Sm+2pi)1}YOSC1t#hjMb1ti$4Wvn(Gu$sYHkPI_YhoA^5sD!lST4~CWQ;64c*~r8 zL(4oDKg~wUT?aQk;Ye_G)%#d&bc$%90V<~0B(KDmy}P`-^yBKXlk^OQ0uUG2)oD&ug6UDWt78VvoOSs_Gb@S&`nDCfKG|7uye5d zb*J!~_NHuDsiIXg%zJ#$7)1?J*BT~cw)W6&om1T?${dl-pq~UL!15xCXPy$tii^K* z*B%%}M~yGXFgkOWG@#x?gr@C{va4Lg^Byypt|9P_FQ110QRltDwcWxc^f)o>mVof) z61HocpE8MH8pgXM zfDwp04j<^r%cMLFoDEQs9b%VCZmnx6$^P{g4wm_&bLboCU0(zdRc>-%GI6-Zcm!+B zaHe7?#_KV2Zosk1{b3CZu&h0{V1Y*2s2d;;nG}e|oUvm}uO^uZFdEPqGO~1F2GeN9 z%C!jTwhL7~SaIHe5l`&(wN|#&8r1hvFHpj-srSceBHwvYPTlE0*-CPuc~&(ORsK<_ zCJCwS=kVxFmgL4tC9oL2RAl16C5aP^4GG7vxAl6R3I`xyq$>6ZTF}x-^2-X0vi73T z*Bw#`{331XkH4-L8l}b~h5nS zYm}8`K0tg-)w(!18OSB}`k3vl;VRsuYyVbxv!QSsyQMVh>aDLiM6DX*Uw@nqicOxe z-D-^gjz77@Ok46r;)`%OM;j1@G_)3dv}P=cPo}$XS#*sSx`r5WuMyzPov=kR0`>uJ zv(Rl=Y9-$Hh*)qN%%M5gpmqYHhrT>tuuU?t|KOi})ZuuqhHr za%c@VFnI&??*+`?1AqQOGyAGTsmCss9+l_apQcooz;?-3(;>A~!i1DNw7K6Q|*eOQ28>BaJ5`b^77%SToofS);M-DczJ zQ6P}|F^RKxNcG2-8EvkFK(&cYE02S2Y>o*3a_4`ebhw!Er1kg&vg@CvY0(|TgHQVYm+kGn?R(DpKiJ#ey#M91d>+NgEK7%+k6?EB zg*f-U^XsdhUp~+O_Me@Ij)r>|*0Jzqr&Ywog!eA~4+s4f&upLbWju@~>;MSqJdbl| zGDy?+ve~bA9LcBbRhFJ&S|liiKgY)>pmM#$<6QPUJ&uR?3_wxfaR1e1|HweZos&!Y zmo9t3&-ghsm@NiibitFoH?s`7;#mjG-I(XS=Pw?=>71q$pxoZY&bWt=3z$ z++bbh`Qgsatms7dX3>miM;DmKJe=^$*4stSXVLIIY^jSlk3gB5@Q(VDpHDAat=6}! zIEizXpQH=adg%=$jP!5$B!f;yR#&sp7!<|D3?6?=VFwoq8oWa6@hAMXhlOO~x_W1z@F^hkcqZ zrIOLvF;gwS%lL#^Q1{q~5|-oQyamsXC^w4X%Rb&=kc@f?ETNx)0dW;pUf|0>(9WAi z=ZITiRw9;$v1bK~^A@1}EKx^)B1EC^zLkp(0rSQ1M9-`X7C=6Xl7wfiK!)|CSqQx{ zipRzEP=PrJ&IzB)&=+gqLUkpupgJ3#;ISfJ0Wq^E*kUF|pMcc>CK-S?OplZJU(h)k z^98bWe9sHw2h$wzyd+PNqRv{*%px{~KX~p5PZH_YK*R!=I7}d>E&-O7K%BGmV1VF} zLgEC|bX#x1Dlv$t^;X8@T)YH0PGb&K*TOScA}o+Zw3N^q%)13FF9r;ONd>k~zOP6U zMxVl@fn4#MrfM+m-U7ERisAwbMBYUi6DPyT zV#Ia$A+S_*f&hdVf~D3CXb?HhMJ|v=@+Ah{F+I+r*~xicoP%V+khRlG`_2U_J=h%S zt`tTaPr>H1`D{L$&*roFY(AUM=Ck>1KAX?xv-xa3o6qL+HGcj-*Bg$R02l!Po4ztg diff --git a/AFP-contribs/afp-Regular-Sets-2017-10-10.tar.gz b/AFP-contribs/afp-Regular-Sets-2017-10-10.tar.gz deleted file mode 100644 index c8c0869805b5e05f56248c8f924ae541ce1e0ed5..0000000000000000000000000000000000000000 GIT binary patch literal 0 HcmV?d00001 literal 22131 zcmV(!K;^$5iwFo*N8MQh17T)xEmCD?b!=gBEmLK5b1gD3F*hwSFfB1KE_7jX0PTHi zcN<5p;C$w*hsvf??JE1j8Gs;&nLg#u706tJItn2*x(?m;%I{^Kuy%+Ch=e0%>s{=2ogxk>+S zd`ti8pTBH=v-#lLjm>X2?%(^%#^x6M{ugooFJItiUd_@{h`)RsWqI+TzTTqmf6||Q zzWzUCWqz8@^3$y9&Q30Fa{V9NyH~UR-+Xg_^BZsd?|-`q>%Vck{(tySl?`Y4q!4Yk z_F{4@N=X+YJD-+WRY8@i-D-92h@JWDWK#CT(~~lkKUZ*l~AqWw?SHEM*^Tao0K2L;6m({ zliwz1)yG`CALg^{a<}|V6+F0iCDP(Z>=d(noR^bRRm1%K-TkZX`-j8Pq{<$(TGf1@ zXRL;{U9DB(Xdx18SJN^dm)Wo-WGm6@iS}9w-R|cfPJpJ$$=M?T1tqkOm$qAHCs~<6 z4{h1SP;~xpR!$PJE%4uV>v#6$RguL%?93)(F(RUt<)$dNuqFM~(I3mrg#EGQwS1G0Gu9N~7c_D)AC1z%D8o-QyzEp~clySLynhK~ zyrMhy0q)ikhxKbG=40C|j?k-9>E#&#(SFVvRpQ;DC}H^0!Ua$a#aE(A=z}V9Km&+c zqij4*MGA{m_32BWh;asRQK7DXj#GL6P=3rlJ(5juJlF`Gyf~Um`o#&S^VuYcbX~>! zuEg1rou7%c9OSbyEiZazB$!$SU4~P5_vWW(FNOU5heHFj8VCR;0oALXgy-XRQ^QWF>UvWWLTPQ>_nJ@ z7^kx#P)pA;iKFZ|FY+1ts0lGnauM#os%q-xIu{{01DuL&{y_po}WGvo%avl7Es|)xu)h-R$Xzac-WdK zuPnx72mS0*KOd(bvYy}RHug43$AhC3y6XztNh1CURoc)1u!Vbt%ZKT81%!b8#2C<2 z?;hml0L$d3>xXV$G zFG{D{6i-C8Rg3>EvjFhNW*|H^>!e5G4_+0MAr4)gfUd~_fbriA4eY#1itGLq4q7mU3QJDX(@f+iz)9Xe+$oM8m0hv=xG0s6)8S0_ zr$N`;mvv-2_t7o8LHr?gkE)64>;1!{$*g+hv~5}!*$>;ye7Te6zU{34>ButLaio0s ztE`ug)UBGn186%gzja1ZL(MCs@BG9lJgfF?MW2gVP?%v`T@aBqEmZA_+kV@k+xnCp z1-Mq&Xxg~k60qd1J&NzzIs`~;!bJR&QM)xSjwhod;vZIn=2T+P#fOe<(R%Dx;plpk z#)hvvHeex$VDU#h^JIA75U}B=Svk8vb4nu)?MaC#5d@spBJlUmRi0IsJN$&8adfWE z2RmIuO6Pd~@q`HBL`sS0i0QPd=BVc?{se~$eSq45fA`>k#Sd2u{f@AC+79Fr2i2)4 zw;qfOCwIG64t#jbLS|6TLCt>qvOmhwYL-N&LPE7yGkRyoirrnQq;w+SIcmE4vfH4x zXc&_Qe+ zyJV+1yPEWgmNB-j@`M=~6qU1O#t-qD4!e#zgDiPGU9qNwKw{ejB40;oSAc=~r#JNmP9D9+P_bsm}S(WJBKNjrVc6r(rr|@Snp*;$xfcFof zPcqnK=b(aCkLF!5hvU&HV5v&%F2kPu^Az=N4^zOUX!>qz(~b zqy)n+G5#P=T4)s^fYR?YxE?l*u4jg!|}aysnbGgajkl3CCt@Rah0LnySS?;L1CgMx2KlZ~7;jzN(D-ZaeW4jjvkp7<a&2Ha{ltccms1|CBZ*I$_= zZg{;0#Qb2`2$%~>!~(XN)LVqFgG!HOG6`R^u0FDuUQVTK26f1U7r55_LwUo-!yz9*r zp9wKjR4x^+;Gb~}Sq-X;y~nH7VpNsDxa#xJ&(mJ&XR7oAtE{|x^&`&oP%ACVjNK>( zLxr0!jxT&H%}B5sj_@l3Rx3DS5OtcaULEjg(I&;{f(esQ(}`HG64eRbFE2Ff)Xa8! z^*M&94TWLdNv8%dEj0-?Ej5L>g8z>vWi~m@%GgfYHd~0U(pc*yEL|>KTJ$Aq*!gId zkJDM^it>SGjaH&ZC5z^g4T5E9{-Oj1$N!B=4(yd1ha|R)Qqb^;A&nc48i_^K@TI*P!hwUJ?}hzEajsEqZW9?Ytn-gl`*0-X7X~aa z6t#y7tKmuu7%dd zbTmClp&%cMv;1gwQsaf&>I{MCGPFRFX)~qD+5}0qN$jndj|W*f}Vigaci`c!3g2e8o= zznd~?qj!p=y*x!lXwxZoZOWSY(tA1NS3?lR5ljbVOkz3{^gR+Nczy> z_Zn3S2@tiJ_YX(eBOxnBC{(Le5&C3@9?yTz-hdH+R0bd=4%p#-f+~GE$DRf~E{7z{ z8XcbLP`cw#EwQ?STqp%(4-0QYsnXKNK>jEd0uwjfM53>qQb zwpwK@>OTLe&M83aMFnhqgJ4e4OJLYBdOB$M-1BS_v*Zv?#*<U3;*;%6Y8 zpYYj4uo%#uG@1a_y9K5naHsD#_z)-?i*LI3tSkLY6~>wNGCVtE*+8nBnr+|p7CkSj ztOOmW29dg}gE<_v8xU?8q&X9)#g+r~^J7$hYn8jh#K&!`jt*Iw?WVOUnybzx#ImhNd`#Yr*2})UDh=o!}-VRF@|^Kql>GwVRr7 z8`EjAK2u^34|Qh^6o(I9vf`-q=YRkC46o+XQC1AI{?ilCY=M#9z(dgH_n%vv_qHB* z??1o2cmLbl_n%+#{ioW=ANMROy5zNl?UZ`w zc$TLyg6Vege5BwF7AIwklR|HSHMkZgZlyJNGMz5Kml=?$ayYBbW}^EJ(IeFk_U=vy zkl`rD`8!J7MSZ z+El}%E!koCa*Oz)a=32$y{AY?+dy}~?v5uV=$wx_<$9IK#og}$Qshfyd%Bhdm2)wG zqo!molD>lWDPax$mSCNC^VjFF;Wosr^;13-dd*B{&oNtc<27^}+0uWv)~V z5+#CwX~jqwW^en&FNzxF0|)JxU-9D!EnWtd*QE3jZTxjxsG|zS4p^5@{i#RA+z1TG zZRppvI_TCS?lC?e^pS_F>4;JuDlZ&aRuiDr@Z;1TgLjgV~oT9Su5jcrsE4r6#f| zbzg@KUr3RsgurAlOY?$WW6Pfy|iCT>_h5A$tEVsIz9^t4| z+jdPAD#B>y1#DTC$C4J$=AbP)7t!yki}5%EIvpN58z{0`b$kI;Df+JvQmqP4FHeE>%wdNQC*$dSM%au7iWsVT zJ-RztULwceqbq&jP9VJ#F`43cMr7-8Q(UhSttrD%{|t|3qVqRm;$8N1pNF3yt=7~T zr&AUuA*~mx35s%8DS<Q|FFKEc;o5FF9xBaBkR zXip+?TO3Tr8JrIQyP!3J+#@WQfHq5^XMs|6SF10x45$k<7~dArb#_6Ysx90KZQW}% z%ce{8O4Y8tdC(aMWn?we(jhM}+)hBWp#IByaf;#7mUG540du_b+jQg{s+l8PJMu|T zHPbAbOarLjYxzXj#GN7b6Gt@BpiJeNDW!)%lC6~L^OcxUYl695gKJlyNU+YJF=OB~ zETF_Sa4R<%3S^{208Fee%EL$@Ijr~s1b_{RqbuVsgzKw57zC3-y$hR)oJ!avj6V%| znS5eE)3R=wy5a(n6(ARS%KTFRC_ zmY_|&ueSO-i9ryPnj;`4T!cZ%A*u3A^v8~qZBI|$j~`zgoY!bGQhD{cgq@Rf)=TOH zJU36?Jub6MZ5UKYn`FP|CX-oPsu-dz71UWYcZ$rWD?atPL5kN0Ln(_5Ean7vXA3= zLF2&A&bwKcyVG?2=kR(_3#HuYAYJklTWS3e#OXGA1|5xn36=stwhS*Z4E(Y~G`!Ba zA!mla6FoxXRP@Bo)vtHR)<8dAQ>5Ip^};v~pXtVDU2z7DQPZfPi?-*7z|~K~b))S8Kq%d*X4_A{JKLXUvy7mypXhJ~+(E zD(h=>%L-eXHJcTv5M`32h&jY)YJWMJ+T)gjtI)|ee&WfCK5Y+r=Gvz- zgz*B_+uoew3mc5W%I{9yPRFI8SFf}OBZ2zPngjKPapwviHbcIKjcTKPxTYDr*QrL|Uj16kn4dbQ#3&ke>v zH;4&tz%QDI%IP2@{pUZ0QXsmL7Z_b^%~8hIV!mJs8BtMS6d<7lYad-XaaFVPfQ+n% z|4}yTy)9%ANX=X?JLl^cpgmtO8&8KF(x&U5nsw_b)2%;A-CCR{S4xU#5hCi&Jii<1 z!);7g{yRugMqQLhl?RCm)uaX`iChutH>V0$nSHWY4Ig^c=q;!tAQ#5X1k^Unj$q6n z&@GP8m%y(Y!cvv8Xe_ob<@uT)QCK`%F1=raV&(z62VHiR?K}0WNv}fM7!2@AOxRzg z-$?n9t=P&wPI4+Keu!77rd;uf4y#C{7U3HD1j}Q1aTb{BbB=2}LVXdol8iP9$ITl5 z<5;nCuWdUbiw80nJk%C+0GpI!QGPFqO8-%PuXvxC7gS`kEYJm?WEmX%NceHiTHtPi z=}gp7NT2-si3j1Ea-NCb;V|JA|Co-d%wEh8SC`RF?RASYA9Lm1z-;LVPt$G7`L*KsDA7J^)K}QVx)jJfM@43*cYIYgnnVwQqEvou}lD4OS*zZRF(|b z5?u{I-|q7p=z@gXH3gv6QFKS7q4e>AD2N{t{`yN_YcC{$oKMJuYT8K6CTwC<8~MwC zjzg(_CVjZodW3rOU zKl7suc*hL+$-4LrcAUH63tEWPx4SN8TV8fWo7(1hC=`vUz0M2SF#|6zbj?noNO6`p zJ#Jlz$OV&-h zk&6ETIX|N-%^{>fa0>ZRbY_yBAZ2MzqDjkCWVI@9F{nIT4d=M4OKoA@ddQbmdO@6H z2nL>`_3*M~pq-c84aRvT`9RNG9?61kW_e^^k>!yeBFm$>AtKTI?je!NLnNB&9ErBD z4vAF5MPg!2Ep+Ny0vUYP*d&-37E1Dh|JovEMUlU;PkfImE~gKL_B3c}J2a$;x1qi@ zme6myDyyN?hHZhrM7}HB>Zi+U0aV3JJt)02bk+|_!_{+7y9ZvnlhT-2Lh)u_G=!G2 z!Y2H{mAW<|%Wfj{sz1o3^~+O7gUm6wC+Lv18KG>e*wQl-eTSJmy_TE|qym9k?nW$g3lBK`@k+1sjLdkuq=e+AP=Yc!y3=pqQw~Q;k z>7)K5ck-;$)t>Q9tNM3*cxgSY{v?n2B(Mof&U%wi`eg5}2YN@(*j#m*lJM?%$v1Tx zQ(0NzbTKZ9;OOC6NLc`NY zrT1uyxdX2=F|ovxM57?B_{0tEyz~GBrIPa+YZ+N2+Vc4gzABlLp@JTK;KLK3C8BcP zQr>xq-v#;pedW6hnQb@aK8&AG79g19-@KggY=FL|mYEQZf=)j$r>Sc>Q;VTk)wVb} zf{A{w9hK?Tw|OWtH6N<^aELm>N{@)XHxA2Z(DXPTk%7y!o_595eQt`wJ8o+Do5UJmSGu)m ziIvHJiD!sFLii3b5O4GVkuBGB(X+vLqnmt~X!OJ{`zTQk8xZfcUn=ScR__kEzuvUE zsTYe&=!a{fdf^cL7)B1mvD{L*Zel_rkuVS30hbF^1yqrn=j<@E~n~xy)SEvP-p0=K0*&ife=(vGc${bLw&eTXRFFX&+|RT z*j(>-*8zPAA9(ecj_R`uI}V$6WLN~DxdG${Ox3@O<~LJS5&_s^bO;hLYX}RAn;>0brju5>qcpSmqb|BcZEpvH;#g)=1s< zOIH;Qzxa20HQ@OFvoM`E5cYLR|No8q8}~Lm|Nr|BzPW$v|Nk%W|L0D-F%Ku@;m_l_ z+9)7m1d2{}p z4aBn$g#TGDq5o(8IOo6pSFhgu0b?vU|80D8|6A|;_szYHZ*I?jU*czYl1|aavGe0= zIIXEnA8k$*Z4m80zD5?#A8WS-1}BtuwMx930neDsQ5Su%v2iHxEhc5I{92(qyyE;h zo1ILKc*#>1yG~Y}Ml*@vm-wr4A&w@)`8X?P{o{P3#%q_8$*eob2W|EzoDABx?5uhJ zM^@zz&;Rqyy$271_zw@Zwr=0myPx0Xv<(DrG@)<-i4yqTS1fWDzH`Z$z` ze*zm9Po9WfHZx12gt5FKstqG zIjZTs12}jhF6e;iHlkbn5J5?+bnK%66CD z*`gH##NXi|FlMX!&@}9Mz2)nu%Gv4ukaEu_X441bF17pR=H>R{0}>PwzRGs^ff6R> zEg^2(Fo6L3!nUtzj124YtSgK^|EI3_1mvS%PwiY8+mUVq*qY%4-VG;58Dhohtn>ci zTQY8(Q3pF+83I#_K8$kg(t+t#UzzKw{p^#Hn69I=0tXmLKQH>GIfh#`3uS!G8EkR? ziXCZ+LZijym0m7pqu}5r0V=Zbbar8fHKSc#Azl~v$B54D)18jHTvxSISv00xx%jXV z{%NOkUg3n?l~gSLI%7#6CO(4BatrKI?k9gJYc#XS2zOU7x<9hZ&z!}Nm>?~9meZNC zT?xr@y4@ux(;xZm%jd6N#zvMO zcEm9btN*Yb!RK9uN03EHvhp_5%%7~s#;qvWy3(sixLDCbK@k{m25+?t$NKoN=n87^ z5n&7-=oX1h&pjW?Kgr1x|B{}O-oUaN3?6e1sRt+ukzGYKCog-q)m!D0WFoS+MgIuc zdYKQr?9EFJ!P)so;-?DcLR@yc4~r|)vMsou5gW&AfE)^bA-r7i7fZDnx{Z7e_!XDT ztCEEk+%D>6d6|)0r$LQ7{${U38nl2nkq{E;5ou)LYwk-BMYKi_S)^|1v9DJMjgyC1SXb z?gABEoAv?nW3C~-CZj^LhWJ_;9Nk`D2&asWYUp_Gueq zcx*)Vp+x(&vbwt|pmm43XO9>hr^q8`U}Lr%UsNvI+j zl~Gwp>2$j;j9ARCSHJ7A_v zeO-0cJhPL_TAH+1W~sIY>d#r2`1tkMuR}ielf=(4by!ap>PvB>I$7sJy@@MV&=?QR78l>yiTZ0x1O=-V0WARDTGD<7+7ZIa-$Z&1avRXZf5iq)m z4~*3cJOOnBz(fEUE@2Y!v|7(ZV(G_PJew#dW|(z#T~c+~d6yeTV<dGU}At;UCpNaY`u3q&ZEJ*$Tj%rM$$awa3{kT^Z|JCHK>Lw?HQ zc`B)m^^qGZp>72@ZWs{Z9iR(QWW%hg(lQ6-!bY>^~fPGea_YEo5CXgc&q?K~DjWm?hpJFB^#ksrO=88w*&1H0Rk%HyJ1PR6-_ zGQ+AdOtMR_!?%&1VscSoKbXVr>T?J#Nz|xINkv)J5sI}Vd*ixR3pQEC#MLyRgiTPM z6{_?&Q;|*2D-%xYyfU|_Zh!5T8`tcj62ED3z60Z5=!QEWY<|;!?6&0%diDti>0F>^ z#BZ>OBKDM;P1jgM%!SLH&Nqo3`@GtO|8MEdM7}6k_5@4$h@0qn!T#QY!M(T5@|&`* zJWF(<#53d~N7GQ7#wIu!Vq?jc9JZ4Ux%HWCwS-HXZ})1 zz5+Af&_ZGUP%p7;L+3@FdW*$sJN zxPxyFiw_{H0ED|3U1C+>lyc5j{;764bsUR-^mj3XEDgFqyQ6 z&98mAJF#u&69xa~(ggp)o>sGXEAV%;a!3&TGhvGTt=7@$A$;_UfeLVKX>F5KhBz=7n>79Nh;GGpHis+Isd zeplPT7T9gTI*Dn3*XYLA0KG0;4bb`MolE?&t%akJTq3Hze=oj>A+~NlCPVD~uY9L{ za}nScy#K#aD#&o>d67`wot$3bp62ONDd61~ z|2p-1>g}opNK31ZpPsTFioxX~6R@0Z} zoANQQ-&6AIowj|W%f7-tBYLG9j70dX%z=BHvcMd zV9q{0@9`L*GAyuvIqeVEZrKZ1`K^m`q6*Q_GB+JHwB9xGdy|%`8QUtnngpK=#d4JV z_`;tmgGU4BHIp-dcC#`qh9mWNA03!g#C3ejl6`8me%>>;!K29#Bc7s3(c-K#oUO~~ zUvEyv-SNl%ATK6U@#GRMS!23al%FsuDjMHgfa<0CN$c`~; zaUvKPf1g>d3p^=X%Fa>Iy z4~JQHL?aGo=Qsu_>Ict%e!cgs|MRmqKfU^4O>}gUk~jPRN5F9dFgF>UX8l<@l+B)8 z&Q35M6+YdUQKqhRyxuoIJ$t!Emo^_J>8ShTtEX=d`mcBPcYZ#gVJ}tI9em*qU9GK) zZnt}-0ihmX(9Rx`V*iKixaum>)q}6u(HW&**?7SS0qn>8I3LPASl5!a)|Ghq>g6-B z={EOg%$gEcx$+x4ef9Dm&-M@S9=h|>tG&sGeAq=wMq-yl(cy$ceJ07`Vc%gV&kr$l zG8SN5WOImCi+hv}^CP?^P=ehP>Wv9kPoQO=ZXrYmJ4;LeP#NM)MP8#gXeP3r%|_`b zE>O`uDCL+*o?s$&Gd`S2M-k+q3Z<_8{Oml%2qQf|0!F*T!_fcwH3%sZ4y=&m7HR1c z;r~;ko%#B|4nOkc;y-WRhrh!3&zraU|CfpXV#nGAB!4PNHckCQWTCuy0mI65F0 zXAfh~&PRUI=3IUbn?k=oYUf%I(+6RmVG0D+vV(_LPGPLgQuPgz{F z8;etho)8(Tq>oq<%Cf6&z3^t3Bhbizdi#`!z}u+LEorYpW1m)0h$wHng@2KtOBJ#3Qy!AOF5w5wtHY%!Xy2PsVN= zU7MtP+pV)L<;Q)U_`Imyx4!;l0y4v3=(sa7*o zg+6x0f1O-BM&7KCua4c>Cnyi>7%XN7UtTqtEn6}Nru0xiudhlv)ncWSO3bS{Jqf}? z&ImPXfO(wGFm#sH&Lqfq*24cIY-EMkf8aH}`Tc|3JLYd|Er74dr_cK|hXi7#O!6XTMbt6@a4ECa=?V+~@FDy0Vi*>Q5Q^*m- zU9nnnc)l|jmSkt1+y+sCmKAhxvfp?+)ARGH4{6%CjT*-R!NT{u#p?wEa-b zdl=iE1amm8ro~JtI{LP(LlqOzzNB9OXG%FmYnDFLD&w+>q@UE-kefd9lw)|$n6X>8 zzEKH&w_p0M>cc;wK&@#bm7=hT5vn{We<~hs!>^Hw{iJRH^F2C>xqzi#WTpt47$j1+ zVIciII*^k0b_FylKI&qbMU+dWJkqsoGo?)i#`Wcr4d`xBbUNLZOEyG~09>Vqe0ek| z(~ln?u_=9T<_Bx~{$VLA)PUQNKS1^3r9nYg@ScO2#0L+}@YNE)&6ebq-01_u;RF zIwra1qkdYA&0{fFv?jF+w=#J&fptqF%ae#>$aIk2u3wChN}O&!pG>TU!05T8tk4JF zj>*+pI!ziym1Ujxhe9pUAJ|!m&|LV5# zrh!BVS`eACxx6k}k22-V(Tu8fX;gHe)>ydB_jG&zt1t4lZtwzlf&b^${jG2O``>Rj zzrDTx{X+M@OI-gxJD&k_045Xh{fyoNZ~cicf~oN3WEPakY~VFrwOYz$sU^+82m108 zolJda)_>z0W?KPKD07&S<@!L})z_A`jzp;o9^%>B>ZNG%UGrys9V*A#!`Vyyn3jYc z9(WZMWGHwfw0E&LC4p0I#B@Iyr=vNoTq_`Ms@rP+9d0Vn=UHGTBBmNis+S|oAo!s-3 zoK$5LG<3N@M^-qAVf3;|Ng+D$mL9zj%IqX7Tz6WK2!M({wWApg^;4LGpZ8j=$!S)O zCaJwioq{&D4QP?Uc5wda7rx5W6~fWq*6JU9)meMh-mI69>1IPlJ5@Rf|Dtks(07@j zzM=fHHaPuK6vXV~Z(K!1zGY8!ZEl1x3US&Qsb`6AF0V8Qth}PBSTZ6V% zEF(hzToU!gR<+zrbjZ~fZWW`3G-ldxuHDrtJ-L+cI`EChllGPGfsJ(ioLp?y$tZ(} zoQod$5&D|hDU|O<%I8l`sRiy%DU)jial%J^_AVRcV~oUU;&7U*TB<7eA3UruP=o^u zd4Oq$C*>k?d4*l5)CBTMg2pic483TTvZHC0gAV0)1q7@++j08B4_MX;XgiKH!0%*; z-WNK89{l&I*-4bI@@c|mjZ6JkIqhdE&We~6ql=zUk;|w>t}L4V4=s75jLI>}dDU}W&Z=i+A*$nd%7{4MXw{(lyE zV&Je<)tWfRpaS*)I)lTfVw2+AF>qSVJpTS(;vK|ji*JsgNp=IKw8^M}kmJu^t zqvF4#j}xXu@f#qTywaqUSLE^~ALbyzMQG_c96GSprVB)f2hcF$OwUB{<9yG715#ZeTxMTQ*qcd4U#s1!P0sQh)-3qlqcx{59aUOPgFBl5V=7xH)-F*&XmNdeuq-} zie>tOB%qWKfk~6JS0Nk&ac>kAlFPDMrx0I@vE-YSqk^~*{5EzD*hLabFyh)t&^d{* z9*HiUCoMmwe>bFm70DZNtGc{O{80jLRMTZ2bT-2~I+s_yo>GqzlTFUbL>5-k?Zu@@ zoxr$foiZiGv3#leS42#JlStG$UzjoXAq+y-H}K2{GTipwoJZLbpVf=0RHe<0Drg{fHkDol#gl)G}|6w-5U*$ zHCt0222g_!_GMtHTmfVg=RE>)BvBj8g3^F#H@6tV5(h3|IJ%bEeYB<;SFr`xsRBL4 z*G71C)dDPkhc4VwF7&)qgDU>82Th{(tZG8=Y}m|zEDkPjspr6s9X(Ws)$TuAd2oY^ z&9(~Uua=xXnD@OAu(ZY^=l@(sJTj2YEi6)7KV=09UU~WoGc!^oXa$Jv$3UZ^BaiLD zs;9ZWs9iH5#*;Eb!-qG(Y3%@o9^lkaOydCa(JUXQvut#s((35bB}%IC*I}k4F49bZ zWu5FMf^)fBX}@8*1CuAgCMejhBi{H~NWG~DMTpm(5+9K*=?J3838ST_;ZQTNqIbwt zh*&n)=_yFRNbxUJJ|%Un3&pfxcS}@r3ggtS9Nu25Ec5tBHOpY$?Z5sNj^JI1}5jw+~bSwvSsg#ulkWE`PF*Lj{qXKpCF0W z^1ZRxBt4c~i*E^|!%ItK2X<=v@g7uqyx&eF85r*Rc+U}SP{RbIUl$o;&D`(Cf7K*k zJ84FXVBzDe%IP^qys{nEbS0Xiv$HA*GVrP~@K#GbvLcnqk`8K=&whcnGI>P+#s3m# z>ROjZCQ~F~sLxtH-iKQF(V|Ox(y=YAJj2{JZL%-pPLs2s%|oxokZH&r2US6&0v~Yl zN3aKGlNm7Ar*tJIETrl;)xh&5>0tCUg#Jg2kvP4*1>t?PhO#pXp#pnJgi2ZNAAJI z@BZ&OATcXulsrjCo2;VOYVrxHx;a|ulF=kUkzJfiwj|E+CiN?3-Mf-ICK%Msx46>K zeBg@GCDG9G5*L=?!WrF-fdRnCcFT+(&jM*-K#{C_11Q+bIeo7tItt1P^MI1yilRa) zca=EZ8;}4?EQK1hs_f}%rm|Akyz0XfI1QVwdG!I+M{`;V{|=(&G~N^OjR=%Mo+tf* zmFuEix62%Ted@ZTkC84_c}PZ{M6!)K%g zB`m|YKfKMB6<3?o%%kVZr3pX9r4!?!XI(3tU>AF}VLP4(-C)lPb#%rpF?+#vNi9Cp z(X8)eS5~t_D7HPY77Xbh(6z`p%1rM@8&Jy7Yy^S=oh$W$!bY6IBMu%U&q+l)UxVfA zdzuF7lU~fdA`DI6uVuUNn6fY^~|FE zI|_vXDAXy~CoV7e2S?vvd06F`;hu=!+v34nwZMfafJJH#1ACfM6`V^PKgn=-LnD(7 zM{aJIDcPTC<2?_bT9~|&c*$>-S}&$Xx2-MYH@ti@*$tf)ZnJY1DA<@3kxa(tJTc;h zlNgcAr_vou3NusJqTnJZvep}F574OWk~(dob4Hi5VY~h}{U}dC-}Q}y-tCi1gPv1{ zi~Q9cRO$#1gE>(kCy#=nZcZGGh`-ZPo56ZO-B^G1GlPBfbuhCUw<+FfgZ~t-R^v#; zt3*AjoC?XZ6VTuInXeV#k)8b7ls22=P=Bc%(8)Nh$1|q9$Y{oAPbkkmf56=(#*0Xf zo$@Fv)+(`wp!gTnDSqsqWTR(fQ$qb$9qLw=jIPjZGRk@PrWi)rZjONNuXj9wrtt|l1hey}x zXbuM;3{pPIe%Qk2^Bb59LisUmNXI)EudiRo!Zzk&AZSj4%my|uY-%*#XPJh;q zxTe>HVHEl%s%~Jc)_fK^Bu5NVjH53QIXldh<_nbFws1uT+YQPUHO7fUt|bB~uU3k9 ztqIwSiMX?){z9GS7wIxvtMmL~9ZHp?Y><(=w(>YxUgz<~*hrdm9)FB$>pY(`vxPcO zfY#)5Mq5_r@up;iw;gKN2VMb+kJM%Sv1&H!olTcG6>8FFt= z*NJSgo#j-W-QZ@T74YWhmcG?=uBGWnTrN4xXX-lcShd;?CxOM z)sF~<>7v3UuO_vtA8>zwNm~b$v^9w*yKZX2{IhV7Q#Z1fDV4F7WKLI8$f9eViq!qY z!)wW+(n;8g@rvCRPLwU(O1xvUqzn6^ zg?U&TN->XQ&0O7NDfl^@f)Xo_h`?sWJ1$Ad2>P6w|Q!{ z?HyDpU)!qDe+d%?r5>(rFx(Z9t(>yORjcK=`8$xSjJg^ye!X9+e7Z27taM-OMDxJw zyuLvuOOx>z&aIKGE|DC?ioi8H@sbpq)iyVExBAts{-^c7qsb7?QN`>(Zgvb*^1i)) zzfS+dA20sfz55#v{vz(*>VN;D^#=hk>kjh4mx=$ox#`FMeXt4DZ}tB#@be@sXZdiH zUCKazFYo^6&i;Bz0Rgu!F#=#(VBm83mAtZ?D1le&tyw-BW!smpNojbUr6p)u;W2_I zw5M+LDM9RvK4gP3g`WQ3WL_5OX#4U%yBL#jf@UDBm{yYlaDTOq4`{Y8UlpSq)by>5 z&CPWI$^goG%raeIc)MbD1w#8tUQjr`3h%s3ju@u zO#hR$uCNl#NvKK+l$5}JIN@vo_BxBPAL+vKeJm_N7&^%e3F^WFd6 z>HfFCad}0gmu( z;@^2y&FRm3_!mupV1Gb=OKjrTzi-~Xd+$40$PtO%wyp$Ba%ca|^QU{yE_aGqKF-U@ z>38?nWr7zo&40i&_17!;(a!Sq6`~0MUUt4jG*YR({P7CiZ8L!9O4H}%(<=-GQcCiy z)OZX*L_ry>4Ez~gWWn(9-F;QW5O`mg88mHu2Wa|c^E*JvtupoRCI8`s@k3gsw}Ue#NDuI!x=mWc`8WwC)90e*YfW=+l#VaRL+julc(81&Hfn4uAaL z6Fl6Ls^NxQhR(<7$Bck9;HLxN_vsM8r{vKXD^HB_0lKTB92s(XK)IULJrmC7gVw?UW~G=koR7)BYbZBi9I)Nv95RY;z2)09xkU! z7V`4E(vTc=h4vp-4#Uud9-L%o9l;K3I)Ft_rS!%=WO~^wf(Im|A&U4x3N(qh+AWoC zvR1X+PSHYk3Y9?l9AFG*P|$`mz#Qm<*?Bgc&nV!0#x!0E@tjd;=vHhEpwCkn0@L1p z4^(WEeixZC8Ign^%w-zzN*v`l=IEjoU(~MHy}*RmQ)&1K2Sm`NA-~jy{B=NTOAVC| z3B&Y&Hk+w5LwFB)GC897)}6daV1lsSX1UZ^{O%}_wIECQx=S_GbqBLEW#@p=L{KiK z9I-3V{DsOWAVfy>fMsj7ew-k6;RHwdS@ApHXGk!w40+>urlo)#Hd5Odxau@21-YTp6mR1ULq$^jMDEf$M;1nYhQUpia zp!FUGW!oOO782X!n6i(+mP5Xo7sJuqM$kq|MQ#Z=!xwV22Vv2GFBYHzURDxl>1-vzy>FCy%&l+iBUh+QQV8Hw3Yhl=8e5Qk9w_|| zq?Q`&$))-w*6-CiO3D^7;iy^wT2YoBd1^?P&By|=mmkj%RM0>#P$FyTiK#An(dV!2 zJ=Ea#F=xZum!j1y2CuaDG|Q>WjlF7;~fP*NnPs>+ij zbBzD^{Fk4f;T0uD^;5lIRBcqKxsnU>)B}TfIw~hqsS$$4mkvO_Qx*{Qh6MZX%dUC~ zf{ukRaUPf&U_e6|@nk!?fZe0Yj`4Qy?MwX(Ha|W#Rn61d(FI5$ zOh??|lZn3HwLr-poww!+pT(p<87k{tCU3gWtw*8FTjgKksbSCQ9#2Odw&{rYgTB|x zjHHPn65~*hv~NaYn2$}PdE)ZTGm?Lg#a@ux0X+luWJaUG-6CfBhh_FTxN6pwievP<|U)K z(&p%ApKPd9Dh6amvC*~>RRI%z=O)Uj7C3T)9q_m~^j^POvvH^}!1+1`h7n&;7s{KQ z#+Du=^y^w3NNd);-)D;OQO1^V+l9QFZ*9X+(CdQS-Eksq6B*-$*z4jNsOV~zAS4df zy5fbN_`ZH7zh_X9Xn%ek8qNf%l-@(yIME-fdmXhq_qW@R_uGd_;BHUjJF8%H0Oo=d zR9Xw1rxmgi8%dIaO=@P@(eN`@bK_!zEYIa}=l}R+#HE|_rNRWOwL7Jab3_x1xAhX2qx5dd3%=vp& zh+=nJeL`8Q%d7cth$`1Oow5i}X}v}PI=^XLWEjOch#xhDv!J^#rxkltlBt-|I5Kqv z!l6@UbsqAs6cY$~~YYoxRAtc!|#dK4{W8Kuv|BaY~M88_8W#AJ#i8|u;!q=>e& zlN@-qtRX44qt?fRds=3aX*4UVMqOU=OG~W0OSHyoAxbL}&f9DW6>)W2qT}liXWm*O z4QdUwR#y%it)x3IF#`5@UA6kNwCaGenVOBXfToN-y#@o224(v3<0D}>6d><=5$tIE zZEYQ?A385(o0f>BMWGSbeB7=nrci@=`7M0N>Q4UB&c1V8%{s(Rl7u0mQx!+LIJx5I z=UDhQ{RCF+pFVjL+oMOBRr3)B5oi0W^Ntqza2$SmNGfA{dj(2b za7?j*!c`DP#O7H2A(z?KABhcHR8?i5njDNBLOh=IkF z1n&PmTbD^7@OtIB01^G1il48G50iA%C%w?|qTl3BE)seT7wG>Sqn~?yzWE;HOf%DuBn?wsTR&K{XHr6;&m9cwT?=;1 zT6D`8WwBE93Cnpe@gQ+BAq0TAyd`G;5|C`v85@kahj?$8vt5bssa;d13?c^Ax(n_CPOmXtF{_F(ZOVra_ z6QnKs~Ngc zhrUdJ`^dAwc&Veu*=|aqES5x?T8?%we1bOcvp+CmFR&LNh|3aRwy&|0@D!P1jnvUH4)P9qdh%xL_MiXbz}ZL04z`_> zlR3fZ>ia61-SDTMsM9Cicd4%@0$?FYH{cOm$(@F#Q<324r7d!&^3ODZ!4~3MhLAXSW}Rr*U~q z9FbB98{Hed0e+VPGpW27E8hHBhD47t^k`Kfqg2TKNf@^a=yXlFex0##JK21KirpdaWyGt8-)NiP4>sCCLYrw^nIxP|?#4$O3Q)4}LIQpf12vvgO~Z2Jw} z=pg$2z0@avHM6H>y<^tYoNt|rp}Ucjuv|$mV3*ktIBYw5?)3Ku*8D?u2(FUH z1znigp@}i3UC_ea3s4`ioIe=GmnMqKVh%KHp-5KyVuA-g)q^`t-P56SW9Fc^VSFd#gT_8tobHgqi0?fpj2D&B!_bL6F(>MH*==KsV=(31iDW4yI4=sb+<_%P}4XlmIsal;34+1ZB% z{AA@w#n?dy<)RU%fe{@R49&b^3gW_`<*Z9eGV@=udwAPXsZ?r1oZ3|9>oggfS!x74 zlr6w?9qhsG_T+j@s5yPLefyBFYugwmQ|rzkr=-N*bg{IXt|slKUsl@v$s}4JqyluE z`H1oe7FN!u)mCUoz0|2g)T*B=fo5%ul1pNi*{I)jedkfT1O>i)@(HCZ7M!4 zYs$REc!brRCw@P;TV)}+6Y>n^YH#aDKaA6b#uUZXU~y1wUd##6fIw$#2 z28XS2wGQjqNAF75ZNvhy^OJO5sf#1^N8)m3U##G2A{88}iLu45W|Jv?9*$}(w??*- zHPBKTt?h79PDUeqnKfj_oZd3ggj~yEByE{%pF0BH`qy4SM%wE^vP*8hWBf9?4McSN ubNh4qbNh4qbNh4qbNh4qbNh4qbNh4qbNh4qbNlnh{QQ3dac)xpxB&p5tGa0b diff --git a/ROOTS b/ROOTS index 54bb305..1e107f5 100644 --- a/ROOTS +++ b/ROOTS @@ -1,2 +1 @@ -AFP-contribs examples