lexing: thys/Re1.thy@a6bb0152ccc2 (annotated)

56 5bc72d6d633d updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 55 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
62 a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	45	fun
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	46	nullable :: "rexp \<Rightarrow> bool"
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	47	where
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	48	"nullable (NULL) = False"
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	49	\| "nullable (EMPTY) = True"
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	50	\| "nullable (CHAR c) = False"
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	51	\| "nullable (ALT r1 r2) = (nullable r1 \<or> nullable r2)"
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	52	\| "nullable (SEQ r1 r2) = (nullable r1 \<and> nullable r2)"
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	53
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	54	lemma nullable_correctness:
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	55	shows "nullable r \<longleftrightarrow> [] \<in> (L r)"
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	56	apply (induct r)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	57	apply(auto simp add: Sequ_def)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	58	done
10 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	section {* Values *}
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	61
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	62	datatype val =
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	63	Void
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	64	\| Char char
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	65	\| Seq val val
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	66	\| Right val
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	67	\| Left val
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	68
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	69	section {* The string behind a value *}
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	70
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	71	fun flat :: "val \<Rightarrow> string"
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	72	where
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	73	"flat(Void) = []"
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	74	\| "flat(Char c) = [c]"
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	75	\| "flat(Left v) = flat(v)"
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	76	\| "flat(Right v) = flat(v)"
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	77	\| "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	78
48 652861c9473f added a function for calculating values Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 20 diff changeset	79	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	80	where
652861c9473f added a function for calculating values Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 20 diff changeset	81	"flats(Void) = [[]]"
652861c9473f added a function for calculating values Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 20 diff changeset	82	\| "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	83	\| "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	84	\| "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	85	\| "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	86
62 a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	87
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	88	section {* Relation between values and regular expressions *}
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	89
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	90	inductive Prf :: "val \<Rightarrow> rexp \<Rightarrow> bool" ("\<turnstile> _ : _" [100, 100] 100)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	91	where
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	92	"\<lbrakk>\<turnstile> v1 : r1; \<turnstile> v2 : r2\<rbrakk> \<Longrightarrow> \<turnstile> Seq v1 v2 : SEQ r1 r2"
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	93	\| "\<turnstile> v1 : r1 \<Longrightarrow> \<turnstile> Left v1 : ALT r1 r2"
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	94	\| "\<turnstile> v2 : r2 \<Longrightarrow> \<turnstile> Right v2 : ALT r1 r2"
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	95	\| "\<turnstile> Void : EMPTY"
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	96	\| "\<turnstile> Char c : CHAR c"
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	97
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	98	fun mkeps :: "rexp \<Rightarrow> val"
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	99	where
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	100	"mkeps(EMPTY) = Void"
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	101	\| "mkeps(SEQ r1 r2) = Seq (mkeps r1) (mkeps r2)"
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	102	\| "mkeps(ALT r1 r2) = (if nullable(r1) then Left (mkeps r1) else Right (mkeps r2))"
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	103
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	104	lemma mkeps_nullable:
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	105	assumes "nullable(r)" shows "\<turnstile> mkeps r : r"
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	106	using assms
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	107	apply(induct rule: nullable.induct)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	108	apply(auto intro: Prf.intros)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	109	done
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	110
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	111
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	112
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	113	lemma mkeps_flat:
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	114	assumes "nullable(r)" shows "flat (mkeps r) = []"
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	115	using assms
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	116	apply(induct rule: nullable.induct)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	117	apply(auto)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	118	done
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	119
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	120	text {*
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	121	The value mkeps returns is always the correct POSIX
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	122	value.
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	123	*}
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	124
10 14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	125	lemma Prf_flat_L:
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	126	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	127	using assms
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	128	apply(induct)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	129	apply(auto simp add: Sequ_def)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	130	done
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	131
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	132	lemma L_flat_Prf:
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	133	"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	134	apply(induct r)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	135	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	136	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	137	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	138	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	139	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	140	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	141	apply(erule Prf.cases)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	142	apply(auto)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	143	done
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	144
48 652861c9473f added a function for calculating values Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 20 diff changeset	145	definition prefix :: "string \<Rightarrow> string \<Rightarrow> bool" ("_ \<sqsubset> _" [100, 100] 100)
652861c9473f added a function for calculating values Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 20 diff changeset	146	where
652861c9473f added a function for calculating values Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 20 diff changeset	147	"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	148
10 14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	149	section {* Ordering of values *}
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	150
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	151	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	152	where
62 a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	153	"v2 \<succ>r2 v2' \<Longrightarrow> (Seq v1 v2) \<succ>(SEQ r1 r2) (Seq v1 v2')"
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	154	\| "\<lbrakk>v1 \<succ>r1 v1'; v1 \<noteq> v1'\<rbrakk> \<Longrightarrow> (Seq v1 v2) \<succ>(SEQ r1 r2) (Seq v1' v2')"
10 14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	155	\| "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	156	\| "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	157	\| "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	158	\| "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	159	\| "Void \<succ>EMPTY Void"
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	160	\| "(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	161
53 38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	162
48 652861c9473f added a function for calculating values Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 20 diff changeset	163	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	164
652861c9473f added a function for calculating values Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 20 diff changeset	165	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	166	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	167	shows "v \<succ>r v"
10 14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	168	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	169	apply(induct)
652861c9473f added a function for calculating values Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 20 diff changeset	170	apply(auto intro: ValOrd.intros)
10 14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	171	done
48 652861c9473f added a function for calculating values Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 20 diff changeset	172
10 14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	173	section {* Posix definition *}
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	174
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	175	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	176	where
62 a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	177	"POSIX v r \<equiv> (\<turnstile> v : r \<and> (\<forall>v'. (\<turnstile> v' : r \<and> flat v = flat v') \<longrightarrow> v \<succ>r v'))"
10 14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	178
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	179	(*
11 26b8a5213355 changed theory name Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 10 diff changeset	180	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	181	with theorem mkeps_POSIX
26b8a5213355 changed theory name Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 10 diff changeset	182	*)
26b8a5213355 changed theory name Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 10 diff changeset	183
62 a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	184	(*
11 26b8a5213355 changed theory name Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 10 diff changeset	185	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	186	where
26b8a5213355 changed theory name Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 10 diff changeset	187	"POSIX2 v r \<equiv> \<turnstile> v : r \<and> (\<forall>v'. \<turnstile> v' : r \<longrightarrow> v \<succ>r v')"
62 a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	188	*)
11 26b8a5213355 changed theory name Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 10 diff changeset	189
62 a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	190	(*
20 c11651bbebf5 some small changes Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 12 diff changeset	191	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	192	where
c11651bbebf5 some small changes Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 12 diff changeset	193	"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')"
62 a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	194	*)
11 26b8a5213355 changed theory name Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 10 diff changeset	195
62 a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	196	lemma POSIX_SEQ1:
10 14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	197	assumes "POSIX (Seq v1 v2) (SEQ r1 r2)" "\<turnstile> v1 : r1" "\<turnstile> v2 : r2"
62 a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	198	shows "POSIX v1 r1"
10 14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	199	using assms
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	200	unfolding POSIX_def
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	201	apply(auto)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	202	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	203	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	204	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	205	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	206	apply(simp)
652861c9473f added a function for calculating values Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 20 diff changeset	207	apply(simp)
652861c9473f added a function for calculating values Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 20 diff changeset	208	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	209	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	210	apply(clarify)
62 a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	211	by (metis ValOrd_refl)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	212
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	213	lemma POSIX_SEQ2:
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	214	assumes "POSIX (Seq v1 v2) (SEQ r1 r2)" "\<turnstile> v1 : r1" "\<turnstile> v2 : r2"
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	215	shows "POSIX v2 r2"
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	216	using assms
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	217	unfolding POSIX_def
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	218	apply(auto)
10 14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	219	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	220	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	221	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	222	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	223	apply(simp)
652861c9473f added a function for calculating values Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 20 diff changeset	224	apply(simp)
652861c9473f added a function for calculating values Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 20 diff changeset	225	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	226	apply(simp_all)
62 a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	227	done
12 232ea10bed6f Delete POSIX_ALT2 fahadausaf <fahad.ausaf@icloud.com> parents: 11 diff changeset	228
232ea10bed6f Delete POSIX_ALT2 fahadausaf <fahad.ausaf@icloud.com> parents: 11 diff changeset	229	lemma POSIX_ALT2:
232ea10bed6f Delete POSIX_ALT2 fahadausaf <fahad.ausaf@icloud.com> parents: 11 diff changeset	230	assumes "POSIX (Left v1) (ALT r1 r2)"
232ea10bed6f Delete POSIX_ALT2 fahadausaf <fahad.ausaf@icloud.com> parents: 11 diff changeset	231	shows "POSIX v1 r1"
232ea10bed6f Delete POSIX_ALT2 fahadausaf <fahad.ausaf@icloud.com> parents: 11 diff changeset	232	using assms
232ea10bed6f Delete POSIX_ALT2 fahadausaf <fahad.ausaf@icloud.com> parents: 11 diff changeset	233	unfolding POSIX_def
232ea10bed6f Delete POSIX_ALT2 fahadausaf <fahad.ausaf@icloud.com> parents: 11 diff changeset	234	apply(auto)
62 a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	235	apply(erule Prf.cases)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	236	apply(simp_all)[5]
12 232ea10bed6f Delete POSIX_ALT2 fahadausaf <fahad.ausaf@icloud.com> parents: 11 diff changeset	237	apply(drule_tac x="Left v'" in spec)
232ea10bed6f Delete POSIX_ALT2 fahadausaf <fahad.ausaf@icloud.com> parents: 11 diff changeset	238	apply(simp)
232ea10bed6f Delete POSIX_ALT2 fahadausaf <fahad.ausaf@icloud.com> parents: 11 diff changeset	239	apply(drule mp)
232ea10bed6f Delete POSIX_ALT2 fahadausaf <fahad.ausaf@icloud.com> parents: 11 diff changeset	240	apply(rule Prf.intros)
232ea10bed6f Delete POSIX_ALT2 fahadausaf <fahad.ausaf@icloud.com> parents: 11 diff changeset	241	apply(auto)
232ea10bed6f Delete POSIX_ALT2 fahadausaf <fahad.ausaf@icloud.com> parents: 11 diff changeset	242	apply(erule ValOrd.cases)
232ea10bed6f Delete POSIX_ALT2 fahadausaf <fahad.ausaf@icloud.com> parents: 11 diff changeset	243	apply(simp_all)
232ea10bed6f Delete POSIX_ALT2 fahadausaf <fahad.ausaf@icloud.com> parents: 11 diff changeset	244	done
232ea10bed6f Delete POSIX_ALT2 fahadausaf <fahad.ausaf@icloud.com> parents: 11 diff changeset	245
10 14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	246	lemma POSIX_ALT1a:
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	247	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	248	shows "POSIX v2 r2"
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	249	using assms
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	250	unfolding POSIX_def
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	251	apply(auto)
62 a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	252	apply(erule Prf.cases)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	253	apply(simp_all)[5]
10 14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	254	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	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
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	263	lemma POSIX_ALT1b:
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	264	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	265	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	266	using assms
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	267	apply(drule_tac POSIX_ALT1a)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	268	unfolding POSIX_def
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	269	apply(auto)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	270	done
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	271
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	272	lemma POSIX_ALT_I1:
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	273	assumes "POSIX v1 r1"
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	274	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	275	using assms
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	276	unfolding POSIX_def
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	277	apply(auto)
62 a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	278	apply (metis Prf.intros(2))
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	279	apply(rotate_tac 2)
10 14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	280	apply(erule Prf.cases)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	281	apply(simp_all)[5]
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	282	apply(auto)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	283	apply(rule ValOrd.intros)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	284	apply(auto)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	285	apply(rule ValOrd.intros)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	286	by simp
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	287
20 c11651bbebf5 some small changes Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 12 diff changeset	288
10 14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	289	lemma POSIX_ALT_I2:
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	290	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	291	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	292	using assms
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	293	unfolding POSIX_def
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	294	apply(auto)
62 a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	295	apply (metis Prf.intros)
10 14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	296	apply(rotate_tac 3)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	297	apply(erule Prf.cases)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	298	apply(simp_all)[5]
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	299	apply(auto)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	300	apply(rule ValOrd.intros)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	301	apply metis
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	302	done
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	303
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	304	lemma mkeps_POSIX:
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	305	assumes "nullable r"
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	306	shows "POSIX (mkeps r) r"
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	307	using assms
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	308	apply(induct r)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	309	apply(auto)[1]
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	310	apply(simp add: POSIX_def)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	311	apply(auto)[1]
62 a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	312	apply (metis Prf.intros(4))
10 14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	313	apply(erule Prf.cases)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	314	apply(simp_all)[5]
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	315	apply (metis ValOrd.intros)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	316	apply(simp add: POSIX_def)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	317	apply(auto)[1]
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	318	apply(simp add: POSIX_def)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	319	apply(auto)[1]
62 a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	320	apply (metis mkeps.simps(2) mkeps_nullable nullable.simps(5))
20 c11651bbebf5 some small changes Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 12 diff changeset	321	apply(rotate_tac 6)
c11651bbebf5 some small changes Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 12 diff changeset	322	apply(erule Prf.cases)
c11651bbebf5 some small changes Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 12 diff changeset	323	apply(simp_all)[5]
62 a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	324	apply (simp add: mkeps_flat)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	325	apply(case_tac "mkeps r1a = v1")
20 c11651bbebf5 some small changes Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 12 diff changeset	326	apply(simp)
62 a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	327	apply (metis ValOrd.intros(1))
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	328	apply (rule ValOrd.intros(2))
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	329	apply metis
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	330	apply(simp)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	331	apply(simp)
20 c11651bbebf5 some small changes Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 12 diff changeset	332	apply(erule disjE)
c11651bbebf5 some small changes Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 12 diff changeset	333	apply(simp)
62 a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	334	apply (metis POSIX_ALT_I1)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	335	apply(auto)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	336	apply (metis POSIX_ALT_I1)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	337	apply(simp add: POSIX_def)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	338	apply(auto)[1]
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	339	apply (metis Prf.intros(3))
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	340	apply(rotate_tac 5)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	341	apply(erule Prf.cases)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	342	apply(simp_all)[5]
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	343	apply(simp add: mkeps_flat)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	344	apply(auto)[1]
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	345	apply (metis Prf_flat_L nullable_correctness)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	346	apply(rule ValOrd.intros)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	347	by metis
20 c11651bbebf5 some small changes Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 12 diff changeset	348
c11651bbebf5 some small changes Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 12 diff changeset	349
10 14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	350	section {* Derivatives *}
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	351
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	352	fun
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	353	der :: "char \<Rightarrow> rexp \<Rightarrow> rexp"
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	354	where
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	355	"der c (NULL) = NULL"
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	356	\| "der c (EMPTY) = NULL"
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	357	\| "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	358	\| "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	359	\| "der c (SEQ r1 r2) =
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	360	(if nullable r1
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	361	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	362	else SEQ (der c r1) r2)"
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	363
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	364	fun
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	365	ders :: "string \<Rightarrow> rexp \<Rightarrow> rexp"
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	366	where
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	367	"ders [] r = r"
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	368	\| "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	369
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	370	section {* Injection function *}
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	371
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	372	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	373	where
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	374	"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	375	\| "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	376	\| "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	377	\| "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	378	\| "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	379	\| "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	380
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	381	section {* Projection function *}
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	382
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	383	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	384	where
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	385	"projval (CHAR d) c _ = Void"
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	386	\| "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	387	\| "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	388	\| "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	389	(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	390	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	391	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	392
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	393	text {*
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	394	Injection value is related to r
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	395	*}
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	396
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	397	lemma v3:
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	398	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	399	using assms
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	400	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	401	apply(simp)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	402	apply(erule Prf.cases)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	403	apply(simp_all)[5]
49 c616ec6b1e3c updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 48 diff changeset	404	apply(simp)
10 14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	405	apply(erule Prf.cases)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	406	apply(simp_all)[5]
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	407	apply(case_tac "c = c'")
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	408	apply(simp)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	409	apply(erule Prf.cases)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	410	apply(simp_all)[5]
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	411	apply (metis Prf.intros(5))
49 c616ec6b1e3c updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 48 diff changeset	412	apply(simp)
10 14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	413	apply(erule Prf.cases)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	414	apply(simp_all)[5]
49 c616ec6b1e3c updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 48 diff changeset	415	apply(simp)
10 14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	416	apply(erule Prf.cases)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	417	apply(simp_all)[5]
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	418	apply (metis Prf.intros(2))
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	419	apply (metis Prf.intros(3))
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	420	apply(simp)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	421	apply(case_tac "nullable r1")
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	422	apply(simp)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	423	apply(erule Prf.cases)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	424	apply(simp_all)[5]
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	425	apply(auto)[1]
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	426	apply(erule Prf.cases)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	427	apply(simp_all)[5]
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	428	apply(auto)[1]
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	429	apply (metis Prf.intros(1))
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	430	apply(auto)[1]
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	431	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	432	apply(simp)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	433	apply(erule Prf.cases)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	434	apply(simp_all)[5]
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	435	apply(auto)[1]
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	436	apply(rule Prf.intros)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	437	apply(auto)[2]
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	438	done
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	439
53 38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	440	lemma v3_proj:
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	441	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	442	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	443	using assms
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	444	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	445	prefer 4
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	446	apply(simp)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	447	prefer 4
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	448	apply(simp)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	449	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	450	prefer 2
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	451	apply(simp)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	452	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	453	prefer 2
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	454	apply(simp)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	455	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	456	apply(auto)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	457	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	458	apply(simp)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	459	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	460	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	461	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	462	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	463	apply(simp)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	464	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	465	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	466	apply(simp)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	467	done
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	468
10 14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	469	text {*
53 38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	470	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	471	*}
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	472
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	473	lemma v4:
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	474	assumes "\<turnstile> v : der c r" shows "flat (injval r c v) = c # (flat v)"
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	475	using assms
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	476	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	477	apply(simp)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	478	apply(erule Prf.cases)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	479	apply(simp_all)[5]
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	480	apply(simp)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	481	apply(erule Prf.cases)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	482	apply(simp_all)[5]
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	483	apply(simp)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	484	apply(case_tac "c = c'")
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	485	apply(simp)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	486	apply(auto)[1]
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	487	apply(erule Prf.cases)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	488	apply(simp_all)[5]
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	489	apply(simp)
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(simp)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	493	apply(erule Prf.cases)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	494	apply(simp_all)[5]
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	495	apply(simp)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	496	apply(case_tac "nullable r1")
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	497	apply(simp)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	498	apply(erule Prf.cases)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	499	apply(simp_all)[5]
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	500	apply(auto)[1]
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	501	apply(erule Prf.cases)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	502	apply(simp_all)[5]
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 (metis mkeps_flat)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	505	apply(simp)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	506	apply(erule Prf.cases)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	507	apply(simp_all)[5]
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	508	done
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	509
53 38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	510	lemma v4_proj:
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	511	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	512	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	513	using assms
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	514	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	515	prefer 4
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	516	apply(simp)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	517	prefer 4
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	518	apply(simp)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	519	prefer 2
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	520	apply(simp)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	521	prefer 2
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	522	apply(simp)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	523	apply(auto)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	524	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	525
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	526	lemma v4_proj2:
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	527	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	528	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	529	using assms
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	530	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	531
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	532	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	533	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	534
62 a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	535	lemma t2: "(xs = ys) \<Longrightarrow> (c#xs) = (c#ys)"
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	536	by (metis)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	537
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	538	fun zeroable where
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	539	"zeroable NULL = True"
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	540	\| "zeroable EMPTY = False"
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	541	\| "zeroable (CHAR c) = False"
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	542	\| "zeroable (ALT r1 r2) = (zeroable r1 \<and> zeroable r2)"
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	543	\| "zeroable (SEQ r1 r2) = (zeroable r1 \<or> zeroable r2)"
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	544
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	545	lemma "\<not>(nullable r) \<Longrightarrow> \<not>(\<exists>v. \<turnstile> v : r \<and> flat v = [])"
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	546	by (metis Prf_flat_L nullable_correctness)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	547
53 38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	548	lemma Prf_inj:
62 a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	549	assumes "v1 \<succ>(der c r) v2" "\<turnstile> v1 : der c r" "\<turnstile> v2 : der c r" ("flat v1 = flat v2")
53 38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	550	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	551	using assms
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	552	apply(induct arbitrary: v1 v2 rule: der.induct)
55 c33cfa1e813a added some notes (still incomplete) Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 53 diff changeset	553	(* NULL case *)
53 38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	554	apply(simp)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	555	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	556	apply(simp_all)[8]
55 c33cfa1e813a added some notes (still incomplete) Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 53 diff changeset	557	(* EMPTY case *)
53 38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	558	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	559	apply(simp_all)[8]
55 c33cfa1e813a added some notes (still incomplete) Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 53 diff changeset	560	(* CHAR case *)
53 38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	561	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	562	apply(simp)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	563	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	564	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	565	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	566	apply(simp)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	567	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	568	apply(simp_all)[8]
55 c33cfa1e813a added some notes (still incomplete) Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 53 diff changeset	569	(* ALT case *)
53 38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	570	apply(simp)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	571	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	572	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	573	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	574	apply(subst v4)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	575	apply(clarify)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	576	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	577	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	578	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	579	apply(subst v4)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	580	apply(clarify)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	581	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	582	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	583	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	584	apply(simp)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	585	apply(rule ValOrd.intros)
62 a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	586	apply(clarify)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	587	apply(rotate_tac 3)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	588	apply(erule Prf.cases)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	589	apply(simp_all)[5]
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	590	apply(clarify)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	591	apply(erule Prf.cases)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	592	apply(simp_all)[5]
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	593	apply(clarify)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	594	apply(subst v4)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	595	apply(simp)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	596	apply(subst v4)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	597	apply(simp)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	598	apply(simp)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	599	apply(rule ValOrd.intros)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	600	apply(clarify)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	601	apply(erule Prf.cases)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	602	apply(simp_all)[5]
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	603	apply(erule Prf.cases)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	604	apply(simp_all)[5]
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	605	apply(rule ValOrd.intros)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	606	apply(clarify)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	607	apply(erule Prf.cases)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	608	apply(simp_all)[5]
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	609	apply(erule Prf.cases)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	610	apply(simp_all)[5]
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	611	(* SEQ case*)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	612	apply(simp)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	613	apply(case_tac "nullable r1")
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	614	apply(simp)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	615	defer
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	616	apply(simp)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	617	apply(erule Prf.cases)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	618	apply(simp_all)[5]
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	619	apply(erule Prf.cases)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	620	apply(simp_all)[5]
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	621	apply(clarify)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	622	apply(erule ValOrd.cases)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	623	apply(simp_all)[8]
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	624	apply(clarify)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	625	apply(rule ValOrd.intros)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	626	apply(simp)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	627	apply(clarify)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	628	apply(rule ValOrd.intros(2))
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	629	apply metis
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	630
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	631	apply(erule Prf.cases)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	632	apply(simp_all)[5]
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	633	apply(erule Prf.cases)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	634	apply(simp_all)[5]
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	635	apply(clarify)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	636	defer
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	637	apply(erule ValOrd.cases)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	638	apply(simp_all del: injval.simps)[8]
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	639	apply(simp)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	640	apply(clarify)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	641	apply(simp)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	642	apply(erule Prf.cases)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	643	apply(simp_all)[5]
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	644	apply(erule Prf.cases)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	645	apply(simp_all)[5]
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	646	apply(clarify)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	647	apply(erule Prf.cases)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	648	apply(simp_all)[5]
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	649	apply(clarify)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	650	apply(rule ValOrd.intros(2))
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	651
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	652
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	653	lemma POSIX_ex: "\<turnstile> v : r \<Longrightarrow> \<exists>v. POSIX v r"
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	654	apply(induct r arbitrary: v)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	655	apply(erule Prf.cases)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	656	apply(simp_all)[5]
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	657	apply(erule Prf.cases)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	658	apply(simp_all)[5]
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	659	apply(rule_tac x="Void" in exI)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	660	apply(simp add: POSIX_def)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	661	apply(auto)[1]
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	662	apply (metis Prf.intros(4))
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	663	apply(erule Prf.cases)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	664	apply(simp_all)[5]
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	665	apply (metis ValOrd.intros(7))
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	666	apply(erule Prf.cases)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	667	apply(simp_all)[5]
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	668	apply(rule_tac x="Char c" in exI)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	669	apply(simp add: POSIX_def)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	670	apply(auto)[1]
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	671	apply (metis Prf.intros(5))
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	672	apply(erule Prf.cases)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	673	apply(simp_all)[5]
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	674	apply (metis ValOrd.intros(8))
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	675	apply(erule Prf.cases)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	676	apply(simp_all)[5]
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	677	apply(auto)[1]
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	678	apply(drule_tac x="v1" in meta_spec)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	679	apply(drule_tac x="v2" in meta_spec)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	680	apply(auto)[1]
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	681	defer
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	682	apply(erule Prf.cases)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	683	apply(simp_all)[5]
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	684	apply(auto)[1]
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	685	apply (metis POSIX_ALT_I1)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	686	apply (metis POSIX_ALT_I1 POSIX_ALT_I2)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	687	apply(case_tac "nullable r1a")
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	688	apply(rule_tac x="Seq (mkeps r1a) va" in exI)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	689	apply(auto simp add: POSIX_def)[1]
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	690	apply (metis Prf.intros(1) mkeps_nullable)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	691	apply(simp add: mkeps_flat)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	692	apply(rotate_tac 7)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	693	apply(erule Prf.cases)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	694	apply(simp_all)[5]
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	695	apply(case_tac "mkeps r1 = v1a")
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	696	apply(simp)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	697	apply (rule ValOrd.intros(1))
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	698	apply (metis append_Nil mkeps_flat)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	699	apply (rule ValOrd.intros(2))
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	700	apply(drule mkeps_POSIX)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	701	apply(simp add: POSIX_def)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	702
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	703	apply metis
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	704	apply(simp)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	705	apply(simp)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	706	apply(erule disjE)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	707	apply(simp)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	708
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	709	apply(drule_tac x="v2" in spec)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	710
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	711	lemma POSIX_ex2: "\<turnstile> v : r \<Longrightarrow> \<exists>v. POSIX v r \<and> \<turnstile> v : r"
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	712	apply(induct r arbitrary: v)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	713	apply(erule Prf.cases)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	714	apply(simp_all)[5]
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	715	apply(erule Prf.cases)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	716	apply(simp_all)[5]
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	717	apply(rule_tac x="Void" in exI)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	718	apply(simp add: POSIX_def)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	719	apply(auto)[1]
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	720	apply(erule Prf.cases)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	721	apply(simp_all)[5]
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	722	apply (metis ValOrd.intros(7))
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	723	apply (metis Prf.intros(4))
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	724	apply(erule Prf.cases)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	725	apply(simp_all)[5]
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	726	apply(rule_tac x="Char c" in exI)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	727	apply(simp add: POSIX_def)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	728	apply(auto)[1]
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	729	apply(erule Prf.cases)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	730	apply(simp_all)[5]
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	731	apply (metis ValOrd.intros(8))
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	732	apply (metis Prf.intros(5))
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	733	apply(erule Prf.cases)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	734	apply(simp_all)[5]
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	735	apply(auto)[1]
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	736	apply(drule_tac x="v1" in meta_spec)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	737	apply(drule_tac x="v2" in meta_spec)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	738	apply(auto)[1]
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	739	apply(simp add: POSIX_def)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	740	apply(auto)[1]
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	741	apply(rule ccontr)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	742	apply(simp)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	743	apply(drule_tac x="Seq v va" in spec)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	744	apply(drule mp)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	745	defer
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	746	apply (metis Prf.intros(1))
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	747
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	748
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	749	oops
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	750
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	751	lemma POSIX_ALT_cases:
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	752	assumes "\<turnstile> v : (ALT r1 r2)" "POSIX v (ALT r1 r2)"
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	753	shows "(\<exists>v1. v = Left v1 \<and> POSIX v1 r1) \<or> (\<exists>v2. v = Right v2 \<and> POSIX v2 r2)"
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	754	using assms
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	755	apply(erule_tac Prf.cases)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	756	apply(simp_all)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	757	unfolding POSIX_def
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	758	apply(auto)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	759	apply (metis POSIX_ALT2 POSIX_def assms(2))
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	760	by (metis POSIX_ALT1b assms(2))
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	761
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	762	lemma POSIX_ALT_cases2:
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	763	assumes "POSIX v (ALT r1 r2)" "\<turnstile> v : (ALT r1 r2)"
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	764	shows "(\<exists>v1. v = Left v1 \<and> POSIX v1 r1) \<or> (\<exists>v2. v = Right v2 \<and> POSIX v2 r2)"
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	765	using assms POSIX_ALT_cases by auto
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	766
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	767	lemma Prf_flat_empty:
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	768	assumes "\<turnstile> v : r" "flat v = []"
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	769	shows "nullable r"
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	770	using assms
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	771	apply(induct)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	772	apply(auto)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	773	done
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	774
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	775	lemma POSIX_proj:
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	776	assumes "POSIX v r" "\<turnstile> v : r" "\<exists>s. flat v = c#s"
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	777	shows "POSIX (projval r c v) (der c r)"
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	778	using assms
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	779	apply(induct r c v arbitrary: rule: projval.induct)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	780	defer
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	781	defer
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	782	defer
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	783	defer
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	784	apply(erule Prf.cases)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	785	apply(simp_all)[5]
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	786	apply(erule Prf.cases)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	787	apply(simp_all)[5]
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	788	apply(erule Prf.cases)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	789	apply(simp_all)[5]
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	790	apply(erule Prf.cases)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	791	apply(simp_all)[5]
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	792	apply(erule Prf.cases)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	793	apply(simp_all)[5]
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	794	apply(erule Prf.cases)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	795	apply(simp_all)[5]
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	796	apply(erule Prf.cases)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	797	apply(simp_all)[5]
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	798	apply(erule Prf.cases)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	799	apply(simp_all)[5]
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	800	apply(erule Prf.cases)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	801	apply(simp_all)[5]
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	802	apply(erule Prf.cases)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	803	apply(simp_all)[5]
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	804	apply(simp add: POSIX_def)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	805	apply(auto)[1]
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	806	apply(erule Prf.cases)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	807	apply(simp_all)[5]
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	808	apply (metis ValOrd.intros(7))
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	809	apply(erule_tac [!] exE)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	810	prefer 3
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	811	apply(frule POSIX_SEQ1)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	812	apply(erule Prf.cases)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	813	apply(simp_all)[5]
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	814	apply(erule Prf.cases)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	815	apply(simp_all)[5]
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	816	apply(case_tac "flat v1 = []")
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	817	apply(subgoal_tac "nullable r1")
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	818	apply(simp)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	819	prefer 2
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	820	apply(rule_tac v="v1" in Prf_flat_empty)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	821	apply(erule Prf.cases)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	822	apply(simp_all)[5]
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	823	apply(simp)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	824	apply(frule POSIX_SEQ2)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	825	apply(erule Prf.cases)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	826	apply(simp_all)[5]
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	827	apply(erule Prf.cases)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	828	apply(simp_all)[5]
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	829	apply(simp)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	830	apply(drule meta_mp)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	831	apply(erule Prf.cases)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	832	apply(simp_all)[5]
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	833	apply(rule ccontr)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	834	apply(subgoal_tac "\<turnstile> val.Right (projval r2 c v2) : (ALT (SEQ (der c r1) r2) (der c r2))")
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	835	apply(rotate_tac 11)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	836	apply(frule POSIX_ex)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	837	apply(erule exE)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	838	apply(drule POSIX_ALT_cases2)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	839	apply(erule Prf.cases)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	840	apply(simp_all)[5]
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	841	apply(drule v3_proj)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	842	apply(simp)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	843	apply(simp)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	844	apply(drule POSIX_ex)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	845	apply(erule exE)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	846	apply(frule POSIX_ALT_cases2)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	847	apply(simp)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	848	apply(simp)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	849	apply(erule
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	850	prefer 2
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	851	apply(case_tac "nullable r1")
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	852	prefer 2
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	853	apply(simp)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	854	apply(rotate_tac 1)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	855	apply(drule meta_mp)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	856	apply(rule POSIX_SEQ1)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	857	apply(assumption)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	858	apply(erule Prf.cases)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	859	apply(simp_all)[5]
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	860	apply(erule Prf.cases)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	861	apply(simp_all)[5]
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	862	apply(rotate_tac 7)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	863	apply(drule meta_mp)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	864	apply(erule Prf.cases)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	865	apply(simp_all)[5]
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	866	apply(rotate_tac 7)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	867	apply(drule meta_mp)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	868	apply (metis Cons_eq_append_conv)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	869
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	870
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	871	apply(erule Prf.cases)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	872	apply(simp_all)[5]
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	873	apply(simp add: POSIX_def)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	874	apply(simp)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	875	apply(simp)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	876	apply(simp_all)[5]
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	877	apply(simp add: POSIX_def)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	878
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	879
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	880	lemma POSIX_proj:
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	881	assumes "POSIX v r" "\<turnstile> v : r" "\<exists>s. flat v = c#s"
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	882	shows "POSIX (projval r c v) (der c r)"
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	883	using assms
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	884	apply(induct r arbitrary: c v rule: rexp.induct)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	885	apply(erule Prf.cases)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	886	apply(simp_all)[5]
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	887	apply(erule Prf.cases)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	888	apply(simp_all)[5]
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	889	apply(erule Prf.cases)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	890	apply(simp_all)[5]
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	891	apply(simp add: POSIX_def)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	892	apply(auto)[1]
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	893	apply(erule Prf.cases)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	894	apply(simp_all)[5]
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	895	apply (metis ValOrd.intros(7))
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	896
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	897	apply(erule Prf.cases)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	898	apply(simp_all)[5]
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	899	apply(erule Prf.cases)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	900	apply(simp_all)[5]
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	901	apply(erule Prf.cases)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	902	apply(simp_all)[5]
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	903	apply(erule Prf.cases)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	904	apply(simp_all)[5]
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	905	apply(erule Prf.cases)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	906	apply(simp_all)[5]
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	907	apply(erule Prf.cases)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	908	apply(simp_all)[5]
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	909	apply(simp add: POSIX_def)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	910	apply(auto)[1]
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	911	apply(erule Prf.cases)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	912	apply(simp_all)[5]
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	913	apply (metis ValOrd.intros(7))
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	914	apply(erule_tac [!] exE)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	915	prefer 3
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	916	apply(frule POSIX_SEQ1)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	917	apply(erule Prf.cases)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	918	apply(simp_all)[5]
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	919	apply(erule Prf.cases)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	920	apply(simp_all)[5]
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	921	apply(case_tac "flat v1 = []")
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	922	apply(subgoal_tac "nullable r1")
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	923	apply(simp)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	924	prefer 2
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	925	apply(rule_tac v="v1" in Prf_flat_empty)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	926	apply(erule Prf.cases)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	927	apply(simp_all)[5]
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	928
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	929
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	930	lemma POSIX_proj:
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	931	assumes "POSIX v r" "\<turnstile> v : r" "\<exists>s. flat v = c#s"
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	932	shows "POSIX (projval r c v) (der c r)"
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	933	using assms
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	934	apply(induct r c v arbitrary: rule: projval.induct)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	935	defer
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	936	defer
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	937	defer
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	938	defer
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	939	apply(erule Prf.cases)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	940	apply(simp_all)[5]
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	941	apply(erule Prf.cases)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	942	apply(simp_all)[5]
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	943	apply(erule Prf.cases)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	944	apply(simp_all)[5]
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	945	apply(erule Prf.cases)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	946	apply(simp_all)[5]
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	947	apply(erule Prf.cases)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	948	apply(simp_all)[5]
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	949	apply(erule Prf.cases)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	950	apply(simp_all)[5]
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	951	apply(erule Prf.cases)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	952	apply(simp_all)[5]
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	953	apply(erule Prf.cases)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	954	apply(simp_all)[5]
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	955	apply(erule Prf.cases)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	956	apply(simp_all)[5]
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	957	apply(erule Prf.cases)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	958	apply(simp_all)[5]
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	959	apply(simp add: POSIX_def)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	960	apply(auto)[1]
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	961	apply(erule Prf.cases)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	962	apply(simp_all)[5]
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	963	apply (metis ValOrd.intros(7))
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	964	apply(erule_tac [!] exE)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	965	prefer 3
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	966	apply(frule POSIX_SEQ1)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	967	apply(erule Prf.cases)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	968	apply(simp_all)[5]
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	969	apply(erule Prf.cases)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	970	apply(simp_all)[5]
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	971	apply(case_tac "flat v1 = []")
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	972	apply(subgoal_tac "nullable r1")
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	973	apply(simp)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	974	prefer 2
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	975	apply(rule_tac v="v1" in Prf_flat_empty)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	976	apply(erule Prf.cases)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	977	apply(simp_all)[5]
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	978	apply(simp)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	979	apply(rule ccontr)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	980	apply(drule v3_proj)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	981	apply(simp)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	982	apply(simp)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	983	apply(drule POSIX_ex)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	984	apply(erule exE)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	985	apply(frule POSIX_ALT_cases2)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	986	apply(simp)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	987	apply(simp)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	988	apply(erule
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	989	prefer 2
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	990	apply(case_tac "nullable r1")
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	991	prefer 2
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	992	apply(simp)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	993	apply(rotate_tac 1)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	994	apply(drule meta_mp)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	995	apply(rule POSIX_SEQ1)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	996	apply(assumption)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	997	apply(erule Prf.cases)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	998	apply(simp_all)[5]
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	999	apply(erule Prf.cases)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	1000	apply(simp_all)[5]
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	1001	apply(rotate_tac 7)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	1002	apply(drule meta_mp)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	1003	apply(erule Prf.cases)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	1004	apply(simp_all)[5]
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	1005	apply(rotate_tac 7)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	1006	apply(drule meta_mp)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	1007	apply (metis Cons_eq_append_conv)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	1008
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	1009
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	1010	apply(erule Prf.cases)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	1011	apply(simp_all)[5]
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	1012	apply(simp add: POSIX_def)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	1013	apply(simp)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	1014	apply(simp)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	1015	apply(simp_all)[5]
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	1016	apply(simp add: POSIX_def)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	1017
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	1018	done
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	1019	(* NULL case *)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	1020	apply(simp add: POSIX_def)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	1021	apply(auto)[1]
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	1022	apply(erule Prf.cases)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	1023	apply(simp_all)[5]
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	1024	apply(erule Prf.cases)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	1025	apply(simp_all)[5]
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	1026	apply (metis ValOrd.intros(7))
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	1027	apply(rotate_tac 4)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	1028	apply(erule Prf.cases)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	1029	apply(simp_all)[5]
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	1030	apply(simp)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	1031	prefer 2
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	1032	apply(simp)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	1033	apply(frule POSIX_ALT1a)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	1034	apply(drule meta_mp)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	1035	apply(simp)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	1036	apply(drule meta_mp)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	1037	apply(erule Prf.cases)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	1038	apply(simp_all)[5]
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	1039	apply(rule POSIX_ALT_I2)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	1040	apply(assumption)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	1041	apply(auto)[1]
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	1042
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	1043	thm v4_proj2
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	1044	prefer 2
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	1045	apply(subst (asm) (13) POSIX_def)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	1046
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	1047	apply(drule_tac x="projval v2" in spec)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	1048	apply(auto)[1]
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	1049	apply(drule mp)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	1050	apply(rule conjI)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	1051	apply(simp)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	1052	apply(simp)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	1053
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	1054	apply(erule Prf.cases)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	1055	apply(simp_all)[5]
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	1056	apply(erule Prf.cases)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	1057	apply(simp_all)[5]
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	1058	prefer 2
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	1059	apply(clarify)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	1060	apply(subst (asm) (2) POSIX_def)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	1061
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	1062	apply (metis ValOrd.intros(5))
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	1063	apply(clarify)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	1064	apply(simp)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	1065	apply(rotate_tac 3)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	1066	apply(drule_tac c="c" in t2)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	1067	apply(subst (asm) v4_proj)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	1068	apply(simp)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	1069	apply(simp)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	1070	thm contrapos_np contrapos_nn
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	1071	apply(erule contrapos_np)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	1072	apply(rule ValOrd.intros)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	1073	apply(subst v4_proj2)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	1074	apply(simp)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	1075	apply(simp)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	1076	apply(subgoal_tac "\<not>(length (flat v1) < length (flat (projval r2a c v2a)))")
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	1077	prefer 2
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	1078	apply(erule contrapos_nn)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	1079	apply (metis nat_less_le v4_proj2)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	1080	apply(simp)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	1081
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	1082	apply(blast)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	1083	thm contrapos_nn
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	1084
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	1085	apply(simp add: POSIX_def)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	1086	apply(auto)[1]
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	1087	apply(erule Prf.cases)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	1088	apply(simp_all)[5]
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	1089	apply(erule Prf.cases)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	1090	apply(simp_all)[5]
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	1091	apply(clarify)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	1092	apply(rule ValOrd.intros)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	1093	apply(drule meta_mp)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	1094	apply(auto)[1]
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	1095	apply (metis POSIX_ALT2 POSIX_def flat.simps(3))
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	1096	apply metis
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	1097	apply(clarify)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	1098	apply(rule ValOrd.intros)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	1099	apply(simp)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	1100	apply(simp add: POSIX_def)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	1101	apply(auto)[1]
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	1102	apply(erule Prf.cases)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	1103	apply(simp_all)[5]
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	1104	apply(erule Prf.cases)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	1105	apply(simp_all)[5]
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	1106	apply(clarify)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	1107	apply(rule ValOrd.intros)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	1108	apply(simp)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	1109
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	1110	apply(drule meta_mp)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	1111	apply(auto)[1]
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	1112	apply (metis POSIX_ALT2 POSIX_def flat.simps(3))
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	1113	apply metis
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	1114	apply(clarify)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	1115	apply(rule ValOrd.intros)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	1116	apply(simp)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	1117
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	1118
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	1119	done
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	1120	(* EMPTY case *)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	1121	apply(simp add: POSIX_def)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	1122	apply(auto)[1]
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	1123	apply(rotate_tac 3)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	1124	apply(erule Prf.cases)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	1125	apply(simp_all)[5]
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	1126	apply(drule_tac c="c" in t2)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	1127	apply(subst (asm) v4_proj)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	1128	apply(auto)[2]
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	1129
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	1130	apply(erule ValOrd.cases)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	1131	apply(simp_all)[8]
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	1132	(* CHAR case *)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	1133	apply(case_tac "c = c'")
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	1134	apply(simp)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	1135	apply(erule ValOrd.cases)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	1136	apply(simp_all)[8]
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	1137	apply(rule ValOrd.intros)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	1138	apply(simp)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	1139	apply(erule ValOrd.cases)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	1140	apply(simp_all)[8]
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	1141	(* ALT case *)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	1142
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	1143
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	1144	unfolding POSIX_def
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	1145	apply(auto)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	1146	thm v4
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	1147
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	1148	lemma Prf_inj:
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	1149	assumes "v1 \<succ>(der c r) v2" "\<turnstile> v1 : der c r" "\<turnstile> v2 : der c r" "flat v1 = flat v2"
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	1150	shows "(injval r c v1) \<succ>r (injval r c v2)"
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	1151	using assms
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	1152	apply(induct arbitrary: v1 v2 rule: der.induct)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	1153	(* NULL case *)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	1154	apply(simp)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	1155	apply(erule ValOrd.cases)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	1156	apply(simp_all)[8]
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	1157	(* EMPTY case *)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	1158	apply(erule ValOrd.cases)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	1159	apply(simp_all)[8]
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	1160	(* CHAR case *)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	1161	apply(case_tac "c = c'")
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	1162	apply(simp)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	1163	apply(erule ValOrd.cases)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	1164	apply(simp_all)[8]
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	1165	apply(rule ValOrd.intros)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	1166	apply(simp)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	1167	apply(erule ValOrd.cases)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	1168	apply(simp_all)[8]
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	1169	(* ALT case *)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	1170	apply(simp)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	1171	apply(erule ValOrd.cases)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	1172	apply(simp_all)[8]
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	1173	apply(rule ValOrd.intros)
53 38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	1174	apply(subst v4)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	1175	apply(clarify)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	1176	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	1177	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	1178	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	1179	apply(subst v4)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	1180	apply(clarify)
62 a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	1181	apply(rotate_tac 2)
53 38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	1182	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	1183	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	1184	apply(simp)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	1185	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	1186	apply(clarify)
62 a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	1187	apply(rotate_tac 3)
53 38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	1188	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	1189	apply(simp_all)[5]
62 a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	1190	apply(clarify)
53 38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	1191	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	1192	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	1193	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	1194	apply(clarify)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	1195	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	1196	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	1197	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	1198	apply(simp_all)[5]
55 c33cfa1e813a added some notes (still incomplete) Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 53 diff changeset	1199	(* SEQ case*)
53 38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	1200	apply(simp)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	1201	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	1202	defer
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	1203	apply(simp)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	1204	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	1205	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	1206	apply(clarify)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	1207	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	1208	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	1209	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	1210	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	1211	apply(clarify)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	1212	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	1213	apply(simp)
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(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	1216	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	1217	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	1218	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	1219	apply(simp_all)[5]
62 a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	1220	apply(clarify)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	1221	defer
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	1222	apply(simp)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	1223	apply(erule ValOrd.cases)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	1224	apply(simp_all del: injval.simps)[8]
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	1225	apply(simp)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	1226	apply(clarify)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	1227	apply(simp)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	1228	apply(erule Prf.cases)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	1229	apply(simp_all)[5]
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	1230	apply(erule Prf.cases)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	1231	apply(simp_all)[5]
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	1232	apply(clarify)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	1233	apply(erule Prf.cases)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	1234	apply(simp_all)[5]
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	1235	apply(clarify)
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	1236	apply(rule ValOrd.intros(2))
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	1237
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	1238
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	1239
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	1240
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	1241	done
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	1242
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	1243
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	1244	txt {*
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	1245	done
55 c33cfa1e813a added some notes (still incomplete) Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 53 diff changeset	1246	(* nullable case - unfinished *)
53 38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	1247	apply(simp)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	1248	apply(erule ValOrd.cases)
62 a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	1249	apply(simp_all del: injval.simps)[8]
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	1250	apply(simp)
53 38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	1251	apply(clarify)
55 c33cfa1e813a added some notes (still incomplete) Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 53 diff changeset	1252	apply(simp)
53 38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	1253	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	1254	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	1255	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	1256	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	1257	apply(clarify)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	1258	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	1259	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	1260	apply(clarify)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	1261	apply(simp)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	1262	apply(rule ValOrd.intros(2))
62 a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	1263	oops
a6bb0152ccc2 updated some rules Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 56 diff changeset	1264	*}
55 c33cfa1e813a added some notes (still incomplete) Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 53 diff changeset	1265	oops
53 38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	1266
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	1267	lemma POSIX_der:
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	1268	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	1269	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	1270	using assms
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	1271	unfolding POSIX_def
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	1272	apply(auto)
55 c33cfa1e813a added some notes (still incomplete) Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 53 diff changeset	1273	thm v4
53 38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	1274	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	1275	apply(assumption)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	1276	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	1277	apply(auto)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	1278	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	1279	apply(simp)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	1280	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	1281	apply(simp)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	1282	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	1283	apply(simp)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	1284	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	1285	apply(simp)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	1286	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	1287	apply(simp)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	1288	apply(simp)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	1289	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	1290	apply(auto)[1]
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	1291
10 14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1292	text {*
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1293	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	1294	*}
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1295
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1296	lemma proj_inj_id:
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1297	assumes "\<turnstile> v : der c r"
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1298	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	1299	using assms
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1300	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	1301	apply(simp)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1302	apply(erule Prf.cases)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1303	apply(simp_all)[5]
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1304	apply(simp)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1305	apply(erule Prf.cases)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1306	apply(simp_all)[5]
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1307	apply(simp)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1308	apply(case_tac "c = char")
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1309	apply(simp)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1310	apply(erule Prf.cases)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1311	apply(simp_all)[5]
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1312	apply(simp)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1313	apply(erule Prf.cases)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1314	apply(simp_all)[5]
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1315	defer
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1316	apply(simp)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1317	apply(erule Prf.cases)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1318	apply(simp_all)[5]
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1319	apply(simp)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1320	apply(case_tac "nullable rexp1")
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1321	apply(simp)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1322	apply(erule Prf.cases)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1323	apply(simp_all)[5]
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1324	apply(auto)[1]
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1325	apply(erule Prf.cases)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1326	apply(simp_all)[5]
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1327	apply(auto)[1]
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1328	apply (metis list.distinct(1) v4)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1329	apply(auto)[1]
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1330	apply (metis mkeps_flat)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1331	apply(auto)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1332	apply(erule Prf.cases)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1333	apply(simp_all)[5]
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1334	apply(auto)[1]
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1335	apply(simp add: v4)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1336	done
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1337
48 652861c9473f added a function for calculating values Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 20 diff changeset	1338	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	1339	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	1340	apply(simp)
652861c9473f added a function for calculating values Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 20 diff changeset	1341	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	1342	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	1343	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	1344	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	1345	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	1346	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	1347	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	1348	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	1349	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	1350	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	1351	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	1352	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	1353	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	1354	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	1355	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	1356	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	1357	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	1358	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	1359	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	1360	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	1361	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	1362	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	1363	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	1364	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	1365	apply(clarify)
652861c9473f added a function for calculating values Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 20 diff changeset	1366	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	1367	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	1368	apply(simp)
652861c9473f added a function for calculating values Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 20 diff changeset	1369	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	1370	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	1371	apply(simp)
652861c9473f added a function for calculating values Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 20 diff changeset	1372	apply(simp)
652861c9473f added a function for calculating values Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 20 diff changeset	1373	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	1374	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	1375	oops
48 652861c9473f added a function for calculating values Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 20 diff changeset	1376
10 14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1377	lemma "\<exists>v. POSIX v r"
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1378	apply(induct r)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1379	apply(rule exI)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1380	apply(simp add: POSIX_def)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1381	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	1382	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	1383	apply(simp add: POSIX_def)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1384	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	1385	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	1386	apply(simp add: POSIX_def)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1387	apply(auto) [1]
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1388	apply(erule Prf.cases)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1389	apply(simp_all) [5]
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1390	apply (metis ValOrd.intros(8))
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1391	defer
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1392	apply(auto)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1393	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	1394	(* 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	1395	(* 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	1396	apply(case_tac "r1 = NULL")
c11651bbebf5 some small changes Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 12 diff changeset	1397	apply(simp add: POSIX_def)
c11651bbebf5 some small changes Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 12 diff changeset	1398	apply(auto)[1]
c11651bbebf5 some small changes Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 12 diff changeset	1399	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	1400	apply(case_tac "r1 = EMPTY")
c11651bbebf5 some small changes Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 12 diff changeset	1401	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	1402	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	1403	apply(auto)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1404	apply(erule Prf.cases)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1405	apply(simp_all)
20 c11651bbebf5 some small changes Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 12 diff changeset	1406	apply(auto)[1]
c11651bbebf5 some small changes Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 12 diff changeset	1407	apply(erule Prf.cases)
c11651bbebf5 some small changes Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 12 diff changeset	1408	apply(simp_all)
c11651bbebf5 some small changes Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 12 diff changeset	1409	apply(rule ValOrd.intros(2))
c11651bbebf5 some small changes Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 12 diff changeset	1410	apply(rule ValOrd.intros)
c11651bbebf5 some small changes Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 12 diff changeset	1411	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	1412	apply(auto)
c11651bbebf5 some small changes Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 12 diff changeset	1413	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	1414	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	1415	apply(auto)
c11651bbebf5 some small changes Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 12 diff changeset	1416	apply(erule Prf.cases)
c11651bbebf5 some small changes Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 12 diff changeset	1417	apply(simp_all)
c11651bbebf5 some small changes Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 12 diff changeset	1418	apply(auto)[1]
c11651bbebf5 some small changes Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 12 diff changeset	1419	apply(erule Prf.cases)
c11651bbebf5 some small changes Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 12 diff changeset	1420	apply(simp_all)
c11651bbebf5 some small changes Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 12 diff changeset	1421	apply(auto)[1]
c11651bbebf5 some small changes Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 12 diff changeset	1422	apply(rule ValOrd.intros(2))
c11651bbebf5 some small changes Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 12 diff changeset	1423	apply(rule ValOrd.intros)
c11651bbebf5 some small changes Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 12 diff changeset	1424	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	1425	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	1426	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	1427
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1428	text {*
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1429
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1430	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	1431
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1432	*}
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1433	lemma v5:
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1434	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	1435	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	1436	using assms
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1437	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	1438	(* NULL case *)
10 14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1439	apply(simp)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1440	apply(erule Prf.cases)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1441	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	1442	(* EMPTY case *)
10 14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1443	apply(simp)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1444	apply(erule Prf.cases)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1445	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	1446	(* CHAR case *)
10 14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1447	apply(simp)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1448	apply(case_tac "c = c'")
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1449	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	1450	apply(erule Prf.cases)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1451	apply(simp_all)[5]
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1452	apply(erule Prf.cases)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1453	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	1454	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	1455	apply(auto)[1]
10 14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1456	apply(erule Prf.cases)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1457	apply(simp_all)[5]
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1458	(* base cases done *)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1459	(* ALT case *)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1460	apply(erule Prf.cases)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1461	apply(simp_all)[5]
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1462	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	1463	apply(clarify)
53 38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	1464	apply(simp)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	1465	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	1466	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	1467	apply metis
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	1468	apply(auto)[1]
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	1469	apply(subst v4)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	1470	apply(assumption)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	1471	apply(simp)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	1472	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	1473	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	1474	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	1475	apply(simp)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	1476
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	1477	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	1478	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	1479	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	1480	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	1481	apply(simp)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	1482	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	1483	apply(assumption)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	1484	apply(clarify)
38cde0214ad5 added some lemmas, attempted others Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 49 diff changeset	1485	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	1486	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	1487	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	1488	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	1489	prefer 2
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1490	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	1491	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	1492	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	1493	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	1494	apply(rule POSIX_ALT_I2)
10 14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1495	apply(rotate_tac 1)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1496	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	1497	apply(simp)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1498	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	1499	prefer 2
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1500	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	1501	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	1502	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	1503	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	1504	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	1505	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	1506	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	1507	apply(simp)
652861c9473f added a function for calculating values Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 20 diff changeset	1508
652861c9473f added a function for calculating values Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 20 diff changeset	1509	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	1510
652861c9473f added a function for calculating values Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 20 diff changeset	1511	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	1512	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	1513
10 14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1514	apply(rule ccontr)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1515	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	1516
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1517	apply(rule allI)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1518	apply(rule impI)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1519	apply(erule conjE)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1520	thm POSIX_ALT_I2
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1521	apply(frule POSIX_ALT1a)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1522	apply(drule POSIX_ALT1b)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1523	apply(rule POSIX_ALT_I2)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1524	apply auto[1]
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1525	apply(subst v4)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1526	apply(auto)[2]
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1527	apply(rotate_tac 1)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1528	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	1529	apply(simp)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1530	apply(subst (asm) (4) POSIX_def)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1531	apply(subst (asm) v4)
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1532	apply(auto)[2]
14d41b5b57b3 added test version Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1533	(* stuck in the ALT case *)

author	Christian Urban <christian dot urban at kcl dot ac dot uk>
	Mon, 09 Feb 2015 12:13:10 +0000
changeset 62	a6bb0152ccc2
parent 56	5bc72d6d633d
child 63	498171d2379a
permissions	-rw-r--r--