# HG changeset patch
# User Christian Urban <christian dot urban at kcl dot ac dot uk>
# Date 1410207216 -3600
# Node ID b409ecf47f644b988cd0500150bdd1748fd9d7c4
# Parent  87618dae0e047700d5e0cb6129fb680ebde5e027
cleaned up the theory

diff -r 87618dae0e04 -r b409ecf47f64 thys/Re.thy
--- 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