theory Sulzmann
imports "Lexer" "~~/src/HOL/Library/Multiset"
begin
section {* Sulzmann's "Ordering" of Values *}
fun
size :: "val \<Rightarrow> nat"
where
"size (Void) = 0"
| "size (Char c) = 0"
| "size (Left v) = 1 + size v"
| "size (Right v) = 1 + size v"
| "size (Seq v1 v2) = 1 + (size v1) + (size v2)"
| "size (Stars []) = 0"
| "size (Stars (v#vs)) = 1 + (size v) + (size (Stars vs))"
lemma Star_size [simp]:
"\<lbrakk>n < length vs; 0 < length vs\<rbrakk> \<Longrightarrow> size (nth vs n) < size (Stars vs)"
apply(induct vs arbitrary: n)
apply(simp)
apply(auto)
by (metis One_nat_def Suc_pred less_Suc0 less_Suc_eq list.size(3) not_add_less1 not_less_eq nth_Cons' trans_less_add2)
lemma Star_size0 [simp]:
"0 < length vs \<Longrightarrow> 0 < size (Stars vs)"
apply(induct vs)
apply(auto)
done
fun
at :: "val \<Rightarrow> nat list \<Rightarrow> val"
where
"at v [] = v"
| "at (Left v) (0#ps)= at v ps"
| "at (Right v) (Suc 0#ps)= at v ps"
| "at (Seq v1 v2) (0#ps)= at v1 ps"
| "at (Seq v1 v2) (Suc 0#ps)= at v2 ps"
| "at (Stars vs) (n#ps)= at (nth vs n) ps"
fun
ato :: "val \<Rightarrow> nat list \<Rightarrow> val option"
where
"ato v [] = Some v"
| "ato (Left v) (0#ps)= ato v ps"
| "ato (Right v) (Suc 0#ps)= ato v ps"
| "ato (Seq v1 v2) (0#ps)= ato v1 ps"
| "ato (Seq v1 v2) (Suc 0#ps)= ato v2 ps"
| "ato (Stars vs) (n#ps)= (if (n < length vs) then ato (nth vs n) ps else None)"
| "ato v p = None"
fun Pos :: "val \<Rightarrow> (nat list) set"
where
"Pos (Void) = {[]}"
| "Pos (Char c) = {[]}"
| "Pos (Left v) = {[]} \<union> {0#ps | ps. ps \<in> Pos v}"
| "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)}"
lemma Pos_empty:
shows "[] \<in> Pos v"
apply(induct v rule: Pos.induct)
apply(auto)
done
lemma Pos_finite_aux:
assumes "\<forall>v \<in> set vs. finite (Pos v)"
shows "finite (Pos (Stars vs))"
using assms
apply(induct vs)
apply(simp)
apply(simp)
apply(subgoal_tac "finite (Pos (Stars vs) - {[]})")
apply(rule_tac f="\<lambda>l. Suc (hd l) # tl l" in finite_surj)
apply(assumption)
back
apply(auto simp add: image_def)
apply(rule_tac x="n#ps" in bexI)
apply(simp)
apply(simp)
done
lemma Pos_finite:
shows "finite (Pos v)"
apply(induct v rule: val.induct)
apply(auto)
apply(simp add: Pos_finite_aux)
done
lemma ato_test:
assumes "p \<in> Pos v"
shows "\<exists>v'. ato v p = Some v'"
using assms
apply(induct v arbitrary: p rule: Pos.induct)
apply(auto)
apply force
by (metis ato.simps(6) option.distinct(1))
definition pflat :: "val \<Rightarrow> nat list => string option"
where
"pflat v p \<equiv> (if p \<in> Pos v then Some (flat (at v p)) else None)"
fun intlen :: "'a list \<Rightarrow> int"
where
"intlen [] = 0"
| "intlen (x#xs) = 1 + intlen xs"
lemma inlen_bigger:
shows "0 \<le> intlen xs"
apply(induct xs)
apply(auto)
done
lemma intlen_append:
shows "intlen (xs @ ys) = intlen xs + intlen ys"
apply(induct xs arbitrary: ys)
apply(auto)
done
lemma intlen_length:
assumes "length xs < length ys"
shows "intlen xs < intlen ys"
using assms
apply(induct xs arbitrary: ys)
apply(auto)
apply(case_tac ys)
apply(simp_all)
apply (smt inlen_bigger)
by (smt Suc_lessE intlen.simps(2) length_Suc_conv)
definition pflat_len :: "val \<Rightarrow> nat list => int"
where
"pflat_len v p \<equiv> (if p \<in> Pos v then intlen (flat (at v p)) else -1)"
lemma pflat_len_simps:
shows "pflat_len (Seq v1 v2) (0#p) = pflat_len v1 p"
and "pflat_len (Seq v1 v2) (Suc 0#p) = pflat_len v2 p"
and "pflat_len (Left v) (0#p) = pflat_len v p"
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 v [] = intlen (flat v)"
apply(auto simp add: pflat_len_def Pos_empty)
done
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 Two_to_Three_aux:
assumes "p \<in> Pos v1 \<union> Pos v2" "pflat_len v1 p = pflat_len v2 p"
shows "p \<in> Pos v1 \<inter> Pos v2"
using assms
apply(simp add: pflat_len_def)
apply(auto split: if_splits)
apply (smt inlen_bigger)+
done
lemma Two_to_Three:
assumes "\<forall>p \<in> Pos v1 \<union> Pos v2. pflat v1 p = pflat v2 p"
shows "Pos v1 = Pos v2"
using assms
by (metis Un_iff option.distinct(1) pflat_def subsetI subset_antisym)
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"
using assms
by (metis Un_iff inlen_bigger neg_0_le_iff_le not_one_le_zero pflat_len_def subsetI subset_antisym)
lemma set_eq1:
assumes "insert [] A = insert [] B" "[] \<notin> A" "[] \<notin> B"
shows "A = B"
using assms
by (simp add: insert_ident)
lemma set_eq2:
assumes "A \<union> B = A \<union> C"
and "A \<inter> B = {}" "A \<inter> C = {}"
shows "B = C"
using assms
using Un_Int_distrib sup_bot.left_neutral sup_commute by blast
lemma Three_to_One:
assumes "\<turnstile> v1 : r" "\<turnstile> v2 : r"
and "Pos v1 = Pos v2"
shows "v1 = v2"
using assms
apply(induct v1 arbitrary: r v2 rule: Pos.induct)
apply(erule Prf.cases)
apply(simp_all)
apply(erule Prf.cases)
apply(simp_all)
apply(erule Prf.cases)
apply(simp_all)
apply(erule Prf.cases)
apply(simp_all)
apply(erule Prf.cases)
apply(simp_all)
apply(erule Prf.cases)
apply(simp_all)
apply(clarify)
apply(simp add: insert_ident)
apply(drule_tac x="r1a" in meta_spec)
apply(drule_tac x="v1a" in meta_spec)
apply(simp)
apply(drule_tac meta_mp)
thm subset_antisym
apply(rule subset_antisym)
apply(auto)[3]
apply(clarify)
apply(simp add: insert_ident)
using Pos_empty apply blast
apply(erule Prf.cases)
apply(simp_all)
apply(erule Prf.cases)
apply(simp_all)
apply(clarify)
apply(simp add: insert_ident)
using Pos_empty apply blast
apply(simp add: insert_ident)
apply(drule_tac x="r2a" in meta_spec)
apply(drule_tac x="v2b" in meta_spec)
apply(simp)
apply(drule_tac meta_mp)
apply(rule subset_antisym)
apply(auto)[3]
apply(erule Prf.cases)
apply(simp_all)
apply(erule Prf.cases)
apply(simp_all)
apply(simp add: insert_ident)
apply(clarify)
apply(drule_tac x="r1a" in meta_spec)
apply(drule_tac x="r2a" in meta_spec)
apply(drule_tac x="v1b" in meta_spec)
apply(drule_tac x="v2c" in meta_spec)
apply(simp)
apply(drule_tac meta_mp)
apply(rule subset_antisym)
apply(rule subsetI)
apply(subgoal_tac "0 # x \<in> {0 # ps |ps. ps \<in> Pos v1a}")
prefer 2
apply(auto)[1]
apply(subgoal_tac "0 # x \<in> {0 # ps |ps. ps \<in> Pos v1b} \<union> {Suc 0 # ps |ps. ps \<in> Pos v2c}")
prefer 2
apply (metis (no_types, lifting) Un_iff)
apply(simp)
apply(rule subsetI)
apply(subgoal_tac "0 # x \<in> {0 # ps |ps. ps \<in> Pos v1b}")
prefer 2
apply(auto)[1]
apply(subgoal_tac "0 # x \<in> {0 # ps |ps. ps \<in> Pos v1a} \<union> {Suc 0 # ps |ps. ps \<in> Pos v2b}")
prefer 2
apply (metis (no_types, lifting) Un_iff)
apply(simp (no_asm_use))
apply(simp)
apply(drule_tac meta_mp)
apply(rule subset_antisym)
apply(rule subsetI)
apply(subgoal_tac "Suc 0 # x \<in> {Suc 0 # ps |ps. ps \<in> Pos v2b}")
prefer 2
apply(auto)[1]
apply(subgoal_tac "Suc 0 # x \<in> {0 # ps |ps. ps \<in> Pos v1b} \<union> {Suc 0 # ps |ps. ps \<in> Pos v2c}")
prefer 2
apply (metis (no_types, lifting) Un_iff)
apply(simp)
apply(rule subsetI)
apply(subgoal_tac "Suc 0 # x \<in> {Suc 0 # ps |ps. ps \<in> Pos v2c}")
prefer 2
apply(auto)[1]
apply(subgoal_tac "Suc 0 # x \<in> {0 # ps |ps. ps \<in> Pos v1b} \<union> {Suc 0 # ps |ps. ps \<in> Pos v2b}")
prefer 2
apply (metis (no_types, lifting) Un_iff)
apply(simp (no_asm_use))
apply(simp)
apply(erule Prf.cases)
apply(simp_all)
apply(erule Prf.cases)
apply(simp_all)
apply(auto)[1]
using Pos_empty apply fastforce
apply(erule Prf.cases)
apply(simp_all)
apply(erule Prf.cases)
apply(simp_all)
apply(auto)[1]
using Pos_empty apply fastforce
apply(clarify)
apply(simp add: insert_ident)
apply(drule_tac x="rb" in meta_spec)
apply(drule_tac x="STAR rb" in meta_spec)
apply(drule_tac x="vb" in meta_spec)
apply(drule_tac x="Stars vsb" in meta_spec)
apply(simp)
apply(drule_tac meta_mp)
apply(rule subset_antisym)
apply(rule subsetI)
apply(subgoal_tac "0 # x \<in> {0 # ps |ps. ps \<in> Pos va}")
prefer 2
apply(auto)[1]
apply(subgoal_tac "0 # x \<in> {0 # ps |ps. ps \<in> Pos vb} \<union> {Suc n # ps |n ps. n # ps \<in> Pos (Stars vsb)}")
prefer 2
apply (metis (no_types, lifting) Un_iff)
apply(simp)
apply(rule subsetI)
apply(subgoal_tac "0 # x \<in> {0 # ps |ps. ps \<in> Pos vb}")
prefer 2
apply(auto)[1]
apply(subgoal_tac "0 # x \<in> {0 # ps |ps. ps \<in> Pos va} \<union> {Suc n # ps |n ps. n # ps \<in> Pos (Stars vsa)}")
prefer 2
apply (metis (no_types, lifting) Un_iff)
apply(simp (no_asm_use))
apply(simp)
apply(drule_tac meta_mp)
apply(rule subset_antisym)
apply(rule subsetI)
apply(case_tac vsa)
apply(simp)
apply (simp add: Pos_empty)
apply(simp)
apply(clarify)
apply(erule disjE)
apply (simp add: Pos_empty)
apply(erule disjE)
apply(clarify)
apply(subgoal_tac
"Suc 0 # ps \<in> {Suc n # ps |n ps. n = 0 \<and> ps \<in> Pos a \<or> (\<exists>na. n = Suc na \<and> na # ps \<in> Pos (Stars list))}")
prefer 2
apply blast
apply(subgoal_tac "Suc 0 # ps \<in> {0 # ps |ps. ps \<in> Pos vb} \<union> {Suc n # ps |n ps. n # ps \<in> Pos (Stars vsb)}")
prefer 2
apply (metis (no_types, lifting) Un_iff)
apply(simp)
apply(clarify)
apply(subgoal_tac
"Suc (Suc n) # ps \<in> {Suc n # ps |n ps. n = 0 \<and> ps \<in> Pos a \<or> (\<exists>na. n = Suc na \<and> na # ps \<in> Pos (Stars list))}")
prefer 2
apply blast
apply(subgoal_tac "Suc (Suc n) # ps \<in> {0 # ps |ps. ps \<in> Pos vb} \<union> {Suc n # ps |n ps. n # ps \<in> Pos (Stars vsb)}")
prefer 2
apply (metis (no_types, lifting) Un_iff)
apply(simp)
apply(rule subsetI)
apply(case_tac vsb)
apply(simp)
apply (simp add: Pos_empty)
apply(simp)
apply(clarify)
apply(erule disjE)
apply (simp add: Pos_empty)
apply(erule disjE)
apply(clarify)
apply(subgoal_tac
"Suc 0 # ps \<in> {Suc n # ps |n ps. n = 0 \<and> ps \<in> Pos a \<or> (\<exists>na. n = Suc na \<and> na # ps \<in> Pos (Stars list))}")
prefer 2
apply(simp)
apply(subgoal_tac "Suc 0 # ps \<in> {Suc n # ps |n ps. n # ps \<in> Pos (Stars vsa)}")
apply blast
using list.inject apply blast
apply(clarify)
apply(subgoal_tac
"Suc (Suc n) # ps \<in> {Suc n # ps |n ps. n = 0 \<and> ps \<in> Pos a \<or> (\<exists>na. n = Suc na \<and> na # ps \<in> Pos (Stars list))}")
prefer 2
apply(simp)
apply(subgoal_tac "Suc (Suc n) # ps \<in> {0 # ps |ps. ps \<in> Pos vb} \<union> {Suc n # ps |n ps. n # ps \<in> Pos (Stars vsa)}")
prefer 2
apply (metis (no_types, lifting) Un_iff)
apply(simp (no_asm_use))
apply(simp)
done
definition prefix_list:: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" ("_ \<sqsubseteq>pre _")
where
"ps1 \<sqsubseteq>pre ps2 \<equiv> (\<exists>ps'. ps1 @ps' = ps2)"
definition sprefix_list:: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" ("_ \<sqsubset>spre _")
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 _")
where
"[] \<sqsubset>lex p#ps"
| "ps1 \<sqsubset>lex ps2 \<Longrightarrow> (p#ps1) \<sqsubset>lex (p#ps2)"
| "p1 < p2 \<Longrightarrow> (p1#ps1) \<sqsubset>lex (p2#ps2)"
lemma lex_irrfl:
fixes ps1 ps2 :: "nat list"
assumes "ps1 \<sqsubset>lex ps2"
shows "ps1 \<noteq> ps2"
using assms
apply(induct rule: lex_lists.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]:
fixes xs ys :: "nat list"
shows "[] \<sqsubset>lex ys = (ys \<noteq> [])"
and "xs \<sqsubset>lex [] = 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
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(simp_all)
apply(rotate_tac 2)
apply(erule lex_lists.cases)
apply(simp_all)
apply(erule lex_lists.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"
shows "p = q \<or> p \<sqsubset>lex q \<or> q \<sqsubset>lex p"
apply(induct p arbitrary: q)
apply(auto)
apply(case_tac q)
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)"
definition
"DPos v1 v2 \<equiv> {p. dpos v1 v2 p}"
lemma outside_lemma:
assumes "p \<notin> Pos v1 \<union> Pos v2"
shows "pflat_len v1 p = pflat_len v2 p"
using assms
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
lemma DPos_lemma:
assumes "p \<in> DPos v1 v2"
shows "pflat_len v1 p \<noteq> pflat_len v2 p"
using assms
unfolding DPos_def
apply(auto simp add: pflat_len_def dpos_def)
apply (smt inlen_bigger)
by (smt inlen_bigger)
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>
(\<forall>q \<in> Pos v1 \<union> Pos v2. q \<sqsubset>lex p \<longrightarrow> pflat_len v1 q = pflat_len v2 q))"
definition val_ord_ex:: "val \<Rightarrow> val \<Rightarrow> bool" ("_ :\<sqsubset>val _")
where
"v1 :\<sqsubset>val v2 \<equiv> (\<exists>p. v1 \<sqsubset>val p v2)"
definition val_ord_ex1:: "val \<Rightarrow> val \<Rightarrow> bool" ("_ :\<sqsubseteq>val _")
where
"v1 :\<sqsubseteq>val v2 \<equiv> v1 :\<sqsubset>val v2 \<or> v1 = v2"
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
lemma val_ord_ALTI:
assumes "v \<sqsubset>val p v'" "flat v = flat v'"
shows "(Left v) \<sqsubset>val (0#p) (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]
using assms(2)
apply(simp add: pflat_len_simps)
apply(auto simp add: pflat_len_simps)[2]
done
lemma val_ord_ALTI2:
assumes "v \<sqsubset>val p v'" "flat v = flat v'"
shows "(Right v) \<sqsubset>val (1#p) (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]
using assms(2)
apply(simp add: pflat_len_simps)
apply(auto simp add: pflat_len_simps)[2]
done
lemma val_ord_STARI:
assumes "v1 \<sqsubset>val p v2" "flat (Stars (v1#vs1)) = flat (Stars (v2#vs2))"
shows "(Stars (v1#vs1)) \<sqsubset>val (0#p) (Stars (v2#vs2))"
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(subst pflat_len_Stars_simps)
apply(simp)
apply(subst pflat_len_Stars_simps)
apply(simp)
apply(simp)
apply(rule ballI)
apply(rule impI)
apply(simp)
apply(auto)
using assms(2)
apply(simp add: pflat_len_simps)
apply(auto simp add: pflat_len_Stars_simps)
done
lemma val_ord_STARI2:
assumes "(Stars vs1) \<sqsubset>val n#p (Stars vs2)" "flat (Stars vs1) = flat (Stars vs2)"
shows "(Stars (v#vs1)) \<sqsubset>val (Suc n#p) (Stars (v#vs2))"
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(case_tac vs1)
apply(simp)
apply(simp)
apply(auto)[1]
apply(case_tac vs2)
apply(simp)
apply (simp add: pflat_len_def)
apply(simp)
apply(auto)[1]
apply (simp add: pflat_len_Stars_simps)
using pflat_len_def apply auto[1]
apply(rule ballI)
apply(rule impI)
apply(simp)
using assms(2)
apply(auto)
apply (simp add: pflat_len_simps(7))
apply (simp add: pflat_len_Stars_simps)
using assms(2)
apply(auto simp add: pflat_len_def)[1]
apply force
apply force
apply(auto simp add: pflat_len_def)[1]
apply force
apply force
apply(auto simp add: pflat_len_def)[1]
apply(auto simp add: pflat_len_def)[1]
apply force
apply force
apply(auto simp add: pflat_len_def)[1]
apply force
apply force
done
lemma val_ord_SEQI:
assumes "v1 \<sqsubset>val p v1'" "flat (Seq v1 v2) = flat (Seq v1' v2')"
shows "(Seq v1 v2) \<sqsubset>val (0#p) (Seq v1' v2')"
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]
apply(simp add: pflat_len_simps)
using assms(2)
apply(simp)
apply(auto simp add: pflat_len_simps)[2]
done
lemma val_ord_SEQI2:
assumes "v2 \<sqsubset>val p v2'" "flat v2 = flat v2'"
shows "(Seq v v2) \<sqsubset>val (1#p) (Seq v v2')"
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)
apply(auto simp add: pflat_len_def intlen_append)
apply(auto simp add: assms(2))
done
lemma val_ord_SEQE_0:
assumes "(Seq v1 v2) \<sqsubset>val 0#p (Seq v1' v2')"
shows "v1 \<sqsubset>val p v1'"
using assms(1)
apply(simp add: val_ord_def val_ord_ex_def)
apply(auto)[1]
apply(simp add: pflat_len_simps)
apply(simp add: val_ord_def pflat_len_def)
apply(auto)[1]
apply(drule_tac x="0#q" in bspec)
apply(simp)
apply(simp)
apply(drule_tac x="0#q" in bspec)
apply(simp)
apply(simp)
apply(drule_tac x="0#q" in bspec)
apply(simp)
apply(simp)
apply(simp add: val_ord_def pflat_len_def)
apply(auto)[1]
done
lemma val_ord_SEQE_1:
assumes "(Seq v1 v2) \<sqsubset>val (Suc 0)#p (Seq v1' v2')"
shows "v2 \<sqsubset>val p v2'"
using assms(1)
apply(simp add: val_ord_def pflat_len_def)
apply(auto)[1]
apply(drule_tac x="1#q" in bspec)
apply(simp)
apply(simp)
apply(drule_tac x="1#q" in bspec)
apply(simp)
apply(simp)
apply(drule_tac x="1#q" in bspec)
apply(simp)
apply(auto)[1]
apply(drule_tac x="1#q" in bspec)
apply(simp)
apply(auto)
apply(simp add: intlen_append)
apply force
apply(simp add: intlen_append)
apply force
apply(simp add: intlen_append)
apply force
apply(simp add: intlen_append)
apply force
done
lemma val_ord_SEQE_2:
assumes "(Seq v1 v2) \<sqsubset>val (Suc 0)#p (Seq v1' v2')"
and "\<turnstile> v1 : r" "\<turnstile> v1' : r"
shows "v1 = v1'"
proof -
have "\<forall>q \<in> Pos v1 \<union> Pos v1'. 0 # q \<sqsubset>lex 1#p \<longrightarrow> pflat_len v1 q = pflat_len v1' q"
using assms(1)
apply(simp add: val_ord_def)
apply(rule ballI)
apply(clarify)
apply(drule_tac x="0#q" in bspec)
apply(auto)[1]
apply(simp add: pflat_len_simps)
done
then have "Pos v1 = Pos v1'"
apply(rule_tac Two_to_Three_orig)
apply(rule ballI)
apply(drule_tac x="pa" in bspec)
apply(simp)
apply(simp)
done
then show "v1 = v1'"
apply(rule_tac Three_to_One)
apply(rule assms)
apply(rule assms)
apply(simp)
done
qed
lemma val_ord_SEQ:
assumes "(Seq v1 v2) :\<sqsubset>val (Seq v1' v2')"
and "flat (Seq v1 v2) = flat (Seq v1' v2')"
and "\<turnstile> v1 : r" "\<turnstile> v1' : r"
shows "(v1 :\<sqsubset>val v1') \<or> (v1 = v1' \<and> (v2 :\<sqsubset>val v2'))"
using assms(1)
apply(subst (asm) val_ord_ex_def)
apply(erule exE)
apply(simp only: val_ord_def)
apply(simp)
apply(erule conjE)+
apply(erule disjE)
prefer 2
apply(erule disjE)
apply(erule exE)
apply(rule disjI1)
apply(simp)
apply(subst val_ord_ex_def)
apply(rule_tac x="ps" in exI)
apply(rule val_ord_SEQE_0)
apply(simp add: val_ord_def)
apply(erule exE)
apply(rule disjI2)
apply(rule conjI)
thm val_ord_SEQE_1
apply(rule_tac val_ord_SEQE_2)
apply(auto simp add: val_ord_def)[3]
apply(rule assms(3))
apply(rule assms(4))
apply(subst val_ord_ex_def)
apply(rule_tac x="ps" in exI)
apply(rule_tac val_ord_SEQE_1)
apply(auto simp add: val_ord_def)[1]
apply(simp)
using assms(2)
apply(simp add: pflat_len_simps)
done
lemma val_ord_ex_trans:
assumes "v1 :\<sqsubset>val v2" "v2 :\<sqsubset>val v3"
shows "v1 :\<sqsubset>val v3"
using assms
unfolding val_ord_ex_def
apply(clarify)
apply(subgoal_tac "p = pa \<or> p \<sqsubset>lex pa \<or> pa \<sqsubset>lex p")
prefer 2
apply(rule trichotomous)
apply(erule disjE)
apply(simp)
apply(rule_tac x="pa" in exI)
apply(subst val_ord_def)
apply(rule conjI)
apply(simp add: val_ord_def)
apply(auto)[1]
apply(simp add: val_ord_def)
apply(simp add: val_ord_def)
apply(auto)[1]
using outside_lemma apply blast
apply(simp add: val_ord_def)
apply(auto)[1]
using outside_lemma apply force
apply auto[1]
apply(simp add: val_ord_def)
apply(auto)[1]
apply (metis (no_types, hide_lams) lex_trans outside_lemma)
apply(simp add: val_ord_def)
apply(auto)[1]
by (metis IntE Two_to_Three_aux UnCI lex_trans outside_lemma)
definition fdpos :: "val \<Rightarrow> val \<Rightarrow> nat list \<Rightarrow> bool"
where
"fdpos v1 v2 p \<equiv> ({q. q \<sqsubset>lex p} \<inter> DPos v1 v2 = {})"
lemma pos_append:
assumes "p @ q \<in> Pos v"
shows "q \<in> Pos (at v p)"
using assms
apply(induct arbitrary: p q rule: Pos.induct)
apply(simp_all)
apply(auto)[1]
apply(simp add: append_eq_Cons_conv)
apply(auto)[1]
apply(auto)[1]
apply(simp add: append_eq_Cons_conv)
apply(auto)[1]
apply(auto)[1]
apply(simp add: append_eq_Cons_conv)
apply(auto)[1]
apply(simp add: append_eq_Cons_conv)
apply(auto)[1]
apply(auto)[1]
apply(simp add: append_eq_Cons_conv)
apply(auto)[1]
apply(simp add: append_eq_Cons_conv)
apply(auto)[1]
by (metis append_Cons at.simps(6))
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
"\<lbrakk>\<Turnstile> v1 : r1; \<Turnstile> v2 : r2\<rbrakk> \<Longrightarrow> \<Turnstile> Seq v1 v2 : SEQ r1 r2"
| "\<Turnstile> v1 : r1 \<Longrightarrow> \<Turnstile> Left v1 : ALT r1 r2"
| "\<Turnstile> v2 : r2 \<Longrightarrow> \<Turnstile> Right v2 : ALT r1 r2"
| "\<Turnstile> Void : ONE"
| "\<Turnstile> Char c : CHAR c"
| "\<Turnstile> Stars [] : STAR r"
| "\<lbrakk>\<Turnstile> v : r; flat v \<noteq> []; \<Turnstile> Stars vs : STAR r\<rbrakk> \<Longrightarrow> \<Turnstile> Stars (v # vs) : STAR r"
lemma Prf_CPrf:
assumes "\<Turnstile> v : r"
shows "\<turnstile> v : r"
using assms
apply(induct)
apply(auto intro: Prf.intros)
done
definition
"CPT r s = {v. flat v = s \<and> \<Turnstile> v : r}"
definition
"CPTpre r s = {v. \<exists>s'. flat v @ s' = s \<and> \<Turnstile> v : r}"
lemma CPT_CPTpre_subset:
shows "CPT r s \<subseteq> CPTpre r s"
apply(auto simp add: CPT_def CPTpre_def)
done
lemma CPTpre_subsets:
"CPTpre ZERO s = {}"
"CPTpre ONE s \<subseteq> {Void}"
"CPTpre (CHAR c) s \<subseteq> {Char c}"
"CPTpre (ALT r1 r2) s \<subseteq> Left ` CPTpre r1 s \<union> Right ` CPTpre r2 s"
"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)}"
"CPTpre (STAR r) s \<subseteq> {Stars []} \<union>
{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)}"
"CPTpre (STAR r) [] = {Stars []}"
apply(auto simp add: CPTpre_def)
apply(erule CPrf.cases)
apply(simp_all)
apply(erule CPrf.cases)
apply(simp_all)
apply(erule CPrf.cases)
apply(simp_all)
apply(erule CPrf.cases)
apply(simp_all)
apply(erule CPrf.cases)
apply(simp_all)
apply(erule CPrf.cases)
apply(simp_all)
apply(erule CPrf.cases)
apply(simp_all)
apply(rule CPrf.intros)
done
lemma CPTpre_simps:
shows "CPTpre ONE s = {Void}"
and "CPTpre (CHAR c) (d#s) = (if c = d then {Char c} else {})"
and "CPTpre (ALT r1 r2) s = Left ` CPTpre r1 s \<union> Right ` CPTpre r2 s"
and "CPTpre (SEQ r1 r2) s =
{Seq v1 v2 | v1 v2. v1 \<in> CPTpre r1 s \<and> v2 \<in> CPTpre r2 (drop (length (flat v1)) s)}"
apply -
apply(rule subset_antisym)
apply(rule CPTpre_subsets)
apply(auto simp add: CPTpre_def intro: "CPrf.intros")[1]
apply(case_tac "c = d")
apply(simp)
apply(rule subset_antisym)
apply(rule CPTpre_subsets)
apply(auto simp add: CPTpre_def intro: CPrf.intros)[1]
apply(simp)
apply(auto simp add: CPTpre_def intro: CPrf.intros)[1]
apply(erule CPrf.cases)
apply(simp_all)
apply(rule subset_antisym)
apply(rule CPTpre_subsets)
apply(auto simp add: CPTpre_def intro: CPrf.intros)[1]
apply(rule subset_antisym)
apply(rule CPTpre_subsets)
apply(auto simp add: CPTpre_def intro: CPrf.intros)[1]
done
lemma CPT_simps:
shows "CPT ONE s = (if s = [] then {Void} else {})"
and "CPT (CHAR c) [d] = (if c = d then {Char c} else {})"
and "CPT (ALT r1 r2) s = Left ` CPT r1 s \<union> Right ` CPT r2 s"
and "CPT (SEQ r1 r2) s =
{Seq v1 v2 | v1 v2 s1 s2. s1 @ s2 = s \<and> v1 \<in> CPT r1 s1 \<and> v2 \<in> CPT r2 s2}"
apply -
apply(rule subset_antisym)
apply(auto simp add: CPT_def)[1]
apply(erule CPrf.cases)
apply(simp_all)[7]
apply(erule CPrf.cases)
apply(simp_all)[7]
apply(auto simp add: CPT_def intro: CPrf.intros)[1]
apply(auto simp add: CPT_def intro: CPrf.intros)[1]
apply(erule CPrf.cases)
apply(simp_all)[7]
apply(erule CPrf.cases)
apply(simp_all)[7]
apply(auto simp add: CPT_def image_def intro: CPrf.intros)[1]
apply(erule CPrf.cases)
apply(simp_all)[7]
apply(clarify)
apply blast
apply(auto simp add: CPT_def image_def intro: CPrf.intros)[1]
apply(erule CPrf.cases)
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))
lemma Cond_prefix:
assumes "\<forall>s\<^sub>3. s1 @ s\<^sub>3 \<in> L r1 \<longrightarrow> s\<^sub>3 = [] \<or> (\<forall>s\<^sub>4. s1 @ s\<^sub>3 @ s\<^sub>4 \<sqsubseteq>pre s1 @ s2 \<longrightarrow> s\<^sub>4 \<notin> L r2)"
and "t1 \<in> L r1" "t2 \<in> L r2" "t1 @ t2 \<sqsubseteq>pre s1 @ s2"
shows "t1 \<sqsubseteq>pre s1"
using assms
apply(auto simp add: Sequ_def prefix_list_def append_eq_append_conv2)
done
lemma CPTpre_test:
assumes "s \<in> r \<rightarrow> v"
shows "\<not>(\<exists>v' \<in> CPT r s. v :\<sqsubset>val v')"
using assms
apply(induct r arbitrary: s v rule: rexp.induct)
apply(erule Posix.cases)
apply(simp_all)
apply(erule Posix.cases)
apply(simp_all)
apply(simp add: CPT_simps)
apply(simp add: val_ord_def val_ord_ex_def)
apply(erule Posix.cases)
apply(simp_all)
apply(simp add: CPT_simps)
apply (simp add: val_ord_def val_ord_ex_def)
(* SEQ *)
apply(rule ballI)
apply(erule Posix.cases)
apply(simp_all)
apply(clarify)
apply(subst (asm) CPT_simps)
apply(simp)
apply(clarify)
thm val_ord_SEQ
apply(drule_tac ?r="r1" in val_ord_SEQ)
apply(simp)
apply (simp add: CPT_def Posix1(2))
apply (simp add: Posix1a)
apply (simp add: CPT_def Posix1a)
using Prf_CPrf apply auto[1]
apply(erule disjE)
apply(drule_tac x="s1" in meta_spec)
apply(drule_tac x="v1" in meta_spec)
apply(simp)
apply(drule_tac x="v1a" in bspec)
apply(subgoal_tac "s1 = s1a")
apply(simp)
apply(auto simp add: append_eq_append_conv2)[1]
apply (metis (mono_tags, lifting) CPT_def L_flat_Prf1 Prf_CPrf append_Nil append_Nil2 mem_Collect_eq)
apply(simp add: CPT_def)
apply(auto)[1]
oops
lemma test:
assumes "finite A"
shows "finite {vs. Stars vs \<in> A}"
using assms
apply(induct A)
apply(simp)
apply(auto)
apply(case_tac x)
apply(simp_all)
done
lemma CPTpre_STAR_finite:
assumes "\<And>s. finite (CPTpre r s)"
shows "finite (CPTpre (STAR r) s)"
apply(induct s rule: length_induct)
apply(case_tac xs)
apply(simp)
apply(simp add: CPTpre_subsets)
apply(rule finite_subset)
apply(rule CPTpre_subsets)
apply(simp)
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)
apply(auto)[1]
apply(rule finite_imageI)
apply(simp add: Collect_case_prod_Sigma)
apply(rule finite_SigmaI)
apply(rule assms)
apply(case_tac "flat v = []")
apply(simp)
apply(drule_tac x="drop (length (flat v)) (a # list)" in spec)
apply(simp)
apply(auto)[1]
apply(rule test)
apply(simp)
done
lemma CPTpre_finite:
shows "finite (CPTpre r s)"
apply(induct r arbitrary: s)
apply(simp add: CPTpre_subsets)
apply(rule finite_subset)
apply(rule CPTpre_subsets)
apply(simp)
apply(rule finite_subset)
apply(rule CPTpre_subsets)
apply(simp)
sorry
lemma CPT_finite:
shows "finite (CPT r s)"
apply(rule finite_subset)
apply(rule CPT_CPTpre_subset)
apply(rule CPTpre_finite)
done
lemma Posix_CPT:
assumes "s \<in> r \<rightarrow> v"
shows "v \<in> CPT r s"
using assms
apply(induct rule: Posix.induct)
apply(simp add: CPT_def)
apply(rule CPrf.intros)
apply(simp add: CPT_def)
apply(rule CPrf.intros)
apply(simp add: CPT_def)
apply(rule CPrf.intros)
apply(simp)
apply(simp add: CPT_def)
apply(rule CPrf.intros)
apply(simp)
apply(simp add: CPT_def)
apply(rule CPrf.intros)
apply(simp)
apply(simp)
apply(simp add: CPT_def)
apply(rule CPrf.intros)
apply(simp)
apply(simp)
apply(simp)
apply(simp add: CPT_def)
apply(rule CPrf.intros)
done
lemma Posix_val_ord:
assumes "s \<in> r \<rightarrow> v1" "v2 \<in> CPTpre r s"
shows "v1 :\<sqsubseteq>val v2"
using assms
apply(induct arbitrary: v2 rule: Posix.induct)
apply(simp add: CPTpre_def)
apply(clarify)
apply(erule CPrf.cases)
apply(simp_all)
apply(simp add: val_ord_ex1_def)
apply(simp add: CPTpre_def)
apply(clarify)
apply(erule CPrf.cases)
apply(simp_all)
apply(simp add: val_ord_ex1_def)
(* ALT1 *)
prefer 3
(* SEQ case *)
apply(subst (asm) (3) CPTpre_def)
apply(clarify)
apply(erule CPrf.cases)
apply(simp_all)
apply(case_tac "s' = []")
apply(simp)
prefer 2
apply(simp add: val_ord_ex1_def)
apply(clarify)
apply(simp)
apply(simp add: val_ord_ex_def)
apply(simp (no_asm) add: val_ord_def)
apply(rule_tac x="[]" in exI)
apply(simp add: pflat_len_simps)
apply(rule intlen_length)
apply (metis Posix1(2) append_assoc append_eq_conv_conj drop_eq_Nil not_le)
apply(subgoal_tac "length (flat v1a) \<le> length s1")
prefer 2
apply (metis L_flat_Prf1 Prf_CPrf append_eq_append_conv_if append_take_drop_id drop_eq_Nil)
apply(subst (asm) append_eq_append_conv_if)
apply(simp)
apply(clarify)
apply(drule_tac x="v1a" in meta_spec)
apply(drule meta_mp)
apply(auto simp add: CPTpre_def)[1]
using append_eq_conv_conj apply blast
apply(subst (asm) (2)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="0#p" in exI)
apply(rule val_ord_SEQI)
apply(simp)
apply(simp)
apply (metis Posix1(2) append_assoc append_take_drop_id)
apply(simp)
apply(drule_tac x="v2b" in meta_spec)
apply(drule meta_mp)
apply(auto simp add: CPTpre_def)[1]
apply (simp add: Posix1(2))
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_SEQI2)
apply(simp)
apply (simp add: Posix1(2))
apply(subst val_ord_ex1_def)
apply(simp)
(* ALT *)
apply(subst (asm) (2) CPTpre_def)
apply(clarify)
apply(erule CPrf.cases)
apply(simp_all)
apply(clarify)
apply(case_tac "s' = []")
apply(simp)
apply(drule_tac x="v1" in meta_spec)
apply(drule meta_mp)
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="0#p" in exI)
apply(rule val_ord_ALTI)
apply(simp)
using Posix1(2) apply blast
using val_ord_ex1_def apply blast
apply(subst val_ord_ex1_def)
apply(rule disjI1)
apply (simp add: Posix1(2) val_ord_shorterI)
apply(subst val_ord_ex1_def)
apply(rule disjI1)
apply(case_tac "s' = []")
apply(simp)
apply(subst val_ord_ex_def)
apply(rule_tac x="[0]" 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 (smt inlen_bigger)
apply(simp)
apply(rule conjI)
apply(simp add: pflat_len_simps)
using Posix1(2) apply auto[1]
apply(rule ballI)
apply(rule impI)
apply(case_tac "q = []")
using Posix1(2) apply auto[1]
apply(auto)[1]
apply(rule val_ord_shorterI)
apply(simp)
apply (simp add: Posix1(2))
(* ALT RIGHT *)
apply(subst (asm) (2) CPTpre_def)
apply(clarify)
apply(erule CPrf.cases)
apply(simp_all)
apply(clarify)
apply(case_tac "s' = []")
apply(simp)
apply (simp add: L_flat_Prf1 Prf_CPrf)
apply(subst val_ord_ex1_def)
apply(rule disjI1)
apply(rule val_ord_shorterI)
apply(simp)
apply (simp add: Posix1(2))
apply(case_tac "s' = []")
apply(simp)
apply(drule_tac x="v2a" in meta_spec)
apply(drule meta_mp)
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(simp)
using Posix1(2) apply blast
apply (simp add: val_ord_ex1_def)
apply(subst val_ord_ex1_def)
apply(rule disjI1)
apply(rule val_ord_shorterI)
apply(simp)
apply (simp add: Posix1(2))
(* STAR empty case *)
prefer 2
apply(subst (asm) CPTpre_def)
apply(clarify)
apply(erule CPrf.cases)
apply(simp_all)
apply(clarify)
apply (simp add: val_ord_ex1_def)
(* STAR non-empty case *)
apply(subst (asm) (3) CPTpre_def)
apply(clarify)
apply(erule CPrf.cases)
apply(simp_all)
apply(clarify)
apply (simp add: val_ord_ex1_def)
apply(rule val_ord_shorterI)
apply(simp)
apply(case_tac "s' = []")
apply(simp)
prefer 2
apply (simp add: val_ord_ex1_def)
apply(rule disjI1)
apply(rule val_ord_shorterI)
apply(simp)
apply (metis Posix1(2) append_assoc append_eq_conv_conj drop_all flat.simps(7) flat_Stars length_append not_less)
apply(drule_tac x="va" in meta_spec)
apply(drule meta_mp)
apply(auto simp add: CPTpre_def)[1]
apply (smt L.simps(6) L_flat_Prf1 Prf_CPrf append_eq_append_conv2 flat_Stars self_append_conv)
apply (subst (asm) (2) val_ord_ex1_def)
apply(erule disjE)
prefer 2
apply(simp)
apply(drule_tac x="Stars vsa" in meta_spec)
apply(drule meta_mp)
apply(auto simp add: CPTpre_def)[1]
apply (simp add: Posix1(2))
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(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)
using Posix1(2) val_ord_STARI2 apply fastforce
apply(simp add: val_ord_ex1_def)
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)
by (metis Posix1(2) flat.simps(7) flat_Stars val_ord_STARI)
lemma Posix_val_ord_stronger:
assumes "s \<in> r \<rightarrow> v1" "v2 \<in> CPT r s"
shows "v1 :\<sqsubseteq>val v2"
using assms
apply(rule_tac Posix_val_ord)
apply(assumption)
apply(simp add: CPTpre_def CPT_def)
done
definition Minval :: "rexp \<Rightarrow> string \<Rightarrow> val \<Rightarrow> bool"
where
"Minval r s v \<equiv> \<Turnstile> v : r \<and> flat v = s \<and> (\<forall>v' \<in> CPT r s. v :\<sqsubset>val v' \<or> v = v')"
lemma
assumes "s \<in> L(r)"
shows "\<exists>v. Minval r s v"
using assms
apply(induct r arbitrary: s)
apply(simp)
apply(simp)
apply(rule_tac x="Void" in exI)
apply(simp add: Minval_def)
apply(rule conjI)
apply (simp add: CPrf.intros(4))
apply(clarify)
apply(simp add: CPT_def)
apply(auto)[1]
apply(erule CPrf.cases)
apply(simp_all)
apply(rule_tac x="Char x" in exI)
apply(simp add: Minval_def)
apply(rule conjI)
apply (simp add: CPrf.intros)
apply(clarify)
apply(simp add: CPT_def)
apply(auto)[1]
apply(erule CPrf.cases)
apply(simp_all)
prefer 2
apply(auto)[1]
apply(drule_tac x="s" in meta_spec)
apply(simp)
apply(clarify)
apply(rule_tac x="Left x" in exI)
apply(simp (no_asm) add: Minval_def)
apply(rule conjI)
apply (simp add: CPrf.intros(2) Minval_def)
apply(rule conjI)
apply(simp add: Minval_def)
apply(clarify)
apply(simp add: CPT_def)
apply(auto)[1]
apply(erule CPrf.cases)
apply(simp_all)
apply(simp add: val_ord_ex_def)
apply(simp only: val_ord_def)
oops
lemma
"wf {(v1, v2). v1 \<in> CPT r s \<and> v2 \<in> CPT r s \<and> (v1 :\<sqsubset>val v2)}"
apply(rule wfI)
oops
inductive ValOrd :: "val \<Rightarrow> rexp \<Rightarrow> val \<Rightarrow> bool" ("_ \<preceq>_ _" [100, 100, 100] 100)
where
C2: "v1 \<preceq>r1 v1' \<Longrightarrow> (Seq v1 v2) \<preceq>(SEQ r1 r2) (Seq v1' v2')"
| C1: "v2 \<preceq>r2 v2' \<Longrightarrow> (Seq v1 v2) \<preceq>(SEQ r1 r2) (Seq v1 v2')"
| A1: "length (flat v2) > length (flat v1) \<Longrightarrow> (Right v2) \<preceq>(ALT r1 r2) (Left v1)"
| A2: "length (flat v1) \<ge> length (flat v2) \<Longrightarrow> (Left v1) \<preceq>(ALT r1 r2) (Right v2)"
| A3: "v2 \<preceq>r2 v2' \<Longrightarrow> (Right v2) \<preceq>(ALT r1 r2) (Right v2')"
| A4: "v1 \<preceq>r1 v1' \<Longrightarrow> (Left v1) \<preceq>(ALT r1 r2) (Left v1')"
| K1: "flat (Stars (v # vs)) = [] \<Longrightarrow> (Stars []) \<preceq>(STAR r) (Stars (v # vs))"
| K2: "flat (Stars (v # vs)) \<noteq> [] \<Longrightarrow> (Stars (v # vs)) \<preceq>(STAR r) (Stars [])"
| K3: "v1 \<preceq>r v2 \<Longrightarrow> (Stars (v1 # vs1)) \<preceq>(STAR r) (Stars (v2 # vs2))"
| K4: "(Stars vs1) \<preceq>(STAR r) (Stars vs2) \<Longrightarrow> (Stars (v # vs1)) \<preceq>(STAR r) (Stars (v # vs2))"
| MY1: "Void \<preceq>ONE Void"
| MY2: "(Char c) \<preceq>(CHAR c) (Char c)"
| MY3: "(Stars []) \<preceq>(STAR r) (Stars [])"
lemma ValOrd_refl:
assumes "\<turnstile> v : r"
shows "v \<preceq>r v"
using assms
apply(induct r rule: Prf.induct)
apply(rule ValOrd.intros)
apply(simp)
apply(rule ValOrd.intros)
apply(simp)
apply(rule ValOrd.intros)
apply(simp)
apply(rule ValOrd.intros)
apply(rule ValOrd.intros)
apply(rule ValOrd.intros)
apply(rule ValOrd.intros)
apply(simp)
done
lemma Posix_CPT2:
assumes "v1 \<preceq>r v2" "flat v1 = flat v2"
shows "v2 :\<sqsubset>val v1 \<or> v1 = v2"
using assms
apply(induct r arbitrary: v1 v2 rule: rexp.induct)
apply(erule ValOrd.cases)
apply(simp_all)
apply(erule ValOrd.cases)
apply(simp_all)
apply(erule ValOrd.cases)
apply(simp_all)
apply(erule ValOrd.cases)
apply(simp_all)
apply(clarify)
(* HERE *)
apply(simp)
apply(subst val_ord_ex_def)
apply(simp)
apply(drule_tac x="v2a" in meta_spec)
apply(rotate_tac 5)
apply(drule_tac x="v2'" in meta_spec)
apply(rule_tac x="0#p" in exI)
apply(rule val_ord_SEQI)
apply(drule_tac r="r1a" in val_ord_SEQ)
apply(simp)
apply(auto)[1]
lemma Posix_CPT:
assumes "v1 :\<sqsubset>val v2" "v1 \<in> CPT r s" "v2 \<in> CPT r s"
shows "v1 \<preceq>r v2"
using assms
apply(induct r arbitrary: v1 v2 s rule: rexp.induct)
apply(simp add: CPT_def)
apply(clarify)
apply(erule CPrf.cases)
apply(simp_all)
apply(simp add: CPT_def)
apply(clarify)
apply(erule CPrf.cases)
apply(simp_all)
apply(erule CPrf.cases)
apply(simp_all)
apply(rule ValOrd.intros)
apply(simp add: CPT_def)
apply(clarify)
apply(erule CPrf.cases)
apply(simp_all)
apply(erule CPrf.cases)
apply(simp_all)
apply(rule ValOrd.intros)
(*SEQ case *)
apply(simp add: CPT_def)
apply(clarify)
apply(erule CPrf.cases)
apply(simp_all)
apply(clarify)
apply(erule CPrf.cases)
apply(simp_all)
apply(clarify)
thm val_ord_SEQ
apply(drule_tac r="r1a" in val_ord_SEQ)
apply(simp)
using Prf_CPrf apply blast
using Prf_CPrf apply blast
apply(erule disjE)
apply(rule C2)
prefer 2
apply(simp)
apply(rule C1)
apply blast
apply(simp add: append_eq_append_conv2)
apply(clarify)
apply(auto)[1]
apply(drule_tac x="v1a" in meta_spec)
apply(rotate_tac 8)
apply(drule_tac x="v1b" in meta_spec)
apply(rotate_tac 8)
apply(simp)
(* HERE *)
apply(subst (asm) (3) val_ord_ex_def)
apply(clarify)
apply(subst (asm) val_ord_def)
apply(clarify)
apply(rule ValOrd.intros)
apply(simp add: val_ord_ex_def)
oops
lemma ValOrd_trans:
assumes "x \<preceq>r y" "y \<preceq>r z"
and "x \<in> CPT r s" "y \<in> CPT r s" "z \<in> CPT r s"
shows "x \<preceq>r z"
using assms
apply(induct x r y arbitrary: s z rule: ValOrd.induct)
apply(rotate_tac 2)
apply(erule ValOrd.cases)
apply(simp_all)[13]
apply(rule ValOrd.intros)
apply(drule_tac x="s" in meta_spec)
apply(drule_tac x="v1'a" in meta_spec)
apply(drule_tac meta_mp)
apply(simp)
apply(drule_tac meta_mp)
apply(simp add: CPT_def)
oops
lemma ValOrd_preorder:
"preorder_on (CPT r s) {(v1, v2). v1 \<preceq>r v2 \<and> v1 \<in> (CPT r s) \<and> v2 \<in> (CPT r s)}"
apply(simp add: preorder_on_def)
apply(rule conjI)
apply(simp add: refl_on_def)
apply(auto)
apply(rule ValOrd_refl)
apply(simp add: CPT_def)
apply(rule Prf_CPrf)
apply(auto)[1]
apply(simp add: trans_def)
apply(auto)
definition ValOrdEq :: "val \<Rightarrow> rexp \<Rightarrow> val \<Rightarrow> bool" ("_ \<ge>_ _" [100, 100, 100] 100)
where
"v\<^sub>1 \<ge>r v\<^sub>2 \<equiv> v\<^sub>1 = v\<^sub>2 \<or> (v\<^sub>1 >r v\<^sub>2 \<and> flat v\<^sub>1 = flat v\<^sub>2)"
(*
inductive ValOrd :: "val \<Rightarrow> rexp \<Rightarrow> val \<Rightarrow> bool" ("_ \<succ>_ _" [100, 100, 100] 100)
where
"v2 \<succ>r2 v2' \<Longrightarrow> (Seq v1 v2) \<succ>(SEQ r1 r2) (Seq v1 v2')"
| "\<lbrakk>v1 \<succ>r1 v1'; v1 \<noteq> v1'\<rbrakk> \<Longrightarrow> (Seq v1 v2) \<succ>(SEQ r1 r2) (Seq v1' v2')"
| "length (flat v1) \<ge> length (flat v2) \<Longrightarrow> (Left v1) \<succ>(ALT r1 r2) (Right v2)"
| "length (flat v2) > length (flat v1) \<Longrightarrow> (Right v2) \<succ>(ALT r1 r2) (Left v1)"
| "v2 \<succ>r2 v2' \<Longrightarrow> (Right v2) \<succ>(ALT r1 r2) (Right v2')"
| "v1 \<succ>r1 v1' \<Longrightarrow> (Left v1) \<succ>(ALT r1 r2) (Left v1')"
| "Void \<succ>EMPTY Void"
| "(Char c) \<succ>(CHAR c) (Char c)"
| "flat (Stars (v # vs)) = [] \<Longrightarrow> (Stars []) \<succ>(STAR r) (Stars (v # vs))"
| "flat (Stars (v # vs)) \<noteq> [] \<Longrightarrow> (Stars (v # vs)) \<succ>(STAR r) (Stars [])"
| "\<lbrakk>v1 \<succ>r v2; v1 \<noteq> v2\<rbrakk> \<Longrightarrow> (Stars (v1 # vs1)) \<succ>(STAR r) (Stars (v2 # vs2))"
| "(Stars vs1) \<succ>(STAR r) (Stars vs2) \<Longrightarrow> (Stars (v # vs1)) \<succ>(STAR r) (Stars (v # vs2))"
| "(Stars []) \<succ>(STAR r) (Stars [])"
*)
section {* Bit-Encodings *}
fun
code :: "val \<Rightarrow> rexp \<Rightarrow> bool list"
where
"code Void ONE = []"
| "code (Char c) (CHAR d) = []"
| "code (Left v) (ALT r1 r2) = False # (code v r1)"
| "code (Right v) (ALT r1 r2) = True # (code v r2)"
| "code (Seq v1 v2) (SEQ r1 r2) = (code v1 r1) @ (code v2 r2)"
| "code (Stars []) (STAR r) = [True]"
| "code (Stars (v # vs)) (STAR r) = False # (code v r) @ code (Stars vs) (STAR r)"
fun
Stars_add :: "val \<Rightarrow> val \<Rightarrow> val"
where
"Stars_add v (Stars vs) = Stars (v # vs)"
function
decode' :: "bool list \<Rightarrow> rexp \<Rightarrow> (val * bool list)"
where
"decode' ds ZERO = (Void, [])"
| "decode' ds ONE = (Void, ds)"
| "decode' ds (CHAR d) = (Char d, ds)"
| "decode' [] (ALT r1 r2) = (Void, [])"
| "decode' (False # ds) (ALT r1 r2) = (let (v, ds') = decode' ds r1 in (Left v, ds'))"
| "decode' (True # ds) (ALT r1 r2) = (let (v, ds') = decode' ds r2 in (Right v, ds'))"
| "decode' ds (SEQ r1 r2) = (let (v1, ds') = decode' ds r1 in
let (v2, ds'') = decode' ds' r2 in (Seq v1 v2, ds''))"
| "decode' [] (STAR r) = (Void, [])"
| "decode' (True # ds) (STAR r) = (Stars [], ds)"
| "decode' (False # ds) (STAR r) = (let (v, ds') = decode' ds r in
let (vs, ds'') = decode' ds' (STAR r)
in (Stars_add v vs, ds''))"
by pat_completeness auto
termination
apply(size_change)
oops
term "inv_image (measure(%cs. size cs) <*lex*> measure(%s. size s)) (%(ds,r). (r,ds))"
lemma decode'_smaller:
assumes "decode'_dom (ds, r)"
shows "length (snd (decode' ds r)) \<le> length ds"
using assms
apply(induct ds r)
apply(auto simp add: decode'.psimps split: prod.split)
using dual_order.trans apply blast
by (meson dual_order.trans le_SucI)
termination "decode'"
apply(relation "inv_image (measure(%cs. size cs) <*lex*> measure(%s. size s)) (%(ds,r). (r,ds))")
apply(auto dest!: decode'_smaller)
by (metis less_Suc_eq_le snd_conv)
fun
decode :: "bool list \<Rightarrow> rexp \<Rightarrow> val option"
where
"decode ds r = (let (v, ds') = decode' ds r
in (if ds' = [] then Some v else None))"
lemma decode'_code:
assumes "\<turnstile> v : r"
shows "decode' ((code v r) @ ds) r = (v, ds)"
using assms
by (induct v r arbitrary: ds) (auto)
lemma decode_code:
assumes "\<turnstile> v : r"
shows "decode (code v r) r = Some v"
using assms decode'_code[of _ _ "[]"]
by auto
datatype arexp =
AZERO
| AONE "bool list"
| ACHAR "bool list" char
| ASEQ "bool list" arexp arexp
| AALT "bool list" arexp arexp
| ASTAR "bool list" arexp
fun fuse :: "bool list \<Rightarrow> arexp \<Rightarrow> arexp" where
"fuse bs AZERO = AZERO"
| "fuse bs (AONE cs) = AONE (bs @ cs)"
| "fuse bs (ACHAR cs c) = ACHAR (bs @ cs) c"
| "fuse bs (AALT cs r1 r2) = AALT (bs @ cs) r1 r2"
| "fuse bs (ASEQ cs r1 r2) = ASEQ (bs @ cs) r1 r2"
| "fuse bs (ASTAR cs r) = ASTAR (bs @ cs) r"
fun internalise :: "rexp \<Rightarrow> arexp" where
"internalise ZERO = AZERO"
| "internalise ONE = AONE []"
| "internalise (CHAR c) = ACHAR [] c"
| "internalise (ALT r1 r2) = AALT [] (fuse [False] (internalise r1))
(fuse [True] (internalise r2))"
| "internalise (SEQ r1 r2) = ASEQ [] (internalise r1) (internalise r2)"
| "internalise (STAR r) = ASTAR [] (internalise r)"
fun retrieve :: "arexp \<Rightarrow> val \<Rightarrow> bool list" where
"retrieve (AONE bs) Void = bs"
| "retrieve (ACHAR bs c) (Char d) = bs"
| "retrieve (AALT bs r1 r2) (Left v) = bs @ retrieve r1 v"
| "retrieve (AALT bs r1 r2) (Right v) = bs @ retrieve r2 v"
| "retrieve (ASEQ bs r1 r2) (Seq v1 v2) = bs @ retrieve r1 v1 @ retrieve r2 v2"
| "retrieve (ASTAR bs r) (Stars []) = bs @ [True]"
| "retrieve (ASTAR bs r) (Stars (v#vs)) =
bs @ [False] @ retrieve r v @ retrieve (ASTAR [] r) (Stars vs)"
fun
anullable :: "arexp \<Rightarrow> bool"
where
"anullable (AZERO) = False"
| "anullable (AONE bs) = True"
| "anullable (ACHAR bs c) = False"
| "anullable (AALT bs r1 r2) = (anullable r1 \<or> anullable r2)"
| "anullable (ASEQ bs r1 r2) = (anullable r1 \<and> anullable r2)"
| "anullable (ASTAR bs r) = True"
fun
amkeps :: "arexp \<Rightarrow> bool list"
where
"amkeps(AONE bs) = bs"
| "amkeps(ASEQ bs r1 r2) = bs @ (amkeps r1) @ (amkeps r2)"
| "amkeps(AALT bs r1 r2) = (if anullable(r1) then bs @ (amkeps r1) else bs @ (amkeps r2))"
| "amkeps(ASTAR bs r) = bs @ [True]"
fun
ader :: "char \<Rightarrow> arexp \<Rightarrow> arexp"
where
"ader c (AZERO) = AZERO"
| "ader c (AONE bs) = AZERO"
| "ader c (ACHAR bs d) = (if c = d then AONE bs else AZERO)"
| "ader c (AALT bs r1 r2) = AALT bs (ader c r1) (ader c r2)"
| "ader c (ASEQ bs r1 r2) =
(if anullable r1
then AALT bs (ASEQ [] (ader c r1) r2) (fuse (amkeps r1) (ader c r2))
else ASEQ bs (ader c r1) r2)"
| "ader c (ASTAR bs r) = ASEQ bs (fuse [False] (ader c r)) (ASTAR [] r)"
lemma
assumes "\<turnstile> v : der c r"
shows "Some (injval r c v) = decode (retrieve (ader c (internalise r)) v) r"
using assms
apply(induct c r arbitrary: v rule: der.induct)
apply(simp_all)
apply(erule Prf_elims)
apply(erule Prf_elims)
apply(case_tac "c = d")
apply(simp)
apply(erule Prf_elims)
apply(simp)
apply(simp)
apply(erule Prf_elims)
apply(auto split: prod.splits)[1]
oops
end