lexing: thys/Re1.thy@45274393f28c (annotated)

10 14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1
11 26b8a5213355 changed theory name Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 10 diff changeset	2	theory Re1
10 14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	3	imports "Main"
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	4	begin
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	5
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	6	section {* Sequential Composition of Sets *}
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	7
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	8	definition
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	9	Sequ :: "string set \<Rightarrow> string set \<Rightarrow> string set" ("_ ;; _" [100,100] 100)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	10	where
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	11	"A ;; B = {s1 @ s2 \| s1 s2. s1 \<in> A \<and> s2 \<in> B}"
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	12
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	13	text {* Two Simple Properties about Sequential Composition *}
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	14
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	15	lemma seq_empty [simp]:
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	16	shows "A ;; {[]} = A"
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	17	and "{[]} ;; A = A"
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	18	by (simp_all add: Sequ_def)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	19
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	20	lemma seq_null [simp]:
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	21	shows "A ;; {} = {}"
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	22	and "{} ;; A = {}"
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	23	by (simp_all add: Sequ_def)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	24
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	25	section {* Regular Expressions *}
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	26
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	27	datatype rexp =
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	28	NULL
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	29	\| EMPTY
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	30	\| CHAR char
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	31	\| SEQ rexp rexp
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	32	\| ALT rexp rexp
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	33
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	34	section {* Semantics of Regular Expressions *}
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	35
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	36	fun
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	37	L :: "rexp \<Rightarrow> string set"
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	38	where
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	39	"L (NULL) = {}"
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	40	\| "L (EMPTY) = {[]}"
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	41	\| "L (CHAR c) = {[c]}"
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	42	\| "L (SEQ r1 r2) = (L r1) ;; (L r2)"
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	43	\| "L (ALT r1 r2) = (L r1) \<union> (L r2)"
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	44
54 45274393f28c no changes fahad parents: 53 diff changeset	45	value "L(CHAR c)"
45274393f28c no changes fahad parents: 53 diff changeset	46	value "L(SEQ(CHAR c)(CHAR b))"
45274393f28c no changes fahad parents: 53 diff changeset	47
10 14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	48
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	49	section {* Values *}
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	50
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	51	datatype val =
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	52	Void
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	53	\| Char char
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	54	\| Seq val val
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	55	\| Right val
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	56	\| Left val
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	57
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	58	section {* Relation between values and regular expressions *}
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	59
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	60	inductive Prf :: "val \<Rightarrow> rexp \<Rightarrow> bool" ("\<turnstile> _ : _" [100, 100] 100)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	61	where
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	62	"\<lbrakk>\<turnstile> v1 : r1; \<turnstile> v2 : r2\<rbrakk> \<Longrightarrow> \<turnstile> Seq v1 v2 : SEQ r1 r2"
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	63	\| "\<turnstile> v1 : r1 \<Longrightarrow> \<turnstile> Left v1 : ALT r1 r2"
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	64	\| "\<turnstile> v2 : r2 \<Longrightarrow> \<turnstile> Right v2 : ALT r1 r2"
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	65	\| "\<turnstile> Void : EMPTY"
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	66	\| "\<turnstile> Char c : CHAR c"
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	67
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	68	section {* The string behind a value *}
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	69
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	70	fun flat :: "val \<Rightarrow> string"
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	71	where
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	72	"flat(Void) = []"
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	73	\| "flat(Char c) = [c]"
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	74	\| "flat(Left v) = flat(v)"
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	75	\| "flat(Right v) = flat(v)"
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	76	\| "flat(Seq v1 v2) = flat(v1) @ flat(v2)"
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	77
54 45274393f28c no changes fahad parents: 53 diff changeset	78	value "flat(Seq(Char c)(Char b))"
45274393f28c no changes fahad parents: 53 diff changeset	79	value "flat(Right(Void))"
45274393f28c no changes fahad parents: 53 diff changeset	80
48 652861c9473f added a function for calculating values Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 20 diff changeset	81	fun flats :: "val \<Rightarrow> string list"
652861c9473f added a function for calculating values Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 20 diff changeset	82	where
652861c9473f added a function for calculating values Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 20 diff changeset	83	"flats(Void) = [[]]"
652861c9473f added a function for calculating values Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 20 diff changeset	84	\| "flats(Char c) = [[c]]"
652861c9473f added a function for calculating values Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 20 diff changeset	85	\| "flats(Left v) = flats(v)"
652861c9473f added a function for calculating values Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 20 diff changeset	86	\| "flats(Right v) = flats(v)"
652861c9473f added a function for calculating values Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 20 diff changeset	87	\| "flats(Seq v1 v2) = (flats v1) @ (flats v2)"
10 14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	88
54 45274393f28c no changes fahad parents: 53 diff changeset	89	value "flats(Seq(Char c)(Char b))"
45274393f28c no changes fahad parents: 53 diff changeset	90
10 14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	91	lemma Prf_flat_L:
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	92	assumes "\<turnstile> v : r" shows "flat v \<in> L r"
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	93	using assms
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	94	apply(induct)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	95	apply(auto simp add: Sequ_def)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	96	done
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	97
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	98	lemma L_flat_Prf:
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	99	"L(r) = {flat v \| v. \<turnstile> v : r}"
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	100	apply(induct r)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	101	apply(auto dest: Prf_flat_L simp add: Sequ_def)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	102	apply (metis Prf.intros(4) flat.simps(1))
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	103	apply (metis Prf.intros(5) flat.simps(2))
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	104	apply (metis Prf.intros(1) flat.simps(5))
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	105	apply (metis Prf.intros(2) flat.simps(3))
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	106	apply (metis Prf.intros(3) flat.simps(4))
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	107	apply(erule Prf.cases)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	108	apply(auto)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	109	done
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	110
54 45274393f28c no changes fahad parents: 53 diff changeset	111	definition definition prefix :: :: "string \<Rightarrow> string \<Rightarrow> bool" ("_ \<sqsubset> _" [100, 100] 100)
48 652861c9473f added a function for calculating values Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 20 diff changeset	112	where
652861c9473f added a function for calculating values Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 20 diff changeset	113	"s1 \<sqsubset> s2 \<equiv> \<exists>s3. s1 @ s3 = s2"
652861c9473f added a function for calculating values Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 20 diff changeset	114
10 14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	115	section {* Ordering of values *}
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	116
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	117	inductive ValOrd :: "val \<Rightarrow> rexp \<Rightarrow> val \<Rightarrow> bool" ("_ \<succ>_ _" [100, 100, 100] 100)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	118	where
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	119	"\<lbrakk>v1 = v1'; v2 \<succ>r2 v2'\<rbrakk> \<Longrightarrow> (Seq v1 v2) \<succ>(SEQ r1 r2) (Seq v1' v2')"
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	120	\| "v1 \<succ>r1 v1' \<Longrightarrow> (Seq v1 v2) \<succ>(SEQ r1 r2) (Seq v1' v2')"
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	121	\| "length (flat v1) \<ge> length (flat v2) \<Longrightarrow> (Left v1) \<succ>(ALT r1 r2) (Right v2)"
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	122	\| "length (flat v2) > length (flat v1) \<Longrightarrow> (Right v2) \<succ>(ALT r1 r2) (Left v1)"
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	123	\| "v2 \<succ>r2 v2' \<Longrightarrow> (Right v2) \<succ>(ALT r1 r2) (Right v2')"
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	124	\| "v1 \<succ>r1 v1' \<Longrightarrow> (Left v1) \<succ>(ALT r1 r2) (Left v1')"
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	125	\| "Void \<succ>EMPTY Void"
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	126	\| "(Char c) \<succ>(CHAR c) (Char c)"
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	127
53 38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	128
48 652861c9473f added a function for calculating values Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 20 diff changeset	129	section {* The ordering is reflexive *}
652861c9473f added a function for calculating values Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 20 diff changeset	130
652861c9473f added a function for calculating values Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 20 diff changeset	131	lemma ValOrd_refl:
652861c9473f added a function for calculating values Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 20 diff changeset	132	assumes "\<turnstile> v : r"
652861c9473f added a function for calculating values Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 20 diff changeset	133	shows "v \<succ>r v"
10 14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	134	using assms
48 652861c9473f added a function for calculating values Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 20 diff changeset	135	apply(induct)
652861c9473f added a function for calculating values Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 20 diff changeset	136	apply(auto intro: ValOrd.intros)
10 14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	137	done
48 652861c9473f added a function for calculating values Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 20 diff changeset	138
652861c9473f added a function for calculating values Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 20 diff changeset	139	lemma ValOrd_flats:
652861c9473f added a function for calculating values Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 20 diff changeset	140	assumes "v1 \<succ>r v2"
652861c9473f added a function for calculating values Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 20 diff changeset	141	shows "hd (flats v2) = hd (flats v1)"
652861c9473f added a function for calculating values Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 20 diff changeset	142	using assms
652861c9473f added a function for calculating values Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 20 diff changeset	143	apply(induct)
652861c9473f added a function for calculating values Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 20 diff changeset	144	apply(auto)
49 c616ec6b1e3c updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 48 diff changeset	145	oops
48 652861c9473f added a function for calculating values Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 20 diff changeset	146
10 14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	147
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	148	section {* Posix definition *}
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	149
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	150	definition POSIX :: "val \<Rightarrow> rexp \<Rightarrow> bool"
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	151	where
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	152	"POSIX v r \<equiv> (\<forall>v'. (\<turnstile> v' : r \<and> flat v = flat v') \<longrightarrow> v \<succ>r v')"
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	153
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	154	(*
11 26b8a5213355 changed theory name Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 10 diff changeset	155	an alternative definition: might cause problems
26b8a5213355 changed theory name Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 10 diff changeset	156	with theorem mkeps_POSIX
26b8a5213355 changed theory name Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 10 diff changeset	157	*)
26b8a5213355 changed theory name Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 10 diff changeset	158
26b8a5213355 changed theory name Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 10 diff changeset	159	definition POSIX2 :: "val \<Rightarrow> rexp \<Rightarrow> bool"
26b8a5213355 changed theory name Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 10 diff changeset	160	where
26b8a5213355 changed theory name Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 10 diff changeset	161	"POSIX2 v r \<equiv> \<turnstile> v : r \<and> (\<forall>v'. \<turnstile> v' : r \<longrightarrow> v \<succ>r v')"
26b8a5213355 changed theory name Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 10 diff changeset	162
20 c11651bbebf5 some small changes Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 12 diff changeset	163	definition POSIX3 :: "val \<Rightarrow> rexp \<Rightarrow> bool"
c11651bbebf5 some small changes Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 12 diff changeset	164	where
c11651bbebf5 some small changes Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 12 diff changeset	165	"POSIX3 v r \<equiv> \<turnstile> v : r \<and> (\<forall>v'. (\<turnstile> v' : r \<and> length (flat v') \<le> length(flat v)) \<longrightarrow> v \<succ>r v')"
c11651bbebf5 some small changes Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 12 diff changeset	166
11 26b8a5213355 changed theory name Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 10 diff changeset	167
10 14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	168	lemma POSIX_SEQ:
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	169	assumes "POSIX (Seq v1 v2) (SEQ r1 r2)" "\<turnstile> v1 : r1" "\<turnstile> v2 : r2"
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	170	shows "POSIX v1 r1 \<and> POSIX v2 r2"
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	171	using assms
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	172	unfolding POSIX_def
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	173	apply(auto)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	174	apply(drule_tac x="Seq v' v2" in spec)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	175	apply(simp)
48 652861c9473f added a function for calculating values Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 20 diff changeset	176	apply(erule impE)
652861c9473f added a function for calculating values Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 20 diff changeset	177	apply(rule Prf.intros)
652861c9473f added a function for calculating values Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 20 diff changeset	178	apply(simp)
652861c9473f added a function for calculating values Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 20 diff changeset	179	apply(simp)
652861c9473f added a function for calculating values Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 20 diff changeset	180	apply(erule ValOrd.cases)
652861c9473f added a function for calculating values Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 20 diff changeset	181	apply(simp_all)
652861c9473f added a function for calculating values Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 20 diff changeset	182	apply(clarify)
652861c9473f added a function for calculating values Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 20 diff changeset	183	defer
10 14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	184	apply(drule_tac x="Seq v1 v'" in spec)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	185	apply(simp)
48 652861c9473f added a function for calculating values Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 20 diff changeset	186	apply(erule impE)
652861c9473f added a function for calculating values Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 20 diff changeset	187	apply(rule Prf.intros)
652861c9473f added a function for calculating values Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 20 diff changeset	188	apply(simp)
652861c9473f added a function for calculating values Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 20 diff changeset	189	apply(simp)
652861c9473f added a function for calculating values Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 20 diff changeset	190	apply(erule ValOrd.cases)
652861c9473f added a function for calculating values Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 20 diff changeset	191	apply(simp_all)
652861c9473f added a function for calculating values Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 20 diff changeset	192	apply(clarify)
652861c9473f added a function for calculating values Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 20 diff changeset	193	oops (not true)
10 14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	194
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	195	lemma POSIX_SEQ_I:
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	196	assumes "POSIX v1 r1" "POSIX v2 r2"
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	197	shows "POSIX (Seq v1 v2) (SEQ r1 r2)"
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	198	using assms
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	199	unfolding POSIX_def
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	200	apply(auto)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	201	apply(rotate_tac 2)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	202	apply(erule Prf.cases)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	203	apply(simp_all)[5]
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	204	apply(auto)[1]
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	205	apply(rule ValOrd.intros)
48 652861c9473f added a function for calculating values Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 20 diff changeset	206	oops (* maybe also not true *)
10 14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	207
48 652861c9473f added a function for calculating values Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 20 diff changeset	208	lemma POSIX3_SEQ_I:
652861c9473f added a function for calculating values Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 20 diff changeset	209	assumes "POSIX3 v1 r1" "POSIX3 v2 r2"
652861c9473f added a function for calculating values Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 20 diff changeset	210	shows "POSIX3 (Seq v1 v2) (SEQ r1 r2)"
652861c9473f added a function for calculating values Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 20 diff changeset	211	using assms
652861c9473f added a function for calculating values Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 20 diff changeset	212	unfolding POSIX3_def
10 14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	213	apply(auto)
48 652861c9473f added a function for calculating values Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 20 diff changeset	214	apply (metis Prf.intros(1))
652861c9473f added a function for calculating values Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 20 diff changeset	215	apply(rotate_tac 4)
652861c9473f added a function for calculating values Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 20 diff changeset	216	apply(erule Prf.cases)
652861c9473f added a function for calculating values Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 20 diff changeset	217	apply(simp_all)[5]
652861c9473f added a function for calculating values Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 20 diff changeset	218	apply(auto)[1]
652861c9473f added a function for calculating values Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 20 diff changeset	219	apply(case_tac "v1 = v1a")
652861c9473f added a function for calculating values Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 20 diff changeset	220	apply(auto)
652861c9473f added a function for calculating values Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 20 diff changeset	221	apply (metis ValOrd.intros(1))
652861c9473f added a function for calculating values Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 20 diff changeset	222	apply (rule ValOrd.intros(2))
49 c616ec6b1e3c updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 48 diff changeset	223	oops
12 232ea10bed6f Delete POSIX_ALT2 fahadausaf <fahad.ausaf@icloud.com> parents: 11 diff changeset	224
232ea10bed6f Delete POSIX_ALT2 fahadausaf <fahad.ausaf@icloud.com> parents: 11 diff changeset	225	lemma POSIX_ALT2:
232ea10bed6f Delete POSIX_ALT2 fahadausaf <fahad.ausaf@icloud.com> parents: 11 diff changeset	226	assumes "POSIX (Left v1) (ALT r1 r2)"
232ea10bed6f Delete POSIX_ALT2 fahadausaf <fahad.ausaf@icloud.com> parents: 11 diff changeset	227	shows "POSIX v1 r1"
232ea10bed6f Delete POSIX_ALT2 fahadausaf <fahad.ausaf@icloud.com> parents: 11 diff changeset	228	using assms
232ea10bed6f Delete POSIX_ALT2 fahadausaf <fahad.ausaf@icloud.com> parents: 11 diff changeset	229	unfolding POSIX_def
232ea10bed6f Delete POSIX_ALT2 fahadausaf <fahad.ausaf@icloud.com> parents: 11 diff changeset	230	apply(auto)
232ea10bed6f Delete POSIX_ALT2 fahadausaf <fahad.ausaf@icloud.com> parents: 11 diff changeset	231	apply(drule_tac x="Left v'" in spec)
232ea10bed6f Delete POSIX_ALT2 fahadausaf <fahad.ausaf@icloud.com> parents: 11 diff changeset	232	apply(simp)
232ea10bed6f Delete POSIX_ALT2 fahadausaf <fahad.ausaf@icloud.com> parents: 11 diff changeset	233	apply(drule mp)
232ea10bed6f Delete POSIX_ALT2 fahadausaf <fahad.ausaf@icloud.com> parents: 11 diff changeset	234	apply(rule Prf.intros)
232ea10bed6f Delete POSIX_ALT2 fahadausaf <fahad.ausaf@icloud.com> parents: 11 diff changeset	235	apply(auto)
232ea10bed6f Delete POSIX_ALT2 fahadausaf <fahad.ausaf@icloud.com> parents: 11 diff changeset	236	apply(erule ValOrd.cases)
232ea10bed6f Delete POSIX_ALT2 fahadausaf <fahad.ausaf@icloud.com> parents: 11 diff changeset	237	apply(simp_all)
232ea10bed6f Delete POSIX_ALT2 fahadausaf <fahad.ausaf@icloud.com> parents: 11 diff changeset	238	done
232ea10bed6f Delete POSIX_ALT2 fahadausaf <fahad.ausaf@icloud.com> parents: 11 diff changeset	239
232ea10bed6f Delete POSIX_ALT2 fahadausaf <fahad.ausaf@icloud.com> parents: 11 diff changeset	240	lemma POSIX2_ALT:
232ea10bed6f Delete POSIX_ALT2 fahadausaf <fahad.ausaf@icloud.com> parents: 11 diff changeset	241	assumes "POSIX2 (Left v1) (ALT r1 r2)"
232ea10bed6f Delete POSIX_ALT2 fahadausaf <fahad.ausaf@icloud.com> parents: 11 diff changeset	242	shows "POSIX2 v1 r1"
232ea10bed6f Delete POSIX_ALT2 fahadausaf <fahad.ausaf@icloud.com> parents: 11 diff changeset	243	using assms
232ea10bed6f Delete POSIX_ALT2 fahadausaf <fahad.ausaf@icloud.com> parents: 11 diff changeset	244	unfolding POSIX2_def
232ea10bed6f Delete POSIX_ALT2 fahadausaf <fahad.ausaf@icloud.com> parents: 11 diff changeset	245	apply(auto)
20 c11651bbebf5 some small changes Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 12 diff changeset	246	oops
12 232ea10bed6f Delete POSIX_ALT2 fahadausaf <fahad.ausaf@icloud.com> parents: 11 diff changeset	247
10 14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	248	lemma POSIX_ALT:
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	249	assumes "POSIX (Left v1) (ALT r1 r2)"
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	250	shows "POSIX v1 r1"
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	251	using assms
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	252	unfolding POSIX_def
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	253	apply(auto)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	254	apply(drule_tac x="Left v'" in spec)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	255	apply(simp)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	256	apply(drule mp)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	257	apply(rule Prf.intros)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	258	apply(auto)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	259	apply(erule ValOrd.cases)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	260	apply(simp_all)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	261	done
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	262
20 c11651bbebf5 some small changes Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 12 diff changeset	263	lemma POSIX2_ALT:
c11651bbebf5 some small changes Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 12 diff changeset	264	assumes "POSIX2 (Left v1) (ALT r1 r2)"
c11651bbebf5 some small changes Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 12 diff changeset	265	shows "POSIX2 v1 r1"
c11651bbebf5 some small changes Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 12 diff changeset	266	using assms
c11651bbebf5 some small changes Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 12 diff changeset	267	apply(simp add: POSIX2_def)
c11651bbebf5 some small changes Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 12 diff changeset	268	apply(auto)
c11651bbebf5 some small changes Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 12 diff changeset	269	apply(erule Prf.cases)
c11651bbebf5 some small changes Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 12 diff changeset	270	apply(simp_all)[5]
c11651bbebf5 some small changes Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 12 diff changeset	271	apply(drule_tac x="Left v'" in spec)
c11651bbebf5 some small changes Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 12 diff changeset	272	apply(drule mp)
c11651bbebf5 some small changes Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 12 diff changeset	273	apply(rule Prf.intros)
c11651bbebf5 some small changes Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 12 diff changeset	274	apply(auto)
c11651bbebf5 some small changes Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 12 diff changeset	275	apply(erule ValOrd.cases)
c11651bbebf5 some small changes Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 12 diff changeset	276	apply(simp_all)
c11651bbebf5 some small changes Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 12 diff changeset	277	done
c11651bbebf5 some small changes Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 12 diff changeset	278
c11651bbebf5 some small changes Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 12 diff changeset	279
10 14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	280	lemma POSIX_ALT1a:
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	281	assumes "POSIX (Right v2) (ALT r1 r2)"
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	282	shows "POSIX v2 r2"
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	283	using assms
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	284	unfolding POSIX_def
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	285	apply(auto)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	286	apply(drule_tac x="Right v'" in spec)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	287	apply(simp)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	288	apply(drule mp)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	289	apply(rule Prf.intros)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	290	apply(auto)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	291	apply(erule ValOrd.cases)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	292	apply(simp_all)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	293	done
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	294
20 c11651bbebf5 some small changes Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 12 diff changeset	295	lemma POSIX2_ALT1a:
c11651bbebf5 some small changes Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 12 diff changeset	296	assumes "POSIX2 (Right v2) (ALT r1 r2)"
c11651bbebf5 some small changes Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 12 diff changeset	297	shows "POSIX2 v2 r2"
c11651bbebf5 some small changes Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 12 diff changeset	298	using assms
c11651bbebf5 some small changes Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 12 diff changeset	299	unfolding POSIX2_def
c11651bbebf5 some small changes Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 12 diff changeset	300	apply(auto)
c11651bbebf5 some small changes Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 12 diff changeset	301	apply(erule Prf.cases)
c11651bbebf5 some small changes Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 12 diff changeset	302	apply(simp_all)[5]
c11651bbebf5 some small changes Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 12 diff changeset	303	apply(drule_tac x="Right v'" in spec)
c11651bbebf5 some small changes Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 12 diff changeset	304	apply(drule mp)
c11651bbebf5 some small changes Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 12 diff changeset	305	apply(rule Prf.intros)
c11651bbebf5 some small changes Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 12 diff changeset	306	apply(auto)
c11651bbebf5 some small changes Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 12 diff changeset	307	apply(erule ValOrd.cases)
c11651bbebf5 some small changes Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 12 diff changeset	308	apply(simp_all)
c11651bbebf5 some small changes Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 12 diff changeset	309	done
c11651bbebf5 some small changes Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 12 diff changeset	310
10 14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	311
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	312	lemma POSIX_ALT1b:
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	313	assumes "POSIX (Right v2) (ALT r1 r2)"
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	314	shows "(\<forall>v'. (\<turnstile> v' : r2 \<and> flat v' = flat v2) \<longrightarrow> v2 \<succ>r2 v')"
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	315	using assms
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	316	apply(drule_tac POSIX_ALT1a)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	317	unfolding POSIX_def
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	318	apply(auto)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	319	done
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	320
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	321	lemma POSIX_ALT_I1:
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	322	assumes "POSIX v1 r1"
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	323	shows "POSIX (Left v1) (ALT r1 r2)"
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	324	using assms
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	325	unfolding POSIX_def
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	326	apply(auto)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	327	apply(rotate_tac 3)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	328	apply(erule Prf.cases)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	329	apply(simp_all)[5]
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	330	apply(auto)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	331	apply(rule ValOrd.intros)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	332	apply(auto)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	333	apply(rule ValOrd.intros)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	334	by simp
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	335
20 c11651bbebf5 some small changes Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 12 diff changeset	336	lemma POSIX2_ALT_I1:
c11651bbebf5 some small changes Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 12 diff changeset	337	assumes "POSIX2 v1 r1"
c11651bbebf5 some small changes Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 12 diff changeset	338	shows "POSIX2 (Left v1) (ALT r1 r2)"
c11651bbebf5 some small changes Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 12 diff changeset	339	using assms
c11651bbebf5 some small changes Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 12 diff changeset	340	unfolding POSIX2_def
c11651bbebf5 some small changes Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 12 diff changeset	341	apply(auto)
c11651bbebf5 some small changes Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 12 diff changeset	342	apply(rule Prf.intros)
c11651bbebf5 some small changes Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 12 diff changeset	343	apply(simp)
c11651bbebf5 some small changes Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 12 diff changeset	344	apply(rotate_tac 2)
c11651bbebf5 some small changes Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 12 diff changeset	345	apply(erule Prf.cases)
c11651bbebf5 some small changes Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 12 diff changeset	346	apply(simp_all)[5]
c11651bbebf5 some small changes Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 12 diff changeset	347	apply(auto)
c11651bbebf5 some small changes Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 12 diff changeset	348	apply(rule ValOrd.intros)
c11651bbebf5 some small changes Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 12 diff changeset	349	apply(auto)
c11651bbebf5 some small changes Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 12 diff changeset	350	apply(rule ValOrd.intros)
c11651bbebf5 some small changes Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 12 diff changeset	351	oops
c11651bbebf5 some small changes Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 12 diff changeset	352
10 14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	353	lemma POSIX_ALT_I2:
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	354	assumes "POSIX v2 r2" "\<forall>v'. \<turnstile> v' : r1 \<longrightarrow> length (flat v2) > length (flat v')"
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	355	shows "POSIX (Right v2) (ALT r1 r2)"
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	356	using assms
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	357	unfolding POSIX_def
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	358	apply(auto)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	359	apply(rotate_tac 3)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	360	apply(erule Prf.cases)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	361	apply(simp_all)[5]
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	362	apply(auto)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	363	apply(rule ValOrd.intros)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	364	apply metis
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	365	done
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	366
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	367
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	368
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	369	section {* The Matcher *}
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	370
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	371	fun
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	372	nullable :: "rexp \<Rightarrow> bool"
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	373	where
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	374	"nullable (NULL) = False"
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	375	\| "nullable (EMPTY) = True"
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	376	\| "nullable (CHAR c) = False"
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	377	\| "nullable (ALT r1 r2) = (nullable r1 \<or> nullable r2)"
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	378	\| "nullable (SEQ r1 r2) = (nullable r1 \<and> nullable r2)"
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	379
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	380	lemma nullable_correctness:
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	381	shows "nullable r \<longleftrightarrow> [] \<in> (L r)"
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	382	apply (induct r)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	383	apply(auto simp add: Sequ_def)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	384	done
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	385
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	386	fun mkeps :: "rexp \<Rightarrow> val"
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	387	where
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	388	"mkeps(EMPTY) = Void"
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	389	\| "mkeps(SEQ r1 r2) = Seq (mkeps r1) (mkeps r2)"
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	390	\| "mkeps(ALT r1 r2) = (if nullable(r1) then Left (mkeps r1) else Right (mkeps r2))"
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	391
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	392	lemma mkeps_nullable:
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	393	assumes "nullable(r)" shows "\<turnstile> mkeps r : r"
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	394	using assms
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	395	apply(induct rule: nullable.induct)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	396	apply(auto intro: Prf.intros)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	397	done
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	398
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	399	lemma mkeps_flat:
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	400	assumes "nullable(r)" shows "flat (mkeps r) = []"
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	401	using assms
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	402	apply(induct rule: nullable.induct)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	403	apply(auto)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	404	done
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	405
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	406	text {*
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	407	The value mkeps returns is always the correct POSIX
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	408	value.
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	409	*}
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	410
12 232ea10bed6f Delete POSIX_ALT2 fahadausaf <fahad.ausaf@icloud.com> parents: 11 diff changeset	411	lemma mkeps_POSIX2:
232ea10bed6f Delete POSIX_ALT2 fahadausaf <fahad.ausaf@icloud.com> parents: 11 diff changeset	412	assumes "nullable r"
232ea10bed6f Delete POSIX_ALT2 fahadausaf <fahad.ausaf@icloud.com> parents: 11 diff changeset	413	shows "POSIX2 (mkeps r) r"
232ea10bed6f Delete POSIX_ALT2 fahadausaf <fahad.ausaf@icloud.com> parents: 11 diff changeset	414	using assms
232ea10bed6f Delete POSIX_ALT2 fahadausaf <fahad.ausaf@icloud.com> parents: 11 diff changeset	415	apply(induct r)
232ea10bed6f Delete POSIX_ALT2 fahadausaf <fahad.ausaf@icloud.com> parents: 11 diff changeset	416	apply(auto)[1]
232ea10bed6f Delete POSIX_ALT2 fahadausaf <fahad.ausaf@icloud.com> parents: 11 diff changeset	417	apply(simp add: POSIX2_def)
20 c11651bbebf5 some small changes Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 12 diff changeset	418	oops
12 232ea10bed6f Delete POSIX_ALT2 fahadausaf <fahad.ausaf@icloud.com> parents: 11 diff changeset	419
48 652861c9473f added a function for calculating values Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 20 diff changeset	420	lemma mkeps_POSIX3:
652861c9473f added a function for calculating values Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 20 diff changeset	421	assumes "nullable r"
652861c9473f added a function for calculating values Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 20 diff changeset	422	shows "POSIX3 (mkeps r) r"
652861c9473f added a function for calculating values Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 20 diff changeset	423	using assms
652861c9473f added a function for calculating values Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 20 diff changeset	424	apply(induct r)
652861c9473f added a function for calculating values Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 20 diff changeset	425	apply(auto)[1]
652861c9473f added a function for calculating values Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 20 diff changeset	426	apply(simp add: POSIX3_def)
652861c9473f added a function for calculating values Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 20 diff changeset	427	apply(auto)[1]
652861c9473f added a function for calculating values Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 20 diff changeset	428	apply (metis Prf.intros(4))
652861c9473f added a function for calculating values Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 20 diff changeset	429	apply(erule Prf.cases)
652861c9473f added a function for calculating values Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 20 diff changeset	430	apply(simp_all)[5]
652861c9473f added a function for calculating values Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 20 diff changeset	431	apply (metis ValOrd.intros)
652861c9473f added a function for calculating values Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 20 diff changeset	432	apply(simp add: POSIX3_def)
652861c9473f added a function for calculating values Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 20 diff changeset	433	apply(auto)[1]
652861c9473f added a function for calculating values Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 20 diff changeset	434	apply(simp add: POSIX3_def)
652861c9473f added a function for calculating values Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 20 diff changeset	435	apply(auto)[1]
652861c9473f added a function for calculating values Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 20 diff changeset	436	apply (metis mkeps.simps(2) mkeps_nullable nullable.simps(5))
652861c9473f added a function for calculating values Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 20 diff changeset	437	apply(rotate_tac 6)
652861c9473f added a function for calculating values Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 20 diff changeset	438	apply(erule Prf.cases)
652861c9473f added a function for calculating values Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 20 diff changeset	439	apply(simp_all)[5]
652861c9473f added a function for calculating values Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 20 diff changeset	440	apply (metis ValOrd.intros(2) add_leE gen_length_code(1) gen_length_def mkeps_flat)
652861c9473f added a function for calculating values Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 20 diff changeset	441	apply(auto)
652861c9473f added a function for calculating values Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 20 diff changeset	442	apply(simp add: POSIX3_def)
652861c9473f added a function for calculating values Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 20 diff changeset	443	apply(auto)
652861c9473f added a function for calculating values Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 20 diff changeset	444	apply (metis Prf.intros(2))
652861c9473f added a function for calculating values Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 20 diff changeset	445	apply(rotate_tac 4)
652861c9473f added a function for calculating values Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 20 diff changeset	446	apply(erule Prf.cases)
652861c9473f added a function for calculating values Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 20 diff changeset	447	apply(simp_all)[5]
652861c9473f added a function for calculating values Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 20 diff changeset	448	apply (metis ValOrd.intros(6))
652861c9473f added a function for calculating values Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 20 diff changeset	449	apply(auto)[1]
652861c9473f added a function for calculating values Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 20 diff changeset	450	apply (metis ValOrd.intros(3))
652861c9473f added a function for calculating values Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 20 diff changeset	451	apply(simp add: POSIX3_def)
652861c9473f added a function for calculating values Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 20 diff changeset	452	apply(auto)
652861c9473f added a function for calculating values Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 20 diff changeset	453	apply (metis Prf.intros(2))
652861c9473f added a function for calculating values Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 20 diff changeset	454	apply(rotate_tac 6)
652861c9473f added a function for calculating values Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 20 diff changeset	455	apply(erule Prf.cases)
652861c9473f added a function for calculating values Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 20 diff changeset	456	apply(simp_all)[5]
652861c9473f added a function for calculating values Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 20 diff changeset	457	apply (metis ValOrd.intros(6))
652861c9473f added a function for calculating values Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 20 diff changeset	458	apply (metis ValOrd.intros(3))
652861c9473f added a function for calculating values Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 20 diff changeset	459	apply(simp add: POSIX3_def)
652861c9473f added a function for calculating values Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 20 diff changeset	460	apply(auto)
652861c9473f added a function for calculating values Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 20 diff changeset	461	apply (metis Prf.intros(3))
652861c9473f added a function for calculating values Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 20 diff changeset	462	apply(rotate_tac 5)
652861c9473f added a function for calculating values Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 20 diff changeset	463	apply(erule Prf.cases)
652861c9473f added a function for calculating values Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 20 diff changeset	464	apply(simp_all)[5]
652861c9473f added a function for calculating values Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 20 diff changeset	465	apply (metis Prf_flat_L drop_0 drop_all list.size(3) mkeps_flat nullable_correctness)
652861c9473f added a function for calculating values Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 20 diff changeset	466	by (metis ValOrd.intros(5))
652861c9473f added a function for calculating values Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 20 diff changeset	467
652861c9473f added a function for calculating values Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 20 diff changeset	468
10 14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	469	lemma mkeps_POSIX:
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	470	assumes "nullable r"
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	471	shows "POSIX (mkeps r) r"
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	472	using assms
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	473	apply(induct r)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	474	apply(auto)[1]
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	475	apply(simp add: POSIX_def)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	476	apply(auto)[1]
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	477	apply(erule Prf.cases)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	478	apply(simp_all)[5]
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	479	apply (metis ValOrd.intros)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	480	apply(simp add: POSIX_def)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	481	apply(auto)[1]
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	482	apply(simp add: POSIX_def)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	483	apply(auto)[1]
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	484	apply(erule Prf.cases)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	485	apply(simp_all)[5]
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	486	apply(auto)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	487	apply (simp add: ValOrd.intros(2) mkeps_flat)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	488	apply(simp add: POSIX_def)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	489	apply(auto)[1]
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	490	apply(erule Prf.cases)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	491	apply(simp_all)[5]
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	492	apply(auto)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	493	apply (simp add: ValOrd.intros(6))
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	494	apply (simp add: ValOrd.intros(3))
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	495	apply(simp add: POSIX_def)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	496	apply(auto)[1]
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	497	apply(erule Prf.cases)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	498	apply(simp_all)[5]
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	499	apply(auto)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	500	apply (simp add: ValOrd.intros(6))
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	501	apply (simp add: ValOrd.intros(3))
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	502	apply(simp add: POSIX_def)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	503	apply(auto)[1]
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	504	apply(erule Prf.cases)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	505	apply(simp_all)[5]
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	506	apply(auto)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	507	apply (metis Prf_flat_L mkeps_flat nullable_correctness)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	508	by (simp add: ValOrd.intros(5))
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	509
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	510
20 c11651bbebf5 some small changes Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 12 diff changeset	511	lemma mkeps_POSIX2:
c11651bbebf5 some small changes Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 12 diff changeset	512	assumes "nullable r"
c11651bbebf5 some small changes Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 12 diff changeset	513	shows "POSIX2 (mkeps r) r"
c11651bbebf5 some small changes Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 12 diff changeset	514	using assms
c11651bbebf5 some small changes Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 12 diff changeset	515	apply(induct r)
c11651bbebf5 some small changes Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 12 diff changeset	516	apply(simp)
c11651bbebf5 some small changes Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 12 diff changeset	517	apply(simp)
c11651bbebf5 some small changes Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 12 diff changeset	518	apply(simp add: POSIX2_def)
c11651bbebf5 some small changes Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 12 diff changeset	519	apply(rule conjI)
c11651bbebf5 some small changes Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 12 diff changeset	520	apply(rule Prf.intros)
c11651bbebf5 some small changes Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 12 diff changeset	521	apply(auto)[1]
c11651bbebf5 some small changes Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 12 diff changeset	522	apply(erule Prf.cases)
c11651bbebf5 some small changes Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 12 diff changeset	523	apply(simp_all)[5]
c11651bbebf5 some small changes Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 12 diff changeset	524	apply(rule ValOrd.intros)
c11651bbebf5 some small changes Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 12 diff changeset	525	apply(simp)
c11651bbebf5 some small changes Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 12 diff changeset	526	apply(simp)
c11651bbebf5 some small changes Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 12 diff changeset	527	apply(simp add: POSIX2_def)
c11651bbebf5 some small changes Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 12 diff changeset	528	apply(rule conjI)
c11651bbebf5 some small changes Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 12 diff changeset	529	apply(rule Prf.intros)
c11651bbebf5 some small changes Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 12 diff changeset	530	apply(simp add: mkeps_nullable)
c11651bbebf5 some small changes Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 12 diff changeset	531	apply(simp add: mkeps_nullable)
c11651bbebf5 some small changes Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 12 diff changeset	532	apply(auto)[1]
c11651bbebf5 some small changes Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 12 diff changeset	533	apply(rotate_tac 6)
c11651bbebf5 some small changes Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 12 diff changeset	534	apply(erule Prf.cases)
c11651bbebf5 some small changes Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 12 diff changeset	535	apply(simp_all)[5]
c11651bbebf5 some small changes Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 12 diff changeset	536	apply(rule ValOrd.intros(2))
c11651bbebf5 some small changes Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 12 diff changeset	537	apply(simp)
c11651bbebf5 some small changes Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 12 diff changeset	538	apply(simp only: nullable.simps)
c11651bbebf5 some small changes Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 12 diff changeset	539	apply(erule disjE)
c11651bbebf5 some small changes Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 12 diff changeset	540	apply(simp)
c11651bbebf5 some small changes Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 12 diff changeset	541	thm POSIX2_ALT1a
c11651bbebf5 some small changes Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 12 diff changeset	542	apply(rule POSIX2_ALT)
c11651bbebf5 some small changes Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 12 diff changeset	543	apply(simp add: POSIX2_def)
c11651bbebf5 some small changes Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 12 diff changeset	544	apply(rule conjI)
c11651bbebf5 some small changes Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 12 diff changeset	545	apply(rule Prf.intros)
c11651bbebf5 some small changes Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 12 diff changeset	546	apply(simp add: mkeps_nullable)
c11651bbebf5 some small changes Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 12 diff changeset	547	oops
c11651bbebf5 some small changes Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 12 diff changeset	548
c11651bbebf5 some small changes Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 12 diff changeset	549
10 14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	550	section {* Derivatives *}
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	551
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	552	fun
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	553	der :: "char \<Rightarrow> rexp \<Rightarrow> rexp"
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	554	where
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	555	"der c (NULL) = NULL"
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	556	\| "der c (EMPTY) = NULL"
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	557	\| "der c (CHAR c') = (if c = c' then EMPTY else NULL)"
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	558	\| "der c (ALT r1 r2) = ALT (der c r1) (der c r2)"
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	559	\| "der c (SEQ r1 r2) =
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	560	(if nullable r1
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	561	then ALT (SEQ (der c r1) r2) (der c r2)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	562	else SEQ (der c r1) r2)"
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	563
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	564	fun
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	565	ders :: "string \<Rightarrow> rexp \<Rightarrow> rexp"
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	566	where
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	567	"ders [] r = r"
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	568	\| "ders (c # s) r = ders s (der c r)"
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	569
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	570	section {* Injection function *}
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	571
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	572	fun injval :: "rexp \<Rightarrow> char \<Rightarrow> val \<Rightarrow> val"
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	573	where
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	574	"injval (CHAR d) c Void = Char d"
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	575	\| "injval (ALT r1 r2) c (Left v1) = Left(injval r1 c v1)"
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	576	\| "injval (ALT r1 r2) c (Right v2) = Right(injval r2 c v2)"
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	577	\| "injval (SEQ r1 r2) c (Seq v1 v2) = Seq (injval r1 c v1) v2"
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	578	\| "injval (SEQ r1 r2) c (Left (Seq v1 v2)) = Seq (injval r1 c v1) v2"
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	579	\| "injval (SEQ r1 r2) c (Right v2) = Seq (mkeps r1) (injval r2 c v2)"
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	580
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	581	section {* Projection function *}
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	582
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	583	fun projval :: "rexp \<Rightarrow> char \<Rightarrow> val \<Rightarrow> val"
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	584	where
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	585	"projval (CHAR d) c _ = Void"
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	586	\| "projval (ALT r1 r2) c (Left v1) = Left(projval r1 c v1)"
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	587	\| "projval (ALT r1 r2) c (Right v2) = Right(projval r2 c v2)"
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	588	\| "projval (SEQ r1 r2) c (Seq v1 v2) =
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	589	(if flat v1 = [] then Right(projval r2 c v2)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	590	else if nullable r1 then Left (Seq (projval r1 c v1) v2)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	591	else Seq (projval r1 c v1) v2)"
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	592
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	593	text {*
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	594	Injection value is related to r
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	595	*}
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	596
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	597	lemma v3:
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	598	assumes "\<turnstile> v : der c r" shows "\<turnstile> (injval r c v) : r"
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	599	using assms
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	600	apply(induct arbitrary: v rule: der.induct)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	601	apply(simp)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	602	apply(erule Prf.cases)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	603	apply(simp_all)[5]
49 c616ec6b1e3c updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 48 diff changeset	604	apply(simp)
10 14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	605	apply(erule Prf.cases)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	606	apply(simp_all)[5]
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	607	apply(case_tac "c = c'")
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	608	apply(simp)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	609	apply(erule Prf.cases)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	610	apply(simp_all)[5]
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	611	apply (metis Prf.intros(5))
49 c616ec6b1e3c updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 48 diff changeset	612	apply(simp)
10 14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	613	apply(erule Prf.cases)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	614	apply(simp_all)[5]
49 c616ec6b1e3c updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 48 diff changeset	615	apply(simp)
10 14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	616	apply(erule Prf.cases)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	617	apply(simp_all)[5]
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	618	apply (metis Prf.intros(2))
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	619	apply (metis Prf.intros(3))
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	620	apply(simp)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	621	apply(case_tac "nullable r1")
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	622	apply(simp)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	623	apply(erule Prf.cases)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	624	apply(simp_all)[5]
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	625	apply(auto)[1]
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	626	apply(erule Prf.cases)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	627	apply(simp_all)[5]
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	628	apply(auto)[1]
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	629	apply (metis Prf.intros(1))
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	630	apply(auto)[1]
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	631	apply (metis Prf.intros(1) mkeps_nullable)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	632	apply(simp)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	633	apply(erule Prf.cases)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	634	apply(simp_all)[5]
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	635	apply(auto)[1]
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	636	apply(rule Prf.intros)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	637	apply(auto)[2]
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	638	done
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	639
53 38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	640	lemma v3_proj:
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	641	assumes "\<turnstile> v : r" and "\<exists>s. (flat v) = c # s"
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	642	shows "\<turnstile> (projval r c v) : der c r"
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	643	using assms
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	644	apply(induct rule: Prf.induct)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	645	prefer 4
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	646	apply(simp)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	647	prefer 4
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	648	apply(simp)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	649	apply (metis Prf.intros(4))
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	650	prefer 2
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	651	apply(simp)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	652	apply (metis Prf.intros(2))
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	653	prefer 2
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	654	apply(simp)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	655	apply (metis Prf.intros(3))
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	656	apply(auto)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	657	apply(rule Prf.intros)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	658	apply(simp)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	659	apply (metis Prf_flat_L nullable_correctness)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	660	apply(rule Prf.intros)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	661	apply(rule Prf.intros)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	662	apply (metis Cons_eq_append_conv)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	663	apply(simp)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	664	apply(rule Prf.intros)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	665	apply (metis Cons_eq_append_conv)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	666	apply(simp)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	667	done
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	668
10 14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	669	text {*
53 38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	670	The string behind the injection value is an added c
10 14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	671	*}
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	672
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	673	lemma v4:
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	674	assumes "\<turnstile> v : der c r" shows "flat (injval r c v) = c # (flat v)"
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	675	using assms
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	676	apply(induct arbitrary: v rule: der.induct)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	677	apply(simp)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	678	apply(erule Prf.cases)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	679	apply(simp_all)[5]
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	680	apply(simp)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	681	apply(erule Prf.cases)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	682	apply(simp_all)[5]
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	683	apply(simp)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	684	apply(case_tac "c = c'")
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	685	apply(simp)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	686	apply(auto)[1]
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	687	apply(erule Prf.cases)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	688	apply(simp_all)[5]
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	689	apply(simp)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	690	apply(erule Prf.cases)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	691	apply(simp_all)[5]
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	692	apply(simp)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	693	apply(erule Prf.cases)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	694	apply(simp_all)[5]
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	695	apply(simp)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	696	apply(case_tac "nullable r1")
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	697	apply(simp)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	698	apply(erule Prf.cases)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	699	apply(simp_all)[5]
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	700	apply(auto)[1]
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	701	apply(erule Prf.cases)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	702	apply(simp_all)[5]
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	703	apply(auto)[1]
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	704	apply (metis mkeps_flat)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	705	apply(simp)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	706	apply(erule Prf.cases)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	707	apply(simp_all)[5]
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	708	done
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	709
53 38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	710	lemma v4_proj:
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	711	assumes "\<turnstile> v : r" and "\<exists>s. (flat v) = c # s"
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	712	shows "c # flat (projval r c v) = flat v"
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	713	using assms
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	714	apply(induct rule: Prf.induct)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	715	prefer 4
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	716	apply(simp)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	717	prefer 4
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	718	apply(simp)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	719	prefer 2
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	720	apply(simp)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	721	prefer 2
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	722	apply(simp)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	723	apply(auto)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	724	by (metis Cons_eq_append_conv)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	725
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	726	lemma v4_proj2:
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	727	assumes "\<turnstile> v : r" and "(flat v) = c # s"
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	728	shows "flat (projval r c v) = s"
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	729	using assms
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	730	by (metis list.inject v4_proj)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	731
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	732	lemma t: "(c#xs = c#ys) \<Longrightarrow> xs = ys"
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	733	by (metis list.sel(3))
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	734
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	735	lemma Prf_proj:
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	736	assumes "v1 \<succ>r v2" "\<turnstile> v1 : r" "\<turnstile> v2 : r" "\<exists>s. (flat v1) = c # s" "\<exists>s. (flat v2) = c # s"
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	737	shows "(projval r c v1) \<succ>(der c r) (projval r c v2)"
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	738	using assms
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	739	apply(induct arbitrary: v1 v2 rule: der.induct)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	740	apply(simp)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	741	apply(erule ValOrd.cases)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	742	apply(simp_all)[8]
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	743	apply(erule ValOrd.cases)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	744	apply(simp_all)[8]
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	745	apply(case_tac "c = c'")
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	746	apply(simp)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	747	apply (metis ValOrd.intros(7))
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	748	apply(erule ValOrd.cases)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	749	apply(simp_all)[8]
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	750	apply(simp)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	751	apply(erule ValOrd.cases)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	752	apply(simp_all)[8]
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	753	apply(erule Prf.cases)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	754	apply(simp_all)[5]
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	755	apply(erule Prf.cases)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	756	apply(simp_all)[5]
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	757	apply(clarify)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	758	apply(rule ValOrd.intros)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	759	apply(subst v4_proj2)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	760	apply(simp)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	761	apply(simp)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	762	apply(subst v4_proj2)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	763	apply(simp)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	764	apply(simp)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	765	apply(simp)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	766	apply(clarify)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	767	apply(erule Prf.cases)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	768	apply(simp_all)[5]
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	769	apply(erule Prf.cases)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	770	apply(simp_all)[5]
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	771	apply(clarify)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	772	apply(rule ValOrd.intros)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	773	apply(subst v4_proj2)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	774	apply(simp)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	775	apply(simp)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	776	apply(subst v4_proj2)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	777	apply(simp)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	778	apply(simp)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	779	apply(simp)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	780	apply(clarify)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	781	apply(erule Prf.cases)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	782	apply(simp_all)[5]
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	783	apply(erule Prf.cases)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	784	apply(simp_all)[5]
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	785	apply(clarify)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	786	apply(rule ValOrd.intros)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	787	apply metis
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	788	apply(clarify)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	789	apply(erule Prf.cases)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	790	apply(simp_all)[5]
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	791	apply(erule Prf.cases)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	792	apply(simp_all)[5]
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	793	apply(clarify)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	794	apply(rule ValOrd.intros)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	795	apply metis
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	796	apply(clarify)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	797	apply(simp)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	798	apply(auto)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	799	defer
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	800	apply(erule ValOrd.cases)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	801	apply(simp_all)[8]
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	802	apply(auto)[1]
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	803	apply(erule Prf.cases)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	804	apply(simp_all)[5]
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	805	apply(erule Prf.cases)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	806	apply(simp_all)[5]
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	807	apply(clarify)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	808	apply(simp)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	809	apply (metis Prf_flat_L nullable_correctness)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	810	apply(erule Prf.cases)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	811	apply(simp_all)[5]
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	812	apply(erule Prf.cases)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	813	apply(simp_all)[5]
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	814	apply(clarify)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	815	apply(rule ValOrd.intros)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	816	apply(simp)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	817	apply(simp)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	818	apply(auto)[1]
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	819	apply(erule Prf.cases)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	820	apply(simp_all)[5]
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	821	apply(erule Prf.cases)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	822	apply(simp_all)[5]
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	823	apply(clarify)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	824	apply (metis Prf_flat_L nullable_correctness)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	825	apply(erule Prf.cases)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	826	apply(simp_all)[5]
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	827	apply(erule Prf.cases)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	828	apply(simp_all)[5]
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	829	apply(clarify)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	830	apply (metis Prf_flat_L nullable_correctness)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	831	apply(erule Prf.cases)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	832	apply(simp_all)[5]
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	833	apply(erule Prf.cases)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	834	apply(simp_all)[5]
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	835	apply(clarify)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	836	apply (metis Prf_flat_L nullable_correctness)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	837	apply(erule Prf.cases)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	838	apply(simp_all)[5]
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	839	apply(erule Prf.cases)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	840	apply(simp_all)[5]
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	841	apply(clarify)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	842	apply(rule ValOrd.intros(2))
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	843	apply (metis append_Cons list.inject neq_Nil_conv)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	844	apply(erule Prf.cases)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	845	apply(simp_all)[5]
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	846	apply(erule Prf.cases)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	847	apply(simp_all)[5]
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	848	apply(clarify)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	849	apply(auto)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	850	apply(erule ValOrd.cases)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	851	apply(simp_all)[8]
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	852	apply(auto)[1]
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	853	apply(rule ValOrd.intros)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	854	apply metis
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	855	apply(clarify)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	856	apply(rule ValOrd.intros)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	857
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	858	apply(rule ValOrd.intros)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	859	apply(simp)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	860	apply(simp)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	861	apply(auto)[1]
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	862	apply(erule Prf.cases)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	863	apply(simp_all)[5]
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	864	apply(erule Prf.cases)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	865	apply(simp_all)[5]
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	866	apply(clarify)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	867	apply(rule ValOrd.intros)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	868	defer
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	869	apply(erule Prf.cases)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	870	apply(simp_all)[5]
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	871	apply(erule Prf.cases)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	872	apply(simp_all)[5]
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	873	apply(clarify)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	874	apply(simp add: append_eq_Cons_conv)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	875	apply(clarify)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	876	apply(rule ValOrd.intros)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	877	apply(simp)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	878	apply(subst v4_proj2)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	879	apply(simp)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	880	apply(simp)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	881	apply(subst v4_proj2)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	882	apply(simp)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	883	apply(simp)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	884
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	885	apply(simp)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	886
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	887	apply (metis Prf_flat_L nullable_correctness)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	888
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	889
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	890
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	891
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	892	apply(rule ValOrd.intros(2))
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	893	apply(erule Prf.cases)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	894	apply(simp_all)[5]
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	895	apply(erule Prf.cases)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	896	apply(simp_all)[5]
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	897	apply(simp)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	898	apply(erule ValOrd.cases)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	899	apply(simp_all)[8]
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	900	apply(clarify)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	901	apply(erule Prf.cases)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	902	apply(simp_all)[5]
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	903	apply(erule Prf.cases)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	904	apply(simp_all)[5]
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	905	apply(clarify)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	906	apply(erule Prf.cases)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	907	apply(simp_all)[5]
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	908	apply(clarify)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	909	apply(simp)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	910
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	911	lemma Prf_inj:
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	912	assumes "v1 \<succ>(der c r) v2" "\<turnstile> v1 : der c r" "\<turnstile> v2 : der c r"
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	913	shows "(injval r c v1) \<succ>r (injval r c v2)"
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	914	using assms
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	915	apply(induct arbitrary: v1 v2 rule: der.induct)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	916	apply(simp)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	917	apply(erule ValOrd.cases)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	918	apply(simp_all)[8]
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	919	apply(erule ValOrd.cases)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	920	apply(simp_all)[8]
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	921	apply(case_tac "c = c'")
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	922	apply(simp)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	923	apply(erule ValOrd.cases)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	924	apply(simp_all)[8]
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	925	apply(rule ValOrd.intros)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	926	apply(simp)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	927	apply(erule ValOrd.cases)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	928	apply(simp_all)[8]
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	929	apply(simp)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	930	apply(erule ValOrd.cases)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	931	apply(simp_all)[8]
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	932	apply(rule ValOrd.intros)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	933	apply(subst v4)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	934	apply(clarify)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	935	apply(rotate_tac 3)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	936	apply(erule Prf.cases)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	937	apply(simp_all)[5]
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	938	apply(subst v4)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	939	apply(clarify)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	940	apply(rotate_tac 2)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	941	apply(erule Prf.cases)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	942	apply(simp_all)[5]
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	943	apply(simp)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	944	apply(rule ValOrd.intros)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	945	apply(subst v4)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	946	apply(clarify)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	947	apply(rotate_tac 3)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	948	apply(erule Prf.cases)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	949	apply(simp_all)[5]
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	950	apply(subst v4)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	951	apply(clarify)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	952	apply(erule Prf.cases)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	953	apply(simp_all)[5]
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	954	apply(simp)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	955	apply(rule ValOrd.intros)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	956	apply(clarify)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	957	apply(erule Prf.cases)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	958	apply(simp_all)[5]
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	959	apply(erule Prf.cases)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	960	apply(simp_all)[5]
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	961	apply(rule ValOrd.intros)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	962	apply(clarify)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	963	apply(erule Prf.cases)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	964	apply(simp_all)[5]
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	965	apply(erule Prf.cases)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	966	apply(simp_all)[5]
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	967	apply(simp)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	968	apply(case_tac "nullable r1")
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	969	defer
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	970	apply(simp)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	971	apply(erule ValOrd.cases)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	972	apply(simp_all)[8]
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	973	apply(clarify)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	974	apply(erule Prf.cases)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	975	apply(simp_all)[5]
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	976	apply(erule Prf.cases)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	977	apply(simp_all)[5]
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	978	apply(clarify)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	979	apply(rule ValOrd.intros)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	980	apply(simp)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	981	apply(simp)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	982	apply(rule ValOrd.intros(2))
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	983	apply(erule Prf.cases)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	984	apply(simp_all)[5]
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	985	apply(erule Prf.cases)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	986	apply(simp_all)[5]
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	987	apply(simp)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	988	apply(erule ValOrd.cases)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	989	apply(simp_all)[8]
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	990	apply(clarify)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	991	apply(erule Prf.cases)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	992	apply(simp_all)[5]
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	993	apply(erule Prf.cases)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	994	apply(simp_all)[5]
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	995	apply(clarify)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	996	apply(erule Prf.cases)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	997	apply(simp_all)[5]
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	998	apply(clarify)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	999	apply(simp)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	1000	apply(case_tac "injval r1 c v1 = mkeps r1")
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	1001	apply(rule ValOrd.intros(1))
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	1002	apply(simp)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	1003	apply (metis impossible_Cons le_add2 list.size(3) mkeps_flat monoid_add_class.add.right_neutral v4)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	1004	apply(rule ValOrd.intros(2))
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	1005
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	1006	apply(rotate_tac 1)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	1007	apply(drule meta_mp)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	1008	apply(rule
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	1009
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	1010	lemma POSIX_der:
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	1011	assumes "POSIX v (der c r)" "\<turnstile> v : der c r"
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	1012	shows "POSIX (injval r c v) r"
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	1013	using assms
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	1014	unfolding POSIX_def
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	1015	apply(auto)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	1016	apply(subst (asm) v4)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	1017	apply(assumption)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	1018	apply(drule_tac x="projval r c v'" in spec)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	1019	apply(drule mp)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	1020	apply(auto)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	1021	apply(rule v3_proj)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	1022	apply(simp)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	1023	apply(rule_tac x="flat v" in exI)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	1024	apply(simp)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	1025	apply(rule_tac c="c" in t)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	1026	apply(simp)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	1027	apply(subst v4_proj)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	1028	apply(simp)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	1029	apply(rule_tac x="flat v" in exI)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	1030	apply(simp)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	1031	apply(simp)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	1032	apply(simp add: Cons_eq_append_conv)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	1033	apply(auto)[1]
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	1034
10 14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1035	text {*
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1036	Injection followed by projection is the identity.
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1037	*}
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1038
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1039	lemma proj_inj_id:
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1040	assumes "\<turnstile> v : der c r"
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1041	shows "projval r c (injval r c v) = v"
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1042	using assms
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1043	apply(induct r arbitrary: c v rule: rexp.induct)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1044	apply(simp)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1045	apply(erule Prf.cases)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1046	apply(simp_all)[5]
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1047	apply(simp)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1048	apply(erule Prf.cases)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1049	apply(simp_all)[5]
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1050	apply(simp)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1051	apply(case_tac "c = char")
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1052	apply(simp)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1053	apply(erule Prf.cases)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1054	apply(simp_all)[5]
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1055	apply(simp)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1056	apply(erule Prf.cases)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1057	apply(simp_all)[5]
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1058	defer
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1059	apply(simp)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1060	apply(erule Prf.cases)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1061	apply(simp_all)[5]
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1062	apply(simp)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1063	apply(case_tac "nullable rexp1")
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1064	apply(simp)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1065	apply(erule Prf.cases)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1066	apply(simp_all)[5]
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1067	apply(auto)[1]
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1068	apply(erule Prf.cases)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1069	apply(simp_all)[5]
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1070	apply(auto)[1]
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1071	apply (metis list.distinct(1) v4)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1072	apply(auto)[1]
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1073	apply (metis mkeps_flat)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1074	apply(auto)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1075	apply(erule Prf.cases)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1076	apply(simp_all)[5]
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1077	apply(auto)[1]
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1078	apply(simp add: v4)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1079	done
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1080
48 652861c9473f added a function for calculating values Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 20 diff changeset	1081	lemma "L r \<noteq> {} \<Longrightarrow> \<exists>v. POSIX3 v r"
652861c9473f added a function for calculating values Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 20 diff changeset	1082	apply(induct r)
652861c9473f added a function for calculating values Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 20 diff changeset	1083	apply(simp)
652861c9473f added a function for calculating values Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 20 diff changeset	1084	apply(simp add: POSIX3_def)
652861c9473f added a function for calculating values Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 20 diff changeset	1085	apply(rule_tac x="Void" in exI)
652861c9473f added a function for calculating values Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 20 diff changeset	1086	apply(auto)[1]
652861c9473f added a function for calculating values Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 20 diff changeset	1087	apply (metis Prf.intros(4))
652861c9473f added a function for calculating values Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 20 diff changeset	1088	apply (metis POSIX3_def flat.simps(1) mkeps.simps(1) mkeps_POSIX3 nullable.simps(2) order_refl)
652861c9473f added a function for calculating values Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 20 diff changeset	1089	apply(simp add: POSIX3_def)
652861c9473f added a function for calculating values Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 20 diff changeset	1090	apply(rule_tac x="Char char" in exI)
652861c9473f added a function for calculating values Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 20 diff changeset	1091	apply(auto)[1]
652861c9473f added a function for calculating values Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 20 diff changeset	1092	apply (metis Prf.intros(5))
652861c9473f added a function for calculating values Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 20 diff changeset	1093	apply(erule Prf.cases)
652861c9473f added a function for calculating values Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 20 diff changeset	1094	apply(simp_all)[5]
652861c9473f added a function for calculating values Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 20 diff changeset	1095	apply (metis ValOrd.intros(8))
652861c9473f added a function for calculating values Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 20 diff changeset	1096	apply(simp add: Sequ_def)
652861c9473f added a function for calculating values Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 20 diff changeset	1097	apply(auto)[1]
652861c9473f added a function for calculating values Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 20 diff changeset	1098	apply(drule meta_mp)
652861c9473f added a function for calculating values Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 20 diff changeset	1099	apply(auto)[2]
652861c9473f added a function for calculating values Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 20 diff changeset	1100	apply(drule meta_mp)
652861c9473f added a function for calculating values Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 20 diff changeset	1101	apply(auto)[2]
652861c9473f added a function for calculating values Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 20 diff changeset	1102	apply(rule_tac x="Seq v va" in exI)
652861c9473f added a function for calculating values Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 20 diff changeset	1103	apply(simp (no_asm) add: POSIX3_def)
652861c9473f added a function for calculating values Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 20 diff changeset	1104	apply(auto)[1]
652861c9473f added a function for calculating values Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 20 diff changeset	1105	apply (metis POSIX3_def Prf.intros(1))
652861c9473f added a function for calculating values Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 20 diff changeset	1106	apply(erule Prf.cases)
652861c9473f added a function for calculating values Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 20 diff changeset	1107	apply(simp_all)[5]
652861c9473f added a function for calculating values Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 20 diff changeset	1108	apply(clarify)
652861c9473f added a function for calculating values Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 20 diff changeset	1109	apply(case_tac "v \<succ>r1a v1")
652861c9473f added a function for calculating values Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 20 diff changeset	1110	apply(rule ValOrd.intros(2))
652861c9473f added a function for calculating values Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 20 diff changeset	1111	apply(simp)
652861c9473f added a function for calculating values Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 20 diff changeset	1112	apply(case_tac "v = v1")
652861c9473f added a function for calculating values Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 20 diff changeset	1113	apply(rule ValOrd.intros(1))
652861c9473f added a function for calculating values Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 20 diff changeset	1114	apply(simp)
652861c9473f added a function for calculating values Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 20 diff changeset	1115	apply(simp)
652861c9473f added a function for calculating values Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 20 diff changeset	1116	apply (metis ValOrd_refl)
652861c9473f added a function for calculating values Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 20 diff changeset	1117	apply(simp add: POSIX3_def)
53 38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	1118	oops
48 652861c9473f added a function for calculating values Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 20 diff changeset	1119
10 14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1120	lemma "\<exists>v. POSIX v r"
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1121	apply(induct r)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1122	apply(rule exI)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1123	apply(simp add: POSIX_def)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1124	apply (metis (full_types) Prf_flat_L der.simps(1) der.simps(2) der.simps(3) flat.simps(1) nullable.simps(1) nullable_correctness proj_inj_id projval.simps(1) v3 v4)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1125	apply(rule_tac x = "Void" in exI)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1126	apply(simp add: POSIX_def)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1127	apply (metis POSIX_def flat.simps(1) mkeps.simps(1) mkeps_POSIX nullable.simps(2))
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1128	apply(rule_tac x = "Char char" in exI)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1129	apply(simp add: POSIX_def)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1130	apply(auto) [1]
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1131	apply(erule Prf.cases)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1132	apply(simp_all) [5]
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1133	apply (metis ValOrd.intros(8))
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1134	defer
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1135	apply(auto)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1136	apply (metis POSIX_ALT_I1)
11 26b8a5213355 changed theory name Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 10 diff changeset	1137	(* maybe it is too early to instantiate this existential quantifier *)
26b8a5213355 changed theory name Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 10 diff changeset	1138	(* potentially this is the wrong POSIX value *)
20 c11651bbebf5 some small changes Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 12 diff changeset	1139	apply(case_tac "r1 = NULL")
c11651bbebf5 some small changes Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 12 diff changeset	1140	apply(simp add: POSIX_def)
c11651bbebf5 some small changes Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 12 diff changeset	1141	apply(auto)[1]
c11651bbebf5 some small changes Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 12 diff changeset	1142	apply (metis L.simps(1) L.simps(4) Prf_flat_L mkeps_flat nullable.simps(1) nullable.simps(2) nullable_correctness seq_null(2))
c11651bbebf5 some small changes Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 12 diff changeset	1143	apply(case_tac "r1 = EMPTY")
c11651bbebf5 some small changes Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 12 diff changeset	1144	apply(rule_tac x = "Seq Void va" in exI )
10 14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1145	apply(simp (no_asm) add: POSIX_def)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1146	apply(auto)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1147	apply(erule Prf.cases)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1148	apply(simp_all)
20 c11651bbebf5 some small changes Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 12 diff changeset	1149	apply(auto)[1]
c11651bbebf5 some small changes Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 12 diff changeset	1150	apply(erule Prf.cases)
c11651bbebf5 some small changes Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 12 diff changeset	1151	apply(simp_all)
c11651bbebf5 some small changes Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 12 diff changeset	1152	apply(rule ValOrd.intros(2))
c11651bbebf5 some small changes Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 12 diff changeset	1153	apply(rule ValOrd.intros)
c11651bbebf5 some small changes Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 12 diff changeset	1154	apply(case_tac "\<exists>c. r1 = CHAR c")
c11651bbebf5 some small changes Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 12 diff changeset	1155	apply(auto)
c11651bbebf5 some small changes Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 12 diff changeset	1156	apply(rule_tac x = "Seq (Char c) va" in exI )
c11651bbebf5 some small changes Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 12 diff changeset	1157	apply(simp (no_asm) add: POSIX_def)
c11651bbebf5 some small changes Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 12 diff changeset	1158	apply(auto)
c11651bbebf5 some small changes Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 12 diff changeset	1159	apply(erule Prf.cases)
c11651bbebf5 some small changes Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 12 diff changeset	1160	apply(simp_all)
c11651bbebf5 some small changes Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 12 diff changeset	1161	apply(auto)[1]
c11651bbebf5 some small changes Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 12 diff changeset	1162	apply(erule Prf.cases)
c11651bbebf5 some small changes Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 12 diff changeset	1163	apply(simp_all)
c11651bbebf5 some small changes Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 12 diff changeset	1164	apply(auto)[1]
c11651bbebf5 some small changes Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 12 diff changeset	1165	apply(rule ValOrd.intros(2))
c11651bbebf5 some small changes Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 12 diff changeset	1166	apply(rule ValOrd.intros)
c11651bbebf5 some small changes Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 12 diff changeset	1167	apply(case_tac "\<exists>r1a r1b. r1 = ALT r1a r1b")
c11651bbebf5 some small changes Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 12 diff changeset	1168	apply(auto)
48 652861c9473f added a function for calculating values Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 20 diff changeset	1169	oops (* not sure if this can be proved by induction *)
10 14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1170
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1171	text {*
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1172
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1173	HERE: Crucial lemma that does not go through in the sequence case.
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1174
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1175	*}
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1176	lemma v5:
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1177	assumes "\<turnstile> v : der c r" "POSIX v (der c r)"
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1178	shows "POSIX (injval r c v) r"
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1179	using assms
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1180	apply(induct arbitrary: v rule: der.induct)
53 38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	1181	(* NULL case *)
10 14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1182	apply(simp)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1183	apply(erule Prf.cases)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1184	apply(simp_all)[5]
53 38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	1185	(* EMPTY case *)
10 14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1186	apply(simp)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1187	apply(erule Prf.cases)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1188	apply(simp_all)[5]
53 38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	1189	(* CHAR case *)
10 14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1190	apply(simp)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1191	apply(case_tac "c = c'")
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1192	apply(auto simp add: POSIX_def)[1]
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1193	apply(erule Prf.cases)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1194	apply(simp_all)[5]
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1195	apply(erule Prf.cases)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1196	apply(simp_all)[5]
53 38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	1197	apply(rule ValOrd.intros)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	1198	apply(auto)[1]
10 14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1199	apply(erule Prf.cases)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1200	apply(simp_all)[5]
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1201	(* base cases done *)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1202	(* ALT case *)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1203	apply(erule Prf.cases)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1204	apply(simp_all)[5]
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1205	using POSIX_ALT POSIX_ALT_I1 apply blast
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1206	apply(clarify)
53 38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	1207	apply(simp)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	1208	apply(rule POSIX_ALT_I2)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	1209	apply(drule POSIX_ALT1a)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	1210	apply metis
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	1211	apply(auto)[1]
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	1212	apply(subst v4)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	1213	apply(assumption)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	1214	apply(simp)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	1215	apply(drule POSIX_ALT1a)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	1216	apply(rotate_tac 1)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	1217	apply(drule_tac x="v2" in meta_spec)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	1218	apply(simp)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	1219
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	1220	apply(rotate_tac 4)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	1221	apply(erule Prf.cases)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	1222	apply(simp_all)[5]
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	1223	apply(rule ValOrd.intros)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	1224	apply(simp)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	1225	apply(subst (asm) v4)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	1226	apply(assumption)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	1227	apply(clarify)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	1228	thm POSIX_ALT1a POSIX_ALT1b POSIX_ALT_I2
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	1229	apply(subst (asm) v4)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	1230	apply(auto simp add: POSIX_def)[1]
10 14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1231	apply(subgoal_tac "POSIX v2 (der c r2)")
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1232	prefer 2
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1233	apply(auto simp add: POSIX_def)[1]
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1234	apply (metis POSIX_ALT1a POSIX_def flat.simps(4))
48 652861c9473f added a function for calculating values Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 20 diff changeset	1235	apply(frule POSIX_ALT1a)
652861c9473f added a function for calculating values Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 20 diff changeset	1236	apply(drule POSIX_ALT1b)
652861c9473f added a function for calculating values Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 20 diff changeset	1237	apply(rule POSIX_ALT_I2)
10 14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1238	apply(rotate_tac 1)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1239	apply(drule_tac x="v2" in meta_spec)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1240	apply(simp)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1241	apply(subgoal_tac "\<turnstile> Right (injval r2 c v2) : (ALT r1 r2)")
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1242	prefer 2
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1243	apply (metis Prf.intros(3) v3)
48 652861c9473f added a function for calculating values Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 20 diff changeset	1244	apply auto[1]
652861c9473f added a function for calculating values Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 20 diff changeset	1245	apply(subst v4)
652861c9473f added a function for calculating values Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 20 diff changeset	1246	apply(auto)[2]
652861c9473f added a function for calculating values Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 20 diff changeset	1247	apply(subst (asm) (4) POSIX_def)
652861c9473f added a function for calculating values Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 20 diff changeset	1248	apply(subst (asm) v4)
652861c9473f added a function for calculating values Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 20 diff changeset	1249	apply(drule_tac x="v2" in meta_spec)
652861c9473f added a function for calculating values Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 20 diff changeset	1250	apply(simp)
652861c9473f added a function for calculating values Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 20 diff changeset	1251
652861c9473f added a function for calculating values Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 20 diff changeset	1252	apply(auto)[2]
652861c9473f added a function for calculating values Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 20 diff changeset	1253
652861c9473f added a function for calculating values Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 20 diff changeset	1254	thm POSIX_ALT_I2
652861c9473f added a function for calculating values Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 20 diff changeset	1255	apply(rule POSIX_ALT_I2)
652861c9473f added a function for calculating values Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 20 diff changeset	1256
10 14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1257	apply(rule ccontr)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1258	apply(auto simp add: POSIX_def)[1]
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1259
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1260	apply(rule allI)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1261	apply(rule impI)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1262	apply(erule conjE)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1263	thm POSIX_ALT_I2
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1264	apply(frule POSIX_ALT1a)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1265	apply(drule POSIX_ALT1b)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1266	apply(rule POSIX_ALT_I2)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1267	apply auto[1]
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1268	apply(subst v4)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1269	apply(auto)[2]
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1270	apply(rotate_tac 1)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1271	apply(drule_tac x="v2" in meta_spec)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1272	apply(simp)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1273	apply(subst (asm) (4) POSIX_def)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1274	apply(subst (asm) v4)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1275	apply(auto)[2]
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1276	(* stuck in the ALT case *)

author	fahad
	Thu, 29 Jan 2015 11:23:05 +0000
changeset 54	45274393f28c
parent 53	38cde0214ad5
child 68	f182c125980e
permissions	-rw-r--r--