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

author	Christian Urban <urbanc@in.tum.de>
	Wed, 19 Jul 2017 14:55:46 +0100
changeset 266	fff2e1b40dfc
parent 265	d36be1e356c0
child 267	32b222d77fa0
permissions	-rw-r--r--