theory Matcher3simple
imports "Main"
begin
section {* Sequential Composition of Sets *}
definition
Sequ :: "string set \<Rightarrow> string set \<Rightarrow> string set" ("_ ;; _" [100,100] 100)
where
"A ;; B = {s1 @ s2 | s1 s2. s1 \<in> A \<and> s2 \<in> B}"
text {* Two Simple Properties about Sequential Composition *}
lemma seq_empty [simp]:
shows "A ;; {[]} = A"
and "{[]} ;; A = A"
by (simp_all add: Sequ_def)
lemma seq_null [simp]:
shows "A ;; {} = {}"
and "{} ;; A = {}"
by (simp_all add: Sequ_def)
section {* Regular Expressions *}
datatype rexp =
NULL
| EMPTY
| CHAR char
| SEQ rexp rexp
| ALT rexp rexp
section {* Semantics of Regular Expressions *}
fun
L :: "rexp \<Rightarrow> string set"
where
"L (NULL) = {}"
| "L (EMPTY) = {[]}"
| "L (CHAR c) = {[c]}"
| "L (SEQ r1 r2) = (L r1) ;; (L r2)"
| "L (ALT r1 r2) = (L r1) \<union> (L r2)"
datatype val =
Void
| Char char
| Seq val val
| Right val
| Left val
inductive Prf :: "val \<Rightarrow> rexp \<Rightarrow> bool" ("\<turnstile> _ : _" [100, 100] 100)
where
"\<lbrakk>\<turnstile> v1 : r1; \<turnstile> v2 : r2\<rbrakk> \<Longrightarrow> \<turnstile> Seq v1 v2 : SEQ r1 r2"
| "\<turnstile> v1 : r1 \<Longrightarrow> \<turnstile> Left v1 : ALT r1 r2"
| "\<turnstile> v2 : r2 \<Longrightarrow> \<turnstile> Right v2 : ALT r1 r2"
| "\<turnstile> Void : EMPTY"
| "\<turnstile> Char c : CHAR c"
fun flat :: "val \<Rightarrow> string"
where
"flat(Void) = []"
| "flat(Char c) = [c]"
| "flat(Left v) = flat(v)"
| "flat(Right v) = flat(v)"
| "flat(Seq v1 v2) = flat(v1) @ flat(v2)"
datatype tree =
Leaf string
| Branch tree tree
fun flats :: "val \<Rightarrow> tree"
where
"flats(Void) = Leaf []"
| "flats(Char c) = Leaf [c]"
| "flats(Left v) = flats(v)"
| "flats(Right v) = flats(v)"
| "flats(Seq v1 v2) = Branch (flats v1) (flats v2)"
fun flatten :: "tree \<Rightarrow> string"
where
"flatten (Leaf s) = s"
| "flatten (Branch t1 t2) = flatten t1 @ flatten t2"
lemma flats_flat:
shows "flat v1 = flatten (flats v1)"
apply(induct v1)
apply(simp_all)
done
lemma Prf_flat_L:
assumes "\<turnstile> v : r" shows "flat v \<in> L r"
using assms
apply(induct)
apply(auto simp add: Sequ_def)
done
lemma L_flat_Prf:
"L(r) = {flat v | v. \<turnstile> v : r}"
apply(induct r)
apply(auto dest: Prf_flat_L simp add: Sequ_def)
apply (metis Prf.intros(4) flat.simps(1))
apply (metis Prf.intros(5) flat.simps(2))
apply (metis Prf.intros(1) flat.simps(5))
apply (metis Prf.intros(2) flat.simps(3))
apply (metis Prf.intros(3) flat.simps(4))
by (smt Prf.cases flat.simps(3) flat.simps(4) rexp.distinct(13) rexp.distinct(17) rexp.distinct(19) rexp.inject(3))
inductive ValOrd :: "val \<Rightarrow> rexp \<Rightarrow> val \<Rightarrow> bool" ("_ \<succ>_ _" [100, 100, 100] 100)
where
"\<lbrakk>v1 \<succ>r1 v1'; v2 \<succ>r2 v2'\<rbrakk> \<Longrightarrow> (Seq v1 v2) \<succ>(SEQ r1 r2) (Seq v1' v2')"
| "length (flat v1) \<ge> length (flat v2) \<Longrightarrow> (Left v1) \<succ>(ALT r1 r2) (Right v2)"
| "length (flat v2) > length (flat v1) \<Longrightarrow> (Right v2) \<succ>(ALT r1 r2) (Left v1)"
| "v2 \<succ>r2 v2' \<Longrightarrow> (Right v2) \<succ>(ALT r1 r2) (Right v2')"
| "v1 \<succ>r1 v1' \<Longrightarrow> (Left v1) \<succ>(ALT r1 r2) (Left v1')"
| "Void \<succ>EMPTY Void"
| "(Char c) \<succ>(CHAR c) (Char c)"
lemma
assumes "r = SEQ (ALT EMPTY EMPTY) (ALT EMPTY (CHAR c))"
shows "(Seq (Left Void) (Right (Char c))) \<succ>r (Seq (Left Void) (Left Void))"
using assms
apply(simp)
apply(rule ValOrd.intros)
apply(rule ValOrd.intros)
apply(rule ValOrd.intros)
apply(rule ValOrd.intros)
apply(simp)
done
definition POSIX :: "val \<Rightarrow> rexp \<Rightarrow> bool"
where
"POSIX v r \<equiv> (\<forall>v'. (\<turnstile> v' : r \<and> flats v = flats v') \<longrightarrow> v \<succ>r v')"
lemma POSIX:
assumes "r = SEQ (ALT EMPTY EMPTY) (ALT EMPTY (CHAR c))"
shows "POSIX (Seq (Left Void) (Right (Char c))) r"
apply(simp add: POSIX_def assms)
apply(auto)
apply(erule Prf.cases)
apply(simp_all)
apply(rule ValOrd.intros)
apply (smt POSIX_def Prf.cases Prf.simps ValOrd.intros(2) ValOrd.intros(5) ValOrd.intros(6) flats.simps(1) flats.simps(3) rexp.distinct(11) rexp.distinct(13) rexp.distinct(17) rexp.distinct(19) rexp.distinct(9) rexp.inject(3) val.distinct(19) val.inject(3))
by (smt Prf.simps ValOrd.intros(4) ValOrd.intros(7) flats.simps(1) flats.simps(3) list.distinct(1) rexp.distinct(11) rexp.distinct(13) rexp.distinct(15) rexp.distinct(17) rexp.distinct(19) rexp.distinct(9) rexp.inject(1) rexp.inject(3) tree.inject(1))
lemma Exists_POSIX: "\<exists>v. POSIX v r"
apply(induct r)
apply(auto simp add: POSIX_def)
apply(rule exI)
apply(auto)
apply(erule Prf.cases)
apply(simp_all)[5]
apply (smt Prf.simps ValOrd.intros(6) rexp.distinct(11) rexp.distinct(13) rexp.distinct(9))
apply(rule exI)
apply(auto)
apply(erule Prf.cases)
apply(simp_all)[5]
apply(rule ValOrd.intros)
apply(rule exI)
apply(auto)
apply(erule Prf.cases)
apply(simp_all)[5]
apply(rule ValOrd.intros)
apply(auto)[2]
apply(rule_tac x="Left v" in exI)
apply(auto)
apply(erule Prf.cases)
apply(simp_all)[5]
apply(rule ValOrd.intros)
apply(auto)[1]
apply(auto)
apply(rule ValOrd.intros)
by (metis flats_flat order_refl)
lemma POSIX_SEQ:
assumes "POSIX (Seq v1 v2) (SEQ r1 r2)" "\<turnstile> v1 : r1" "\<turnstile> v2 : r2"
shows "POSIX v1 r1 \<and> POSIX v2 r2"
using assms
unfolding POSIX_def
apply(auto)
apply(drule_tac x="Seq v' v2" in spec)
apply(simp)
apply (smt Prf.intros(1) ValOrd.simps assms(3) rexp.inject(2) val.distinct(15) val.distinct(17) val.distinct(3) val.distinct(9) val.inject(2))
apply(drule_tac x="Seq v1 v'" in spec)
apply(simp)
by (smt Prf.intros(1) ValOrd.simps rexp.inject(2) val.distinct(15) val.distinct(17) val.distinct(3) val.distinct(9) val.inject(2))
lemma POSIX_SEQ_I:
assumes "POSIX v1 r1" "POSIX v2 r2"
shows "POSIX (Seq v1 v2) (SEQ r1 r2)"
using assms
unfolding POSIX_def
apply(auto)
apply(rotate_tac 4)
apply(erule Prf.cases)
apply(simp_all)[5]
apply(auto)[1]
apply(rule ValOrd.intros)
apply(auto)
done
lemma POSIX_ALT:
assumes "POSIX (Left v1) (ALT r1 r2)"
shows "POSIX v1 r1"
using assms
unfolding POSIX_def
apply(auto)
apply(drule_tac x="Left v'" in spec)
apply(simp)
apply(drule mp)
apply(rule Prf.intros)
apply(auto)
apply(erule ValOrd.cases)
apply(simp_all)[7]
done
lemma POSIX_ALT1a:
assumes "POSIX (Right v2) (ALT r1 r2)"
shows "POSIX v2 r2"
using assms
unfolding POSIX_def
apply(auto)
apply(drule_tac x="Right v'" in spec)
apply(simp)
apply(drule mp)
apply(rule Prf.intros)
apply(auto)
apply(erule ValOrd.cases)
apply(simp_all)[7]
done
lemma POSIX_ALT1b:
assumes "POSIX (Right v2) (ALT r1 r2)"
shows "(\<forall>v'. (\<turnstile> v' : r2 \<and> flats v' = flats v2) \<longrightarrow> v2 \<succ>r2 v')"
using assms
apply(drule_tac POSIX_ALT1a)
unfolding POSIX_def
apply(auto)
done
lemma POSIX_ALT_I1:
assumes "POSIX v1 r1"
shows "POSIX (Left v1) (ALT r1 r2)"
using assms
unfolding POSIX_def
apply(auto)
apply(rotate_tac 3)
apply(erule Prf.cases)
apply(simp_all)[5]
apply(auto)
apply(rule ValOrd.intros)
apply(auto)
apply(rule ValOrd.intros)
by (metis flats_flat order_refl)
lemma POSIX_ALT_I2:
assumes "POSIX v2 r2" "\<forall>v'. \<turnstile> v' : r1 \<longrightarrow> length (flat v2) > length (flat v')"
shows "POSIX (Right v2) (ALT r1 r2)"
using assms
unfolding POSIX_def
apply(auto)
apply(rotate_tac 3)
apply(erule Prf.cases)
apply(simp_all)[5]
apply(auto)
prefer 2
apply(rule ValOrd.intros)
apply metis
apply(rule ValOrd.intros)
apply(auto)
done
lemma ValOrd_refl:
assumes "\<turnstile> v : r"
shows "v \<succ>r v"
using assms
apply(induct)
apply(auto intro: ValOrd.intros)
done
lemma ValOrd_length:
assumes "v1 \<succ>r v2" shows "length (flat v1) \<ge> length (flat v2)"
using assms
apply(induct)
apply(auto)
done
section {* The Matcher *}
fun
nullable :: "rexp \<Rightarrow> bool"
where
"nullable (NULL) = False"
| "nullable (EMPTY) = True"
| "nullable (CHAR c) = False"
| "nullable (ALT r1 r2) = (nullable r1 \<or> nullable r2)"
| "nullable (SEQ r1 r2) = (nullable r1 \<and> nullable r2)"
lemma nullable_correctness:
shows "nullable r \<longleftrightarrow> [] \<in> (L r)"
apply (induct r)
apply(auto simp add: Sequ_def)
done
fun mkeps :: "rexp \<Rightarrow> val"
where
"mkeps(EMPTY) = Void"
| "mkeps(SEQ r1 r2) = Seq (mkeps r1) (mkeps r2)"
| "mkeps(ALT r1 r2) = (if nullable(r1) then Left (mkeps r1) else Right (mkeps r2))"
lemma mkeps_nullable:
assumes "nullable(r)" shows "\<turnstile> mkeps r : r"
using assms
apply(induct rule: nullable.induct)
apply(auto intro: Prf.intros)
done
lemma mkeps_flat:
assumes "nullable(r)" shows "flat (mkeps r) = []"
using assms
apply(induct rule: nullable.induct)
apply(auto)
done
lemma mkeps_flats:
assumes "nullable(r)" shows "flatten (flats (mkeps r)) = []"
using assms
apply(induct rule: nullable.induct)
apply(auto)
done
lemma mkeps_POSIX:
assumes "nullable r"
shows "POSIX (mkeps r) r"
using assms
apply(induct r)
apply(auto)
apply(simp add: POSIX_def)
apply(auto)[1]
apply(erule Prf.cases)
apply(simp_all)[5]
apply (metis ValOrd.intros(6))
apply(simp add: POSIX_def)
apply(auto)[1]
apply(erule Prf.cases)
apply(simp_all)[5]
apply(auto)
apply (metis ValOrd.intros(1) append_is_Nil_conv mkeps_flat)
apply(simp add: POSIX_def)
apply(auto)[1]
apply(erule Prf.cases)
apply(simp_all)[5]
apply(auto)
apply (metis ValOrd.intros(5))
apply(rule ValOrd.intros(2))
apply(simp add: mkeps_flat)
apply(simp add: flats_flat)
apply (metis mkeps_flats)
apply(simp add: POSIX_def)
apply(auto)[1]
apply(erule Prf.cases)
apply(simp_all)[5]
apply(auto)
apply (metis ValOrd.intros(5))
apply (smt ValOrd.intros(2) flats_flat)
apply(simp add: POSIX_def)
apply(auto)[1]
apply(erule Prf.cases)
apply(simp_all)[5]
apply (metis Prf_flat_L flats_flat mkeps_flats nullable_correctness)
by (metis ValOrd.intros(4))
fun
der :: "char \<Rightarrow> rexp \<Rightarrow> rexp"
where
"der c (NULL) = NULL"
| "der c (EMPTY) = NULL"
| "der c (CHAR c') = (if c = c' then EMPTY else NULL)"
| "der c (ALT r1 r2) = ALT (der c r1) (der c r2)"
| "der c (SEQ r1 r2) =
(if nullable r1
then ALT (SEQ (der c r1) r2) (der c r2)
else SEQ (der c r1) r2)"
fun
ders :: "string \<Rightarrow> rexp \<Rightarrow> rexp"
where
"ders [] r = r"
| "ders (c # s) r = ders s (der c r)"
fun injval :: "rexp \<Rightarrow> char \<Rightarrow> val \<Rightarrow> val"
where
"injval (CHAR d) c Void = Char d"
| "injval (ALT r1 r2) c (Left v1) = Left(injval r1 c v1)"
| "injval (ALT r1 r2) c (Right v2) = Right(injval r2 c v2)"
| "injval (SEQ r1 r2) c (Seq v1 v2) = Seq (injval r1 c v1) v2"
| "injval (SEQ r1 r2) c (Left (Seq v1 v2)) = Seq (injval r1 c v1) v2"
| "injval (SEQ r1 r2) c (Right v2) = Seq (mkeps r1) (injval r2 c v2)"
fun projval :: "rexp \<Rightarrow> char \<Rightarrow> val \<Rightarrow> val"
where
"projval (CHAR d) c _ = Void"
| "projval (ALT r1 r2) c (Left v1) = Left(projval r1 c v1)"
| "projval (ALT r1 r2) c (Right v2) = Right(projval r2 c v2)"
| "projval (SEQ r1 r2) c (Seq v1 v2) =
(if flat v1 = [] then Right(projval r2 c v2)
else if nullable r1 then Left (Seq (projval r1 c v1) v2)
else Seq (projval r1 c v1) v2)"
lemma v3:
assumes "\<turnstile> v : der c r" shows "\<turnstile> (injval r c v) : r"
using assms
apply(induct arbitrary: v rule: der.induct)
apply(simp)
apply(erule Prf.cases)
apply(simp_all)[5]
apply(erule Prf.cases)
apply(simp_all)[5]
apply(case_tac "c = c'")
apply(simp)
apply(erule Prf.cases)
apply(simp_all)[5]
apply (metis Prf.intros(5))
apply(erule Prf.cases)
apply(simp_all)[5]
apply(erule Prf.cases)
apply(simp_all)[5]
apply (metis Prf.intros(2))
apply (metis Prf.intros(3))
apply(simp)
apply(case_tac "nullable r1")
apply(simp)
apply(erule Prf.cases)
apply(simp_all)[5]
apply(auto)[1]
apply(erule Prf.cases)
apply(simp_all)[5]
apply(auto)[1]
apply (metis Prf.intros(1))
apply(auto)[1]
apply (metis Prf.intros(1) mkeps_nullable)
apply(simp)
apply(erule Prf.cases)
apply(simp_all)[5]
apply(auto)[1]
apply(rule Prf.intros)
apply(auto)[2]
done
fun head where
"head [] = None"
| "head (x#xs) = Some x"
lemma head1:
assumes "head (xs @ ys) = Some x"
shows "(head xs = Some x) \<or> (xs = [] \<and> head ys = Some x)"
using assms
apply(induct xs)
apply(auto)
done
lemma head2:
assumes "head (xs @ ys) = None"
shows "(head xs = None) \<and> (head ys = None)"
using assms
apply(induct xs)
apply(auto)
done
lemma v4:
assumes "\<turnstile> v : der c r" shows "flat (injval r c v) = c#(flat v)"
using assms
apply(induct arbitrary: v rule: der.induct)
apply(simp)
apply(erule Prf.cases)
apply(simp_all)[5]
apply(simp)
apply(erule Prf.cases)
apply(simp_all)[5]
apply(simp)
apply(case_tac "c = c'")
apply(simp)
apply(auto)[1]
apply(erule Prf.cases)
apply(simp_all)[5]
apply(simp)
apply(erule Prf.cases)
apply(simp_all)[5]
apply(simp)
apply(erule Prf.cases)
apply(simp_all)[5]
apply(simp)
apply(case_tac "nullable r1")
apply(simp)
apply(erule Prf.cases)
apply(simp_all)[5]
apply(auto)[1]
apply(erule Prf.cases)
apply(simp_all)[5]
apply(auto)[1]
apply (metis mkeps_flat)
apply(simp)
apply(erule Prf.cases)
apply(simp_all)[5]
done
lemma proj_inj_id:
assumes "\<turnstile> v : der c r"
shows "projval r c (injval r c v) = v"
using assms
apply(induct r arbitrary: c v rule: rexp.induct)
apply(simp)
apply(erule Prf.cases)
apply(simp_all)[5]
apply(simp)
apply(erule Prf.cases)
apply(simp_all)[5]
apply(simp)
apply(case_tac "c = char")
apply(simp)
apply(erule Prf.cases)
apply(simp_all)[5]
apply(simp)
apply(erule Prf.cases)
apply(simp_all)[5]
defer
apply(simp)
apply(erule Prf.cases)
apply(simp_all)[5]
apply(simp)
apply(case_tac "nullable rexp1")
apply(simp)
apply(erule Prf.cases)
apply(simp_all)[5]
apply(auto)[1]
apply(erule Prf.cases)
apply(simp_all)[5]
apply(auto)[1]
apply (metis list.distinct(1) v4)
apply(auto)[1]
apply (metis mkeps_flat)
apply(auto)
apply(erule Prf.cases)
apply(simp_all)[5]
apply(auto)[1]
apply(simp add: v4)
done
lemma Le_2a: "(head (flat v) = None) = (flat v = [])"
apply(induct v)
apply(simp_all)
apply (metis Nil_is_append_conv head.elims option.distinct(1))
done
lemma v5:
assumes "\<turnstile> v : der c r" "POSIX v (der c r)"
shows "POSIX (injval r c v) r"
using assms
apply(induct arbitrary: v rule: der.induct)
apply(simp)
apply(erule Prf.cases)
apply(simp_all)[5]
apply(simp)
apply(erule Prf.cases)
apply(simp_all)[5]
apply(simp)
apply(case_tac "c = c'")
apply(auto simp add: POSIX_def)[1]
apply(erule Prf.cases)
apply(simp_all)[5]
apply(erule Prf.cases)
apply(simp_all)[5]
apply (metis ValOrd.intros(7))
apply(erule Prf.cases)
apply(simp_all)[5]
prefer 2
apply(simp)
apply(case_tac "nullable r1")
apply(simp)
defer
apply(simp)
apply(erule Prf.cases)
apply(simp_all)[5]
apply(auto)[1]
apply(drule POSIX_SEQ)
apply(assumption)
apply(assumption)
apply(auto)[1]
apply(rule POSIX_SEQ_I)
apply metis
apply(simp)
apply(simp)
apply(erule Prf.cases)
apply(simp_all)[5]
apply(auto)[1]
apply(drule POSIX_ALT)
apply(rule POSIX_ALT_I1)
apply metis
defer
apply(erule Prf.cases)
apply(simp_all)[5]
apply(auto)
apply(rotate_tac 5)
apply(erule Prf.cases)
apply(simp_all)[5]
apply(auto)[1]
apply(drule POSIX_ALT)
apply(drule POSIX_SEQ)
apply(simp)
apply(simp)
apply(rule POSIX_SEQ_I)
apply metis
apply(simp)
apply(drule POSIX_ALT1a)
apply(rule POSIX_SEQ_I)
apply (metis mkeps_POSIX)
apply(metis)
apply(frule POSIX_ALT1a)
apply(rotate_tac 1)
apply(drule_tac x="v2" in meta_spec)
apply(simp)
apply(rule POSIX_ALT_I2)
apply(simp)
apply(frule POSIX_ALT1a)
apply(auto)
apply(subst v4)
apply(simp)
apply(simp)
apply(case_tac "\<exists>r. v2 \<succ>r v'")
apply (metis ValOrd_length le_neq_implies_less less_Suc_eq)
apply(auto)[1]
apply(frule_tac x="der c r2" in spec)
apply(subgoal_tac "\<not>(Right v2 \<succ>(ALT (der c r1) (der c r2)) Right v')")
prefer 2
apply(rule notI)
apply(erule ValOrd.cases)
apply(simp_all)[7]
apply(subst (asm) (1) POSIX_def)
apply(simp)
apply(subgoal_tac "(\<not> \<turnstile> Right v' : ALT (der c r1) (der c r2)) \<or> (flats v2 \<noteq> flats v')")
prefer 2
apply (metis flats.simps(4))
apply(simp)
apply(auto)[1]
apply(subst v4)
apply(simp)
apply(simp)
apply(case_tac "v2 \<succ>r1 v'")
apply (metis ValOrd_length le_neq_implies_less less_Suc_eq)
apply(
apply(drule_tac x="projval (ALT r1 r2) c v'" in spec)
apply(drule mp)
apply(auto)
apply(frule POSIX_ALT1b)
apply(auto)
apply(subst v4)
apply(simp)
apply(simp)
apply(simp add: flats_flat)
apply(rotate_tac 1)
apply(drule_tac x="v2" in meta_spec)
apply(simp)
apply(rule POSIX_ALT_I2)
apply(simp)
apply(auto)[1]
apply(subst v4)
apply(simp)
defer
apply(erule Prf.cases)
apply(simp_all)[5]
apply(auto)
apply(rotate_tac 5)
apply(erule Prf.cases)
apply(simp_all)[5]
apply(auto)[1]
apply(drule POSIX_ALT)
apply(drule POSIX_SEQ)
apply(simp)
apply(simp)
apply(rule POSIX_SEQ_I)
apply metis
apply(simp)
apply(drule POSIX_ALT1a)
apply(rule POSIX_SEQ_I)
apply (metis mkeps_POSIX)
apply metis
apply(drule_tac x="projval r1 c v'" in meta_spec)
apply(drule meta_mp)
defer
apply(drule meta_mp)
defer
apply(subst (asm) (1) POSIX_def)
apply(simp)
lemma inj_proj_id:
assumes "\<turnstile> v : r" "POSIX v r" "head (flat v) = Some c"
shows "injval r c (projval r c v) = v"
using assms
apply(induct v r arbitrary: rule: Prf.induct)
apply(simp)
apply(auto)[1]
apply(simp)
apply(frule POSIX_head)
apply(assumption)
apply(simp)
apply(drule meta_mp)
apply(frule POSIX_E1)
apply(erule Prf.cases)
apply(simp_all)[7]
apply(frule POSIX_E1)
apply(erule Prf.cases)
apply(simp_all)[7]
apply(frule POSIX_E1)
apply(erule Prf.cases)
apply(simp_all)[7]
apply(frule POSIX_E1)
defer
apply(frule POSIX_E1)
apply(erule Prf.cases)
apply(simp_all)[7]
apply(auto)[1]
apply(simp)
apply(erule Prf.cases)
apply(simp_all)[7]
apply(simp)
apply(case_tac "c = char")
apply(simp)
apply(erule Prf.cases)
apply(simp_all)[7]
apply(simp)
apply(erule Prf.cases)
apply(simp_all)[7]
lemma POSIX_head:
assumes "POSIX (Stars (v#vs)) (STAR r)" "head (flat v @ flat (Stars vs)) = Some c"
shows "head (flat v) = Some c"
using assms
apply(rule_tac ccontr)
apply(frule POSIX_E1)
apply(drule Le_1)
apply(assumption)
apply(auto)[1]
apply(auto simp add: POSIX_def)
apply(drule_tac x="Stars (v'#vs')" in spec)
apply(simp)
apply(simp add: ValOrd_eq_def)
apply(auto)
apply(erule ValOrd.cases)
apply(simp_all)
apply(auto)
using Le_2
by (metis Le_2 Le_2a head1)
lemma inj_proj_id:
assumes "\<turnstile> v : r" "POSIX v r" "head (flat v) = Some c"
shows "injval r c (projval r c v) = v"
using assms
apply(induct r arbitrary: rule: Prf.induct)
apply(simp)
apply(simp)
apply(frule POSIX_head)
apply(assumption)
apply(simp)
apply(drule meta_mp)
apply(frule POSIX_E1)
apply(erule Prf.cases)
apply(simp_all)[7]
apply(frule POSIX_E1)
apply(erule Prf.cases)
apply(simp_all)[7]
apply(frule POSIX_E1)
apply(erule Prf.cases)
apply(simp_all)[7]
apply(frule POSIX_E1)
defer
apply(frule POSIX_E1)
apply(erule Prf.cases)
apply(simp_all)[7]
apply(auto)[1]
apply(simp)
apply(erule Prf.cases)
apply(simp_all)[7]
apply(simp)
apply(case_tac "c = char")
apply(simp)
apply(erule Prf.cases)
apply(simp_all)[7]
apply(simp)
apply(erule Prf.cases)
apply(simp_all)[7]
defer
apply(simp)
apply(erule Prf.cases)
apply(simp_all)[7]
apply(simp)
apply(erule Prf.cases)
apply(simp_all)[7]
apply(auto)[1]
apply(rotate_tac 2)
apply(erule Prf.cases)
apply(simp_all)[7]
apply(case_tac "nullable rexp1")
apply(simp)
apply(erule Prf.cases)
apply(simp_all)[7]
apply(auto)[1]
apply(erule Prf.cases)
apply(simp_all)[7]
apply(auto)[1]
apply(simp add: v4)
apply(auto)[1]
apply(simp add: v2a)
apply(simp only: der.simps)
apply(simp)
apply(erule Prf.cases)
apply(simp_all)[7]
apply(auto)[1]
apply(simp add: v4)
done
lemma STAR_obtain:
assumes "\<turnstile> v : STAR r"
obtains vs where "\<turnstile> Stars vs : STAR r" and "v = Stars vs"
using assms
by (smt Prf.cases rexp.distinct(17) rexp.distinct(23) rexp.distinct(27) rexp.distinct(29))
fun first :: "val \<Rightarrow> char option"
where
"first Void = None"
| "first (Char c) = Some c"
| "first (Seq v1 v2) = (if (\<exists>c. first v1 = Some c) then first v1 else first v2)"
| "first (Right v) = first v"
| "first (Left v) = first v"
| "first (Stars []) = None"
| "first (Stars (v#vs)) = (if (\<exists>c. first v = Some c) then first v else first (Stars vs))"
lemma flat:
shows "flat v = [] \<longleftrightarrow> first v = None"
and "flat (Stars vs) = [] \<longleftrightarrow> first (Stars vs) = None"
apply(induct v and vs)
apply(auto)
done
lemma first:
shows "first v = Some c \<Longrightarrow> head (flat v @ ys) = Some c"
apply(induct arbitrary: ys rule: first.induct)
apply(auto split: if_splits simp add: flat[symmetric])
done
lemma v5:
assumes "POSIX v r" "head (flat v) = Some c"
shows "\<turnstile> projval r c v : der c r"
using assms
apply(induct r arbitrary: c v rule: rexp.induct)
prefer 6
apply(frule POSIX_E1)
apply(erule Prf.cases)
apply(simp_all)[7]
apply(rule Prf.intros)
apply(drule_tac x="c" in meta_spec)
apply(drule_tac x="va" in meta_spec)
apply(drule meta_mp)
apply(simp add: POSIX_def)
apply(auto)[1]
apply(drule_tac x="Stars (v'#vs)" in spec)
apply(simp)
apply(drule mp)
apply (metis Prf.intros(2))
apply(simp add: ValOrd_eq_def)
apply(erule disjE)
apply(simp)
apply(erule ValOrd.cases)
apply(simp_all)[10]
apply(drule_tac meta_mp)
apply(drule head1)
apply(auto)[1]
apply(simp add: POSIX_def)
apply(auto)[1]
apply(drule_tac x="Stars (va#vs)" in spec)
apply(simp)
prefer 6
apply(simp)
apply(auto split: if_splits)[1]
apply(erule Prf.cases)
apply(simp_all)[7]
apply(rule Prf.intros)
apply metis
apply(simp)
apply(erule Prf.cases)
apply(simp_all)[7]
apply(auto split: if_splits)[1]
apply(rule Prf.intros)
apply(auto split: if_splits)[1]
apply(erule Prf.cases)
apply(simp_all)[7]
apply(auto)
apply(case_tac "char = c")
apply(simp)
apply(rule Prf.intros)
apply(simp)
apply(erule Prf.cases)
apply(simp_all)[
lemma uu:
assumes ih: "\<And>v c. \<lbrakk>head (flat v) = Some c\<rbrakk> \<Longrightarrow> \<turnstile> projval rexp c v : der c rexp"
assumes "\<turnstile> Stars vs : STAR rexp"
and "first (Stars (v#vs)) = Some c"
shows "\<turnstile> projval rexp c v : der c rexp"
using assms(2,3)
apply(induct vs)
apply(simp_all)
apply(auto split: if_splits)
apply (metis first head1 ih)
apply (metis first head1 ih)
apply(auto)
lemma v5:
assumes "\<turnstile> v : r" "head (flat v) = Some c"
shows "\<turnstile> projval r c v : der c r"
using assms
apply(induct r arbitrary: v c rule: rexp.induct)
apply(simp)
apply(erule Prf.cases)
apply(simp_all)[7]
apply(erule Prf.cases)
apply(simp_all)[7]
apply(case_tac "char = c")
apply(simp)
apply(rule Prf.intros)
apply(simp)
apply(erule Prf.cases)
apply(simp_all)[7]
prefer 3
proof -
fix rexp v c vs
assume ih: "\<And>v c. \<lbrakk>\<turnstile> v : rexp; head (flat v) = Some c\<rbrakk> \<Longrightarrow> \<turnstile> projval rexp c v : der c rexp"
assume a: "head (flat (Stars vs)) = Some c"
assume b: "\<turnstile> Stars vs : STAR rexp"
have c: "first (Stars vs) = Some c \<Longrightarrow> \<turnstile> (hd vs) : rexp \<Longrightarrow> \<turnstile> projval rexp c (hd vs) : der c rexp"
using b
apply(induct arbitrary: rule: Prf.induct)
apply(simp_all)
apply(case_tac "\<exists>c. first v = Some c")
apply(auto)[1]
apply(rule ih)
apply(simp)
apply (metis append_Nil2 first)
apply(auto)[1]
apply(simp)
apply(auto split: if_splits)[1]
apply (metis append_Nil2 first ih)
apply(drule_tac x="v" in meta_spec)
apply(simp)
apply(rotate_tac 1)
apply(erule Prf.cases)
apply(simp_all)[7]
apply(drule_tac x="v" in meta_spec)
apply(simp)
using a
apply(rotate_tac 1)
apply(erule Prf.cases)
apply(simp_all)[7]
apply (metis (full_types) Prf.cases Prf.simps a b flat.simps(6) head.simps(1) list.distinct(1) list.inject option.distinct(1) rexp.distinct(17) rexp.distinct(23) rexp.distinct(27) rexp.distinct(29) val.distinct(17) val.distinct(27) val.distinct(29) val.inject(5))
apply(auto)[1]
apply(case_tac "\<exists>c. first a = Some c")
apply(auto)[1]
apply(rule ih)
apply(simp)
apply (metis append_Nil2 first ih)
apply(auto)[1]
apply(case_tac "\<exists>c. first a = Some c")
apply(auto)[1]
apply(rule ih)
apply(simp)
apply(auto)[1]
apply(erule Prf.cases)
apply(simp_all)[7]
apply (metis append_Nil2 first)
apply(simp)
apply(simp add: )
apply(simp add: flat)
apply(erule Prf.cases)
apply(simp_all)[7]
apply(rule Prf.intros)
*)
show "\<turnstile> projval (STAR rexp) c (Stars vs) : SEQ (der c rexp) (STAR rexp)"
using b a
apply -
apply(erule Prf.cases)
apply(simp_all)[7]
apply(drule head1)
apply(auto)
apply(rule Prf.intros)
apply(rule ih)
apply(simp_all)[3]
using k
apply -
apply(rule Prf.intros)
apply(auto)
apply(simp)
apply(erule Prf.cases)
apply(simp_all)[7]
apply(rule Prf.intros)
defer
apply(rotate_tac 1)
apply(erule Prf.cases)
apply(simp_all)[7]
apply(drule_tac meta_mp)
apply(erule Prf.cases)
apply(simp_all)[7]
apply(rule ih)
apply(case_tac vs)
apply(simp)
apply(simp)
apply(rotate_tac 3)
apply(erule Prf.cases)
apply(simp_all)[7]
apply(auto)[1]
apply (metis Prf.intros(1) Prf.intros(3))
apply(simp)
apply(drule head1)
apply(auto)[1]
apply (metis Prf.intros(3))
apply (metis Prf.intros)
apply(case_tac "nullable r1")
apply(simp)
apply(erule Prf.cases)
apply(simp_all)[7]
apply(auto)[1]
apply (metis Prf.intros(5))
apply (metis Prf.intros(3) Prf.intros(4) head1)
apply(simp)
apply(erule Prf.cases)
apply(simp_all)[7]
apply(auto)[1]
apply (metis nullable_correctness v1)
apply(drule head1)
apply(auto)[1]
apply (metis Prf.intros(3))
apply(simp)
apply(erule Prf.cases)
apply(simp_all)[7]
apply(auto)[1]
apply(drule head1)
apply(auto)[1]
apply(rule Prf.intros)
apply(auto)
apply(rule Prf.intros)
apply(auto)
apply(rotate_tac 2)
apply(erule Prf.cases)
apply(simp_all)[7]
apply(auto)
apply(drule head1)
apply(auto)
apply(rule Prf.intros)
apply(auto)
apply(rule Prf.intros)
apply(auto)
defer
apply(erule Prf.cases)
apply(simp_all)[7]
apply(auto)[1]
apply(rule Prf.intros)
apply(auto)
apply(drule head1)
apply(auto)[1]
defer
apply(rotate_tac 3)
apply(erule Prf.cases)
apply(simp_all)[7]
apply(auto)
apply(drule head1)
apply(auto)[1]
apply(simp)
apply(rule Prf.intros)
apply(auto)
apply(drule_tac x="v" in meta_spec)
apply(simp)
apply(erule Prf.cases)
apply(simp_all)[7]
apply(auto)[1]
apply(drule head1)
apply(auto)[1]
apply(rule Prf.intros)
apply(auto)
apply(drule meta_mp)
apply(rule Prf.intros)
apply(auto)
apply(simp)
apply (metis Prf.intros(3) head1)
defer
apply(simp)
apply(drule_tac head1)
apply(auto)[1]
apply(rule Prf.intros)
apply(rule Prf.intros)
apply(simp)
apply(simp)
apply(rule Prf.intros)
apply(simp)
apply(simp)
apply(rule Prf.intros)
apply(simp)
apply (metis nullable_correctness v1)
apply(simp)
apply(rule Prf.intros)
apply(simp)
apply(simp)
apply(rule Prf.intros)
apply(simp)
apply(simp)
apply(simp)
apply(rule Prf.intros)
apply(drule_tac head1)
apply(auto)[1]
apply (metis Prf.intros(3))
apply(rotate_tac 2)
apply(erule Prf.cases)
apply(simp_all)[7]
apply(auto)[1]
apply(rule Prf.intros)
defer
apply(drule_tac x="c" in meta_spec)
apply(simp)
apply(rotate_tac 6)
apply(erule Prf.cases)
apply(simp_all)[7]
apply(auto)[1]
apply(rule Prf.intros)
apply(auto)[2]
apply(drule v1)
apply(simp)
apply(rule Prf.intros)
apply(simp add: nullable_correctness[symmetric])
apply(rotate_tac 1)
apply(erule Prf.cases)
apply(simp_all)[7]
apply(auto)[1]
apply(drule head1)
apply(auto)[1]
apply(rule Prf.intros)
apply(simp)
apply(simp)
apply(simp)
lemma inj_proj_id:
assumes "\<turnstile> v : r" "head (flat v) = Some c"
shows "injval r c (projval r c v) = v"
using assms
apply(induct arbitrary: c rule: Prf.induct)
apply(simp)
apply(simp)
apply(drule head1)
apply(auto)[1]
apply(rotate_tac 2)
apply(erule Prf.cases)
apply(simp_all)[7]
apply(auto)[1]
apply(drule head1)
apply(auto)[1]
apply(simp)
apply(erule Prf.cases)
apply(simp_all)[7]
apply(simp)
apply(case_tac "ca = c'")
apply(simp)
apply(erule Prf.cases)
apply(simp_all)[7]
apply(simp)
apply(erule Prf.cases)
apply(simp_all)[7]
defer
apply(simp)
apply(case_tac "nullable r1")
apply(simp)
apply(erule Prf.cases)
apply(simp_all)[7]
apply(auto)[1]
apply(erule Prf.cases)
apply(simp_all)[7]
apply(auto)[1]
apply(rotate_tac 2)
apply(erule Prf.cases)
apply(simp_all)[7]
apply(simp)
apply(case_tac "nullable rexp1")
apply(simp)
apply(erule Prf.cases)
apply(simp_all)[7]
apply(auto)[1]
apply(erule Prf.cases)
apply(simp_all)[7]
apply(auto)[1]
apply(simp add: v4)
apply(auto)[1]
apply(simp add: v2a)
apply(simp only: der.simps)
apply(simp)
apply(erule Prf.cases)
apply(simp_all)[7]
apply(auto)[1]
apply(simp add: v4)
done
lemma POSIX_I:
assumes "\<turnstile> v : r" "\<And>v'. \<turnstile> v' : r \<Longrightarrow> flat v = flat v' \<Longrightarrow> v \<succeq>r v'"
shows "POSIX v r"
using assms
unfolding POSIX_def
apply(auto)
done
lemma DISJ:
"(\<not> A \<Longrightarrow> B) \<Longrightarrow> A \<or> B"
by metis
lemma DISJ2:
"\<not>(A \<and> B) \<longleftrightarrow> \<not>A \<or> \<not>B"
by metis
lemma APP: "xs @ [] = xs" by simp
lemma v5:
assumes "POSIX v (der c r)"
shows "POSIX (injval r c v) r"
using assms
apply(induct arbitrary: v rule: der.induct)
apply(simp)
apply(auto simp add: POSIX_def)[1]
apply(erule Prf.cases)
apply(simp_all)[7]
apply(erule Prf.cases)
apply(simp_all)[7]
apply(auto simp add: POSIX_def)[1]
apply(erule Prf.cases)
apply(simp_all)[7]
apply(erule Prf.cases)
apply(simp_all)[7]
apply(case_tac "c = c'")
apply(auto simp add: POSIX_def)[1]
apply(erule Prf.cases)
apply(simp_all)[7]
apply(rule Prf.intros)
apply(erule Prf.cases)
apply(simp_all)[7]
apply(simp add: ValOrd_eq_def)
apply(erule Prf.cases)
apply(simp_all)[7]
apply(simp)
apply(auto simp add: POSIX_def)[1]
apply(erule Prf.cases)
apply(simp_all)[7]
apply(erule Prf.cases)
apply(simp_all)[7]
prefer 3
apply(simp)
apply(frule POSIX_E1)
apply(erule Prf.cases)
apply(simp_all)[7]
apply(auto)[1]
apply(drule_tac x="v1" in meta_spec)
apply(drule meta_mp)
apply(rule POSIX_I)
apply(simp)
apply(simp add: POSIX_def)
apply(auto)[1]
apply(drule_tac x="Seq v' v2" in spec)
apply(simp)
apply(drule mp)
apply (metis Prf.intros(3))
apply(simp add: ValOrd_eq_def)
apply(erule disjE)
apply(simp)
apply(erule ValOrd.cases)
apply(simp_all)[10]
apply(subgoal_tac "\<exists>vs2. v2 = Stars vs2")
prefer 2
apply(rotate_tac 2)
apply(erule Prf.cases)
apply(auto)[7]
apply(erule exE)
apply(clarify)
apply(simp only: injval.simps)
apply(case_tac "POSIX (Stars (injval r c v1 # vs2)) (STAR r)")
apply(simp)
apply(subgoal_tac "\<exists>v'' vs''. Stars (v''#vs'') \<succ>(STAR r) Stars (injval r c v1 # vs2)")
apply(erule exE)+
apply(erule ValOrd.cases)
apply(simp_all)[8]
apply(auto)[1]
apply(subst (asm) (2) POSIX_def)
prefer 2
apply(subst (asm) (3) POSIX_def)
apply(simp)
apply(drule mp)
apply (metis Prf.intros(2) v3)
apply(erule exE)
apply(auto)[1]
apply
apply(subgoal_tac "\<turnstile> Stars (injval r c v1 # vs2) : STAR r")
apply(simp)
apply(case_tac "flat () = []")
apply(rule POSIX_I)
apply (metis POSIX_E1 der.simps(6) v3)
apply(rotate_tac 2)
apply(erule Prf.cases)
defer
defer
apply(simp_all)[5]
prefer 4
apply(clarify)
apply(simp only: v4 flat.simps injval.simps)
prefer 4
apply(clarify)
apply(simp only: v4 APP flat.simps injval.simps)
prefer 2
apply(erule Prf.cases)
apply(simp_all)[7]
apply(clarify)
apply(simp add: ValOrd_eq_def)
apply(subst (asm) POSIX_def)
apply(erule conjE)
apply(drule_tac x="va" in spec)
apply(simp)
apply(simp add: v4)
apply(simp add: ValOrd_eq_def)
apply(simp)
apply(rule disjI2)
apply(rule ValOrd.intros)
apply(rotate_tac 2)
apply(subst (asm) POSIX_def)
apply(simp)
apply(auto)[1]
apply(drule_tac x="v" in spec)
apply(simp)
apply(drule mp)
prefer 2
apply(simp add: ValOrd_eq_def)
apply(auto)[1]
apply(case_tac "injval rb c v1 = v \<and> [] = vs")
apply(simp)
apply(simp only: DISJ2)
apply(rule disjI2)
apply(erule disjE)
apply(auto)[1]
apply (metis list.distinct(1) v4)
apply(auto)[1]
apply(simp add: ValOrd_eq_def)
apply(rule DISJ)
apply(simp only: DISJ2)
apply(erule disjE)
apply(rule ValOrd.intros)
apply(subst (asm) POSIX_def)
apply(auto)[1]
apply (metis list.distinct(1) v4)
apply(subst (asm) POSIX_def)
apply(auto)[1]
apply(erule Prf.cases)
apply(simp_all)[7]
apply(rotate_tac 3)
apply(erule Prf.cases)
apply(simp_all)[7]
apply(auto)[1]
apply (metis list.distinct(1) v4)
apply (metis list.distinct(1) v4)
apply(clarify)
apply(rotate_tac 3)
apply(erule Prf.cases)
apply(simp_all)[7]
prefer 2
apply(clarify)
apply(simp add: ValOrd_eq_def)
apply(drule_tac x="Stars (v#vs)" in spec)
apply(drule mp)
apply(auto)[1]
apply(simp add: ValOrd_eq_def)
apply (metis POSIX_E1 der.simps(6) list.distinct(1) v4)
apply(rotate_tac 3)
apply(erule Prf.cases)
apply(simp_all)[7]
apply(simp)
apply(case_tac v2)
apply(simp)
apply(simp (no_asm) POSIX_def)
apply(auto)[1]
apply(auto)[1]
apply (metis POSIX_E der.simps(6) v3)
apply(rule Prf.intros)
apply(drule_tac x="v1" in meta_spec)
apply(drule meta_mp)
prefer 2
apply(subgoal_tac "POSIX v1 (der c r)")
prefer 2
apply(simp add: POSIX_def)
apply(auto)[1]
apply(simp add: ValOrd_eq_def)
apply(auto)[1]
lemma v5:
assumes "\<turnstile> v : der c r" "POSIX v (der c r)"
shows "POSIX (injval r c v) r"
using assms
apply(induct arbitrary: v rule: der.induct)
apply(simp)
apply(erule Prf.cases)
apply(simp_all)[7]
apply(simp)
apply(erule Prf.cases)
apply(simp_all)[7]
apply(simp)
apply(case_tac "c = c'")
apply(simp)
apply(erule Prf.cases)
apply(simp_all)[7]
apply(simp add: POSIX_def)
apply(auto)[1]
apply(rule Prf.intros)
apply(erule Prf.cases)
apply(simp_all)[7]
apply(simp add: ValOrd_eq_def)
apply(erule Prf.cases)
apply(simp_all)[7]
apply(simp)
apply(erule Prf.cases)
apply(simp_all)[7]
prefer 3
apply(simp)
apply(erule Prf.cases)
apply(simp_all)[7]
apply(auto)[1]
apply(case_tac "flat (Seq v1 v2) \<noteq> []")
apply(subgoal_tac "POSIX v1 (der c r)")
prefer 2
apply(simp add: POSIX_def)
apply(auto)[1]
apply(drule_tac x="v1" in meta_spec)
apply(simp)
apply(simp (no_asm) add: POSIX_def)
apply(auto)[1]
apply(rule v3)
apply (metis Prf.intros(3) der.simps(6))
apply(rotate_tac 1)
apply(erule Prf.cases)
apply(simp_all)[7]
apply(simp add: ValOrd_eq_def)
apply(rule disjI2)
apply(rotate_tac 1)
apply(erule Prf.cases)
apply(simp_all)[7]
apply(rule ValOrd.intros)
apply(simp)
apply (metis list.distinct(1) v4)
apply(rule ValOrd.intros)
apply(simp add: POSIX_def)
apply(auto)[1]
apply(rotate_tac 3)
apply(erule Prf.cases)
apply(simp_all)[7]
apply(simp add: ValOrd_eq_def)
apply(drule_tac x="v" in spec)
apply(simp)
apply(auto)[1]
apply(simp)
apply(simp add: POSIX_def)
apply(auto)[1]
apply(
apply(rotate_tac 1)
apply(erule Prf.cases)
apply(simp_all)[7]
apply (metis list.distinct(1) v4)
apply(rotate_tac 8)
apply(erule Prf.cases)
apply(simp_all)[7]
apply (metis POSIX_def ValOrd.intros(9) ValOrd_eq_def)
apply(simp add: ValOrd_eq_def)
apply(simp)
apply(simp add: ValOrd_eq_def)
apply(simp add: POSIX_def)
apply(auto)[1]
apply(simp)
apply(simp add: ValOrd_eq_def)
apply(simp add: POSIX_def)
apply(erule conjE)+
apply(drule_tac x="Seq v1 v2" in spec)
apply(simp)
apply(rotate_tac 2)
apply(erule Prf.cases)
apply(simp_all)[7]
apply(auto)[1]
apply(simp add: POSIX_def)
apply(auto)[1]
apply(rule Prf.intros)
apply(rule v3)
apply(simp)
apply(rotate_tac 5)
apply(erule Prf.cases)
apply(simp_all)[7]
apply(auto)[1]
apply(rotate_tac 4)
apply(erule Prf.cases)
apply(simp_all)[7]
apply(auto)[1]
apply(simp add: ValOrd_eq_def)
apply(simp)
prefer 2
apply(auto)[1]
apply(subgoal_tac "POSIX v2 (der c r2)")
apply(rotate_tac 1)
apply(drule_tac x="v2" in meta_spec)
apply(simp)
apply(subgoal_tac "\<turnstile> Right (injval r2 c v2) : (ALT r1 r2)")
prefer 2
apply (metis Prf.intros(5) v3)
apply(simp (no_asm) add: POSIX_def)
apply(auto)[1]
apply(rotate_tac 6)
apply(erule Prf.cases)
apply(simp_all)[7]
prefer 2
apply(auto)[1]
apply(simp add: ValOrd_eq_def)
apply (metis POSIX_def ValOrd.intros(5) ValOrd_eq_def)
apply(auto)[1]
apply(simp add: ValOrd_eq_def)
section {* Correctness Proof of the Matcher *}
section {* Left-Quotient of a Set *}
fun
zeroable :: "rexp \<Rightarrow> bool"
where
"zeroable (NULL) = True"
| "zeroable (EMPTY) = False"
| "zeroable (CHAR c) = False"
| "zeroable (ALT r1 r2) = (zeroable r1 \<and> zeroable r2)"
| "zeroable (SEQ r1 r2) = (zeroable r1 \<or> zeroable r2)"
| "zeroable (STAR r) = False"
lemma zeroable_correctness:
shows "zeroable r \<longleftrightarrow> (L r = {})"
apply(induct r)
apply(auto simp add: Seq_def)[6]
done
section {* Left-Quotient of a Set *}
definition
Der :: "char \<Rightarrow> string set \<Rightarrow> string set"
where
"Der c A \<equiv> {s. [c] @ s \<in> A}"
lemma Der_null [simp]:
shows "Der c {} = {}"
unfolding Der_def
by auto
lemma Der_empty [simp]:
shows "Der c {[]} = {}"
unfolding Der_def
by auto
lemma Der_char [simp]:
shows "Der c {[d]} = (if c = d then {[]} else {})"
unfolding Der_def
by auto
lemma Der_union [simp]:
shows "Der c (A \<union> B) = Der c A \<union> Der c B"
unfolding Der_def
by auto
lemma Der_seq [simp]:
shows "Der c (A ;; B) = (Der c A) ;; B \<union> (if [] \<in> A then Der c B else {})"
unfolding Der_def Seq_def
by (auto simp add: Cons_eq_append_conv)
lemma Der_star [simp]:
shows "Der c (A\<star>) = (Der c A) ;; A\<star>"
proof -
have "Der c (A\<star>) = Der c ({[]} \<union> A ;; A\<star>)"
by (simp only: star_cases[symmetric])
also have "... = Der c (A ;; A\<star>)"
by (simp only: Der_union Der_empty) (simp)
also have "... = (Der c A) ;; A\<star> \<union> (if [] \<in> A then Der c (A\<star>) else {})"
by simp
also have "... = (Der c A) ;; A\<star>"
unfolding Seq_def Der_def
by (auto dest: star_decomp)
finally show "Der c (A\<star>) = (Der c A) ;; A\<star>" .
qed
lemma der_correctness:
shows "L (der c r) = Der c (L r)"
by (induct r)
(simp_all add: nullable_correctness)
lemma matcher_correctness:
shows "matcher r s \<longleftrightarrow> s \<in> L r"
by (induct s arbitrary: r)
(simp_all add: nullable_correctness der_correctness Der_def)
section {* Examples *}
definition
"CHRA \<equiv> CHAR (CHR ''a'')"
definition
"ALT1 \<equiv> ALT CHRA EMPTY"
definition
"SEQ3 \<equiv> SEQ (SEQ ALT1 ALT1) ALT1"
value "matcher SEQ3 ''aaa''"
value "matcher NULL []"
value "matcher (CHAR (CHR ''a'')) [CHR ''a'']"
value "matcher (CHAR a) [a,a]"
value "matcher (STAR (CHAR a)) []"
value "matcher (STAR (CHAR a)) [a,a]"
value "matcher (SEQ (CHAR (CHR ''a'')) (SEQ (STAR (CHAR (CHR ''b''))) (CHAR (CHR ''c'')))) ''abbbbc''"
value "matcher (SEQ (CHAR (CHR ''a'')) (SEQ (STAR (CHAR (CHR ''b''))) (CHAR (CHR ''c'')))) ''abbcbbc''"
section {* Incorrect Matcher - fun-definition rejected *}
fun
match :: "rexp list \<Rightarrow> string \<Rightarrow> bool"
where
"match [] [] = True"
| "match [] (c # s) = False"
| "match (NULL # rs) s = False"
| "match (EMPTY # rs) s = match rs s"
| "match (CHAR c # rs) [] = False"
| "match (CHAR c # rs) (d # s) = (if c = d then match rs s else False)"
| "match (ALT r1 r2 # rs) s = (match (r1 # rs) s \<or> match (r2 # rs) s)"
| "match (SEQ r1 r2 # rs) s = match (r1 # r2 # rs) s"
| "match (STAR r # rs) s = (match rs s \<or> match (r # (STAR r) # rs) s)"
end