lexing: thys/Positions.thy@32b222d77fa0 (annotated)

248 b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	1
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	2	theory Positions
266 fff2e1b40dfc updated Christian Urban <urbanc@in.tum.de> parents: 265 diff changeset	3	imports "Spec"
248 b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	4	begin
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	5
265 d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	6	section {* Positions in Values *}
254 7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	7
248 b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	8	fun
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	9	at :: "val \<Rightarrow> nat list \<Rightarrow> val"
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	10	where
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	11	"at v [] = v"
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	12	\| "at (Left v) (0#ps)= at v ps"
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	13	\| "at (Right v) (Suc 0#ps)= at v ps"
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	14	\| "at (Seq v1 v2) (0#ps)= at v1 ps"
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	15	\| "at (Seq v1 v2) (Suc 0#ps)= at v2 ps"
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	16	\| "at (Stars vs) (n#ps)= at (nth vs n) ps"
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	17
265 d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	18
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	19
248 b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	20	fun Pos :: "val \<Rightarrow> (nat list) set"
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	21	where
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	22	"Pos (Void) = {[]}"
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	23	\| "Pos (Char c) = {[]}"
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	24	\| "Pos (Left v) = {[]} \<union> {0#ps \| ps. ps \<in> Pos v}"
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	25	\| "Pos (Right v) = {[]} \<union> {1#ps \| ps. ps \<in> Pos v}"
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	26	\| "Pos (Seq v1 v2) = {[]} \<union> {0#ps \| ps. ps \<in> Pos v1} \<union> {1#ps \| ps. ps \<in> Pos v2}"
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	27	\| "Pos (Stars []) = {[]}"
251 925232418a15 polished Christian Urban <urbanc@in.tum.de> parents: 250 diff changeset	28	\| "Pos (Stars (v#vs)) = {[]} \<union> {0#ps \| ps. ps \<in> Pos v} \<union> {Suc n#ps \| n ps. n#ps \<in> Pos (Stars vs)}"
248 b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	29
265 d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	30
253 ca4e9eb8d576 polished Christian Urban <urbanc@in.tum.de> parents: 252 diff changeset	31	lemma Pos_stars:
ca4e9eb8d576 polished Christian Urban <urbanc@in.tum.de> parents: 252 diff changeset	32	"Pos (Stars vs) = {[]} \<union> (\<Union>n < length vs. {n#ps \| ps. ps \<in> Pos (vs ! n)})"
ca4e9eb8d576 polished Christian Urban <urbanc@in.tum.de> parents: 252 diff changeset	33	apply(induct vs)
267 32b222d77fa0 updated Christian Urban <urbanc@in.tum.de> parents: 266 diff changeset	34	apply(auto simp add: insert_ident less_Suc_eq_0_disj)
32b222d77fa0 updated Christian Urban <urbanc@in.tum.de> parents: 266 diff changeset	35	done
253 ca4e9eb8d576 polished Christian Urban <urbanc@in.tum.de> parents: 252 diff changeset	36
248 b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	37	lemma Pos_empty:
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	38	shows "[] \<in> Pos v"
251 925232418a15 polished Christian Urban <urbanc@in.tum.de> parents: 250 diff changeset	39	by (induct v rule: Pos.induct)(auto)
248 b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	40
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	41	fun intlen :: "'a list \<Rightarrow> int"
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	42	where
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	43	"intlen [] = 0"
265 d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	44	\| "intlen (x # xs) = 1 + intlen xs"
248 b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	45
267 32b222d77fa0 updated Christian Urban <urbanc@in.tum.de> parents: 266 diff changeset	46	lemma intlen_int:
32b222d77fa0 updated Christian Urban <urbanc@in.tum.de> parents: 266 diff changeset	47	shows "intlen xs = int (length xs)"
32b222d77fa0 updated Christian Urban <urbanc@in.tum.de> parents: 266 diff changeset	48	by (induct xs)(simp_all)
32b222d77fa0 updated Christian Urban <urbanc@in.tum.de> parents: 266 diff changeset	49
255 222ed43892ea updated Christian Urban <urbanc@in.tum.de> parents: 254 diff changeset	50	lemma intlen_bigger:
248 b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	51	shows "0 \<le> intlen xs"
251 925232418a15 polished Christian Urban <urbanc@in.tum.de> parents: 250 diff changeset	52	by (induct xs)(auto)
248 b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	53
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	54	lemma intlen_append:
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	55	shows "intlen (xs @ ys) = intlen xs + intlen ys"
267 32b222d77fa0 updated Christian Urban <urbanc@in.tum.de> parents: 266 diff changeset	56	by (simp add: intlen_int)
248 b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	57
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	58	lemma intlen_length:
256 146b4817aebd updated Christian Urban <urbanc@in.tum.de> parents: 255 diff changeset	59	shows "intlen xs < intlen ys \<longleftrightarrow> length xs < length ys"
267 32b222d77fa0 updated Christian Urban <urbanc@in.tum.de> parents: 266 diff changeset	60	by (simp add: intlen_int)
248 b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	61
265 d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	62	lemma intlen_length_eq:
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	63	shows "intlen xs = intlen ys \<longleftrightarrow> length xs = length ys"
267 32b222d77fa0 updated Christian Urban <urbanc@in.tum.de> parents: 266 diff changeset	64	by (simp add: intlen_int)
255 222ed43892ea updated Christian Urban <urbanc@in.tum.de> parents: 254 diff changeset	65
248 b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	66	definition pflat_len :: "val \<Rightarrow> nat list => int"
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	67	where
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	68	"pflat_len v p \<equiv> (if p \<in> Pos v then intlen (flat (at v p)) else -1)"
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	69
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	70	lemma pflat_len_simps:
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	71	shows "pflat_len (Seq v1 v2) (0#p) = pflat_len v1 p"
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	72	and "pflat_len (Seq v1 v2) (Suc 0#p) = pflat_len v2 p"
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	73	and "pflat_len (Left v) (0#p) = pflat_len v p"
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	74	and "pflat_len (Left v) (Suc 0#p) = -1"
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	75	and "pflat_len (Right v) (Suc 0#p) = pflat_len v p"
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	76	and "pflat_len (Right v) (0#p) = -1"
251 925232418a15 polished Christian Urban <urbanc@in.tum.de> parents: 250 diff changeset	77	and "pflat_len (Stars (v#vs)) (Suc n#p) = pflat_len (Stars vs) (n#p)"
925232418a15 polished Christian Urban <urbanc@in.tum.de> parents: 250 diff changeset	78	and "pflat_len (Stars (v#vs)) (0#p) = pflat_len v p"
248 b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	79	and "pflat_len v [] = intlen (flat v)"
251 925232418a15 polished Christian Urban <urbanc@in.tum.de> parents: 250 diff changeset	80	by (auto simp add: pflat_len_def Pos_empty)
248 b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	81
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	82	lemma pflat_len_Stars_simps:
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	83	assumes "n < length vs"
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	84	shows "pflat_len (Stars vs) (n#p) = pflat_len (vs!n) p"
267 32b222d77fa0 updated Christian Urban <urbanc@in.tum.de> parents: 266 diff changeset	85	using assms
248 b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	86	apply(induct vs arbitrary: n p)
251 925232418a15 polished Christian Urban <urbanc@in.tum.de> parents: 250 diff changeset	87	apply(auto simp add: less_Suc_eq_0_disj pflat_len_simps)
248 b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	88	done
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	89
265 d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	90	lemma pflat_len_outside:
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	91	assumes "p \<notin> Pos v1"
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	92	shows "pflat_len v1 p = -1 "
267 32b222d77fa0 updated Christian Urban <urbanc@in.tum.de> parents: 266 diff changeset	93	using assms by (simp add: pflat_len_def)
32b222d77fa0 updated Christian Urban <urbanc@in.tum.de> parents: 266 diff changeset	94
252 022b80503766 polished Christian Urban <urbanc@in.tum.de> parents: 251 diff changeset	95
022b80503766 polished Christian Urban <urbanc@in.tum.de> parents: 251 diff changeset	96
022b80503766 polished Christian Urban <urbanc@in.tum.de> parents: 251 diff changeset	97	section {* Orderings *}
022b80503766 polished Christian Urban <urbanc@in.tum.de> parents: 251 diff changeset	98
022b80503766 polished Christian Urban <urbanc@in.tum.de> parents: 251 diff changeset	99
257 9deaff82e0c5 updated Christian Urban <urbanc@in.tum.de> parents: 256 diff changeset	100	definition prefix_list:: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" ("_ \<sqsubseteq>pre _" [60,59] 60)
248 b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	101	where
252 022b80503766 polished Christian Urban <urbanc@in.tum.de> parents: 251 diff changeset	102	"ps1 \<sqsubseteq>pre ps2 \<equiv> \<exists>ps'. ps1 @ps' = ps2"
248 b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	103
257 9deaff82e0c5 updated Christian Urban <urbanc@in.tum.de> parents: 256 diff changeset	104	definition sprefix_list:: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" ("_ \<sqsubset>spre _" [60,59] 60)
248 b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	105	where
252 022b80503766 polished Christian Urban <urbanc@in.tum.de> parents: 251 diff changeset	106	"ps1 \<sqsubset>spre ps2 \<equiv> ps1 \<sqsubseteq>pre ps2 \<and> ps1 \<noteq> ps2"
248 b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	107
257 9deaff82e0c5 updated Christian Urban <urbanc@in.tum.de> parents: 256 diff changeset	108	inductive lex_list :: "nat list \<Rightarrow> nat list \<Rightarrow> bool" ("_ \<sqsubset>lex _" [60,59] 60)
248 b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	109	where
252 022b80503766 polished Christian Urban <urbanc@in.tum.de> parents: 251 diff changeset	110	"[] \<sqsubset>lex (p#ps)"
248 b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	111	\| "ps1 \<sqsubset>lex ps2 \<Longrightarrow> (p#ps1) \<sqsubset>lex (p#ps2)"
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	112	\| "p1 < p2 \<Longrightarrow> (p1#ps1) \<sqsubset>lex (p2#ps2)"
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	113
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	114	lemma lex_irrfl:
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	115	fixes ps1 ps2 :: "nat list"
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	116	assumes "ps1 \<sqsubset>lex ps2"
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	117	shows "ps1 \<noteq> ps2"
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	118	using assms
257 9deaff82e0c5 updated Christian Urban <urbanc@in.tum.de> parents: 256 diff changeset	119	by(induct rule: lex_list.induct)(auto)
9deaff82e0c5 updated Christian Urban <urbanc@in.tum.de> parents: 256 diff changeset	120
251 925232418a15 polished Christian Urban <urbanc@in.tum.de> parents: 250 diff changeset	121	lemma lex_simps [simp]:
248 b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	122	fixes xs ys :: "nat list"
251 925232418a15 polished Christian Urban <urbanc@in.tum.de> parents: 250 diff changeset	123	shows "[] \<sqsubset>lex ys \<longleftrightarrow> ys \<noteq> []"
925232418a15 polished Christian Urban <urbanc@in.tum.de> parents: 250 diff changeset	124	and "xs \<sqsubset>lex [] \<longleftrightarrow> False"
265 d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	125	and "(x # xs) \<sqsubset>lex (y # ys) \<longleftrightarrow> (x < y \<or> (x = y \<and> xs \<sqsubset>lex ys))"
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	126	by (auto simp add: neq_Nil_conv elim: lex_list.cases intro: lex_list.intros)
248 b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	127
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	128	lemma lex_trans:
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	129	fixes ps1 ps2 ps3 :: "nat list"
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	130	assumes "ps1 \<sqsubset>lex ps2" "ps2 \<sqsubset>lex ps3"
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	131	shows "ps1 \<sqsubset>lex ps3"
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	132	using assms
264 e2828c4a1e23 updated Christian Urban <urbanc@in.tum.de> parents: 263 diff changeset	133	by (induct arbitrary: ps3 rule: lex_list.induct)
e2828c4a1e23 updated Christian Urban <urbanc@in.tum.de> parents: 263 diff changeset	134	(auto elim: lex_list.cases)
e2828c4a1e23 updated Christian Urban <urbanc@in.tum.de> parents: 263 diff changeset	135
248 b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	136
257 9deaff82e0c5 updated Christian Urban <urbanc@in.tum.de> parents: 256 diff changeset	137	lemma lex_trichotomous:
248 b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	138	fixes p q :: "nat list"
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	139	shows "p = q \<or> p \<sqsubset>lex q \<or> q \<sqsubset>lex p"
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	140	apply(induct p arbitrary: q)
265 d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	141	apply(auto elim: lex_list.cases)
248 b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	142	apply(case_tac q)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	143	apply(auto)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	144	done
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	145
254 7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	146
7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	147
7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	148
265 d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	149	section {* POSIX Ordering of Values According to Okui & Suzuki *}
254 7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	150
248 b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	151
261 247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	152	definition PosOrd:: "val \<Rightarrow> nat list \<Rightarrow> val \<Rightarrow> bool" ("_ \<sqsubset>val _ _" [60, 60, 59] 60)
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	153	where
264 e2828c4a1e23 updated Christian Urban <urbanc@in.tum.de> parents: 263 diff changeset	154	"v1 \<sqsubset>val p v2 \<equiv> pflat_len v1 p > pflat_len v2 p \<and>
e2828c4a1e23 updated Christian Urban <urbanc@in.tum.de> parents: 263 diff changeset	155	(\<forall>q \<in> Pos v1 \<union> Pos v2. q \<sqsubset>lex p \<longrightarrow> pflat_len v1 q = pflat_len v2 q)"
e2828c4a1e23 updated Christian Urban <urbanc@in.tum.de> parents: 263 diff changeset	156
265 d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	157
261 247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	158
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	159	definition PosOrd_ex:: "val \<Rightarrow> val \<Rightarrow> bool" ("_ :\<sqsubset>val _" [60, 59] 60)
248 b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	160	where
265 d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	161	"v1 :\<sqsubset>val v2 \<equiv> \<exists>p. v1 \<sqsubset>val p v2"
248 b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	162
265 d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	163	definition PosOrd_ex_eq:: "val \<Rightarrow> val \<Rightarrow> bool" ("_ :\<sqsubseteq>val _" [60, 59] 60)
248 b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	164	where
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	165	"v1 :\<sqsubseteq>val v2 \<equiv> v1 :\<sqsubset>val v2 \<or> v1 = v2"
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	166
265 d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	167
261 247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	168	lemma PosOrd_shorterE:
255 222ed43892ea updated Christian Urban <urbanc@in.tum.de> parents: 254 diff changeset	169	assumes "v1 :\<sqsubset>val v2"
222ed43892ea updated Christian Urban <urbanc@in.tum.de> parents: 254 diff changeset	170	shows "length (flat v2) \<le> length (flat v1)"
267 32b222d77fa0 updated Christian Urban <urbanc@in.tum.de> parents: 266 diff changeset	171	using assms unfolding PosOrd_ex_def PosOrd_def
32b222d77fa0 updated Christian Urban <urbanc@in.tum.de> parents: 266 diff changeset	172	apply(auto simp add: pflat_len_def intlen_int split: if_splits)
32b222d77fa0 updated Christian Urban <urbanc@in.tum.de> parents: 266 diff changeset	173	apply (metis Pos_empty Un_iff at.simps(1) eq_iff lex_simps(1) nat_less_le)
32b222d77fa0 updated Christian Urban <urbanc@in.tum.de> parents: 266 diff changeset	174	by (metis Pos_empty UnI2 at.simps(1) lex_simps(2) lex_trichotomous linear)
255 222ed43892ea updated Christian Urban <urbanc@in.tum.de> parents: 254 diff changeset	175
261 247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	176	lemma PosOrd_shorterI:
265 d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	177	assumes "length (flat v2) < length (flat v1)"
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	178	shows "v1 :\<sqsubset>val v2"
251 925232418a15 polished Christian Urban <urbanc@in.tum.de> parents: 250 diff changeset	179	using assms
261 247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	180	unfolding PosOrd_ex_def
264 e2828c4a1e23 updated Christian Urban <urbanc@in.tum.de> parents: 263 diff changeset	181	by (metis intlen_length lex_simps(2) pflat_len_simps(9) PosOrd_def)
248 b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	182
261 247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	183	lemma PosOrd_spreI:
265 d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	184	assumes "flat v' \<sqsubset>spre flat v"
248 b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	185	shows "v :\<sqsubset>val v'"
251 925232418a15 polished Christian Urban <urbanc@in.tum.de> parents: 250 diff changeset	186	using assms
261 247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	187	apply(rule_tac PosOrd_shorterI)
251 925232418a15 polished Christian Urban <urbanc@in.tum.de> parents: 250 diff changeset	188	by (metis append_eq_conv_conj le_less_linear prefix_list_def sprefix_list_def take_all)
248 b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	189
265 d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	190
261 247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	191	lemma PosOrd_Left_Right:
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	192	assumes "flat v1 = flat v2"
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	193	shows "Left v1 :\<sqsubset>val Right v2"
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	194	unfolding PosOrd_ex_def
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	195	apply(rule_tac x="[0]" in exI)
265 d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	196	using assms
267 32b222d77fa0 updated Christian Urban <urbanc@in.tum.de> parents: 266 diff changeset	197	apply(auto simp add: PosOrd_def pflat_len_simps intlen_int)
261 247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	198	done
256 146b4817aebd updated Christian Urban <urbanc@in.tum.de> parents: 255 diff changeset	199
265 d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	200	lemma PosOrd_Left_eq:
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	201	assumes "flat v = flat v'"
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	202	shows "Left v :\<sqsubset>val Left v' \<longleftrightarrow> v :\<sqsubset>val v'"
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	203	using assms
261 247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	204	unfolding PosOrd_ex_def
251 925232418a15 polished Christian Urban <urbanc@in.tum.de> parents: 250 diff changeset	205	apply(auto)
265 d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	206	apply(case_tac p)
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	207	apply(simp add: PosOrd_def pflat_len_simps)
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	208	apply(case_tac a)
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	209	apply(simp add: PosOrd_def pflat_len_simps)
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	210	apply(rule_tac x="list" in exI)
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	211	apply(auto simp add: PosOrd_def pflat_len_simps)[1]
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	212	apply (smt Un_def lex_list.intros(2) mem_Collect_eq pflat_len_simps(3))
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	213	apply (smt Collect_disj_eq lex_list.intros(2) mem_Collect_eq pflat_len_simps(3))
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	214	apply(auto simp add: PosOrd_def pflat_len_outside)[1]
251 925232418a15 polished Christian Urban <urbanc@in.tum.de> parents: 250 diff changeset	215	apply(rule_tac x="0#p" in exI)
261 247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	216	apply(auto simp add: PosOrd_def pflat_len_simps)
248 b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	217	done
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	218
265 d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	219
261 247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	220	lemma PosOrd_RightI:
251 925232418a15 polished Christian Urban <urbanc@in.tum.de> parents: 250 diff changeset	221	assumes "v :\<sqsubset>val v'" "flat v = flat v'"
925232418a15 polished Christian Urban <urbanc@in.tum.de> parents: 250 diff changeset	222	shows "(Right v) :\<sqsubset>val (Right v')"
248 b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	223	using assms(1)
261 247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	224	unfolding PosOrd_ex_def
251 925232418a15 polished Christian Urban <urbanc@in.tum.de> parents: 250 diff changeset	225	apply(auto)
925232418a15 polished Christian Urban <urbanc@in.tum.de> parents: 250 diff changeset	226	apply(rule_tac x="Suc 0#p" in exI)
248 b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	227	using assms(2)
261 247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	228	apply(auto simp add: PosOrd_def pflat_len_simps)
248 b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	229	done
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	230
261 247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	231	lemma PosOrd_RightE:
252 022b80503766 polished Christian Urban <urbanc@in.tum.de> parents: 251 diff changeset	232	assumes "(Right v1) :\<sqsubset>val (Right v2)"
022b80503766 polished Christian Urban <urbanc@in.tum.de> parents: 251 diff changeset	233	shows "v1 :\<sqsubset>val v2"
022b80503766 polished Christian Urban <urbanc@in.tum.de> parents: 251 diff changeset	234	using assms
261 247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	235	apply(simp add: PosOrd_ex_def)
252 022b80503766 polished Christian Urban <urbanc@in.tum.de> parents: 251 diff changeset	236	apply(erule exE)
264 e2828c4a1e23 updated Christian Urban <urbanc@in.tum.de> parents: 263 diff changeset	237	apply(case_tac p)
261 247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	238	apply(simp add: PosOrd_def)
248 b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	239	apply(auto simp add: pflat_len_simps)
252 022b80503766 polished Christian Urban <urbanc@in.tum.de> parents: 251 diff changeset	240	apply(rule_tac x="[]" in exI)
022b80503766 polished Christian Urban <urbanc@in.tum.de> parents: 251 diff changeset	241	apply(simp add: Pos_empty pflat_len_simps)
264 e2828c4a1e23 updated Christian Urban <urbanc@in.tum.de> parents: 263 diff changeset	242	apply(case_tac a)
e2828c4a1e23 updated Christian Urban <urbanc@in.tum.de> parents: 263 diff changeset	243	apply(simp add: pflat_len_def PosOrd_def)
e2828c4a1e23 updated Christian Urban <urbanc@in.tum.de> parents: 263 diff changeset	244	apply(case_tac nat)
e2828c4a1e23 updated Christian Urban <urbanc@in.tum.de> parents: 263 diff changeset	245	prefer 2
e2828c4a1e23 updated Christian Urban <urbanc@in.tum.de> parents: 263 diff changeset	246	apply(simp add: pflat_len_def PosOrd_def)
261 247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	247	apply(auto simp add: pflat_len_simps PosOrd_def)
264 e2828c4a1e23 updated Christian Urban <urbanc@in.tum.de> parents: 263 diff changeset	248	apply(rule_tac x="list" in exI)
252 022b80503766 polished Christian Urban <urbanc@in.tum.de> parents: 251 diff changeset	249	apply(auto)
022b80503766 polished Christian Urban <urbanc@in.tum.de> parents: 251 diff changeset	250	apply(drule_tac x="Suc 0#q" in bspec)
022b80503766 polished Christian Urban <urbanc@in.tum.de> parents: 251 diff changeset	251	apply(simp)
022b80503766 polished Christian Urban <urbanc@in.tum.de> parents: 251 diff changeset	252	apply(simp add: pflat_len_simps)
022b80503766 polished Christian Urban <urbanc@in.tum.de> parents: 251 diff changeset	253	apply(drule_tac x="Suc 0#q" in bspec)
022b80503766 polished Christian Urban <urbanc@in.tum.de> parents: 251 diff changeset	254	apply(simp)
022b80503766 polished Christian Urban <urbanc@in.tum.de> parents: 251 diff changeset	255	apply(simp add: pflat_len_simps)
022b80503766 polished Christian Urban <urbanc@in.tum.de> parents: 251 diff changeset	256	done
022b80503766 polished Christian Urban <urbanc@in.tum.de> parents: 251 diff changeset	257
248 b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	258
261 247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	259	lemma PosOrd_SeqI1:
252 022b80503766 polished Christian Urban <urbanc@in.tum.de> parents: 251 diff changeset	260	assumes "v1 :\<sqsubset>val v1'" "flat (Seq v1 v2) = flat (Seq v1' v2')"
022b80503766 polished Christian Urban <urbanc@in.tum.de> parents: 251 diff changeset	261	shows "(Seq v1 v2) :\<sqsubset>val (Seq v1' v2')"
248 b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	262	using assms(1)
261 247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	263	apply(subst (asm) PosOrd_ex_def)
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	264	apply(subst (asm) PosOrd_def)
252 022b80503766 polished Christian Urban <urbanc@in.tum.de> parents: 251 diff changeset	265	apply(clarify)
261 247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	266	apply(subst PosOrd_ex_def)
252 022b80503766 polished Christian Urban <urbanc@in.tum.de> parents: 251 diff changeset	267	apply(rule_tac x="0#p" in exI)
261 247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	268	apply(subst PosOrd_def)
248 b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	269	apply(rule conjI)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	270	apply(simp add: pflat_len_simps)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	271	apply(rule ballI)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	272	apply(rule impI)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	273	apply(simp only: Pos.simps)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	274	apply(auto)[1]
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	275	apply(simp add: pflat_len_simps)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	276	using assms(2)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	277	apply(simp)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	278	apply(auto simp add: pflat_len_simps)[2]
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	279	done
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	280
261 247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	281	lemma PosOrd_SeqI2:
252 022b80503766 polished Christian Urban <urbanc@in.tum.de> parents: 251 diff changeset	282	assumes "v2 :\<sqsubset>val v2'" "flat v2 = flat v2'"
022b80503766 polished Christian Urban <urbanc@in.tum.de> parents: 251 diff changeset	283	shows "(Seq v v2) :\<sqsubset>val (Seq v v2')"
248 b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	284	using assms(1)
261 247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	285	apply(subst (asm) PosOrd_ex_def)
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	286	apply(subst (asm) PosOrd_def)
252 022b80503766 polished Christian Urban <urbanc@in.tum.de> parents: 251 diff changeset	287	apply(clarify)
261 247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	288	apply(subst PosOrd_ex_def)
252 022b80503766 polished Christian Urban <urbanc@in.tum.de> parents: 251 diff changeset	289	apply(rule_tac x="Suc 0#p" in exI)
261 247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	290	apply(subst PosOrd_def)
248 b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	291	apply(rule conjI)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	292	apply(simp add: pflat_len_simps)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	293	apply(rule ballI)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	294	apply(rule impI)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	295	apply(simp only: Pos.simps)
252 022b80503766 polished Christian Urban <urbanc@in.tum.de> parents: 251 diff changeset	296	apply(auto)[1]
022b80503766 polished Christian Urban <urbanc@in.tum.de> parents: 251 diff changeset	297	apply(simp add: pflat_len_simps)
022b80503766 polished Christian Urban <urbanc@in.tum.de> parents: 251 diff changeset	298	using assms(2)
022b80503766 polished Christian Urban <urbanc@in.tum.de> parents: 251 diff changeset	299	apply(simp)
022b80503766 polished Christian Urban <urbanc@in.tum.de> parents: 251 diff changeset	300	apply(auto simp add: pflat_len_simps)
248 b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	301	done
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	302
261 247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	303	lemma PosOrd_SeqE:
254 7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	304	assumes "(Seq v1 v2) :\<sqsubset>val (Seq v1' v2')"
7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	305	shows "v1 :\<sqsubset>val v1' \<or> v2 :\<sqsubset>val v2'"
7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	306	using assms
261 247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	307	apply(simp add: PosOrd_ex_def)
254 7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	308	apply(erule exE)
7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	309	apply(case_tac p)
261 247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	310	apply(simp add: PosOrd_def)
254 7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	311	apply(auto simp add: pflat_len_simps intlen_append)[1]
7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	312	apply(rule_tac x="[]" in exI)
7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	313	apply(drule_tac x="[]" in spec)
7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	314	apply(simp add: Pos_empty pflat_len_simps)
7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	315	apply(case_tac a)
7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	316	apply(rule disjI1)
261 247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	317	apply(simp add: PosOrd_def)
254 7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	318	apply(auto simp add: pflat_len_simps intlen_append)[1]
7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	319	apply(rule_tac x="list" in exI)
7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	320	apply(simp)
7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	321	apply(rule ballI)
7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	322	apply(rule impI)
248 b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	323	apply(drule_tac x="0#q" in bspec)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	324	apply(simp)
254 7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	325	apply(simp add: pflat_len_simps)
7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	326	apply(case_tac nat)
7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	327	apply(rule disjI2)
261 247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	328	apply(simp add: PosOrd_def)
254 7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	329	apply(auto simp add: pflat_len_simps intlen_append)
7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	330	apply(rule_tac x="list" in exI)
7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	331	apply(simp add: Pos_empty)
7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	332	apply(rule ballI)
7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	333	apply(rule impI)
264 e2828c4a1e23 updated Christian Urban <urbanc@in.tum.de> parents: 263 diff changeset	334	apply(auto)[1]
254 7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	335	apply(drule_tac x="Suc 0#q" in bspec)
248 b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	336	apply(simp)
254 7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	337	apply(simp add: pflat_len_simps)
264 e2828c4a1e23 updated Christian Urban <urbanc@in.tum.de> parents: 263 diff changeset	338	apply(drule_tac x="Suc 0#q" in bspec)
e2828c4a1e23 updated Christian Urban <urbanc@in.tum.de> parents: 263 diff changeset	339	apply(simp)
e2828c4a1e23 updated Christian Urban <urbanc@in.tum.de> parents: 263 diff changeset	340	apply(simp add: pflat_len_simps)
e2828c4a1e23 updated Christian Urban <urbanc@in.tum.de> parents: 263 diff changeset	341	apply(simp add: PosOrd_def pflat_len_def)
248 b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	342	done
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	343
261 247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	344	lemma PosOrd_StarsI:
254 7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	345	assumes "v1 :\<sqsubset>val v2" "flat (Stars (v1#vs1)) = flat (Stars (v2#vs2))"
7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	346	shows "(Stars (v1#vs1)) :\<sqsubset>val (Stars (v2#vs2))"
248 b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	347	using assms(1)
261 247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	348	apply(subst (asm) PosOrd_ex_def)
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	349	apply(subst (asm) PosOrd_def)
254 7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	350	apply(clarify)
261 247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	351	apply(subst PosOrd_ex_def)
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	352	apply(subst PosOrd_def)
254 7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	353	apply(rule_tac x="0#p" in exI)
7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	354	apply(simp add: pflat_len_Stars_simps pflat_len_simps)
7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	355	using assms(2)
7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	356	apply(simp add: pflat_len_simps intlen_append)
7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	357	apply(auto simp add: pflat_len_Stars_simps pflat_len_simps)
248 b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	358	done
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	359
261 247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	360	lemma PosOrd_StarsI2:
254 7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	361	assumes "(Stars vs1) :\<sqsubset>val (Stars vs2)" "flat (Stars vs1) = flat (Stars vs2)"
7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	362	shows "(Stars (v#vs1)) :\<sqsubset>val (Stars (v#vs2))"
248 b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	363	using assms(1)
261 247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	364	apply(subst (asm) PosOrd_ex_def)
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	365	apply(subst (asm) PosOrd_def)
254 7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	366	apply(clarify)
261 247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	367	apply(subst PosOrd_ex_def)
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	368	apply(subst PosOrd_def)
254 7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	369	apply(case_tac p)
7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	370	apply(simp add: pflat_len_simps)
7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	371	apply(rule_tac x="[]" in exI)
7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	372	apply(simp add: pflat_len_Stars_simps pflat_len_simps intlen_append)
7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	373	apply(rule_tac x="Suc a#list" in exI)
7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	374	apply(simp add: pflat_len_Stars_simps pflat_len_simps)
7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	375	using assms(2)
7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	376	apply(simp add: pflat_len_simps intlen_append)
7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	377	apply(auto simp add: pflat_len_Stars_simps pflat_len_simps)
7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	378	done
7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	379
261 247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	380	lemma PosOrd_Stars_appendI:
254 7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	381	assumes "Stars vs1 :\<sqsubset>val Stars vs2" "flat (Stars vs1) = flat (Stars vs2)"
7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	382	shows "Stars (vs @ vs1) :\<sqsubset>val Stars (vs @ vs2)"
7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	383	using assms
7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	384	apply(induct vs)
248 b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	385	apply(simp)
261 247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	386	apply(simp add: PosOrd_StarsI2)
254 7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	387	done
7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	388
261 247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	389	lemma PosOrd_StarsE2:
254 7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	390	assumes "Stars (v # vs1) :\<sqsubset>val Stars (v # vs2)"
7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	391	shows "Stars vs1 :\<sqsubset>val Stars vs2"
7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	392	using assms
261 247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	393	apply(subst (asm) PosOrd_ex_def)
248 b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	394	apply(erule exE)
254 7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	395	apply(case_tac p)
7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	396	apply(simp)
261 247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	397	apply(simp add: PosOrd_def pflat_len_simps intlen_append)
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	398	apply(subst PosOrd_ex_def)
254 7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	399	apply(rule_tac x="[]" in exI)
261 247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	400	apply(simp add: PosOrd_def pflat_len_simps Pos_empty)
254 7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	401	apply(simp)
7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	402	apply(case_tac a)
7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	403	apply(clarify)
264 e2828c4a1e23 updated Christian Urban <urbanc@in.tum.de> parents: 263 diff changeset	404	apply(auto simp add: pflat_len_simps PosOrd_def pflat_len_def split: if_splits)[1]
254 7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	405	apply(clarify)
261 247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	406	apply(simp add: PosOrd_ex_def)
254 7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	407	apply(rule_tac x="nat#list" in exI)
261 247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	408	apply(auto simp add: PosOrd_def pflat_len_simps intlen_append)[1]
254 7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	409	apply(case_tac q)
261 247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	410	apply(simp add: PosOrd_def pflat_len_simps intlen_append)
254 7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	411	apply(clarify)
7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	412	apply(drule_tac x="Suc a # lista" in bspec)
7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	413	apply(simp)
261 247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	414	apply(auto simp add: PosOrd_def pflat_len_simps intlen_append)[1]
254 7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	415	apply(case_tac q)
261 247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	416	apply(simp add: PosOrd_def pflat_len_simps intlen_append)
254 7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	417	apply(clarify)
7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	418	apply(drule_tac x="Suc a # lista" in bspec)
248 b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	419	apply(simp)
261 247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	420	apply(auto simp add: PosOrd_def pflat_len_simps intlen_append)[1]
254 7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	421	done
7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	422
261 247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	423	lemma PosOrd_Stars_appendE:
254 7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	424	assumes "Stars (vs @ vs1) :\<sqsubset>val Stars (vs @ vs2)"
7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	425	shows "Stars vs1 :\<sqsubset>val Stars vs2"
7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	426	using assms
7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	427	apply(induct vs)
7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	428	apply(simp)
261 247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	429	apply(simp add: PosOrd_StarsE2)
254 7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	430	done
7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	431
261 247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	432	lemma PosOrd_Stars_append_eq:
254 7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	433	assumes "flat (Stars vs1) = flat (Stars vs2)"
7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	434	shows "Stars (vs @ vs1) :\<sqsubset>val Stars (vs @ vs2) \<longleftrightarrow> Stars vs1 :\<sqsubset>val Stars vs2"
7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	435	using assms
7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	436	apply(rule_tac iffI)
261 247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	437	apply(erule PosOrd_Stars_appendE)
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	438	apply(rule PosOrd_Stars_appendI)
254 7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	439	apply(auto)
248 b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	440	done
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	441
261 247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	442	lemma PosOrd_trans:
248 b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	443	assumes "v1 :\<sqsubset>val v2" "v2 :\<sqsubset>val v3"
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	444	shows "v1 :\<sqsubset>val v3"
264 e2828c4a1e23 updated Christian Urban <urbanc@in.tum.de> parents: 263 diff changeset	445	proof -
e2828c4a1e23 updated Christian Urban <urbanc@in.tum.de> parents: 263 diff changeset	446	from assms obtain p p'
e2828c4a1e23 updated Christian Urban <urbanc@in.tum.de> parents: 263 diff changeset	447	where as: "v1 \<sqsubset>val p v2" "v2 \<sqsubset>val p' v3" unfolding PosOrd_ex_def by blast
e2828c4a1e23 updated Christian Urban <urbanc@in.tum.de> parents: 263 diff changeset	448	have "p = p' \<or> p \<sqsubset>lex p' \<or> p' \<sqsubset>lex p"
e2828c4a1e23 updated Christian Urban <urbanc@in.tum.de> parents: 263 diff changeset	449	by (rule lex_trichotomous)
e2828c4a1e23 updated Christian Urban <urbanc@in.tum.de> parents: 263 diff changeset	450	moreover
e2828c4a1e23 updated Christian Urban <urbanc@in.tum.de> parents: 263 diff changeset	451	{ assume "p = p'"
265 d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	452	with as have "v1 \<sqsubset>val p v3" unfolding PosOrd_def pflat_len_def
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	453	by fastforce
264 e2828c4a1e23 updated Christian Urban <urbanc@in.tum.de> parents: 263 diff changeset	454	then have " v1 :\<sqsubset>val v3" unfolding PosOrd_ex_def by blast
e2828c4a1e23 updated Christian Urban <urbanc@in.tum.de> parents: 263 diff changeset	455	}
e2828c4a1e23 updated Christian Urban <urbanc@in.tum.de> parents: 263 diff changeset	456	moreover
e2828c4a1e23 updated Christian Urban <urbanc@in.tum.de> parents: 263 diff changeset	457	{ assume "p \<sqsubset>lex p'"
265 d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	458	with as have "v1 \<sqsubset>val p v3" unfolding PosOrd_def pflat_len_def
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	459	by (smt Un_iff lex_trans)
264 e2828c4a1e23 updated Christian Urban <urbanc@in.tum.de> parents: 263 diff changeset	460	then have " v1 :\<sqsubset>val v3" unfolding PosOrd_ex_def by blast
e2828c4a1e23 updated Christian Urban <urbanc@in.tum.de> parents: 263 diff changeset	461	}
e2828c4a1e23 updated Christian Urban <urbanc@in.tum.de> parents: 263 diff changeset	462	moreover
e2828c4a1e23 updated Christian Urban <urbanc@in.tum.de> parents: 263 diff changeset	463	{ assume "p' \<sqsubset>lex p"
e2828c4a1e23 updated Christian Urban <urbanc@in.tum.de> parents: 263 diff changeset	464	with as have "v1 \<sqsubset>val p' v3" unfolding PosOrd_def
e2828c4a1e23 updated Christian Urban <urbanc@in.tum.de> parents: 263 diff changeset	465	by (smt Un_iff intlen_bigger lex_trans pflat_len_def)
e2828c4a1e23 updated Christian Urban <urbanc@in.tum.de> parents: 263 diff changeset	466	then have "v1 :\<sqsubset>val v3" unfolding PosOrd_ex_def by blast
e2828c4a1e23 updated Christian Urban <urbanc@in.tum.de> parents: 263 diff changeset	467	}
e2828c4a1e23 updated Christian Urban <urbanc@in.tum.de> parents: 263 diff changeset	468	ultimately show "v1 :\<sqsubset>val v3" by blast
e2828c4a1e23 updated Christian Urban <urbanc@in.tum.de> parents: 263 diff changeset	469	qed
e2828c4a1e23 updated Christian Urban <urbanc@in.tum.de> parents: 263 diff changeset	470
254 7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	471
261 247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	472	lemma PosOrd_irrefl:
256 146b4817aebd updated Christian Urban <urbanc@in.tum.de> parents: 255 diff changeset	473	assumes "v :\<sqsubset>val v"
146b4817aebd updated Christian Urban <urbanc@in.tum.de> parents: 255 diff changeset	474	shows "False"
264 e2828c4a1e23 updated Christian Urban <urbanc@in.tum.de> parents: 263 diff changeset	475	using assms unfolding PosOrd_ex_def PosOrd_def
e2828c4a1e23 updated Christian Urban <urbanc@in.tum.de> parents: 263 diff changeset	476	by auto
256 146b4817aebd updated Christian Urban <urbanc@in.tum.de> parents: 255 diff changeset	477
261 247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	478	lemma PosOrd_almost_trichotomous:
256 146b4817aebd updated Christian Urban <urbanc@in.tum.de> parents: 255 diff changeset	479	shows "v1 :\<sqsubset>val v2 \<or> v2 :\<sqsubset>val v1 \<or> (intlen (flat v1) = intlen (flat v2))"
261 247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	480	apply(auto simp add: PosOrd_ex_def)
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	481	apply(auto simp add: PosOrd_def)
256 146b4817aebd updated Christian Urban <urbanc@in.tum.de> parents: 255 diff changeset	482	apply(rule_tac x="[]" in exI)
146b4817aebd updated Christian Urban <urbanc@in.tum.de> parents: 255 diff changeset	483	apply(auto simp add: Pos_empty pflat_len_simps)
146b4817aebd updated Christian Urban <urbanc@in.tum.de> parents: 255 diff changeset	484	apply(drule_tac x="[]" in spec)
146b4817aebd updated Christian Urban <urbanc@in.tum.de> parents: 255 diff changeset	485	apply(auto simp add: Pos_empty pflat_len_simps)
146b4817aebd updated Christian Urban <urbanc@in.tum.de> parents: 255 diff changeset	486	done
146b4817aebd updated Christian Urban <urbanc@in.tum.de> parents: 255 diff changeset	487
146b4817aebd updated Christian Urban <urbanc@in.tum.de> parents: 255 diff changeset	488	lemma WW1:
146b4817aebd updated Christian Urban <urbanc@in.tum.de> parents: 255 diff changeset	489	assumes "v1 :\<sqsubset>val v2" "v2 :\<sqsubset>val v1"
146b4817aebd updated Christian Urban <urbanc@in.tum.de> parents: 255 diff changeset	490	shows "False"
146b4817aebd updated Christian Urban <urbanc@in.tum.de> parents: 255 diff changeset	491	using assms
261 247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	492	apply(auto simp add: PosOrd_ex_def PosOrd_def)
264 e2828c4a1e23 updated Christian Urban <urbanc@in.tum.de> parents: 263 diff changeset	493	using assms PosOrd_irrefl PosOrd_trans by blast
256 146b4817aebd updated Christian Urban <urbanc@in.tum.de> parents: 255 diff changeset	494
261 247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	495	lemma PosOrd_SeqE2:
265 d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	496	assumes "(Seq v1 v2) :\<sqsubset>val (Seq v1' v2')" "flat (Seq v1 v2) = flat (Seq v1' v2')"
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	497	shows "v1 :\<sqsubset>val v1' \<or> (intlen (flat v1) = intlen (flat v1') \<and> v2 :\<sqsubset>val v2')"
256 146b4817aebd updated Christian Urban <urbanc@in.tum.de> parents: 255 diff changeset	498	using assms
261 247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	499	apply(frule_tac PosOrd_SeqE)
256 146b4817aebd updated Christian Urban <urbanc@in.tum.de> parents: 255 diff changeset	500	apply(erule disjE)
146b4817aebd updated Christian Urban <urbanc@in.tum.de> parents: 255 diff changeset	501	apply(simp)
146b4817aebd updated Christian Urban <urbanc@in.tum.de> parents: 255 diff changeset	502	apply(case_tac "v1 :\<sqsubset>val v1'")
146b4817aebd updated Christian Urban <urbanc@in.tum.de> parents: 255 diff changeset	503	apply(simp)
265 d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	504	apply(rule disjI2)
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	505	apply(rule conjI)
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	506	prefer 2
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	507	apply(simp)
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	508	apply(auto)
261 247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	509	apply(auto simp add: PosOrd_ex_def)
265 d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	510	apply(auto simp add: PosOrd_def pflat_len_simps)
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	511	apply(case_tac p)
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	512	apply(auto simp add: PosOrd_def pflat_len_simps)
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	513	apply(case_tac a)
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	514	apply(auto simp add: PosOrd_def pflat_len_simps)
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	515	apply (metis PosOrd_SeqI1 PosOrd_almost_trichotomous PosOrd_def PosOrd_ex_def WW1 assms(1) assms(2))
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	516	by (metis PosOrd_SeqI1 PosOrd_almost_trichotomous PosOrd_def PosOrd_ex_def WW1 assms(1) assms(2))
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	517
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	518	lemma PosOrd_SeqE4:
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	519	assumes "(Seq v1 v2) :\<sqsubset>val (Seq v1' v2')" "flat (Seq v1 v2) = flat (Seq v1' v2')"
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	520	shows "v1 :\<sqsubset>val v1' \<or> (flat v1 = flat v1' \<and> v2 :\<sqsubset>val v2')"
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	521	using assms
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	522	apply(frule_tac PosOrd_SeqE)
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	523	apply(erule disjE)
256 146b4817aebd updated Christian Urban <urbanc@in.tum.de> parents: 255 diff changeset	524	apply(simp)
265 d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	525	apply(case_tac "v1 :\<sqsubset>val v1'")
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	526	apply(simp)
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	527	apply(rule disjI2)
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	528	apply(rule conjI)
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	529	prefer 2
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	530	apply(simp)
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	531	apply(auto)
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	532	apply(case_tac "length (flat v1') < length (flat v1)")
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	533	using PosOrd_shorterI apply blast
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	534	by (metis PosOrd_SeqI1 PosOrd_shorterI WW1 antisym_conv3 append_eq_append_conv assms(2))
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	535
254 7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	536
267 32b222d77fa0 updated Christian Urban <urbanc@in.tum.de> parents: 266 diff changeset	537
261 247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	538	section {* The Posix Value is smaller than any other Value *}
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	539
262 45ad887fa6aa isar proofs Christian Urban <urbanc@in.tum.de> parents: 261 diff changeset	540
261 247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	541	lemma Posix_PosOrd:
267 32b222d77fa0 updated Christian Urban <urbanc@in.tum.de> parents: 266 diff changeset	542	assumes "s \<in> r \<rightarrow> v1" "v2 \<in> CV r s"
248 b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	543	shows "v1 :\<sqsubseteq>val v2"
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	544	using assms
261 247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	545	proof (induct arbitrary: v2 rule: Posix.induct)
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	546	case (Posix_ONE v)
267 32b222d77fa0 updated Christian Urban <urbanc@in.tum.de> parents: 266 diff changeset	547	have "v \<in> CV ONE []" by fact
262 45ad887fa6aa isar proofs Christian Urban <urbanc@in.tum.de> parents: 261 diff changeset	548	then have "v = Void"
267 32b222d77fa0 updated Christian Urban <urbanc@in.tum.de> parents: 266 diff changeset	549	by (simp add: CV_simps)
261 247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	550	then show "Void :\<sqsubseteq>val v"
265 d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	551	by (simp add: PosOrd_ex_eq_def)
261 247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	552	next
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	553	case (Posix_CHAR c v)
267 32b222d77fa0 updated Christian Urban <urbanc@in.tum.de> parents: 266 diff changeset	554	have "v \<in> CV (CHAR c) [c]" by fact
262 45ad887fa6aa isar proofs Christian Urban <urbanc@in.tum.de> parents: 261 diff changeset	555	then have "v = Char c"
267 32b222d77fa0 updated Christian Urban <urbanc@in.tum.de> parents: 266 diff changeset	556	by (simp add: CV_simps)
261 247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	557	then show "Char c :\<sqsubseteq>val v"
265 d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	558	by (simp add: PosOrd_ex_eq_def)
261 247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	559	next
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	560	case (Posix_ALT1 s r1 v r2 v2)
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	561	have as1: "s \<in> r1 \<rightarrow> v" by fact
267 32b222d77fa0 updated Christian Urban <urbanc@in.tum.de> parents: 266 diff changeset	562	have IH: "\<And>v2. v2 \<in> CV r1 s \<Longrightarrow> v :\<sqsubseteq>val v2" by fact
32b222d77fa0 updated Christian Urban <urbanc@in.tum.de> parents: 266 diff changeset	563	have "v2 \<in> CV (ALT r1 r2) s" by fact
262 45ad887fa6aa isar proofs Christian Urban <urbanc@in.tum.de> parents: 261 diff changeset	564	then have "\<Turnstile> v2 : ALT r1 r2" "flat v2 = s"
267 32b222d77fa0 updated Christian Urban <urbanc@in.tum.de> parents: 266 diff changeset	565	by(auto simp add: CV_def prefix_list_def)
261 247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	566	then consider
262 45ad887fa6aa isar proofs Christian Urban <urbanc@in.tum.de> parents: 261 diff changeset	567	(Left) v3 where "v2 = Left v3" "\<Turnstile> v3 : r1" "flat v3 = s"
45ad887fa6aa isar proofs Christian Urban <urbanc@in.tum.de> parents: 261 diff changeset	568	\| (Right) v3 where "v2 = Right v3" "\<Turnstile> v3 : r2" "flat v3 = s"
261 247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	569	by (auto elim: CPrf.cases)
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	570	then show "Left v :\<sqsubseteq>val v2"
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	571	proof(cases)
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	572	case (Left v3)
267 32b222d77fa0 updated Christian Urban <urbanc@in.tum.de> parents: 266 diff changeset	573	have "v3 \<in> CV r1 s" using Left(2,3)
32b222d77fa0 updated Christian Urban <urbanc@in.tum.de> parents: 266 diff changeset	574	by (auto simp add: CV_def prefix_list_def)
261 247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	575	with IH have "v :\<sqsubseteq>val v3" by simp
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	576	moreover
262 45ad887fa6aa isar proofs Christian Urban <urbanc@in.tum.de> parents: 261 diff changeset	577	have "flat v3 = flat v" using as1 Left(3)
45ad887fa6aa isar proofs Christian Urban <urbanc@in.tum.de> parents: 261 diff changeset	578	by (simp add: Posix1(2))
261 247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	579	ultimately have "Left v :\<sqsubseteq>val Left v3"
265 d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	580	by (simp add: PosOrd_ex_eq_def PosOrd_Left_eq)
261 247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	581	then show "Left v :\<sqsubseteq>val v2" unfolding Left .
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	582	next
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	583	case (Right v3)
262 45ad887fa6aa isar proofs Christian Urban <urbanc@in.tum.de> parents: 261 diff changeset	584	have "flat v3 = flat v" using as1 Right(3)
45ad887fa6aa isar proofs Christian Urban <urbanc@in.tum.de> parents: 261 diff changeset	585	by (simp add: Posix1(2))
261 247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	586	then have "Left v :\<sqsubseteq>val Right v3" using Right(3) as1
265 d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	587	by (auto simp add: PosOrd_ex_eq_def PosOrd_Left_Right)
261 247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	588	then show "Left v :\<sqsubseteq>val v2" unfolding Right .
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	589	qed
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	590	next
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	591	case (Posix_ALT2 s r2 v r1 v2)
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	592	have as1: "s \<in> r2 \<rightarrow> v" by fact
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	593	have as2: "s \<notin> L r1" by fact
267 32b222d77fa0 updated Christian Urban <urbanc@in.tum.de> parents: 266 diff changeset	594	have IH: "\<And>v2. v2 \<in> CV r2 s \<Longrightarrow> v :\<sqsubseteq>val v2" by fact
32b222d77fa0 updated Christian Urban <urbanc@in.tum.de> parents: 266 diff changeset	595	have "v2 \<in> CV (ALT r1 r2) s" by fact
262 45ad887fa6aa isar proofs Christian Urban <urbanc@in.tum.de> parents: 261 diff changeset	596	then have "\<Turnstile> v2 : ALT r1 r2" "flat v2 = s"
267 32b222d77fa0 updated Christian Urban <urbanc@in.tum.de> parents: 266 diff changeset	597	by(auto simp add: CV_def prefix_list_def)
261 247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	598	then consider
262 45ad887fa6aa isar proofs Christian Urban <urbanc@in.tum.de> parents: 261 diff changeset	599	(Left) v3 where "v2 = Left v3" "\<Turnstile> v3 : r1" "flat v3 = s"
45ad887fa6aa isar proofs Christian Urban <urbanc@in.tum.de> parents: 261 diff changeset	600	\| (Right) v3 where "v2 = Right v3" "\<Turnstile> v3 : r2" "flat v3 = s"
261 247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	601	by (auto elim: CPrf.cases)
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	602	then show "Right v :\<sqsubseteq>val v2"
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	603	proof (cases)
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	604	case (Right v3)
267 32b222d77fa0 updated Christian Urban <urbanc@in.tum.de> parents: 266 diff changeset	605	have "v3 \<in> CV r2 s" using Right(2,3)
32b222d77fa0 updated Christian Urban <urbanc@in.tum.de> parents: 266 diff changeset	606	by (auto simp add: CV_def prefix_list_def)
261 247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	607	with IH have "v :\<sqsubseteq>val v3" by simp
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	608	moreover
262 45ad887fa6aa isar proofs Christian Urban <urbanc@in.tum.de> parents: 261 diff changeset	609	have "flat v3 = flat v" using as1 Right(3)
45ad887fa6aa isar proofs Christian Urban <urbanc@in.tum.de> parents: 261 diff changeset	610	by (simp add: Posix1(2))
261 247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	611	ultimately have "Right v :\<sqsubseteq>val Right v3"
265 d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	612	by (auto simp add: PosOrd_ex_eq_def PosOrd_RightI)
261 247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	613	then show "Right v :\<sqsubseteq>val v2" unfolding Right .
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	614	next
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	615	case (Left v3)
267 32b222d77fa0 updated Christian Urban <urbanc@in.tum.de> parents: 266 diff changeset	616	have "v3 \<in> CV r1 s" using Left(2,3) as2
32b222d77fa0 updated Christian Urban <urbanc@in.tum.de> parents: 266 diff changeset	617	by (auto simp add: CV_def prefix_list_def)
262 45ad887fa6aa isar proofs Christian Urban <urbanc@in.tum.de> parents: 261 diff changeset	618	then have "flat v3 = flat v \<and> \<Turnstile> v3 : r1" using as1 Left(3)
267 32b222d77fa0 updated Christian Urban <urbanc@in.tum.de> parents: 266 diff changeset	619	by (simp add: Posix1(2) CV_def)
262 45ad887fa6aa isar proofs Christian Urban <urbanc@in.tum.de> parents: 261 diff changeset	620	then have "False" using as1 as2 Left
45ad887fa6aa isar proofs Christian Urban <urbanc@in.tum.de> parents: 261 diff changeset	621	by (auto simp add: Posix1(2) L_flat_Prf1 Prf_CPrf)
45ad887fa6aa isar proofs Christian Urban <urbanc@in.tum.de> parents: 261 diff changeset	622	then show "Right v :\<sqsubseteq>val v2" by simp
261 247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	623	qed
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	624	next
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	625	case (Posix_SEQ s1 r1 v1 s2 r2 v2 v3)
264 e2828c4a1e23 updated Christian Urban <urbanc@in.tum.de> parents: 263 diff changeset	626	have "s1 \<in> r1 \<rightarrow> v1" "s2 \<in> r2 \<rightarrow> v2" by fact+
e2828c4a1e23 updated Christian Urban <urbanc@in.tum.de> parents: 263 diff changeset	627	then have as1: "s1 = flat v1" "s2 = flat v2" by (simp_all add: Posix1(2))
267 32b222d77fa0 updated Christian Urban <urbanc@in.tum.de> parents: 266 diff changeset	628	have IH1: "\<And>v3. v3 \<in> CV r1 s1 \<Longrightarrow> v1 :\<sqsubseteq>val v3" by fact
32b222d77fa0 updated Christian Urban <urbanc@in.tum.de> parents: 266 diff changeset	629	have IH2: "\<And>v3. v3 \<in> CV r2 s2 \<Longrightarrow> v2 :\<sqsubseteq>val v3" by fact
261 247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	630	have cond: "\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> s1 @ s\<^sub>3 \<in> L r1 \<and> s\<^sub>4 \<in> L r2)" by fact
267 32b222d77fa0 updated Christian Urban <urbanc@in.tum.de> parents: 266 diff changeset	631	have "v3 \<in> CV (SEQ r1 r2) (s1 @ s2)" by fact
261 247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	632	then obtain v3a v3b where eqs:
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	633	"v3 = Seq v3a v3b" "\<Turnstile> v3a : r1" "\<Turnstile> v3b : r2"
262 45ad887fa6aa isar proofs Christian Urban <urbanc@in.tum.de> parents: 261 diff changeset	634	"flat v3a @ flat v3b = s1 @ s2"
267 32b222d77fa0 updated Christian Urban <urbanc@in.tum.de> parents: 266 diff changeset	635	by (force simp add: prefix_list_def CV_def elim: CPrf.cases)
262 45ad887fa6aa isar proofs Christian Urban <urbanc@in.tum.de> parents: 261 diff changeset	636	with cond have "flat v3a \<sqsubseteq>pre s1" unfolding prefix_list_def
45ad887fa6aa isar proofs Christian Urban <urbanc@in.tum.de> parents: 261 diff changeset	637	by (smt L_flat_Prf1 Prf_CPrf append_eq_append_conv2 append_self_conv)
45ad887fa6aa isar proofs Christian Urban <urbanc@in.tum.de> parents: 261 diff changeset	638	then have "flat v3a \<sqsubset>spre s1 \<or> (flat v3a = s1 \<and> flat v3b = s2)" using eqs
45ad887fa6aa isar proofs Christian Urban <urbanc@in.tum.de> parents: 261 diff changeset	639	by (simp add: sprefix_list_def append_eq_conv_conj)
45ad887fa6aa isar proofs Christian Urban <urbanc@in.tum.de> parents: 261 diff changeset	640	then have q2: "v1 :\<sqsubset>val v3a \<or> (flat v3a = s1 \<and> flat v3b = s2)"
264 e2828c4a1e23 updated Christian Urban <urbanc@in.tum.de> parents: 263 diff changeset	641	using PosOrd_spreI as1(1) eqs by blast
267 32b222d77fa0 updated Christian Urban <urbanc@in.tum.de> parents: 266 diff changeset	642	then have "v1 :\<sqsubset>val v3a \<or> (v3a \<in> CV r1 s1 \<and> v3b \<in> CV r2 s2)" using eqs(2,3)
32b222d77fa0 updated Christian Urban <urbanc@in.tum.de> parents: 266 diff changeset	643	by (auto simp add: CV_def)
262 45ad887fa6aa isar proofs Christian Urban <urbanc@in.tum.de> parents: 261 diff changeset	644	then have "v1 :\<sqsubset>val v3a \<or> (v1 :\<sqsubseteq>val v3a \<and> v2 :\<sqsubseteq>val v3b)" using IH1 IH2 by blast
45ad887fa6aa isar proofs Christian Urban <urbanc@in.tum.de> parents: 261 diff changeset	645	then have "Seq v1 v2 :\<sqsubseteq>val Seq v3a v3b" using eqs q2 as1
265 d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	646	unfolding PosOrd_ex_eq_def by (auto simp add: PosOrd_SeqI1 PosOrd_SeqI2)
262 45ad887fa6aa isar proofs Christian Urban <urbanc@in.tum.de> parents: 261 diff changeset	647	then show "Seq v1 v2 :\<sqsubseteq>val v3" unfolding eqs by blast
261 247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	648	next
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	649	case (Posix_STAR1 s1 r v s2 vs v3)
264 e2828c4a1e23 updated Christian Urban <urbanc@in.tum.de> parents: 263 diff changeset	650	have "s1 \<in> r \<rightarrow> v" "s2 \<in> STAR r \<rightarrow> Stars vs" by fact+
e2828c4a1e23 updated Christian Urban <urbanc@in.tum.de> parents: 263 diff changeset	651	then have as1: "s1 = flat v" "s2 = flat (Stars vs)" by (auto dest: Posix1(2))
267 32b222d77fa0 updated Christian Urban <urbanc@in.tum.de> parents: 266 diff changeset	652	have IH1: "\<And>v3. v3 \<in> CV r s1 \<Longrightarrow> v :\<sqsubseteq>val v3" by fact
32b222d77fa0 updated Christian Urban <urbanc@in.tum.de> parents: 266 diff changeset	653	have IH2: "\<And>v3. v3 \<in> CV (STAR r) s2 \<Longrightarrow> Stars vs :\<sqsubseteq>val v3" by fact
261 247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	654	have cond: "\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> s1 @ s\<^sub>3 \<in> L r \<and> s\<^sub>4 \<in> L (STAR r))" by fact
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	655	have cond2: "flat v \<noteq> []" by fact
267 32b222d77fa0 updated Christian Urban <urbanc@in.tum.de> parents: 266 diff changeset	656	have "v3 \<in> CV (STAR r) (s1 @ s2)" by fact
265 d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	657	then consider
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	658	(NonEmpty) v3a vs3 where "v3 = Stars (v3a # vs3)"
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	659	"\<Turnstile> v3a : r" "\<Turnstile> Stars vs3 : STAR r"
262 45ad887fa6aa isar proofs Christian Urban <urbanc@in.tum.de> parents: 261 diff changeset	660	"flat (Stars (v3a # vs3)) = s1 @ s2"
261 247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	661	\| (Empty) "v3 = Stars []"
267 32b222d77fa0 updated Christian Urban <urbanc@in.tum.de> parents: 266 diff changeset	662	unfolding CV_def
265 d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	663	apply(auto)
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	664	apply(erule CPrf.cases)
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	665	apply(simp_all)
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	666	apply(auto)[1]
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	667	apply(case_tac vs)
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	668	apply(auto)
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	669	using CPrf.intros(6) by blast
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	670	then show "Stars (v # vs) :\<sqsubseteq>val v3" (* HERE *)
261 247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	671	proof (cases)
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	672	case (NonEmpty v3a vs3)
262 45ad887fa6aa isar proofs Christian Urban <urbanc@in.tum.de> parents: 261 diff changeset	673	have "flat (Stars (v3a # vs3)) = s1 @ s2" using NonEmpty(4) .
45ad887fa6aa isar proofs Christian Urban <urbanc@in.tum.de> parents: 261 diff changeset	674	with cond have "flat v3a \<sqsubseteq>pre s1" using NonEmpty(2,3)
45ad887fa6aa isar proofs Christian Urban <urbanc@in.tum.de> parents: 261 diff changeset	675	unfolding prefix_list_def
45ad887fa6aa isar proofs Christian Urban <urbanc@in.tum.de> parents: 261 diff changeset	676	by (smt L_flat_Prf1 Prf_CPrf append_Nil2 append_eq_append_conv2 flat.simps(7))
45ad887fa6aa isar proofs Christian Urban <urbanc@in.tum.de> parents: 261 diff changeset	677	then have "flat v3a \<sqsubset>spre s1 \<or> (flat v3a = s1 \<and> flat (Stars vs3) = s2)" using NonEmpty(4)
45ad887fa6aa isar proofs Christian Urban <urbanc@in.tum.de> parents: 261 diff changeset	678	by (simp add: sprefix_list_def append_eq_conv_conj)
45ad887fa6aa isar proofs Christian Urban <urbanc@in.tum.de> parents: 261 diff changeset	679	then have q2: "v :\<sqsubset>val v3a \<or> (flat v3a = s1 \<and> flat (Stars vs3) = s2)"
264 e2828c4a1e23 updated Christian Urban <urbanc@in.tum.de> parents: 263 diff changeset	680	using PosOrd_spreI as1(1) NonEmpty(4) by blast
267 32b222d77fa0 updated Christian Urban <urbanc@in.tum.de> parents: 266 diff changeset	681	then have "v :\<sqsubset>val v3a \<or> (v3a \<in> CV r s1 \<and> Stars vs3 \<in> CV (STAR r) s2)"
32b222d77fa0 updated Christian Urban <urbanc@in.tum.de> parents: 266 diff changeset	682	using NonEmpty(2,3) by (auto simp add: CV_def)
264 e2828c4a1e23 updated Christian Urban <urbanc@in.tum.de> parents: 263 diff changeset	683	then have "v :\<sqsubset>val v3a \<or> (v :\<sqsubseteq>val v3a \<and> Stars vs :\<sqsubseteq>val Stars vs3)" using IH1 IH2 by blast
e2828c4a1e23 updated Christian Urban <urbanc@in.tum.de> parents: 263 diff changeset	684	then have "v :\<sqsubset>val v3a \<or> (v = v3a \<and> Stars vs :\<sqsubseteq>val Stars vs3)"
265 d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	685	unfolding PosOrd_ex_eq_def by auto
262 45ad887fa6aa isar proofs Christian Urban <urbanc@in.tum.de> parents: 261 diff changeset	686	then have "Stars (v # vs) :\<sqsubseteq>val Stars (v3a # vs3)" using NonEmpty(4) q2 as1
265 d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	687	unfolding PosOrd_ex_eq_def
264 e2828c4a1e23 updated Christian Urban <urbanc@in.tum.de> parents: 263 diff changeset	688	by (metis PosOrd_StarsI PosOrd_StarsI2 flat.simps(7) val.inject(5))
262 45ad887fa6aa isar proofs Christian Urban <urbanc@in.tum.de> parents: 261 diff changeset	689	then show "Stars (v # vs) :\<sqsubseteq>val v3" unfolding NonEmpty by blast
261 247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	690	next
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	691	case Empty
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	692	have "v3 = Stars []" by fact
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	693	then show "Stars (v # vs) :\<sqsubseteq>val v3"
265 d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	694	unfolding PosOrd_ex_eq_def using cond2
261 247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	695	by (simp add: PosOrd_shorterI)
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	696	qed
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	697	next
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	698	case (Posix_STAR2 r v2)
267 32b222d77fa0 updated Christian Urban <urbanc@in.tum.de> parents: 266 diff changeset	699	have "v2 \<in> CV (STAR r) []" by fact
262 45ad887fa6aa isar proofs Christian Urban <urbanc@in.tum.de> parents: 261 diff changeset	700	then have "v2 = Stars []"
267 32b222d77fa0 updated Christian Urban <urbanc@in.tum.de> parents: 266 diff changeset	701	unfolding CV_def by (auto elim: CPrf.cases)
261 247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	702	then show "Stars [] :\<sqsubseteq>val v2"
265 d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	703	by (simp add: PosOrd_ex_eq_def)
261 247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	704	qed
253 ca4e9eb8d576 polished Christian Urban <urbanc@in.tum.de> parents: 252 diff changeset	705
263 00c9a95d492e isar proofs Christian Urban <urbanc@in.tum.de> parents: 262 diff changeset	706
261 247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	707	lemma Posix_PosOrd_reverse:
248 b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	708	assumes "s \<in> r \<rightarrow> v1"
267 32b222d77fa0 updated Christian Urban <urbanc@in.tum.de> parents: 266 diff changeset	709	shows "\<not>(\<exists>v2 \<in> CV r s. v2 :\<sqsubset>val v1)"
248 b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	710	using assms
267 32b222d77fa0 updated Christian Urban <urbanc@in.tum.de> parents: 266 diff changeset	711	by (metis Posix_PosOrd less_irrefl PosOrd_def
265 d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	712	PosOrd_ex_eq_def PosOrd_ex_def PosOrd_trans)
248 b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	713
265 d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	714
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	715
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	716	lemma PosOrd_Posix_Stars:
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	717	assumes "\<forall>v \<in> set vs. flat v \<in> r \<rightarrow> v \<and> flat v \<noteq> []"
267 32b222d77fa0 updated Christian Urban <urbanc@in.tum.de> parents: 266 diff changeset	718	and "\<not>(\<exists>vs2 \<in> LV (STAR r) (flat (Stars vs)). vs2 :\<sqsubset>val (Stars vs))"
265 d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	719	shows "(flat (Stars vs)) \<in> (STAR r) \<rightarrow> Stars vs"
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	720	using assms
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	721	proof(induct vs)
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	722	case Nil
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	723	show "flat (Stars []) \<in> STAR r \<rightarrow> Stars []"
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	724	by(simp add: Posix.intros)
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	725	next
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	726	case (Cons v vs)
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	727	have IH: "\<lbrakk>\<forall>v\<in>set vs. flat v \<in> r \<rightarrow> v \<and> flat v \<noteq> [];
267 32b222d77fa0 updated Christian Urban <urbanc@in.tum.de> parents: 266 diff changeset	728	\<not> (\<exists>vs2\<in>LV (STAR r) (flat (Stars vs)). vs2 :\<sqsubset>val Stars vs)\<rbrakk>
265 d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	729	\<Longrightarrow> flat (Stars vs) \<in> STAR r \<rightarrow> Stars vs" by fact
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	730	have as2: "\<forall>v\<in>set (v # vs). flat v \<in> r \<rightarrow> v \<and> flat v \<noteq> []" by fact
267 32b222d77fa0 updated Christian Urban <urbanc@in.tum.de> parents: 266 diff changeset	731	have as3: "\<not> (\<exists>vs2\<in>LV (STAR r) (flat (Stars (v # vs))). vs2 :\<sqsubset>val Stars (v # vs))" by fact
265 d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	732	have "flat v \<in> r \<rightarrow> v" using as2 by simp
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	733	moreover
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	734	have "flat (Stars vs) \<in> STAR r \<rightarrow> Stars vs"
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	735	proof (rule IH)
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	736	show "\<forall>v\<in>set vs. flat v \<in> r \<rightarrow> v \<and> flat v \<noteq> []" using as2 by simp
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	737	next
267 32b222d77fa0 updated Christian Urban <urbanc@in.tum.de> parents: 266 diff changeset	738	show "\<not> (\<exists>vs2\<in>LV (STAR r) (flat (Stars vs)). vs2 :\<sqsubset>val Stars vs)" using as3
265 d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	739	apply(auto)
267 32b222d77fa0 updated Christian Urban <urbanc@in.tum.de> parents: 266 diff changeset	740	apply(subst (asm) (2) LV_def)
265 d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	741	apply(auto)
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	742	apply(erule Prf.cases)
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	743	apply(simp_all)
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	744	apply(drule_tac x="Stars (v # vs)" in bspec)
267 32b222d77fa0 updated Christian Urban <urbanc@in.tum.de> parents: 266 diff changeset	745	apply(simp add: LV_def CV_def)
266 fff2e1b40dfc updated Christian Urban <urbanc@in.tum.de> parents: 265 diff changeset	746	using Posix_Prf Prf.intros(6) calculation
265 d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	747	apply(rule_tac Prf.intros)
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	748	apply(simp add:)
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	749	apply (simp add: PosOrd_StarsI2)
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	750	done
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	751	qed
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	752	moreover
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	753	have "flat v \<noteq> []" using as2 by simp
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	754	moreover
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	755	have "\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = flat (Stars vs) \<and> flat v @ s\<^sub>3 \<in> L r \<and> s\<^sub>4 \<in> L (STAR r))"
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	756	using as3
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	757	apply(auto)
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	758	apply(drule L_flat_Prf2)
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	759	apply(erule exE)
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	760	apply(simp only: L.simps[symmetric])
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	761	apply(drule L_flat_Prf2)
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	762	apply(erule exE)
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	763	apply(clarify)
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	764	apply(rotate_tac 5)
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	765	apply(erule Prf.cases)
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	766	apply(simp_all)
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	767	apply(clarify)
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	768	apply(drule_tac x="Stars (va#vs)" in bspec)
267 32b222d77fa0 updated Christian Urban <urbanc@in.tum.de> parents: 266 diff changeset	769	apply(auto simp add: LV_def)[1]
265 d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	770	apply(rule Prf.intros)
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	771	apply(simp)
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	772	by (simp add: PosOrd_StarsI PosOrd_shorterI)
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	773	ultimately show "flat (Stars (v # vs)) \<in> STAR r \<rightarrow> Stars (v # vs)"
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	774	by (simp add: Posix.intros)
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	775	qed
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	776
248 b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	777
254 7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	778
261 247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	779	section {* The Smallest Value is indeed the Posix Value *}
248 b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	780
265 d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	781	text {*
267 32b222d77fa0 updated Christian Urban <urbanc@in.tum.de> parents: 266 diff changeset	782	The next lemma seems to require LV instead of CV in the Star-case.
265 d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	783	*}
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	784
261 247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	785	lemma PosOrd_Posix:
267 32b222d77fa0 updated Christian Urban <urbanc@in.tum.de> parents: 266 diff changeset	786	assumes "v1 \<in> CV r s" "\<forall>v\<^sub>2 \<in> LV r s. \<not> v\<^sub>2 :\<sqsubset>val v1"
248 b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	787	shows "s \<in> r \<rightarrow> v1"
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	788	using assms
261 247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	789	proof(induct r arbitrary: s v1)
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	790	case (ZERO s v1)
267 32b222d77fa0 updated Christian Urban <urbanc@in.tum.de> parents: 266 diff changeset	791	have "v1 \<in> CV ZERO s" by fact
32b222d77fa0 updated Christian Urban <urbanc@in.tum.de> parents: 266 diff changeset	792	then show "s \<in> ZERO \<rightarrow> v1" unfolding CV_def
261 247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	793	by (auto elim: CPrf.cases)
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	794	next
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	795	case (ONE s v1)
267 32b222d77fa0 updated Christian Urban <urbanc@in.tum.de> parents: 266 diff changeset	796	have "v1 \<in> CV ONE s" by fact
32b222d77fa0 updated Christian Urban <urbanc@in.tum.de> parents: 266 diff changeset	797	then show "s \<in> ONE \<rightarrow> v1" unfolding CV_def
261 247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	798	by(auto elim!: CPrf.cases intro: Posix.intros)
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	799	next
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	800	case (CHAR c s v1)
267 32b222d77fa0 updated Christian Urban <urbanc@in.tum.de> parents: 266 diff changeset	801	have "v1 \<in> CV (CHAR c) s" by fact
32b222d77fa0 updated Christian Urban <urbanc@in.tum.de> parents: 266 diff changeset	802	then show "s \<in> CHAR c \<rightarrow> v1" unfolding CV_def
261 247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	803	by (auto elim!: CPrf.cases intro: Posix.intros)
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	804	next
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	805	case (ALT r1 r2 s v1)
267 32b222d77fa0 updated Christian Urban <urbanc@in.tum.de> parents: 266 diff changeset	806	have IH1: "\<And>s v1. \<lbrakk>v1 \<in> CV r1 s; \<forall>v2 \<in> LV r1 s. \<not> v2 :\<sqsubset>val v1\<rbrakk> \<Longrightarrow> s \<in> r1 \<rightarrow> v1" by fact
32b222d77fa0 updated Christian Urban <urbanc@in.tum.de> parents: 266 diff changeset	807	have IH2: "\<And>s v1. \<lbrakk>v1 \<in> CV r2 s; \<forall>v2 \<in> LV r2 s. \<not> v2 :\<sqsubset>val v1\<rbrakk> \<Longrightarrow> s \<in> r2 \<rightarrow> v1" by fact
32b222d77fa0 updated Christian Urban <urbanc@in.tum.de> parents: 266 diff changeset	808	have as1: "\<forall>v2\<in>LV (ALT r1 r2) s. \<not> v2 :\<sqsubset>val v1" by fact
32b222d77fa0 updated Christian Urban <urbanc@in.tum.de> parents: 266 diff changeset	809	have as2: "v1 \<in> CV (ALT r1 r2) s" by fact
261 247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	810	then consider
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	811	(Left) v1' where
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	812	"v1 = Left v1'" "s = flat v1'"
267 32b222d77fa0 updated Christian Urban <urbanc@in.tum.de> parents: 266 diff changeset	813	"v1' \<in> CV r1 s"
261 247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	814	\| (Right) v1' where
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	815	"v1 = Right v1'" "s = flat v1'"
267 32b222d77fa0 updated Christian Urban <urbanc@in.tum.de> parents: 266 diff changeset	816	"v1' \<in> CV r2 s"
32b222d77fa0 updated Christian Urban <urbanc@in.tum.de> parents: 266 diff changeset	817	unfolding CV_def by (auto elim: CPrf.cases)
261 247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	818	then show "s \<in> ALT r1 r2 \<rightarrow> v1"
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	819	proof (cases)
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	820	case (Left v1')
267 32b222d77fa0 updated Christian Urban <urbanc@in.tum.de> parents: 266 diff changeset	821	have "v1' \<in> CV r1 s" using as2
32b222d77fa0 updated Christian Urban <urbanc@in.tum.de> parents: 266 diff changeset	822	unfolding CV_def Left by (auto elim: CPrf.cases)
261 247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	823	moreover
267 32b222d77fa0 updated Christian Urban <urbanc@in.tum.de> parents: 266 diff changeset	824	have "\<forall>v2 \<in> LV r1 s. \<not> v2 :\<sqsubset>val v1'" using as1
32b222d77fa0 updated Christian Urban <urbanc@in.tum.de> parents: 266 diff changeset	825	unfolding LV_def Left using Prf.intros(2) PosOrd_Left_eq by force
261 247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	826	ultimately have "s \<in> r1 \<rightarrow> v1'" using IH1 by simp
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	827	then have "s \<in> ALT r1 r2 \<rightarrow> Left v1'" by (rule Posix.intros)
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	828	then show "s \<in> ALT r1 r2 \<rightarrow> v1" using Left by simp
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	829	next
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	830	case (Right v1')
267 32b222d77fa0 updated Christian Urban <urbanc@in.tum.de> parents: 266 diff changeset	831	have "v1' \<in> CV r2 s" using as2
32b222d77fa0 updated Christian Urban <urbanc@in.tum.de> parents: 266 diff changeset	832	unfolding CV_def Right by (auto elim: CPrf.cases)
261 247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	833	moreover
267 32b222d77fa0 updated Christian Urban <urbanc@in.tum.de> parents: 266 diff changeset	834	have "\<forall>v2 \<in> LV r2 s. \<not> v2 :\<sqsubset>val v1'" using as1
32b222d77fa0 updated Christian Urban <urbanc@in.tum.de> parents: 266 diff changeset	835	unfolding LV_def Right using Prf.intros(3) PosOrd_RightI by force
261 247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	836	ultimately have "s \<in> r2 \<rightarrow> v1'" using IH2 by simp
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	837	moreover
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	838	{ assume "s \<in> L r1"
267 32b222d77fa0 updated Christian Urban <urbanc@in.tum.de> parents: 266 diff changeset	839	then obtain v' where "v' \<in> LV r1 s"
32b222d77fa0 updated Christian Urban <urbanc@in.tum.de> parents: 266 diff changeset	840	unfolding LV_def using L_flat_Prf2 by blast
32b222d77fa0 updated Christian Urban <urbanc@in.tum.de> parents: 266 diff changeset	841	then have "Left v' \<in> LV (ALT r1 r2) s"
32b222d77fa0 updated Christian Urban <urbanc@in.tum.de> parents: 266 diff changeset	842	unfolding LV_def by (auto intro: Prf.intros)
261 247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	843	with as1 have "\<not> (Left v' :\<sqsubset>val Right v1') \<and> (flat v' = s)"
267 32b222d77fa0 updated Christian Urban <urbanc@in.tum.de> parents: 266 diff changeset	844	unfolding LV_def Right by (auto)
261 247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	845	then have False using PosOrd_Left_Right Right by blast
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	846	}
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	847	then have "s \<notin> L r1" by rule
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	848	ultimately have "s \<in> ALT r1 r2 \<rightarrow> Right v1'" by (rule Posix.intros)
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	849	then show "s \<in> ALT r1 r2 \<rightarrow> v1" using Right by simp
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	850	qed
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	851	next
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	852	case (SEQ r1 r2 s v1)
267 32b222d77fa0 updated Christian Urban <urbanc@in.tum.de> parents: 266 diff changeset	853	have IH1: "\<And>s v1. \<lbrakk>v1 \<in> CV r1 s; \<forall>v2 \<in> LV r1 s. \<not> v2 :\<sqsubset>val v1\<rbrakk> \<Longrightarrow> s \<in> r1 \<rightarrow> v1" by fact
32b222d77fa0 updated Christian Urban <urbanc@in.tum.de> parents: 266 diff changeset	854	have IH2: "\<And>s v1. \<lbrakk>v1 \<in> CV r2 s; \<forall>v2 \<in> LV r2 s. \<not> v2 :\<sqsubset>val v1\<rbrakk> \<Longrightarrow> s \<in> r2 \<rightarrow> v1" by fact
32b222d77fa0 updated Christian Urban <urbanc@in.tum.de> parents: 266 diff changeset	855	have as1: "\<forall>v2\<in>LV (SEQ r1 r2) s. \<not> v2 :\<sqsubset>val v1" by fact
32b222d77fa0 updated Christian Urban <urbanc@in.tum.de> parents: 266 diff changeset	856	have as2: "v1 \<in> CV (SEQ r1 r2) s" by fact
261 247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	857	then obtain
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	858	v1a v1b where eqs:
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	859	"v1 = Seq v1a v1b" "s = flat v1a @ flat v1b"
267 32b222d77fa0 updated Christian Urban <urbanc@in.tum.de> parents: 266 diff changeset	860	"v1a \<in> CV r1 (flat v1a)" "v1b \<in> CV r2 (flat v1b)"
32b222d77fa0 updated Christian Urban <urbanc@in.tum.de> parents: 266 diff changeset	861	unfolding CV_def by(auto elim: CPrf.cases)
32b222d77fa0 updated Christian Urban <urbanc@in.tum.de> parents: 266 diff changeset	862	have "\<forall>v2 \<in> LV r1 (flat v1a). \<not> v2 :\<sqsubset>val v1a"
261 247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	863	proof
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	864	fix v2
267 32b222d77fa0 updated Christian Urban <urbanc@in.tum.de> parents: 266 diff changeset	865	assume "v2 \<in> LV r1 (flat v1a)"
32b222d77fa0 updated Christian Urban <urbanc@in.tum.de> parents: 266 diff changeset	866	with eqs(2,4) have "Seq v2 v1b \<in> LV (SEQ r1 r2) s"
32b222d77fa0 updated Christian Urban <urbanc@in.tum.de> parents: 266 diff changeset	867	by (simp add: CV_def LV_def Prf.intros(1) Prf_CPrf)
261 247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	868	with as1 have "\<not> Seq v2 v1b :\<sqsubset>val Seq v1a v1b \<and> flat (Seq v2 v1b) = flat (Seq v1a v1b)"
267 32b222d77fa0 updated Christian Urban <urbanc@in.tum.de> parents: 266 diff changeset	869	using eqs by (simp add: LV_def)
261 247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	870	then show "\<not> v2 :\<sqsubset>val v1a"
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	871	using PosOrd_SeqI1 by blast
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	872	qed
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	873	then have "flat v1a \<in> r1 \<rightarrow> v1a" using IH1 eqs by simp
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	874	moreover
267 32b222d77fa0 updated Christian Urban <urbanc@in.tum.de> parents: 266 diff changeset	875	have "\<forall>v2 \<in> LV r2 (flat v1b). \<not> v2 :\<sqsubset>val v1b"
261 247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	876	proof
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	877	fix v2
267 32b222d77fa0 updated Christian Urban <urbanc@in.tum.de> parents: 266 diff changeset	878	assume "v2 \<in> LV r2 (flat v1b)"
32b222d77fa0 updated Christian Urban <urbanc@in.tum.de> parents: 266 diff changeset	879	with eqs(2,3,4) have "Seq v1a v2 \<in> LV (SEQ r1 r2) s"
32b222d77fa0 updated Christian Urban <urbanc@in.tum.de> parents: 266 diff changeset	880	by (simp add: CV_def LV_def Prf.intros Prf_CPrf)
261 247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	881	with as1 have "\<not> Seq v1a v2 :\<sqsubset>val Seq v1a v1b \<and> flat v2 = flat v1b"
267 32b222d77fa0 updated Christian Urban <urbanc@in.tum.de> parents: 266 diff changeset	882	using eqs by (simp add: LV_def)
261 247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	883	then show "\<not> v2 :\<sqsubset>val v1b"
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	884	using PosOrd_SeqI2 by auto
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	885	qed
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	886	then have "flat v1b \<in> r2 \<rightarrow> v1b" using IH2 eqs by simp
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	887	moreover
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	888	have "\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = flat v1b \<and> flat v1a @ s\<^sub>3 \<in> L r1 \<and> s\<^sub>4 \<in> L r2)"
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	889	proof
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	890	assume "\<exists>s3 s4. s3 \<noteq> [] \<and> s3 @ s4 = flat v1b \<and> flat v1a @ s3 \<in> L r1 \<and> s4 \<in> L r2"
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	891	then obtain s3 s4 where q1: "s3 \<noteq> [] \<and> s3 @ s4 = flat v1b \<and> flat v1a @ s3 \<in> L r1 \<and> s4 \<in> L r2" by blast
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	892	then obtain vA vB where q2: "flat vA = flat v1a @ s3" "\<turnstile> vA : r1" "flat vB = s4" "\<turnstile> vB : r2"
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	893	using L_flat_Prf2 by blast
267 32b222d77fa0 updated Christian Urban <urbanc@in.tum.de> parents: 266 diff changeset	894	then have "Seq vA vB \<in> LV (SEQ r1 r2) s" unfolding eqs using q1
32b222d77fa0 updated Christian Urban <urbanc@in.tum.de> parents: 266 diff changeset	895	by (auto simp add: LV_def intro: Prf.intros)
261 247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	896	with as1 have "\<not> Seq vA vB :\<sqsubset>val Seq v1a v1b" unfolding eqs by auto
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	897	then have "\<not> vA :\<sqsubset>val v1a \<and> length (flat vA) > length (flat v1a)" using q1 q2 PosOrd_SeqI1 by auto
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	898	then show "False"
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	899	using PosOrd_shorterI by blast
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	900	qed
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	901	ultimately
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	902	show "s \<in> SEQ r1 r2 \<rightarrow> v1" unfolding eqs
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	903	by (rule Posix.intros)
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	904	next
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	905	case (STAR r s v1)
267 32b222d77fa0 updated Christian Urban <urbanc@in.tum.de> parents: 266 diff changeset	906	have IH: "\<And>s v1. \<lbrakk>v1 \<in> CV r s; \<forall>v2\<in>LV r s. \<not> v2 :\<sqsubset>val v1\<rbrakk> \<Longrightarrow> s \<in> r \<rightarrow> v1" by fact
32b222d77fa0 updated Christian Urban <urbanc@in.tum.de> parents: 266 diff changeset	907	have as1: "\<forall>v2\<in>LV (STAR r) s. \<not> v2 :\<sqsubset>val v1" by fact
32b222d77fa0 updated Christian Urban <urbanc@in.tum.de> parents: 266 diff changeset	908	have as2: "v1 \<in> CV (STAR r) s" by fact
261 247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	909	then obtain
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	910	vs where eqs:
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	911	"v1 = Stars vs" "s = flat (Stars vs)"
267 32b222d77fa0 updated Christian Urban <urbanc@in.tum.de> parents: 266 diff changeset	912	"\<forall>v \<in> set vs. v \<in> CV r (flat v)"
32b222d77fa0 updated Christian Urban <urbanc@in.tum.de> parents: 266 diff changeset	913	unfolding CV_def by (auto elim: CPrf.cases)
265 d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	914	have "\<forall>v\<in>set vs. flat v \<in> r \<rightarrow> v \<and> flat v \<noteq> []"
261 247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	915	proof
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	916	fix v
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	917	assume a: "v \<in> set vs"
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	918	then obtain pre post where e: "vs = pre @ [v] @ post"
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	919	by (metis append_Cons append_Nil in_set_conv_decomp_first)
267 32b222d77fa0 updated Christian Urban <urbanc@in.tum.de> parents: 266 diff changeset	920	then have q: "\<forall>v2\<in>LV (STAR r) s. \<not> v2 :\<sqsubset>val Stars (pre @ [v] @ post)"
261 247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	921	using as1 unfolding eqs by simp
267 32b222d77fa0 updated Christian Urban <urbanc@in.tum.de> parents: 266 diff changeset	922	have "\<forall>v2\<in>LV r (flat v). \<not> v2 :\<sqsubset>val v" unfolding eqs
261 247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	923	proof (rule ballI, rule notI)
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	924	fix v2
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	925	assume w: "v2 :\<sqsubset>val v"
267 32b222d77fa0 updated Christian Urban <urbanc@in.tum.de> parents: 266 diff changeset	926	assume "v2 \<in> LV r (flat v)"
32b222d77fa0 updated Christian Urban <urbanc@in.tum.de> parents: 266 diff changeset	927	then have "Stars (pre @ [v2] @ post) \<in> LV (STAR r) s"
261 247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	928	using as2 unfolding e eqs
267 32b222d77fa0 updated Christian Urban <urbanc@in.tum.de> parents: 266 diff changeset	929	apply(auto simp add: CV_def LV_def intro!: Prf.intros)[1]
32b222d77fa0 updated Christian Urban <urbanc@in.tum.de> parents: 266 diff changeset	930	using CPrf_Stars_appendE Prf_CPrf Prf_elims(6) list.set_intros apply blast
32b222d77fa0 updated Christian Urban <urbanc@in.tum.de> parents: 266 diff changeset	931	by (metis CPrf_Stars_appendE Prf_CPrf Prf_elims(6) list.set_intros(2) val.inject(5))
261 247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	932	then have "\<not> Stars (pre @ [v2] @ post) :\<sqsubset>val Stars (pre @ [v] @ post)"
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	933	using q by simp
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	934	with w show "False"
267 32b222d77fa0 updated Christian Urban <urbanc@in.tum.de> parents: 266 diff changeset	935	using LV_def \<open>v2 \<in> LV r (flat v)\<close> append_Cons flat.simps(7) mem_Collect_eq
261 247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	936	PosOrd_StarsI PosOrd_Stars_appendI by auto
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	937	qed
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	938	with IH
267 32b222d77fa0 updated Christian Urban <urbanc@in.tum.de> parents: 266 diff changeset	939	show "flat v \<in> r \<rightarrow> v \<and> flat v \<noteq> []" using a as2 unfolding eqs CV_def
32b222d77fa0 updated Christian Urban <urbanc@in.tum.de> parents: 266 diff changeset	940	by (auto elim: CPrf.cases)
261 247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	941	qed
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	942	moreover
267 32b222d77fa0 updated Christian Urban <urbanc@in.tum.de> parents: 266 diff changeset	943	have "\<not> (\<exists>vs2\<in>LV (STAR r) (flat (Stars vs)). vs2 :\<sqsubset>val Stars vs)"
261 247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	944	proof
267 32b222d77fa0 updated Christian Urban <urbanc@in.tum.de> parents: 266 diff changeset	945	assume "\<exists>vs2 \<in> LV (STAR r) (flat (Stars vs)). vs2 :\<sqsubset>val Stars vs"
261 247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	946	then obtain vs2 where "\<turnstile> Stars vs2 : STAR r" "flat (Stars vs2) = flat (Stars vs)"
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	947	"Stars vs2 :\<sqsubset>val Stars vs"
267 32b222d77fa0 updated Christian Urban <urbanc@in.tum.de> parents: 266 diff changeset	948	unfolding LV_def
32b222d77fa0 updated Christian Urban <urbanc@in.tum.de> parents: 266 diff changeset	949	apply(auto)
261 247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	950	apply(erule Prf.cases)
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	951	apply(auto intro: Prf.intros)
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	952	done
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	953	then show "False" using as1 unfolding eqs
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	954	apply -
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	955	apply(drule_tac x="Stars vs2" in bspec)
267 32b222d77fa0 updated Christian Urban <urbanc@in.tum.de> parents: 266 diff changeset	956	apply(auto simp add: LV_def)
261 247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	957	done
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	958	qed
265 d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	959	ultimately have "flat (Stars vs) \<in> STAR r \<rightarrow> Stars vs"
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	960	thm PosOrd_Posix_Stars
261 247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	961	by (rule PosOrd_Posix_Stars)
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	962	then show "s \<in> STAR r \<rightarrow> v1" unfolding eqs .
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	963	qed
248 b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	964
249 256484ef4be4 updated Christian Urban <urbanc@in.tum.de> parents: 248 diff changeset	965	unused_thms
256484ef4be4 updated Christian Urban <urbanc@in.tum.de> parents: 248 diff changeset	966
248 b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	967	end

author	Christian Urban <urbanc@in.tum.de>
	Fri, 11 Aug 2017 20:29:01 +0100
changeset 267	32b222d77fa0
parent 266	fff2e1b40dfc
child 268	6746f5e1f1f8
permissions	-rw-r--r--