lexing: thys/Positions.thy@7c89d3f6923e (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
254 7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	6
7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	7	section {* Position in values *}
7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	8
248 b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	9	fun
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	10	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	11	where
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	12	"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	13	\| "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	14	\| "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	15	\| "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	16	\| "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	17	\| "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	18
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	19	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	20	where
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	21	"Pos (Void) = {[]}"
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	22	\| "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	23	\| "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	24	\| "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	25	\| "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	26	\| "Pos (Stars []) = {[]}"
251 925232418a15 polished Christian Urban <urbanc@in.tum.de> parents: 250 diff changeset	27	\| "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	28
253 ca4e9eb8d576 polished Christian Urban <urbanc@in.tum.de> parents: 252 diff changeset	29	lemma Pos_stars:
ca4e9eb8d576 polished Christian Urban <urbanc@in.tum.de> parents: 252 diff changeset	30	"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	31	apply(induct vs)
ca4e9eb8d576 polished Christian Urban <urbanc@in.tum.de> parents: 252 diff changeset	32	apply(simp)
ca4e9eb8d576 polished Christian Urban <urbanc@in.tum.de> parents: 252 diff changeset	33	apply(simp)
ca4e9eb8d576 polished Christian Urban <urbanc@in.tum.de> parents: 252 diff changeset	34	apply(simp add: insert_ident)
ca4e9eb8d576 polished Christian Urban <urbanc@in.tum.de> parents: 252 diff changeset	35	apply(rule subset_antisym)
ca4e9eb8d576 polished Christian Urban <urbanc@in.tum.de> parents: 252 diff changeset	36	apply(auto)
ca4e9eb8d576 polished Christian Urban <urbanc@in.tum.de> parents: 252 diff changeset	37	apply(auto)[1]
ca4e9eb8d576 polished Christian Urban <urbanc@in.tum.de> parents: 252 diff changeset	38	using less_Suc_eq_0_disj by auto
ca4e9eb8d576 polished Christian Urban <urbanc@in.tum.de> parents: 252 diff changeset	39
248 b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	40	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	41	shows "[] \<in> Pos v"
251 925232418a15 polished Christian Urban <urbanc@in.tum.de> parents: 250 diff changeset	42	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	43
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	44	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	45	where
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	46	"intlen [] = 0"
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	47	\| "intlen (x#xs) = 1 + intlen xs"
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	48
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	49	lemma inlen_bigger:
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	50	shows "0 \<le> intlen xs"
251 925232418a15 polished Christian Urban <urbanc@in.tum.de> parents: 250 diff changeset	51	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	52
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	53	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	54	shows "intlen (xs @ ys) = intlen xs + intlen ys"
251 925232418a15 polished Christian Urban <urbanc@in.tum.de> parents: 250 diff changeset	55	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	56
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	57	lemma intlen_length:
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	58	assumes "length xs < length ys"
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	59	shows "intlen xs < intlen ys"
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	60	using assms
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	61	apply(induct xs arbitrary: ys)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	62	apply(auto)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	63	apply(case_tac ys)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	64	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	65	apply (smt inlen_bigger)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	66	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	67
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	68
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	69	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	70	where
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	71	"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	72
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	73	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	74	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	75	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	76	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	77	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	78	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	79	and "pflat_len (Right v) (0#p) = -1"
251 925232418a15 polished Christian Urban <urbanc@in.tum.de> parents: 250 diff changeset	80	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	81	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	82	and "pflat_len v [] = intlen (flat v)"
251 925232418a15 polished Christian Urban <urbanc@in.tum.de> parents: 250 diff changeset	83	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	84
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	85	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	86	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	87	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	88	using assms
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	89	apply(induct vs arbitrary: n p)
251 925232418a15 polished Christian Urban <urbanc@in.tum.de> parents: 250 diff changeset	90	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	91	done
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	92
254 7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	93	lemma outside_lemma:
7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	94	assumes "p \<notin> Pos v1 \<union> Pos v2"
7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	95	shows "pflat_len v1 p = pflat_len v2 p"
7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	96	using assms by (auto simp add: pflat_len_def)
252 022b80503766 polished Christian Urban <urbanc@in.tum.de> parents: 251 diff changeset	97
022b80503766 polished Christian Urban <urbanc@in.tum.de> parents: 251 diff changeset	98
022b80503766 polished Christian Urban <urbanc@in.tum.de> parents: 251 diff changeset	99	section {* Orderings *}
022b80503766 polished Christian Urban <urbanc@in.tum.de> parents: 251 diff changeset	100
022b80503766 polished Christian Urban <urbanc@in.tum.de> parents: 251 diff changeset	101
248 b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	102	definition prefix_list:: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" ("_ \<sqsubseteq>pre _")
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	103	where
252 022b80503766 polished Christian Urban <urbanc@in.tum.de> parents: 251 diff changeset	104	"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	105
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	106	definition sprefix_list:: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" ("_ \<sqsubset>spre _")
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	107	where
252 022b80503766 polished Christian Urban <urbanc@in.tum.de> parents: 251 diff changeset	108	"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	109
251 925232418a15 polished Christian Urban <urbanc@in.tum.de> parents: 250 diff changeset	110	inductive lex_list :: "nat list \<Rightarrow> nat list \<Rightarrow> bool" ("_ \<sqsubset>lex _")
248 b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	111	where
252 022b80503766 polished Christian Urban <urbanc@in.tum.de> parents: 251 diff changeset	112	"[] \<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	113	\| "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	114	\| "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	115
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	116	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	117	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	118	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	119	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	120	using assms
251 925232418a15 polished Christian Urban <urbanc@in.tum.de> parents: 250 diff changeset	121	apply(induct rule: lex_list.induct)
248 b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	122	apply(auto)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	123	done
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	124
251 925232418a15 polished Christian Urban <urbanc@in.tum.de> parents: 250 diff changeset	125	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	126	fixes xs ys :: "nat list"
251 925232418a15 polished Christian Urban <urbanc@in.tum.de> parents: 250 diff changeset	127	shows "[] \<sqsubset>lex ys \<longleftrightarrow> ys \<noteq> []"
925232418a15 polished Christian Urban <urbanc@in.tum.de> parents: 250 diff changeset	128	and "xs \<sqsubset>lex [] \<longleftrightarrow> False"
248 b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	129	and "(x # xs) \<sqsubset>lex (y # ys) \<longleftrightarrow> (x < y \<or> (\<not> y < x \<and> xs \<sqsubset>lex ys))"
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	130	apply -
251 925232418a15 polished Christian Urban <urbanc@in.tum.de> parents: 250 diff changeset	131	apply (metis lex_irrfl lex_list.intros(1) list.exhaust)
925232418a15 polished Christian Urban <urbanc@in.tum.de> parents: 250 diff changeset	132	using lex_list.cases apply blast
925232418a15 polished Christian Urban <urbanc@in.tum.de> parents: 250 diff changeset	133	using lex_list.cases lex_list.intros(2) lex_list.intros(3) not_less_iff_gr_or_eq by fastforce
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
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	136	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	137	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	138	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	139	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	140	using assms
251 925232418a15 polished Christian Urban <urbanc@in.tum.de> parents: 250 diff changeset	141	apply(induct arbitrary: ps3 rule: lex_list.induct)
925232418a15 polished Christian Urban <urbanc@in.tum.de> parents: 250 diff changeset	142	apply(erule 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	143	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	144	apply(rotate_tac 2)
251 925232418a15 polished Christian Urban <urbanc@in.tum.de> parents: 250 diff changeset	145	apply(erule 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	146	apply(simp_all)
251 925232418a15 polished Christian Urban <urbanc@in.tum.de> parents: 250 diff changeset	147	apply(erule 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	148	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	149	done
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	150
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	151
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	152	lemma trichotomous:
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	153	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	154	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	155	apply(induct p arbitrary: q)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	156	apply(auto)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	157	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	158	apply(auto)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	159	done
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	160
254 7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	161
7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	162
7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	163
7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	164	section {* Ordering of values according to Okui & Suzuki *}
7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	165
248 b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	166
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	167	definition val_ord:: "val \<Rightarrow> nat list \<Rightarrow> val \<Rightarrow> bool" ("_ \<sqsubset>val _ _")
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	168	where
254 7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	169	"v1 \<sqsubset>val p v2 \<equiv> (p \<in> Pos v1 \<and>
7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	170	pflat_len v1 p > pflat_len v2 p \<and>
248 b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	171	(\<forall>q \<in> Pos v1 \<union> Pos v2. q \<sqsubset>lex p \<longrightarrow> pflat_len v1 q = pflat_len v2 q))"
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	172
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	173
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	174	definition val_ord_ex:: "val \<Rightarrow> val \<Rightarrow> bool" ("_ :\<sqsubset>val _")
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	175	where
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	176	"v1 :\<sqsubset>val v2 \<equiv> (\<exists>p. v1 \<sqsubset>val p v2)"
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	177
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	178	definition val_ord_ex1:: "val \<Rightarrow> val \<Rightarrow> bool" ("_ :\<sqsubseteq>val _")
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	179	where
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	180	"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	181
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	182	lemma val_ord_shorterI:
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	183	assumes "length (flat v') < length (flat v)"
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	184	shows "v :\<sqsubset>val v'"
251 925232418a15 polished Christian Urban <urbanc@in.tum.de> parents: 250 diff changeset	185	using assms
925232418a15 polished Christian Urban <urbanc@in.tum.de> parents: 250 diff changeset	186	unfolding val_ord_ex_def
925232418a15 polished Christian Urban <urbanc@in.tum.de> parents: 250 diff changeset	187	by (metis Pos_empty intlen_length lex_simps(2) pflat_len_simps(9) val_ord_def)
248 b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	188
251 925232418a15 polished Christian Urban <urbanc@in.tum.de> parents: 250 diff changeset	189	lemma val_ord_spreI:
248 b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	190	assumes "(flat v') \<sqsubset>spre (flat v)"
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	191	shows "v :\<sqsubset>val v'"
251 925232418a15 polished Christian Urban <urbanc@in.tum.de> parents: 250 diff changeset	192	using assms
248 b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	193	apply(rule_tac val_ord_shorterI)
251 925232418a15 polished Christian Urban <urbanc@in.tum.de> parents: 250 diff changeset	194	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	195
254 7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	196
251 925232418a15 polished Christian Urban <urbanc@in.tum.de> parents: 250 diff changeset	197	lemma val_ord_LeftI:
925232418a15 polished Christian Urban <urbanc@in.tum.de> parents: 250 diff changeset	198	assumes "v :\<sqsubset>val v'" "flat v = flat v'"
925232418a15 polished Christian Urban <urbanc@in.tum.de> parents: 250 diff changeset	199	shows "(Left v) :\<sqsubset>val (Left v')"
248 b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	200	using assms(1)
251 925232418a15 polished Christian Urban <urbanc@in.tum.de> parents: 250 diff changeset	201	unfolding val_ord_ex_def
925232418a15 polished Christian Urban <urbanc@in.tum.de> parents: 250 diff changeset	202	apply(auto)
925232418a15 polished Christian Urban <urbanc@in.tum.de> parents: 250 diff changeset	203	apply(rule_tac x="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	204	using assms(2)
251 925232418a15 polished Christian Urban <urbanc@in.tum.de> parents: 250 diff changeset	205	apply(auto simp add: val_ord_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	206	done
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	207
251 925232418a15 polished Christian Urban <urbanc@in.tum.de> parents: 250 diff changeset	208	lemma val_ord_RightI:
925232418a15 polished Christian Urban <urbanc@in.tum.de> parents: 250 diff changeset	209	assumes "v :\<sqsubset>val v'" "flat v = flat v'"
925232418a15 polished Christian Urban <urbanc@in.tum.de> parents: 250 diff changeset	210	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	211	using assms(1)
251 925232418a15 polished Christian Urban <urbanc@in.tum.de> parents: 250 diff changeset	212	unfolding val_ord_ex_def
925232418a15 polished Christian Urban <urbanc@in.tum.de> parents: 250 diff changeset	213	apply(auto)
925232418a15 polished Christian Urban <urbanc@in.tum.de> parents: 250 diff changeset	214	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	215	using assms(2)
251 925232418a15 polished Christian Urban <urbanc@in.tum.de> parents: 250 diff changeset	216	apply(auto simp add: val_ord_def pflat_len_simps)
248 b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	217	done
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	218
252 022b80503766 polished Christian Urban <urbanc@in.tum.de> parents: 251 diff changeset	219	lemma val_ord_LeftE:
022b80503766 polished Christian Urban <urbanc@in.tum.de> parents: 251 diff changeset	220	assumes "(Left v1) :\<sqsubset>val (Left v2)"
022b80503766 polished Christian Urban <urbanc@in.tum.de> parents: 251 diff changeset	221	shows "v1 :\<sqsubset>val v2"
022b80503766 polished Christian Urban <urbanc@in.tum.de> parents: 251 diff changeset	222	using assms
022b80503766 polished Christian Urban <urbanc@in.tum.de> parents: 251 diff changeset	223	apply(simp add: val_ord_ex_def)
022b80503766 polished Christian Urban <urbanc@in.tum.de> parents: 251 diff changeset	224	apply(erule exE)
022b80503766 polished Christian Urban <urbanc@in.tum.de> parents: 251 diff changeset	225	apply(case_tac "p = []")
248 b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	226	apply(simp add: val_ord_def)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	227	apply(auto simp add: pflat_len_simps)
252 022b80503766 polished Christian Urban <urbanc@in.tum.de> parents: 251 diff changeset	228	apply(rule_tac x="[]" in exI)
022b80503766 polished Christian Urban <urbanc@in.tum.de> parents: 251 diff changeset	229	apply(simp add: Pos_empty pflat_len_simps)
022b80503766 polished Christian Urban <urbanc@in.tum.de> parents: 251 diff changeset	230	apply(auto simp add: pflat_len_simps val_ord_def)
022b80503766 polished Christian Urban <urbanc@in.tum.de> parents: 251 diff changeset	231	apply(rule_tac x="ps" in exI)
022b80503766 polished Christian Urban <urbanc@in.tum.de> parents: 251 diff changeset	232	apply(auto)
022b80503766 polished Christian Urban <urbanc@in.tum.de> parents: 251 diff changeset	233	apply(drule_tac x="0#q" in bspec)
022b80503766 polished Christian Urban <urbanc@in.tum.de> parents: 251 diff changeset	234	apply(simp)
022b80503766 polished Christian Urban <urbanc@in.tum.de> parents: 251 diff changeset	235	apply(simp add: pflat_len_simps)
022b80503766 polished Christian Urban <urbanc@in.tum.de> parents: 251 diff changeset	236	apply(drule_tac x="0#q" in bspec)
022b80503766 polished Christian Urban <urbanc@in.tum.de> parents: 251 diff changeset	237	apply(simp)
022b80503766 polished Christian Urban <urbanc@in.tum.de> parents: 251 diff changeset	238	apply(simp add: pflat_len_simps)
022b80503766 polished Christian Urban <urbanc@in.tum.de> parents: 251 diff changeset	239	done
248 b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	240
252 022b80503766 polished Christian Urban <urbanc@in.tum.de> parents: 251 diff changeset	241	lemma val_ord_RightE:
022b80503766 polished Christian Urban <urbanc@in.tum.de> parents: 251 diff changeset	242	assumes "(Right v1) :\<sqsubset>val (Right v2)"
022b80503766 polished Christian Urban <urbanc@in.tum.de> parents: 251 diff changeset	243	shows "v1 :\<sqsubset>val v2"
022b80503766 polished Christian Urban <urbanc@in.tum.de> parents: 251 diff changeset	244	using assms
022b80503766 polished Christian Urban <urbanc@in.tum.de> parents: 251 diff changeset	245	apply(simp add: val_ord_ex_def)
022b80503766 polished Christian Urban <urbanc@in.tum.de> parents: 251 diff changeset	246	apply(erule exE)
022b80503766 polished Christian Urban <urbanc@in.tum.de> parents: 251 diff changeset	247	apply(case_tac "p = []")
248 b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	248	apply(simp add: val_ord_def)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	249	apply(auto simp add: pflat_len_simps)
252 022b80503766 polished Christian Urban <urbanc@in.tum.de> parents: 251 diff changeset	250	apply(rule_tac x="[]" in exI)
022b80503766 polished Christian Urban <urbanc@in.tum.de> parents: 251 diff changeset	251	apply(simp add: Pos_empty pflat_len_simps)
022b80503766 polished Christian Urban <urbanc@in.tum.de> parents: 251 diff changeset	252	apply(auto simp add: pflat_len_simps val_ord_def)
022b80503766 polished Christian Urban <urbanc@in.tum.de> parents: 251 diff changeset	253	apply(rule_tac x="ps" in exI)
022b80503766 polished Christian Urban <urbanc@in.tum.de> parents: 251 diff changeset	254	apply(auto)
022b80503766 polished Christian Urban <urbanc@in.tum.de> parents: 251 diff changeset	255	apply(drule_tac x="Suc 0#q" in bspec)
022b80503766 polished Christian Urban <urbanc@in.tum.de> parents: 251 diff changeset	256	apply(simp)
022b80503766 polished Christian Urban <urbanc@in.tum.de> parents: 251 diff changeset	257	apply(simp add: pflat_len_simps)
022b80503766 polished Christian Urban <urbanc@in.tum.de> parents: 251 diff changeset	258	apply(drule_tac x="Suc 0#q" in bspec)
022b80503766 polished Christian Urban <urbanc@in.tum.de> parents: 251 diff changeset	259	apply(simp)
022b80503766 polished Christian Urban <urbanc@in.tum.de> parents: 251 diff changeset	260	apply(simp add: pflat_len_simps)
022b80503766 polished Christian Urban <urbanc@in.tum.de> parents: 251 diff changeset	261	done
022b80503766 polished Christian Urban <urbanc@in.tum.de> parents: 251 diff changeset	262
248 b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	263
252 022b80503766 polished Christian Urban <urbanc@in.tum.de> parents: 251 diff changeset	264	lemma val_ord_SeqI1:
022b80503766 polished Christian Urban <urbanc@in.tum.de> parents: 251 diff changeset	265	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	266	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	267	using assms(1)
252 022b80503766 polished Christian Urban <urbanc@in.tum.de> parents: 251 diff changeset	268	apply(subst (asm) val_ord_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	269	apply(subst (asm) val_ord_def)
252 022b80503766 polished Christian Urban <urbanc@in.tum.de> parents: 251 diff changeset	270	apply(clarify)
022b80503766 polished Christian Urban <urbanc@in.tum.de> parents: 251 diff changeset	271	apply(subst val_ord_ex_def)
022b80503766 polished Christian Urban <urbanc@in.tum.de> parents: 251 diff changeset	272	apply(rule_tac x="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	273	apply(subst val_ord_def)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	274	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	275	apply(simp)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	276	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	277	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	278	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	279	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	280	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	281	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	282	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	283	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	284	apply(simp)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	285	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	286	done
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	287
252 022b80503766 polished Christian Urban <urbanc@in.tum.de> parents: 251 diff changeset	288	lemma val_ord_SeqI2:
022b80503766 polished Christian Urban <urbanc@in.tum.de> parents: 251 diff changeset	289	assumes "v2 :\<sqsubset>val v2'" "flat v2 = flat v2'"
022b80503766 polished Christian Urban <urbanc@in.tum.de> parents: 251 diff changeset	290	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	291	using assms(1)
252 022b80503766 polished Christian Urban <urbanc@in.tum.de> parents: 251 diff changeset	292	apply(subst (asm) val_ord_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	293	apply(subst (asm) val_ord_def)
252 022b80503766 polished Christian Urban <urbanc@in.tum.de> parents: 251 diff changeset	294	apply(clarify)
022b80503766 polished Christian Urban <urbanc@in.tum.de> parents: 251 diff changeset	295	apply(subst val_ord_ex_def)
022b80503766 polished Christian Urban <urbanc@in.tum.de> parents: 251 diff changeset	296	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	297	apply(subst val_ord_def)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	298	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	299	apply(simp)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	300	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	301	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	302	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	303	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	304	apply(simp only: Pos.simps)
252 022b80503766 polished Christian Urban <urbanc@in.tum.de> parents: 251 diff changeset	305	apply(auto)[1]
022b80503766 polished Christian Urban <urbanc@in.tum.de> parents: 251 diff changeset	306	apply(simp add: pflat_len_simps)
022b80503766 polished Christian Urban <urbanc@in.tum.de> parents: 251 diff changeset	307	using assms(2)
022b80503766 polished Christian Urban <urbanc@in.tum.de> parents: 251 diff changeset	308	apply(simp)
022b80503766 polished Christian Urban <urbanc@in.tum.de> parents: 251 diff changeset	309	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	310	done
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	311
254 7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	312	lemma val_ord_SeqE:
7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	313	assumes "(Seq v1 v2) :\<sqsubset>val (Seq v1' v2')"
7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	314	shows "v1 :\<sqsubset>val v1' \<or> v2 :\<sqsubset>val v2'"
7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	315	using assms
7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	316	apply(simp add: val_ord_ex_def)
7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	317	apply(erule exE)
7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	318	apply(case_tac p)
7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	319	apply(simp add: val_ord_def)
7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	320	apply(auto simp add: pflat_len_simps intlen_append)[1]
7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	321	apply(rule_tac x="[]" in exI)
7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	322	apply(drule_tac x="[]" in spec)
7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	323	apply(simp add: Pos_empty pflat_len_simps)
7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	324	apply(case_tac a)
7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	325	apply(rule disjI1)
7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	326	apply(simp add: val_ord_def)
7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	327	apply(auto simp add: pflat_len_simps intlen_append)[1]
7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	328	apply(rule_tac x="list" in exI)
7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	329	apply(simp)
7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	330	apply(rule ballI)
7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	331	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	332	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	333	apply(simp)
254 7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	334	apply(simp add: pflat_len_simps)
7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	335	apply(case_tac nat)
7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	336	apply(rule disjI2)
7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	337	apply(simp add: val_ord_def)
7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	338	apply(auto simp add: pflat_len_simps intlen_append)
7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	339	apply(rule_tac x="list" in exI)
7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	340	apply(simp add: Pos_empty)
7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	341	apply(rule ballI)
7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	342	apply(rule impI)
7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	343	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	344	apply(simp)
254 7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	345	apply(simp add: pflat_len_simps)
7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	346	apply(simp add: val_ord_def)
248 b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	347	done
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	348
254 7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	349	lemma val_ord_StarsI:
7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	350	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	351	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	352	using assms(1)
254 7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	353	apply(subst (asm) val_ord_ex_def)
7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	354	apply(subst (asm) val_ord_def)
7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	355	apply(clarify)
7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	356	apply(subst val_ord_ex_def)
7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	357	apply(subst val_ord_def)
7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	358	apply(rule_tac x="0#p" in exI)
7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	359	apply(simp add: pflat_len_Stars_simps pflat_len_simps)
7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	360	using assms(2)
7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	361	apply(simp add: pflat_len_simps intlen_append)
7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	362	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	363	done
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	364
254 7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	365	lemma val_ord_StarsI2:
7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	366	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	367	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	368	using assms(1)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	369	apply(subst (asm) val_ord_ex_def)
254 7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	370	apply(subst (asm) val_ord_def)
7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	371	apply(clarify)
7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	372	apply(subst val_ord_ex_def)
7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	373	apply(subst val_ord_def)
7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	374	apply(case_tac p)
7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	375	apply(simp add: pflat_len_simps)
7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	376	apply(rule_tac x="[]" in exI)
7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	377	apply(simp add: pflat_len_Stars_simps pflat_len_simps intlen_append)
7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	378	apply(rule_tac x="Suc a#list" in exI)
7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	379	apply(simp add: pflat_len_Stars_simps pflat_len_simps)
7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	380	using assms(2)
7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	381	apply(simp add: pflat_len_simps intlen_append)
7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	382	apply(auto simp add: pflat_len_Stars_simps pflat_len_simps)
7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	383	done
7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	384
7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	385	lemma val_ord_Stars_appendI:
7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	386	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	387	shows "Stars (vs @ vs1) :\<sqsubset>val Stars (vs @ vs2)"
7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	388	using assms
7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	389	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	390	apply(simp)
254 7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	391	apply(simp add: val_ord_StarsI2)
7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	392	done
7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	393
7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	394	lemma val_ord_StarsE2:
7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	395	assumes "Stars (v # vs1) :\<sqsubset>val Stars (v # vs2)"
7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	396	shows "Stars vs1 :\<sqsubset>val Stars vs2"
7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	397	using assms
7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	398	apply(subst (asm) val_ord_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	399	apply(erule exE)
254 7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	400	apply(case_tac p)
7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	401	apply(simp)
7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	402	apply(simp add: val_ord_def pflat_len_simps intlen_append)
248 b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	403	apply(subst val_ord_ex_def)
254 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: val_ord_def pflat_len_simps Pos_empty)
7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	406	apply(simp)
7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	407	apply(case_tac a)
7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	408	apply(clarify)
7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	409	apply(auto simp add: pflat_len_simps val_ord_def pflat_len_def)[1]
7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	410	apply(clarify)
7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	411	apply(simp add: val_ord_ex_def)
7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	412	apply(rule_tac x="nat#list" in exI)
7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	413	apply(auto simp add: val_ord_def pflat_len_simps intlen_append)[1]
7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	414	apply(case_tac q)
7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	415	apply(simp add: val_ord_def pflat_len_simps intlen_append)
7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	416	apply(clarify)
7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	417	apply(drule_tac x="Suc a # lista" in bspec)
7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	418	apply(simp)
7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	419	apply(auto simp add: val_ord_def pflat_len_simps intlen_append)[1]
7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	420	apply(case_tac q)
7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	421	apply(simp add: val_ord_def pflat_len_simps intlen_append)
7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	422	apply(clarify)
7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	423	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	424	apply(simp)
254 7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	425	apply(auto simp add: val_ord_def pflat_len_simps intlen_append)[1]
7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	426	done
7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	427
7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	428	lemma val_ord_Stars_appendE:
7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	429	assumes "Stars (vs @ vs1) :\<sqsubset>val Stars (vs @ vs2)"
7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	430	shows "Stars vs1 :\<sqsubset>val Stars vs2"
7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	431	using assms
7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	432	apply(induct vs)
7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	433	apply(simp)
7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	434	apply(simp add: val_ord_StarsE2)
7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	435	done
7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	436
7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	437	lemma val_ord_Stars_append_eq:
7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	438	assumes "flat (Stars vs1) = flat (Stars vs2)"
7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	439	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	440	using assms
7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	441	apply(rule_tac iffI)
7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	442	apply(erule val_ord_Stars_appendE)
7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	443	apply(rule val_ord_Stars_appendI)
7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	444	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	445	done
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	446
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	447
254 7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	448	lemma val_ord_trans:
248 b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	449	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	450	shows "v1 :\<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	451	using assms
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	452	unfolding val_ord_ex_def
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	453	apply(clarify)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	454	apply(subgoal_tac "p = pa \<or> p \<sqsubset>lex pa \<or> pa \<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	455	prefer 2
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	456	apply(rule trichotomous)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	457	apply(erule disjE)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	458	apply(simp)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	459	apply(rule_tac x="pa" in exI)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	460	apply(subst val_ord_def)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	461	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	462	apply(simp add: val_ord_def)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	463	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	464	apply(simp add: val_ord_def)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	465	apply(simp add: val_ord_def)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	466	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	467	using outside_lemma apply blast
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	468	apply(simp add: val_ord_def)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	469	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	470	using outside_lemma apply force
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	471	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	472	apply(simp add: val_ord_def)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	473	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	474	apply (metis (no_types, hide_lams) lex_trans outside_lemma)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	475	apply(simp add: val_ord_def)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	476	apply(auto)[1]
254 7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	477	by (smt inlen_bigger lex_trans outside_lemma pflat_len_def)
7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	478
7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	479
7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	480	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	481
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	482
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	483	inductive
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	484	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	485	where
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	486	"\<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	487	\| "\<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	488	\| "\<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	489	\| "\<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	490	\| "\<Turnstile> Char c : CHAR c"
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	491	\| "\<Turnstile> Stars [] : STAR r"
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	492	\| "\<lbrakk>\<Turnstile> v : r; flat v \<noteq> []; \<Turnstile> Stars vs : STAR r\<rbrakk> \<Longrightarrow> \<Turnstile> Stars (v # vs) : STAR r"
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	493
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	494	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	495	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	496	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	497	using assms
254 7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	498	by (induct) (auto intro: Prf.intros)
7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	499
7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	500	lemma CPrf_stars:
7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	501	assumes "\<Turnstile> Stars vs : STAR r"
7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	502	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	503	using assms
7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	504	apply(induct vs)
7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	505	apply(auto)
7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	506	apply(erule CPrf.cases)
7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	507	apply(simp_all)
7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	508	apply(erule CPrf.cases)
7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	509	apply(simp_all)
7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	510	apply(erule CPrf.cases)
7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	511	apply(simp_all)
7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	512	apply(erule CPrf.cases)
7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	513	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	514	done
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	515
254 7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	516	lemma CPrf_Stars_appendE:
7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	517	assumes "\<Turnstile> Stars (vs1 @ vs2) : STAR r"
7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	518	shows "\<Turnstile> Stars vs1 : STAR r \<and> \<Turnstile> Stars vs2 : STAR r"
7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	519	using assms
7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	520	apply(induct vs1 arbitrary: vs2)
7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	521	apply(auto intro: CPrf.intros)[1]
7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	522	apply(erule CPrf.cases)
7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	523	apply(simp_all)
7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	524	apply(auto intro: CPrf.intros)
7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	525	done
7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	526
7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	527	definition PT :: "rexp \<Rightarrow> string \<Rightarrow> val set"
7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	528	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	529
248 b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	530	definition
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	531	"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	532
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	533	definition
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	534	"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	535
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	536	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	537	shows "CPT r s \<subseteq> CPTpre r s"
254 7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	538	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	539
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	540	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	541	"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	542	"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	543	"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	544	"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	545	"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	546	"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	547	{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	548	"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	549	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	550	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	551	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	552	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	553	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	554	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	555	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	556	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	557	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	558	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	559	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	560	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	561	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	562	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	563	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	564	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	565	done
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	566
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	567
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	568	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	569	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	570	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	571	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	572	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	573	{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	574	apply -
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	575	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	576	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	577	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	578	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	579	apply(simp)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	580	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	581	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	582	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	583	apply(simp)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	584	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	585	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	586	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	587	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	588	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	589	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	590	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	591	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	592	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	593	done
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	594
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	595	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	596	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	597	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	598	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	599	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	600	{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	601	apply -
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	602	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	603	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	604	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	605	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	606	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	607	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	608	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	609	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	610	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	611	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	612	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	613	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	614	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	615	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	616	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	617	apply(clarify)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	618	apply blast
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	619	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	620	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	621	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	622	done
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	623
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	624	lemma test:
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	625	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	626	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	627	using assms
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	628	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	629	apply(simp)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	630	apply(auto)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	631	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	632	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	633	done
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	634
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	635	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	636	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	637	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	638	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	639	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	640	apply(simp)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	641	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	642	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	643	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	644	apply(simp)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	645	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	646	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	647	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	648	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	649	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	650	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	651	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	652	apply(simp)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	653	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	654	apply(simp)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	655	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	656	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	657	apply(simp)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	658	done
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	659
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	660	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	661	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	662	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	663	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	664	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	665	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	666	apply(simp)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	667	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	668	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	669	apply(simp)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	670	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	671	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	672	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	673	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	674	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	675	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	676	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	677	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	678	apply(simp)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	679	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	680
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	681
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	682	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	683	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	684	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	685	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	686	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	687	done
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	688
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	689	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	690	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	691	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	692	using assms
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	693	apply(induct rule: Posix.induct)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	694	apply(simp add: CPT_def)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	695	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	696	apply(simp add: CPT_def)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	697	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	698	apply(simp add: CPT_def)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	699	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	700	apply(simp)
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 add: CPT_def)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	702	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	703	apply(simp)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	704	apply(simp add: CPT_def)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	705	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	706	apply(simp)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	707	apply(simp)
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 add: CPT_def)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	709	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	710	apply(simp)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	711	apply(simp)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	712	apply(simp)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	713	apply(simp add: CPT_def)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	714	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	715	done
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	716
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	717	lemma Posix_val_ord:
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	718	assumes "s \<in> r \<rightarrow> v1" "v2 \<in> 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	719	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	720	using assms
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	721	apply(induct arbitrary: v2 rule: Posix.induct)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	722	apply(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	723	apply(clarify)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	724	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	725	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	726	apply(simp add: val_ord_ex1_def)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	727	apply(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	728	apply(clarify)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	729	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	730	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	731	apply(simp add: val_ord_ex1_def)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	732	(* ALT1 *)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	733	prefer 3
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	734	(* SEQ case *)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	735	apply(subst (asm) (3) CPTpre_def)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	736	apply(clarify)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	737	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	738	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	739	apply(case_tac "s' = []")
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	740	apply(simp)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	741	prefer 2
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	742	apply(simp add: val_ord_ex1_def)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	743	apply(clarify)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	744	apply(simp)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	745	apply(simp add: val_ord_ex_def)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	746	apply(simp (no_asm) add: val_ord_def)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	747	apply(rule_tac x="[]" in exI)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	748	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	749	apply(rule intlen_length)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	750	apply (metis Posix1(2) append_assoc append_eq_conv_conj drop_eq_Nil not_le)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	751	apply(subgoal_tac "length (flat v1a) \<le> length s1")
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	752	prefer 2
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	753	apply (metis L_flat_Prf1 Prf_CPrf append_eq_append_conv_if append_take_drop_id drop_eq_Nil)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	754	apply(subst (asm) append_eq_append_conv_if)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	755	apply(simp)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	756	apply(clarify)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	757	apply(drule_tac x="v1a" in meta_spec)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	758	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	759	apply(auto simp add: CPTpre_def)[1]
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	760	using append_eq_conv_conj apply blast
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	761	apply(subst (asm) (2)val_ord_ex1_def)
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 disjE)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	763	apply(subst val_ord_ex1_def)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	764	apply(rule disjI1)
252 022b80503766 polished Christian Urban <urbanc@in.tum.de> parents: 251 diff changeset	765	apply(rule val_ord_SeqI1)
248 b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	766	apply(simp)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	767	apply(simp)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	768	apply (metis Posix1(2) append_assoc append_take_drop_id)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	769	apply(simp)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	770	apply(drule_tac x="v2b" in meta_spec)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	771	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	772	apply(auto simp add: CPTpre_def)[1]
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	773	apply (simp add: Posix1(2))
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	774	apply(subst (asm) val_ord_ex1_def)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	775	apply(erule disjE)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	776	apply(subst val_ord_ex1_def)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	777	apply(rule disjI1)
252 022b80503766 polished Christian Urban <urbanc@in.tum.de> parents: 251 diff changeset	778	apply(rule val_ord_SeqI2)
248 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)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	780	apply (simp add: Posix1(2))
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	781	apply(subst val_ord_ex1_def)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	782	apply(simp)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	783	(* ALT *)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	784	apply(subst (asm) (2) CPTpre_def)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	785	apply(clarify)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	786	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	787	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	788	apply(clarify)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	789	apply(case_tac "s' = []")
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	790	apply(simp)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	791	apply(drule_tac x="v1" in meta_spec)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	792	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	793	apply(auto simp add: CPTpre_def)[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(subst (asm) val_ord_ex1_def)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	795	apply(erule disjE)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	796	apply(subst (asm) val_ord_ex_def)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	797	apply(erule exE)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	798	apply(subst val_ord_ex1_def)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	799	apply(rule disjI1)
251 925232418a15 polished Christian Urban <urbanc@in.tum.de> parents: 250 diff changeset	800	apply(rule val_ord_LeftI)
248 b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	801	apply(subst val_ord_ex_def)
251 925232418a15 polished Christian Urban <urbanc@in.tum.de> parents: 250 diff changeset	802	apply(auto)[1]
248 b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	803	using Posix1(2) apply blast
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	804	using val_ord_ex1_def apply blast
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	805	apply(subst val_ord_ex1_def)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	806	apply(rule disjI1)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	807	apply (simp add: Posix1(2) val_ord_shorterI)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	808	apply(subst val_ord_ex1_def)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	809	apply(rule disjI1)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	810	apply(case_tac "s' = []")
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	811	apply(simp)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	812	apply(subst val_ord_ex_def)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	813	apply(rule_tac x="[0]" in exI)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	814	apply(subst val_ord_def)
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 conjI)
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 add: Pos_empty)
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 conjI)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	818	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	819	apply (smt inlen_bigger)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	820	apply(simp)
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 conjI)
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: 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	823	using Posix1(2) 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	824	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	825	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	826	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	827	using Posix1(2) 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	828	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	829	apply(rule val_ord_shorterI)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	830	apply(simp)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	831	apply (simp add: Posix1(2))
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	832	(* ALT RIGHT *)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	833	apply(subst (asm) (2) CPTpre_def)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	834	apply(clarify)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	835	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	836	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	837	apply(clarify)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	838	apply(case_tac "s' = []")
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	839	apply(simp)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	840	apply (simp add: L_flat_Prf1 Prf_CPrf)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	841	apply(subst val_ord_ex1_def)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	842	apply(rule disjI1)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	843	apply(rule val_ord_shorterI)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	844	apply(simp)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	845	apply (simp add: Posix1(2))
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	846	apply(case_tac "s' = []")
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	847	apply(simp)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	848	apply(drule_tac x="v2a" in meta_spec)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	849	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	850	apply(auto simp add: CPTpre_def)[1]
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	851	apply(subst (asm) val_ord_ex1_def)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	852	apply(erule disjE)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	853	apply(subst val_ord_ex1_def)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	854	apply(rule disjI1)
251 925232418a15 polished Christian Urban <urbanc@in.tum.de> parents: 250 diff changeset	855	apply(rule val_ord_RightI)
248 b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	856	apply(simp)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	857	using Posix1(2) apply blast
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	858	apply (simp add: val_ord_ex1_def)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	859	apply(subst val_ord_ex1_def)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	860	apply(rule disjI1)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	861	apply(rule val_ord_shorterI)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	862	apply(simp)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	863	apply (simp add: Posix1(2))
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	864	(* STAR empty case *)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	865	prefer 2
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	866	apply(subst (asm) CPTpre_def)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	867	apply(clarify)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	868	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	869	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	870	apply(clarify)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	871	apply (simp add: val_ord_ex1_def)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	872	(* STAR non-empty case *)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	873	apply(subst (asm) (3) CPTpre_def)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	874	apply(clarify)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	875	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	876	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	877	apply(clarify)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	878	apply (simp add: val_ord_ex1_def)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	879	apply(rule val_ord_shorterI)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	880	apply(simp)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	881	apply(case_tac "s' = []")
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	882	apply(simp)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	883	prefer 2
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	884	apply (simp add: val_ord_ex1_def)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	885	apply(rule disjI1)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	886	apply(rule val_ord_shorterI)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	887	apply(simp)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	888	apply (metis Posix1(2) append_assoc append_eq_conv_conj drop_all flat.simps(7) flat_Stars length_append not_less)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	889	apply(drule_tac x="va" in meta_spec)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	890	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	891	apply(auto simp add: CPTpre_def)[1]
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	892	apply (smt L.simps(6) L_flat_Prf1 Prf_CPrf append_eq_append_conv2 flat_Stars self_append_conv)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	893	apply (subst (asm) (2) val_ord_ex1_def)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	894	apply(erule disjE)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	895	prefer 2
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	896	apply(simp)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	897	apply(drule_tac x="Stars vsa" in meta_spec)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	898	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	899	apply(auto simp add: CPTpre_def)[1]
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	900	apply (simp add: Posix1(2))
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	901	apply (subst (asm) val_ord_ex1_def)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	902	apply(erule disjE)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	903	apply (subst val_ord_ex1_def)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	904	apply(rule disjI1)
253 ca4e9eb8d576 polished Christian Urban <urbanc@in.tum.de> parents: 252 diff changeset	905	apply(rule val_ord_StarsI2)
248 b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	906	apply(simp)
253 ca4e9eb8d576 polished Christian Urban <urbanc@in.tum.de> parents: 252 diff changeset	907	using Posix1(2) apply force
248 b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	908	apply(simp add: val_ord_ex1_def)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	909	apply (subst val_ord_ex1_def)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	910	apply(rule disjI1)
253 ca4e9eb8d576 polished Christian Urban <urbanc@in.tum.de> parents: 252 diff changeset	911	apply(rule val_ord_StarsI)
ca4e9eb8d576 polished Christian Urban <urbanc@in.tum.de> parents: 252 diff changeset	912	apply(simp)
ca4e9eb8d576 polished Christian Urban <urbanc@in.tum.de> parents: 252 diff changeset	913	apply(simp add: Posix1)
ca4e9eb8d576 polished Christian Urban <urbanc@in.tum.de> parents: 252 diff changeset	914	using Posix1(2) by force
ca4e9eb8d576 polished Christian Urban <urbanc@in.tum.de> parents: 252 diff changeset	915
248 b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	916
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	917	lemma Posix_val_ord_stronger:
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	918	assumes "s \<in> r \<rightarrow> v1" "v2 \<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	919	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	920	using assms
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	921	apply(rule_tac Posix_val_ord)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	922	apply(assumption)
254 7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	923	using CPT_CPTpre_subset by auto
248 b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	924
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	925
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	926	lemma Posix_val_ord_reverse:
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	927	assumes "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	928	shows "\<not>(\<exists>v2 \<in> CPT r s. v2 :\<sqsubset>val v1)"
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	929	using assms
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	930	by (metis Posix_val_ord_stronger less_irrefl val_ord_def
254 7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	931	val_ord_ex1_def val_ord_ex_def val_ord_trans)
248 b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	932
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	933
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	934	lemma val_ord_Posix_Stars:
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	935	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	936	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	937	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	938	using assms
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	939	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	940	apply(simp)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	941	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	942	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	943	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	944	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	945	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	946	defer
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	947	apply(simp)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	948	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	949	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	950	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	951	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	952	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	953	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	954	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	955	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	956	apply (metis CPrf_stars Cons_eq_map_conv Posix_CPT Posix_STAR2 Posix_val_ord_reverse list.exhaust list.set_intros(2) map_idI val.distinct(25))
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	957	apply(clarify)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	958	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	959	apply(simp)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	960	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	961	apply (meson CPrf_stars Prf.intros(7) Prf_CPrf list.set_intros(1))
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	962	apply(subst (asm) (2) val_ord_ex_def)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	963	apply(simp)
253 ca4e9eb8d576 polished Christian Urban <urbanc@in.tum.de> parents: 252 diff changeset	964	apply (metis flat.simps(7) flat_Stars val_ord_StarsI2 val_ord_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	965	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	966	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	967	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	968	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	969	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	970	prefer 2
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	971	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	972	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	973	apply(clarify)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	974	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	975	apply(simp)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	976	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	977	using Prf.intros(7) apply blast
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	978	apply(subst (asm) (2) val_ord_ex_def)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	979	apply(simp)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	980	prefer 2
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	981	apply(simp)
254 7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	982	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	983	prefer 2
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	984	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	985	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	986	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	987	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	988	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	989	prefer 2
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	990	apply(simp)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	991	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	992	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	993	apply(clarify)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	994	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	995	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	996	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	997	apply (metis CPrf_stars intlen.cases less_irrefl list.set_intros(1) val_ord_def val_ord_ex_def)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	998	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	999	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	1000	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	1001	apply(simp)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	1002	apply(subst (asm) (2) val_ord_ex_def)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	1003	apply(simp)
253 ca4e9eb8d576 polished Christian Urban <urbanc@in.tum.de> parents: 252 diff changeset	1004	apply (metis flat.simps(7) flat_Stars val_ord_StarsI2 val_ord_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	1005	proof -
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	1006	fix a :: val and vsa :: "val list" and s\<^sub>3 :: "char list" and vA :: val and vB :: "val list"
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	1007	assume a1: "s\<^sub>3 \<noteq> []"
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	1008	assume a2: "s\<^sub>3 @ concat (map flat vB) = concat (map flat vsa)"
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	1009	assume a3: "flat vA = flat a @ s\<^sub>3"
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	1010	assume a4: "\<forall>p. \<not> Stars (vA # vB) \<sqsubset>val p Stars (a # vsa)"
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	1011	have f5: "\<And>n cs. drop n (cs::char list) = [] \<or> n < length cs"
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	1012	by (meson drop_eq_Nil not_less)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	1013	have f6: "\<not> length (flat vA) \<le> length (flat a)"
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	1014	using a3 a1 by simp
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	1015	have "flat (Stars (a # vsa)) = flat (Stars (vA # vB))"
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	1016	using a3 a2 by simp
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	1017	then show False
253 ca4e9eb8d576 polished Christian Urban <urbanc@in.tum.de> parents: 252 diff changeset	1018	using f6 f5 a4 by (metis (full_types) drop_eq_Nil val_ord_StarsI val_ord_ex_def val_ord_shorterI)
248 b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	1019	qed
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	1020
254 7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	1021
248 b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	1022
254 7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	1023
248 b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	1024
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	1025	lemma val_ord_Posix:
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	1026	assumes "v1 \<in> CPT r s" "\<not>(\<exists>v2 \<in> PT r s. v2 :\<sqsubset>val v1)"
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	1027	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	1028	using assms
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	1029	apply(induct r arbitrary: s v1)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	1030	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	1031	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	1032	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	1033	(* ONE *)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	1034	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	1035	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	1036	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	1037	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	1038	(* CHAR *)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	1039	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	1040	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	1041	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	1042	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	1043	prefer 2
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	1044	(* ALT *)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	1045	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	1046	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	1047	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	1048	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	1049	apply(drule_tac x="flat v1a" in meta_spec)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	1050	apply(drule_tac x="v1a" in meta_spec)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	1051	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	1052	apply(simp)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	1053	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	1054	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	1055	apply(drule_tac x="Left v2" in spec)
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)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	1057	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	1058	apply(rule Prf.intros)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	1059	apply(simp)
251 925232418a15 polished Christian Urban <urbanc@in.tum.de> parents: 250 diff changeset	1060	apply (meson val_ord_LeftI)
248 b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	1061	apply(assumption)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	1062	(* ALT Right *)
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)[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(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	1065	apply(rotate_tac 1)
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_tac x="flat v2" in meta_spec)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	1067	apply(drule_tac x="v2" in meta_spec)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	1068	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	1069	apply(simp)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	1070	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	1071	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	1072	apply(drule_tac x="Right v2a" 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(rule Prf.intros)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	1076	apply(simp)
251 925232418a15 polished Christian Urban <urbanc@in.tum.de> parents: 250 diff changeset	1077	apply(drule val_ord_RightI)
248 b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	1078	apply(assumption)
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: val_ord_ex_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	apply(assumption)
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(subgoal_tac "\<exists>v2'. flat v2' = flat v2 \<and> \<turnstile> v2' : r1a")
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	1083	apply(clarify)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	1084	apply(drule_tac x="Left v2'" in spec)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	1085	apply(simp)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	1086	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	1087	apply(rule Prf.intros)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	1088	apply(assumption)
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 add: val_ord_ex_def)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	1090	apply(subst (asm) (3) val_ord_def)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	1091	apply(simp)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	1092	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	1093	apply(drule_tac x="[0]" in spec)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	1094	apply(simp add: pflat_len_simps Pos_empty)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	1095	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	1096	apply (smt inlen_bigger)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	1097	apply(erule disjE)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	1098	apply blast
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	1099	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	1100	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	1101	(* SEQ *)
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 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	1103	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	1104	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	1105	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	1106	apply(drule_tac x="flat v1a" in meta_spec)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	1107	apply(drule_tac x="v1a" in meta_spec)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	1108	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	1109	apply(simp)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	1110	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	1111	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	1112	apply(auto simp add: 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	1113	apply(drule_tac x="Seq v2a v2" in spec)
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)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	1115	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	1116	apply (simp add: Prf.intros(1) Prf_CPrf)
252 022b80503766 polished Christian Urban <urbanc@in.tum.de> parents: 251 diff changeset	1117	using val_ord_SeqI1 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	1118	apply(assumption)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	1119	apply(rotate_tac 1)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	1120	apply(drule_tac x="flat v2" in meta_spec)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	1121	apply(drule_tac x="v2" in meta_spec)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	1122	apply(simp)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	1123	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	1124	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	1125	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	1126	apply(auto simp add: 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	1127	apply(drule_tac x="Seq v1a v2a" in spec)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	1128	apply(simp)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	1129	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	1130	apply (simp add: Prf.intros(1) Prf_CPrf)
252 022b80503766 polished Christian Urban <urbanc@in.tum.de> parents: 251 diff changeset	1131	apply (meson val_ord_SeqI2)
248 b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	1132	apply(assumption)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	1133	(* SEQ side condition *)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	1134	apply(auto simp add: PT_def)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	1135	apply(subgoal_tac "\<exists>vA. flat vA = flat v1a @ s\<^sub>3 \<and> \<turnstile> vA : r1a")
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	1136	prefer 2
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	1137	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	1138	apply(subgoal_tac "\<exists>vB. flat vB = s\<^sub>4 \<and> \<turnstile> vB : r2a")
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	1139	prefer 2
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	1140	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	1141	apply(clarify)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	1142	apply(drule_tac x="Seq 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	1143	apply(simp)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	1144	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	1145	apply (simp add: Prf.intros(1))
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	1146	apply(subst (asm) (3) val_ord_ex_def)
252 022b80503766 polished Christian Urban <urbanc@in.tum.de> parents: 251 diff changeset	1147	apply (metis append_Nil2 append_assoc append_eq_conv_conj flat.simps(5) length_append not_add_less1 not_less_iff_gr_or_eq val_ord_SeqI1 val_ord_ex_def val_ord_shorterI)
248 b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	1148	(* STAR *)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	1149	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	1150	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	1151	apply(simp_all)[6]
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	1152	using Posix_STAR2 apply blast
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	1153	apply(clarify)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	1154	apply(rule val_ord_Posix_Stars)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	1155	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	1156	apply (simp add: CPrf.intros(7))
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	1157	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	1158	apply(drule_tac x="flat v" in meta_spec)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	1159	apply(drule_tac x="v" in meta_spec)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	1160	apply(simp)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	1161	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	1162	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	1163	apply(drule_tac x="Stars (v2#vs)" in spec)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	1164	apply(simp)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	1165	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	1166	using Prf.intros(7) Prf_CPrf apply blast
253 ca4e9eb8d576 polished Christian Urban <urbanc@in.tum.de> parents: 252 diff changeset	1167	apply(simp add: val_ord_StarsI)
248 b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	1168	apply(assumption)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	1169	apply(drule_tac x="flat va" in meta_spec)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	1170	apply(drule_tac x="va" in meta_spec)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	1171	apply(simp)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	1172	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	1173	using CPrf_stars apply blast
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	1174	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	1175	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	1176	apply(subgoal_tac "\<exists>pre post. vs = pre @ [va] @ post")
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	1177	prefer 2
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	1178	apply (metis append_Cons append_Nil in_set_conv_decomp_first)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	1179	apply(clarify)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	1180	apply(drule_tac x="Stars (v#(pre @ [v2] @ post))" in spec)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	1181	apply(simp)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	1182	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	1183	apply(rule Prf.intros)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	1184	apply (simp add: Prf_CPrf)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	1185	apply(rule Prf_Stars_append)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	1186	apply(drule CPrf_Stars_appendE)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	1187	apply(auto simp add: Prf_CPrf)[1]
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	1188	apply (metis CPrf_Stars_appendE CPrf_stars Prf_CPrf Prf_Stars list.set_intros(2) set_ConsD)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	1189	apply(subgoal_tac "\<not> Stars ([v] @ pre @ v2 # post) :\<sqsubset>val Stars ([v] @ pre @ va # post)")
254 7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	1190	apply(subst (asm) val_ord_Stars_append_eq)
248 b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	1191	apply(simp)
254 7c89d3f6923e polished Christian Urban <urbanc@in.tum.de> parents: 253 diff changeset	1192	apply(subst (asm) val_ord_Stars_append_eq)
248 b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	1193	apply(simp)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	1194	prefer 2
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	1195	apply(simp)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	1196	prefer 2
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	1197	apply(simp)
253 ca4e9eb8d576 polished Christian Urban <urbanc@in.tum.de> parents: 252 diff changeset	1198	apply (simp add: val_ord_StarsI)
248 b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	1199	apply(auto simp add: PT_def)
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	1200	done
b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	1201
249 256484ef4be4 updated Christian Urban <urbanc@in.tum.de> parents: 248 diff changeset	1202	unused_thms
256484ef4be4 updated Christian Urban <urbanc@in.tum.de> parents: 248 diff changeset	1203
248 b90ff5abb437 added a proof that Positional ordering is equivalent to direct posix definition Christian Urban <urbanc@in.tum.de> parents: diff changeset	1204	end

author	Christian Urban <urbanc@in.tum.de>
	Tue, 27 Jun 2017 13:15:55 +0100
changeset 254	7c89d3f6923e
parent 253	ca4e9eb8d576
child 255	222ed43892ea
permissions	-rw-r--r--