forked from Isabelle_DOF/Isabelle_DOF
merge
This commit is contained in:
commit
4e4d1a1aad
|
@ -0,0 +1,52 @@
|
|||
(* Author: Tobias Nipkow
|
||||
Copyright 1998 TUM
|
||||
*)
|
||||
|
||||
section "Automata based scanner"
|
||||
|
||||
theory AutoMaxChop
|
||||
imports DA MaxChop
|
||||
begin
|
||||
|
||||
primrec auto_split :: "('a,'s)da \<Rightarrow> 's \<Rightarrow> 'a list * 'a list \<Rightarrow> 'a list \<Rightarrow> 'a splitter" where
|
||||
"auto_split A q res ps [] = (if fin A q then (ps,[]) else res)" |
|
||||
"auto_split A q res ps (x#xs) =
|
||||
auto_split A (next A x q) (if fin A q then (ps,x#xs) else res) (ps@[x]) xs"
|
||||
|
||||
definition
|
||||
auto_chop :: "('a,'s)da \<Rightarrow> 'a chopper" where
|
||||
"auto_chop A = chop (\<lambda>xs. auto_split A (start A) ([],xs) [] xs)"
|
||||
|
||||
|
||||
lemma delta_snoc: "delta A (xs@[y]) q = next A y (delta A xs q)"
|
||||
by simp
|
||||
|
||||
lemma auto_split_lemma:
|
||||
"\<And>q ps res. auto_split A (delta A ps q) res ps xs =
|
||||
maxsplit (\<lambda>ys. fin A (delta A ys q)) res ps xs"
|
||||
apply (induct xs)
|
||||
apply simp
|
||||
apply (simp add: delta_snoc[symmetric] del: delta_append)
|
||||
done
|
||||
|
||||
lemma auto_split_is_maxsplit:
|
||||
"auto_split A (start A) res [] xs = maxsplit (accepts A) res [] xs"
|
||||
apply (unfold accepts_def)
|
||||
apply (subst delta_Nil[where ?s = "start A", symmetric])
|
||||
apply (subst auto_split_lemma)
|
||||
apply simp
|
||||
done
|
||||
|
||||
lemma is_maxsplitter_auto_split:
|
||||
"is_maxsplitter (accepts A) (\<lambda>xs. auto_split A (start A) ([],xs) [] xs)"
|
||||
by (simp add: auto_split_is_maxsplit is_maxsplitter_maxsplit)
|
||||
|
||||
|
||||
lemma is_maxchopper_auto_chop:
|
||||
"is_maxchopper (accepts A) (auto_chop A)"
|
||||
apply (unfold auto_chop_def)
|
||||
apply (rule is_maxchopper_chop)
|
||||
apply (rule is_maxsplitter_auto_split)
|
||||
done
|
||||
|
||||
end
|
|
@ -0,0 +1,29 @@
|
|||
(* Author: Tobias Nipkow
|
||||
Copyright 1998 TUM
|
||||
|
||||
Is there an optimal order of arguments for `next'?
|
||||
Currently we can have laws like `delta A (a#w) = delta A w o delta A a'
|
||||
Otherwise we could have `acceps A == fin A o delta A (start A)'
|
||||
and use foldl instead of foldl2.
|
||||
*)
|
||||
|
||||
section "Projection functions for automata"
|
||||
|
||||
theory AutoProj
|
||||
imports Main
|
||||
begin
|
||||
|
||||
definition start :: "'a * 'b * 'c \<Rightarrow> 'a" where "start A = fst A"
|
||||
definition "next" :: "'a * 'b * 'c \<Rightarrow> 'b" where "next A = fst(snd(A))"
|
||||
definition fin :: "'a * 'b * 'c \<Rightarrow> 'c" where "fin A = snd(snd(A))"
|
||||
|
||||
lemma [simp]: "start(q,d,f) = q"
|
||||
by(simp add:start_def)
|
||||
|
||||
lemma [simp]: "next(q,d,f) = d"
|
||||
by(simp add:next_def)
|
||||
|
||||
lemma [simp]: "fin(q,d,f) = f"
|
||||
by(simp add:fin_def)
|
||||
|
||||
end
|
|
@ -0,0 +1,17 @@
|
|||
(* Author: Tobias Nipkow
|
||||
Copyright 1998 TUM
|
||||
*)
|
||||
|
||||
section "Combining automata and regular expressions"
|
||||
|
||||
theory AutoRegExp
|
||||
imports Automata RegExp2NA RegExp2NAe
|
||||
begin
|
||||
|
||||
theorem "DA.accepts (na2da(rexp2na r)) w = (w : lang r)"
|
||||
by (simp add: NA_DA_equiv[THEN sym] accepts_rexp2na)
|
||||
|
||||
theorem "DA.accepts (nae2da(rexp2nae r)) w = (w : lang r)"
|
||||
by (simp add: NAe_DA_equiv accepts_rexp2nae)
|
||||
|
||||
end
|
|
@ -0,0 +1,55 @@
|
|||
(* Author: Tobias Nipkow
|
||||
Copyright 1998 TUM
|
||||
*)
|
||||
|
||||
section "Conversions between automata"
|
||||
|
||||
theory Automata
|
||||
imports DA NAe
|
||||
begin
|
||||
|
||||
definition
|
||||
na2da :: "('a,'s)na \<Rightarrow> ('a,'s set)da" where
|
||||
"na2da A = ({start A}, \<lambda>a Q. Union(next A a ` Q), \<lambda>Q. \<exists>q\<in>Q. fin A q)"
|
||||
|
||||
definition
|
||||
nae2da :: "('a,'s)nae \<Rightarrow> ('a,'s set)da" where
|
||||
"nae2da A = ({start A},
|
||||
\<lambda>a Q. Union(next A (Some a) ` ((eps A)\<^sup>* `` Q)),
|
||||
\<lambda>Q. \<exists>p \<in> (eps A)\<^sup>* `` Q. fin A p)"
|
||||
|
||||
(*** Equivalence of NA and DA ***)
|
||||
|
||||
lemma DA_delta_is_lift_NA_delta:
|
||||
"\<And>Q. DA.delta (na2da A) w Q = Union(NA.delta A w ` Q)"
|
||||
by (induct w)(auto simp:na2da_def)
|
||||
|
||||
lemma NA_DA_equiv:
|
||||
"NA.accepts A w = DA.accepts (na2da A) w"
|
||||
apply (simp add: DA.accepts_def NA.accepts_def DA_delta_is_lift_NA_delta)
|
||||
apply (simp add: na2da_def)
|
||||
done
|
||||
|
||||
(*** Direct equivalence of NAe and DA ***)
|
||||
|
||||
lemma espclosure_DA_delta_is_steps:
|
||||
"\<And>Q. (eps A)\<^sup>* `` (DA.delta (nae2da A) w Q) = steps A w `` Q"
|
||||
apply (induct w)
|
||||
apply(simp)
|
||||
apply (simp add: step_def nae2da_def)
|
||||
apply (blast)
|
||||
done
|
||||
|
||||
lemma NAe_DA_equiv:
|
||||
"DA.accepts (nae2da A) w = NAe.accepts A w"
|
||||
proof -
|
||||
have "\<And>Q. fin (nae2da A) Q = (\<exists>q \<in> (eps A)\<^sup>* `` Q. fin A q)"
|
||||
by(simp add:nae2da_def)
|
||||
thus ?thesis
|
||||
apply(simp add:espclosure_DA_delta_is_steps NAe.accepts_def DA.accepts_def)
|
||||
apply(simp add:nae2da_def)
|
||||
apply blast
|
||||
done
|
||||
qed
|
||||
|
||||
end
|
|
@ -0,0 +1,38 @@
|
|||
(* Author: Tobias Nipkow
|
||||
Copyright 1998 TUM
|
||||
*)
|
||||
|
||||
section "Deterministic automata"
|
||||
|
||||
theory DA
|
||||
imports AutoProj
|
||||
begin
|
||||
|
||||
type_synonym ('a,'s)da = "'s * ('a \<Rightarrow> 's \<Rightarrow> 's) * ('s \<Rightarrow> bool)"
|
||||
|
||||
definition
|
||||
foldl2 :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a list \<Rightarrow> 'b \<Rightarrow> 'b" where
|
||||
"foldl2 f xs a = foldl (\<lambda>a b. f b a) a xs"
|
||||
|
||||
definition
|
||||
delta :: "('a,'s)da \<Rightarrow> 'a list \<Rightarrow> 's \<Rightarrow> 's" where
|
||||
"delta A = foldl2 (next A)"
|
||||
|
||||
definition
|
||||
accepts :: "('a,'s)da \<Rightarrow> 'a list \<Rightarrow> bool" where
|
||||
"accepts A = (\<lambda>w. fin A (delta A w (start A)))"
|
||||
|
||||
lemma [simp]: "foldl2 f [] a = a \<and> foldl2 f (x#xs) a = foldl2 f xs (f x a)"
|
||||
by(simp add:foldl2_def)
|
||||
|
||||
lemma delta_Nil[simp]: "delta A [] s = s"
|
||||
by(simp add:delta_def)
|
||||
|
||||
lemma delta_Cons[simp]: "delta A (a#w) s = delta A w (next A a s)"
|
||||
by(simp add:delta_def)
|
||||
|
||||
lemma delta_append[simp]:
|
||||
"\<And>q ys. delta A (xs@ys) q = delta A ys (delta A xs q)"
|
||||
by(induct xs) simp_all
|
||||
|
||||
end
|
|
@ -0,0 +1,20 @@
|
|||
(* Author: Lukas Bulwahn, TUM 2011 *)
|
||||
|
||||
section \<open>Executing Automata and membership of Regular Expressions\<close>
|
||||
|
||||
theory Execute
|
||||
imports AutoRegExp
|
||||
begin
|
||||
|
||||
subsection \<open>Example\<close>
|
||||
|
||||
definition example_expression
|
||||
where
|
||||
"example_expression = (let r0 = Atom (0::nat); r1 = Atom (1::nat)
|
||||
in Times (Star (Plus (Times r1 r1) r0)) (Star (Plus (Times r0 r0) r1)))"
|
||||
|
||||
value "NA.accepts (rexp2na example_expression) [0,1,1,0,0,1]"
|
||||
|
||||
value "DA.accepts (na2da (rexp2na example_expression)) [0,1,1,0,0,1]"
|
||||
|
||||
end
|
|
@ -0,0 +1,5 @@
|
|||
theory Functional_Automata
|
||||
imports AutoRegExp AutoMaxChop RegSet_of_nat_DA Execute
|
||||
begin
|
||||
|
||||
end
|
|
@ -0,0 +1,120 @@
|
|||
(* Author: Tobias Nipkow
|
||||
Copyright 1998 TUM
|
||||
*)
|
||||
|
||||
section "Generic scanner"
|
||||
|
||||
theory MaxChop
|
||||
imports MaxPrefix
|
||||
begin
|
||||
|
||||
type_synonym 'a chopper = "'a list \<Rightarrow> 'a list list * 'a list"
|
||||
|
||||
definition
|
||||
is_maxchopper :: "('a list \<Rightarrow> bool) \<Rightarrow> 'a chopper \<Rightarrow> bool" where
|
||||
"is_maxchopper P chopper =
|
||||
(\<forall>xs zs yss.
|
||||
(chopper(xs) = (yss,zs)) =
|
||||
(xs = concat yss @ zs \<and> (\<forall>ys \<in> set yss. ys \<noteq> []) \<and>
|
||||
(case yss of
|
||||
[] \<Rightarrow> is_maxpref P [] xs
|
||||
| us#uss \<Rightarrow> is_maxpref P us xs \<and> chopper(concat(uss)@zs) = (uss,zs))))"
|
||||
|
||||
definition
|
||||
reducing :: "'a splitter \<Rightarrow> bool" where
|
||||
"reducing splitf =
|
||||
(\<forall>xs ys zs. splitf xs = (ys,zs) \<and> ys \<noteq> [] \<longrightarrow> length zs < length xs)"
|
||||
|
||||
function chop :: "'a splitter \<Rightarrow> 'a list \<Rightarrow> 'a list list \<times> 'a list" where
|
||||
[simp del]: "chop splitf xs = (if reducing splitf
|
||||
then let pp = splitf xs
|
||||
in if fst pp = [] then ([], xs)
|
||||
else let qq = chop splitf (snd pp)
|
||||
in (fst pp # fst qq, snd qq)
|
||||
else undefined)"
|
||||
by pat_completeness auto
|
||||
|
||||
termination apply (relation "measure (length \<circ> snd)")
|
||||
apply (auto simp: reducing_def)
|
||||
apply (case_tac "splitf xs")
|
||||
apply auto
|
||||
done
|
||||
|
||||
lemma chop_rule: "reducing splitf \<Longrightarrow>
|
||||
chop splitf xs = (let (pre, post) = splitf xs
|
||||
in if pre = [] then ([], xs)
|
||||
else let (xss, zs) = chop splitf post
|
||||
in (pre # xss,zs))"
|
||||
apply (simp add: chop.simps)
|
||||
apply (simp add: Let_def split: prod.split)
|
||||
done
|
||||
|
||||
lemma reducing_maxsplit: "reducing(\<lambda>qs. maxsplit P ([],qs) [] qs)"
|
||||
by (simp add: reducing_def maxsplit_eq)
|
||||
|
||||
lemma is_maxsplitter_reducing:
|
||||
"is_maxsplitter P splitf \<Longrightarrow> reducing splitf"
|
||||
by(simp add:is_maxsplitter_def reducing_def)
|
||||
|
||||
lemma chop_concat[rule_format]: "is_maxsplitter P splitf \<Longrightarrow>
|
||||
(\<forall>yss zs. chop splitf xs = (yss,zs) \<longrightarrow> xs = concat yss @ zs)"
|
||||
apply (induct xs rule:length_induct)
|
||||
apply (simp (no_asm_simp) split del: if_split
|
||||
add: chop_rule[OF is_maxsplitter_reducing])
|
||||
apply (simp add: Let_def is_maxsplitter_def split: prod.split)
|
||||
done
|
||||
|
||||
lemma chop_nonempty: "is_maxsplitter P splitf \<Longrightarrow>
|
||||
\<forall>yss zs. chop splitf xs = (yss,zs) \<longrightarrow> (\<forall>ys \<in> set yss. ys \<noteq> [])"
|
||||
apply (induct xs rule:length_induct)
|
||||
apply (simp (no_asm_simp) add: chop_rule is_maxsplitter_reducing)
|
||||
apply (simp add: Let_def is_maxsplitter_def split: prod.split)
|
||||
apply (intro allI impI)
|
||||
apply (rule ballI)
|
||||
apply (erule exE)
|
||||
apply (erule allE)
|
||||
apply auto
|
||||
done
|
||||
|
||||
lemma is_maxchopper_chop:
|
||||
assumes prem: "is_maxsplitter P splitf" shows "is_maxchopper P (chop splitf)"
|
||||
apply(unfold is_maxchopper_def)
|
||||
apply clarify
|
||||
apply (rule iffI)
|
||||
apply (rule conjI)
|
||||
apply (erule chop_concat[OF prem])
|
||||
apply (rule conjI)
|
||||
apply (erule prem[THEN chop_nonempty[THEN spec, THEN spec, THEN mp]])
|
||||
apply (erule rev_mp)
|
||||
apply (subst prem[THEN is_maxsplitter_reducing[THEN chop_rule]])
|
||||
apply (simp add: Let_def prem[simplified is_maxsplitter_def]
|
||||
split: prod.split)
|
||||
apply clarify
|
||||
apply (rule conjI)
|
||||
apply (clarify)
|
||||
apply (clarify)
|
||||
apply simp
|
||||
apply (frule chop_concat[OF prem])
|
||||
apply (clarify)
|
||||
apply (subst prem[THEN is_maxsplitter_reducing, THEN chop_rule])
|
||||
apply (simp add: Let_def prem[simplified is_maxsplitter_def]
|
||||
split: prod.split)
|
||||
apply (clarify)
|
||||
apply (rename_tac xs1 ys1 xss1 ys)
|
||||
apply (simp split: list.split_asm)
|
||||
apply (simp add: is_maxpref_def)
|
||||
apply (blast intro: prefix_append[THEN iffD2])
|
||||
apply (rule conjI)
|
||||
apply (clarify)
|
||||
apply (simp (no_asm_use) add: is_maxpref_def)
|
||||
apply (blast intro: prefix_append[THEN iffD2])
|
||||
apply (clarify)
|
||||
apply (rename_tac us uss)
|
||||
apply (subgoal_tac "xs1=us")
|
||||
apply simp
|
||||
apply simp
|
||||
apply (simp (no_asm_use) add: is_maxpref_def)
|
||||
apply (blast intro: prefix_append[THEN iffD2] prefix_order.antisym)
|
||||
done
|
||||
|
||||
end
|
|
@ -0,0 +1,92 @@
|
|||
(* Author: Tobias Nipkow
|
||||
Copyright 1998 TUM
|
||||
*)
|
||||
|
||||
section "Maximal prefix"
|
||||
|
||||
theory MaxPrefix
|
||||
imports "HOL-Library.Sublist"
|
||||
begin
|
||||
|
||||
definition
|
||||
is_maxpref :: "('a list \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> bool" where
|
||||
"is_maxpref P xs ys =
|
||||
(prefix xs ys \<and> (xs=[] \<or> P xs) \<and> (\<forall>zs. prefix zs ys \<and> P zs \<longrightarrow> prefix zs xs))"
|
||||
|
||||
type_synonym 'a splitter = "'a list \<Rightarrow> 'a list * 'a list"
|
||||
|
||||
definition
|
||||
is_maxsplitter :: "('a list \<Rightarrow> bool) \<Rightarrow> 'a splitter \<Rightarrow> bool" where
|
||||
"is_maxsplitter P f =
|
||||
(\<forall>xs ps qs. f xs = (ps,qs) = (xs=ps@qs \<and> is_maxpref P ps xs))"
|
||||
|
||||
fun maxsplit :: "('a list \<Rightarrow> bool) \<Rightarrow> 'a list * 'a list \<Rightarrow> 'a list \<Rightarrow> 'a splitter" where
|
||||
"maxsplit P res ps [] = (if P ps then (ps,[]) else res)" |
|
||||
"maxsplit P res ps (q#qs) = maxsplit P (if P ps then (ps,q#qs) else res)
|
||||
(ps@[q]) qs"
|
||||
|
||||
declare if_split[split del]
|
||||
|
||||
lemma maxsplit_lemma: "(maxsplit P res ps qs = (xs,ys)) =
|
||||
(if \<exists>us. prefix us qs \<and> P(ps@us) then xs@ys=ps@qs \<and> is_maxpref P xs (ps@qs)
|
||||
else (xs,ys)=res)"
|
||||
proof (induction P res ps qs rule: maxsplit.induct)
|
||||
case 1
|
||||
thus ?case by (auto simp: is_maxpref_def split: if_splits)
|
||||
next
|
||||
case (2 P res ps q qs)
|
||||
show ?case
|
||||
proof (cases "\<exists>us. prefix us qs \<and> P ((ps @ [q]) @ us)")
|
||||
case True
|
||||
note ex1 = this
|
||||
then guess us by (elim exE conjE) note us = this
|
||||
hence ex2: "\<exists>us. prefix us (q # qs) \<and> P (ps @ us)"
|
||||
by (intro exI[of _ "q#us"]) auto
|
||||
with ex1 and 2 show ?thesis by simp
|
||||
next
|
||||
case False
|
||||
note ex1 = this
|
||||
show ?thesis
|
||||
proof (cases "\<exists>us. prefix us (q#qs) \<and> P (ps @ us)")
|
||||
case False
|
||||
from 2 show ?thesis
|
||||
by (simp only: ex1 False) (insert ex1 False, auto simp: prefix_Cons)
|
||||
next
|
||||
case True
|
||||
note ex2 = this
|
||||
show ?thesis
|
||||
proof (cases "P ps")
|
||||
case True
|
||||
with 2 have "(maxsplit P (ps, q # qs) (ps @ [q]) qs = (xs, ys)) \<longleftrightarrow> (xs = ps \<and> ys = q # qs)"
|
||||
by (simp only: ex1 ex2) simp_all
|
||||
also have "\<dots> \<longleftrightarrow> (xs @ ys = ps @ q # qs \<and> is_maxpref P xs (ps @ q # qs))"
|
||||
using ex1 True
|
||||
by (auto simp: is_maxpref_def prefix_append prefix_Cons append_eq_append_conv2)
|
||||
finally show ?thesis using True by (simp only: ex1 ex2) simp_all
|
||||
next
|
||||
case False
|
||||
with 2 have "(maxsplit P res (ps @ [q]) qs = (xs, ys)) \<longleftrightarrow> ((xs, ys) = res)"
|
||||
by (simp only: ex1 ex2) simp
|
||||
also have "\<dots> \<longleftrightarrow> (xs @ ys = ps @ q # qs \<and> is_maxpref P xs (ps @ q # qs))"
|
||||
using ex1 ex2 False
|
||||
by (auto simp: append_eq_append_conv2 is_maxpref_def prefix_Cons)
|
||||
finally show ?thesis
|
||||
using False by (simp only: ex1 ex2) simp
|
||||
qed
|
||||
qed
|
||||
qed
|
||||
qed
|
||||
|
||||
declare if_split[split]
|
||||
|
||||
lemma is_maxpref_Nil[simp]:
|
||||
"\<not>(\<exists>us. prefix us xs \<and> P us) \<Longrightarrow> is_maxpref P ps xs = (ps = [])"
|
||||
by (auto simp: is_maxpref_def)
|
||||
|
||||
lemma is_maxsplitter_maxsplit:
|
||||
"is_maxsplitter P (\<lambda>xs. maxsplit P ([],xs) [] xs)"
|
||||
by (auto simp: maxsplit_lemma is_maxsplitter_def)
|
||||
|
||||
lemmas maxsplit_eq = is_maxsplitter_maxsplit[simplified is_maxsplitter_def]
|
||||
|
||||
end
|
|
@ -0,0 +1,50 @@
|
|||
(* Author: Tobias Nipkow
|
||||
Copyright 1998 TUM
|
||||
*)
|
||||
|
||||
section "Nondeterministic automata"
|
||||
|
||||
theory NA
|
||||
imports AutoProj
|
||||
begin
|
||||
|
||||
type_synonym ('a,'s) na = "'s * ('a \<Rightarrow> 's \<Rightarrow> 's set) * ('s \<Rightarrow> bool)"
|
||||
|
||||
primrec delta :: "('a,'s)na \<Rightarrow> 'a list \<Rightarrow> 's \<Rightarrow> 's set" where
|
||||
"delta A [] p = {p}" |
|
||||
"delta A (a#w) p = Union(delta A w ` next A a p)"
|
||||
|
||||
definition
|
||||
accepts :: "('a,'s)na \<Rightarrow> 'a list \<Rightarrow> bool" where
|
||||
"accepts A w = (\<exists>q \<in> delta A w (start A). fin A q)"
|
||||
|
||||
definition
|
||||
step :: "('a,'s)na \<Rightarrow> 'a \<Rightarrow> ('s * 's)set" where
|
||||
"step A a = {(p,q) . q : next A a p}"
|
||||
|
||||
primrec steps :: "('a,'s)na \<Rightarrow> 'a list \<Rightarrow> ('s * 's)set" where
|
||||
"steps A [] = Id" |
|
||||
"steps A (a#w) = step A a O steps A w"
|
||||
|
||||
lemma steps_append[simp]:
|
||||
"steps A (v@w) = steps A v O steps A w"
|
||||
by(induct v, simp_all add:O_assoc)
|
||||
|
||||
lemma in_steps_append[iff]:
|
||||
"(p,r) : steps A (v@w) = ((p,r) : (steps A v O steps A w))"
|
||||
apply(rule steps_append[THEN equalityE])
|
||||
apply blast
|
||||
done
|
||||
|
||||
lemma delta_conv_steps: "\<And>p. delta A w p = {q. (p,q) : steps A w}"
|
||||
by(induct w)(auto simp:step_def)
|
||||
|
||||
lemma accepts_conv_steps:
|
||||
"accepts A w = (\<exists>q. (start A,q) \<in> steps A w \<and> fin A q)"
|
||||
by(simp add: delta_conv_steps accepts_def)
|
||||
|
||||
abbreviation
|
||||
Cons_syn :: "'a \<Rightarrow> 'a list set \<Rightarrow> 'a list set" (infixr "##" 65) where
|
||||
"x ## S \<equiv> Cons x ` S"
|
||||
|
||||
end
|
|
@ -0,0 +1,72 @@
|
|||
(* Author: Tobias Nipkow
|
||||
Copyright 1998 TUM
|
||||
*)
|
||||
|
||||
section "Nondeterministic automata with epsilon transitions"
|
||||
|
||||
theory NAe
|
||||
imports NA
|
||||
begin
|
||||
|
||||
type_synonym ('a,'s)nae = "('a option,'s)na"
|
||||
|
||||
abbreviation
|
||||
eps :: "('a,'s)nae \<Rightarrow> ('s * 's)set" where
|
||||
"eps A \<equiv> step A None"
|
||||
|
||||
primrec steps :: "('a,'s)nae \<Rightarrow> 'a list \<Rightarrow> ('s * 's)set" where
|
||||
"steps A [] = (eps A)\<^sup>*" |
|
||||
"steps A (a#w) = (eps A)\<^sup>* O step A (Some a) O steps A w"
|
||||
|
||||
definition
|
||||
accepts :: "('a,'s)nae \<Rightarrow> 'a list \<Rightarrow> bool" where
|
||||
"accepts A w = (\<exists>q. (start A,q) \<in> steps A w \<and> fin A q)"
|
||||
|
||||
(* not really used:
|
||||
consts delta :: "('a,'s)nae \<Rightarrow> 'a list \<Rightarrow> 's \<Rightarrow> 's set"
|
||||
primrec
|
||||
"delta A [] s = (eps A)\<^sup>* `` {s}"
|
||||
"delta A (a#w) s = lift(delta A w) (lift(next A (Some a)) ((eps A)\<^sup>* `` {s}))"
|
||||
*)
|
||||
|
||||
lemma steps_epsclosure[simp]: "(eps A)\<^sup>* O steps A w = steps A w"
|
||||
by (cases w) (simp_all add: O_assoc[symmetric])
|
||||
|
||||
lemma in_steps_epsclosure:
|
||||
"[| (p,q) : (eps A)\<^sup>*; (q,r) : steps A w |] ==> (p,r) : steps A w"
|
||||
apply(rule steps_epsclosure[THEN equalityE])
|
||||
apply blast
|
||||
done
|
||||
|
||||
lemma epsclosure_steps: "steps A w O (eps A)\<^sup>* = steps A w"
|
||||
apply(induct w)
|
||||
apply simp
|
||||
apply(simp add:O_assoc)
|
||||
done
|
||||
|
||||
lemma in_epsclosure_steps:
|
||||
"[| (p,q) : steps A w; (q,r) : (eps A)\<^sup>* |] ==> (p,r) : steps A w"
|
||||
apply(rule epsclosure_steps[THEN equalityE])
|
||||
apply blast
|
||||
done
|
||||
|
||||
lemma steps_append[simp]: "steps A (v@w) = steps A v O steps A w"
|
||||
by(induct v)(simp_all add:O_assoc[symmetric])
|
||||
|
||||
lemma in_steps_append[iff]:
|
||||
"(p,r) : steps A (v@w) = ((p,r) : (steps A v O steps A w))"
|
||||
apply(rule steps_append[THEN equalityE])
|
||||
apply blast
|
||||
done
|
||||
|
||||
(* Equivalence of steps and delta
|
||||
* Use "(\<exists>x \<in> f ` A. P x) = (\<exists>a\<in>A. P(f x))" ?? *
|
||||
Goal "\<forall>p. (p,q) : steps A w = (q : delta A w p)";
|
||||
by (induct_tac "w" 1);
|
||||
by (Simp_tac 1);
|
||||
by (asm_simp_tac (simpset() addsimps [comp_def,step_def]) 1);
|
||||
by (Blast_tac 1);
|
||||
qed_spec_mp "steps_equiv_delta";
|
||||
*)
|
||||
|
||||
end
|
|
@ -0,0 +1,11 @@
|
|||
chapter AFP
|
||||
|
||||
session "Functional-Automata" (AFP) = "HOL-Library" +
|
||||
options [timeout = 600]
|
||||
sessions
|
||||
"Regular-Sets"
|
||||
theories
|
||||
Functional_Automata
|
||||
document_files
|
||||
"root.bib"
|
||||
"root.tex"
|
|
@ -0,0 +1,442 @@
|
|||
(* Author: Tobias Nipkow
|
||||
Copyright 1998 TUM
|
||||
*)
|
||||
|
||||
section "From regular expressions directly to nondeterministic automata"
|
||||
|
||||
theory RegExp2NA
|
||||
imports "Regular-Sets.Regular_Exp" NA
|
||||
begin
|
||||
|
||||
type_synonym 'a bitsNA = "('a,bool list)na"
|
||||
|
||||
definition
|
||||
"atom" :: "'a \<Rightarrow> 'a bitsNA" where
|
||||
"atom a = ([True],
|
||||
\<lambda>b s. if s=[True] \<and> b=a then {[False]} else {},
|
||||
\<lambda>s. s=[False])"
|
||||
|
||||
definition
|
||||
or :: "'a bitsNA \<Rightarrow> 'a bitsNA \<Rightarrow> 'a bitsNA" where
|
||||
"or = (\<lambda>(ql,dl,fl)(qr,dr,fr).
|
||||
([],
|
||||
\<lambda>a s. case s of
|
||||
[] \<Rightarrow> (True ## dl a ql) \<union> (False ## dr a qr)
|
||||
| left#s \<Rightarrow> if left then True ## dl a s
|
||||
else False ## dr a s,
|
||||
\<lambda>s. case s of [] \<Rightarrow> (fl ql | fr qr)
|
||||
| left#s \<Rightarrow> if left then fl s else fr s))"
|
||||
|
||||
definition
|
||||
conc :: "'a bitsNA \<Rightarrow> 'a bitsNA \<Rightarrow> 'a bitsNA" where
|
||||
"conc = (\<lambda>(ql,dl,fl)(qr,dr,fr).
|
||||
(True#ql,
|
||||
\<lambda>a s. case s of
|
||||
[] \<Rightarrow> {}
|
||||
| left#s \<Rightarrow> if left then (True ## dl a s) \<union>
|
||||
(if fl s then False ## dr a qr else {})
|
||||
else False ## dr a s,
|
||||
\<lambda>s. case s of [] \<Rightarrow> False | left#s \<Rightarrow> left \<and> fl s \<and> fr qr | \<not>left \<and> fr s))"
|
||||
|
||||
definition
|
||||
epsilon :: "'a bitsNA" where
|
||||
"epsilon = ([],\<lambda>a s. {}, \<lambda>s. s=[])"
|
||||
|
||||
definition
|
||||
plus :: "'a bitsNA \<Rightarrow> 'a bitsNA" where
|
||||
"plus = (\<lambda>(q,d,f). (q, \<lambda>a s. d a s \<union> (if f s then d a q else {}), f))"
|
||||
|
||||
definition
|
||||
star :: "'a bitsNA \<Rightarrow> 'a bitsNA" where
|
||||
"star A = or epsilon (plus A)"
|
||||
|
||||
primrec rexp2na :: "'a rexp \<Rightarrow> 'a bitsNA" where
|
||||
"rexp2na Zero = ([], \<lambda>a s. {}, \<lambda>s. False)" |
|
||||
"rexp2na One = epsilon" |
|
||||
"rexp2na(Atom a) = atom a" |
|
||||
"rexp2na(Plus r s) = or (rexp2na r) (rexp2na s)" |
|
||||
"rexp2na(Times r s) = conc (rexp2na r) (rexp2na s)" |
|
||||
"rexp2na(Star r) = star (rexp2na r)"
|
||||
|
||||
declare split_paired_all[simp]
|
||||
|
||||
(******************************************************)
|
||||
(* atom *)
|
||||
(******************************************************)
|
||||
|
||||
lemma fin_atom: "(fin (atom a) q) = (q = [False])"
|
||||
by(simp add:atom_def)
|
||||
|
||||
lemma start_atom: "start (atom a) = [True]"
|
||||
by(simp add:atom_def)
|
||||
|
||||
lemma in_step_atom_Some[simp]:
|
||||
"(p,q) : step (atom a) b = (p=[True] \<and> q=[False] \<and> b=a)"
|
||||
by (simp add: atom_def step_def)
|
||||
|
||||
lemma False_False_in_steps_atom:
|
||||
"([False],[False]) : steps (atom a) w = (w = [])"
|
||||
apply (induct "w")
|
||||
apply simp
|
||||
apply (simp add: relcomp_unfold)
|
||||
done
|
||||
|
||||
lemma start_fin_in_steps_atom:
|
||||
"(start (atom a), [False]) : steps (atom a) w = (w = [a])"
|
||||
apply (induct "w")
|
||||
apply (simp add: start_atom)
|
||||
apply (simp add: False_False_in_steps_atom relcomp_unfold start_atom)
|
||||
done
|
||||
|
||||
lemma accepts_atom:
|
||||
"accepts (atom a) w = (w = [a])"
|
||||
by (simp add: accepts_conv_steps start_fin_in_steps_atom fin_atom)
|
||||
|
||||
(******************************************************)
|
||||
(* or *)
|
||||
(******************************************************)
|
||||
|
||||
(***** lift True/False over fin *****)
|
||||
|
||||
lemma fin_or_True[iff]:
|
||||
"\<And>L R. fin (or L R) (True#p) = fin L p"
|
||||
by(simp add:or_def)
|
||||
|
||||
lemma fin_or_False[iff]:
|
||||
"\<And>L R. fin (or L R) (False#p) = fin R p"
|
||||
by(simp add:or_def)
|
||||
|
||||
(***** lift True/False over step *****)
|
||||
|
||||
lemma True_in_step_or[iff]:
|
||||
"\<And>L R. (True#p,q) : step (or L R) a = (\<exists>r. q = True#r \<and> (p,r) \<in> step L a)"
|
||||
apply (simp add:or_def step_def)
|
||||
apply blast
|
||||
done
|
||||
|
||||
lemma False_in_step_or[iff]:
|
||||
"\<And>L R. (False#p,q) : step (or L R) a = (\<exists>r. q = False#r \<and> (p,r) \<in> step R a)"
|
||||
apply (simp add:or_def step_def)
|
||||
apply blast
|
||||
done
|
||||
|
||||
|
||||
(***** lift True/False over steps *****)
|
||||
|
||||
lemma lift_True_over_steps_or[iff]:
|
||||
"\<And>p. (True#p,q)\<in>steps (or L R) w = (\<exists>r. q = True # r \<and> (p,r) \<in> steps L w)"
|
||||
apply (induct "w")
|
||||
apply force
|
||||
apply force
|
||||
done
|
||||
|
||||
lemma lift_False_over_steps_or[iff]:
|
||||
"\<And>p. (False#p,q)\<in>steps (or L R) w = (\<exists>r. q = False#r \<and> (p,r)\<in>steps R w)"
|
||||
apply (induct "w")
|
||||
apply force
|
||||
apply force
|
||||
done
|
||||
|
||||
(** From the start **)
|
||||
|
||||
lemma start_step_or[iff]:
|
||||
"\<And>L R. (start(or L R),q) : step(or L R) a =
|
||||
(\<exists>p. (q = True#p \<and> (start L,p) : step L a) |
|
||||
(q = False#p \<and> (start R,p) : step R a))"
|
||||
apply (simp add:or_def step_def)
|
||||
apply blast
|
||||
done
|
||||
|
||||
lemma steps_or:
|
||||
"(start(or L R), q) : steps (or L R) w =
|
||||
( (w = [] \<and> q = start(or L R)) |
|
||||
(w \<noteq> [] \<and> (\<exists>p. q = True # p \<and> (start L,p) : steps L w |
|
||||
q = False # p \<and> (start R,p) : steps R w)))"
|
||||
apply (case_tac "w")
|
||||
apply (simp)
|
||||
apply blast
|
||||
apply (simp)
|
||||
apply blast
|
||||
done
|
||||
|
||||
lemma fin_start_or[iff]:
|
||||
"\<And>L R. fin (or L R) (start(or L R)) = (fin L (start L) | fin R (start R))"
|
||||
by (simp add:or_def)
|
||||
|
||||
lemma accepts_or[iff]:
|
||||
"accepts (or L R) w = (accepts L w | accepts R w)"
|
||||
apply (simp add: accepts_conv_steps steps_or)
|
||||
(* get rid of case_tac: *)
|
||||
apply (case_tac "w = []")
|
||||
apply auto
|
||||
done
|
||||
|
||||
(******************************************************)
|
||||
(* conc *)
|
||||
(******************************************************)
|
||||
|
||||
(** True/False in fin **)
|
||||
|
||||
lemma fin_conc_True[iff]:
|
||||
"\<And>L R. fin (conc L R) (True#p) = (fin L p \<and> fin R (start R))"
|
||||
by(simp add:conc_def)
|
||||
|
||||
lemma fin_conc_False[iff]:
|
||||
"\<And>L R. fin (conc L R) (False#p) = fin R p"
|
||||
by(simp add:conc_def)
|
||||
|
||||
|
||||
(** True/False in step **)
|
||||
|
||||
lemma True_step_conc[iff]:
|
||||
"\<And>L R. (True#p,q) : step (conc L R) a =
|
||||
((\<exists>r. q=True#r \<and> (p,r): step L a) |
|
||||
(fin L p \<and> (\<exists>r. q=False#r \<and> (start R,r) : step R a)))"
|
||||
apply (simp add:conc_def step_def)
|
||||
apply blast
|
||||
done
|
||||
|
||||
lemma False_step_conc[iff]:
|
||||
"\<And>L R. (False#p,q) : step (conc L R) a =
|
||||
(\<exists>r. q = False#r \<and> (p,r) : step R a)"
|
||||
apply (simp add:conc_def step_def)
|
||||
apply blast
|
||||
done
|
||||
|
||||
(** False in steps **)
|
||||
|
||||
lemma False_steps_conc[iff]:
|
||||
"\<And>p. (False#p,q): steps (conc L R) w = (\<exists>r. q=False#r \<and> (p,r): steps R w)"
|
||||
apply (induct "w")
|
||||
apply fastforce
|
||||
apply force
|
||||
done
|
||||
|
||||
(** True in steps **)
|
||||
|
||||
lemma True_True_steps_concI:
|
||||
"\<And>L R p. (p,q) : steps L w \<Longrightarrow> (True#p,True#q) : steps (conc L R) w"
|
||||
apply (induct "w")
|
||||
apply simp
|
||||
apply simp
|
||||
apply fast
|
||||
done
|
||||
|
||||
lemma True_False_step_conc[iff]:
|
||||
"\<And>L R. (True#p,False#q) : step (conc L R) a =
|
||||
(fin L p \<and> (start R,q) : step R a)"
|
||||
by simp
|
||||
|
||||
lemma True_steps_concD[rule_format]:
|
||||
"\<forall>p. (True#p,q) : steps (conc L R) w \<longrightarrow>
|
||||
((\<exists>r. (p,r) : steps L w \<and> q = True#r) \<or>
|
||||
(\<exists>u a v. w = u@a#v \<and>
|
||||
(\<exists>r. (p,r) : steps L u \<and> fin L r \<and>
|
||||
(\<exists>s. (start R,s) : step R a \<and>
|
||||
(\<exists>t. (s,t) : steps R v \<and> q = False#t)))))"
|
||||
apply (induct "w")
|
||||
apply simp
|
||||
apply simp
|
||||
apply (clarify del:disjCI)
|
||||
apply (erule disjE)
|
||||
apply (clarify del:disjCI)
|
||||
apply (erule allE, erule impE, assumption)
|
||||
apply (erule disjE)
|
||||
apply blast
|
||||
apply (rule disjI2)
|
||||
apply (clarify)
|
||||
apply simp
|
||||
apply (rule_tac x = "a#u" in exI)
|
||||
apply simp
|
||||
apply blast
|
||||
apply (rule disjI2)
|
||||
apply (clarify)
|
||||
apply simp
|
||||
apply (rule_tac x = "[]" in exI)
|
||||
apply simp
|
||||
apply blast
|
||||
done
|
||||
|
||||
lemma True_steps_conc:
|
||||
"(True#p,q) : steps (conc L R) w =
|
||||
((\<exists>r. (p,r) : steps L w \<and> q = True#r) \<or>
|
||||
(\<exists>u a v. w = u@a#v \<and>
|
||||
(\<exists>r. (p,r) : steps L u \<and> fin L r \<and>
|
||||
(\<exists>s. (start R,s) : step R a \<and>
|
||||
(\<exists>t. (s,t) : steps R v \<and> q = False#t)))))"
|
||||
by(force dest!: True_steps_concD intro!: True_True_steps_concI)
|
||||
|
||||
(** starting from the start **)
|
||||
|
||||
lemma start_conc:
|
||||
"\<And>L R. start(conc L R) = True#start L"
|
||||
by (simp add:conc_def)
|
||||
|
||||
lemma final_conc:
|
||||
"\<And>L R. fin(conc L R) p = ((fin R (start R) \<and> (\<exists>s. p = True#s \<and> fin L s)) \<or>
|
||||
(\<exists>s. p = False#s \<and> fin R s))"
|
||||
apply (simp add:conc_def split: list.split)
|
||||
apply blast
|
||||
done
|
||||
|
||||
lemma accepts_conc:
|
||||
"accepts (conc L R) w = (\<exists>u v. w = u@v \<and> accepts L u \<and> accepts R v)"
|
||||
apply (simp add: accepts_conv_steps True_steps_conc final_conc start_conc)
|
||||
apply (rule iffI)
|
||||
apply (clarify)
|
||||
apply (erule disjE)
|
||||
apply (clarify)
|
||||
apply (erule disjE)
|
||||
apply (rule_tac x = "w" in exI)
|
||||
apply simp
|
||||
apply blast
|
||||
apply blast
|
||||
apply (erule disjE)
|
||||
apply blast
|
||||
apply (clarify)
|
||||
apply (rule_tac x = "u" in exI)
|
||||
apply simp
|
||||
apply blast
|
||||
apply (clarify)
|
||||
apply (case_tac "v")
|
||||
apply simp
|
||||
apply blast
|
||||
apply simp
|
||||
apply blast
|
||||
done
|
||||
|
||||
(******************************************************)
|
||||
(* epsilon *)
|
||||
(******************************************************)
|
||||
|
||||
lemma step_epsilon[simp]: "step epsilon a = {}"
|
||||
by(simp add:epsilon_def step_def)
|
||||
|
||||
lemma steps_epsilon: "((p,q) : steps epsilon w) = (w=[] \<and> p=q)"
|
||||
by (induct "w") auto
|
||||
|
||||
lemma accepts_epsilon[iff]: "accepts epsilon w = (w = [])"
|
||||
apply (simp add: steps_epsilon accepts_conv_steps)
|
||||
apply (simp add: epsilon_def)
|
||||
done
|
||||
|
||||
(******************************************************)
|
||||
(* plus *)
|
||||
(******************************************************)
|
||||
|
||||
lemma start_plus[simp]: "\<And>A. start (plus A) = start A"
|
||||
by(simp add:plus_def)
|
||||
|
||||
lemma fin_plus[iff]: "\<And>A. fin (plus A) = fin A"
|
||||
by(simp add:plus_def)
|
||||
|
||||
lemma step_plusI:
|
||||
"\<And>A. (p,q) : step A a \<Longrightarrow> (p,q) : step (plus A) a"
|
||||
by(simp add:plus_def step_def)
|
||||
|
||||
lemma steps_plusI: "\<And>p. (p,q) : steps A w \<Longrightarrow> (p,q) \<in> steps (plus A) w"
|
||||
apply (induct "w")
|
||||
apply simp
|
||||
apply simp
|
||||
apply (blast intro: step_plusI)
|
||||
done
|
||||
|
||||
lemma step_plus_conv[iff]:
|
||||
"\<And>A. (p,r): step (plus A) a =
|
||||
( (p,r): step A a | fin A p \<and> (start A,r) : step A a )"
|
||||
by(simp add:plus_def step_def)
|
||||
|
||||
lemma fin_steps_plusI:
|
||||
"[| (start A,q) : steps A u; u \<noteq> []; fin A p |]
|
||||
==> (p,q) : steps (plus A) u"
|
||||
apply (case_tac "u")
|
||||
apply blast
|
||||
apply simp
|
||||
apply (blast intro: steps_plusI)
|
||||
done
|
||||
|
||||
(* reverse list induction! Complicates matters for conc? *)
|
||||
lemma start_steps_plusD[rule_format]:
|
||||
"\<forall>r. (start A,r) \<in> steps (plus A) w \<longrightarrow>
|
||||
(\<exists>us v. w = concat us @ v \<and>
|
||||
(\<forall>u\<in>set us. accepts A u) \<and>
|
||||
(start A,r) \<in> steps A v)"
|
||||
apply (induct w rule: rev_induct)
|
||||
apply simp
|
||||
apply (rule_tac x = "[]" in exI)
|
||||
apply simp
|
||||
apply simp
|
||||
apply (clarify)
|
||||
apply (erule allE, erule impE, assumption)
|
||||
apply (clarify)
|
||||
apply (erule disjE)
|
||||
apply (rule_tac x = "us" in exI)
|
||||
apply (simp)
|
||||
apply blast
|
||||
apply (rule_tac x = "us@[v]" in exI)
|
||||
apply (simp add: accepts_conv_steps)
|
||||
apply blast
|
||||
done
|
||||
|
||||
lemma steps_star_cycle[rule_format]:
|
||||
"us \<noteq> [] \<longrightarrow> (\<forall>u \<in> set us. accepts A u) \<longrightarrow> accepts (plus A) (concat us)"
|
||||
apply (simp add: accepts_conv_steps)
|
||||
apply (induct us rule: rev_induct)
|
||||
apply simp
|
||||
apply (rename_tac u us)
|
||||
apply simp
|
||||
apply (clarify)
|
||||
apply (case_tac "us = []")
|
||||
apply (simp)
|
||||
apply (blast intro: steps_plusI fin_steps_plusI)
|
||||
apply (clarify)
|
||||
apply (case_tac "u = []")
|
||||
apply (simp)
|
||||
apply (blast intro: steps_plusI fin_steps_plusI)
|
||||
apply (blast intro: steps_plusI fin_steps_plusI)
|
||||
done
|
||||
|
||||
lemma accepts_plus[iff]:
|
||||
"accepts (plus A) w =
|
||||
(\<exists>us. us \<noteq> [] \<and> w = concat us \<and> (\<forall>u \<in> set us. accepts A u))"
|
||||
apply (rule iffI)
|
||||
apply (simp add: accepts_conv_steps)
|
||||
apply (clarify)
|
||||
apply (drule start_steps_plusD)
|
||||
apply (clarify)
|
||||
apply (rule_tac x = "us@[v]" in exI)
|
||||
apply (simp add: accepts_conv_steps)
|
||||
apply blast
|
||||
apply (blast intro: steps_star_cycle)
|
||||
done
|
||||
|
||||
(******************************************************)
|
||||
(* star *)
|
||||
(******************************************************)
|
||||
|
||||
lemma accepts_star:
|
||||
"accepts (star A) w = (\<exists>us. (\<forall>u \<in> set us. accepts A u) \<and> w = concat us)"
|
||||
apply(unfold star_def)
|
||||
apply (rule iffI)
|
||||
apply (clarify)
|
||||
apply (erule disjE)
|
||||
apply (rule_tac x = "[]" in exI)
|
||||
apply simp
|
||||
apply blast
|
||||
apply force
|
||||
done
|
||||
|
||||
(***** Correctness of r2n *****)
|
||||
|
||||
lemma accepts_rexp2na:
|
||||
"\<And>w. accepts (rexp2na r) w = (w : lang r)"
|
||||
apply (induct "r")
|
||||
apply (simp add: accepts_conv_steps)
|
||||
apply simp
|
||||
apply (simp add: accepts_atom)
|
||||
apply (simp)
|
||||
apply (simp add: accepts_conc Regular_Set.conc_def)
|
||||
apply (simp add: accepts_star in_star_iff_concat subset_iff Ball_def)
|
||||
done
|
||||
|
||||
end
|
|
@ -0,0 +1,641 @@
|
|||
(* Author: Tobias Nipkow
|
||||
Copyright 1998 TUM
|
||||
*)
|
||||
|
||||
section "From regular expressions to nondeterministic automata with epsilon"
|
||||
|
||||
theory RegExp2NAe
|
||||
imports "Regular-Sets.Regular_Exp" NAe
|
||||
begin
|
||||
|
||||
type_synonym 'a bitsNAe = "('a,bool list)nae"
|
||||
|
||||
definition
|
||||
epsilon :: "'a bitsNAe" where
|
||||
"epsilon = ([],\<lambda>a s. {}, \<lambda>s. s=[])"
|
||||
|
||||
definition
|
||||
"atom" :: "'a \<Rightarrow> 'a bitsNAe" where
|
||||
"atom a = ([True],
|
||||
\<lambda>b s. if s=[True] \<and> b=Some a then {[False]} else {},
|
||||
\<lambda>s. s=[False])"
|
||||
|
||||
definition
|
||||
or :: "'a bitsNAe \<Rightarrow> 'a bitsNAe \<Rightarrow> 'a bitsNAe" where
|
||||
"or = (\<lambda>(ql,dl,fl)(qr,dr,fr).
|
||||
([],
|
||||
\<lambda>a s. case s of
|
||||
[] \<Rightarrow> if a=None then {True#ql,False#qr} else {}
|
||||
| left#s \<Rightarrow> if left then True ## dl a s
|
||||
else False ## dr a s,
|
||||
\<lambda>s. case s of [] \<Rightarrow> False | left#s \<Rightarrow> if left then fl s else fr s))"
|
||||
|
||||
definition
|
||||
conc :: "'a bitsNAe \<Rightarrow> 'a bitsNAe \<Rightarrow> 'a bitsNAe" where
|
||||
"conc = (\<lambda>(ql,dl,fl)(qr,dr,fr).
|
||||
(True#ql,
|
||||
\<lambda>a s. case s of
|
||||
[] \<Rightarrow> {}
|
||||
| left#s \<Rightarrow> if left then (True ## dl a s) \<union>
|
||||
(if fl s \<and> a=None then {False#qr} else {})
|
||||
else False ## dr a s,
|
||||
\<lambda>s. case s of [] \<Rightarrow> False | left#s \<Rightarrow> \<not>left \<and> fr s))"
|
||||
|
||||
definition
|
||||
star :: "'a bitsNAe \<Rightarrow> 'a bitsNAe" where
|
||||
"star = (\<lambda>(q,d,f).
|
||||
([],
|
||||
\<lambda>a s. case s of
|
||||
[] \<Rightarrow> if a=None then {True#q} else {}
|
||||
| left#s \<Rightarrow> if left then (True ## d a s) \<union>
|
||||
(if f s \<and> a=None then {True#q} else {})
|
||||
else {},
|
||||
\<lambda>s. case s of [] \<Rightarrow> True | left#s \<Rightarrow> left \<and> f s))"
|
||||
|
||||
primrec rexp2nae :: "'a rexp \<Rightarrow> 'a bitsNAe" where
|
||||
"rexp2nae Zero = ([], \<lambda>a s. {}, \<lambda>s. False)" |
|
||||
"rexp2nae One = epsilon" |
|
||||
"rexp2nae(Atom a) = atom a" |
|
||||
"rexp2nae(Plus r s) = or (rexp2nae r) (rexp2nae s)" |
|
||||
"rexp2nae(Times r s) = conc (rexp2nae r) (rexp2nae s)" |
|
||||
"rexp2nae(Star r) = star (rexp2nae r)"
|
||||
|
||||
declare split_paired_all[simp]
|
||||
|
||||
(******************************************************)
|
||||
(* epsilon *)
|
||||
(******************************************************)
|
||||
|
||||
lemma step_epsilon[simp]: "step epsilon a = {}"
|
||||
by(simp add:epsilon_def step_def)
|
||||
|
||||
lemma steps_epsilon: "((p,q) : steps epsilon w) = (w=[] \<and> p=q)"
|
||||
by (induct "w") auto
|
||||
|
||||
lemma accepts_epsilon[simp]: "accepts epsilon w = (w = [])"
|
||||
apply (simp add: steps_epsilon accepts_def)
|
||||
apply (simp add: epsilon_def)
|
||||
done
|
||||
|
||||
(******************************************************)
|
||||
(* atom *)
|
||||
(******************************************************)
|
||||
|
||||
lemma fin_atom: "(fin (atom a) q) = (q = [False])"
|
||||
by(simp add:atom_def)
|
||||
|
||||
lemma start_atom: "start (atom a) = [True]"
|
||||
by(simp add:atom_def)
|
||||
|
||||
(* Use {x. False} = {}? *)
|
||||
|
||||
lemma eps_atom[simp]:
|
||||
"eps(atom a) = {}"
|
||||
by (simp add:atom_def step_def)
|
||||
|
||||
lemma in_step_atom_Some[simp]:
|
||||
"(p,q) : step (atom a) (Some b) = (p=[True] \<and> q=[False] \<and> b=a)"
|
||||
by (simp add:atom_def step_def)
|
||||
|
||||
lemma False_False_in_steps_atom:
|
||||
"([False],[False]) : steps (atom a) w = (w = [])"
|
||||
apply (induct "w")
|
||||
apply (simp)
|
||||
apply (simp add: relcomp_unfold)
|
||||
done
|
||||
|
||||
lemma start_fin_in_steps_atom:
|
||||
"(start (atom a), [False]) : steps (atom a) w = (w = [a])"
|
||||
apply (induct "w")
|
||||
apply (simp add: start_atom rtrancl_empty)
|
||||
apply (simp add: False_False_in_steps_atom relcomp_unfold start_atom)
|
||||
done
|
||||
|
||||
lemma accepts_atom: "accepts (atom a) w = (w = [a])"
|
||||
by (simp add: accepts_def start_fin_in_steps_atom fin_atom)
|
||||
|
||||
|
||||
(******************************************************)
|
||||
(* or *)
|
||||
(******************************************************)
|
||||
|
||||
(***** lift True/False over fin *****)
|
||||
|
||||
lemma fin_or_True[iff]:
|
||||
"\<And>L R. fin (or L R) (True#p) = fin L p"
|
||||
by(simp add:or_def)
|
||||
|
||||
lemma fin_or_False[iff]:
|
||||
"\<And>L R. fin (or L R) (False#p) = fin R p"
|
||||
by(simp add:or_def)
|
||||
|
||||
(***** lift True/False over step *****)
|
||||
|
||||
lemma True_in_step_or[iff]:
|
||||
"\<And>L R. (True#p,q) : step (or L R) a = (\<exists>r. q = True#r \<and> (p,r) : step L a)"
|
||||
apply (simp add:or_def step_def)
|
||||
apply blast
|
||||
done
|
||||
|
||||
lemma False_in_step_or[iff]:
|
||||
"\<And>L R. (False#p,q) : step (or L R) a = (\<exists>r. q = False#r \<and> (p,r) : step R a)"
|
||||
apply (simp add:or_def step_def)
|
||||
apply blast
|
||||
done
|
||||
|
||||
|
||||
(***** lift True/False over epsclosure *****)
|
||||
|
||||
lemma lemma1a:
|
||||
"(tp,tq) : (eps(or L R))\<^sup>* \<Longrightarrow>
|
||||
(\<And>p. tp = True#p \<Longrightarrow> \<exists>q. (p,q) : (eps L)\<^sup>* \<and> tq = True#q)"
|
||||
apply (induct rule:rtrancl_induct)
|
||||
apply (blast)
|
||||
apply (clarify)
|
||||
apply (simp)
|
||||
apply (blast intro: rtrancl_into_rtrancl)
|
||||
done
|
||||
|
||||
lemma lemma1b:
|
||||
"(tp,tq) : (eps(or L R))\<^sup>* \<Longrightarrow>
|
||||
(\<And>p. tp = False#p \<Longrightarrow> \<exists>q. (p,q) : (eps R)\<^sup>* \<and> tq = False#q)"
|
||||
apply (induct rule:rtrancl_induct)
|
||||
apply (blast)
|
||||
apply (clarify)
|
||||
apply (simp)
|
||||
apply (blast intro: rtrancl_into_rtrancl)
|
||||
done
|
||||
|
||||
lemma lemma2a:
|
||||
"(p,q) : (eps L)\<^sup>* \<Longrightarrow> (True#p, True#q) : (eps(or L R))\<^sup>*"
|
||||
apply (induct rule: rtrancl_induct)
|
||||
apply (blast)
|
||||
apply (blast intro: rtrancl_into_rtrancl)
|
||||
done
|
||||
|
||||
lemma lemma2b:
|
||||
"(p,q) : (eps R)\<^sup>* \<Longrightarrow> (False#p, False#q) : (eps(or L R))\<^sup>*"
|
||||
apply (induct rule: rtrancl_induct)
|
||||
apply (blast)
|
||||
apply (blast intro: rtrancl_into_rtrancl)
|
||||
done
|
||||
|
||||
lemma True_epsclosure_or[iff]:
|
||||
"(True#p,q) : (eps(or L R))\<^sup>* = (\<exists>r. q = True#r \<and> (p,r) : (eps L)\<^sup>*)"
|
||||
by (blast dest: lemma1a lemma2a)
|
||||
|
||||
lemma False_epsclosure_or[iff]:
|
||||
"(False#p,q) : (eps(or L R))\<^sup>* = (\<exists>r. q = False#r \<and> (p,r) : (eps R)\<^sup>*)"
|
||||
by (blast dest: lemma1b lemma2b)
|
||||
|
||||
(***** lift True/False over steps *****)
|
||||
|
||||
lemma lift_True_over_steps_or[iff]:
|
||||
"\<And>p. (True#p,q):steps (or L R) w = (\<exists>r. q = True # r \<and> (p,r):steps L w)"
|
||||
apply (induct "w")
|
||||
apply auto
|
||||
apply force
|
||||
done
|
||||
|
||||
lemma lift_False_over_steps_or[iff]:
|
||||
"\<And>p. (False#p,q):steps (or L R) w = (\<exists>r. q = False#r \<and> (p,r):steps R w)"
|
||||
apply (induct "w")
|
||||
apply auto
|
||||
apply (force)
|
||||
done
|
||||
|
||||
(***** Epsilon closure of start state *****)
|
||||
|
||||
lemma unfold_rtrancl2:
|
||||
"R\<^sup>* = Id \<union> (R O R\<^sup>*)"
|
||||
apply (rule set_eqI)
|
||||
apply (simp)
|
||||
apply (rule iffI)
|
||||
apply (erule rtrancl_induct)
|
||||
apply (blast)
|
||||
apply (blast intro: rtrancl_into_rtrancl)
|
||||
apply (blast intro: converse_rtrancl_into_rtrancl)
|
||||
done
|
||||
|
||||
lemma in_unfold_rtrancl2:
|
||||
"(p,q) : R\<^sup>* = (q = p | (\<exists>r. (p,r) : R \<and> (r,q) : R\<^sup>*))"
|
||||
apply (rule unfold_rtrancl2[THEN equalityE])
|
||||
apply (blast)
|
||||
done
|
||||
|
||||
lemmas [iff] = in_unfold_rtrancl2[where ?p = "start(or L R)"] for L R
|
||||
|
||||
lemma start_eps_or[iff]:
|
||||
"\<And>L R. (start(or L R),q) : eps(or L R) =
|
||||
(q = True#start L | q = False#start R)"
|
||||
by (simp add:or_def step_def)
|
||||
|
||||
lemma not_start_step_or_Some[iff]:
|
||||
"\<And>L R. (start(or L R),q) \<notin> step (or L R) (Some a)"
|
||||
by (simp add:or_def step_def)
|
||||
|
||||
lemma steps_or:
|
||||
"(start(or L R), q) : steps (or L R) w =
|
||||
( (w = [] \<and> q = start(or L R)) |
|
||||
(\<exists>p. q = True # p \<and> (start L,p) : steps L w |
|
||||
q = False # p \<and> (start R,p) : steps R w) )"
|
||||
apply (case_tac "w")
|
||||
apply (simp)
|
||||
apply (blast)
|
||||
apply (simp)
|
||||
apply (blast)
|
||||
done
|
||||
|
||||
lemma start_or_not_final[iff]:
|
||||
"\<And>L R. \<not> fin (or L R) (start(or L R))"
|
||||
by (simp add:or_def)
|
||||
|
||||
lemma accepts_or:
|
||||
"accepts (or L R) w = (accepts L w | accepts R w)"
|
||||
apply (simp add:accepts_def steps_or)
|
||||
apply auto
|
||||
done
|
||||
|
||||
|
||||
(******************************************************)
|
||||
(* conc *)
|
||||
(******************************************************)
|
||||
|
||||
(** True/False in fin **)
|
||||
|
||||
lemma in_conc_True[iff]:
|
||||
"\<And>L R. fin (conc L R) (True#p) = False"
|
||||
by (simp add:conc_def)
|
||||
|
||||
lemma fin_conc_False[iff]:
|
||||
"\<And>L R. fin (conc L R) (False#p) = fin R p"
|
||||
by (simp add:conc_def)
|
||||
|
||||
(** True/False in step **)
|
||||
|
||||
lemma True_step_conc[iff]:
|
||||
"\<And>L R. (True#p,q) : step (conc L R) a =
|
||||
((\<exists>r. q=True#r \<and> (p,r): step L a) |
|
||||
(fin L p \<and> a=None \<and> q=False#start R))"
|
||||
by (simp add:conc_def step_def) (blast)
|
||||
|
||||
lemma False_step_conc[iff]:
|
||||
"\<And>L R. (False#p,q) : step (conc L R) a =
|
||||
(\<exists>r. q = False#r \<and> (p,r) : step R a)"
|
||||
by (simp add:conc_def step_def) (blast)
|
||||
|
||||
(** False in epsclosure **)
|
||||
|
||||
lemma lemma1b':
|
||||
"(tp,tq) : (eps(conc L R))\<^sup>* \<Longrightarrow>
|
||||
(\<And>p. tp = False#p \<Longrightarrow> \<exists>q. (p,q) : (eps R)\<^sup>* \<and> tq = False#q)"
|
||||
apply (induct rule: rtrancl_induct)
|
||||
apply (blast)
|
||||
apply (blast intro: rtrancl_into_rtrancl)
|
||||
done
|
||||
|
||||
lemma lemma2b':
|
||||
"(p,q) : (eps R)\<^sup>* \<Longrightarrow> (False#p, False#q) : (eps(conc L R))\<^sup>*"
|
||||
apply (induct rule: rtrancl_induct)
|
||||
apply (blast)
|
||||
apply (blast intro: rtrancl_into_rtrancl)
|
||||
done
|
||||
|
||||
lemma False_epsclosure_conc[iff]:
|
||||
"((False # p, q) : (eps (conc L R))\<^sup>*) =
|
||||
(\<exists>r. q = False # r \<and> (p, r) : (eps R)\<^sup>*)"
|
||||
apply (rule iffI)
|
||||
apply (blast dest: lemma1b')
|
||||
apply (blast dest: lemma2b')
|
||||
done
|
||||
|
||||
(** False in steps **)
|
||||
|
||||
lemma False_steps_conc[iff]:
|
||||
"\<And>p. (False#p,q): steps (conc L R) w = (\<exists>r. q=False#r \<and> (p,r): steps R w)"
|
||||
apply (induct "w")
|
||||
apply (simp)
|
||||
apply (simp)
|
||||
apply (fast) (*MUCH faster than blast*)
|
||||
done
|
||||
|
||||
(** True in epsclosure **)
|
||||
|
||||
lemma True_True_eps_concI:
|
||||
"(p,q): (eps L)\<^sup>* \<Longrightarrow> (True#p,True#q) : (eps(conc L R))\<^sup>*"
|
||||
apply (induct rule: rtrancl_induct)
|
||||
apply (blast)
|
||||
apply (blast intro: rtrancl_into_rtrancl)
|
||||
done
|
||||
|
||||
lemma True_True_steps_concI:
|
||||
"\<And>p. (p,q) : steps L w \<Longrightarrow> (True#p,True#q) : steps (conc L R) w"
|
||||
apply (induct "w")
|
||||
apply (simp add: True_True_eps_concI)
|
||||
apply (simp)
|
||||
apply (blast intro: True_True_eps_concI)
|
||||
done
|
||||
|
||||
lemma lemma1a':
|
||||
"(tp,tq) : (eps(conc L R))\<^sup>* \<Longrightarrow>
|
||||
(\<And>p. tp = True#p \<Longrightarrow>
|
||||
(\<exists>q. tq = True#q \<and> (p,q) : (eps L)\<^sup>*) |
|
||||
(\<exists>q r. tq = False#q \<and> (p,r):(eps L)\<^sup>* \<and> fin L r \<and> (start R,q) : (eps R)\<^sup>*))"
|
||||
apply (induct rule: rtrancl_induct)
|
||||
apply (blast)
|
||||
apply (blast intro: rtrancl_into_rtrancl)
|
||||
done
|
||||
|
||||
lemma lemma2a':
|
||||
"(p, q) : (eps L)\<^sup>* \<Longrightarrow> (True#p, True#q) : (eps(conc L R))\<^sup>*"
|
||||
apply (induct rule: rtrancl_induct)
|
||||
apply (blast)
|
||||
apply (blast intro: rtrancl_into_rtrancl)
|
||||
done
|
||||
|
||||
lemma lem:
|
||||
"\<And>L R. (p,q) : step R None \<Longrightarrow> (False#p, False#q) : step (conc L R) None"
|
||||
by(simp add: conc_def step_def)
|
||||
|
||||
lemma lemma2b'':
|
||||
"(p,q) : (eps R)\<^sup>* \<Longrightarrow> (False#p, False#q) : (eps(conc L R))\<^sup>*"
|
||||
apply (induct rule: rtrancl_induct)
|
||||
apply (blast)
|
||||
apply (drule lem)
|
||||
apply (blast intro: rtrancl_into_rtrancl)
|
||||
done
|
||||
|
||||
lemma True_False_eps_concI:
|
||||
"\<And>L R. fin L p \<Longrightarrow> (True#p, False#start R) : eps(conc L R)"
|
||||
by(simp add: conc_def step_def)
|
||||
|
||||
lemma True_epsclosure_conc[iff]:
|
||||
"((True#p,q) \<in> (eps(conc L R))\<^sup>*) =
|
||||
((\<exists>r. (p,r) \<in> (eps L)\<^sup>* \<and> q = True#r) \<or>
|
||||
(\<exists>r. (p,r) \<in> (eps L)\<^sup>* \<and> fin L r \<and>
|
||||
(\<exists>s. (start R, s) \<in> (eps R)\<^sup>* \<and> q = False#s)))"
|
||||
apply (rule iffI)
|
||||
apply (blast dest: lemma1a')
|
||||
apply (erule disjE)
|
||||
apply (blast intro: lemma2a')
|
||||
apply (clarify)
|
||||
apply (rule rtrancl_trans)
|
||||
apply (erule lemma2a')
|
||||
apply (rule converse_rtrancl_into_rtrancl)
|
||||
apply (erule True_False_eps_concI)
|
||||
apply (erule lemma2b'')
|
||||
done
|
||||
|
||||
(** True in steps **)
|
||||
|
||||
lemma True_steps_concD[rule_format]:
|
||||
"\<forall>p. (True#p,q) : steps (conc L R) w \<longrightarrow>
|
||||
((\<exists>r. (p,r) : steps L w \<and> q = True#r) \<or>
|
||||
(\<exists>u v. w = u@v \<and> (\<exists>r. (p,r) \<in> steps L u \<and> fin L r \<and>
|
||||
(\<exists>s. (start R,s) \<in> steps R v \<and> q = False#s))))"
|
||||
apply (induct "w")
|
||||
apply (simp)
|
||||
apply (simp)
|
||||
apply (clarify del: disjCI)
|
||||
apply (erule disjE)
|
||||
apply (clarify del: disjCI)
|
||||
apply (erule disjE)
|
||||
apply (clarify del: disjCI)
|
||||
apply (erule allE, erule impE, assumption)
|
||||
apply (erule disjE)
|
||||
apply (blast)
|
||||
apply (rule disjI2)
|
||||
apply (clarify)
|
||||
apply (simp)
|
||||
apply (rule_tac x = "a#u" in exI)
|
||||
apply (simp)
|
||||
apply (blast)
|
||||
apply (blast)
|
||||
apply (rule disjI2)
|
||||
apply (clarify)
|
||||
apply (simp)
|
||||
apply (rule_tac x = "[]" in exI)
|
||||
apply (simp)
|
||||
apply (blast)
|
||||
done
|
||||
|
||||
lemma True_steps_conc:
|
||||
"(True#p,q) \<in> steps (conc L R) w =
|
||||
((\<exists>r. (p,r) \<in> steps L w \<and> q = True#r) |
|
||||
(\<exists>u v. w = u@v \<and> (\<exists>r. (p,r) : steps L u \<and> fin L r \<and>
|
||||
(\<exists>s. (start R,s) : steps R v \<and> q = False#s))))"
|
||||
by (blast dest: True_steps_concD
|
||||
intro: True_True_steps_concI in_steps_epsclosure)
|
||||
|
||||
(** starting from the start **)
|
||||
|
||||
lemma start_conc:
|
||||
"\<And>L R. start(conc L R) = True#start L"
|
||||
by (simp add: conc_def)
|
||||
|
||||
lemma final_conc:
|
||||
"\<And>L R. fin(conc L R) p = (\<exists>s. p = False#s \<and> fin R s)"
|
||||
by (simp add:conc_def split: list.split)
|
||||
|
||||
lemma accepts_conc:
|
||||
"accepts (conc L R) w = (\<exists>u v. w = u@v \<and> accepts L u \<and> accepts R v)"
|
||||
apply (simp add: accepts_def True_steps_conc final_conc start_conc)
|
||||
apply (blast)
|
||||
done
|
||||
|
||||
(******************************************************)
|
||||
(* star *)
|
||||
(******************************************************)
|
||||
|
||||
lemma True_in_eps_star[iff]:
|
||||
"\<And>A. (True#p,q) \<in> eps(star A) =
|
||||
( (\<exists>r. q = True#r \<and> (p,r) \<in> eps A) \<or> (fin A p \<and> q = True#start A) )"
|
||||
by (simp add:star_def step_def) (blast)
|
||||
|
||||
lemma True_True_step_starI:
|
||||
"\<And>A. (p,q) : step A a \<Longrightarrow> (True#p, True#q) : step (star A) a"
|
||||
by (simp add:star_def step_def)
|
||||
|
||||
lemma True_True_eps_starI:
|
||||
"(p,r) : (eps A)\<^sup>* \<Longrightarrow> (True#p, True#r) : (eps(star A))\<^sup>*"
|
||||
apply (induct rule: rtrancl_induct)
|
||||
apply (blast)
|
||||
apply (blast intro: True_True_step_starI rtrancl_into_rtrancl)
|
||||
done
|
||||
|
||||
lemma True_start_eps_starI:
|
||||
"\<And>A. fin A p \<Longrightarrow> (True#p,True#start A) : eps(star A)"
|
||||
by (simp add:star_def step_def)
|
||||
|
||||
lemma lem':
|
||||
"(tp,s) : (eps(star A))\<^sup>* \<Longrightarrow> (\<forall>p. tp = True#p \<longrightarrow>
|
||||
(\<exists>r. ((p,r) \<in> (eps A)\<^sup>* \<or>
|
||||
(\<exists>q. (p,q) \<in> (eps A)\<^sup>* \<and> fin A q \<and> (start A,r) : (eps A)\<^sup>*)) \<and>
|
||||
s = True#r))"
|
||||
apply (induct rule: rtrancl_induct)
|
||||
apply (simp)
|
||||
apply (clarify)
|
||||
apply (simp)
|
||||
apply (blast intro: rtrancl_into_rtrancl)
|
||||
done
|
||||
|
||||
lemma True_eps_star[iff]:
|
||||
"((True#p,s) \<in> (eps(star A))\<^sup>*) =
|
||||
(\<exists>r. ((p,r) \<in> (eps A)\<^sup>* \<or>
|
||||
(\<exists>q. (p,q) : (eps A)\<^sup>* \<and> fin A q \<and> (start A,r) : (eps A)\<^sup>*)) \<and>
|
||||
s = True#r)"
|
||||
apply (rule iffI)
|
||||
apply (drule lem')
|
||||
apply (blast)
|
||||
(* Why can't blast do the rest? *)
|
||||
apply (clarify)
|
||||
apply (erule disjE)
|
||||
apply (erule True_True_eps_starI)
|
||||
apply (clarify)
|
||||
apply (rule rtrancl_trans)
|
||||
apply (erule True_True_eps_starI)
|
||||
apply (rule rtrancl_trans)
|
||||
apply (rule r_into_rtrancl)
|
||||
apply (erule True_start_eps_starI)
|
||||
apply (erule True_True_eps_starI)
|
||||
done
|
||||
|
||||
(** True in step Some **)
|
||||
|
||||
lemma True_step_star[iff]:
|
||||
"\<And>A. (True#p,r) \<in> step (star A) (Some a) =
|
||||
(\<exists>q. (p,q) \<in> step A (Some a) \<and> r=True#q)"
|
||||
by (simp add:star_def step_def) (blast)
|
||||
|
||||
|
||||
(** True in steps **)
|
||||
|
||||
(* reverse list induction! Complicates matters for conc? *)
|
||||
lemma True_start_steps_starD[rule_format]:
|
||||
"\<forall>rr. (True#start A,rr) \<in> steps (star A) w \<longrightarrow>
|
||||
(\<exists>us v. w = concat us @ v \<and>
|
||||
(\<forall>u\<in>set us. accepts A u) \<and>
|
||||
(\<exists>r. (start A,r) \<in> steps A v \<and> rr = True#r))"
|
||||
apply (induct w rule: rev_induct)
|
||||
apply (simp)
|
||||
apply (clarify)
|
||||
apply (rule_tac x = "[]" in exI)
|
||||
apply (erule disjE)
|
||||
apply (simp)
|
||||
apply (clarify)
|
||||
apply (simp)
|
||||
apply (simp add: O_assoc[symmetric] epsclosure_steps)
|
||||
apply (clarify)
|
||||
apply (erule allE, erule impE, assumption)
|
||||
apply (clarify)
|
||||
apply (erule disjE)
|
||||
apply (rule_tac x = "us" in exI)
|
||||
apply (rule_tac x = "v@[x]" in exI)
|
||||
apply (simp add: O_assoc[symmetric] epsclosure_steps)
|
||||
apply (blast)
|
||||
apply (clarify)
|
||||
apply (rule_tac x = "us@[v@[x]]" in exI)
|
||||
apply (rule_tac x = "[]" in exI)
|
||||
apply (simp add: accepts_def)
|
||||
apply (blast)
|
||||
done
|
||||
|
||||
lemma True_True_steps_starI:
|
||||
"\<And>p. (p,q) : steps A w \<Longrightarrow> (True#p,True#q) : steps (star A) w"
|
||||
apply (induct "w")
|
||||
apply (simp)
|
||||
apply (simp)
|
||||
apply (blast intro: True_True_eps_starI True_True_step_starI)
|
||||
done
|
||||
|
||||
lemma steps_star_cycle:
|
||||
"(\<forall>u \<in> set us. accepts A u) \<Longrightarrow>
|
||||
(True#start A,True#start A) \<in> steps (star A) (concat us)"
|
||||
apply (induct "us")
|
||||
apply (simp add:accepts_def)
|
||||
apply (simp add:accepts_def)
|
||||
by(blast intro: True_True_steps_starI True_start_eps_starI in_epsclosure_steps)
|
||||
|
||||
(* Better stated directly with start(star A)? Loop in star A back to start(star A)?*)
|
||||
lemma True_start_steps_star:
|
||||
"(True#start A,rr) : steps (star A) w =
|
||||
(\<exists>us v. w = concat us @ v \<and>
|
||||
(\<forall>u\<in>set us. accepts A u) \<and>
|
||||
(\<exists>r. (start A,r) \<in> steps A v \<and> rr = True#r))"
|
||||
apply (rule iffI)
|
||||
apply (erule True_start_steps_starD)
|
||||
apply (clarify)
|
||||
apply (blast intro: steps_star_cycle True_True_steps_starI)
|
||||
done
|
||||
|
||||
(** the start state **)
|
||||
|
||||
lemma start_step_star[iff]:
|
||||
"\<And>A. (start(star A),r) : step (star A) a = (a=None \<and> r = True#start A)"
|
||||
by (simp add:star_def step_def)
|
||||
|
||||
lemmas epsclosure_start_step_star =
|
||||
in_unfold_rtrancl2[where ?p = "start (star A)"] for A
|
||||
|
||||
lemma start_steps_star:
|
||||
"(start(star A),r) : steps (star A) w =
|
||||
((w=[] \<and> r= start(star A)) | (True#start A,r) : steps (star A) w)"
|
||||
apply (rule iffI)
|
||||
apply (case_tac "w")
|
||||
apply (simp add: epsclosure_start_step_star)
|
||||
apply (simp)
|
||||
apply (clarify)
|
||||
apply (simp add: epsclosure_start_step_star)
|
||||
apply (blast)
|
||||
apply (erule disjE)
|
||||
apply (simp)
|
||||
apply (blast intro: in_steps_epsclosure)
|
||||
done
|
||||
|
||||
lemma fin_star_True[iff]: "\<And>A. fin (star A) (True#p) = fin A p"
|
||||
by (simp add:star_def)
|
||||
|
||||
lemma fin_star_start[iff]: "\<And>A. fin (star A) (start(star A))"
|
||||
by (simp add:star_def)
|
||||
|
||||
(* too complex! Simpler if loop back to start(star A)? *)
|
||||
lemma accepts_star:
|
||||
"accepts (star A) w =
|
||||
(\<exists>us. (\<forall>u \<in> set(us). accepts A u) \<and> (w = concat us))"
|
||||
apply(unfold accepts_def)
|
||||
apply (simp add: start_steps_star True_start_steps_star)
|
||||
apply (rule iffI)
|
||||
apply (clarify)
|
||||
apply (erule disjE)
|
||||
apply (clarify)
|
||||
apply (simp)
|
||||
apply (rule_tac x = "[]" in exI)
|
||||
apply (simp)
|
||||
apply (clarify)
|
||||
apply (rule_tac x = "us@[v]" in exI)
|
||||
apply (simp add: accepts_def)
|
||||
apply (blast)
|
||||
apply (clarify)
|
||||
apply (rule_tac xs = "us" in rev_exhaust)
|
||||
apply (simp)
|
||||
apply (blast)
|
||||
apply (clarify)
|
||||
apply (simp add: accepts_def)
|
||||
apply (blast)
|
||||
done
|
||||
|
||||
|
||||
(***** Correctness of r2n *****)
|
||||
|
||||
lemma accepts_rexp2nae:
|
||||
"\<And>w. accepts (rexp2nae r) w = (w : lang r)"
|
||||
apply (induct "r")
|
||||
apply (simp add: accepts_def)
|
||||
apply simp
|
||||
apply (simp add: accepts_atom)
|
||||
apply (simp add: accepts_or)
|
||||
apply (simp add: accepts_conc Regular_Set.conc_def)
|
||||
apply (simp add: accepts_star in_star_iff_concat subset_iff Ball_def)
|
||||
done
|
||||
|
||||
end
|
|
@ -0,0 +1,233 @@
|
|||
(* Author: Tobias Nipkow
|
||||
Copyright 1998 TUM
|
||||
|
||||
To generate a regular expression, the alphabet must be finite.
|
||||
regexp needs to be supplied with an 'a list for a unique order
|
||||
|
||||
add_Atom d i j r a = (if d a i = j then Union r (Atom a) else r)
|
||||
atoms d i j as = foldl (add_Atom d i j) Empty as
|
||||
|
||||
regexp as d i j 0 = (if i=j then Union (Star Empty) (atoms d i j as)
|
||||
else atoms d i j as
|
||||
*)
|
||||
|
||||
section "From deterministic automata to regular sets"
|
||||
|
||||
theory RegSet_of_nat_DA
|
||||
imports "Regular-Sets.Regular_Set" DA
|
||||
begin
|
||||
|
||||
type_synonym 'a nat_next = "'a \<Rightarrow> nat \<Rightarrow> nat"
|
||||
|
||||
abbreviation
|
||||
deltas :: "'a nat_next \<Rightarrow> 'a list \<Rightarrow> nat \<Rightarrow> nat" where
|
||||
"deltas \<equiv> foldl2"
|
||||
|
||||
primrec trace :: "'a nat_next \<Rightarrow> nat \<Rightarrow> 'a list \<Rightarrow> nat list" where
|
||||
"trace d i [] = []" |
|
||||
"trace d i (x#xs) = d x i # trace d (d x i) xs"
|
||||
|
||||
(* conversion a la Warshall *)
|
||||
|
||||
primrec regset :: "'a nat_next \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> 'a list set" where
|
||||
"regset d i j 0 = (if i=j then insert [] {[a] | a. d a i = j}
|
||||
else {[a] | a. d a i = j})" |
|
||||
"regset d i j (Suc k) =
|
||||
regset d i j k \<union>
|
||||
(regset d i k k) @@ (star(regset d k k k)) @@ (regset d k j k)"
|
||||
|
||||
definition
|
||||
regset_of_DA :: "('a,nat)da \<Rightarrow> nat \<Rightarrow> 'a list set" where
|
||||
"regset_of_DA A k = (\<Union>j\<in>{j. j<k \<and> fin A j}. regset (next A) (start A) j k)"
|
||||
|
||||
definition
|
||||
bounded :: "'a nat_next \<Rightarrow> nat \<Rightarrow> bool" where
|
||||
"bounded d k = (\<forall>n. n < k \<longrightarrow> (\<forall>x. d x n < k))"
|
||||
|
||||
declare
|
||||
in_set_butlast_appendI[simp,intro] less_SucI[simp] image_eqI[simp]
|
||||
|
||||
(* Lists *)
|
||||
|
||||
lemma butlast_empty[iff]:
|
||||
"(butlast xs = []) = (case xs of [] \<Rightarrow> True | y#ys \<Rightarrow> ys=[])"
|
||||
by (cases xs) simp_all
|
||||
|
||||
lemma in_set_butlast_concatI:
|
||||
"x:set(butlast xs) \<Longrightarrow> xs:set xss \<Longrightarrow> x:set(butlast(concat xss))"
|
||||
apply (induct "xss")
|
||||
apply simp
|
||||
apply (simp add: butlast_append del: ball_simps)
|
||||
apply (rule conjI)
|
||||
apply (clarify)
|
||||
apply (erule disjE)
|
||||
apply (blast)
|
||||
apply (subgoal_tac "xs=[]")
|
||||
apply simp
|
||||
apply (blast)
|
||||
apply (blast dest: in_set_butlastD)
|
||||
done
|
||||
|
||||
(* Regular sets *)
|
||||
|
||||
(* The main lemma:
|
||||
how to decompose a trace into a prefix, a list of loops and a suffix.
|
||||
*)
|
||||
lemma decompose[rule_format]:
|
||||
"\<forall>i. k \<in> set(trace d i xs) \<longrightarrow> (\<exists>pref mids suf.
|
||||
xs = pref @ concat mids @ suf \<and>
|
||||
deltas d pref i = k \<and> (\<forall>n\<in>set(butlast(trace d i pref)). n \<noteq> k) \<and>
|
||||
(\<forall>mid\<in>set mids. (deltas d mid k = k) \<and>
|
||||
(\<forall>n\<in>set(butlast(trace d k mid)). n \<noteq> k)) \<and>
|
||||
(\<forall>n\<in>set(butlast(trace d k suf)). n \<noteq> k))"
|
||||
apply (induct "xs")
|
||||
apply (simp)
|
||||
apply (rename_tac a as)
|
||||
apply (intro strip)
|
||||
apply (case_tac "d a i = k")
|
||||
apply (rule_tac x = "[a]" in exI)
|
||||
apply simp
|
||||
apply (case_tac "k : set(trace d (d a i) as)")
|
||||
apply (erule allE)
|
||||
apply (erule impE)
|
||||
apply (assumption)
|
||||
apply (erule exE)+
|
||||
apply (rule_tac x = "pref#mids" in exI)
|
||||
apply (rule_tac x = "suf" in exI)
|
||||
apply simp
|
||||
apply (rule_tac x = "[]" in exI)
|
||||
apply (rule_tac x = "as" in exI)
|
||||
apply simp
|
||||
apply (blast dest: in_set_butlastD)
|
||||
apply simp
|
||||
apply (erule allE)
|
||||
apply (erule impE)
|
||||
apply (assumption)
|
||||
apply (erule exE)+
|
||||
apply (rule_tac x = "a#pref" in exI)
|
||||
apply (rule_tac x = "mids" in exI)
|
||||
apply (rule_tac x = "suf" in exI)
|
||||
apply simp
|
||||
done
|
||||
|
||||
lemma length_trace[simp]: "\<And>i. length(trace d i xs) = length xs"
|
||||
by (induct "xs") simp_all
|
||||
|
||||
lemma deltas_append[simp]:
|
||||
"\<And>i. deltas d (xs@ys) i = deltas d ys (deltas d xs i)"
|
||||
by (induct "xs") simp_all
|
||||
|
||||
lemma trace_append[simp]:
|
||||
"\<And>i. trace d i (xs@ys) = trace d i xs @ trace d (deltas d xs i) ys"
|
||||
by (induct "xs") simp_all
|
||||
|
||||
lemma trace_concat[simp]:
|
||||
"(\<forall>xs \<in> set xss. deltas d xs i = i) \<Longrightarrow>
|
||||
trace d i (concat xss) = concat (map (trace d i) xss)"
|
||||
by (induct "xss") simp_all
|
||||
|
||||
lemma trace_is_Nil[simp]: "\<And>i. (trace d i xs = []) = (xs = [])"
|
||||
by (case_tac "xs") simp_all
|
||||
|
||||
lemma trace_is_Cons_conv[simp]:
|
||||
"(trace d i xs = n#ns) =
|
||||
(case xs of [] \<Rightarrow> False | y#ys \<Rightarrow> n = d y i \<and> ns = trace d n ys)"
|
||||
apply (case_tac "xs")
|
||||
apply simp_all
|
||||
apply (blast)
|
||||
done
|
||||
|
||||
lemma set_trace_conv:
|
||||
"\<And>i. set(trace d i xs) =
|
||||
(if xs=[] then {} else insert(deltas d xs i)(set(butlast(trace d i xs))))"
|
||||
apply (induct "xs")
|
||||
apply (simp)
|
||||
apply (simp add: insert_commute)
|
||||
done
|
||||
|
||||
lemma deltas_concat[simp]:
|
||||
"(\<forall>mid\<in>set mids. deltas d mid k = k) \<Longrightarrow> deltas d (concat mids) k = k"
|
||||
by (induct mids) simp_all
|
||||
|
||||
lemma lem: "[| n < Suc k; n \<noteq> k |] ==> n < k"
|
||||
by arith
|
||||
|
||||
lemma regset_spec:
|
||||
"\<And>i j xs. xs \<in> regset d i j k =
|
||||
((\<forall>n\<in>set(butlast(trace d i xs)). n < k) \<and> deltas d xs i = j)"
|
||||
apply (induct k)
|
||||
apply(simp split: list.split)
|
||||
apply(fastforce)
|
||||
apply (simp add: conc_def)
|
||||
apply (rule iffI)
|
||||
apply (erule disjE)
|
||||
apply simp
|
||||
apply (erule exE conjE)+
|
||||
apply simp
|
||||
apply (subgoal_tac
|
||||
"(\<forall>m\<in>set(butlast(trace d k xsb)). m < Suc k) \<and> deltas d xsb k = k")
|
||||
apply (simp add: set_trace_conv butlast_append ball_Un)
|
||||
apply (erule star_induct)
|
||||
apply (simp)
|
||||
apply (simp add: set_trace_conv butlast_append ball_Un)
|
||||
apply (case_tac "k : set(butlast(trace d i xs))")
|
||||
prefer 2 apply (rule disjI1)
|
||||
apply (blast intro:lem)
|
||||
apply (rule disjI2)
|
||||
apply (drule in_set_butlastD[THEN decompose])
|
||||
apply (clarify)
|
||||
apply (rule_tac x = "pref" in exI)
|
||||
apply simp
|
||||
apply (rule conjI)
|
||||
apply (rule ballI)
|
||||
apply (rule lem)
|
||||
prefer 2 apply simp
|
||||
apply (drule bspec) prefer 2 apply assumption
|
||||
apply simp
|
||||
apply (rule_tac x = "concat mids" in exI)
|
||||
apply (simp)
|
||||
apply (rule conjI)
|
||||
apply (rule concat_in_star)
|
||||
apply (clarsimp simp: subset_iff)
|
||||
apply (rule lem)
|
||||
prefer 2 apply simp
|
||||
apply (drule bspec) prefer 2 apply assumption
|
||||
apply (simp add: image_eqI in_set_butlast_concatI)
|
||||
apply (rule ballI)
|
||||
apply (rule lem)
|
||||
apply auto
|
||||
done
|
||||
|
||||
lemma trace_below:
|
||||
"bounded d k \<Longrightarrow> \<forall>i. i < k \<longrightarrow> (\<forall>n\<in>set(trace d i xs). n < k)"
|
||||
apply (unfold bounded_def)
|
||||
apply (induct "xs")
|
||||
apply simp
|
||||
apply (simp (no_asm))
|
||||
apply (blast)
|
||||
done
|
||||
|
||||
lemma regset_below:
|
||||
"[| bounded d k; i < k; j < k |] ==>
|
||||
regset d i j k = {xs. deltas d xs i = j}"
|
||||
apply (rule set_eqI)
|
||||
apply (simp add: regset_spec)
|
||||
apply (blast dest: trace_below in_set_butlastD)
|
||||
done
|
||||
|
||||
lemma deltas_below:
|
||||
"\<And>i. bounded d k \<Longrightarrow> i < k \<Longrightarrow> deltas d w i < k"
|
||||
apply (unfold bounded_def)
|
||||
apply (induct "w")
|
||||
apply simp_all
|
||||
done
|
||||
|
||||
lemma regset_DA_equiv:
|
||||
"[| bounded (next A) k; start A < k; j < k |] ==>
|
||||
w : regset_of_DA A k = accepts A w"
|
||||
apply(unfold regset_of_DA_def)
|
||||
apply (simp cong: conj_cong
|
||||
add: regset_below deltas_below accepts_def delta_def)
|
||||
done
|
||||
|
||||
end
|
|
@ -0,0 +1,6 @@
|
|||
@inproceedings{Nipkow-TPHOLs98,author={Tobias Nipkow},
|
||||
title={Verified Lexical Analysis},
|
||||
booktitle={Theorem Proving in Higher Order Logics},
|
||||
editor={J. Grundy and M. Newey},
|
||||
publisher=Springer,series=LNCS,volume={1479},pages={1--15},year=1998,
|
||||
note={\url{http://www4.informatik.tu-muenchen.de/~nipkow/pubs/tphols98.html}}}
|
|
@ -0,0 +1,54 @@
|
|||
|
||||
|
||||
\documentclass[11pt,a4paper]{article}
|
||||
\usepackage{isabelle,isabellesym}
|
||||
|
||||
|
||||
% this should be the last package used
|
||||
\usepackage{pdfsetup}
|
||||
|
||||
\begin{document}
|
||||
|
||||
\title{Functional Automata}
|
||||
\author{Tobias Nipkow}
|
||||
\maketitle
|
||||
|
||||
\begin{abstract}
|
||||
This theory defines deterministic and nondeterministic automata in a
|
||||
functional representation: the transition function/relation and the finality
|
||||
predicate are just functions. Hence the state space may be infinite. It is
|
||||
shown how to convert regular expressions into such automata. A scanner
|
||||
(generator) is implemented with the help of functional automata: the scanner
|
||||
chops the input up into longest recognized substrings. Finally we also show
|
||||
how to convert a certain subclass of functional automata (essentially the
|
||||
finite deterministic ones) into regular sets.
|
||||
\end{abstract}
|
||||
|
||||
\section{Overview}
|
||||
|
||||
The theories are structured as follows:
|
||||
\begin{itemize}
|
||||
\item Automata:
|
||||
\texttt{AutoProj}, \texttt{NA}, \texttt{NAe}, \texttt{DA}, \texttt{Automata}
|
||||
\item Conversion of regular expressions into automata:\\
|
||||
\texttt{RegExp2NA}, \texttt{RegExp2NAe}, \texttt{AutoRegExp}.
|
||||
\item Scanning: \texttt{MaxPrefix}, \texttt{MaxChop}, \texttt{AutoMaxChop}.
|
||||
\end{itemize}
|
||||
For a full description see \cite{Nipkow-TPHOLs98}.
|
||||
|
||||
In contrast to that paper, the latest version of the theories provides a
|
||||
fully executable scanner generator. The non-executable bits (transitive
|
||||
closure) have been eliminated by going from regular expressions directly to
|
||||
nondeterministic automata, thus bypassing epsilon-moves.
|
||||
|
||||
Not described in the paper is the conversion of certain functional automata
|
||||
(essentially the finite deterministic ones) into regular sets contained in
|
||||
\texttt{RegSet\_of\_nat\_DA}.
|
||||
|
||||
% include generated text of all theories
|
||||
\input{session}
|
||||
|
||||
\bibliographystyle{abbrv}
|
||||
\bibliography{root}
|
||||
|
||||
\end{document}
|
|
@ -46,6 +46,10 @@ begin
|
|||
|
||||
|
||||
text\<open> @{footnote \<open>sdf\<close>}, @{file "$ISABELLE_HOME/src/Pure/ROOT.ML"}\<close>
|
||||
<<<<<<< HEAD
|
||||
=======
|
||||
(*ML_file "patches/thy_output.ML";*)
|
||||
>>>>>>> d2e5bea25a311ff8210d30366b61b78bd7056efe
|
||||
|
||||
section\<open>Primitive Markup Generators\<close>
|
||||
ML\<open>
|
||||
|
|
|
@ -0,0 +1,375 @@
|
|||
section "Derivatives of regular expressions"
|
||||
|
||||
(* Author: Christian Urban *)
|
||||
|
||||
theory Derivatives
|
||||
imports Regular_Exp
|
||||
begin
|
||||
|
||||
text\<open>This theory is based on work by Brozowski \cite{Brzozowski64} and Antimirov \cite{Antimirov95}.\<close>
|
||||
|
||||
subsection \<open>Brzozowski's derivatives of regular expressions\<close>
|
||||
|
||||
primrec
|
||||
deriv :: "'a \<Rightarrow> 'a rexp \<Rightarrow> '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 \<Rightarrow> 'a rexp \<Rightarrow> 'a rexp"
|
||||
where
|
||||
"derivs [] r = r"
|
||||
| "derivs (c # s) r = derivs s (deriv c r)"
|
||||
|
||||
|
||||
lemma atoms_deriv_subset: "atoms (deriv x r) \<subseteq> atoms r"
|
||||
by (induction r) (auto)
|
||||
|
||||
lemma atoms_derivs_subset: "atoms (derivs w r) \<subseteq> 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 \<open>A regular expression matcher:\<close>
|
||||
|
||||
definition matcher :: "'a rexp \<Rightarrow> 'a list \<Rightarrow> bool" where
|
||||
"matcher r s = nullable (derivs s r)"
|
||||
|
||||
lemma matcher_correctness: "matcher r s \<longleftrightarrow> s \<in> lang r"
|
||||
by (induct s arbitrary: r)
|
||||
(simp_all add: nullable_iff lang_deriv matcher_def Deriv_def)
|
||||
|
||||
|
||||
subsection \<open>Antimirov's partial derivatives\<close>
|
||||
|
||||
abbreviation
|
||||
"Timess rs r \<equiv> (\<Union>r' \<in> rs. {Times r' r})"
|
||||
|
||||
lemma Timess_eq_image:
|
||||
"Timess rs r = (\<lambda>r'. Times r' r) ` rs"
|
||||
by auto
|
||||
|
||||
primrec
|
||||
pderiv :: "'a \<Rightarrow> 'a rexp \<Rightarrow> '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) \<union> (pderiv c r2)"
|
||||
| "pderiv c (Times r1 r2) =
|
||||
(if nullable r1 then Timess (pderiv c r1) r2 \<union> pderiv c r2 else Timess (pderiv c r1) r2)"
|
||||
| "pderiv c (Star r) = Timess (pderiv c r) (Star r)"
|
||||
|
||||
primrec
|
||||
pderivs :: "'a list \<Rightarrow> 'a rexp \<Rightarrow> ('a rexp) set"
|
||||
where
|
||||
"pderivs [] r = {r}"
|
||||
| "pderivs (c # s) r = \<Union> (pderivs s ` pderiv c r)"
|
||||
|
||||
abbreviation
|
||||
pderiv_set :: "'a \<Rightarrow> 'a rexp set \<Rightarrow> 'a rexp set"
|
||||
where
|
||||
"pderiv_set c rs \<equiv> \<Union> (pderiv c ` rs)"
|
||||
|
||||
abbreviation
|
||||
pderivs_set :: "'a list \<Rightarrow> 'a rexp set \<Rightarrow> 'a rexp set"
|
||||
where
|
||||
"pderivs_set s rs \<equiv> \<Union> (pderivs s ` rs)"
|
||||
|
||||
lemma pderivs_append:
|
||||
"pderivs (s1 @ s2) r = \<Union> (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) \<union> (pderivs s r2))"
|
||||
by (induct s) (simp_all)
|
||||
|
||||
lemma pderivs_Atom:
|
||||
shows "pderivs s (Atom c) \<subseteq> {Atom c, One}"
|
||||
by (induct s) (simp_all)
|
||||
|
||||
subsection \<open>Relating left-quotients and partial derivatives\<close>
|
||||
|
||||
lemma Deriv_pderiv:
|
||||
shows "Deriv c (lang r) = \<Union> (lang ` pderiv c r)"
|
||||
by (induct r) (auto simp add: nullable_iff conc_UNION_distrib)
|
||||
|
||||
lemma Derivs_pderivs:
|
||||
shows "Derivs s (lang r) = \<Union> (lang ` pderivs s r)"
|
||||
proof (induct s arbitrary: r)
|
||||
case (Cons c s)
|
||||
have ih: "\<And>r. Derivs s (lang r) = \<Union> (lang ` pderivs s r)" by fact
|
||||
have "Derivs (c # s) (lang r) = Derivs s (Deriv c (lang r))" by simp
|
||||
also have "\<dots> = Derivs s (\<Union> (lang ` pderiv c r))" by (simp add: Deriv_pderiv)
|
||||
also have "\<dots> = Derivss s (lang ` (pderiv c r))"
|
||||
by (auto simp add: Derivs_def)
|
||||
also have "\<dots> = \<Union> (lang ` (pderivs_set s (pderiv c r)))"
|
||||
using ih by auto
|
||||
also have "\<dots> = \<Union> (lang ` (pderivs (c # s) r))" by simp
|
||||
finally show "Derivs (c # s) (lang r) = \<Union> (lang ` pderivs (c # s) r)" .
|
||||
qed (simp add: Derivs_def)
|
||||
|
||||
subsection \<open>Relating derivatives and partial derivatives\<close>
|
||||
|
||||
lemma deriv_pderiv:
|
||||
shows "\<Union> (lang ` (pderiv c r)) = lang (deriv c r)"
|
||||
unfolding lang_deriv Deriv_pderiv by simp
|
||||
|
||||
lemma derivs_pderivs:
|
||||
shows "\<Union> (lang ` (pderivs s r)) = lang (derivs s r)"
|
||||
unfolding lang_derivs Derivs_pderivs by simp
|
||||
|
||||
|
||||
subsection \<open>Finiteness property of partial derivatives\<close>
|
||||
|
||||
definition
|
||||
pderivs_lang :: "'a lang \<Rightarrow> 'a rexp \<Rightarrow> 'a rexp set"
|
||||
where
|
||||
"pderivs_lang A r \<equiv> \<Union>x \<in> A. pderivs x r"
|
||||
|
||||
lemma pderivs_lang_subsetI:
|
||||
assumes "\<And>s. s \<in> A \<Longrightarrow> pderivs s r \<subseteq> C"
|
||||
shows "pderivs_lang A r \<subseteq> C"
|
||||
using assms unfolding pderivs_lang_def by (rule UN_least)
|
||||
|
||||
lemma pderivs_lang_union:
|
||||
shows "pderivs_lang (A \<union> B) r = (pderivs_lang A r \<union> pderivs_lang B r)"
|
||||
by (simp add: pderivs_lang_def)
|
||||
|
||||
lemma pderivs_lang_subset:
|
||||
shows "A \<subseteq> B \<Longrightarrow> pderivs_lang A r \<subseteq> pderivs_lang B r"
|
||||
by (auto simp add: pderivs_lang_def)
|
||||
|
||||
definition
|
||||
"UNIV1 \<equiv> 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 \<union> pderivs_lang UNIV1 r2"
|
||||
unfolding UNIV1_def pderivs_lang_def by auto
|
||||
|
||||
|
||||
text \<open>Non-empty suffixes of a string (needed for the cases of @{const Times} and @{const Star} below)\<close>
|
||||
|
||||
definition
|
||||
"PSuf s \<equiv> {v. v \<noteq> [] \<and> (\<exists>u. u @ v = s)}"
|
||||
|
||||
lemma PSuf_snoc:
|
||||
shows "PSuf (s @ [c]) = (PSuf s) @@ {[c]} \<union> {[c]}"
|
||||
unfolding PSuf_def conc_def
|
||||
by (auto simp add: append_eq_append_conv2 append_eq_Cons_conv)
|
||||
|
||||
lemma PSuf_Union:
|
||||
shows "(\<Union>v \<in> PSuf s @@ {[c]}. f v) = (\<Union>v \<in> 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) \<subseteq> Timess (pderivs s r1) r2 \<union> (pderivs_lang (PSuf s) r2)"
|
||||
proof (induct s rule: rev_induct)
|
||||
case (snoc c s)
|
||||
have ih: "pderivs s (Times r1 r2) \<subseteq> Timess (pderivs s r1) r2 \<union> (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 "\<dots> \<subseteq> pderiv_set c (Timess (pderivs s r1) r2 \<union> (pderivs_lang (PSuf s) r2))"
|
||||
using ih by fastforce
|
||||
also have "\<dots> = pderiv_set c (Timess (pderivs s r1) r2) \<union> pderiv_set c (pderivs_lang (PSuf s) r2)"
|
||||
by (simp)
|
||||
also have "\<dots> = pderiv_set c (Timess (pderivs s r1) r2) \<union> pderivs_lang (PSuf s @@ {[c]}) r2"
|
||||
by (simp add: pderivs_lang_snoc)
|
||||
also
|
||||
have "\<dots> \<subseteq> pderiv_set c (Timess (pderivs s r1) r2) \<union> pderiv c r2 \<union> pderivs_lang (PSuf s @@ {[c]}) r2"
|
||||
by auto
|
||||
also
|
||||
have "\<dots> \<subseteq> Timess (pderiv_set c (pderivs s r1)) r2 \<union> pderiv c r2 \<union> pderivs_lang (PSuf s @@ {[c]}) r2"
|
||||
by (auto simp add: if_splits)
|
||||
also have "\<dots> = Timess (pderivs (s @ [c]) r1) r2 \<union> pderiv c r2 \<union> pderivs_lang (PSuf s @@ {[c]}) r2"
|
||||
by (simp add: pderivs_snoc)
|
||||
also have "\<dots> \<subseteq> Timess (pderivs (s @ [c]) r1) r2 \<union> 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 \<in> UNIV1"
|
||||
shows "pderivs_lang (PSuf s) r \<subseteq> pderivs_lang UNIV1 r"
|
||||
using a unfolding UNIV1_def PSuf_def pderivs_lang_def by auto
|
||||
|
||||
lemma pderivs_lang_Times_aux2:
|
||||
assumes a: "s \<in> UNIV1"
|
||||
shows "Timess (pderivs s r1) r2 \<subseteq> 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) \<subseteq> Timess (pderivs_lang UNIV1 r1) r2 \<union> 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 \<noteq> []"
|
||||
shows "pderivs s (Star r) \<subseteq> Timess (pderivs_lang (PSuf s) r) (Star r)"
|
||||
using a
|
||||
proof (induct s rule: rev_induct)
|
||||
case (snoc c s)
|
||||
have ih: "s \<noteq> [] \<Longrightarrow> pderivs s (Star r) \<subseteq> Timess (pderivs_lang (PSuf s) r) (Star r)" by fact
|
||||
{ assume asm: "s \<noteq> []"
|
||||
have "pderivs (s @ [c]) (Star r) = pderiv_set c (pderivs s (Star r))" by (simp add: pderivs_snoc)
|
||||
also have "\<dots> \<subseteq> pderiv_set c (Timess (pderivs_lang (PSuf s) r) (Star r))"
|
||||
using ih[OF asm] by fast
|
||||
also have "\<dots> \<subseteq> Timess (pderiv_set c (pderivs_lang (PSuf s) r)) (Star r) \<union> pderiv c (Star r)"
|
||||
by (auto split: if_splits)
|
||||
also have "\<dots> \<subseteq> Timess (pderivs_lang (PSuf (s @ [c])) r) (Star r) \<union> (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 "\<dots> = 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) \<subseteq> 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 \<union> 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\<open>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.\<close>
|
||||
|
||||
fun awidth :: "'a rexp \<Rightarrow> 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) \<le> 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) \<le> awidth r"
|
||||
proof (induction r)
|
||||
case (Plus r1 r2)
|
||||
have "card (pderivs_lang UNIV1 (Plus r1 r2)) = card (pderivs_lang UNIV1 r1 \<union> pderivs_lang UNIV1 r2)" by simp
|
||||
also have "\<dots> \<le> card (pderivs_lang UNIV1 r1) + card (pderivs_lang UNIV1 r2)"
|
||||
by(simp add: card_Un_le)
|
||||
also have "\<dots> \<le> 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)) \<le> card (Timess (pderivs_lang UNIV1 r1) r2 \<union> pderivs_lang UNIV1 r2)"
|
||||
by (simp add: card_mono finite_pderivs_lang pderivs_lang_Times)
|
||||
also have "\<dots> \<le> card (Timess (pderivs_lang UNIV1 r1) r2) + card (pderivs_lang UNIV1 r2)"
|
||||
by (simp add: card_Un_le)
|
||||
also have "\<dots> \<le> card (pderivs_lang UNIV1 r1) + card (pderivs_lang UNIV1 r2)"
|
||||
by (simp add: card_Timess_pderivs_lang_le)
|
||||
also have "\<dots> \<le> awidth (Times r1 r2)" using Times.IH by simp
|
||||
finally show ?case .
|
||||
next
|
||||
case (Star r)
|
||||
have "card (pderivs_lang UNIV1 (Star r)) \<le> card (Timess (pderivs_lang UNIV1 r) (Star r))"
|
||||
by (simp add: card_mono finite_pderivs_lang pderivs_lang_Star)
|
||||
also have "\<dots> \<le> card (pderivs_lang UNIV1 r)" by (rule card_Timess_pderivs_lang_le)
|
||||
also have "\<dots> \<le> awidth (Star r)" by (simp add: Star.IH)
|
||||
finally show ?case .
|
||||
qed (auto)
|
||||
|
||||
text\<open>Antimirov's Theorem 3.4:\<close>
|
||||
theorem card_pderivs_lang_UNIV_le_awidth: "card (pderivs_lang UNIV r) \<le> awidth r + 1"
|
||||
proof -
|
||||
have "card (insert r (pderivs_lang UNIV1 r)) \<le> Suc (card (pderivs_lang UNIV1 r))"
|
||||
by(auto simp: card_insert_if[OF finite_pderivs_lang_UNIV1])
|
||||
also have "\<dots> \<le> Suc (awidth r)" by(simp add: card_pderivs_lang_UNIV1_le_awidth)
|
||||
finally show ?thesis by(simp add: pderivs_lang_UNIV)
|
||||
qed
|
||||
|
||||
text\<open>Antimirov's Corollary 3.5:\<close>
|
||||
corollary card_pderivs_lang_le_awidth: "card (pderivs_lang A r) \<le> 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
|
|
@ -0,0 +1,230 @@
|
|||
section \<open>Deciding Regular Expression Equivalence\<close>
|
||||
|
||||
theory Equivalence_Checking
|
||||
imports
|
||||
NDerivative
|
||||
"HOL-Library.While_Combinator"
|
||||
begin
|
||||
|
||||
|
||||
subsection \<open>Bisimulation between languages and regular expressions\<close>
|
||||
|
||||
coinductive bisimilar :: "'a lang \<Rightarrow> 'a lang \<Rightarrow> bool" where
|
||||
"([] \<in> K \<longleftrightarrow> [] \<in> L)
|
||||
\<Longrightarrow> (\<And>x. bisimilar (Deriv x K) (Deriv x L))
|
||||
\<Longrightarrow> bisimilar K L"
|
||||
|
||||
lemma equal_if_bisimilar:
|
||||
assumes "bisimilar K L" shows "K = L"
|
||||
proof (rule set_eqI)
|
||||
fix w
|
||||
from \<open>bisimilar K L\<close> show "w \<in> K \<longleftrightarrow> w \<in> L"
|
||||
proof (induct w arbitrary: K L)
|
||||
case Nil thus ?case by (auto elim: bisimilar.cases)
|
||||
next
|
||||
case (Cons a w K L)
|
||||
from \<open>bisimilar K L\<close> have "bisimilar (Deriv a K) (Deriv a L)"
|
||||
by (auto elim: bisimilar.cases)
|
||||
then have "w \<in> Deriv a K \<longleftrightarrow> w \<in> Deriv a L" by (rule Cons(1))
|
||||
thus ?case by (auto simp: Deriv_def)
|
||||
qed
|
||||
qed
|
||||
|
||||
lemma language_coinduct:
|
||||
fixes R (infixl "\<sim>" 50)
|
||||
assumes "K \<sim> L"
|
||||
assumes "\<And>K L. K \<sim> L \<Longrightarrow> ([] \<in> K \<longleftrightarrow> [] \<in> L)"
|
||||
assumes "\<And>K L x. K \<sim> L \<Longrightarrow> Deriv x K \<sim> Deriv x L"
|
||||
shows "K = L"
|
||||
apply (rule equal_if_bisimilar)
|
||||
apply (rule bisimilar.coinduct[of R, OF \<open>K \<sim> L\<close>])
|
||||
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 \<Rightarrow> 'a rexp_pair set \<Rightarrow> bool"
|
||||
where
|
||||
"is_bisimulation as R =
|
||||
(\<forall>(r,s)\<in> R. (atoms r \<union> atoms s \<subseteq> set as) \<and> (nullable r \<longleftrightarrow> nullable s) \<and>
|
||||
(\<forall>a\<in>set as. (nderiv a r, nderiv a s) \<in> R))"
|
||||
|
||||
lemma bisim_lang_eq:
|
||||
assumes bisim: "is_bisimulation as ps"
|
||||
assumes "(r, s) \<in> 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 = "\<lambda>K L. (\<exists>(r,s)\<in>ps'. K = lang r \<and> L = lang s)"
|
||||
show ?thesis
|
||||
proof (rule language_coinduct[where R="?R"])
|
||||
from \<open>(r, s) \<in> ps\<close>
|
||||
have "(r, s) \<in> 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) \<in> ps'"
|
||||
and KL: "K = lang r" "L = lang s" by auto
|
||||
with bisim' have "nullable r \<longleftrightarrow> nullable s"
|
||||
by (auto simp: is_bisimulation_def)
|
||||
thus "[] \<in> K \<longleftrightarrow> [] \<in> L" by (auto simp: nullable_iff KL)
|
||||
fix a
|
||||
show "?R (Deriv a K) (Deriv a L)"
|
||||
proof cases
|
||||
assume "a \<in> set as"
|
||||
with rs bisim'
|
||||
have "(nderiv a r, nderiv a s) \<in> ps'"
|
||||
by (auto simp: is_bisimulation_def)
|
||||
thus ?thesis by (force simp: KL lang_nderiv)
|
||||
next
|
||||
assume "a \<notin> set as"
|
||||
with bisim' rs
|
||||
have "a \<notin> atoms r" "a \<notin> 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 \<open>Closure computation\<close>
|
||||
|
||||
definition closure ::
|
||||
"'a::order list \<Rightarrow> 'a rexp_pair \<Rightarrow> ('a rexp_pairs * 'a rexp_pair set) option"
|
||||
where
|
||||
"closure as = rtrancl_while (%(r,s). nullable r = nullable s)
|
||||
(%(r,s). map (\<lambda>a. (nderiv a r, nderiv a s)) as)"
|
||||
|
||||
definition pre_bisim :: "'a::order list \<Rightarrow> 'a rexp \<Rightarrow> 'a rexp \<Rightarrow>
|
||||
'a rexp_pairs * 'a rexp_pair set \<Rightarrow> bool"
|
||||
where
|
||||
"pre_bisim as r s = (\<lambda>(ws,R).
|
||||
(r,s) \<in> R \<and> set ws \<subseteq> R \<and>
|
||||
(\<forall>(r,s)\<in> R. atoms r \<union> atoms s \<subseteq> set as) \<and>
|
||||
(\<forall>(r,s)\<in> R - set ws. (nullable r \<longleftrightarrow> nullable s) \<and>
|
||||
(\<forall>a\<in>set as. (nderiv a r, nderiv a s) \<in> R)))"
|
||||
|
||||
theorem closure_sound:
|
||||
assumes result: "closure as (r,s) = Some([],R)"
|
||||
and atoms: "atoms r \<union> atoms s \<subseteq> 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 (\<lambda>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) \<in> R"
|
||||
by (auto simp: pre_bisim_def is_bisimulation_def)
|
||||
thus "lang r = lang s" by (rule bisim_lang_eq)
|
||||
qed
|
||||
|
||||
subsection \<open>Bisimulation-free proof of closure computation\<close>
|
||||
|
||||
text\<open>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.\<close>
|
||||
|
||||
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 \<Longrightarrow> ((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 "\<forall>x\<in>set w. x \<in> A \<Longrightarrow> ((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 \<Longrightarrow> ((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 \<union> atoms s"
|
||||
shows "ws = [] \<longleftrightarrow> lang r = lang s"
|
||||
proof -
|
||||
have leq: "(lang r = lang s) =
|
||||
(\<forall>(r',s') \<in> {((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 \<in> set ((\<lambda>(p,q). map (\<lambda>a. (nderiv a p, nderiv a q)) as) x)} =
|
||||
{((r,s), nderiv a r, nderiv a s) |r s a. a \<in> 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 \<open>The overall procedure\<close>
|
||||
|
||||
primrec add_atoms :: "'a rexp \<Rightarrow> 'a list \<Rightarrow> '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 \<union> set as"
|
||||
by (induct r arbitrary: as) auto
|
||||
|
||||
|
||||
definition check_eqv :: "nat rexp \<Rightarrow> nat rexp \<Rightarrow> 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([],_) \<Rightarrow> True | _ \<Rightarrow> 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\<open>Test:\<close>
|
||||
lemma "check_eqv (Plus One (Times (Atom 0) (Star(Atom 0)))) (Star(Atom 0))"
|
||||
by eval
|
||||
|
||||
end
|
|
@ -0,0 +1,318 @@
|
|||
section \<open>Deciding Equivalence of Extended Regular Expressions\<close>
|
||||
|
||||
theory Equivalence_Checking2
|
||||
imports Regular_Exp2 "HOL-Library.While_Combinator"
|
||||
begin
|
||||
|
||||
subsection \<open>Term ordering\<close>
|
||||
|
||||
fun le_rexp :: "nat rexp \<Rightarrow> nat rexp \<Rightarrow> 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 \<open>Normalizing operations\<close>
|
||||
|
||||
text \<open>associativity, commutativity, idempotence, zero\<close>
|
||||
|
||||
fun nPlus :: "nat rexp \<Rightarrow> nat rexp \<Rightarrow> 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 \<open>associativity, zero, one\<close>
|
||||
|
||||
fun nTimes :: "nat rexp \<Rightarrow> nat rexp \<Rightarrow> 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 \<open>more optimisations:\<close>
|
||||
|
||||
fun nInter :: "nat rexp \<Rightarrow> nat rexp \<Rightarrow> 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 \<Rightarrow> 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 \<open>Derivative\<close>
|
||||
|
||||
primrec nderiv :: "nat \<Rightarrow> nat rexp \<Rightarrow> 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 \<Longrightarrow> 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 \<union> atoms s"
|
||||
by (induct r s rule: nPlus.induct) auto
|
||||
|
||||
lemma atoms_nTimes: "atoms (nTimes r s) \<subseteq> atoms r \<union> atoms s"
|
||||
by (induct r s rule: nTimes.induct) auto
|
||||
|
||||
lemma atoms_nInter: "atoms (nInter r s) \<subseteq> atoms r \<union> atoms s"
|
||||
by (induct r s rule: nInter.induct) auto
|
||||
|
||||
lemma atoms_norm: "atoms (norm r) \<subseteq> atoms r"
|
||||
by (induct r) (auto dest!:subsetD[OF atoms_nTimes]subsetD[OF atoms_nInter])
|
||||
|
||||
lemma atoms_nderiv: "atoms (nderiv a r) \<subseteq> atoms r"
|
||||
by (induct r) (auto simp: Let_def dest!:subsetD[OF atoms_nTimes]subsetD[OF atoms_nInter])
|
||||
|
||||
|
||||
subsection \<open>Bisimulation between languages and regular expressions\<close>
|
||||
|
||||
context
|
||||
fixes S :: "'a set"
|
||||
begin
|
||||
|
||||
coinductive bisimilar :: "'a lang \<Rightarrow> 'a lang \<Rightarrow> bool" where
|
||||
"K \<subseteq> lists S \<Longrightarrow> L \<subseteq> lists S
|
||||
\<Longrightarrow> ([] \<in> K \<longleftrightarrow> [] \<in> L)
|
||||
\<Longrightarrow> (\<And>x. x:S \<Longrightarrow> bisimilar (Deriv x K) (Deriv x L))
|
||||
\<Longrightarrow> bisimilar K L"
|
||||
|
||||
lemma equal_if_bisimilar:
|
||||
assumes "K \<subseteq> lists S" "L \<subseteq> lists S" "bisimilar K L" shows "K = L"
|
||||
proof (rule set_eqI)
|
||||
fix w
|
||||
from assms show "w \<in> K \<longleftrightarrow> w \<in> 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 \<open>bisimilar K L\<close> have "bisimilar (Deriv a K) (Deriv a L)"
|
||||
by (auto elim: bisimilar.cases)
|
||||
then have "w \<in> Deriv a K \<longleftrightarrow> w \<in> Deriv a L"
|
||||
by (metis Cons.IH bisimilar.cases)
|
||||
thus ?case by (auto simp: Deriv_def)
|
||||
next
|
||||
assume "a \<notin> S"
|
||||
thus ?case using Cons.prems by auto
|
||||
qed
|
||||
qed
|
||||
qed
|
||||
|
||||
lemma language_coinduct:
|
||||
fixes R (infixl "\<sim>" 50)
|
||||
assumes "\<And>K L. K \<sim> L \<Longrightarrow> K \<subseteq> lists S \<and> L \<subseteq> lists S"
|
||||
assumes "K \<sim> L"
|
||||
assumes "\<And>K L. K \<sim> L \<Longrightarrow> ([] \<in> K \<longleftrightarrow> [] \<in> L)"
|
||||
assumes "\<And>K L x. K \<sim> L \<Longrightarrow> x : S \<Longrightarrow> Deriv x K \<sim> 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 \<open>K \<sim> L\<close>])
|
||||
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 \<Rightarrow> rexp_pairs \<Rightarrow> bool"
|
||||
where
|
||||
"is_bisimulation as ps =
|
||||
(\<forall>(r,s)\<in> set ps. (atoms r \<union> atoms s \<subseteq> set as) \<and> (nullable r \<longleftrightarrow> nullable s) \<and>
|
||||
(\<forall>a\<in>set as. (nderiv a r, nderiv a s) \<in> set ps))"
|
||||
|
||||
|
||||
lemma bisim_lang_eq:
|
||||
assumes bisim: "is_bisimulation as ps"
|
||||
assumes "(r, s) \<in> set ps"
|
||||
shows "lang (set as) r = lang (set as) s"
|
||||
proof -
|
||||
let ?R = "\<lambda>K L. (\<exists>(r,s)\<in>set ps. K = lang (set as) r \<and> L = lang (set as) s)"
|
||||
show ?thesis
|
||||
proof (rule language_coinduct[where R="?R" and S = "set as"])
|
||||
from \<open>(r, s) \<in> set ps\<close> 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) \<in> set ps"
|
||||
and KL: "K = lang (set as) r" "L = lang (set as) s" by auto
|
||||
with bisim have "nullable r \<longleftrightarrow> nullable s"
|
||||
by (auto simp: is_bisimulation_def)
|
||||
thus "[] \<in> K \<longleftrightarrow> [] \<in> L" by (auto simp: nullable_iff[where S="set as"] KL)
|
||||
txt\<open>next case, but shared context\<close>
|
||||
from bisim rs KL lang_subset_lists[of _ "set as"]
|
||||
show "K \<subseteq> lists (set as) \<and> L \<subseteq> lists (set as)"
|
||||
unfolding is_bisimulation_def by blast
|
||||
txt\<open>next case, but shared context\<close>
|
||||
fix a assume "a \<in> set as"
|
||||
with rs bisim
|
||||
have "(nderiv a r, nderiv a s) \<in> set ps"
|
||||
by (auto simp: is_bisimulation_def)
|
||||
thus "?R (Deriv a K) (Deriv a L)" using \<open>a \<in> set as\<close>
|
||||
by (force simp: KL lang_nderiv)
|
||||
qed
|
||||
qed
|
||||
|
||||
subsection \<open>Closure computation\<close>
|
||||
|
||||
fun test :: "rexp_pairs * rexp_pairs \<Rightarrow> bool"
|
||||
where "test (ws, ps) = (case ws of [] \<Rightarrow> False | (p,q)#_ \<Rightarrow> nullable p = nullable q)"
|
||||
|
||||
fun step :: "nat list \<Rightarrow> rexp_pairs * rexp_pairs \<Rightarrow> rexp_pairs * rexp_pairs"
|
||||
where "step as (ws,ps) =
|
||||
(let
|
||||
(r, s) = hd ws;
|
||||
ps' = (r, s) # ps;
|
||||
succs = map (\<lambda>a. (nderiv a r, nderiv a s)) as;
|
||||
new = filter (\<lambda>p. p \<notin> set ps' \<union> set ws) succs
|
||||
in (new @ tl ws, ps'))"
|
||||
|
||||
definition closure ::
|
||||
"nat list \<Rightarrow> rexp_pairs * rexp_pairs
|
||||
\<Rightarrow> (rexp_pairs * rexp_pairs) option" where
|
||||
"closure as = while_option test (step as)"
|
||||
|
||||
definition pre_bisim :: "nat list \<Rightarrow> nat rexp \<Rightarrow> nat rexp \<Rightarrow>
|
||||
rexp_pairs * rexp_pairs \<Rightarrow> bool"
|
||||
where
|
||||
"pre_bisim as r s = (\<lambda>(ws,ps).
|
||||
((r, s) \<in> set ws \<union> set ps) \<and>
|
||||
(\<forall>(r,s)\<in> set ws \<union> set ps. atoms r \<union> atoms s \<subseteq> set as) \<and>
|
||||
(\<forall>(r,s)\<in> set ps. (nullable r \<longleftrightarrow> nullable s) \<and>
|
||||
(\<forall>a\<in>set as. (nderiv a r, nderiv a s) \<in> set ps \<union> set ws)))"
|
||||
|
||||
theorem closure_sound:
|
||||
assumes result: "closure as ([(r,s)],[]) = Some([],ps)"
|
||||
and atoms: "atoms r \<union> atoms s \<subseteq> set as"
|
||||
shows "lang (set as) r = lang (set as) s"
|
||||
proof-
|
||||
{ fix st have "pre_bisim as r s st \<Longrightarrow> test st \<Longrightarrow> 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) \<in> 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 \<open>The overall procedure\<close>
|
||||
|
||||
primrec add_atoms :: "nat rexp \<Rightarrow> nat list \<Rightarrow> 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 \<union> set as"
|
||||
by (induct r arbitrary: as) auto
|
||||
|
||||
definition check_eqv :: "nat list \<Rightarrow> nat rexp \<Rightarrow> nat rexp \<Rightarrow> bool"
|
||||
where
|
||||
"check_eqv as r s \<longleftrightarrow> set(add_atoms r (add_atoms s [])) \<subseteq> set as \<and>
|
||||
(case closure as ([(norm r, norm s)], []) of
|
||||
Some([],_) \<Rightarrow> True | _ \<Rightarrow> 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 \<union> atoms s \<subseteq> set as"
|
||||
using assms
|
||||
by (auto simp: check_eqv_def set_add_atoms split:option.splits list.splits)
|
||||
hence "atoms(norm r) \<union> atoms(norm s) \<subseteq> 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
|
|
@ -0,0 +1,85 @@
|
|||
section \<open>Normalizing Derivative\<close>
|
||||
|
||||
theory NDerivative
|
||||
imports
|
||||
Regular_Exp
|
||||
begin
|
||||
|
||||
subsection \<open>Normalizing operations\<close>
|
||||
|
||||
text \<open>associativity, commutativity, idempotence, zero\<close>
|
||||
|
||||
fun nPlus :: "'a::order rexp \<Rightarrow> 'a rexp \<Rightarrow> '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 \<open>associativity, zero, one\<close>
|
||||
|
||||
fun nTimes :: "'a::order rexp \<Rightarrow> 'a rexp \<Rightarrow> '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 \<Rightarrow> '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 \<Rightarrow> 'a rexp \<Rightarrow> '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 \<notin> atoms r \<Longrightarrow> nderiv x r = Zero"
|
||||
by (induction r) auto
|
||||
|
||||
lemma atoms_nPlus[simp]: "atoms (nPlus r s) = atoms r \<union> atoms s"
|
||||
by (induction r s rule: nPlus.induct) auto
|
||||
|
||||
lemma atoms_nTimes: "atoms (nTimes r s) \<subseteq> atoms r \<union> atoms s"
|
||||
by (induction r s rule: nTimes.induct) auto
|
||||
|
||||
lemma atoms_norm: "atoms (norm r) \<subseteq> atoms r"
|
||||
by (induction r) (auto dest!:subsetD[OF atoms_nTimes])
|
||||
|
||||
lemma atoms_nderiv: "atoms (nderiv a r) \<subseteq> atoms r"
|
||||
by (induction r) (auto simp: Let_def dest!:subsetD[OF atoms_nTimes])
|
||||
|
||||
end
|
|
@ -0,0 +1,12 @@
|
|||
chapter AFP
|
||||
|
||||
session "Regular-Sets" (AFP) = "HOL-Library" +
|
||||
options [timeout = 600]
|
||||
theories
|
||||
Regexp_Method
|
||||
Regexp_Constructions
|
||||
pEquivalence_Checking
|
||||
Equivalence_Checking2
|
||||
document_files
|
||||
"root.bib"
|
||||
"root.tex"
|
|
@ -0,0 +1,395 @@
|
|||
(*
|
||||
File: Regexp_Constructions.thy
|
||||
Author: Manuel Eberl <eberlm@in.tum.de>
|
||||
|
||||
Some simple constructions on regular expressions to illustrate closure properties of regular
|
||||
languages: reversal, substitution, prefixes, suffixes, subwords ("fragments")
|
||||
*)
|
||||
section \<open>Basic constructions on regular expressions\<close>
|
||||
theory Regexp_Constructions
|
||||
imports
|
||||
Main
|
||||
"HOL-Library.Sublist"
|
||||
Regular_Exp
|
||||
begin
|
||||
|
||||
subsection \<open>Reverse language\<close>
|
||||
|
||||
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 \<open>Substituting characters in a language\<close>
|
||||
|
||||
definition subst_word :: "('a \<Rightarrow> 'b list) \<Rightarrow> 'a list \<Rightarrow> '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 \<open>Suffix language\<close>
|
||||
|
||||
definition Suffixes :: "'a list set \<Rightarrow> 'a list set" where
|
||||
"Suffixes A = {w. \<exists>q. q @ w \<in> A}"
|
||||
|
||||
lemma Suffixes_altdef [code]: "Suffixes A = (\<Union>w\<in>A. set (suffixes w))"
|
||||
unfolding Suffixes_def set_suffixes_eq suffix_def by blast
|
||||
|
||||
lemma Nil_in_Suffixes_iff [simp]: "[] \<in> Suffixes A \<longleftrightarrow> A \<noteq> {}"
|
||||
by (auto simp: Suffixes_def)
|
||||
|
||||
lemma Suffixes_empty [simp]: "Suffixes {} = {}"
|
||||
by (auto simp: Suffixes_def)
|
||||
|
||||
lemma Suffixes_empty_iff [simp]: "Suffixes A = {} \<longleftrightarrow> 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) \<union> Suffixes A"
|
||||
by (simp add: Suffixes_altdef)
|
||||
|
||||
lemma Suffixes_conc [simp]: "A \<noteq> {} \<Longrightarrow> Suffixes (A @@ B) = Suffixes B \<union> (Suffixes A @@ B)"
|
||||
unfolding Suffixes_altdef conc_def by (force simp: suffix_append)
|
||||
|
||||
lemma Suffixes_union [simp]: "Suffixes (A \<union> B) = Suffixes A \<union> Suffixes B"
|
||||
by (auto simp: Suffixes_def)
|
||||
|
||||
lemma Suffixes_UNION [simp]: "Suffixes (UNION A f) = UNION A (\<lambda>x. Suffixes (f x))"
|
||||
by (auto simp: Suffixes_def)
|
||||
|
||||
lemma Suffixes_compower:
|
||||
assumes "A \<noteq> {}"
|
||||
shows "Suffixes (A ^^ n) = insert [] (Suffixes A @@ (\<Union>k<n. A ^^ k))"
|
||||
proof (induction n)
|
||||
case (Suc n)
|
||||
from Suc have "Suffixes (A ^^ Suc n) =
|
||||
insert [] (Suffixes A @@ ((\<Union>k<n. A ^^ k) \<union> A ^^ n))"
|
||||
by (simp_all add: assms conc_Un_distrib)
|
||||
also have "(\<Union>k<n. A ^^ k) \<union> A ^^ n = (\<Union>k\<in>insert n {..<n}. A ^^ k)" by blast
|
||||
also have "insert n {..<n} = {..<Suc n}" by auto
|
||||
finally show ?case .
|
||||
qed simp_all
|
||||
|
||||
lemma Suffixes_star [simp]:
|
||||
assumes "A \<noteq> {}"
|
||||
shows "Suffixes (star A) = Suffixes A @@ star A"
|
||||
proof -
|
||||
have "star A = (\<Union>n. A ^^ n)" unfolding star_def ..
|
||||
also have "Suffixes \<dots> = (\<Union>x. Suffixes (A ^^ x))" by simp
|
||||
also have "\<dots> = (\<Union>n. insert [] (Suffixes A @@ (\<Union>k<n. A ^^ k)))"
|
||||
using assms by (subst Suffixes_compower) auto
|
||||
also have "\<dots> = insert [] (Suffixes A @@ (\<Union>n. (\<Union>k<n. A ^^ k)))"
|
||||
by (simp_all add: conc_UNION_distrib)
|
||||
also have "(\<Union>n. (\<Union>k<n. A ^^ k)) = (\<Union>n. A ^^ n)" by auto
|
||||
also have "\<dots> = 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 \<open>Prefix language\<close>
|
||||
|
||||
definition Prefixes :: "'a list set \<Rightarrow> 'a list set" where
|
||||
"Prefixes A = {w. \<exists>q. w @ q \<in> A}"
|
||||
|
||||
lemma Prefixes_altdef [code]: "Prefixes A = (\<Union>w\<in>A. set (prefixes w))"
|
||||
unfolding Prefixes_def set_prefixes_eq prefix_def by blast
|
||||
|
||||
lemma Nil_in_Prefixes_iff [simp]: "[] \<in> Prefixes A \<longleftrightarrow> A \<noteq> {}"
|
||||
by (auto simp: Prefixes_def)
|
||||
|
||||
lemma Prefixes_empty [simp]: "Prefixes {} = {}"
|
||||
by (auto simp: Prefixes_def)
|
||||
|
||||
lemma Prefixes_empty_iff [simp]: "Prefixes A = {} \<longleftrightarrow> 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) \<union> Prefixes A"
|
||||
by (simp add: Prefixes_altdef)
|
||||
|
||||
lemma Prefixes_conc [simp]: "B \<noteq> {} \<Longrightarrow> Prefixes (A @@ B) = Prefixes A \<union> (A @@ Prefixes B)"
|
||||
unfolding Prefixes_altdef conc_def by (force simp: prefix_append)
|
||||
|
||||
lemma Prefixes_union [simp]: "Prefixes (A \<union> B) = Prefixes A \<union> Prefixes B"
|
||||
by (auto simp: Prefixes_def)
|
||||
|
||||
lemma Prefixes_UNION [simp]: "Prefixes (UNION A f) = UNION A (\<lambda>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 \<noteq> {}"
|
||||
shows "Prefixes (A ^^ n) = insert [] ((\<Union>k<n. A ^^ k) @@ Prefixes A)"
|
||||
proof -
|
||||
have "A ^^ n = rev ` ((rev ` A) ^^ n)" by (simp add: image_image)
|
||||
also have "Prefixes \<dots> = insert [] ((\<Union>k<n. A ^^ k) @@ Prefixes A)"
|
||||
unfolding Prefixes_rev
|
||||
by (subst Suffixes_compower) (simp_all add: image_UN image_image Suffixes_rev assms)
|
||||
finally show ?thesis .
|
||||
qed
|
||||
|
||||
lemma Prefixes_star [simp]:
|
||||
assumes "A \<noteq> {}"
|
||||
shows "Prefixes (star A) = star A @@ Prefixes A"
|
||||
proof -
|
||||
have "star A = rev ` star (rev ` A)" by (simp add: image_image)
|
||||
also have "Prefixes \<dots> = star A @@ Prefixes A"
|
||||
unfolding Prefixes_rev
|
||||
by (subst Suffixes_star) (simp_all add: assms image_image Suffixes_rev)
|
||||
finally show ?thesis .
|
||||
qed
|
||||
|
||||
|
||||
subsection \<open>Subword language\<close>
|
||||
|
||||
text \<open>
|
||||
The language of all sub-words, i.e. all words that are a contiguous sublist of a word in
|
||||
the original language.
|
||||
\<close>
|
||||
definition Sublists :: "'a list set \<Rightarrow> 'a list set" where
|
||||
"Sublists A = {w. \<exists>q\<in>A. sublist w q}"
|
||||
|
||||
lemma Sublists_altdef [code]: "Sublists A = (\<Union>w\<in>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) \<union> Sublists A"
|
||||
by (auto simp: Sublists_altdef)
|
||||
|
||||
lemma Sublists_Un [simp]: "Sublists (A \<union> B) = Sublists A \<union> Sublists B"
|
||||
by (auto simp: Sublists_altdef)
|
||||
|
||||
lemma Sublists_UN [simp]: "Sublists (UNION A f) = UNION A (\<lambda>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 \<noteq> {}" "B \<noteq> {}"
|
||||
shows "Sublists (A @@ B) = Sublists A \<union> Sublists B \<union> Suffixes A @@ Prefixes B"
|
||||
using assms unfolding Sublists_conv_Suffixes by auto
|
||||
|
||||
lemma star_not_empty [simp]: "star A \<noteq> {}"
|
||||
by auto
|
||||
|
||||
lemma Sublists_star:
|
||||
"A \<noteq> {} \<Longrightarrow> Sublists (star A) = Sublists A \<union> Suffixes A @@ star A @@ Prefixes A"
|
||||
by (simp add: Sublists_conv_Prefixes)
|
||||
|
||||
lemma Prefixes_subset_Sublists: "Prefixes A \<subseteq> Sublists A"
|
||||
unfolding Prefixes_def Sublists_def by auto
|
||||
|
||||
lemma Suffixes_subset_Sublists: "Suffixes A \<subseteq> Sublists A"
|
||||
unfolding Suffixes_def Sublists_def by auto
|
||||
|
||||
|
||||
subsection \<open>Fragment language\<close>
|
||||
|
||||
text \<open>
|
||||
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.
|
||||
\<close>
|
||||
definition Subseqs where "Subseqs A = (\<Union>w\<in>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) \<union> Subseqs A"
|
||||
by (simp add: Subseqs_def)
|
||||
|
||||
lemma Subseqs_singleton [simp]: "Subseqs {xs} = set (subseqs xs)"
|
||||
by simp
|
||||
|
||||
lemma Subseqs_Un [simp]: "Subseqs (A \<union> B) = Subseqs A \<union> Subseqs B"
|
||||
by (simp add: Subseqs_def)
|
||||
|
||||
lemma Subseqs_UNION [simp]: "Subseqs (UNION A f) = UNION A (\<lambda>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 \<in> Subseqs (A @@ B)"
|
||||
then obtain ys zs where *: "ys \<in> A" "zs \<in> 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 \<in> Subseqs A @@ Subseqs B" by (auto simp: Subseqs_def set_subseqs_eq)
|
||||
next
|
||||
fix xs assume "xs \<in> Subseqs A @@ Subseqs B"
|
||||
then obtain xs1 xs2 ys zs
|
||||
where "xs = xs1 @ xs2" "subseq xs1 ys" "subseq xs2 zs" "ys \<in> A" "zs \<in> B"
|
||||
by (auto simp: conc_def Subseqs_def)
|
||||
thus "xs \<in> 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 \<subseteq> Subseqs A"
|
||||
by (auto simp: Sublists_def Subseqs_def dest!: sublist_imp_subseq)
|
||||
|
||||
|
||||
subsection \<open>Various regular expression constructions\<close>
|
||||
|
||||
text \<open>A construction for language reversal of a regular expression:\<close>
|
||||
|
||||
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 \<open>The obvious construction for a singleton-language regular expression:\<close>
|
||||
|
||||
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 \<open>Character substitution in a regular expression:\<close>
|
||||
|
||||
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 \<open>Suffix language of a regular expression:\<close>
|
||||
|
||||
primrec suffix_rexp :: "'a rexp \<Rightarrow> '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 \<open>Prefix language of a regular expression:\<close>
|
||||
|
||||
primrec prefix_rexp :: "'a rexp \<Rightarrow> '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 \<open>Sub-word language of a regular expression\<close>
|
||||
|
||||
primrec sublist_rexp :: "'a rexp \<Rightarrow> '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 \<or> 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 \<open>Fragment language of a regular expression:\<close>
|
||||
|
||||
primrec subseqs_rexp :: "'a rexp \<Rightarrow> '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 \<open>Subword language of a regular expression\<close>
|
||||
|
||||
|
||||
end
|
|
@ -0,0 +1,67 @@
|
|||
section \<open>Proving Relation (In)equalities via Regular Expressions\<close>
|
||||
|
||||
theory Regexp_Method
|
||||
imports Equivalence_Checking Relation_Interpretation
|
||||
begin
|
||||
|
||||
primrec rel_of_regexp :: "('a * 'a) set list \<Rightarrow> nat rexp \<Rightarrow> ('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 \<union> 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 (\<lambda>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 \<Longrightarrow> 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 \<open>
|
||||
local
|
||||
|
||||
fun check_eqv (ct, b) = Thm.mk_binop @{cterm "Pure.eq :: bool \<Rightarrow> bool \<Rightarrow> 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
|
||||
\<close>
|
||||
|
||||
method_setup regexp = \<open>
|
||||
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)))
|
||||
\<close> \<open>decide relation equalities via regular expressions\<close>
|
||||
|
||||
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 \<open>Example:\<close>
|
||||
|
||||
lemma "(r \<union> s^+)^* = (r \<union> s)^*"
|
||||
by regexp
|
||||
|
||||
end
|
|
@ -0,0 +1,176 @@
|
|||
(* Author: Tobias Nipkow *)
|
||||
|
||||
section "Regular expressions"
|
||||
|
||||
theory Regular_Exp
|
||||
imports Regular_Set
|
||||
begin
|
||||
|
||||
datatype (atoms: 'a) rexp =
|
||||
is_Zero: Zero |
|
||||
is_One: One |
|
||||
Atom 'a |
|
||||
Plus "('a rexp)" "('a rexp)" |
|
||||
Times "('a rexp)" "('a rexp)" |
|
||||
Star "('a rexp)"
|
||||
|
||||
primrec lang :: "'a rexp => 'a lang" where
|
||||
"lang Zero = {}" |
|
||||
"lang One = {[]}" |
|
||||
"lang (Atom a) = {[a]}" |
|
||||
"lang (Plus r s) = (lang r) Un (lang s)" |
|
||||
"lang (Times r s) = conc (lang r) (lang s)" |
|
||||
"lang (Star r) = star(lang r)"
|
||||
|
||||
abbreviation (input) regular_lang where "regular_lang A \<equiv> (\<exists>r. lang r = A)"
|
||||
|
||||
primrec nullable :: "'a rexp \<Rightarrow> bool" where
|
||||
"nullable Zero = False" |
|
||||
"nullable One = True" |
|
||||
"nullable (Atom c) = False" |
|
||||
"nullable (Plus r1 r2) = (nullable r1 \<or> nullable r2)" |
|
||||
"nullable (Times r1 r2) = (nullable r1 \<and> nullable r2)" |
|
||||
"nullable (Star r) = True"
|
||||
|
||||
lemma nullable_iff [code_abbrev]: "nullable r \<longleftrightarrow> [] \<in> lang r"
|
||||
by (induct r) (auto simp add: conc_def split: if_splits)
|
||||
|
||||
primrec rexp_empty where
|
||||
"rexp_empty Zero \<longleftrightarrow> True"
|
||||
| "rexp_empty One \<longleftrightarrow> False"
|
||||
| "rexp_empty (Atom a) \<longleftrightarrow> False"
|
||||
| "rexp_empty (Plus r s) \<longleftrightarrow> rexp_empty r \<and> rexp_empty s"
|
||||
| "rexp_empty (Times r s) \<longleftrightarrow> rexp_empty r \<or> rexp_empty s"
|
||||
| "rexp_empty (Star r) \<longleftrightarrow> False"
|
||||
|
||||
(* TODO Fixme: This code_abbrev rule does not work. Why? *)
|
||||
lemma rexp_empty_iff [code_abbrev]: "rexp_empty r \<longleftrightarrow> lang r = {}"
|
||||
by (induction r) auto
|
||||
|
||||
|
||||
|
||||
text\<open>Composition on rhs usually complicates matters:\<close>
|
||||
lemma map_map_rexp:
|
||||
"map_rexp f (map_rexp g r) = map_rexp (\<lambda>r. f (g r)) r"
|
||||
unfolding rexp.map_comp o_def ..
|
||||
|
||||
lemma map_rexp_ident[simp]: "map_rexp (\<lambda>x. x) = (\<lambda>r. r)"
|
||||
unfolding id_def[symmetric] fun_eq_iff rexp.map_id id_apply by (intro allI refl)
|
||||
|
||||
lemma atoms_lang: "w : lang r \<Longrightarrow> set w \<subseteq> 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) =
|
||||
(\<forall>w \<in> lists(atoms r \<union> atoms s). w \<in> lang r \<longleftrightarrow> w \<in> lang s)"
|
||||
by (auto simp: atoms_lang[unfolded subset_iff])
|
||||
|
||||
lemma lang_eq_ext_Nil_fold_Deriv:
|
||||
fixes r s
|
||||
defines "\<BB> \<equiv> {(fold Deriv w (lang r), fold Deriv w (lang s))| w. w\<in>lists (atoms r \<union> atoms s)}"
|
||||
shows "lang r = lang s \<longleftrightarrow> (\<forall>(K, L) \<in> \<BB>. [] \<in> K \<longleftrightarrow> [] \<in> L)"
|
||||
unfolding lang_eq_ext \<BB>_def by (subst (1 2) in_fold_Deriv[of "[]", simplified, symmetric]) auto
|
||||
|
||||
|
||||
subsection \<open>Term ordering\<close>
|
||||
|
||||
instantiation rexp :: (order) "{order}"
|
||||
begin
|
||||
|
||||
fun le_rexp :: "('a::order) rexp \<Rightarrow> ('a::order) rexp \<Rightarrow> 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 \<le> s \<equiv> le_rexp r s"
|
||||
definition less_rexp where "r < s \<equiv> le_rexp r s \<and> r \<noteq> s"
|
||||
|
||||
lemma le_rexp_Zero: "le_rexp r Zero \<Longrightarrow> r = Zero"
|
||||
by (induction r) auto
|
||||
|
||||
lemma le_rexp_refl: "le_rexp r r"
|
||||
by (induction r) auto
|
||||
|
||||
lemma le_rexp_antisym: "\<lbrakk>le_rexp r s; le_rexp s r\<rbrakk> \<Longrightarrow> r = s"
|
||||
by (induction r s rule: le_rexp.induct) (auto dest: le_rexp_Zero)
|
||||
|
||||
lemma le_rexp_trans: "\<lbrakk>le_rexp r s; le_rexp s t\<rbrakk> \<Longrightarrow> 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: "\<And>t. le_rexp r s \<Longrightarrow> le_rexp s t \<Longrightarrow> 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 "\<And>t. r1 = s1 \<Longrightarrow> le_rexp r2 s2 \<Longrightarrow> le_rexp s2 t \<Longrightarrow> le_rexp r2 t"
|
||||
"\<And>t. r1 \<noteq> s1 \<Longrightarrow> le_rexp r1 s1 \<Longrightarrow> le_rexp s1 t \<Longrightarrow> 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 "\<And>t. r1 = s1 \<Longrightarrow> le_rexp r2 s2 \<Longrightarrow> le_rexp s2 t \<Longrightarrow> le_rexp r2 t"
|
||||
"\<And>t. r1 \<noteq> s1 \<Longrightarrow> le_rexp r1 s1 \<Longrightarrow> le_rexp s1 t \<Longrightarrow> 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 \<or> 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
|
|
@ -0,0 +1,51 @@
|
|||
(* Author: Tobias Nipkow *)
|
||||
|
||||
section "Extended Regular Expressions"
|
||||
|
||||
theory Regular_Exp2
|
||||
imports Regular_Set
|
||||
begin
|
||||
|
||||
datatype (atoms: 'a) rexp =
|
||||
is_Zero: Zero |
|
||||
is_One: One |
|
||||
Atom 'a |
|
||||
Plus "('a rexp)" "('a rexp)" |
|
||||
Times "('a rexp)" "('a rexp)" |
|
||||
Star "('a rexp)" |
|
||||
Not "('a rexp)" |
|
||||
Inter "('a rexp)" "('a rexp)"
|
||||
|
||||
context
|
||||
fixes S :: "'a set"
|
||||
begin
|
||||
|
||||
primrec lang :: "'a rexp => 'a lang" where
|
||||
"lang Zero = {}" |
|
||||
"lang One = {[]}" |
|
||||
"lang (Atom a) = {[a]}" |
|
||||
"lang (Plus r s) = (lang r) Un (lang s)" |
|
||||
"lang (Times r s) = conc (lang r) (lang s)" |
|
||||
"lang (Star r) = star(lang r)" |
|
||||
"lang (Not r) = lists S - lang r" |
|
||||
"lang (Inter r s) = (lang r Int lang s)"
|
||||
|
||||
end
|
||||
|
||||
lemma lang_subset_lists: "atoms r \<subseteq> S \<Longrightarrow> lang S r \<subseteq> lists S"
|
||||
by(induction r)(auto simp: conc_subset_lists star_subset_lists)
|
||||
|
||||
primrec nullable :: "'a rexp \<Rightarrow> bool" where
|
||||
"nullable Zero = False" |
|
||||
"nullable One = True" |
|
||||
"nullable (Atom c) = False" |
|
||||
"nullable (Plus r1 r2) = (nullable r1 \<or> nullable r2)" |
|
||||
"nullable (Times r1 r2) = (nullable r1 \<and> nullable r2)" |
|
||||
"nullable (Star r) = True" |
|
||||
"nullable (Not r) = (\<not> (nullable r))" |
|
||||
"nullable (Inter r s) = (nullable r \<and> nullable s)"
|
||||
|
||||
lemma nullable_iff: "nullable r \<longleftrightarrow> [] \<in> lang S r"
|
||||
by (induct r) (auto simp add: conc_def split: if_splits)
|
||||
|
||||
end
|
|
@ -0,0 +1,456 @@
|
|||
(* 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 \<Rightarrow> 'a lang \<Rightarrow> 'a lang" (infixr "@@" 75) where
|
||||
"A @@ B = {xs@ys | xs ys. xs:A & ys:B}"
|
||||
|
||||
text \<open>checks the code preprocessor for set comprehensions\<close>
|
||||
export_code conc checking SML
|
||||
|
||||
overloading lang_pow == "compow :: nat \<Rightarrow> 'a lang \<Rightarrow> 'a lang"
|
||||
begin
|
||||
primrec lang_pow :: "nat \<Rightarrow> 'a lang \<Rightarrow> 'a lang" where
|
||||
"lang_pow 0 A = {[]}" |
|
||||
"lang_pow (Suc n) A = A @@ (lang_pow n A)"
|
||||
end
|
||||
|
||||
text \<open>for code generation\<close>
|
||||
|
||||
definition lang_pow :: "nat \<Rightarrow> 'a lang \<Rightarrow> '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 \<Rightarrow> 'a lang" where
|
||||
"star A = (\<Union>n. A ^^ n)"
|
||||
|
||||
|
||||
subsection\<open>@{term "(@@)"}\<close>
|
||||
|
||||
lemma concI[simp,intro]: "u : A \<Longrightarrow> v : B \<Longrightarrow> u@v : A @@ B"
|
||||
by (auto simp add: conc_def)
|
||||
|
||||
lemma concE[elim]:
|
||||
assumes "w \<in> A @@ B"
|
||||
obtains u v where "u \<in> A" "v \<in> B" "w = u@v"
|
||||
using assms by (auto simp: conc_def)
|
||||
|
||||
lemma conc_mono: "A \<subseteq> C \<Longrightarrow> B \<subseteq> D \<Longrightarrow> A @@ B \<subseteq> 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 \<union> C) = A @@ B \<union> A @@ C"
|
||||
and "(A \<union> B) @@ C = A @@ C \<union> 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 \<subseteq> lists S \<Longrightarrow> B \<subseteq> lists S \<Longrightarrow> A @@ B \<subseteq> lists S"
|
||||
by(fastforce simp: conc_def in_lists_conv_set)
|
||||
|
||||
lemma Nil_in_conc[simp]: "[] \<in> A @@ B \<longleftrightarrow> [] \<in> A \<and> [] \<in> B"
|
||||
by (metis append_is_Nil_conv concE concI)
|
||||
|
||||
lemma concI_if_Nil1: "[] \<in> A \<Longrightarrow> xs : B \<Longrightarrow> xs \<in> A @@ B"
|
||||
by (metis append_Nil concI)
|
||||
|
||||
lemma conc_Diff_if_Nil1: "[] \<in> A \<Longrightarrow> A @@ B = (A - {[]}) @@ B \<union> B"
|
||||
by (fastforce elim: concI_if_Nil1)
|
||||
|
||||
lemma concI_if_Nil2: "[] \<in> B \<Longrightarrow> xs : A \<Longrightarrow> xs \<in> A @@ B"
|
||||
by (metis append_Nil2 concI)
|
||||
|
||||
lemma conc_Diff_if_Nil2: "[] \<in> B \<Longrightarrow> A @@ B = A @@ (B - {[]}) \<union> A"
|
||||
by (fastforce elim: concI_if_Nil2)
|
||||
|
||||
lemma singleton_in_conc:
|
||||
"[x] : A @@ B \<longleftrightarrow> [x] : A \<and> [] : B \<or> [] : A \<and> [x] : B"
|
||||
by (fastforce simp: Cons_eq_append_conv append_eq_Cons_conv
|
||||
conc_Diff_if_Nil1 conc_Diff_if_Nil2)
|
||||
|
||||
|
||||
subsection\<open>@{term "A ^^ n"}\<close>
|
||||
|
||||
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:
|
||||
"\<forall>w \<in> A. length w \<le> k \<Longrightarrow> w : A^^n \<Longrightarrow> length w \<le> k*n"
|
||||
by(induct n arbitrary: w) (fastforce simp: conc_def)+
|
||||
|
||||
lemma length_lang_pow_lb:
|
||||
"\<forall>w \<in> A. length w \<ge> k \<Longrightarrow> w : A^^n \<Longrightarrow> length w \<ge> k*n"
|
||||
by(induct n arbitrary: w) (fastforce simp: conc_def)+
|
||||
|
||||
lemma lang_pow_subset_lists: "A \<subseteq> lists S \<Longrightarrow> A ^^ n \<subseteq> lists S"
|
||||
by(induct n)(auto simp: conc_subset_lists)
|
||||
|
||||
|
||||
subsection\<open>@{const star}\<close>
|
||||
|
||||
lemma star_subset_lists: "A \<subseteq> lists S \<Longrightarrow> star A \<subseteq> lists S"
|
||||
unfolding star_def by(blast dest: lang_pow_subset_lists)
|
||||
|
||||
lemma star_if_lang_pow[simp]: "w : A ^^ n \<Longrightarrow> 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 \<open>w : A\<close> by simp
|
||||
qed
|
||||
|
||||
lemma append_in_starI[simp]:
|
||||
assumes "u : star A" and "v : star A" shows "u@v : star A"
|
||||
proof -
|
||||
from \<open>u : star A\<close> obtain m where "u : A ^^ m" by (auto simp: star_def)
|
||||
moreover
|
||||
from \<open>v : star A\<close> 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 \<Longrightarrow> v : star A \<Longrightarrow> P v \<Longrightarrow> P (u@v)"
|
||||
shows "P w"
|
||||
proof -
|
||||
{ fix n have "w : A ^^ n \<Longrightarrow> P w"
|
||||
by (induct n arbitrary: w) (auto intro: \<open>P []\<close> step star_if_lang_pow) }
|
||||
with \<open>w : star A\<close> 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 \<union> {[]}" (is "?L = ?R")
|
||||
proof
|
||||
show "?L \<subseteq> ?R" by (rule, erule star_induct) auto
|
||||
qed auto
|
||||
|
||||
lemma concat_in_star: "set ws \<subseteq> A \<Longrightarrow> concat ws : star A"
|
||||
by (induct ws) simp_all
|
||||
|
||||
lemma in_star_iff_concat:
|
||||
"w \<in> star A = (\<exists>ws. set ws \<subseteq> A \<and> w = concat ws)"
|
||||
(is "_ = (\<exists>ws. ?R w ws)")
|
||||
proof
|
||||
assume "w : star A" thus "\<exists>ws. ?R w ws"
|
||||
proof induct
|
||||
case Nil have "?R [] []" by simp
|
||||
thus ?case ..
|
||||
next
|
||||
case (append u v)
|
||||
then obtain ws where "set ws \<subseteq> A \<and> v = concat ws" by blast
|
||||
with append have "?R (u@v) (u#ws)" by auto
|
||||
thus ?case ..
|
||||
qed
|
||||
next
|
||||
assume "\<exists>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 \<subseteq> A}"
|
||||
by (fastforce simp: in_star_iff_concat)
|
||||
|
||||
lemma star_insert_eps[simp]: "star (insert [] A) = star(A)"
|
||||
proof-
|
||||
{ fix us
|
||||
have "set us \<subseteq> insert [] A \<Longrightarrow> \<exists>vs. concat us = concat vs \<and> set vs \<subseteq> A"
|
||||
(is "?P \<Longrightarrow> \<exists>vs. ?Q vs")
|
||||
proof
|
||||
let ?vs = "filter (%u. u \<noteq> []) us"
|
||||
show "?P \<Longrightarrow> ?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) \<union> {[]}"
|
||||
by (metis insert_Diff_single star_insert_eps star_unfold_left)
|
||||
|
||||
lemma star_Diff_Nil_fold: "(A - {[]}) @@ star A = star A - {[]}"
|
||||
proof -
|
||||
have "[] \<notin> (A - {[]}) @@ star A" by simp
|
||||
thus ?thesis using star_unfold_left_Nil by blast
|
||||
qed
|
||||
|
||||
lemma star_decom:
|
||||
assumes a: "x \<in> star A" "x \<noteq> []"
|
||||
shows "\<exists>a b. x = a @ b \<and> a \<noteq> [] \<and> a \<in> A \<and> b \<in> star A"
|
||||
using a by (induct rule: star_induct) (blast)+
|
||||
|
||||
|
||||
subsection \<open>Left-Quotients of languages\<close>
|
||||
|
||||
definition Deriv :: "'a \<Rightarrow> 'a lang \<Rightarrow> 'a lang"
|
||||
where "Deriv x A = { xs. x#xs \<in> A }"
|
||||
|
||||
definition Derivs :: "'a list \<Rightarrow> 'a lang \<Rightarrow> 'a lang"
|
||||
where "Derivs xs A = { ys. xs @ ys \<in> A }"
|
||||
|
||||
abbreviation
|
||||
Derivss :: "'a list \<Rightarrow> 'a lang set \<Rightarrow> 'a lang"
|
||||
where
|
||||
"Derivss s As \<equiv> \<Union> (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 \<union> B) = Deriv a A \<union> Deriv a B"
|
||||
and Deriv_inter[simp]: "Deriv a (A \<inter> B) = Deriv a A \<inter> 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 \<union> (if [] \<in> 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 ({[]} \<union> 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) \<union> (if [] \<in> 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 \<Longrightarrow> 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 \<in> fold Deriv w L \<longleftrightarrow> w @ v \<in> 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 (\<lambda>xs. case xs of x' # _ \<Rightarrow> x = x' | _ \<Rightarrow> False) A"
|
||||
by (auto simp: Deriv_def Set.filter_def image_iff tl_def split: list.splits)
|
||||
|
||||
subsection \<open>Shuffle product\<close>
|
||||
|
||||
definition Shuffle (infixr "\<parallel>" 80) where
|
||||
"Shuffle A B = \<Union>{shuffle xs ys | xs ys. xs \<in> A \<and> ys \<in> B}"
|
||||
|
||||
lemma Deriv_Shuffle[simp]:
|
||||
"Deriv a (A \<parallel> B) = Deriv a A \<parallel> B \<union> A \<parallel> Deriv a B"
|
||||
unfolding Shuffle_def Deriv_def by (fastforce simp: Cons_in_shuffle_iff neq_Nil_conv)
|
||||
|
||||
lemma shuffle_subset_lists:
|
||||
assumes "A \<subseteq> lists S" "B \<subseteq> lists S"
|
||||
shows "A \<parallel> B \<subseteq> lists S"
|
||||
unfolding Shuffle_def proof safe
|
||||
fix x and zs xs ys :: "'a list"
|
||||
assume zs: "zs \<in> shuffle xs ys" "x \<in> set zs" and "xs \<in> A" "ys \<in> B"
|
||||
with assms have "xs \<in> lists S" "ys \<in> lists S" by auto
|
||||
with zs show "x \<in> S" by (induct xs ys arbitrary: zs rule: shuffle.induct) auto
|
||||
qed
|
||||
|
||||
lemma Nil_in_Shuffle[simp]: "[] \<in> A \<parallel> B \<longleftrightarrow> [] \<in> A \<and> [] \<in> B"
|
||||
unfolding Shuffle_def by force
|
||||
|
||||
lemma shuffle_Un_distrib:
|
||||
shows "A \<parallel> (B \<union> C) = A \<parallel> B \<union> A \<parallel> C"
|
||||
and "A \<parallel> (B \<union> C) = A \<parallel> B \<union> A \<parallel> C"
|
||||
unfolding Shuffle_def by fast+
|
||||
|
||||
lemma shuffle_UNION_distrib:
|
||||
shows "A \<parallel> UNION I M = UNION I (%i. A \<parallel> M i)"
|
||||
and "UNION I M \<parallel> A = UNION I (%i. M i \<parallel> A)"
|
||||
unfolding Shuffle_def by fast+
|
||||
|
||||
lemma Shuffle_empty[simp]:
|
||||
"A \<parallel> {} = {}"
|
||||
"{} \<parallel> B = {}"
|
||||
unfolding Shuffle_def by auto
|
||||
|
||||
lemma Shuffle_eps[simp]:
|
||||
"A \<parallel> {[]} = A"
|
||||
"{[]} \<parallel> B = B"
|
||||
unfolding Shuffle_def by auto
|
||||
|
||||
|
||||
subsection \<open>Arden's Lemma\<close>
|
||||
|
||||
lemma arden_helper:
|
||||
assumes eq: "X = A @@ X \<union> B"
|
||||
shows "X = (A ^^ Suc n) @@ X \<union> (\<Union>m\<le>n. (A ^^ m) @@ B)"
|
||||
proof (induct n)
|
||||
case 0
|
||||
show "X = (A ^^ Suc 0) @@ X \<union> (\<Union>m\<le>0. (A ^^ m) @@ B)"
|
||||
using eq by simp
|
||||
next
|
||||
case (Suc n)
|
||||
have ih: "X = (A ^^ Suc n) @@ X \<union> (\<Union>m\<le>n. (A ^^ m) @@ B)" by fact
|
||||
also have "\<dots> = (A ^^ Suc n) @@ (A @@ X \<union> B) \<union> (\<Union>m\<le>n. (A ^^ m) @@ B)" using eq by simp
|
||||
also have "\<dots> = (A ^^ Suc (Suc n)) @@ X \<union> ((A ^^ Suc n) @@ B) \<union> (\<Union>m\<le>n. (A ^^ m) @@ B)"
|
||||
by (simp add: conc_Un_distrib conc_assoc[symmetric] conc_pow_comm)
|
||||
also have "\<dots> = (A ^^ Suc (Suc n)) @@ X \<union> (\<Union>m\<le>Suc n. (A ^^ m) @@ B)"
|
||||
by (auto simp add: atMost_Suc)
|
||||
finally show "X = (A ^^ Suc (Suc n)) @@ X \<union> (\<Union>m\<le>Suc n. (A ^^ m) @@ B)" .
|
||||
qed
|
||||
|
||||
lemma Arden:
|
||||
assumes "[] \<notin> A"
|
||||
shows "X = A @@ X \<union> B \<longleftrightarrow> X = star A @@ B"
|
||||
proof
|
||||
assume eq: "X = A @@ X \<union> B"
|
||||
{ fix w assume "w : X"
|
||||
let ?n = "size w"
|
||||
from \<open>[] \<notin> A\<close> have "\<forall>u \<in> A. length u \<ge> 1"
|
||||
by (metis Suc_eq_plus1 add_leD2 le_0_eq length_0_conv not_less_eq_eq)
|
||||
hence "\<forall>u \<in> A^^(?n+1). length u \<ge> ?n+1"
|
||||
by (metis length_lang_pow_lb nat_mult_1)
|
||||
hence "\<forall>u \<in> A^^(?n+1)@@X. length u \<ge> ?n+1"
|
||||
by(auto simp only: conc_def length_append)
|
||||
hence "w \<notin> A^^(?n+1)@@X" by auto
|
||||
hence "w : star A @@ B" using \<open>w : X\<close> 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 "\<exists>n. w \<in> 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 \<union> {[]}"
|
||||
by (rule star_unfold_left)
|
||||
then have "star A @@ B = (A @@ star A \<union> {[]}) @@ B"
|
||||
by metis
|
||||
also have "\<dots> = (A @@ star A) @@ B \<union> B"
|
||||
unfolding conc_Un_distrib by simp
|
||||
also have "\<dots> = A @@ (star A @@ B) \<union> B"
|
||||
by (simp only: conc_assoc)
|
||||
finally show "X = A @@ X \<union> B"
|
||||
using eq by blast
|
||||
qed
|
||||
|
||||
|
||||
lemma reversed_arden_helper:
|
||||
assumes eq: "X = X @@ A \<union> B"
|
||||
shows "X = X @@ (A ^^ Suc n) \<union> (\<Union>m\<le>n. B @@ (A ^^ m))"
|
||||
proof (induct n)
|
||||
case 0
|
||||
show "X = X @@ (A ^^ Suc 0) \<union> (\<Union>m\<le>0. B @@ (A ^^ m))"
|
||||
using eq by simp
|
||||
next
|
||||
case (Suc n)
|
||||
have ih: "X = X @@ (A ^^ Suc n) \<union> (\<Union>m\<le>n. B @@ (A ^^ m))" by fact
|
||||
also have "\<dots> = (X @@ A \<union> B) @@ (A ^^ Suc n) \<union> (\<Union>m\<le>n. B @@ (A ^^ m))" using eq by simp
|
||||
also have "\<dots> = X @@ (A ^^ Suc (Suc n)) \<union> (B @@ (A ^^ Suc n)) \<union> (\<Union>m\<le>n. B @@ (A ^^ m))"
|
||||
by (simp add: conc_Un_distrib conc_assoc)
|
||||
also have "\<dots> = X @@ (A ^^ Suc (Suc n)) \<union> (\<Union>m\<le>Suc n. B @@ (A ^^ m))"
|
||||
by (auto simp add: atMost_Suc)
|
||||
finally show "X = X @@ (A ^^ Suc (Suc n)) \<union> (\<Union>m\<le>Suc n. B @@ (A ^^ m))" .
|
||||
qed
|
||||
|
||||
theorem reversed_Arden:
|
||||
assumes nemp: "[] \<notin> A"
|
||||
shows "X = X @@ A \<union> B \<longleftrightarrow> X = B @@ star A"
|
||||
proof
|
||||
assume eq: "X = X @@ A \<union> B"
|
||||
{ fix w assume "w : X"
|
||||
let ?n = "size w"
|
||||
from \<open>[] \<notin> A\<close> have "\<forall>u \<in> A. length u \<ge> 1"
|
||||
by (metis Suc_eq_plus1 add_leD2 le_0_eq length_0_conv not_less_eq_eq)
|
||||
hence "\<forall>u \<in> A^^(?n+1). length u \<ge> ?n+1"
|
||||
by (metis length_lang_pow_lb nat_mult_1)
|
||||
hence "\<forall>u \<in> X @@ A^^(?n+1). length u \<ge> ?n+1"
|
||||
by(auto simp only: conc_def length_append)
|
||||
hence "w \<notin> X @@ A^^(?n+1)" by auto
|
||||
hence "w : B @@ star A" using \<open>w : X\<close> 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 "\<exists>n. w \<in> 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 = {[]} \<union> star A @@ A"
|
||||
unfolding conc_star_comm[symmetric]
|
||||
by(metis Un_commute star_unfold_left)
|
||||
then have "B @@ star A = B @@ ({[]} \<union> star A @@ A)"
|
||||
by metis
|
||||
also have "\<dots> = B \<union> B @@ (star A @@ A)"
|
||||
unfolding conc_Un_distrib by simp
|
||||
also have "\<dots> = B \<union> (B @@ star A) @@ A"
|
||||
by (simp only: conc_assoc)
|
||||
finally show "X = X @@ A \<union> B"
|
||||
using eq by blast
|
||||
qed
|
||||
|
||||
end
|
|
@ -0,0 +1,53 @@
|
|||
section \<open>Regular Expressions as Homogeneous Binary Relations\<close>
|
||||
|
||||
theory Relation_Interpretation
|
||||
imports Regular_Exp
|
||||
begin
|
||||
|
||||
primrec rel :: "('a \<Rightarrow> ('b * 'b) set) \<Rightarrow> 'a rexp \<Rightarrow> ('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 \<union> 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 \<Rightarrow> ('b * 'b) set) \<Rightarrow> 'a list \<Rightarrow> ('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 = (\<Union>w\<in>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 = (\<Union>w \<in> 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 \<open>Soundness:\<close>
|
||||
|
||||
lemma soundness:
|
||||
"lang r = lang s \<Longrightarrow> rel v r = rel v s"
|
||||
unfolding rel_word_rel by auto
|
||||
|
||||
end
|
|
@ -0,0 +1,36 @@
|
|||
@article{KraussN-JAR,author={Alexander Krauss and Tobias Nipkow},
|
||||
title={Proof Pearl: Regular Expression Equivalence and Relation Algebra},
|
||||
journal={J. Automated Reasoning},volume=49,pages={95--106},year=2012,note={published online March 2011}}
|
||||
|
||||
@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}
|
||||
}
|
|
@ -0,0 +1,47 @@
|
|||
\documentclass[11pt,a4paper]{article}
|
||||
\usepackage{isabelle,isabellesym}
|
||||
\usepackage{eufrak}
|
||||
|
||||
% this should be the last package used
|
||||
\usepackage{pdfsetup}
|
||||
|
||||
% urls in roman style, theory text in math-similar italics
|
||||
\urlstyle{rm}
|
||||
\isabellestyle{it}
|
||||
|
||||
|
||||
\begin{document}
|
||||
|
||||
\title{Regular Sets, Expressions, Derivatives and Relation Algebra}
|
||||
\author{Alexander Krauss, Tobias Nipkow,\\
|
||||
Chunhan Wu, Xingyuan Zhang and Christian Urban}
|
||||
\maketitle
|
||||
|
||||
\begin{abstract}
|
||||
This is a library of constructions on regular expressions and languages. It
|
||||
provides the operations of concatenation, Kleene star and left-quotients of
|
||||
languages. A theory of derivatives and partial derivatives is
|
||||
provided. Arden's lemma and finiteness of partial derivatives is
|
||||
established. A simple regular expression matcher based on Brozowski's
|
||||
derivatives is proved to be correct. An executable equivalence checker for
|
||||
regular expressions is verified; it does not need automata but works directly
|
||||
on regular expressions. By mapping regular expressions to binary relations, an
|
||||
automatic and complete proof method for (in)equalities of binary relations
|
||||
over union, concatenation and (reflexive) transitive closure is obtained.
|
||||
|
||||
For an exposition of the equivalence checker for regular and relation
|
||||
algebraic expressions see the paper by Krauss and Nipkow~\cite{KraussN-JAR}.
|
||||
|
||||
Extended regular expressions with complement and intersection
|
||||
are also defined and an equivalence checker is provided.
|
||||
\end{abstract}
|
||||
|
||||
\tableofcontents
|
||||
|
||||
% include generated text of all theories
|
||||
\input{session}
|
||||
|
||||
\bibliographystyle{abbrv}
|
||||
\bibliography{root}
|
||||
|
||||
\end{document}
|
|
@ -0,0 +1,306 @@
|
|||
section \<open>Deciding Regular Expression Equivalence (2)\<close>
|
||||
|
||||
theory pEquivalence_Checking
|
||||
imports Equivalence_Checking Derivatives
|
||||
begin
|
||||
|
||||
text\<open>\noindent Similar to theory @{theory "Regular-Sets.Equivalence_Checking"}, but
|
||||
with partial derivatives instead of derivatives.\<close>
|
||||
|
||||
text\<open>Lifting many notions to sets:\<close>
|
||||
|
||||
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) \<subseteq> atoms r"
|
||||
apply (induct r)
|
||||
apply (auto simp: Atoms_def UN_subset_iff)
|
||||
apply (fastforce)+
|
||||
done
|
||||
|
||||
lemma Atoms_Pderiv: "Atoms(Pderiv a R) \<subseteq> Atoms R"
|
||||
using Atoms_pderiv by (fastforce simp: Atoms_def Pderiv_def)
|
||||
|
||||
lemma pderiv_no_occurrence:
|
||||
"x \<notin> atoms r \<Longrightarrow> pderiv x r = {}"
|
||||
by (induct r) auto
|
||||
|
||||
lemma Pderiv_no_occurrence:
|
||||
"x \<notin> Atoms R \<Longrightarrow> 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 \<Rightarrow> 'a Rexp_pairs \<Rightarrow> bool"
|
||||
where
|
||||
"is_Bisimulation as ps =
|
||||
(\<forall>(R,S)\<in> set ps. Atoms R \<union> Atoms S \<subseteq> set as \<and>
|
||||
(Nullable R \<longleftrightarrow> Nullable S) \<and>
|
||||
(\<forall>a\<in>set as. (Pderiv a R, Pderiv a S) \<in> set ps))"
|
||||
|
||||
lemma Bisim_Lang_eq:
|
||||
assumes Bisim: "is_Bisimulation as ps"
|
||||
assumes "(R, S) \<in> set ps"
|
||||
shows "Lang R = Lang S"
|
||||
proof -
|
||||
define ps' where "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 = "\<lambda>K L. (\<exists>(R,S)\<in>set ps'. K = Lang R \<and> L = Lang S)"
|
||||
show ?thesis
|
||||
proof (rule language_coinduct[where R="?R"])
|
||||
from \<open>(R,S) \<in> set ps\<close>
|
||||
have "(R,S) \<in> 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) \<in> set ps'"
|
||||
and KL: "K = Lang R" "L = Lang S" by auto
|
||||
with Bisim' have "Nullable R \<longleftrightarrow> Nullable S"
|
||||
by (auto simp: is_Bisimulation_def)
|
||||
thus "[] \<in> K \<longleftrightarrow> [] \<in> 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 \<in> set as"
|
||||
with rs Bisim'
|
||||
have "(Pderiv a R, Pderiv a S) \<in> set ps'"
|
||||
by (auto simp: is_Bisimulation_def)
|
||||
thus ?thesis by (fastforce simp: KL Deriv_Lang)
|
||||
next
|
||||
assume "a \<notin> set as"
|
||||
with Bisim' rs
|
||||
have "a \<notin> Atoms R \<union> 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 \<open>Closure computation\<close>
|
||||
|
||||
fun test :: "'a Rexp_pairs * 'a Rexp_pairs \<Rightarrow> bool" where
|
||||
"test (ws, ps) = (case ws of [] \<Rightarrow> False | (R,S)#_ \<Rightarrow> Nullable R = Nullable S)"
|
||||
|
||||
fun step :: "'a list \<Rightarrow>
|
||||
'a Rexp_pairs * 'a Rexp_pairs \<Rightarrow> 'a Rexp_pairs * 'a Rexp_pairs"
|
||||
where "step as (ws,ps) =
|
||||
(let
|
||||
(R,S) = hd ws;
|
||||
ps' = (R,S) # ps;
|
||||
succs = map (\<lambda>a. (Pderiv a R, Pderiv a S)) as;
|
||||
new = filter (\<lambda>p. p \<notin> set ps \<union> set ws) succs
|
||||
in (remdups new @ tl ws, ps'))"
|
||||
|
||||
definition closure ::
|
||||
"'a list \<Rightarrow> 'a Rexp_pairs * 'a Rexp_pairs
|
||||
\<Rightarrow> ('a Rexp_pairs * 'a Rexp_pairs) option" where
|
||||
"closure as = while_option test (step as)"
|
||||
|
||||
definition pre_Bisim :: "'a list \<Rightarrow> 'a rexp set \<Rightarrow> 'a rexp set \<Rightarrow>
|
||||
'a Rexp_pairs * 'a Rexp_pairs \<Rightarrow> bool"
|
||||
where
|
||||
"pre_Bisim as R S = (\<lambda>(ws,ps).
|
||||
((R,S) \<in> set ws \<union> set ps) \<and>
|
||||
(\<forall>(R,S)\<in> set ws \<union> set ps. Atoms R \<union> Atoms S \<subseteq> set as) \<and>
|
||||
(\<forall>(R,S)\<in> set ps. (Nullable R \<longleftrightarrow> Nullable S) \<and>
|
||||
(\<forall>a\<in>set as. (Pderiv a R, Pderiv a S) \<in> set ps \<union> set ws)))"
|
||||
|
||||
lemma step_set_eq: "\<lbrakk> test (ws,ps); step as (ws,ps) = (ws',ps') \<rbrakk>
|
||||
\<Longrightarrow> set ws' \<union> set ps' =
|
||||
set ws \<union> set ps
|
||||
\<union> (\<Union>a\<in>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 \<union> Atoms S \<subseteq> set as"
|
||||
shows "Lang R = Lang S"
|
||||
proof-
|
||||
{ fix st
|
||||
have "pre_Bisim as R S st \<Longrightarrow> test st \<Longrightarrow> 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 \<open>test st\<close> obtain wstl R S where [simp]: "ws = (R,S)#wstl"
|
||||
by (auto split: list.splits)
|
||||
from \<open>step as st = (ws',ps')\<close> obtain P where [simp]: "ps' = (R,S) # ps"
|
||||
and [simp]: "ws' = remdups(filter P (map (\<lambda>a. (Pderiv a R, Pderiv a S)) as)) @ wstl"
|
||||
by auto
|
||||
have "\<forall>(R',S')\<in>set wstl \<union> set ps'. Atoms R' \<union> Atoms S' \<subseteq> set as"
|
||||
using prems(4) by auto
|
||||
moreover
|
||||
have "\<forall>a\<in>set as. Atoms(Pderiv a R) \<union> Atoms(Pderiv a S) \<subseteq> 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) \<in> set ps"
|
||||
by (auto simp: pre_Bisim_def is_Bisimulation_def)
|
||||
thus "Lang R = Lang S" by (rule Bisim_Lang_eq)
|
||||
qed
|
||||
|
||||
|
||||
subsection \<open>The overall procedure\<close>
|
||||
|
||||
definition check_eqv :: "'a rexp \<Rightarrow> 'a rexp \<Rightarrow> bool"
|
||||
where
|
||||
"check_eqv r s =
|
||||
(case closure (add_atoms r (add_atoms s [])) ([({r}, {s})], []) of
|
||||
Some([],_) \<Rightarrow> True | _ \<Rightarrow> 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\<open>Test:\<close>
|
||||
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 \<subseteq> PDERIVS R"
|
||||
apply(auto simp add: PDERIVS_def pderivs_lang_def)
|
||||
by (metis pderivs.simps(1) insertI1)
|
||||
|
||||
lemma Pderiv_PDERIVS: assumes "R' \<subseteq> PDERIVS R" shows "Pderiv a R' \<subseteq> 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 \<open>r' : R'\<close> \<open>R' \<subseteq> PDERIVS R\<close> obtain s w where "s : R" "r' : pderivs w s"
|
||||
by(auto simp: PDERIVS_def pderivs_lang_def)
|
||||
hence "r \<in> pderivs (w @ [a]) s" using \<open>r : pderiv a r'\<close> by(auto simp add:pderivs_snoc)
|
||||
thus "r : PDERIVS R" using \<open>s : R\<close> by(auto simp: PDERIVS_def pderivs_lang_def)
|
||||
qed
|
||||
|
||||
lemma finite_PDERIVS: "finite R \<Longrightarrow> finite(PDERIVS R)"
|
||||
by(simp add: PDERIVS_def finite_pderivs_lang_UNIV)
|
||||
|
||||
lemma closure_Some: assumes "finite R0" "finite S0" shows "\<exists>p. closure as ([(R0,S0)],[]) = Some p"
|
||||
proof(unfold closure_def)
|
||||
let ?Inv = "%(ws,bs). distinct ws \<and> (ALL (R,S) : set ws. R \<subseteq> PDERIVS R0 \<and> S \<subseteq> PDERIVS S0 \<and> (R,S) \<notin> set bs)"
|
||||
let ?m1 = "%bs. Pow(PDERIVS R0) \<times> 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 \<open>test s\<close> 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 (\<lambda>a. (Pderiv a R, Pderiv a S)) as"
|
||||
let ?new = "filter (\<lambda>p. p \<notin> set bs \<union> set ws) ?succs"
|
||||
let ?ws' = "remdups ?new @ ws'"
|
||||
have *: "?Inv (step as s)"
|
||||
proof -
|
||||
from \<open>?Inv s\<close> have "distinct ?ws'" by auto
|
||||
have "ALL (R,S) : set ?ws'. R \<subseteq> PDERIVS R0 \<and> S \<subseteq> PDERIVS S0 \<and> (R,S) \<notin> set ?bs'" using \<open>?Inv s\<close>
|
||||
by(simp add: Ball_def image_iff) (metis Pderiv_PDERIVS)
|
||||
with \<open>distinct ?ws'\<close> 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 \<open>?Inv s\<close>
|
||||
by(auto intro: psubset_card_mono[OF \<open>finite(?m1 bs)\<close>])
|
||||
then show ?thesis using \<open>?Inv s\<close> by simp
|
||||
qed
|
||||
note * and this
|
||||
} note step = this
|
||||
show "\<exists>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 "\<forall>(R,S)\<in>set(fst p). \<exists>w. R = pderivs w r \<and> 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 \<open>test p\<close> obtain R S ws' where [simp]: "ws = (R,S)#ws'"
|
||||
by(auto split: prod.splits list.splits)
|
||||
let ?succs = "map (\<lambda>a. (Pderiv a R, Pderiv a S)) as"
|
||||
let ?new = "filter (\<lambda>p. p \<notin> set bs \<union> set ws) ?succs"
|
||||
let ?ws' = "remdups ?new @ ws'"
|
||||
from \<open>?Inv p\<close> 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 \<and> Pderiv x S = pderivs w s"
|
||||
by(rule_tac x="w@[x]" in exI)(simp add: pderivs_append Pderiv_def)
|
||||
}
|
||||
with \<open>?Inv p\<close> 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 "\<not> ?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 \<Longrightarrow> check_eqv r s"
|
||||
by(auto simp add: check_eqv_def dest!: closure_complete
|
||||
split: option.split list.split)
|
||||
|
||||
end
|
Binary file not shown.
Binary file not shown.
Binary file not shown.
|
@ -174,15 +174,6 @@ val is_black_comment = Token.is_formal_comment;
|
|||
|
||||
(* presentation tokens *)
|
||||
|
||||
(* orig Isabelle 2018
|
||||
datatype token =
|
||||
Ignore_Token
|
||||
| Basic_Token of Token.T
|
||||
| Markup_Token of string * Input.source
|
||||
| Markup_Env_Token of string * Input.source
|
||||
| Raw_Token of Input.source;
|
||||
*)
|
||||
|
||||
datatype token =
|
||||
Ignore_Token
|
||||
| Basic_Token of Token.T
|
||||
|
@ -198,46 +189,20 @@ val white_comment_token = basic_token is_white_comment;
|
|||
val blank_token = basic_token Token.is_blank;
|
||||
val newline_token = basic_token Token.is_newline;
|
||||
|
||||
(* orig Isabelle 2018
|
||||
fun present_token ctxt tok =
|
||||
(case tok of
|
||||
Ignore_Token => []
|
||||
| Basic_Token tok => output_token ctxt tok
|
||||
| Markup_Token (cmd, source) =>
|
||||
Latex.enclose_body ("%\n\\isamarkup" ^ cmd ^ "{") "%\n}\n"
|
||||
(output_document ctxt {markdown = false} source)
|
||||
| Markup_Env_Token (cmd, source) =>
|
||||
[Latex.environment_block ("isamarkup" ^ cmd) (output_document ctxt {markdown = true} source)]
|
||||
| Raw_Token source =>
|
||||
Latex.string "%\n" :: output_document ctxt {markdown = true} source @ [Latex.string "\n"]);
|
||||
|
||||
*)
|
||||
|
||||
(* modified by bu: added meta_args; currently ignored*)
|
||||
fun present_token ctxt tok =
|
||||
(case tok of
|
||||
Ignore_Token => []
|
||||
| Basic_Token tok => output_token ctxt tok
|
||||
| Markup_Token (cmd, meta_args, source) =>
|
||||
Latex.enclose_body ("%\n\\isamarkup" ^ cmd ^ "{") "%\n}\n"
|
||||
Latex.enclose_body ("%\n\\isamarkup" ^ cmd ^ meta_args ^ "{") "%\n}\n"
|
||||
(output_document ctxt {markdown = false} source)
|
||||
| Markup_Env_Token (cmd, meta_args,source) =>
|
||||
[Latex.environment_block ("isamarkup" ^ cmd) (output_document ctxt {markdown = true} source)]
|
||||
| Raw_Token source =>
|
||||
Latex.string "%\n" :: output_document ctxt {markdown = true} source @ [Latex.string "\n"]);
|
||||
(*
|
||||
fun output_token state tok =
|
||||
(case tok of
|
||||
No_Token => ""
|
||||
| Basic_Token tok => Latex.output_token tok
|
||||
| Markup_Token (cmd, meta_args, source) =>
|
||||
"%\n\\isamarkup" ^ cmd ^ meta_args ^ "{" ^ output_text state {markdown = false} source ^ "%\n}\n"
|
||||
| Markup_Env_Token (cmd, meta_args, source) =>
|
||||
Latex.environment ("isamarkup" ^ cmd)
|
||||
(meta_args ^ output_text state {markdown = true} source)
|
||||
[Latex.environment_block
|
||||
("isamarkup" ^ cmd)
|
||||
(Latex.string meta_args :: output_document ctxt {markdown = true} source)]
|
||||
| Raw_Token source =>
|
||||
"%\n" ^ output_text state {markdown = true} source ^ "\n");
|
||||
*)
|
||||
Latex.string "%\n" :: output_document ctxt {markdown = true} source @ [Latex.string "\n"]);
|
||||
|
||||
|
||||
(* command spans *)
|
||||
|
||||
|
@ -401,8 +366,12 @@ val locale =
|
|||
Scan.option ((Parse.$$$ "(" -- improper -- Parse.$$$ "in") |--
|
||||
Parse.!!! (improper |-- Parse.name --| (improper -- Parse.$$$ ")")));
|
||||
|
||||
<<<<<<< HEAD
|
||||
val meta_args_parser_hook = Synchronized.var "meta args parder hook"
|
||||
((fn thy => fn s => ("",s)): theory -> string parser);
|
||||
=======
|
||||
val meta_args_parser_hook = Unsynchronized.ref ((fn thy => fn s => ("",s)): theory -> string parser)
|
||||
>>>>>>> d2e5bea25a311ff8210d30366b61b78bd7056efe
|
||||
|
||||
|
||||
in
|
||||
|
@ -411,7 +380,10 @@ type segment = {span: Command_Span.span, command: Toplevel.transition, state: To
|
|||
|
||||
fun present_thy options thy (segments: segment list) =
|
||||
let
|
||||
<<<<<<< HEAD
|
||||
|
||||
=======
|
||||
>>>>>>> d2e5bea25a311ff8210d30366b61b78bd7056efe
|
||||
val keywords = Thy_Header.get_keywords thy;
|
||||
|
||||
|
||||
|
@ -420,30 +392,22 @@ fun present_thy options thy (segments: segment list) =
|
|||
val ignored = Scan.state --| ignore
|
||||
>> (fn d => (NONE, (Ignore_Token, ("", d))));
|
||||
|
||||
(* orig Isabelle 2018
|
||||
fun markup pred mk flag = Scan.peek (fn d =>
|
||||
improper |--
|
||||
Parse.position (Scan.one (fn tok =>
|
||||
Token.is_command tok andalso pred keywords (Token.content_of tok))) --
|
||||
Scan.repeat tag --
|
||||
Parse.!!!! ((improper -- locale -- improper) |-- Parse.document_source --| improper_end)
|
||||
>> (fn (((tok, pos'), tags), source) =>
|
||||
let val name = Token.content_of tok
|
||||
in (SOME (name, pos', tags), (mk (name, source), (flag, d))) end));
|
||||
*)
|
||||
|
||||
fun markup pred mk flag = Scan.peek (fn d =>
|
||||
improper |--
|
||||
Parse.position (Scan.one (fn tok => Token.is_command tok andalso
|
||||
pred keywords (Token.content_of tok))) --
|
||||
Scan.repeat tag --
|
||||
(improper |--
|
||||
(Parse.!!!!
|
||||
<<<<<<< HEAD
|
||||
( (Synchronized.value meta_args_parser_hook thy)
|
||||
=======
|
||||
((!meta_args_parser_hook thy)
|
||||
>>>>>>> d2e5bea25a311ff8210d30366b61b78bd7056efe
|
||||
-- ( (improper -- locale -- improper)
|
||||
|-- (Parse.document_source))
|
||||
--| improper_end)))
|
||||
>> (fn (((tok, pos'), tags), (meta_args,source)) =>
|
||||
>> (fn (((tok, pos'), tags), (meta_args, source)) =>
|
||||
let val name = Token.content_of tok
|
||||
in (SOME (name, pos', tags), (mk (name, meta_args, source), (flag, d))) end));
|
||||
|
||||
|
@ -458,13 +422,6 @@ fun present_thy options thy (segments: segment list) =
|
|||
val cmt = Scan.peek (fn d =>
|
||||
Scan.one is_black_comment >> (fn tok => (NONE, (Basic_Token tok, ("", d)))));
|
||||
|
||||
(* from 17 - necessary in 18 ?
|
||||
val cmt = Scan.peek (fn d =>
|
||||
(Parse.$$$ "--" || Parse.$$$ Symbol.comment) |--
|
||||
Parse.!!!! (improper |-- Parse.document_source) >>
|
||||
(fn source => (NONE, (Markup_Token ("cmt", "", source), ("", d)))));
|
||||
*)
|
||||
|
||||
val other = Scan.peek (fn d =>
|
||||
Parse.not_eof >> (fn tok => (NONE, (Basic_Token tok, ("", d)))));
|
||||
|
||||
|
@ -521,7 +478,8 @@ fun present_thy options thy (segments: segment list) =
|
|||
Toplevel.setmp_thread_position tr (present_span thy command_tag span st st');
|
||||
|
||||
fun present _ [] = I
|
||||
| present st ((span, (tr, st')) :: rest) = present_command tr span st st' #> present st' rest;
|
||||
| present st ((span, (tr, st')) :: rest) = present_command tr span st st'
|
||||
#> present st' rest;
|
||||
|
||||
in
|
||||
if length command_results = length spans then
|
||||
|
|
Loading…
Reference in New Issue