--- a/thys/Positions.thy Mon Jun 26 18:40:58 2017 +0100
+++ b/thys/Positions.thy Tue Jun 27 01:02:17 2017 +0100
@@ -21,13 +21,11 @@
| "Pos (Right v) = {[]} \<union> {1#ps | ps. ps \<in> Pos v}"
| "Pos (Seq v1 v2) = {[]} \<union> {0#ps | ps. ps \<in> Pos v1} \<union> {1#ps | ps. ps \<in> Pos v2}"
| "Pos (Stars []) = {[]}"
-| "Pos (Stars (v#vs)) = {[]} \<union> {0#ps | ps. ps \<in> Pos v} \<union> {(Suc n)#ps | n ps. n#ps \<in> Pos (Stars vs)}"
+| "Pos (Stars (v#vs)) = {[]} \<union> {0#ps | ps. ps \<in> Pos v} \<union> {Suc n#ps | n ps. n#ps \<in> Pos (Stars vs)}"
lemma Pos_empty:
shows "[] \<in> Pos v"
-apply(induct v rule: Pos.induct)
-apply(auto)
-done
+by (induct v rule: Pos.induct)(auto)
fun intlen :: "'a list \<Rightarrow> int"
where
@@ -36,15 +34,11 @@
lemma inlen_bigger:
shows "0 \<le> intlen xs"
-apply(induct xs)
-apply(auto)
-done
+by (induct xs)(auto)
lemma intlen_append:
shows "intlen (xs @ ys) = intlen xs + intlen ys"
-apply(induct xs arbitrary: ys)
-apply(auto)
-done
+by (induct xs arbitrary: ys) (auto)
lemma intlen_length:
assumes "length xs < length ys"
@@ -69,29 +63,17 @@
and "pflat_len (Left v) (Suc 0#p) = -1"
and "pflat_len (Right v) (Suc 0#p) = pflat_len v p"
and "pflat_len (Right v) (0#p) = -1"
+ and "pflat_len (Stars (v#vs)) (Suc n#p) = pflat_len (Stars vs) (n#p)"
+ and "pflat_len (Stars (v#vs)) (0#p) = pflat_len v p"
and "pflat_len v [] = intlen (flat v)"
-apply(auto simp add: pflat_len_def Pos_empty)
-done
+by (auto simp add: pflat_len_def Pos_empty)
lemma pflat_len_Stars_simps:
assumes "n < length vs"
shows "pflat_len (Stars vs) (n#p) = pflat_len (vs!n) p"
using assms
apply(induct vs arbitrary: n p)
-apply(simp)
-apply(simp)
-apply(simp add: pflat_len_def)
-apply(auto)[1]
-apply (metis at.simps(6))
-apply (metis Suc_less_eq Suc_pred)
-by (metis diff_Suc_1 less_Suc_eq_0_disj nth_Cons')
-
-
-lemma pflat_len_Stars_simps2:
- shows "pflat_len (Stars (v#vs)) (Suc n # p) = pflat_len (Stars vs) (n#p)"
- and "pflat_len (Stars (v#vs)) (0 # p) = pflat_len v p"
-using assms
-apply(simp_all add: pflat_len_def)
+apply(auto simp add: less_Suc_eq_0_disj pflat_len_simps)
done
lemma Two_to_Three_aux:
@@ -103,7 +85,6 @@
apply (smt inlen_bigger)+
done
-
lemma Two_to_Three_orig:
assumes "\<forall>p \<in> Pos v1 \<union> Pos v2. pflat_len v1 p = pflat_len v2 p"
shows "Pos v1 = Pos v2"
@@ -308,7 +289,7 @@
where
"ps1 \<sqsubset>spre ps2 \<equiv> (ps1 \<sqsubseteq>pre ps2 \<and> ps1 \<noteq> ps2)"
-inductive lex_lists :: "nat list \<Rightarrow> nat list \<Rightarrow> bool" ("_ \<sqsubset>lex _")
+inductive lex_list :: "nat list \<Rightarrow> nat list \<Rightarrow> bool" ("_ \<sqsubset>lex _")
where
"[] \<sqsubset>lex p#ps"
| "ps1 \<sqsubset>lex ps2 \<Longrightarrow> (p#ps1) \<sqsubset>lex (p#ps2)"
@@ -319,71 +300,36 @@
assumes "ps1 \<sqsubset>lex ps2"
shows "ps1 \<noteq> ps2"
using assms
-apply(induct rule: lex_lists.induct)
+apply(induct rule: lex_list.induct)
apply(auto)
done
-lemma lex_append:
- assumes "ps2 \<noteq> []"
- shows "ps \<sqsubset>lex ps @ ps2"
-using assms
-apply(induct ps)
-apply(auto intro: lex_lists.intros)
-apply(case_tac ps2)
-apply(simp)
-apply(simp)
-apply(auto intro: lex_lists.intros)
-done
-
-lemma lexordp_simps [simp]:
+lemma lex_simps [simp]:
fixes xs ys :: "nat list"
- shows "[] \<sqsubset>lex ys = (ys \<noteq> [])"
- and "xs \<sqsubset>lex [] = False"
+ shows "[] \<sqsubset>lex ys \<longleftrightarrow> ys \<noteq> []"
+ and "xs \<sqsubset>lex [] \<longleftrightarrow> False"
and "(x # xs) \<sqsubset>lex (y # ys) \<longleftrightarrow> (x < y \<or> (\<not> y < x \<and> xs \<sqsubset>lex ys))"
apply -
-apply (metis lex_append lex_lists.simps list.simps(3))
-using lex_lists.cases apply blast
-using lex_lists.cases lex_lists.intros(2) lex_lists.intros(3) not_less_iff_gr_or_eq by fastforce
+apply (metis lex_irrfl lex_list.intros(1) list.exhaust)
+using lex_list.cases apply blast
+using lex_list.cases lex_list.intros(2) lex_list.intros(3) not_less_iff_gr_or_eq by fastforce
-lemma lex_append_cancel [simp]:
- fixes ps ps1 ps2 :: "nat list"
- shows "ps @ ps1 \<sqsubset>lex ps @ ps2 \<longleftrightarrow> ps1 \<sqsubset>lex ps2"
-apply(induct ps)
-apply(auto)
-done
lemma lex_trans:
fixes ps1 ps2 ps3 :: "nat list"
assumes "ps1 \<sqsubset>lex ps2" "ps2 \<sqsubset>lex ps3"
shows "ps1 \<sqsubset>lex ps3"
using assms
-apply(induct arbitrary: ps3 rule: lex_lists.induct)
-apply(erule lex_lists.cases)
+apply(induct arbitrary: ps3 rule: lex_list.induct)
+apply(erule lex_list.cases)
apply(simp_all)
apply(rotate_tac 2)
-apply(erule lex_lists.cases)
+apply(erule lex_list.cases)
apply(simp_all)
-apply(erule lex_lists.cases)
+apply(erule lex_list.cases)
apply(simp_all)
done
-lemma trichotomous_aux:
- fixes p q :: "nat list"
- assumes "p \<sqsubset>lex q" "p \<noteq> q"
- shows "\<not>(q \<sqsubset>lex p)"
-using assms
-apply(induct rule: lex_lists.induct)
-apply(auto)
-done
-
-lemma trichotomous_aux2:
- fixes p q :: "nat list"
- assumes "p \<sqsubset>lex q" "q \<sqsubset>lex p"
- shows "False"
-using assms
-apply(induct rule: lex_lists.induct)
-apply(auto)
-done
lemma trichotomous:
fixes p q :: "nat list"
@@ -394,12 +340,6 @@
apply(auto)
done
-(*
-definition dpos :: "val \<Rightarrow> val \<Rightarrow> nat list \<Rightarrow> bool"
- where
- "dpos v1 v2 p \<equiv> (p \<in> Pos v1 \<union> Pos v2) \<and> (p \<notin> Pos v1 \<inter> Pos v2)"
-*)
-
lemma outside_lemma:
assumes "p \<notin> Pos v1 \<union> Pos v2"
shows "pflat_len v1 p = pflat_len v2 p"
@@ -407,35 +347,6 @@
apply(auto simp add: pflat_len_def)
done
-(*
-lemma dpos_lemma_aux:
- assumes "p \<in> Pos v1 \<union> Pos v2"
- and "pflat_len v1 p = pflat_len v2 p"
- shows "p \<in> Pos v1 \<inter> Pos v2"
-using assms
-apply(auto simp add: pflat_len_def)
-apply (smt inlen_bigger)
-apply (smt inlen_bigger)
-done
-
-lemma dpos_lemma:
- assumes "p \<in> Pos v1 \<union> Pos v2"
- and "pflat_len v1 p = pflat_len v2 p"
- shows "\<not>dpos v1 v2 p"
-using assms
-apply(auto simp add: dpos_def dpos_lemma_aux)
-using dpos_lemma_aux apply auto[1]
-using dpos_lemma_aux apply auto[1]
-done
-
-lemma dpos_lemma2:
- assumes "p \<in> Pos v1 \<union> Pos v2"
- and "dpos v1 v2 p"
- shows "pflat_len v1 p \<noteq> pflat_len v2 p"
-using assms
-using dpos_lemma by blast
-*)
-
definition val_ord:: "val \<Rightarrow> nat list \<Rightarrow> val \<Rightarrow> bool" ("_ \<sqsubset>val _ _")
where
"v1 \<sqsubset>val p v2 \<equiv> (p \<in> Pos v1 \<and> pflat_len v1 p > pflat_len v2 p \<and>
@@ -453,78 +364,48 @@
lemma val_ord_shorterI:
assumes "length (flat v') < length (flat v)"
shows "v :\<sqsubset>val v'"
-using assms(1)
-apply(subst val_ord_ex_def)
-apply(rule_tac x="[]" in exI)
-apply(subst val_ord_def)
-apply(rule conjI)
-apply (simp add: Pos_empty)
-apply(rule conjI)
-apply(simp add: pflat_len_simps)
-apply (simp add: intlen_length)
-apply(simp)
-done
+using assms
+unfolding val_ord_ex_def
+by (metis Pos_empty intlen_length lex_simps(2) pflat_len_simps(9) val_ord_def)
-lemma val_ord_spre:
+lemma val_ord_spreI:
assumes "(flat v') \<sqsubset>spre (flat v)"
shows "v :\<sqsubset>val v'"
-using assms(1)
+using assms
apply(rule_tac val_ord_shorterI)
-apply(simp add: sprefix_list_def prefix_list_def)
-apply(auto)
-apply(case_tac ps')
-apply(auto)
-by (metis append_eq_conv_conj drop_all le_less_linear neq_Nil_conv)
+by (metis append_eq_conv_conj le_less_linear prefix_list_def sprefix_list_def take_all)
-
-lemma val_ord_ALTI:
- assumes "v \<sqsubset>val p v'" "flat v = flat v'"
- shows "(Left v) \<sqsubset>val (0#p) (Left v')"
+lemma val_ord_LeftI:
+ assumes "v :\<sqsubset>val v'" "flat v = flat v'"
+ shows "(Left v) :\<sqsubset>val (Left v')"
using assms(1)
-apply(subst (asm) val_ord_def)
-apply(erule conjE)
-apply(subst val_ord_def)
-apply(rule conjI)
-apply(simp)
-apply(rule conjI)
-apply(simp add: pflat_len_simps)
-apply(rule ballI)
-apply(rule impI)
-apply(simp only: Pos.simps)
-apply(auto)[1]
+unfolding val_ord_ex_def
+apply(auto)
+apply(rule_tac x="0#p" in exI)
using assms(2)
-apply(simp add: pflat_len_simps)
-apply(auto simp add: pflat_len_simps)[2]
+apply(auto simp add: val_ord_def pflat_len_simps)
done
-lemma val_ord_ALTI2:
- assumes "v \<sqsubset>val p v'" "flat v = flat v'"
- shows "(Right v) \<sqsubset>val (1#p) (Right v')"
+lemma val_ord_RightI:
+ assumes "v :\<sqsubset>val v'" "flat v = flat v'"
+ shows "(Right v) :\<sqsubset>val (Right v')"
using assms(1)
-apply(subst (asm) val_ord_def)
-apply(erule conjE)
-apply(subst val_ord_def)
-apply(rule conjI)
-apply(simp)
-apply(rule conjI)
-apply(simp add: pflat_len_simps)
-apply(rule ballI)
-apply(rule impI)
-apply(simp only: Pos.simps)
-apply(auto)[1]
+unfolding val_ord_ex_def
+apply(auto)
+apply(rule_tac x="Suc 0#p" in exI)
using assms(2)
-apply(simp add: pflat_len_simps)
-apply(auto simp add: pflat_len_simps)[2]
+apply(auto simp add: val_ord_def pflat_len_simps)
done
+
lemma val_ord_ALTE:
assumes "(Left v1) \<sqsubset>val (p # ps) (Left v2)"
shows "p = 0 \<and> v1 \<sqsubset>val ps v2"
using assms(1)
apply(simp add: val_ord_def)
apply(auto simp add: pflat_len_simps)
-apply (metis (no_types, hide_lams) assms lex_lists.intros(2) outside_lemma pflat_len_simps(3) val_ord_def)
-by (metis (no_types, hide_lams) assms lex_lists.intros(2) outside_lemma pflat_len_simps(3) val_ord_def)
+apply (metis (no_types, hide_lams) assms lex_list.intros(2) outside_lemma pflat_len_simps(3) val_ord_def)
+by (metis (no_types, hide_lams) assms lex_list.intros(2) outside_lemma pflat_len_simps(3) val_ord_def)
lemma val_ord_ALTE2:
assumes "(Right v1) \<sqsubset>val (p # ps) (Right v2)"
@@ -532,8 +413,8 @@
using assms(1)
apply(simp add: val_ord_def)
apply(auto simp add: pflat_len_simps)
-apply (metis (no_types, hide_lams) assms lex_lists.intros(2) outside_lemma pflat_len_simps(5) val_ord_def)
-by (metis (no_types, hide_lams) assms lex_lists.intros(2) outside_lemma pflat_len_simps(5) val_ord_def)
+apply (metis (no_types, hide_lams) assms lex_list.intros(2) outside_lemma pflat_len_simps(5) val_ord_def)
+by (metis (no_types, hide_lams) assms lex_list.intros(2) outside_lemma pflat_len_simps(5) val_ord_def)
lemma val_ord_STARI:
assumes "v1 \<sqsubset>val p v2" "flat (Stars (v1#vs1)) = flat (Stars (v2#vs2))"
@@ -585,7 +466,7 @@
apply(simp)
using assms(2)
apply(auto)
-apply (simp add: pflat_len_simps(7))
+apply (simp add: pflat_len_simps(9))
apply (simp add: pflat_len_Stars_simps)
using assms(2)
apply(auto simp add: pflat_len_def)[1]
@@ -795,39 +676,6 @@
by (metis IntE Two_to_Three_aux UnCI lex_trans outside_lemma)
-lemma Pos_pre:
- assumes "p \<in> Pos v" "q \<sqsubseteq>pre p"
- shows "q \<in> Pos v"
-using assms
-apply(induct v arbitrary: p q rule: Pos.induct)
-apply(simp_all add: prefix_list_def)
-apply (meson append_eq_Cons_conv append_is_Nil_conv)
-apply (meson append_eq_Cons_conv append_is_Nil_conv)
-apply (metis (no_types, lifting) Cons_eq_append_conv append_is_Nil_conv)
-apply(auto)
-apply (meson append_eq_Cons_conv)
-apply(simp add: append_eq_Cons_conv)
-apply(auto)
-done
-
-lemma lex_lists_order:
- assumes "q' \<sqsubset>lex q" "\<not>(q' \<sqsubseteq>pre q)"
- shows "\<not>(q \<sqsubset>lex q')"
-using assms
-apply(induct rule: lex_lists.induct)
-apply(simp add: prefix_list_def)
-apply(auto)
-using trichotomous_aux2 by auto
-
-lemma lex_appendL:
- assumes "q \<sqsubset>lex p"
- shows "q \<sqsubset>lex p @ q'"
-using assms
-apply(induct arbitrary: q' rule: lex_lists.induct)
-apply(auto)
-done
-
-
inductive
CPrf :: "val \<Rightarrow> rexp \<Rightarrow> bool" ("\<Turnstile> _ : _" [100, 100] 100)
where
@@ -943,17 +791,6 @@
apply(simp_all)[7]
done
-lemma CPTpre_SEQ:
- assumes "v \<in> CPTpre (SEQ r1 r2) s"
- shows "\<exists>s'. flat v = s' \<and> (s' \<sqsubseteq>pre s) \<and> s' \<in> L (SEQ r1 r2)"
-using assms
-apply(simp add: CPTpre_simps)
-apply(auto simp add: CPTpre_def)
-apply (simp add: prefix_list_def)
-by (metis L.simps(4) L_flat_Prf1 Prf.intros(1) Prf_CPrf flat.simps(5))
-
-term "{vs. Stars vs \<in> A}"
-
lemma test:
assumes "finite A"
shows "finite {vs. Stars vs \<in> A}"
@@ -1138,10 +975,9 @@
apply(erule exE)
apply(subst val_ord_ex1_def)
apply(rule disjI1)
+apply(rule val_ord_LeftI)
apply(subst val_ord_ex_def)
-apply(rule_tac x="0#p" in exI)
-apply(rule val_ord_ALTI)
-apply(simp)
+apply(auto)[1]
using Posix1(2) apply blast
using val_ord_ex1_def apply blast
apply(subst val_ord_ex1_def)
@@ -1192,13 +1028,9 @@
apply(auto simp add: CPTpre_def)[1]
apply(subst (asm) val_ord_ex1_def)
apply(erule disjE)
-apply(subst (asm) val_ord_ex_def)
-apply(erule exE)
apply(subst val_ord_ex1_def)
apply(rule disjI1)
-apply(subst val_ord_ex_def)
-apply(rule_tac x="1#p" in exI)
-apply(rule val_ord_ALTI2)
+apply(rule val_ord_RightI)
apply(simp)
using Posix1(2) apply blast
apply (simp add: val_ord_ex1_def)
@@ -1253,7 +1085,10 @@
apply (subst val_ord_ex_def)
apply(case_tac p)
apply(simp)
-apply (metis Posix1(2) flat_Stars not_less_iff_gr_or_eq pflat_len_simps(7) same_append_eq val_ord_def)
+apply (metis Posix1(2) append_eq_conv_conj flat_Stars not_less_iff_gr_or_eq pflat_len_simps(9) val_ord_def)
+
+
+
using Posix1(2) val_ord_STARI2 apply fastforce
apply(simp add: val_ord_ex1_def)
apply (subst (asm) val_ord_ex_def)
@@ -1283,13 +1118,13 @@
apply(simp add: val_ord_def)
apply(rule conjI)
apply(simp add: val_ord_def)
-apply(auto simp add: pflat_len_simps pflat_len_Stars_simps2)[1]
+apply(auto simp add: pflat_len_simps)[1]
apply(rule ballI)
apply(rule impI)
-apply(simp add: val_ord_def pflat_len_simps pflat_len_Stars_simps2 intlen_append)
+apply(simp add: val_ord_def pflat_len_simps intlen_append)
apply(clarify)
apply(case_tac q)
-apply(simp add: val_ord_def pflat_len_simps pflat_len_Stars_simps2 intlen_append)
+apply(simp add: val_ord_def pflat_len_simps intlen_append)
apply(clarify)
apply(erule disjE)
prefer 2
@@ -1297,12 +1132,12 @@
apply(simp)
apply(drule mp)
apply(simp)
-apply(simp add: val_ord_def pflat_len_simps pflat_len_Stars_simps2 intlen_append)
+apply(simp add: val_ord_def pflat_len_simps intlen_append)
apply(drule_tac x="Suc a # list" in bspec)
apply(simp)
apply(drule mp)
apply(simp)
-apply(simp add: val_ord_def pflat_len_simps pflat_len_Stars_simps2 intlen_append)
+apply(simp add: val_ord_def pflat_len_simps intlen_append)
done
@@ -1313,14 +1148,6 @@
by (metis Posix_val_ord_stronger less_irrefl val_ord_def
val_ord_ex1_def val_ord_ex_def val_ord_ex_trans)
-thm Posix.intros(6)
-
-inductive Prop :: "rexp \<Rightarrow> val list \<Rightarrow> bool"
-where
- "Prop r []"
-| "\<lbrakk>Prop r vs;
- \<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = concat (map flat vs) \<and> flat v @ s\<^sub>3 \<in> L r \<and> s\<^sub>4 \<in> L (STAR r))\<rbrakk>
- \<Longrightarrow> Prop r (v # vs)"
lemma STAR_val_ord_ex:
assumes "Stars (v # vs1) :\<sqsubset>val Stars (v # vs2)"
@@ -1339,7 +1166,7 @@
apply(clarify)
prefer 2
using STAR_val_ord val_ord_ex_def apply blast
-apply(auto simp add: pflat_len_Stars_simps2 val_ord_def pflat_len_def)[1]
+apply(auto simp add: pflat_len_simps val_ord_def pflat_len_def)[1]
done
lemma STAR_val_ord_exI:
@@ -1384,25 +1211,6 @@
apply(auto)
done
-lemma Posix_STARI:
- assumes "\<forall>v \<in> set vs. flat v \<noteq> [] \<and> (flat v) \<in> r \<rightarrow> v" "Prop r vs"
- shows "flat (Stars vs) \<in> STAR r \<rightarrow> Stars vs"
-using assms
-apply(induct vs arbitrary: r)
-apply(simp)
-apply(rule Posix.intros)
-apply(simp)
-apply(rule Posix.intros)
-apply(simp)
-apply(auto)[1]
-apply(erule Prop.cases)
-apply(simp)
-apply(simp)
-apply(simp)
-apply(erule Prop.cases)
-apply(simp)
-apply(auto)[1]
-done
lemma CPrf_stars:
assumes "\<Turnstile> Stars vs : STAR r"
@@ -1462,7 +1270,7 @@
apply (meson CPrf_stars Prf.intros(7) Prf_CPrf list.set_intros(1))
apply(subst (asm) (2) val_ord_ex_def)
apply(simp)
-apply (metis flat.simps(7) flat_Stars intlen.cases not_less_iff_gr_or_eq pflat_len_simps(7) val_ord_STARI2 val_ord_def val_ord_ex_def)
+apply (metis flat.simps(7) flat_Stars intlen.cases not_less_iff_gr_or_eq pflat_len_simps(9) val_ord_STARI2 val_ord_def val_ord_ex_def)
apply(auto simp add: CPT_def PT_def)[1]
using CPrf_stars apply auto[1]
apply(auto)[1]
@@ -1502,7 +1310,7 @@
apply(simp)
apply(subst (asm) (2) val_ord_ex_def)
apply(simp)
-apply (metis flat.simps(7) flat_Stars intlen.cases not_less_iff_gr_or_eq pflat_len_simps(7) val_ord_STARI2 val_ord_def val_ord_ex_def)
+apply (metis flat.simps(7) flat_Stars intlen.cases not_less_iff_gr_or_eq pflat_len_simps(9) val_ord_STARI2 val_ord_def val_ord_ex_def)
proof -
fix a :: val and vsa :: "val list" and s\<^sub>3 :: "char list" and vA :: val and vB :: "val list"
assume a1: "s\<^sub>3 \<noteq> []"
@@ -1576,7 +1384,7 @@
apply(drule mp)
apply(rule Prf.intros)
apply(simp)
-apply (meson val_ord_ALTI val_ord_ex_def)
+apply (meson val_ord_LeftI)
apply(assumption)
(* ALT Right *)
apply(auto simp add: CPT_def)[1]
@@ -1593,9 +1401,7 @@
apply(drule mp)
apply(rule Prf.intros)
apply(simp)
-apply(subst (asm) (2) val_ord_ex_def)
-apply(erule exE)
-apply(drule val_ord_ALTI2)
+apply(drule val_ord_RightI)
apply(assumption)
apply(auto simp add: val_ord_ex_def)[1]
apply(assumption)