lexing: thys/Positions.thy@d36be1e356c0 (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
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	3	imports "Lexer"
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
265 d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	166	definition pflat_len2 :: "val \<Rightarrow> nat list => (bool * nat)"
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	167	where
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	168	"pflat_len2 v p \<equiv> (if p \<in> Pos v then (True, length (flat (at v p))) else (False, 0))"
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	169
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	170	instance prod :: (ord, ord) ord
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	171	by (rule Orderings.class.Orderings.ord.of_class.intro)
264 e2828c4a1e23 updated Christian Urban <urbanc@in.tum.de> parents: 263 diff changeset	172
e2828c4a1e23 updated Christian Urban <urbanc@in.tum.de> parents: 263 diff changeset	173
265 d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	174	lemma "(0, 0) < (3::nat, 2::nat)"
264 e2828c4a1e23 updated Christian Urban <urbanc@in.tum.de> parents: 263 diff changeset	175
265 d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	176
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	177
261 247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	178
265 d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	179	definition PosOrd2:: "val \<Rightarrow> nat list \<Rightarrow> val \<Rightarrow> bool" ("_ \<sqsubset>val2 _ _" [60, 60, 59] 60)
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	180	where
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	181	"v1 \<sqsubset>val2 p v2 \<equiv> (fst (pflat_len2 v1 p) > fst (pflat_len2 v2 p) \<or>
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	182	snd (pflat_len2 v1 p) > fst (pflat_len2 v2 p)) \<and>
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	183	(\<forall>q \<in> Pos v1 \<union> Pos v2. q \<sqsubset>lex p \<longrightarrow> pflat_len v1 q = pflat_len v2 q)"
248 b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	184
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	185
261 247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	186	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	187	where
265 d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	188	"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	189
265 d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	190	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	191	where
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	192	"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	193
265 d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	194
261 247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	195	lemma PosOrd_shorterE:
255 222ed43892ea updated Christian Urban <urbanc@in.tum.de> parents: 254 diff changeset	196	assumes "v1 :\<sqsubset>val v2"
222ed43892ea updated Christian Urban <urbanc@in.tum.de> parents: 254 diff changeset	197	shows "length (flat v2) \<le> length (flat v1)"
222ed43892ea updated Christian Urban <urbanc@in.tum.de> parents: 254 diff changeset	198	using assms
265 d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	199	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	200	apply(case_tac p)
265 d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	201	apply(simp add: pflat_len_simps intlen_length)
255 222ed43892ea updated Christian Urban <urbanc@in.tum.de> parents: 254 diff changeset	202	apply(simp)
222ed43892ea updated Christian Urban <urbanc@in.tum.de> parents: 254 diff changeset	203	apply(drule_tac x="[]" in bspec)
222ed43892ea updated Christian Urban <urbanc@in.tum.de> parents: 254 diff changeset	204	apply(simp add: Pos_empty)
265 d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	205	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	206	done
255 222ed43892ea updated Christian Urban <urbanc@in.tum.de> parents: 254 diff changeset	207
261 247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	208	lemma PosOrd_shorterI:
265 d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	209	assumes "length (flat v2) < length (flat v1)"
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	210	shows "v1 :\<sqsubset>val v2"
251 925232418a15 polished Christian Urban <urbanc@in.tum.de> parents: 250 diff changeset	211	using assms
261 247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	212	unfolding PosOrd_ex_def
264 e2828c4a1e23 updated Christian Urban <urbanc@in.tum.de> parents: 263 diff changeset	213	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	214
261 247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	215	lemma PosOrd_spreI:
265 d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	216	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	217	shows "v :\<sqsubset>val v'"
251 925232418a15 polished Christian Urban <urbanc@in.tum.de> parents: 250 diff changeset	218	using assms
261 247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	219	apply(rule_tac PosOrd_shorterI)
251 925232418a15 polished Christian Urban <urbanc@in.tum.de> parents: 250 diff changeset	220	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	221
265 d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	222
261 247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	223	lemma PosOrd_Left_Right:
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	224	assumes "flat v1 = flat v2"
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	225	shows "Left v1 :\<sqsubset>val Right v2"
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	226	unfolding PosOrd_ex_def
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	227	apply(rule_tac x="[0]" in exI)
265 d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	228	using assms
264 e2828c4a1e23 updated Christian Urban <urbanc@in.tum.de> parents: 263 diff changeset	229	apply(auto simp add: PosOrd_def pflat_len_simps)
261 247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	230	apply(smt intlen_bigger)
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	231	done
256 146b4817aebd updated Christian Urban <urbanc@in.tum.de> parents: 255 diff changeset	232
265 d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	233	lemma PosOrd_Left_eq:
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	234	assumes "flat v = flat v'"
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	235	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	236	using assms
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)
265 d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	239	apply(case_tac p)
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	240	apply(simp add: PosOrd_def pflat_len_simps)
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	241	apply(case_tac a)
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	242	apply(simp add: PosOrd_def pflat_len_simps)
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	243	apply(rule_tac x="list" in exI)
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	244	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	245	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	246	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	247	apply(auto simp add: PosOrd_def pflat_len_outside)[1]
251 925232418a15 polished Christian Urban <urbanc@in.tum.de> parents: 250 diff changeset	248	apply(rule_tac x="0#p" in exI)
261 247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	249	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	250	done
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	251
265 d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	252
261 247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	253	lemma PosOrd_RightI:
251 925232418a15 polished Christian Urban <urbanc@in.tum.de> parents: 250 diff changeset	254	assumes "v :\<sqsubset>val v'" "flat v = flat v'"
925232418a15 polished Christian Urban <urbanc@in.tum.de> parents: 250 diff changeset	255	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	256	using assms(1)
261 247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	257	unfolding PosOrd_ex_def
251 925232418a15 polished Christian Urban <urbanc@in.tum.de> parents: 250 diff changeset	258	apply(auto)
925232418a15 polished Christian Urban <urbanc@in.tum.de> parents: 250 diff changeset	259	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	260	using assms(2)
261 247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	261	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	262	done
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	263
261 247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	264	lemma PosOrd_RightE:
252 022b80503766 polished Christian Urban <urbanc@in.tum.de> parents: 251 diff changeset	265	assumes "(Right v1) :\<sqsubset>val (Right v2)"
022b80503766 polished Christian Urban <urbanc@in.tum.de> parents: 251 diff changeset	266	shows "v1 :\<sqsubset>val v2"
022b80503766 polished Christian Urban <urbanc@in.tum.de> parents: 251 diff changeset	267	using assms
261 247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	268	apply(simp add: PosOrd_ex_def)
252 022b80503766 polished Christian Urban <urbanc@in.tum.de> parents: 251 diff changeset	269	apply(erule exE)
264 e2828c4a1e23 updated Christian Urban <urbanc@in.tum.de> parents: 263 diff changeset	270	apply(case_tac p)
261 247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	271	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	272	apply(auto simp add: pflat_len_simps)
252 022b80503766 polished Christian Urban <urbanc@in.tum.de> parents: 251 diff changeset	273	apply(rule_tac x="[]" in exI)
022b80503766 polished Christian Urban <urbanc@in.tum.de> parents: 251 diff changeset	274	apply(simp add: Pos_empty pflat_len_simps)
264 e2828c4a1e23 updated Christian Urban <urbanc@in.tum.de> parents: 263 diff changeset	275	apply(case_tac a)
e2828c4a1e23 updated Christian Urban <urbanc@in.tum.de> parents: 263 diff changeset	276	apply(simp add: pflat_len_def PosOrd_def)
e2828c4a1e23 updated Christian Urban <urbanc@in.tum.de> parents: 263 diff changeset	277	apply(case_tac nat)
e2828c4a1e23 updated Christian Urban <urbanc@in.tum.de> parents: 263 diff changeset	278	prefer 2
e2828c4a1e23 updated Christian Urban <urbanc@in.tum.de> parents: 263 diff changeset	279	apply(simp add: pflat_len_def PosOrd_def)
261 247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	280	apply(auto simp add: pflat_len_simps PosOrd_def)
264 e2828c4a1e23 updated Christian Urban <urbanc@in.tum.de> parents: 263 diff changeset	281	apply(rule_tac x="list" in exI)
252 022b80503766 polished Christian Urban <urbanc@in.tum.de> parents: 251 diff changeset	282	apply(auto)
022b80503766 polished Christian Urban <urbanc@in.tum.de> parents: 251 diff changeset	283	apply(drule_tac x="Suc 0#q" in bspec)
022b80503766 polished Christian Urban <urbanc@in.tum.de> parents: 251 diff changeset	284	apply(simp)
022b80503766 polished Christian Urban <urbanc@in.tum.de> parents: 251 diff changeset	285	apply(simp add: pflat_len_simps)
022b80503766 polished Christian Urban <urbanc@in.tum.de> parents: 251 diff changeset	286	apply(drule_tac x="Suc 0#q" in bspec)
022b80503766 polished Christian Urban <urbanc@in.tum.de> parents: 251 diff changeset	287	apply(simp)
022b80503766 polished Christian Urban <urbanc@in.tum.de> parents: 251 diff changeset	288	apply(simp add: pflat_len_simps)
022b80503766 polished Christian Urban <urbanc@in.tum.de> parents: 251 diff changeset	289	done
022b80503766 polished Christian Urban <urbanc@in.tum.de> parents: 251 diff changeset	290
248 b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	291
261 247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	292	lemma PosOrd_SeqI1:
252 022b80503766 polished Christian Urban <urbanc@in.tum.de> parents: 251 diff changeset	293	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	294	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	295	using assms(1)
261 247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	296	apply(subst (asm) PosOrd_ex_def)
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	297	apply(subst (asm) PosOrd_def)
252 022b80503766 polished Christian Urban <urbanc@in.tum.de> parents: 251 diff changeset	298	apply(clarify)
261 247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	299	apply(subst PosOrd_ex_def)
252 022b80503766 polished Christian Urban <urbanc@in.tum.de> parents: 251 diff changeset	300	apply(rule_tac x="0#p" in exI)
261 247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	301	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	302	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	303	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	304	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	305	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	306	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	307	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	308	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	309	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	310	apply(simp)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	311	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	312	done
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	313
261 247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	314	lemma PosOrd_SeqI2:
252 022b80503766 polished Christian Urban <urbanc@in.tum.de> parents: 251 diff changeset	315	assumes "v2 :\<sqsubset>val v2'" "flat v2 = flat v2'"
022b80503766 polished Christian Urban <urbanc@in.tum.de> parents: 251 diff changeset	316	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	317	using assms(1)
261 247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	318	apply(subst (asm) PosOrd_ex_def)
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	319	apply(subst (asm) PosOrd_def)
252 022b80503766 polished Christian Urban <urbanc@in.tum.de> parents: 251 diff changeset	320	apply(clarify)
261 247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	321	apply(subst PosOrd_ex_def)
252 022b80503766 polished Christian Urban <urbanc@in.tum.de> parents: 251 diff changeset	322	apply(rule_tac x="Suc 0#p" in exI)
261 247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	323	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	324	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	325	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	326	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	327	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	328	apply(simp only: Pos.simps)
252 022b80503766 polished Christian Urban <urbanc@in.tum.de> parents: 251 diff changeset	329	apply(auto)[1]
022b80503766 polished Christian Urban <urbanc@in.tum.de> parents: 251 diff changeset	330	apply(simp add: pflat_len_simps)
022b80503766 polished Christian Urban <urbanc@in.tum.de> parents: 251 diff changeset	331	using assms(2)
022b80503766 polished Christian Urban <urbanc@in.tum.de> parents: 251 diff changeset	332	apply(simp)
022b80503766 polished Christian Urban <urbanc@in.tum.de> parents: 251 diff changeset	333	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	334	done
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	335
261 247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	336	lemma PosOrd_SeqE:
254 7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	337	assumes "(Seq v1 v2) :\<sqsubset>val (Seq v1' v2')"
7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	338	shows "v1 :\<sqsubset>val v1' \<or> v2 :\<sqsubset>val v2'"
7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	339	using assms
261 247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	340	apply(simp add: PosOrd_ex_def)
254 7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	341	apply(erule exE)
7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	342	apply(case_tac p)
261 247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	343	apply(simp add: PosOrd_def)
254 7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	344	apply(auto simp add: pflat_len_simps intlen_append)[1]
7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	345	apply(rule_tac x="[]" in exI)
7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	346	apply(drule_tac x="[]" in spec)
7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	347	apply(simp add: Pos_empty pflat_len_simps)
7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	348	apply(case_tac a)
7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	349	apply(rule disjI1)
261 247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	350	apply(simp add: PosOrd_def)
254 7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	351	apply(auto simp add: pflat_len_simps intlen_append)[1]
7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	352	apply(rule_tac x="list" in exI)
7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	353	apply(simp)
7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	354	apply(rule ballI)
7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	355	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	356	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	357	apply(simp)
254 7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	358	apply(simp add: pflat_len_simps)
7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	359	apply(case_tac nat)
7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	360	apply(rule disjI2)
261 247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	361	apply(simp add: PosOrd_def)
254 7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	362	apply(auto simp add: pflat_len_simps intlen_append)
7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	363	apply(rule_tac x="list" in exI)
7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	364	apply(simp add: Pos_empty)
7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	365	apply(rule ballI)
7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	366	apply(rule impI)
264 e2828c4a1e23 updated Christian Urban <urbanc@in.tum.de> parents: 263 diff changeset	367	apply(auto)[1]
254 7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	368	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	369	apply(simp)
254 7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	370	apply(simp add: pflat_len_simps)
264 e2828c4a1e23 updated Christian Urban <urbanc@in.tum.de> parents: 263 diff changeset	371	apply(drule_tac x="Suc 0#q" in bspec)
e2828c4a1e23 updated Christian Urban <urbanc@in.tum.de> parents: 263 diff changeset	372	apply(simp)
e2828c4a1e23 updated Christian Urban <urbanc@in.tum.de> parents: 263 diff changeset	373	apply(simp add: pflat_len_simps)
e2828c4a1e23 updated Christian Urban <urbanc@in.tum.de> parents: 263 diff changeset	374	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	375	done
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	376
261 247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	377	lemma PosOrd_StarsI:
254 7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	378	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	379	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	380	using assms(1)
261 247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	381	apply(subst (asm) PosOrd_ex_def)
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	382	apply(subst (asm) PosOrd_def)
254 7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	383	apply(clarify)
261 247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	384	apply(subst PosOrd_ex_def)
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	385	apply(subst PosOrd_def)
254 7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	386	apply(rule_tac x="0#p" 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)
248 b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	391	done
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	392
261 247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	393	lemma PosOrd_StarsI2:
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 (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	396	using assms(1)
261 247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	397	apply(subst (asm) PosOrd_ex_def)
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	398	apply(subst (asm) PosOrd_def)
254 7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	399	apply(clarify)
261 247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	400	apply(subst PosOrd_ex_def)
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	401	apply(subst PosOrd_def)
254 7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	402	apply(case_tac p)
7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	403	apply(simp add: pflat_len_simps)
7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	404	apply(rule_tac x="[]" in exI)
7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	405	apply(simp add: pflat_len_Stars_simps pflat_len_simps intlen_append)
7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	406	apply(rule_tac x="Suc a#list" in exI)
7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	407	apply(simp add: pflat_len_Stars_simps pflat_len_simps)
7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	408	using assms(2)
7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	409	apply(simp add: pflat_len_simps intlen_append)
7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	410	apply(auto simp add: pflat_len_Stars_simps pflat_len_simps)
7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	411	done
7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	412
261 247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	413	lemma PosOrd_Stars_appendI:
254 7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	414	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	415	shows "Stars (vs @ vs1) :\<sqsubset>val Stars (vs @ vs2)"
7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	416	using assms
7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	417	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	418	apply(simp)
261 247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	419	apply(simp add: PosOrd_StarsI2)
254 7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	420	done
7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	421
261 247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	422	lemma PosOrd_StarsE2:
254 7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	423	assumes "Stars (v # vs1) :\<sqsubset>val Stars (v # vs2)"
7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	424	shows "Stars vs1 :\<sqsubset>val Stars vs2"
7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	425	using assms
261 247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	426	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	427	apply(erule exE)
254 7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	428	apply(case_tac p)
7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	429	apply(simp)
261 247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	430	apply(simp add: PosOrd_def pflat_len_simps intlen_append)
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	431	apply(subst PosOrd_ex_def)
254 7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	432	apply(rule_tac x="[]" in exI)
261 247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	433	apply(simp add: PosOrd_def pflat_len_simps Pos_empty)
254 7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	434	apply(simp)
7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	435	apply(case_tac a)
7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	436	apply(clarify)
264 e2828c4a1e23 updated Christian Urban <urbanc@in.tum.de> parents: 263 diff changeset	437	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	438	apply(clarify)
261 247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	439	apply(simp add: PosOrd_ex_def)
254 7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	440	apply(rule_tac x="nat#list" in exI)
261 247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	441	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	442	apply(case_tac q)
261 247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	443	apply(simp add: PosOrd_def pflat_len_simps intlen_append)
254 7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	444	apply(clarify)
7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	445	apply(drule_tac x="Suc a # lista" in bspec)
7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	446	apply(simp)
261 247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	447	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	448	apply(case_tac q)
261 247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	449	apply(simp add: PosOrd_def pflat_len_simps intlen_append)
254 7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	450	apply(clarify)
7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	451	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	452	apply(simp)
261 247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	453	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	454	done
7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	455
261 247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	456	lemma PosOrd_Stars_appendE:
254 7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	457	assumes "Stars (vs @ vs1) :\<sqsubset>val Stars (vs @ vs2)"
7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	458	shows "Stars vs1 :\<sqsubset>val Stars vs2"
7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	459	using assms
7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	460	apply(induct vs)
7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	461	apply(simp)
261 247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	462	apply(simp add: PosOrd_StarsE2)
254 7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	463	done
7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	464
261 247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	465	lemma PosOrd_Stars_append_eq:
254 7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	466	assumes "flat (Stars vs1) = flat (Stars vs2)"
7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	467	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	468	using assms
7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	469	apply(rule_tac iffI)
261 247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	470	apply(erule PosOrd_Stars_appendE)
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	471	apply(rule PosOrd_Stars_appendI)
254 7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	472	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	473	done
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	474
261 247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	475	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	476	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	477	shows "v1 :\<sqsubset>val v3"
264 e2828c4a1e23 updated Christian Urban <urbanc@in.tum.de> parents: 263 diff changeset	478	proof -
e2828c4a1e23 updated Christian Urban <urbanc@in.tum.de> parents: 263 diff changeset	479	from assms obtain p p'
e2828c4a1e23 updated Christian Urban <urbanc@in.tum.de> parents: 263 diff changeset	480	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	481	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	482	by (rule lex_trichotomous)
e2828c4a1e23 updated Christian Urban <urbanc@in.tum.de> parents: 263 diff changeset	483	moreover
e2828c4a1e23 updated Christian Urban <urbanc@in.tum.de> parents: 263 diff changeset	484	{ assume "p = p'"
265 d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	485	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	486	by fastforce
264 e2828c4a1e23 updated Christian Urban <urbanc@in.tum.de> parents: 263 diff changeset	487	then have " v1 :\<sqsubset>val v3" unfolding PosOrd_ex_def by blast
e2828c4a1e23 updated Christian Urban <urbanc@in.tum.de> parents: 263 diff changeset	488	}
e2828c4a1e23 updated Christian Urban <urbanc@in.tum.de> parents: 263 diff changeset	489	moreover
e2828c4a1e23 updated Christian Urban <urbanc@in.tum.de> parents: 263 diff changeset	490	{ assume "p \<sqsubset>lex p'"
265 d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	491	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	492	by (smt Un_iff lex_trans)
264 e2828c4a1e23 updated Christian Urban <urbanc@in.tum.de> parents: 263 diff changeset	493	then have " v1 :\<sqsubset>val v3" unfolding PosOrd_ex_def by blast
e2828c4a1e23 updated Christian Urban <urbanc@in.tum.de> parents: 263 diff changeset	494	}
e2828c4a1e23 updated Christian Urban <urbanc@in.tum.de> parents: 263 diff changeset	495	moreover
e2828c4a1e23 updated Christian Urban <urbanc@in.tum.de> parents: 263 diff changeset	496	{ assume "p' \<sqsubset>lex p"
e2828c4a1e23 updated Christian Urban <urbanc@in.tum.de> parents: 263 diff changeset	497	with as have "v1 \<sqsubset>val p' v3" unfolding PosOrd_def
e2828c4a1e23 updated Christian Urban <urbanc@in.tum.de> parents: 263 diff changeset	498	by (smt Un_iff intlen_bigger lex_trans pflat_len_def)
e2828c4a1e23 updated Christian Urban <urbanc@in.tum.de> parents: 263 diff changeset	499	then have "v1 :\<sqsubset>val v3" unfolding PosOrd_ex_def by blast
e2828c4a1e23 updated Christian Urban <urbanc@in.tum.de> parents: 263 diff changeset	500	}
e2828c4a1e23 updated Christian Urban <urbanc@in.tum.de> parents: 263 diff changeset	501	ultimately show "v1 :\<sqsubset>val v3" by blast
e2828c4a1e23 updated Christian Urban <urbanc@in.tum.de> parents: 263 diff changeset	502	qed
e2828c4a1e23 updated Christian Urban <urbanc@in.tum.de> parents: 263 diff changeset	503
254 7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	504
261 247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	505	lemma PosOrd_irrefl:
256 146b4817aebd updated Christian Urban <urbanc@in.tum.de> parents: 255 diff changeset	506	assumes "v :\<sqsubset>val v"
146b4817aebd updated Christian Urban <urbanc@in.tum.de> parents: 255 diff changeset	507	shows "False"
264 e2828c4a1e23 updated Christian Urban <urbanc@in.tum.de> parents: 263 diff changeset	508	using assms unfolding PosOrd_ex_def PosOrd_def
e2828c4a1e23 updated Christian Urban <urbanc@in.tum.de> parents: 263 diff changeset	509	by auto
256 146b4817aebd updated Christian Urban <urbanc@in.tum.de> parents: 255 diff changeset	510
261 247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	511	lemma PosOrd_almost_trichotomous:
256 146b4817aebd updated Christian Urban <urbanc@in.tum.de> parents: 255 diff changeset	512	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	513	apply(auto simp add: PosOrd_ex_def)
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	514	apply(auto simp add: PosOrd_def)
256 146b4817aebd updated Christian Urban <urbanc@in.tum.de> parents: 255 diff changeset	515	apply(rule_tac x="[]" in exI)
146b4817aebd updated Christian Urban <urbanc@in.tum.de> parents: 255 diff changeset	516	apply(auto simp add: Pos_empty pflat_len_simps)
146b4817aebd updated Christian Urban <urbanc@in.tum.de> parents: 255 diff changeset	517	apply(drule_tac x="[]" in spec)
146b4817aebd updated Christian Urban <urbanc@in.tum.de> parents: 255 diff changeset	518	apply(auto simp add: Pos_empty pflat_len_simps)
146b4817aebd updated Christian Urban <urbanc@in.tum.de> parents: 255 diff changeset	519	done
146b4817aebd updated Christian Urban <urbanc@in.tum.de> parents: 255 diff changeset	520
146b4817aebd updated Christian Urban <urbanc@in.tum.de> parents: 255 diff changeset	521	lemma WW1:
146b4817aebd updated Christian Urban <urbanc@in.tum.de> parents: 255 diff changeset	522	assumes "v1 :\<sqsubset>val v2" "v2 :\<sqsubset>val v1"
146b4817aebd updated Christian Urban <urbanc@in.tum.de> parents: 255 diff changeset	523	shows "False"
146b4817aebd updated Christian Urban <urbanc@in.tum.de> parents: 255 diff changeset	524	using assms
261 247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	525	apply(auto simp add: PosOrd_ex_def PosOrd_def)
264 e2828c4a1e23 updated Christian Urban <urbanc@in.tum.de> parents: 263 diff changeset	526	using assms PosOrd_irrefl PosOrd_trans by blast
256 146b4817aebd updated Christian Urban <urbanc@in.tum.de> parents: 255 diff changeset	527
261 247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	528	lemma PosOrd_SeqE2:
265 d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	529	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	530	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	531	using assms
261 247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	532	apply(frule_tac PosOrd_SeqE)
256 146b4817aebd updated Christian Urban <urbanc@in.tum.de> parents: 255 diff changeset	533	apply(erule disjE)
146b4817aebd updated Christian Urban <urbanc@in.tum.de> parents: 255 diff changeset	534	apply(simp)
146b4817aebd updated Christian Urban <urbanc@in.tum.de> parents: 255 diff changeset	535	apply(case_tac "v1 :\<sqsubset>val v1'")
146b4817aebd updated Christian Urban <urbanc@in.tum.de> parents: 255 diff changeset	536	apply(simp)
265 d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	537	apply(rule disjI2)
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	538	apply(rule conjI)
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	539	prefer 2
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	540	apply(simp)
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	541	apply(auto)
261 247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	542	apply(auto simp add: PosOrd_ex_def)
265 d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	543	apply(auto simp add: PosOrd_def pflat_len_simps)
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	544	apply(case_tac p)
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	545	apply(auto simp add: PosOrd_def pflat_len_simps)
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	546	apply(case_tac a)
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	547	apply(auto simp add: PosOrd_def pflat_len_simps)
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	548	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	549	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	550
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	551	lemma PosOrd_SeqE4:
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	552	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	553	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	554	using assms
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	555	apply(frule_tac PosOrd_SeqE)
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	556	apply(erule disjE)
256 146b4817aebd updated Christian Urban <urbanc@in.tum.de> parents: 255 diff changeset	557	apply(simp)
265 d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	558	apply(case_tac "v1 :\<sqsubset>val v1'")
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	559	apply(simp)
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	560	apply(rule disjI2)
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	561	apply(rule conjI)
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	562	prefer 2
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	563	apply(simp)
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	564	apply(auto)
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	565	apply(case_tac "length (flat v1') < length (flat v1)")
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	566	using PosOrd_shorterI apply blast
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	567	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	568
254 7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	569
7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	570	section {* CPT and CPTpre *}
248 b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	571
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	572
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	573	inductive
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	574	CPrf :: "val \<Rightarrow> rexp \<Rightarrow> bool" ("\<Turnstile> _ : _" [100, 100] 100)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	575	where
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	576	"\<lbrakk>\<Turnstile> v1 : r1; \<Turnstile> v2 : r2\<rbrakk> \<Longrightarrow> \<Turnstile> Seq v1 v2 : SEQ r1 r2"
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	577	\| "\<Turnstile> v1 : r1 \<Longrightarrow> \<Turnstile> Left v1 : ALT r1 r2"
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	578	\| "\<Turnstile> v2 : r2 \<Longrightarrow> \<Turnstile> Right v2 : ALT r1 r2"
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	579	\| "\<Turnstile> Void : ONE"
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	580	\| "\<Turnstile> Char c : CHAR c"
265 d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	581	\| "\<forall>v \<in> set vs. \<Turnstile> v : r \<and> flat v \<noteq> [] \<Longrightarrow> \<Turnstile> Stars vs : STAR r"
248 b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	582
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	583	lemma Prf_CPrf:
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	584	assumes "\<Turnstile> v : r"
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	585	shows "\<turnstile> v : r"
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	586	using assms
265 d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	587	by (induct)(auto intro: Prf.intros)
256 146b4817aebd updated Christian Urban <urbanc@in.tum.de> parents: 255 diff changeset	588
254 7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	589	lemma CPrf_stars:
7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	590	assumes "\<Turnstile> Stars vs : STAR r"
7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	591	shows "\<forall>v \<in> set vs. flat v \<noteq> [] \<and> \<Turnstile> v : r"
7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	592	using assms
265 d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	593	apply(erule_tac CPrf.cases)
254 7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	594	apply(simp_all)
248 b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	595	done
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	596
254 7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	597	lemma CPrf_Stars_appendE:
7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	598	assumes "\<Turnstile> Stars (vs1 @ vs2) : STAR r"
7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	599	shows "\<Turnstile> Stars vs1 : STAR r \<and> \<Turnstile> Stars vs2 : STAR r"
7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	600	using assms
265 d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	601	apply(erule_tac CPrf.cases)
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	602	apply(auto intro: CPrf.intros elim: Prf.cases)
254 7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	603	done
7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	604
7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	605	definition PT :: "rexp \<Rightarrow> string \<Rightarrow> val set"
7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	606	where "PT r s \<equiv> {v. flat v = s \<and> \<turnstile> v : r}"
7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	607
248 b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	608	definition
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	609	"CPT r s = {v. flat v = s \<and> \<Turnstile> v : r}"
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	610
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	611	definition
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	612	"CPTpre r s = {v. \<exists>s'. flat v @ s' = s \<and> \<Turnstile> v : r}"
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	613
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	614	lemma CPT_CPTpre_subset:
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	615	shows "CPT r s \<subseteq> CPTpre r s"
254 7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	616	by(auto simp add: CPT_def CPTpre_def)
248 b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	617
265 d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	618	lemma CPT_simps:
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	619	shows "CPT ZERO s = {}"
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	620	and "CPT ONE s = (if s = [] then {Void} else {})"
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	621	and "CPT (CHAR c) s = (if s = [c] then {Char c} else {})"
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	622	and "CPT (ALT r1 r2) s = Left ` CPT r1 s \<union> Right ` CPT r2 s"
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	623	and "CPT (SEQ r1 r2) s =
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	624	{Seq v1 v2 \| v1 v2. flat v1 @ flat v2 = s \<and> v1 \<in> CPT r1 (flat v1) \<and> v2 \<in> CPT r2 (flat v2)}"
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	625	and "CPT (STAR r) s =
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	626	Stars ` {vs. concat (map flat vs) = s \<and> (\<forall>v \<in> set vs. v \<in> CPT r (flat v) \<and> flat v \<noteq> [])}"
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	627	apply -
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	628	apply(auto simp add: CPT_def intro: CPrf.intros)[1]
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	629	apply(erule CPrf.cases)
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	630	apply(simp_all)[6]
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	631	apply(auto simp add: CPT_def intro: CPrf.intros)[1]
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	632	apply(erule CPrf.cases)
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	633	apply(simp_all)[6]
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	634	apply(erule CPrf.cases)
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	635	apply(simp_all)[6]
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	636	apply(auto simp add: CPT_def intro: CPrf.intros)[1]
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	637	apply(erule CPrf.cases)
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	638	apply(simp_all)[6]
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	639	apply(erule CPrf.cases)
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	640	apply(simp_all)[6]
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	641	apply(auto simp add: CPT_def intro: CPrf.intros)[1]
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	642	apply(erule CPrf.cases)
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	643	apply(simp_all)[6]
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	644	apply(auto simp add: CPT_def intro: CPrf.intros)[1]
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	645	apply(erule CPrf.cases)
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	646	apply(simp_all)[6]
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	647	(* STAR case *)
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	648	apply(auto simp add: CPT_def intro: CPrf.intros)[1]
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	649	apply(erule CPrf.cases)
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	650	apply(simp_all)[6]
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	651	done
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	652
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	653	(*
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	654	lemma CPTpre_STAR_finite:
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	655	assumes "\<And>s. finite (CPT r s)"
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	656	shows "finite (CPT (STAR r) s)"
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	657	apply(induct s rule: length_induct)
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	658	apply(case_tac xs)
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	659	apply(simp)
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	660	apply(simp add: CPT_simps)
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	661	apply(auto)
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	662	apply(rule finite_imageI)
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	663	using assms
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	664	thm finite_Un
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	665	prefer 2
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	666	apply(simp add: CPT_simps)
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	667	apply(rule finite_imageI)
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	668	apply(rule finite_subset)
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	669	apply(rule CPTpre_subsets)
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	670	apply(simp)
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	671	apply(rule_tac B="(\<lambda>(v, vs). Stars (v#vs)) ` {(v, vs). v \<in> CPTpre r (a#list) \<and> flat v \<noteq> [] \<and> Stars vs \<in> CPTpre (STAR r) (drop (length (flat v)) (a#list))}" in finite_subset)
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	672	apply(auto)[1]
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	673	apply(rule finite_imageI)
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	674	apply(simp add: Collect_case_prod_Sigma)
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	675	apply(rule finite_SigmaI)
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	676	apply(rule assms)
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	677	apply(case_tac "flat v = []")
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	678	apply(simp)
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	679	apply(drule_tac x="drop (length (flat v)) (a # list)" in spec)
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	680	apply(simp)
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	681	apply(auto)[1]
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	682	apply(rule test)
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	683	apply(simp)
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	684	done
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	685
248 b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	686	lemma CPTpre_subsets:
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	687	"CPTpre ZERO s = {}"
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	688	"CPTpre ONE s \<subseteq> {Void}"
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	689	"CPTpre (CHAR c) s \<subseteq> {Char c}"
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	690	"CPTpre (ALT r1 r2) s \<subseteq> Left ` CPTpre r1 s \<union> Right ` CPTpre r2 s"
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	691	"CPTpre (SEQ r1 r2) s \<subseteq> {Seq v1 v2 \| v1 v2. v1 \<in> CPTpre r1 s \<and> v2 \<in> CPTpre r2 (drop (length (flat v1)) s)}"
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	692	"CPTpre (STAR r) s \<subseteq> {Stars []} \<union>
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	693	{Stars (v#vs) \| v vs. v \<in> CPTpre r s \<and> flat v \<noteq> [] \<and> Stars vs \<in> CPTpre (STAR r) (drop (length (flat v)) s)}"
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	694	"CPTpre (STAR r) [] = {Stars []}"
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	695	apply(auto simp add: CPTpre_def)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	696	apply(erule CPrf.cases)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	697	apply(simp_all)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	698	apply(erule CPrf.cases)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	699	apply(simp_all)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	700	apply(erule CPrf.cases)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	701	apply(simp_all)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	702	apply(erule CPrf.cases)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	703	apply(simp_all)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	704	apply(erule CPrf.cases)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	705	apply(simp_all)
265 d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	706
248 b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	707	apply(erule CPrf.cases)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	708	apply(simp_all)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	709	apply(erule CPrf.cases)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	710	apply(simp_all)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	711	apply(rule CPrf.intros)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	712	done
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	713
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	714
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	715	lemma CPTpre_simps:
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	716	shows "CPTpre ONE s = {Void}"
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	717	and "CPTpre (CHAR c) (d#s) = (if c = d then {Char c} else {})"
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	718	and "CPTpre (ALT r1 r2) s = Left ` CPTpre r1 s \<union> Right ` CPTpre r2 s"
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	719	and "CPTpre (SEQ r1 r2) s =
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	720	{Seq v1 v2 \| v1 v2. v1 \<in> CPTpre r1 s \<and> v2 \<in> CPTpre r2 (drop (length (flat v1)) s)}"
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	721	apply -
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	722	apply(rule subset_antisym)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	723	apply(rule CPTpre_subsets)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	724	apply(auto simp add: CPTpre_def intro: "CPrf.intros")[1]
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	725	apply(case_tac "c = d")
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	726	apply(simp)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	727	apply(rule subset_antisym)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	728	apply(rule CPTpre_subsets)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	729	apply(auto simp add: CPTpre_def intro: CPrf.intros)[1]
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	730	apply(simp)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	731	apply(auto simp add: CPTpre_def intro: CPrf.intros)[1]
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	732	apply(erule CPrf.cases)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	733	apply(simp_all)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	734	apply(rule subset_antisym)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	735	apply(rule CPTpre_subsets)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	736	apply(auto simp add: CPTpre_def intro: CPrf.intros)[1]
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	737	apply(rule subset_antisym)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	738	apply(rule CPTpre_subsets)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	739	apply(auto simp add: CPTpre_def intro: CPrf.intros)[1]
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	740	done
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	741
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	742	lemma CPT_simps:
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	743	shows "CPT ONE s = (if s = [] then {Void} else {})"
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	744	and "CPT (CHAR c) [d] = (if c = d then {Char c} else {})"
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	745	and "CPT (ALT r1 r2) s = Left ` CPT r1 s \<union> Right ` CPT r2 s"
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	746	and "CPT (SEQ r1 r2) s =
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	747	{Seq v1 v2 \| v1 v2 s1 s2. s1 @ s2 = s \<and> v1 \<in> CPT r1 s1 \<and> v2 \<in> CPT r2 s2}"
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	748	apply -
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	749	apply(rule subset_antisym)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	750	apply(auto simp add: CPT_def)[1]
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	751	apply(erule CPrf.cases)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	752	apply(simp_all)[7]
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	753	apply(erule CPrf.cases)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	754	apply(simp_all)[7]
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	755	apply(auto simp add: CPT_def intro: CPrf.intros)[1]
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	756	apply(auto simp add: CPT_def intro: CPrf.intros)[1]
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	757	apply(erule CPrf.cases)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	758	apply(simp_all)[7]
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	759	apply(erule CPrf.cases)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	760	apply(simp_all)[7]
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	761	apply(auto simp add: CPT_def image_def intro: CPrf.intros)[1]
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	762	apply(erule CPrf.cases)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	763	apply(simp_all)[7]
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	764	apply(clarify)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	765	apply blast
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	766	apply(auto simp add: CPT_def image_def intro: CPrf.intros)[1]
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	767	apply(erule CPrf.cases)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	768	apply(simp_all)[7]
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	769	done
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	770
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	771	lemma test:
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	772	assumes "finite A"
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	773	shows "finite {vs. Stars vs \<in> A}"
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	774	using assms
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	775	apply(induct A)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	776	apply(simp)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	777	apply(auto)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	778	apply(case_tac x)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	779	apply(simp_all)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	780	done
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	781
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	782	lemma CPTpre_STAR_finite:
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	783	assumes "\<And>s. finite (CPTpre r s)"
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	784	shows "finite (CPTpre (STAR r) s)"
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	785	apply(induct s rule: length_induct)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	786	apply(case_tac xs)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	787	apply(simp)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	788	apply(simp add: CPTpre_subsets)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	789	apply(rule finite_subset)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	790	apply(rule CPTpre_subsets)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	791	apply(simp)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	792	apply(rule_tac B="(\<lambda>(v, vs). Stars (v#vs)) ` {(v, vs). v \<in> CPTpre r (a#list) \<and> flat v \<noteq> [] \<and> Stars vs \<in> CPTpre (STAR r) (drop (length (flat v)) (a#list))}" in finite_subset)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	793	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	794	apply(rule finite_imageI)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	795	apply(simp add: Collect_case_prod_Sigma)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	796	apply(rule finite_SigmaI)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	797	apply(rule assms)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	798	apply(case_tac "flat v = []")
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	799	apply(simp)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	800	apply(drule_tac x="drop (length (flat v)) (a # list)" in spec)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	801	apply(simp)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	802	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	803	apply(rule test)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	804	apply(simp)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	805	done
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	806
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	807	lemma CPTpre_finite:
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	808	shows "finite (CPTpre r s)"
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	809	apply(induct r arbitrary: s)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	810	apply(simp add: CPTpre_subsets)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	811	apply(rule finite_subset)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	812	apply(rule CPTpre_subsets)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	813	apply(simp)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	814	apply(rule finite_subset)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	815	apply(rule CPTpre_subsets)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	816	apply(simp)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	817	apply(rule finite_subset)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	818	apply(rule CPTpre_subsets)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	819	apply(rule_tac B="(\<lambda>(v1, v2). Seq v1 v2) ` {(v1, v2). v1 \<in> CPTpre r1 s \<and> v2 \<in> CPTpre r2 (drop (length (flat v1)) s)}" in finite_subset)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	820	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	821	apply(rule finite_imageI)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	822	apply(simp add: Collect_case_prod_Sigma)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	823	apply(rule finite_subset)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	824	apply(rule CPTpre_subsets)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	825	apply(simp)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	826	by (simp add: CPTpre_STAR_finite)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	827
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	828
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	829	lemma CPT_finite:
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	830	shows "finite (CPT r s)"
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	831	apply(rule finite_subset)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	832	apply(rule CPT_CPTpre_subset)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	833	apply(rule CPTpre_finite)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	834	done
265 d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	835	*)
248 b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	836
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	837	lemma Posix_CPT:
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	838	assumes "s \<in> r \<rightarrow> v"
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	839	shows "v \<in> CPT r s"
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	840	using assms
265 d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	841	apply(induct rule: Posix.induct)
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	842	apply(auto simp add: CPT_def intro: CPrf.intros elim: CPrf.cases)
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	843	apply(rotate_tac 5)
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	844	apply(erule CPrf.cases)
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	845	apply(simp_all)
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	846	apply(rule CPrf.intros)
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	847	apply(simp_all)
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	848	done
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	849
248 b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	850
261 247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	851	section {* The Posix Value is smaller than any other Value *}
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	852
262 45ad887fa6aa isar proofs Christian Urban <urbanc@in.tum.de> parents: 261 diff changeset	853
261 247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	854	lemma Posix_PosOrd:
262 45ad887fa6aa isar proofs Christian Urban <urbanc@in.tum.de> parents: 261 diff changeset	855	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	856	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	857	using assms
261 247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	858	proof (induct arbitrary: v2 rule: Posix.induct)
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	859	case (Posix_ONE v)
262 45ad887fa6aa isar proofs Christian Urban <urbanc@in.tum.de> parents: 261 diff changeset	860	have "v \<in> CPT ONE []" by fact
45ad887fa6aa isar proofs Christian Urban <urbanc@in.tum.de> parents: 261 diff changeset	861	then have "v = Void"
45ad887fa6aa isar proofs Christian Urban <urbanc@in.tum.de> parents: 261 diff changeset	862	by (simp add: CPT_simps)
261 247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	863	then show "Void :\<sqsubseteq>val v"
265 d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	864	by (simp add: PosOrd_ex_eq_def)
261 247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	865	next
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	866	case (Posix_CHAR c v)
262 45ad887fa6aa isar proofs Christian Urban <urbanc@in.tum.de> parents: 261 diff changeset	867	have "v \<in> CPT (CHAR c) [c]" by fact
45ad887fa6aa isar proofs Christian Urban <urbanc@in.tum.de> parents: 261 diff changeset	868	then have "v = Char c"
45ad887fa6aa isar proofs Christian Urban <urbanc@in.tum.de> parents: 261 diff changeset	869	by (simp add: CPT_simps)
261 247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	870	then show "Char c :\<sqsubseteq>val v"
265 d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	871	by (simp add: PosOrd_ex_eq_def)
261 247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	872	next
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	873	case (Posix_ALT1 s r1 v r2 v2)
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	874	have as1: "s \<in> r1 \<rightarrow> v" by fact
262 45ad887fa6aa isar proofs Christian Urban <urbanc@in.tum.de> parents: 261 diff changeset	875	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	876	have "v2 \<in> CPT (ALT r1 r2) s" by fact
45ad887fa6aa isar proofs Christian Urban <urbanc@in.tum.de> parents: 261 diff changeset	877	then have "\<Turnstile> v2 : ALT r1 r2" "flat v2 = s"
45ad887fa6aa isar proofs Christian Urban <urbanc@in.tum.de> parents: 261 diff changeset	878	by(auto simp add: CPT_def prefix_list_def)
261 247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	879	then consider
262 45ad887fa6aa isar proofs Christian Urban <urbanc@in.tum.de> parents: 261 diff changeset	880	(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	881	\| (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	882	by (auto elim: CPrf.cases)
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	883	then show "Left v :\<sqsubseteq>val v2"
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	884	proof(cases)
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	885	case (Left v3)
262 45ad887fa6aa isar proofs Christian Urban <urbanc@in.tum.de> parents: 261 diff changeset	886	have "v3 \<in> CPT r1 s" using Left(2,3)
45ad887fa6aa isar proofs Christian Urban <urbanc@in.tum.de> parents: 261 diff changeset	887	by (auto simp add: CPT_def prefix_list_def)
261 247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	888	with IH have "v :\<sqsubseteq>val v3" by simp
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	889	moreover
262 45ad887fa6aa isar proofs Christian Urban <urbanc@in.tum.de> parents: 261 diff changeset	890	have "flat v3 = flat v" using as1 Left(3)
45ad887fa6aa isar proofs Christian Urban <urbanc@in.tum.de> parents: 261 diff changeset	891	by (simp add: Posix1(2))
261 247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	892	ultimately have "Left v :\<sqsubseteq>val Left v3"
265 d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	893	by (simp add: PosOrd_ex_eq_def PosOrd_Left_eq)
261 247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	894	then show "Left v :\<sqsubseteq>val v2" unfolding Left .
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 (Right v3)
262 45ad887fa6aa isar proofs Christian Urban <urbanc@in.tum.de> parents: 261 diff changeset	897	have "flat v3 = flat v" using as1 Right(3)
45ad887fa6aa isar proofs Christian Urban <urbanc@in.tum.de> parents: 261 diff changeset	898	by (simp add: Posix1(2))
261 247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	899	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	900	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	901	then show "Left v :\<sqsubseteq>val v2" unfolding Right .
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	902	qed
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	903	next
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	904	case (Posix_ALT2 s r2 v r1 v2)
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	905	have as1: "s \<in> r2 \<rightarrow> v" by fact
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	906	have as2: "s \<notin> L r1" by fact
262 45ad887fa6aa isar proofs Christian Urban <urbanc@in.tum.de> parents: 261 diff changeset	907	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	908	have "v2 \<in> CPT (ALT r1 r2) s" by fact
45ad887fa6aa isar proofs Christian Urban <urbanc@in.tum.de> parents: 261 diff changeset	909	then have "\<Turnstile> v2 : ALT r1 r2" "flat v2 = s"
45ad887fa6aa isar proofs Christian Urban <urbanc@in.tum.de> parents: 261 diff changeset	910	by(auto simp add: CPT_def prefix_list_def)
261 247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	911	then consider
262 45ad887fa6aa isar proofs Christian Urban <urbanc@in.tum.de> parents: 261 diff changeset	912	(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	913	\| (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	914	by (auto elim: CPrf.cases)
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	915	then show "Right v :\<sqsubseteq>val v2"
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	916	proof (cases)
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	917	case (Right v3)
262 45ad887fa6aa isar proofs Christian Urban <urbanc@in.tum.de> parents: 261 diff changeset	918	have "v3 \<in> CPT r2 s" using Right(2,3)
45ad887fa6aa isar proofs Christian Urban <urbanc@in.tum.de> parents: 261 diff changeset	919	by (auto simp add: CPT_def prefix_list_def)
261 247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	920	with IH have "v :\<sqsubseteq>val v3" by simp
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	921	moreover
262 45ad887fa6aa isar proofs Christian Urban <urbanc@in.tum.de> parents: 261 diff changeset	922	have "flat v3 = flat v" using as1 Right(3)
45ad887fa6aa isar proofs Christian Urban <urbanc@in.tum.de> parents: 261 diff changeset	923	by (simp add: Posix1(2))
261 247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	924	ultimately have "Right v :\<sqsubseteq>val Right v3"
265 d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	925	by (auto simp add: PosOrd_ex_eq_def PosOrd_RightI)
261 247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	926	then show "Right v :\<sqsubseteq>val v2" unfolding Right .
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	927	next
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	928	case (Left v3)
262 45ad887fa6aa isar proofs Christian Urban <urbanc@in.tum.de> parents: 261 diff changeset	929	have "v3 \<in> CPT r1 s" using Left(2,3) as2
45ad887fa6aa isar proofs Christian Urban <urbanc@in.tum.de> parents: 261 diff changeset	930	by (auto simp add: CPT_def prefix_list_def)
45ad887fa6aa isar proofs Christian Urban <urbanc@in.tum.de> parents: 261 diff changeset	931	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	932	by (simp add: Posix1(2) CPT_def)
45ad887fa6aa isar proofs Christian Urban <urbanc@in.tum.de> parents: 261 diff changeset	933	then have "False" using as1 as2 Left
45ad887fa6aa isar proofs Christian Urban <urbanc@in.tum.de> parents: 261 diff changeset	934	by (auto simp add: Posix1(2) L_flat_Prf1 Prf_CPrf)
45ad887fa6aa isar proofs Christian Urban <urbanc@in.tum.de> parents: 261 diff changeset	935	then show "Right v :\<sqsubseteq>val v2" by simp
261 247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	936	qed
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	937	next
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	938	case (Posix_SEQ s1 r1 v1 s2 r2 v2 v3)
264 e2828c4a1e23 updated Christian Urban <urbanc@in.tum.de> parents: 263 diff changeset	939	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	940	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	941	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	942	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	943	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	944	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	945	then obtain v3a v3b where eqs:
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	946	"v3 = Seq v3a v3b" "\<Turnstile> v3a : r1" "\<Turnstile> v3b : r2"
262 45ad887fa6aa isar proofs Christian Urban <urbanc@in.tum.de> parents: 261 diff changeset	947	"flat v3a @ flat v3b = s1 @ s2"
45ad887fa6aa isar proofs Christian Urban <urbanc@in.tum.de> parents: 261 diff changeset	948	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	949	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	950	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	951	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	952	by (simp add: sprefix_list_def append_eq_conv_conj)
45ad887fa6aa isar proofs Christian Urban <urbanc@in.tum.de> parents: 261 diff changeset	953	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	954	using PosOrd_spreI as1(1) eqs by blast
262 45ad887fa6aa isar proofs Christian Urban <urbanc@in.tum.de> parents: 261 diff changeset	955	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	956	by (auto simp add: CPT_def)
45ad887fa6aa isar proofs Christian Urban <urbanc@in.tum.de> parents: 261 diff changeset	957	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	958	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	959	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	960	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	961	next
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	962	case (Posix_STAR1 s1 r v s2 vs v3)
264 e2828c4a1e23 updated Christian Urban <urbanc@in.tum.de> parents: 263 diff changeset	963	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	964	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	965	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	966	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	967	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	968	have cond2: "flat v \<noteq> []" by fact
262 45ad887fa6aa isar proofs Christian Urban <urbanc@in.tum.de> parents: 261 diff changeset	969	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	970	then consider
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	971	(NonEmpty) v3a vs3 where "v3 = Stars (v3a # vs3)"
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	972	"\<Turnstile> v3a : r" "\<Turnstile> Stars vs3 : STAR r"
262 45ad887fa6aa isar proofs Christian Urban <urbanc@in.tum.de> parents: 261 diff changeset	973	"flat (Stars (v3a # vs3)) = s1 @ s2"
261 247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	974	\| (Empty) "v3 = Stars []"
265 d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	975	unfolding CPT_def
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	976	apply(auto)
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	977	apply(erule CPrf.cases)
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	978	apply(simp_all)
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	979	apply(auto)[1]
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	980	apply(case_tac vs)
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	981	apply(auto)
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	982	using CPrf.intros(6) by blast
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	983	then show "Stars (v # vs) :\<sqsubseteq>val v3" (* HERE *)
261 247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	984	proof (cases)
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	985	case (NonEmpty v3a vs3)
262 45ad887fa6aa isar proofs Christian Urban <urbanc@in.tum.de> parents: 261 diff changeset	986	have "flat (Stars (v3a # vs3)) = s1 @ s2" using NonEmpty(4) .
45ad887fa6aa isar proofs Christian Urban <urbanc@in.tum.de> parents: 261 diff changeset	987	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	988	unfolding prefix_list_def
45ad887fa6aa isar proofs Christian Urban <urbanc@in.tum.de> parents: 261 diff changeset	989	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	990	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	991	by (simp add: sprefix_list_def append_eq_conv_conj)
45ad887fa6aa isar proofs Christian Urban <urbanc@in.tum.de> parents: 261 diff changeset	992	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	993	using PosOrd_spreI as1(1) NonEmpty(4) by blast
262 45ad887fa6aa isar proofs Christian Urban <urbanc@in.tum.de> parents: 261 diff changeset	994	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	995	using NonEmpty(2,3) by (auto simp add: CPT_def)
264 e2828c4a1e23 updated Christian Urban <urbanc@in.tum.de> parents: 263 diff changeset	996	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	997	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	998	unfolding PosOrd_ex_eq_def by auto
262 45ad887fa6aa isar proofs Christian Urban <urbanc@in.tum.de> parents: 261 diff changeset	999	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	1000	unfolding PosOrd_ex_eq_def
264 e2828c4a1e23 updated Christian Urban <urbanc@in.tum.de> parents: 263 diff changeset	1001	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	1002	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	1003	next
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	1004	case Empty
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	1005	have "v3 = Stars []" by fact
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	1006	then show "Stars (v # vs) :\<sqsubseteq>val v3"
265 d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	1007	unfolding PosOrd_ex_eq_def using cond2
261 247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	1008	by (simp add: PosOrd_shorterI)
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	1009	qed
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	1010	next
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	1011	case (Posix_STAR2 r v2)
262 45ad887fa6aa isar proofs Christian Urban <urbanc@in.tum.de> parents: 261 diff changeset	1012	have "v2 \<in> CPT (STAR r) []" by fact
45ad887fa6aa isar proofs Christian Urban <urbanc@in.tum.de> parents: 261 diff changeset	1013	then have "v2 = Stars []"
45ad887fa6aa isar proofs Christian Urban <urbanc@in.tum.de> parents: 261 diff changeset	1014	unfolding CPT_def by (auto elim: CPrf.cases)
261 247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	1015	then show "Stars [] :\<sqsubseteq>val v2"
265 d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	1016	by (simp add: PosOrd_ex_eq_def)
261 247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	1017	qed
253 ca4e9eb8d576 polished Christian Urban <urbanc@in.tum.de> parents: 252 diff changeset	1018
263 00c9a95d492e isar proofs Christian Urban <urbanc@in.tum.de> parents: 262 diff changeset	1019	lemma Posix_PosOrd_stronger:
00c9a95d492e isar proofs Christian Urban <urbanc@in.tum.de> parents: 262 diff changeset	1020	assumes "s \<in> r \<rightarrow> v1" "v2 \<in> CPTpre r s"
00c9a95d492e isar proofs Christian Urban <urbanc@in.tum.de> parents: 262 diff changeset	1021	shows "v1 :\<sqsubseteq>val v2"
00c9a95d492e isar proofs Christian Urban <urbanc@in.tum.de> parents: 262 diff changeset	1022	proof -
00c9a95d492e isar proofs Christian Urban <urbanc@in.tum.de> parents: 262 diff changeset	1023	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	1024	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	1025	moreover
00c9a95d492e isar proofs Christian Urban <urbanc@in.tum.de> parents: 262 diff changeset	1026	{ assume "v2 \<in> CPT r s"
264 e2828c4a1e23 updated Christian Urban <urbanc@in.tum.de> parents: 263 diff changeset	1027	with assms(1)
e2828c4a1e23 updated Christian Urban <urbanc@in.tum.de> parents: 263 diff changeset	1028	have "v1 :\<sqsubseteq>val v2" by (rule Posix_PosOrd)
263 00c9a95d492e isar proofs Christian Urban <urbanc@in.tum.de> parents: 262 diff changeset	1029	}
00c9a95d492e isar proofs Christian Urban <urbanc@in.tum.de> parents: 262 diff changeset	1030	moreover
00c9a95d492e isar proofs Christian Urban <urbanc@in.tum.de> parents: 262 diff changeset	1031	{ assume "flat v2 \<sqsubset>spre s"
00c9a95d492e isar proofs Christian Urban <urbanc@in.tum.de> parents: 262 diff changeset	1032	then have "flat v2 \<sqsubset>spre flat v1" using assms(1)
00c9a95d492e isar proofs Christian Urban <urbanc@in.tum.de> parents: 262 diff changeset	1033	using Posix1(2) by blast
00c9a95d492e isar proofs Christian Urban <urbanc@in.tum.de> parents: 262 diff changeset	1034	then have "v1 :\<sqsubseteq>val v2"
265 d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	1035	by (simp add: PosOrd_ex_eq_def PosOrd_spreI)
263 00c9a95d492e isar proofs Christian Urban <urbanc@in.tum.de> parents: 262 diff changeset	1036	}
00c9a95d492e isar proofs Christian Urban <urbanc@in.tum.de> parents: 262 diff changeset	1037	ultimately show "v1 :\<sqsubseteq>val v2" by blast
00c9a95d492e isar proofs Christian Urban <urbanc@in.tum.de> parents: 262 diff changeset	1038	qed
00c9a95d492e isar proofs Christian Urban <urbanc@in.tum.de> parents: 262 diff changeset	1039
261 247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	1040	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	1041	assumes "s \<in> r \<rightarrow> v1"
263 00c9a95d492e isar proofs Christian Urban <urbanc@in.tum.de> parents: 262 diff changeset	1042	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	1043	using assms
263 00c9a95d492e isar proofs Christian Urban <urbanc@in.tum.de> parents: 262 diff changeset	1044	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	1045	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	1046
265 d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	1047	(*
261 247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	1048	lemma PosOrd_Posix_Stars:
248 b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	1049	assumes "(Stars vs) \<in> CPT (STAR r) (flat (Stars vs))" "\<forall>v \<in> set vs. flat v \<in> r \<rightarrow> v"
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	1050	and "\<not>(\<exists>vs2 \<in> PT (STAR r) (flat (Stars vs)). vs2 :\<sqsubset>val (Stars vs))"
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	1051	shows "(flat (Stars vs)) \<in> (STAR r) \<rightarrow> Stars vs"
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	1052	using assms
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	1053	apply(induct vs)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	1054	apply(simp)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	1055	apply(rule Posix.intros)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	1056	apply(simp (no_asm))
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	1057	apply(rule Posix.intros)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	1058	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	1059	apply(auto simp add: CPT_def PT_def)[1]
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	1060	defer
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	1061	apply(simp)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	1062	apply(drule meta_mp)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	1063	apply(auto simp add: CPT_def PT_def)[1]
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	1064	apply(erule CPrf.cases)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	1065	apply(simp_all)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	1066	apply(drule meta_mp)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	1067	apply(auto simp add: CPT_def PT_def)[1]
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	1068	apply(erule Prf.cases)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	1069	apply(simp_all)
264 e2828c4a1e23 updated Christian Urban <urbanc@in.tum.de> parents: 263 diff changeset	1070	using CPrf_stars PosOrd_irrefl apply fastforce
248 b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	1071	apply(clarify)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	1072	apply(drule_tac x="Stars (a#v#vsa)" in spec)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	1073	apply(simp)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	1074	apply(drule mp)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	1075	apply (meson CPrf_stars Prf.intros(7) Prf_CPrf list.set_intros(1))
261 247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	1076	apply(subst (asm) (2) 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	1077	apply(simp)
261 247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	1078	apply (metis flat.simps(7) flat_Stars PosOrd_StarsI2 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	1079	apply(auto simp add: CPT_def PT_def)[1]
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	1080	using CPrf_stars 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	1081	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	1082	apply(auto simp add: CPT_def PT_def)[1]
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	1083	apply(subgoal_tac "\<exists>vA. flat vA = flat a @ s\<^sub>3 \<and> \<turnstile> vA : r")
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	1084	prefer 2
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	1085	apply (meson L_flat_Prf2)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	1086	apply(subgoal_tac "\<exists>vB. flat (Stars vB) = s\<^sub>4 \<and> \<turnstile> (Stars vB) : (STAR r)")
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	1087	apply(clarify)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	1088	apply(drule_tac x="Stars (vA # vB)" in spec)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	1089	apply(simp)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	1090	apply(drule mp)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	1091	using Prf.intros(7) apply blast
261 247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	1092	apply(subst (asm) (2) 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	1093	apply(simp)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	1094	prefer 2
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	1095	apply(simp)
254 7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	1096	using Star_values_exists apply blast
248 b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	1097	prefer 2
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	1098	apply(drule meta_mp)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	1099	apply(erule CPrf.cases)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	1100	apply(simp_all)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	1101	apply(drule meta_mp)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	1102	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	1103	prefer 2
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	1104	apply(simp)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	1105	apply(erule CPrf.cases)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	1106	apply(simp_all)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	1107	apply(clarify)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	1108	apply(rotate_tac 3)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	1109	apply(erule Prf.cases)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	1110	apply(simp_all)
261 247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	1111	apply (metis CPrf_stars intlen.cases less_irrefl list.set_intros(1) PosOrd_def 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	1112	apply(drule_tac x="Stars (v#va#vsb)" in spec)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	1113	apply(drule mp)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	1114	apply (simp add: Posix1a Prf.intros(7))
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	1115	apply(simp)
261 247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	1116	apply(subst (asm) (2) 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	1117	apply(simp)
261 247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	1118	apply (metis flat.simps(7) flat_Stars PosOrd_StarsI2 PosOrd_ex_def)
264 e2828c4a1e23 updated Christian Urban <urbanc@in.tum.de> parents: 263 diff changeset	1119	by (metis PosOrd_StarsI PosOrd_ex_def PosOrd_spreI append_assoc append_self_conv flat.simps(7) flat_Stars prefix_list_def sprefix_list_def)
265 d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	1120	*)
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	1121
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	1122
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	1123	lemma test2:
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	1124	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	1125	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	1126	using assms
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	1127	apply(induct vs)
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	1128	apply(auto simp add: CPT_def)
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	1129	apply(rule CPrf.intros)
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	1130	apply(simp)
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	1131	apply(rule CPrf.intros)
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	1132	apply(simp_all)
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	1133	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	1134
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	1135
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	1136	lemma PosOrd_Posix_Stars:
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	1137	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	1138	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	1139	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	1140	using assms
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	1141	proof(induct vs)
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	1142	case Nil
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	1143	show "flat (Stars []) \<in> STAR r \<rightarrow> Stars []"
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	1144	by(simp add: Posix.intros)
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	1145	next
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	1146	case (Cons v vs)
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	1147	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	1148	\<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	1149	\<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	1150	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	1151	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	1152	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	1153	moreover
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	1154	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	1155	proof (rule IH)
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	1156	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	1157	next
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	1158	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	1159	apply(auto)
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	1160	apply(subst (asm) (2) PT_def)
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	1161	apply(auto)
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	1162	apply(erule Prf.cases)
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	1163	apply(simp_all)
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	1164	apply(drule_tac x="Stars (v # vs)" in bspec)
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	1165	apply(simp add: PT_def CPT_def)
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	1166	using Posix1a Prf.intros(6) calculation
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	1167	apply(rule_tac Prf.intros)
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	1168	apply(simp add:)
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	1169	apply (simp add: PosOrd_StarsI2)
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	1170	done
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	1171	qed
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	1172	moreover
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	1173	have "flat v \<noteq> []" using as2 by simp
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	1174	moreover
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	1175	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	1176	using as3
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	1177	apply(auto)
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	1178	apply(drule L_flat_Prf2)
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	1179	apply(erule exE)
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	1180	apply(simp only: L.simps[symmetric])
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	1181	apply(drule L_flat_Prf2)
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	1182	apply(erule exE)
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	1183	apply(clarify)
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	1184	apply(rotate_tac 5)
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	1185	apply(erule Prf.cases)
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	1186	apply(simp_all)
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	1187	apply(clarify)
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	1188	apply(drule_tac x="Stars (va#vs)" in bspec)
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	1189	apply(auto simp add: PT_def)[1]
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	1190	apply(rule Prf.intros)
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	1191	apply(simp)
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	1192	by (simp add: PosOrd_StarsI PosOrd_shorterI)
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	1193	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	1194	by (simp add: Posix.intros)
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	1195	qed
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	1196
248 b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	1197
254 7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	1198
261 247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	1199	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	1200
265 d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	1201	text {*
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	1202	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	1203	*}
d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	1204
261 247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	1205	lemma PosOrd_Posix:
265 d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	1206	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	1207	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	1208	using assms
261 247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	1209	proof(induct r arbitrary: s v1)
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	1210	case (ZERO s v1)
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	1211	have "v1 \<in> CPT ZERO s" by fact
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	1212	then show "s \<in> ZERO \<rightarrow> v1" unfolding CPT_def
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	1213	by (auto elim: CPrf.cases)
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	1214	next
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	1215	case (ONE s v1)
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	1216	have "v1 \<in> CPT ONE s" by fact
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	1217	then show "s \<in> ONE \<rightarrow> v1" unfolding CPT_def
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	1218	by(auto elim!: CPrf.cases intro: Posix.intros)
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	1219	next
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	1220	case (CHAR c s v1)
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	1221	have "v1 \<in> CPT (CHAR c) s" by fact
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	1222	then show "s \<in> CHAR c \<rightarrow> v1" unfolding CPT_def
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	1223	by (auto elim!: CPrf.cases intro: Posix.intros)
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	1224	next
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	1225	case (ALT r1 r2 s v1)
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	1226	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	1227	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	1228	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	1229	have as2: "v1 \<in> CPT (ALT r1 r2) s" by fact
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	1230	then consider
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	1231	(Left) v1' where
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	1232	"v1 = Left v1'" "s = flat v1'"
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	1233	"v1' \<in> CPT r1 s"
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	1234	\| (Right) v1' where
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	1235	"v1 = Right v1'" "s = flat v1'"
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	1236	"v1' \<in> CPT r2 s"
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	1237	unfolding CPT_def by (auto elim: CPrf.cases)
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	1238	then show "s \<in> ALT r1 r2 \<rightarrow> v1"
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	1239	proof (cases)
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	1240	case (Left v1')
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	1241	have "v1' \<in> CPT r1 s" using as2
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	1242	unfolding CPT_def Left by (auto elim: CPrf.cases)
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	1243	moreover
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	1244	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	1245	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	1246	ultimately have "s \<in> r1 \<rightarrow> v1'" using IH1 by simp
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	1247	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	1248	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	1249	next
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	1250	case (Right v1')
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	1251	have "v1' \<in> CPT r2 s" using as2
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	1252	unfolding CPT_def Right by (auto elim: CPrf.cases)
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	1253	moreover
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	1254	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	1255	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	1256	ultimately have "s \<in> r2 \<rightarrow> v1'" using IH2 by simp
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	1257	moreover
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	1258	{ assume "s \<in> L r1"
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	1259	then obtain v' where "v' \<in> PT r1 s"
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	1260	unfolding PT_def using L_flat_Prf2 by blast
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	1261	then have "Left v' \<in> PT (ALT r1 r2) s"
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	1262	unfolding PT_def by (auto intro: Prf.intros)
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	1263	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	1264	unfolding PT_def Right by (auto)
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	1265	then have False using PosOrd_Left_Right Right by blast
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	1266	}
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	1267	then have "s \<notin> L r1" by rule
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	1268	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	1269	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	1270	qed
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	1271	next
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	1272	case (SEQ r1 r2 s v1)
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	1273	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	1274	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	1275	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	1276	have as2: "v1 \<in> CPT (SEQ r1 r2) s" by fact
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	1277	then obtain
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	1278	v1a v1b where eqs:
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	1279	"v1 = Seq v1a v1b" "s = flat v1a @ flat v1b"
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	1280	"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	1281	unfolding CPT_def by(auto elim: CPrf.cases)
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	1282	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	1283	proof
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	1284	fix v2
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	1285	assume "v2 \<in> PT r1 (flat v1a)"
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	1286	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	1287	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	1288	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	1289	using eqs by (simp add: PT_def)
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	1290	then show "\<not> v2 :\<sqsubset>val v1a"
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	1291	using PosOrd_SeqI1 by blast
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	1292	qed
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	1293	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	1294	moreover
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	1295	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	1296	proof
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	1297	fix v2
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	1298	assume "v2 \<in> PT r2 (flat v1b)"
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	1299	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	1300	by (simp add: CPT_def PT_def Prf.intros Prf_CPrf)
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	1301	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	1302	using eqs by (simp add: PT_def)
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	1303	then show "\<not> v2 :\<sqsubset>val v1b"
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	1304	using PosOrd_SeqI2 by auto
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	1305	qed
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	1306	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	1307	moreover
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	1308	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	1309	proof
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	1310	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	1311	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	1312	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	1313	using L_flat_Prf2 by blast
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	1314	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	1315	by (auto simp add: PT_def intro: Prf.intros)
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	1316	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	1317	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	1318	then show "False"
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	1319	using PosOrd_shorterI by blast
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	1320	qed
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	1321	ultimately
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	1322	show "s \<in> SEQ r1 r2 \<rightarrow> v1" unfolding eqs
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	1323	by (rule Posix.intros)
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	1324	next
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	1325	case (STAR r s v1)
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	1326	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	1327	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	1328	have as2: "v1 \<in> CPT (STAR r) s" by fact
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	1329	then obtain
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	1330	vs where eqs:
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	1331	"v1 = Stars vs" "s = flat (Stars vs)"
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	1332	"\<forall>v \<in> set vs. v \<in> CPT r (flat v)"
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	1333	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	1334	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	1335	proof
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	1336	fix v
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	1337	assume a: "v \<in> set vs"
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	1338	then obtain pre post where e: "vs = pre @ [v] @ post"
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	1339	by (metis append_Cons append_Nil in_set_conv_decomp_first)
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	1340	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	1341	using as1 unfolding eqs by simp
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	1342	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	1343	proof (rule ballI, rule notI)
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	1344	fix v2
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	1345	assume w: "v2 :\<sqsubset>val v"
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	1346	assume "v2 \<in> PT r (flat v)"
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	1347	then have "Stars (pre @ [v2] @ post) \<in> PT (STAR r) s"
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	1348	using as2 unfolding e eqs
265 d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	1349	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	1350	using CPrf_Stars_appendE CPrf_stars Prf_CPrf apply blast
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	1351	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	1352	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	1353	using q by simp
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	1354	with w show "False"
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	1355	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	1356	PosOrd_StarsI PosOrd_Stars_appendI by auto
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	1357	qed
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	1358	with IH
265 d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	1359	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	1360	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	1361	qed
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	1362	moreover
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	1363	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	1364	proof
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	1365	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	1366	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	1367	"Stars vs2 :\<sqsubset>val Stars vs"
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	1368	unfolding PT_def
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	1369	apply(auto elim: Prf.cases)
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	1370	apply(erule Prf.cases)
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	1371	apply(auto intro: Prf.intros)
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	1372	done
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	1373	then show "False" using as1 unfolding eqs
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	1374	apply -
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	1375	apply(drule_tac x="Stars vs2" in bspec)
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	1376	apply(auto simp add: PT_def)
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	1377	done
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	1378	qed
265 d36be1e356c0 changed definitions of PRF Christian Urban <urbanc@in.tum.de> parents: 264 diff changeset	1379	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	1380	thm PosOrd_Posix_Stars
261 247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	1381	by (rule PosOrd_Posix_Stars)
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	1382	then show "s \<in> STAR r \<rightarrow> v1" unfolding eqs .
247fc5dd4943 isar proofs Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	1383	qed
248 b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	1384
249 256484ef4be4 updated Christian Urban <urbanc@in.tum.de> parents: 248 diff changeset	1385	unused_thms
256484ef4be4 updated Christian Urban <urbanc@in.tum.de> parents: 248 diff changeset	1386
248 b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	1387	end

author	Christian Urban <urbanc@in.tum.de>
	Tue, 18 Jul 2017 18:39:20 +0100
changeset 265	d36be1e356c0
parent 264	e2828c4a1e23
child 266	fff2e1b40dfc
permissions	-rw-r--r--