lexing: thys/Re.thy@fe177dfc4697 (annotated)

5 fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1	theory Matcher3simple
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	2	imports "Main"
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	3	begin
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	4
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	5	section {* Sequential Composition of Sets *}
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	6
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	7	definition
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	8	Sequ :: "string set \<Rightarrow> string set \<Rightarrow> string set" ("_ ;; _" [100,100] 100)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	9	where
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	10	"A ;; B = {s1 @ s2 \| s1 s2. s1 \<in> A \<and> s2 \<in> B}"
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	11
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	12	text {* Two Simple Properties about Sequential Composition *}
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	13
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	14	lemma seq_empty [simp]:
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	15	shows "A ;; {[]} = A"
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	16	and "{[]} ;; A = A"
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	17	by (simp_all add: Sequ_def)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	18
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	19	lemma seq_null [simp]:
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	20	shows "A ;; {} = {}"
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	21	and "{} ;; A = {}"
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	22	by (simp_all add: Sequ_def)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	23
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	24	section {* Regular Expressions *}
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	25
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	26	datatype rexp =
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	27	NULL
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	28	\| EMPTY
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	29	\| CHAR char
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	30	\| SEQ rexp rexp
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	31	\| ALT rexp rexp
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	32
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	33	section {* Semantics of Regular Expressions *}
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	34
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	35	fun
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	36	L :: "rexp \<Rightarrow> string set"
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	37	where
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	38	"L (NULL) = {}"
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	39	\| "L (EMPTY) = {[]}"
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	40	\| "L (CHAR c) = {[c]}"
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	41	\| "L (SEQ r1 r2) = (L r1) ;; (L r2)"
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	42	\| "L (ALT r1 r2) = (L r1) \<union> (L r2)"
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	43
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	44	datatype val =
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	45	Void
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	46	\| Char char
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	47	\| Seq val val
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	48	\| Right val
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	49	\| Left val
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	50
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	51	inductive Prf :: "val \<Rightarrow> rexp \<Rightarrow> bool" ("\<turnstile> _ : _" [100, 100] 100)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	52	where
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	53	"\<lbrakk>\<turnstile> v1 : r1; \<turnstile> v2 : r2\<rbrakk> \<Longrightarrow> \<turnstile> Seq v1 v2 : SEQ r1 r2"
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	54	\| "\<turnstile> v1 : r1 \<Longrightarrow> \<turnstile> Left v1 : ALT r1 r2"
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	55	\| "\<turnstile> v2 : r2 \<Longrightarrow> \<turnstile> Right v2 : ALT r1 r2"
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	56	\| "\<turnstile> Void : EMPTY"
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	57	\| "\<turnstile> Char c : CHAR c"
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	58
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	59	fun flat :: "val \<Rightarrow> string"
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	60	where
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	61	"flat(Void) = []"
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	62	\| "flat(Char c) = [c]"
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	63	\| "flat(Left v) = flat(v)"
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	64	\| "flat(Right v) = flat(v)"
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	65	\| "flat(Seq v1 v2) = flat(v1) @ flat(v2)"
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	66
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	67	datatype tree =
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	68	Leaf string
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	69	\| Branch tree tree
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	70
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	71	fun flats :: "val \<Rightarrow> tree"
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	72	where
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	73	"flats(Void) = Leaf []"
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	74	\| "flats(Char c) = Leaf [c]"
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	75	\| "flats(Left v) = flats(v)"
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	76	\| "flats(Right v) = flats(v)"
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	77	\| "flats(Seq v1 v2) = Branch (flats v1) (flats v2)"
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	78
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	79	fun flatten :: "tree \<Rightarrow> string"
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	80	where
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	81	"flatten (Leaf s) = s"
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	82	\| "flatten (Branch t1 t2) = flatten t1 @ flatten t2"
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	83
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	84	lemma flats_flat:
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	85	shows "flat v1 = flatten (flats v1)"
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	86	apply(induct v1)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	87	apply(simp_all)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	88	done
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	89
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	90	lemma Prf_flat_L:
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	91	assumes "\<turnstile> v : r" shows "flat v \<in> L r"
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	92	using assms
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	93	apply(induct)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	94	apply(auto simp add: Sequ_def)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	95	done
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	96
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	97	lemma L_flat_Prf:
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	98	"L(r) = {flat v \| v. \<turnstile> v : r}"
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	99	apply(induct r)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	100	apply(auto dest: Prf_flat_L simp add: Sequ_def)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	101	apply (metis Prf.intros(4) flat.simps(1))
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	102	apply (metis Prf.intros(5) flat.simps(2))
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	103	apply (metis Prf.intros(1) flat.simps(5))
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	104	apply (metis Prf.intros(2) flat.simps(3))
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	105	apply (metis Prf.intros(3) flat.simps(4))
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	106	by (smt Prf.cases flat.simps(3) flat.simps(4) rexp.distinct(13) rexp.distinct(17) rexp.distinct(19) rexp.inject(3))
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	107
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	108	inductive ValOrd :: "val \<Rightarrow> rexp \<Rightarrow> val \<Rightarrow> bool" ("_ \<succ>_ _" [100, 100, 100] 100)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	109	where
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	110	"\<lbrakk>v1 \<succ>r1 v1'; v2 \<succ>r2 v2'\<rbrakk> \<Longrightarrow> (Seq v1 v2) \<succ>(SEQ r1 r2) (Seq v1' v2')"
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	111	\| "length (flat v1) \<ge> length (flat v2) \<Longrightarrow> (Left v1) \<succ>(ALT r1 r2) (Right v2)"
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	112	\| "length (flat v2) > length (flat v1) \<Longrightarrow> (Right v2) \<succ>(ALT r1 r2) (Left v1)"
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	113	\| "v2 \<succ>r2 v2' \<Longrightarrow> (Right v2) \<succ>(ALT r1 r2) (Right v2')"
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	114	\| "v1 \<succ>r1 v1' \<Longrightarrow> (Left v1) \<succ>(ALT r1 r2) (Left v1')"
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	115	\| "Void \<succ>EMPTY Void"
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	116	\| "(Char c) \<succ>(CHAR c) (Char c)"
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	117
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	118	lemma
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	119	assumes "r = SEQ (ALT EMPTY EMPTY) (ALT EMPTY (CHAR c))"
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	120	shows "(Seq (Left Void) (Right (Char c))) \<succ>r (Seq (Left Void) (Left Void))"
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	121	using assms
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	122	apply(simp)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	123	apply(rule ValOrd.intros)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	124	apply(rule ValOrd.intros)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	125	apply(rule ValOrd.intros)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	126	apply(rule ValOrd.intros)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	127	apply(simp)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	128	done
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	129
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	130
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	131	definition POSIX :: "val \<Rightarrow> rexp \<Rightarrow> bool"
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	132	where
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	133	"POSIX v r \<equiv> (\<forall>v'. (\<turnstile> v' : r \<and> flats v = flats v') \<longrightarrow> v \<succ>r v')"
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	134
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	135	lemma POSIX:
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	136	assumes "r = SEQ (ALT EMPTY EMPTY) (ALT EMPTY (CHAR c))"
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	137	shows "POSIX (Seq (Left Void) (Right (Char c))) r"
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	138	apply(simp add: POSIX_def assms)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	139	apply(auto)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	140	apply(erule Prf.cases)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	141	apply(simp_all)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	142	apply(rule ValOrd.intros)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	143	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))
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	144	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))
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	145
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	146
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	147	lemma Exists_POSIX: "\<exists>v. POSIX v r"
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	148	apply(induct r)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	149	apply(auto simp add: POSIX_def)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	150	apply(rule exI)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	151	apply(auto)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	152	apply(erule Prf.cases)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	153	apply(simp_all)[5]
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	154	apply (smt Prf.simps ValOrd.intros(6) rexp.distinct(11) rexp.distinct(13) rexp.distinct(9))
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	155	apply(rule exI)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	156	apply(auto)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	157	apply(erule Prf.cases)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	158	apply(simp_all)[5]
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	159	apply(rule ValOrd.intros)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	160	apply(rule exI)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	161	apply(auto)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	162	apply(erule Prf.cases)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	163	apply(simp_all)[5]
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	164	apply(rule ValOrd.intros)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	165	apply(auto)[2]
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	166	apply(rule_tac x="Left v" in exI)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	167	apply(auto)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	168	apply(erule Prf.cases)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	169	apply(simp_all)[5]
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	170	apply(rule ValOrd.intros)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	171	apply(auto)[1]
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	172	apply(auto)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	173	apply(rule ValOrd.intros)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	174	by (metis flats_flat order_refl)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	175
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	176
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	177	lemma POSIX_SEQ:
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	178	assumes "POSIX (Seq v1 v2) (SEQ r1 r2)" "\<turnstile> v1 : r1" "\<turnstile> v2 : r2"
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	179	shows "POSIX v1 r1 \<and> POSIX v2 r2"
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	180	using assms
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	181	unfolding POSIX_def
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	182	apply(auto)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	183	apply(drule_tac x="Seq v' v2" in spec)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	184	apply(simp)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	185	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))
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	186	apply(drule_tac x="Seq v1 v'" in spec)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	187	apply(simp)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	188	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))
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	189
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	190	lemma POSIX_SEQ_I:
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	191	assumes "POSIX v1 r1" "POSIX v2 r2"
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	192	shows "POSIX (Seq v1 v2) (SEQ r1 r2)"
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	193	using assms
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	194	unfolding POSIX_def
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	195	apply(auto)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	196	apply(rotate_tac 4)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	197	apply(erule Prf.cases)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	198	apply(simp_all)[5]
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	199	apply(auto)[1]
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	200	apply(rule ValOrd.intros)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	201	apply(auto)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	202	done
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	203
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	204	lemma POSIX_ALT:
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	205	assumes "POSIX (Left v1) (ALT r1 r2)"
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	206	shows "POSIX v1 r1"
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	207	using assms
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	208	unfolding POSIX_def
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	209	apply(auto)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	210	apply(drule_tac x="Left v'" in spec)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	211	apply(simp)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	212	apply(drule mp)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	213	apply(rule Prf.intros)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	214	apply(auto)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	215	apply(erule ValOrd.cases)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	216	apply(simp_all)[7]
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	217	done
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	218
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	219	lemma POSIX_ALT1a:
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	220	assumes "POSIX (Right v2) (ALT r1 r2)"
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	221	shows "POSIX v2 r2"
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	222	using assms
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	223	unfolding POSIX_def
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	224	apply(auto)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	225	apply(drule_tac x="Right v'" in spec)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	226	apply(simp)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	227	apply(drule mp)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	228	apply(rule Prf.intros)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	229	apply(auto)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	230	apply(erule ValOrd.cases)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	231	apply(simp_all)[7]
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	232	done
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	233
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	234	lemma POSIX_ALT1b:
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	235	assumes "POSIX (Right v2) (ALT r1 r2)"
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	236	shows "(\<forall>v'. (\<turnstile> v' : r2 \<and> flats v' = flats v2) \<longrightarrow> v2 \<succ>r2 v')"
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	237	using assms
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	238	apply(drule_tac POSIX_ALT1a)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	239	unfolding POSIX_def
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	240	apply(auto)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	241	done
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	242
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	243	lemma POSIX_ALT_I1:
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	244	assumes "POSIX v1 r1"
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	245	shows "POSIX (Left v1) (ALT r1 r2)"
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	246	using assms
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	247	unfolding POSIX_def
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	248	apply(auto)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	249	apply(rotate_tac 3)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	250	apply(erule Prf.cases)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	251	apply(simp_all)[5]
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	252	apply(auto)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	253	apply(rule ValOrd.intros)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	254	apply(auto)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	255	apply(rule ValOrd.intros)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	256	by (metis flats_flat order_refl)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	257
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	258	lemma POSIX_ALT_I2:
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	259	assumes "POSIX v2 r2" "\<forall>v'. \<turnstile> v' : r1 \<longrightarrow> length (flat v2) > length (flat v')"
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	260	shows "POSIX (Right v2) (ALT r1 r2)"
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	261	using assms
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	262	unfolding POSIX_def
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	263	apply(auto)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	264	apply(rotate_tac 3)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	265	apply(erule Prf.cases)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	266	apply(simp_all)[5]
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	267	apply(auto)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	268	prefer 2
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	269	apply(rule ValOrd.intros)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	270	apply metis
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	271	apply(rule ValOrd.intros)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	272	apply(auto)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	273	done
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	274
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	275	lemma ValOrd_refl:
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	276	assumes "\<turnstile> v : r"
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	277	shows "v \<succ>r v"
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	278	using assms
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	279	apply(induct)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	280	apply(auto intro: ValOrd.intros)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	281	done
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	282
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	283	lemma ValOrd_length:
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	284	assumes "v1 \<succ>r v2" shows "length (flat v1) \<ge> length (flat v2)"
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	285	using assms
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	286	apply(induct)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	287	apply(auto)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	288	done
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	289
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	290	section {* The Matcher *}
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	291
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	292	fun
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	293	nullable :: "rexp \<Rightarrow> bool"
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	294	where
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	295	"nullable (NULL) = False"
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	296	\| "nullable (EMPTY) = True"
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	297	\| "nullable (CHAR c) = False"
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	298	\| "nullable (ALT r1 r2) = (nullable r1 \<or> nullable r2)"
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	299	\| "nullable (SEQ r1 r2) = (nullable r1 \<and> nullable r2)"
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	300
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	301	lemma nullable_correctness:
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	302	shows "nullable r \<longleftrightarrow> [] \<in> (L r)"
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	303	apply (induct r)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	304	apply(auto simp add: Sequ_def)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	305	done
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	306
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	307	fun mkeps :: "rexp \<Rightarrow> val"
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	308	where
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	309	"mkeps(EMPTY) = Void"
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	310	\| "mkeps(SEQ r1 r2) = Seq (mkeps r1) (mkeps r2)"
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	311	\| "mkeps(ALT r1 r2) = (if nullable(r1) then Left (mkeps r1) else Right (mkeps r2))"
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	312
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	313	lemma mkeps_nullable:
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	314	assumes "nullable(r)" shows "\<turnstile> mkeps r : r"
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	315	using assms
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	316	apply(induct rule: nullable.induct)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	317	apply(auto intro: Prf.intros)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	318	done
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	319
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	320	lemma mkeps_flat:
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	321	assumes "nullable(r)" shows "flat (mkeps r) = []"
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	322	using assms
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	323	apply(induct rule: nullable.induct)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	324	apply(auto)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	325	done
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	326
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	327
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	328	lemma mkeps_flats:
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	329	assumes "nullable(r)" shows "flatten (flats (mkeps r)) = []"
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	330	using assms
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	331	apply(induct rule: nullable.induct)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	332	apply(auto)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	333	done
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	334
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	335	lemma mkeps_POSIX:
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	336	assumes "nullable r"
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	337	shows "POSIX (mkeps r) r"
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	338	using assms
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	339	apply(induct r)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	340	apply(auto)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	341	apply(simp add: POSIX_def)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	342	apply(auto)[1]
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	343	apply(erule Prf.cases)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	344	apply(simp_all)[5]
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	345	apply (metis ValOrd.intros(6))
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	346	apply(simp add: POSIX_def)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	347	apply(auto)[1]
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	348	apply(erule Prf.cases)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	349	apply(simp_all)[5]
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	350	apply(auto)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	351	apply (metis ValOrd.intros(1) append_is_Nil_conv mkeps_flat)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	352	apply(simp add: POSIX_def)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	353	apply(auto)[1]
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	354	apply(erule Prf.cases)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	355	apply(simp_all)[5]
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	356	apply(auto)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	357	apply (metis ValOrd.intros(5))
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	358	apply(rule ValOrd.intros(2))
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	359	apply(simp add: mkeps_flat)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	360	apply(simp add: flats_flat)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	361	apply (metis mkeps_flats)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	362	apply(simp add: POSIX_def)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	363	apply(auto)[1]
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	364	apply(erule Prf.cases)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	365	apply(simp_all)[5]
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	366	apply(auto)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	367	apply (metis ValOrd.intros(5))
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	368	apply (smt ValOrd.intros(2) flats_flat)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	369	apply(simp add: POSIX_def)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	370	apply(auto)[1]
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	371	apply(erule Prf.cases)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	372	apply(simp_all)[5]
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	373	apply (metis Prf_flat_L flats_flat mkeps_flats nullable_correctness)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	374	by (metis ValOrd.intros(4))
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	375
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	376	fun
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	377	der :: "char \<Rightarrow> rexp \<Rightarrow> rexp"
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	378	where
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	379	"der c (NULL) = NULL"
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	380	\| "der c (EMPTY) = NULL"
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	381	\| "der c (CHAR c') = (if c = c' then EMPTY else NULL)"
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	382	\| "der c (ALT r1 r2) = ALT (der c r1) (der c r2)"
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	383	\| "der c (SEQ r1 r2) =
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	384	(if nullable r1
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	385	then ALT (SEQ (der c r1) r2) (der c r2)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	386	else SEQ (der c r1) r2)"
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	387
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	388	fun
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	389	ders :: "string \<Rightarrow> rexp \<Rightarrow> rexp"
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	390	where
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	391	"ders [] r = r"
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	392	\| "ders (c # s) r = ders s (der c r)"
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	393
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	394	fun injval :: "rexp \<Rightarrow> char \<Rightarrow> val \<Rightarrow> val"
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	395	where
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	396	"injval (CHAR d) c Void = Char d"
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	397	\| "injval (ALT r1 r2) c (Left v1) = Left(injval r1 c v1)"
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	398	\| "injval (ALT r1 r2) c (Right v2) = Right(injval r2 c v2)"
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	399	\| "injval (SEQ r1 r2) c (Seq v1 v2) = Seq (injval r1 c v1) v2"
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	400	\| "injval (SEQ r1 r2) c (Left (Seq v1 v2)) = Seq (injval r1 c v1) v2"
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	401	\| "injval (SEQ r1 r2) c (Right v2) = Seq (mkeps r1) (injval r2 c v2)"
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	402
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	403	fun projval :: "rexp \<Rightarrow> char \<Rightarrow> val \<Rightarrow> val"
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	404	where
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	405	"projval (CHAR d) c _ = Void"
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	406	\| "projval (ALT r1 r2) c (Left v1) = Left(projval r1 c v1)"
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	407	\| "projval (ALT r1 r2) c (Right v2) = Right(projval r2 c v2)"
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	408	\| "projval (SEQ r1 r2) c (Seq v1 v2) =
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	409	(if flat v1 = [] then Right(projval r2 c v2)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	410	else if nullable r1 then Left (Seq (projval r1 c v1) v2)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	411	else Seq (projval r1 c v1) v2)"
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	412
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	413	lemma v3:
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	414	assumes "\<turnstile> v : der c r" shows "\<turnstile> (injval r c v) : r"
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	415	using assms
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	416	apply(induct arbitrary: v rule: der.induct)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	417	apply(simp)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	418	apply(erule Prf.cases)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	419	apply(simp_all)[5]
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	420	apply(erule Prf.cases)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	421	apply(simp_all)[5]
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	422	apply(case_tac "c = c'")
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	423	apply(simp)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	424	apply(erule Prf.cases)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	425	apply(simp_all)[5]
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	426	apply (metis Prf.intros(5))
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	427	apply(erule Prf.cases)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	428	apply(simp_all)[5]
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	429	apply(erule Prf.cases)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	430	apply(simp_all)[5]
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	431	apply (metis Prf.intros(2))
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	432	apply (metis Prf.intros(3))
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	433	apply(simp)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	434	apply(case_tac "nullable r1")
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	435	apply(simp)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	436	apply(erule Prf.cases)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	437	apply(simp_all)[5]
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	438	apply(auto)[1]
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	439	apply(erule Prf.cases)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	440	apply(simp_all)[5]
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	441	apply(auto)[1]
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	442	apply (metis Prf.intros(1))
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	443	apply(auto)[1]
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	444	apply (metis Prf.intros(1) mkeps_nullable)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	445	apply(simp)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	446	apply(erule Prf.cases)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	447	apply(simp_all)[5]
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	448	apply(auto)[1]
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	449	apply(rule Prf.intros)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	450	apply(auto)[2]
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	451	done
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	452
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	453	fun head where
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	454	"head [] = None"
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	455	\| "head (x#xs) = Some x"
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	456
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	457	lemma head1:
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	458	assumes "head (xs @ ys) = Some x"
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	459	shows "(head xs = Some x) \<or> (xs = [] \<and> head ys = Some x)"
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	460	using assms
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	461	apply(induct xs)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	462	apply(auto)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	463	done
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	464
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	465	lemma head2:
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	466	assumes "head (xs @ ys) = None"
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	467	shows "(head xs = None) \<and> (head ys = None)"
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	468	using assms
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	469	apply(induct xs)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	470	apply(auto)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	471	done
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	472
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	473	lemma v4:
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	474	assumes "\<turnstile> v : der c r" shows "flat (injval r c v) = c#(flat v)"
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	475	using assms
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	476	apply(induct arbitrary: v rule: der.induct)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	477	apply(simp)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	478	apply(erule Prf.cases)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	479	apply(simp_all)[5]
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	480	apply(simp)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	481	apply(erule Prf.cases)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	482	apply(simp_all)[5]
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	483	apply(simp)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	484	apply(case_tac "c = c'")
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	485	apply(simp)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	486	apply(auto)[1]
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	487	apply(erule Prf.cases)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	488	apply(simp_all)[5]
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	489	apply(simp)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	490	apply(erule Prf.cases)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	491	apply(simp_all)[5]
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	492	apply(simp)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	493	apply(erule Prf.cases)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	494	apply(simp_all)[5]
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	495	apply(simp)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	496	apply(case_tac "nullable r1")
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	497	apply(simp)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	498	apply(erule Prf.cases)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	499	apply(simp_all)[5]
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	500	apply(auto)[1]
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	501	apply(erule Prf.cases)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	502	apply(simp_all)[5]
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	503	apply(auto)[1]
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	504	apply (metis mkeps_flat)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	505	apply(simp)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	506	apply(erule Prf.cases)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	507	apply(simp_all)[5]
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	508	done
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	509
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	510
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	511	lemma proj_inj_id:
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	512	assumes "\<turnstile> v : der c r"
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	513	shows "projval r c (injval r c v) = v"
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	514	using assms
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	515	apply(induct r arbitrary: c v rule: rexp.induct)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	516	apply(simp)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	517	apply(erule Prf.cases)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	518	apply(simp_all)[5]
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	519	apply(simp)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	520	apply(erule Prf.cases)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	521	apply(simp_all)[5]
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	522	apply(simp)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	523	apply(case_tac "c = char")
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	524	apply(simp)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	525	apply(erule Prf.cases)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	526	apply(simp_all)[5]
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	527	apply(simp)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	528	apply(erule Prf.cases)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	529	apply(simp_all)[5]
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	530	defer
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	531	apply(simp)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	532	apply(erule Prf.cases)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	533	apply(simp_all)[5]
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	534	apply(simp)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	535	apply(case_tac "nullable rexp1")
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	536	apply(simp)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	537	apply(erule Prf.cases)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	538	apply(simp_all)[5]
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	539	apply(auto)[1]
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	540	apply(erule Prf.cases)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	541	apply(simp_all)[5]
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	542	apply(auto)[1]
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	543	apply (metis list.distinct(1) v4)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	544	apply(auto)[1]
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	545	apply (metis mkeps_flat)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	546	apply(auto)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	547	apply(erule Prf.cases)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	548	apply(simp_all)[5]
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	549	apply(auto)[1]
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	550	apply(simp add: v4)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	551	done
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	552
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	553	lemma Le_2a: "(head (flat v) = None) = (flat v = [])"
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	554	apply(induct v)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	555	apply(simp_all)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	556	apply (metis Nil_is_append_conv head.elims option.distinct(1))
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	557	done
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	558
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	559	lemma v5:
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	560	assumes "\<turnstile> v : der c r" "POSIX v (der c r)"
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	561	shows "POSIX (injval r c v) r"
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	562	using assms
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	563	apply(induct arbitrary: v rule: der.induct)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	564	apply(simp)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	565	apply(erule Prf.cases)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	566	apply(simp_all)[5]
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	567	apply(simp)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	568	apply(erule Prf.cases)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	569	apply(simp_all)[5]
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	570	apply(simp)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	571	apply(case_tac "c = c'")
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	572	apply(auto simp add: POSIX_def)[1]
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	573	apply(erule Prf.cases)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	574	apply(simp_all)[5]
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	575	apply(erule Prf.cases)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	576	apply(simp_all)[5]
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	577	apply (metis ValOrd.intros(7))
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	578	apply(erule Prf.cases)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	579	apply(simp_all)[5]
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	580	prefer 2
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	581	apply(simp)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	582	apply(case_tac "nullable r1")
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	583	apply(simp)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	584	defer
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	585	apply(simp)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	586	apply(erule Prf.cases)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	587	apply(simp_all)[5]
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	588	apply(auto)[1]
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	589	apply(drule POSIX_SEQ)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	590	apply(assumption)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	591	apply(assumption)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	592	apply(auto)[1]
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	593	apply(rule POSIX_SEQ_I)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	594	apply metis
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	595	apply(simp)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	596	apply(simp)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	597	apply(erule Prf.cases)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	598	apply(simp_all)[5]
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	599	apply(auto)[1]
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	600	apply(drule POSIX_ALT)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	601	apply(rule POSIX_ALT_I1)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	602	apply metis
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	603	defer
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	604	apply(erule Prf.cases)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	605	apply(simp_all)[5]
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	606	apply(auto)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	607	apply(rotate_tac 5)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	608	apply(erule Prf.cases)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	609	apply(simp_all)[5]
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	610	apply(auto)[1]
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	611	apply(drule POSIX_ALT)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	612	apply(drule POSIX_SEQ)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	613	apply(simp)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	614	apply(simp)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	615	apply(rule POSIX_SEQ_I)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	616	apply metis
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	617	apply(simp)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	618	apply(drule POSIX_ALT1a)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	619	apply(rule POSIX_SEQ_I)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	620	apply (metis mkeps_POSIX)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	621	apply(metis)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	622	apply(frule POSIX_ALT1a)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	623	apply(rotate_tac 1)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	624	apply(drule_tac x="v2" in meta_spec)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	625	apply(simp)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	626	apply(rule POSIX_ALT_I2)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	627	apply(simp)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	628	apply(frule POSIX_ALT1a)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	629	apply(auto)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	630	apply(subst v4)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	631	apply(simp)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	632	apply(simp)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	633	apply(case_tac "\<exists>r. v2 \<succ>r v'")
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	634	apply (metis ValOrd_length le_neq_implies_less less_Suc_eq)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	635	apply(auto)[1]
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	636	apply(frule_tac x="der c r2" in spec)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	637	apply(subgoal_tac "\<not>(Right v2 \<succ>(ALT (der c r1) (der c r2)) Right v')")
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	638	prefer 2
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	639	apply(rule notI)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	640	apply(erule ValOrd.cases)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	641	apply(simp_all)[7]
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	642	apply(subst (asm) (1) POSIX_def)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	643	apply(simp)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	644	apply(subgoal_tac "(\<not> \<turnstile> Right v' : ALT (der c r1) (der c r2)) \<or> (flats v2 \<noteq> flats v')")
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	645	prefer 2
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	646	apply (metis flats.simps(4))
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	647	apply(simp)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	648	apply(auto)[1]
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	649	apply(subst v4)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	650	apply(simp)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	651	apply(simp)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	652	apply(case_tac "v2 \<succ>r1 v'")
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	653	apply (metis ValOrd_length le_neq_implies_less less_Suc_eq)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	654	apply(
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	655
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	656	apply(drule_tac x="projval (ALT r1 r2) c v'" in spec)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	657	apply(drule mp)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	658	apply(auto)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	659	apply(frule POSIX_ALT1b)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	660	apply(auto)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	661	apply(subst v4)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	662	apply(simp)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	663	apply(simp)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	664	apply(simp add: flats_flat)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	665	apply(rotate_tac 1)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	666	apply(drule_tac x="v2" in meta_spec)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	667	apply(simp)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	668	apply(rule POSIX_ALT_I2)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	669	apply(simp)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	670	apply(auto)[1]
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	671	apply(subst v4)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	672	apply(simp)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	673	defer
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	674	apply(erule Prf.cases)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	675	apply(simp_all)[5]
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	676	apply(auto)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	677	apply(rotate_tac 5)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	678	apply(erule Prf.cases)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	679	apply(simp_all)[5]
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	680	apply(auto)[1]
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	681	apply(drule POSIX_ALT)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	682	apply(drule POSIX_SEQ)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	683	apply(simp)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	684	apply(simp)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	685	apply(rule POSIX_SEQ_I)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	686	apply metis
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	687	apply(simp)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	688	apply(drule POSIX_ALT1a)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	689	apply(rule POSIX_SEQ_I)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	690	apply (metis mkeps_POSIX)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	691	apply metis
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	692	apply(drule_tac x="projval r1 c v'" in meta_spec)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	693	apply(drule meta_mp)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	694	defer
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	695	apply(drule meta_mp)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	696	defer
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	697	apply(subst (asm) (1) POSIX_def)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	698	apply(simp)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	699
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	700
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	701
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	702	lemma inj_proj_id:
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	703	assumes "\<turnstile> v : r" "POSIX v r" "head (flat v) = Some c"
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	704	shows "injval r c (projval r c v) = v"
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	705	using assms
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	706	apply(induct v r arbitrary: rule: Prf.induct)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	707	apply(simp)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	708	apply(auto)[1]
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	709
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	710	apply(simp)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	711	apply(frule POSIX_head)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	712	apply(assumption)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	713	apply(simp)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	714	apply(drule meta_mp)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	715
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	716	apply(frule POSIX_E1)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	717	apply(erule Prf.cases)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	718	apply(simp_all)[7]
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	719	apply(frule POSIX_E1)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	720	apply(erule Prf.cases)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	721	apply(simp_all)[7]
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	722	apply(frule POSIX_E1)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	723	apply(erule Prf.cases)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	724	apply(simp_all)[7]
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	725	apply(frule POSIX_E1)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	726	defer
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	727	apply(frule POSIX_E1)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	728	apply(erule Prf.cases)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	729	apply(simp_all)[7]
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	730	apply(auto)[1]
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	731
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	732	apply(simp)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	733	apply(erule Prf.cases)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	734	apply(simp_all)[7]
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	735	apply(simp)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	736	apply(case_tac "c = char")
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	737	apply(simp)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	738	apply(erule Prf.cases)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	739	apply(simp_all)[7]
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	740	apply(simp)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	741	apply(erule Prf.cases)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	742	apply(simp_all)[7]
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	743
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	744
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	745	lemma POSIX_head:
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	746	assumes "POSIX (Stars (v#vs)) (STAR r)" "head (flat v @ flat (Stars vs)) = Some c"
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	747	shows "head (flat v) = Some c"
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	748	using assms
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	749	apply(rule_tac ccontr)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	750	apply(frule POSIX_E1)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	751	apply(drule Le_1)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	752	apply(assumption)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	753	apply(auto)[1]
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	754	apply(auto simp add: POSIX_def)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	755	apply(drule_tac x="Stars (v'#vs')" in spec)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	756	apply(simp)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	757	apply(simp add: ValOrd_eq_def)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	758	apply(auto)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	759	apply(erule ValOrd.cases)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	760	apply(simp_all)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	761	apply(auto)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	762	using Le_2
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	763
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	764	by (metis Le_2 Le_2a head1)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	765
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	766
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	767	lemma inj_proj_id:
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	768	assumes "\<turnstile> v : r" "POSIX v r" "head (flat v) = Some c"
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	769	shows "injval r c (projval r c v) = v"
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	770	using assms
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	771	apply(induct r arbitrary: rule: Prf.induct)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	772	apply(simp)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	773	apply(simp)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	774	apply(frule POSIX_head)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	775	apply(assumption)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	776	apply(simp)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	777	apply(drule meta_mp)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	778
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	779	apply(frule POSIX_E1)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	780	apply(erule Prf.cases)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	781	apply(simp_all)[7]
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	782	apply(frule POSIX_E1)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	783	apply(erule Prf.cases)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	784	apply(simp_all)[7]
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	785	apply(frule POSIX_E1)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	786	apply(erule Prf.cases)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	787	apply(simp_all)[7]
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	788	apply(frule POSIX_E1)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	789	defer
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	790	apply(frule POSIX_E1)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	791	apply(erule Prf.cases)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	792	apply(simp_all)[7]
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	793	apply(auto)[1]
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	794
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	795	apply(simp)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	796	apply(erule Prf.cases)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	797	apply(simp_all)[7]
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	798	apply(simp)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	799	apply(case_tac "c = char")
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	800	apply(simp)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	801	apply(erule Prf.cases)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	802	apply(simp_all)[7]
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	803	apply(simp)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	804	apply(erule Prf.cases)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	805	apply(simp_all)[7]
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	806	defer
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	807	apply(simp)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	808	apply(erule Prf.cases)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	809	apply(simp_all)[7]
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	810	apply(simp)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	811	apply(erule Prf.cases)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	812	apply(simp_all)[7]
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	813	apply(auto)[1]
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	814	apply(rotate_tac 2)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	815	apply(erule Prf.cases)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	816	apply(simp_all)[7]
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	817	apply(case_tac "nullable rexp1")
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	818	apply(simp)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	819	apply(erule Prf.cases)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	820	apply(simp_all)[7]
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	821	apply(auto)[1]
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	822	apply(erule Prf.cases)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	823	apply(simp_all)[7]
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	824	apply(auto)[1]
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	825	apply(simp add: v4)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	826	apply(auto)[1]
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	827	apply(simp add: v2a)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	828	apply(simp only: der.simps)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	829	apply(simp)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	830	apply(erule Prf.cases)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	831	apply(simp_all)[7]
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	832	apply(auto)[1]
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	833	apply(simp add: v4)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	834	done
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	835
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	836
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	837
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	838	lemma STAR_obtain:
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	839	assumes "\<turnstile> v : STAR r"
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	840	obtains vs where "\<turnstile> Stars vs : STAR r" and "v = Stars vs"
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	841	using assms
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	842	by (smt Prf.cases rexp.distinct(17) rexp.distinct(23) rexp.distinct(27) rexp.distinct(29))
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	843
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	844	fun first :: "val \<Rightarrow> char option"
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	845	where
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	846	"first Void = None"
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	847	\| "first (Char c) = Some c"
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	848	\| "first (Seq v1 v2) = (if (\<exists>c. first v1 = Some c) then first v1 else first v2)"
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	849	\| "first (Right v) = first v"
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	850	\| "first (Left v) = first v"
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	851	\| "first (Stars []) = None"
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	852	\| "first (Stars (v#vs)) = (if (\<exists>c. first v = Some c) then first v else first (Stars vs))"
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	853
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	854	lemma flat:
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	855	shows "flat v = [] \<longleftrightarrow> first v = None"
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	856	and "flat (Stars vs) = [] \<longleftrightarrow> first (Stars vs) = None"
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	857	apply(induct v and vs)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	858	apply(auto)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	859	done
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	860
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	861	lemma first:
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	862	shows "first v = Some c \<Longrightarrow> head (flat v @ ys) = Some c"
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	863	apply(induct arbitrary: ys rule: first.induct)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	864	apply(auto split: if_splits simp add: flat[symmetric])
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	865	done
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	866
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	867
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	868
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	869	lemma v5:
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	870	assumes "POSIX v r" "head (flat v) = Some c"
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	871	shows "\<turnstile> projval r c v : der c r"
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	872	using assms
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	873	apply(induct r arbitrary: c v rule: rexp.induct)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	874	prefer 6
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	875	apply(frule POSIX_E1)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	876	apply(erule Prf.cases)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	877	apply(simp_all)[7]
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	878	apply(rule Prf.intros)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	879	apply(drule_tac x="c" in meta_spec)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	880	apply(drule_tac x="va" in meta_spec)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	881	apply(drule meta_mp)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	882	apply(simp add: POSIX_def)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	883	apply(auto)[1]
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	884	apply(drule_tac x="Stars (v'#vs)" in spec)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	885	apply(simp)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	886	apply(drule mp)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	887	apply (metis Prf.intros(2))
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	888	apply(simp add: ValOrd_eq_def)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	889	apply(erule disjE)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	890	apply(simp)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	891	apply(erule ValOrd.cases)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	892	apply(simp_all)[10]
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	893	apply(drule_tac meta_mp)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	894	apply(drule head1)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	895	apply(auto)[1]
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	896	apply(simp add: POSIX_def)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	897	apply(auto)[1]
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	898	apply(drule_tac x="Stars (va#vs)" in spec)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	899	apply(simp)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	900	prefer 6
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	901	apply(simp)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	902	apply(auto split: if_splits)[1]
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	903	apply(erule Prf.cases)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	904	apply(simp_all)[7]
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	905	apply(rule Prf.intros)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	906	apply metis
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	907	apply(simp)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	908	apply(erule Prf.cases)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	909	apply(simp_all)[7]
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	910	apply(auto split: if_splits)[1]
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	911	apply(rule Prf.intros)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	912	apply(auto split: if_splits)[1]
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	913	apply(erule Prf.cases)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	914	apply(simp_all)[7]
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	915	apply(auto)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	916	apply(case_tac "char = c")
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	917	apply(simp)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	918	apply(rule Prf.intros)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	919	apply(simp)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	920	apply(erule Prf.cases)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	921	apply(simp_all)[
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	922
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	923
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	924	lemma uu:
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	925	assumes ih: "\<And>v c. \<lbrakk>head (flat v) = Some c\<rbrakk> \<Longrightarrow> \<turnstile> projval rexp c v : der c rexp"
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	926	assumes "\<turnstile> Stars vs : STAR rexp"
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	927	and "first (Stars (v#vs)) = Some c"
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	928	shows "\<turnstile> projval rexp c v : der c rexp"
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	929	using assms(2,3)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	930	apply(induct vs)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	931	apply(simp_all)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	932	apply(auto split: if_splits)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	933	apply (metis first head1 ih)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	934	apply (metis first head1 ih)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	935
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	936	apply(auto)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	937
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	938	lemma v5:
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	939	assumes "\<turnstile> v : r" "head (flat v) = Some c"
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	940	shows "\<turnstile> projval r c v : der c r"
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	941	using assms
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	942	apply(induct r arbitrary: v c rule: rexp.induct)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	943	apply(simp)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	944	apply(erule Prf.cases)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	945	apply(simp_all)[7]
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	946	apply(erule Prf.cases)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	947	apply(simp_all)[7]
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	948	apply(case_tac "char = c")
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	949	apply(simp)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	950	apply(rule Prf.intros)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	951	apply(simp)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	952	apply(erule Prf.cases)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	953	apply(simp_all)[7]
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	954	prefer 3
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	955	proof -
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	956	fix rexp v c vs
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	957	assume ih: "\<And>v c. \<lbrakk>\<turnstile> v : rexp; head (flat v) = Some c\<rbrakk> \<Longrightarrow> \<turnstile> projval rexp c v : der c rexp"
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	958	assume a: "head (flat (Stars vs)) = Some c"
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	959	assume b: "\<turnstile> Stars vs : STAR rexp"
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	960	have c: "first (Stars vs) = Some c \<Longrightarrow> \<turnstile> (hd vs) : rexp \<Longrightarrow> \<turnstile> projval rexp c (hd vs) : der c rexp"
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	961	using b
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	962	apply(induct arbitrary: rule: Prf.induct)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	963	apply(simp_all)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	964	apply(case_tac "\<exists>c. first v = Some c")
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	965	apply(auto)[1]
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	966	apply(rule ih)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	967	apply(simp)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	968	apply (metis append_Nil2 first)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	969	apply(auto)[1]
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	970	apply(simp)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	971	apply(auto split: if_splits)[1]
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	972	apply (metis append_Nil2 first ih)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	973	apply(drule_tac x="v" in meta_spec)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	974	apply(simp)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	975	apply(rotate_tac 1)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	976	apply(erule Prf.cases)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	977	apply(simp_all)[7]
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	978	apply(drule_tac x="v" in meta_spec)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	979	apply(simp)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	980	using a
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	981	apply(rotate_tac 1)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	982	apply(erule Prf.cases)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	983	apply(simp_all)[7]
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	984
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	985
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	986	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))
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	987
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	988	apply(auto)[1]
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	989	apply(case_tac "\<exists>c. first a = Some c")
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	990	apply(auto)[1]
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	991	apply(rule ih)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	992	apply(simp)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	993	apply (metis append_Nil2 first ih)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	994	apply(auto)[1]
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	995	apply(case_tac "\<exists>c. first a = Some c")
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	996	apply(auto)[1]
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	997	apply(rule ih)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	998	apply(simp)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	999	apply(auto)[1]
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1000
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1001	apply(erule Prf.cases)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1002	apply(simp_all)[7]
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1003	apply (metis append_Nil2 first)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1004	apply(simp)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1005	apply(simp add: )
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1006	apply(simp add: flat)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1007	apply(erule Prf.cases)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1008	apply(simp_all)[7]
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1009	apply(rule Prf.intros)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1010	*)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1011	show "\<turnstile> projval (STAR rexp) c (Stars vs) : SEQ (der c rexp) (STAR rexp)"
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1012	using b a
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1013	apply -
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1014	apply(erule Prf.cases)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1015	apply(simp_all)[7]
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1016	apply(drule head1)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1017	apply(auto)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1018	apply(rule Prf.intros)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1019	apply(rule ih)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1020	apply(simp_all)[3]
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1021	using k
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1022	apply -
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1023	apply(rule Prf.intros)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1024	apply(auto)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1025
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1026	apply(simp)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1027	apply(erule Prf.cases)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1028	apply(simp_all)[7]
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1029	apply(rule Prf.intros)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1030	defer
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1031	apply(rotate_tac 1)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1032	apply(erule Prf.cases)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1033	apply(simp_all)[7]
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1034	apply(drule_tac meta_mp)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1035	apply(erule Prf.cases)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1036	apply(simp_all)[7]
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1037	apply(rule ih)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1038	apply(case_tac vs)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1039	apply(simp)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1040	apply(simp)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1041	apply(rotate_tac 3)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1042	apply(erule Prf.cases)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1043	apply(simp_all)[7]
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1044	apply(auto)[1]
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1045	apply (metis Prf.intros(1) Prf.intros(3))
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1046	apply(simp)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1047
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1048	apply(drule head1)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1049	apply(auto)[1]
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1050	apply (metis Prf.intros(3))
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1051
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1052
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1053	apply (metis Prf.intros)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1054	apply(case_tac "nullable r1")
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1055	apply(simp)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1056	apply(erule Prf.cases)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1057	apply(simp_all)[7]
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1058	apply(auto)[1]
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1059	apply (metis Prf.intros(5))
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1060	apply (metis Prf.intros(3) Prf.intros(4) head1)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1061	apply(simp)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1062	apply(erule Prf.cases)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1063	apply(simp_all)[7]
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1064	apply(auto)[1]
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1065	apply (metis nullable_correctness v1)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1066	apply(drule head1)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1067	apply(auto)[1]
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1068	apply (metis Prf.intros(3))
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1069	apply(simp)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1070	apply(erule Prf.cases)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1071	apply(simp_all)[7]
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1072	apply(auto)[1]
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1073	apply(drule head1)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1074	apply(auto)[1]
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1075	apply(rule Prf.intros)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1076	apply(auto)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1077	apply(rule Prf.intros)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1078	apply(auto)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1079	apply(rotate_tac 2)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1080	apply(erule Prf.cases)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1081	apply(simp_all)[7]
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1082	apply(auto)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1083	apply(drule head1)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1084	apply(auto)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1085	apply(rule Prf.intros)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1086	apply(auto)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1087	apply(rule Prf.intros)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1088	apply(auto)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1089
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1090	defer
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1091	apply(erule Prf.cases)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1092	apply(simp_all)[7]
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1093	apply(auto)[1]
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1094	apply(rule Prf.intros)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1095	apply(auto)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1096	apply(drule head1)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1097	apply(auto)[1]
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1098	defer
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1099	apply(rotate_tac 3)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1100	apply(erule Prf.cases)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1101	apply(simp_all)[7]
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1102	apply(auto)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1103	apply(drule head1)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1104	apply(auto)[1]
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1105
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1106	apply(simp)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1107	apply(rule Prf.intros)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1108	apply(auto)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1109	apply(drule_tac x="v" in meta_spec)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1110	apply(simp)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1111	apply(erule Prf.cases)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1112	apply(simp_all)[7]
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1113	apply(auto)[1]
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1114	apply(drule head1)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1115	apply(auto)[1]
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1116	apply(rule Prf.intros)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1117	apply(auto)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1118	apply(drule meta_mp)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1119	apply(rule Prf.intros)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1120	apply(auto)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1121
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1122	apply(simp)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1123	apply (metis Prf.intros(3) head1)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1124
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1125	defer
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1126	apply(simp)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1127	apply(drule_tac head1)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1128	apply(auto)[1]
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1129	apply(rule Prf.intros)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1130	apply(rule Prf.intros)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1131	apply(simp)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1132	apply(simp)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1133	apply(rule Prf.intros)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1134	apply(simp)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1135	apply(simp)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1136	apply(rule Prf.intros)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1137	apply(simp)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1138	apply (metis nullable_correctness v1)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1139	apply(simp)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1140	apply(rule Prf.intros)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1141	apply(simp)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1142	apply(simp)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1143	apply(rule Prf.intros)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1144	apply(simp)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1145	apply(simp)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1146	apply(simp)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1147	apply(rule Prf.intros)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1148	apply(drule_tac head1)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1149	apply(auto)[1]
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1150	apply (metis Prf.intros(3))
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1151	apply(rotate_tac 2)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1152	apply(erule Prf.cases)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1153	apply(simp_all)[7]
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1154	apply(auto)[1]
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1155	apply(rule Prf.intros)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1156	defer
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1157	apply(drule_tac x="c" in meta_spec)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1158	apply(simp)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1159	apply(rotate_tac 6)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1160	apply(erule Prf.cases)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1161	apply(simp_all)[7]
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1162	apply(auto)[1]
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1163	apply(rule Prf.intros)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1164	apply(auto)[2]
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1165	apply(drule v1)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1166	apply(simp)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1167	apply(rule Prf.intros)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1168	apply(simp add: nullable_correctness[symmetric])
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1169	apply(rotate_tac 1)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1170	apply(erule Prf.cases)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1171	apply(simp_all)[7]
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1172	apply(auto)[1]
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1173	apply(drule head1)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1174	apply(auto)[1]
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1175	apply(rule Prf.intros)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1176	apply(simp)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1177	apply(simp)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1178	apply(simp)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1179
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1180	lemma inj_proj_id:
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1181	assumes "\<turnstile> v : r" "head (flat v) = Some c"
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1182	shows "injval r c (projval r c v) = v"
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1183	using assms
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1184	apply(induct arbitrary: c rule: Prf.induct)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1185	apply(simp)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1186	apply(simp)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1187	apply(drule head1)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1188	apply(auto)[1]
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1189	apply(rotate_tac 2)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1190	apply(erule Prf.cases)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1191	apply(simp_all)[7]
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1192	apply(auto)[1]
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1193	apply(drule head1)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1194	apply(auto)[1]
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1195	apply(simp)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1196	apply(erule Prf.cases)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1197	apply(simp_all)[7]
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1198	apply(simp)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1199	apply(case_tac "ca = c'")
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1200	apply(simp)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1201	apply(erule Prf.cases)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1202	apply(simp_all)[7]
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1203	apply(simp)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1204	apply(erule Prf.cases)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1205	apply(simp_all)[7]
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1206	defer
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1207	apply(simp)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1208	apply(case_tac "nullable r1")
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1209	apply(simp)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1210	apply(erule Prf.cases)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1211	apply(simp_all)[7]
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1212	apply(auto)[1]
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1213	apply(erule Prf.cases)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1214	apply(simp_all)[7]
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1215	apply(auto)[1]
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1216	apply(rotate_tac 2)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1217	apply(erule Prf.cases)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1218	apply(simp_all)[7]
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1219	apply(simp)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1220	apply(case_tac "nullable rexp1")
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1221	apply(simp)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1222	apply(erule Prf.cases)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1223	apply(simp_all)[7]
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1224	apply(auto)[1]
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1225	apply(erule Prf.cases)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1226	apply(simp_all)[7]
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1227	apply(auto)[1]
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1228	apply(simp add: v4)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1229	apply(auto)[1]
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1230	apply(simp add: v2a)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1231	apply(simp only: der.simps)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1232	apply(simp)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1233	apply(erule Prf.cases)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1234	apply(simp_all)[7]
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1235	apply(auto)[1]
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1236	apply(simp add: v4)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1237	done
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1238
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1239
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1240
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1241	lemma POSIX_I:
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1242	assumes "\<turnstile> v : r" "\<And>v'. \<turnstile> v' : r \<Longrightarrow> flat v = flat v' \<Longrightarrow> v \<succeq>r v'"
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1243	shows "POSIX v r"
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1244	using assms
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1245	unfolding POSIX_def
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1246	apply(auto)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1247	done
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1248
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1249	lemma DISJ:
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1250	"(\<not> A \<Longrightarrow> B) \<Longrightarrow> A \<or> B"
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1251	by metis
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1252
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1253	lemma DISJ2:
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1254	"\<not>(A \<and> B) \<longleftrightarrow> \<not>A \<or> \<not>B"
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1255	by metis
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1256
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1257	lemma APP: "xs @ [] = xs" by simp
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1258
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1259	lemma v5:
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1260	assumes "POSIX v (der c r)"
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1261	shows "POSIX (injval r c v) r"
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1262	using assms
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1263	apply(induct arbitrary: v rule: der.induct)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1264	apply(simp)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1265	apply(auto simp add: POSIX_def)[1]
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1266	apply(erule Prf.cases)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1267	apply(simp_all)[7]
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1268	apply(erule Prf.cases)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1269	apply(simp_all)[7]
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1270	apply(auto simp add: POSIX_def)[1]
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1271	apply(erule Prf.cases)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1272	apply(simp_all)[7]
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1273	apply(erule Prf.cases)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1274	apply(simp_all)[7]
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1275	apply(case_tac "c = c'")
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1276	apply(auto simp add: POSIX_def)[1]
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1277	apply(erule Prf.cases)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1278	apply(simp_all)[7]
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1279	apply(rule Prf.intros)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1280	apply(erule Prf.cases)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1281	apply(simp_all)[7]
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1282	apply(simp add: ValOrd_eq_def)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1283	apply(erule Prf.cases)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1284	apply(simp_all)[7]
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1285	apply(simp)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1286	apply(auto simp add: POSIX_def)[1]
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1287	apply(erule Prf.cases)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1288	apply(simp_all)[7]
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1289	apply(erule Prf.cases)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1290	apply(simp_all)[7]
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1291	prefer 3
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1292	apply(simp)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1293	apply(frule POSIX_E1)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1294	apply(erule Prf.cases)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1295	apply(simp_all)[7]
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1296	apply(auto)[1]
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1297	apply(drule_tac x="v1" in meta_spec)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1298	apply(drule meta_mp)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1299	apply(rule POSIX_I)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1300	apply(simp)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1301	apply(simp add: POSIX_def)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1302	apply(auto)[1]
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1303	apply(drule_tac x="Seq v' v2" in spec)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1304	apply(simp)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1305	apply(drule mp)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1306	apply (metis Prf.intros(3))
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1307	apply(simp add: ValOrd_eq_def)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1308	apply(erule disjE)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1309	apply(simp)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1310	apply(erule ValOrd.cases)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1311	apply(simp_all)[10]
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1312	apply(subgoal_tac "\<exists>vs2. v2 = Stars vs2")
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1313	prefer 2
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1314	apply(rotate_tac 2)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1315	apply(erule Prf.cases)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1316	apply(auto)[7]
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1317	apply(erule exE)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1318	apply(clarify)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1319	apply(simp only: injval.simps)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1320	apply(case_tac "POSIX (Stars (injval r c v1 # vs2)) (STAR r)")
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1321	apply(simp)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1322	apply(subgoal_tac "\<exists>v'' vs''. Stars (v''#vs'') \<succ>(STAR r) Stars (injval r c v1 # vs2)")
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1323	apply(erule exE)+
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1324	apply(erule ValOrd.cases)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1325	apply(simp_all)[8]
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1326	apply(auto)[1]
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1327	apply(subst (asm) (2) POSIX_def)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1328
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1329
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1330	prefer 2
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1331	apply(subst (asm) (3) POSIX_def)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1332	apply(simp)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1333	apply(drule mp)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1334	apply (metis Prf.intros(2) v3)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1335	apply(erule exE)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1336	apply(auto)[1]
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1337
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1338	apply
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1339	apply(subgoal_tac "\<turnstile> Stars (injval r c v1 # vs2) : STAR r")
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1340	apply(simp)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1341	apply(case_tac "flat () = []")
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1342
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1343	apply(rule POSIX_I)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1344	apply (metis POSIX_E1 der.simps(6) v3)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1345	apply(rotate_tac 2)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1346	apply(erule Prf.cases)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1347	defer
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1348	defer
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1349	apply(simp_all)[5]
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1350	prefer 4
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1351	apply(clarify)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1352	apply(simp only: v4 flat.simps injval.simps)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1353	prefer 4
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1354	apply(clarify)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1355	apply(simp only: v4 APP flat.simps injval.simps)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1356	prefer 2
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1357	apply(erule Prf.cases)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1358	apply(simp_all)[7]
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1359	apply(clarify)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1360
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1361
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1362	apply(simp add: ValOrd_eq_def)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1363	apply(subst (asm) POSIX_def)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1364	apply(erule conjE)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1365	apply(drule_tac x="va" in spec)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1366	apply(simp)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1367	apply(simp add: v4)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1368	apply(simp add: ValOrd_eq_def)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1369	apply(simp)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1370	apply(rule disjI2)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1371	apply(rule ValOrd.intros)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1372	apply(rotate_tac 2)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1373	apply(subst (asm) POSIX_def)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1374	apply(simp)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1375	apply(auto)[1]
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1376	apply(drule_tac x="v" in spec)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1377	apply(simp)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1378	apply(drule mp)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1379	prefer 2
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1380	apply(simp add: ValOrd_eq_def)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1381	apply(auto)[1]
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1382
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1383	apply(case_tac "injval rb c v1 = v \<and> [] = vs")
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1384	apply(simp)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1385	apply(simp only: DISJ2)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1386	apply(rule disjI2)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1387	apply(erule disjE)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1388
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1389
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1390	apply(auto)[1]
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1391	apply (metis list.distinct(1) v4)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1392	apply(auto)[1]
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1393	apply(simp add: ValOrd_eq_def)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1394	apply(rule DISJ)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1395	apply(simp only: DISJ2)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1396	apply(erule disjE)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1397	apply(rule ValOrd.intros)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1398	apply(subst (asm) POSIX_def)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1399	apply(auto)[1]
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1400
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1401	apply (metis list.distinct(1) v4)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1402	apply(subst (asm) POSIX_def)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1403	apply(auto)[1]
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1404	apply(erule Prf.cases)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1405	apply(simp_all)[7]
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1406	apply(rotate_tac 3)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1407	apply(erule Prf.cases)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1408	apply(simp_all)[7]
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1409	apply(auto)[1]
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1410	apply (metis list.distinct(1) v4)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1411	apply (metis list.distinct(1) v4)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1412	apply(clarify)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1413	apply(rotate_tac 3)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1414	apply(erule Prf.cases)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1415	apply(simp_all)[7]
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1416	prefer 2
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1417	apply(clarify)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1418	apply(simp add: ValOrd_eq_def)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1419	apply(drule_tac x="Stars (v#vs)" in spec)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1420	apply(drule mp)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1421	apply(auto)[1]
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1422
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1423	apply(simp add: ValOrd_eq_def)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1424
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1425	apply (metis POSIX_E1 der.simps(6) list.distinct(1) v4)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1426	apply(rotate_tac 3)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1427	apply(erule Prf.cases)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1428	apply(simp_all)[7]
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1429
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1430	apply(simp)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1431	apply(case_tac v2)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1432	apply(simp)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1433	apply(simp (no_asm) POSIX_def)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1434	apply(auto)[1]
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1435	apply(auto)[1]
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1436
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1437
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1438	apply (metis POSIX_E der.simps(6) v3)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1439
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1440	apply(rule Prf.intros)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1441	apply(drule_tac x="v1" in meta_spec)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1442	apply(drule meta_mp)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1443	prefer 2
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1444
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1445	apply(subgoal_tac "POSIX v1 (der c r)")
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1446	prefer 2
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1447	apply(simp add: POSIX_def)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1448	apply(auto)[1]
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1449	apply(simp add: ValOrd_eq_def)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1450	apply(auto)[1]
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1451
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1452
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1453	lemma v5:
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1454	assumes "\<turnstile> v : der c r" "POSIX v (der c r)"
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1455	shows "POSIX (injval r c v) r"
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1456	using assms
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1457	apply(induct arbitrary: v rule: der.induct)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1458	apply(simp)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1459	apply(erule Prf.cases)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1460	apply(simp_all)[7]
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1461	apply(simp)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1462	apply(erule Prf.cases)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1463	apply(simp_all)[7]
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1464	apply(simp)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1465	apply(case_tac "c = c'")
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1466	apply(simp)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1467	apply(erule Prf.cases)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1468	apply(simp_all)[7]
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1469	apply(simp add: POSIX_def)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1470	apply(auto)[1]
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1471	apply(rule Prf.intros)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1472	apply(erule Prf.cases)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1473	apply(simp_all)[7]
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1474	apply(simp add: ValOrd_eq_def)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1475	apply(erule Prf.cases)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1476	apply(simp_all)[7]
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1477	apply(simp)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1478	apply(erule Prf.cases)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1479	apply(simp_all)[7]
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1480	prefer 3
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1481	apply(simp)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1482	apply(erule Prf.cases)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1483	apply(simp_all)[7]
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1484	apply(auto)[1]
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1485	apply(case_tac "flat (Seq v1 v2) \<noteq> []")
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1486	apply(subgoal_tac "POSIX v1 (der c r)")
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1487	prefer 2
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1488	apply(simp add: POSIX_def)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1489	apply(auto)[1]
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1490
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1491
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1492	apply(drule_tac x="v1" in meta_spec)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1493	apply(simp)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1494	apply(simp (no_asm) add: POSIX_def)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1495	apply(auto)[1]
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1496	apply(rule v3)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1497	apply (metis Prf.intros(3) der.simps(6))
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1498	apply(rotate_tac 1)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1499	apply(erule Prf.cases)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1500	apply(simp_all)[7]
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1501	apply(simp add: ValOrd_eq_def)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1502	apply(rule disjI2)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1503	apply(rotate_tac 1)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1504	apply(erule Prf.cases)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1505	apply(simp_all)[7]
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1506	apply(rule ValOrd.intros)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1507	apply(simp)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1508	apply (metis list.distinct(1) v4)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1509	apply(rule ValOrd.intros)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1510	apply(simp add: POSIX_def)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1511	apply(auto)[1]
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1512	apply(rotate_tac 3)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1513	apply(erule Prf.cases)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1514	apply(simp_all)[7]
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1515	apply(simp add: ValOrd_eq_def)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1516	apply(drule_tac x="v" in spec)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1517	apply(simp)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1518	apply(auto)[1]
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1519	apply(simp)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1520
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1521	apply(simp add: POSIX_def)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1522	apply(auto)[1]
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1523	apply(
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1524
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1525	apply(rotate_tac 1)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1526	apply(erule Prf.cases)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1527	apply(simp_all)[7]
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1528	apply (metis list.distinct(1) v4)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1529	apply(rotate_tac 8)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1530	apply(erule Prf.cases)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1531	apply(simp_all)[7]
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1532	apply (metis POSIX_def ValOrd.intros(9) ValOrd_eq_def)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1533	apply(simp add: ValOrd_eq_def)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1534	apply(simp)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1535
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1536	apply(simp add: ValOrd_eq_def)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1537	apply(simp add: POSIX_def)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1538	apply(auto)[1]
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1539
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1540
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1541	apply(simp)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1542	apply(simp add: ValOrd_eq_def)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1543	apply(simp add: POSIX_def)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1544	apply(erule conjE)+
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1545	apply(drule_tac x="Seq v1 v2" in spec)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1546	apply(simp)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1547
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1548
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1549
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1550	apply(rotate_tac 2)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1551	apply(erule Prf.cases)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1552	apply(simp_all)[7]
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1553	apply(auto)[1]
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1554	apply(simp add: POSIX_def)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1555	apply(auto)[1]
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1556	apply(rule Prf.intros)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1557	apply(rule v3)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1558	apply(simp)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1559	apply(rotate_tac 5)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1560	apply(erule Prf.cases)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1561	apply(simp_all)[7]
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1562	apply(auto)[1]
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1563	apply(rotate_tac 4)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1564	apply(erule Prf.cases)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1565	apply(simp_all)[7]
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1566	apply(auto)[1]
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1567	apply(simp add: ValOrd_eq_def)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1568
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1569	apply(simp)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1570
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1571
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1572	prefer 2
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1573	apply(auto)[1]
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1574	apply(subgoal_tac "POSIX v2 (der c r2)")
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1575	apply(rotate_tac 1)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1576	apply(drule_tac x="v2" in meta_spec)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1577	apply(simp)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1578	apply(subgoal_tac "\<turnstile> Right (injval r2 c v2) : (ALT r1 r2)")
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1579	prefer 2
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1580	apply (metis Prf.intros(5) v3)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1581	apply(simp (no_asm) add: POSIX_def)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1582	apply(auto)[1]
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1583	apply(rotate_tac 6)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1584	apply(erule Prf.cases)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1585	apply(simp_all)[7]
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1586	prefer 2
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1587	apply(auto)[1]
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1588	apply(simp add: ValOrd_eq_def)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1589	apply (metis POSIX_def ValOrd.intros(5) ValOrd_eq_def)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1590	apply(auto)[1]
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1591	apply(simp add: ValOrd_eq_def)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1592
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1593
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1594	section {* Correctness Proof of the Matcher *}
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1595
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1596
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1597	section {* Left-Quotient of a Set *}
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1598
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1599	fun
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1600	zeroable :: "rexp \<Rightarrow> bool"
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1601	where
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1602	"zeroable (NULL) = True"
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1603	\| "zeroable (EMPTY) = False"
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1604	\| "zeroable (CHAR c) = False"
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1605	\| "zeroable (ALT r1 r2) = (zeroable r1 \<and> zeroable r2)"
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1606	\| "zeroable (SEQ r1 r2) = (zeroable r1 \<or> zeroable r2)"
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1607	\| "zeroable (STAR r) = False"
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1608
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1609
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1610	lemma zeroable_correctness:
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1611	shows "zeroable r \<longleftrightarrow> (L r = {})"
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1612	apply(induct r)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1613	apply(auto simp add: Seq_def)[6]
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1614	done
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1615
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1616	section {* Left-Quotient of a Set *}
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1617
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1618	definition
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1619	Der :: "char \<Rightarrow> string set \<Rightarrow> string set"
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1620	where
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1621	"Der c A \<equiv> {s. [c] @ s \<in> A}"
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1622
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1623	lemma Der_null [simp]:
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1624	shows "Der c {} = {}"
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1625	unfolding Der_def
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1626	by auto
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1627
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1628	lemma Der_empty [simp]:
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1629	shows "Der c {[]} = {}"
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1630	unfolding Der_def
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1631	by auto
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1632
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1633	lemma Der_char [simp]:
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1634	shows "Der c {[d]} = (if c = d then {[]} else {})"
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1635	unfolding Der_def
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1636	by auto
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1637
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1638	lemma Der_union [simp]:
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1639	shows "Der c (A \<union> B) = Der c A \<union> Der c B"
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1640	unfolding Der_def
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1641	by auto
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1642
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1643	lemma Der_seq [simp]:
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1644	shows "Der c (A ;; B) = (Der c A) ;; B \<union> (if [] \<in> A then Der c B else {})"
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1645	unfolding Der_def Seq_def
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1646	by (auto simp add: Cons_eq_append_conv)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1647
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1648	lemma Der_star [simp]:
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1649	shows "Der c (A\<star>) = (Der c A) ;; A\<star>"
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1650	proof -
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1651	have "Der c (A\<star>) = Der c ({[]} \<union> A ;; A\<star>)"
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1652	by (simp only: star_cases[symmetric])
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1653	also have "... = Der c (A ;; A\<star>)"
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1654	by (simp only: Der_union Der_empty) (simp)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1655	also have "... = (Der c A) ;; A\<star> \<union> (if [] \<in> A then Der c (A\<star>) else {})"
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1656	by simp
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1657	also have "... = (Der c A) ;; A\<star>"
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1658	unfolding Seq_def Der_def
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1659	by (auto dest: star_decomp)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1660	finally show "Der c (A\<star>) = (Der c A) ;; A\<star>" .
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1661	qed
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1662
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1663
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1664	lemma der_correctness:
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1665	shows "L (der c r) = Der c (L r)"
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1666	by (induct r)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1667	(simp_all add: nullable_correctness)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1668
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1669	lemma matcher_correctness:
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1670	shows "matcher r s \<longleftrightarrow> s \<in> L r"
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1671	by (induct s arbitrary: r)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1672	(simp_all add: nullable_correctness der_correctness Der_def)
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1673
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1674	section {* Examples *}
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1675
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1676	definition
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1677	"CHRA \<equiv> CHAR (CHR ''a'')"
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1678
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1679	definition
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1680	"ALT1 \<equiv> ALT CHRA EMPTY"
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1681
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1682	definition
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1683	"SEQ3 \<equiv> SEQ (SEQ ALT1 ALT1) ALT1"
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1684
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1685	value "matcher SEQ3 ''aaa''"
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1686
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1687	value "matcher NULL []"
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1688	value "matcher (CHAR (CHR ''a'')) [CHR ''a'']"
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1689	value "matcher (CHAR a) [a,a]"
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1690	value "matcher (STAR (CHAR a)) []"
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1691	value "matcher (STAR (CHAR a)) [a,a]"
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1692	value "matcher (SEQ (CHAR (CHR ''a'')) (SEQ (STAR (CHAR (CHR ''b''))) (CHAR (CHR ''c'')))) ''abbbbc''"
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1693	value "matcher (SEQ (CHAR (CHR ''a'')) (SEQ (STAR (CHAR (CHR ''b''))) (CHAR (CHR ''c'')))) ''abbcbbc''"
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1694
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1695	section {* Incorrect Matcher - fun-definition rejected *}
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1696
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1697	fun
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1698	match :: "rexp list \<Rightarrow> string \<Rightarrow> bool"
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1699	where
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1700	"match [] [] = True"
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1701	\| "match [] (c # s) = False"
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1702	\| "match (NULL # rs) s = False"
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1703	\| "match (EMPTY # rs) s = match rs s"
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1704	\| "match (CHAR c # rs) [] = False"
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1705	\| "match (CHAR c # rs) (d # s) = (if c = d then match rs s else False)"
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1706	\| "match (ALT r1 r2 # rs) s = (match (r1 # rs) s \<or> match (r2 # rs) s)"
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1707	\| "match (SEQ r1 r2 # rs) s = match (r1 # r2 # rs) s"
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1708	\| "match (STAR r # rs) s = (match rs s \<or> match (r # (STAR r) # rs) s)"
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1709
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1710
fe177dfc4697 initial version of the theory Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1711	end

author	Christian Urban <christian dot urban at kcl dot ac dot uk>
	Mon, 08 Sep 2014 14:06:15 +0100
changeset 5	fe177dfc4697
child 6	87618dae0e04
permissions	-rw-r--r--