lexing: thys/Re.thy@26202889f829 (annotated)

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

author	Christian Urban <christian dot urban at kcl dot ac dot uk>
	Thu, 17 Dec 2015 14:16:24 +0000
changeset 82	26202889f829
parent 10	14d41b5b57b3
child 83	a8bcb5a0f9b9
permissions	-rw-r--r--