--- a/thys/Re.thy Mon Sep 08 16:36:13 2014 +0100
+++ b/thys/Re.thy Mon Sep 08 21:13:36 2014 +0100
@@ -1,4 +1,4 @@
-theory Matcher3simple
+theory Re
imports "Main"
begin
@@ -41,6 +41,9 @@
| "L (SEQ r1 r2) = (L r1) ;; (L r2)"
| "L (ALT r1 r2) = (L r1) \<union> (L r2)"
+
+section {* Values *}
+
datatype val =
Void
| Char char
@@ -48,6 +51,8 @@
| Right val
| Left val
+section {* Relation between values and regular expressions *}
+
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"
@@ -56,6 +61,8 @@
| "\<turnstile> Void : EMPTY"
| "\<turnstile> Char c : CHAR c"
+section {* The string behind a value *}
+
fun flat :: "val \<Rightarrow> string"
where
"flat(Void) = []"
@@ -64,29 +71,6 @@
| "flat(Right v) = flat(v)"
| "flat(Seq v1 v2) = flat(v1) @ flat(v2)"
-(* not actually in the paper *)
-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"
@@ -104,9 +88,11 @@
apply (metis Prf.intros(1) flat.simps(5))
apply (metis Prf.intros(2) flat.simps(3))
apply (metis Prf.intros(3) flat.simps(4))
-sorry
+apply(erule Prf.cases)
+apply(auto)
+done
-(*by (smt Prf.cases flat.simps(3) flat.simps(4) rexp.distinct(13) rexp.distinct(17) rexp.distinct(19) rexp.inject(3))*)
+section {* Ordering of values *}
inductive ValOrd :: "val \<Rightarrow> rexp \<Rightarrow> val \<Rightarrow> bool" ("_ \<succ>_ _" [100, 100, 100] 100)
where
@@ -133,6 +119,8 @@
done
*)
+section {* Posix definition *}
+
definition POSIX :: "val \<Rightarrow> rexp \<Rightarrow> bool"
where
"POSIX v r \<equiv> (\<forall>v'. (\<turnstile> v' : r \<and> flat v = flat v') \<longrightarrow> v \<succ>r v')"
@@ -247,14 +235,6 @@
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 *}
@@ -293,13 +273,10 @@
apply(auto)
done
-
-lemma mkeps_flats:
- assumes "nullable(r)" shows "flatten (flats (mkeps r)) = []"
-using assms
-apply(induct rule: nullable.induct)
-apply(auto)
-done
+text {*
+ The value mkeps returns is always the correct POSIX
+ value.
+*}
lemma mkeps_POSIX:
assumes "nullable r"
@@ -314,9 +291,37 @@
apply (metis ValOrd.intros)
apply(simp add: POSIX_def)
apply(auto)[1]
-sorry
+apply(simp add: POSIX_def)
+apply(auto)[1]
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(auto)
+apply (simp add: ValOrd.intros(2) mkeps_flat)
+apply(simp add: POSIX_def)
+apply(auto)[1]
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(auto)
+apply (simp add: ValOrd.intros(6))
+apply (simp add: ValOrd.intros(3))
+apply(simp add: POSIX_def)
+apply(auto)[1]
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(auto)
+apply (simp add: ValOrd.intros(6))
+apply (simp add: ValOrd.intros(3))
+apply(simp add: POSIX_def)
+apply(auto)[1]
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(auto)
+apply (metis Prf_flat_L mkeps_flat nullable_correctness)
+by (simp add: ValOrd.intros(5))
+section {* Derivatives *}
+
fun
der :: "char \<Rightarrow> rexp \<Rightarrow> rexp"
where
@@ -335,6 +340,8 @@
"ders [] r = r"
| "ders (c # s) r = ders s (der c r)"
+section {* Injection function *}
+
fun injval :: "rexp \<Rightarrow> char \<Rightarrow> val \<Rightarrow> val"
where
"injval (CHAR d) c Void = Char d"
@@ -344,6 +351,8 @@
| "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)"
+section {* Projection function *}
+
fun projval :: "rexp \<Rightarrow> char \<Rightarrow> val \<Rightarrow> val"
where
"projval (CHAR d) c _ = Void"
@@ -354,6 +363,10 @@
else if nullable r1 then Left (Seq (projval r1 c v1) v2)
else Seq (projval r1 c v1) v2)"
+text {*
+ Injection value is related to r
+*}
+
lemma v3:
assumes "\<turnstile> v : der c r" shows "\<turnstile> (injval r c v) : r"
using assms
@@ -394,28 +407,12 @@
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
+text {*
+ The string behin the injection value is an added c
+*}
lemma v4:
- assumes "\<turnstile> v : der c r" shows "flat (injval r c v) = c#(flat v)"
+ 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)
@@ -451,6 +448,9 @@
apply(simp_all)[5]
done
+text {*
+ Injection followed by projection is the identity.
+*}
lemma proj_inj_id:
assumes "\<turnstile> v : der c r"
@@ -494,24 +494,15 @@
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
+text {*
-(* HERE *)
+ HERE: Crucial lemma that does not go through in the sequence case.
+
+*}
lemma v5:
assumes "\<turnstile> v : der c r" "POSIX v (der c r)"
shows "POSIX (injval r c v) r"
using assms
-apply(induct r)
-apply(simp (no_asm) only: POSIX_def)
-apply(rule allI)
-apply(rule impI)
-apply(simp)
-apply(erule Prf.cases)
-apply(simp_all)[5]
apply(induct arbitrary: v rule: der.induct)
apply(simp)
apply(erule Prf.cases)
@@ -526,11 +517,11 @@
apply(simp_all)[5]
apply(erule Prf.cases)
apply(simp_all)[5]
-apply (metis ValOrd.intros(7))
+using ValOrd.simps apply blast
+apply(auto)
apply(erule Prf.cases)
apply(simp_all)[5]
-prefer 2
-apply(simp)
+prefer 2
apply(case_tac "nullable r1")
apply(simp)
defer
@@ -538,1126 +529,4 @@
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
\ No newline at end of file
+oops