Mercurial Mercurial > hg > lexing / comparison
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
thys/Positions.thy
changeset 265 d36be1e356c0
parent 264 e2828c4a1e23
child 266 fff2e1b40dfc
equal deleted inserted replaced
264:e2828c4a1e23 265:d36be1e356c0 
     1    
     1    
     2 theory Positions
 
     2 theory Positions
 
     3   imports "Lexer" 
     3   imports "Lexer" 
     4 begin
 
     4 begin
 
     5 
     5 
     6 
     6 section {* Positions in Values *}
 
     7 section {* Position in values *}
 
       
     8 
     7 
     9 fun 
     8 fun 
    10   at :: "val \<Rightarrow> nat list \<Rightarrow> val"
 
     9   at :: "val \<Rightarrow> nat list \<Rightarrow> val"
 
    11 where
 
    10 where
 
    12   "at v [] = v"
 
    11   "at v [] = v"
 
    14 | "at (Right v) (Suc 0#ps)= at v ps"
 
    13 | "at (Right v) (Suc 0#ps)= at v ps"
 
    15 | "at (Seq v1 v2) (0#ps)= at v1 ps"
 
    14 | "at (Seq v1 v2) (0#ps)= at v1 ps"
 
    16 | "at (Seq v1 v2) (Suc 0#ps)= at v2 ps"
 
    15 | "at (Seq v1 v2) (Suc 0#ps)= at v2 ps"
 
    17 | "at (Stars vs) (n#ps)= at (nth vs n) ps"
 
    16 | "at (Stars vs) (n#ps)= at (nth vs n) ps"
 
    18 
    17 
       
    18 
       
    19 
    19 fun Pos :: "val \<Rightarrow> (nat list) set"
 
    20 fun Pos :: "val \<Rightarrow> (nat list) set"
 
    20 where
 
    21 where
 
    21   "Pos (Void) = {[]}"
 
    22   "Pos (Void) = {[]}"
 
    22 | "Pos (Char c) = {[]}"
 
    23 | "Pos (Char c) = {[]}"
 
    23 | "Pos (Left v) = {[]} \<union> {0#ps | ps. ps \<in> Pos v}"
 
    24 | "Pos (Left v) = {[]} \<union> {0#ps | ps. ps \<in> Pos v}"
 
    24 | "Pos (Right v) = {[]} \<union> {1#ps | ps. ps \<in> Pos v}"
 
    25 | "Pos (Right v) = {[]} \<union> {1#ps | ps. ps \<in> Pos v}"
 
    25 | "Pos (Seq v1 v2) = {[]} \<union> {0#ps | ps. ps \<in> Pos v1} \<union> {1#ps | ps. ps \<in> Pos v2}" 
    26 | "Pos (Seq v1 v2) = {[]} \<union> {0#ps | ps. ps \<in> Pos v1} \<union> {1#ps | ps. ps \<in> Pos v2}" 
    26 | "Pos (Stars []) = {[]}"
 
    27 | "Pos (Stars []) = {[]}"
 
    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)}"
 
    28 | "Pos (Stars (v#vs)) = {[]} \<union> {0#ps | ps. ps \<in> Pos v} \<union> {Suc n#ps | n ps. n#ps \<in> Pos (Stars vs)}"
 
    28 
    29 
       
    30 
    29 lemma Pos_stars:
 
    31 lemma Pos_stars:
 
    30   "Pos (Stars vs) = {[]} \<union> (\<Union>n < length vs. {n#ps | ps. ps \<in> Pos (vs ! n)})"
 
    32   "Pos (Stars vs) = {[]} \<union> (\<Union>n < length vs. {n#ps | ps. ps \<in> Pos (vs ! n)})"
 
    31 apply(induct vs)
 
    33 apply(induct vs)
 
    32 apply(simp) 
    34 apply(simp) 
    33 apply(simp)
 
       
    34 apply(simp add: insert_ident)
 
    35 apply(simp add: insert_ident)
 
    35 apply(rule subset_antisym)
 
    36 apply(rule subset_antisym)
 
    36 apply(auto)
 
       
    37 apply(auto)[1]
 
       
    38 using less_Suc_eq_0_disj by auto
 
    37 using less_Suc_eq_0_disj by auto
 
    39 
    38 
    40 lemma Pos_empty:
 
    39 lemma Pos_empty:
 
    41   shows "[] \<in> Pos v"
 
    40   shows "[] \<in> Pos v"
 
    42 by (induct v rule: Pos.induct)(auto)
 
    41 by (induct v rule: Pos.induct)(auto)
 
    43 
    42 
    44 fun intlen :: "'a list \<Rightarrow> int"
 
    43 fun intlen :: "'a list \<Rightarrow> int"
 
    45 where
 
    44 where
 
    46   "intlen [] = 0"
 
    45   "intlen [] = 0"
 
    47 | "intlen (x#xs) = 1 + intlen xs"
 
    46 | "intlen (x # xs) = 1 + intlen xs"
 
    48 
    47 
    49 lemma intlen_bigger:
 
    48 lemma intlen_bigger:
 
    50   shows "0 \<le> intlen xs"
 
    49   shows "0 \<le> intlen xs"
 
    51 by (induct xs)(auto)
 
    50 by (induct xs)(auto)
 
    52 
    51 
    60 apply (auto simp add: intlen_bigger not_less)
 
    59 apply (auto simp add: intlen_bigger not_less)
 
    61 apply (metis intlen.elims intlen_bigger le_imp_0_less)
 
    60 apply (metis intlen.elims intlen_bigger le_imp_0_less)
 
    62 apply (smt Suc_lessI intlen.simps(2) length_Suc_conv nat_neq_iff)
 
    61 apply (smt Suc_lessI intlen.simps(2) length_Suc_conv nat_neq_iff)
 
    63 by (smt Suc_lessE intlen.simps(2) length_Suc_conv)
 
    62 by (smt Suc_lessE intlen.simps(2) length_Suc_conv)
 
    64 
    63 
       
    64 lemma intlen_length_eq:
 
       
    65   shows "intlen xs = intlen ys \<longleftrightarrow> length xs = length ys"
 
       
    66 apply(induct xs arbitrary: ys)
 
       
    67 apply (auto simp add: intlen_bigger not_less)
 
       
    68 apply(case_tac ys)
 
       
    69 apply(simp_all)
 
       
    70 apply (smt intlen_bigger)
 
       
    71 apply (smt intlen.elims intlen_bigger length_Suc_conv)
 
       
    72 by (metis intlen.simps(2) length_Suc_conv)
 
    65 
    73 
    66 definition pflat_len :: "val \<Rightarrow> nat list => int"
 
    74 definition pflat_len :: "val \<Rightarrow> nat list => int"
 
    67 where
 
    75 where
 
    68   "pflat_len v p \<equiv> (if p \<in> Pos v then intlen (flat (at v p)) else -1)"
 
    76   "pflat_len v p \<equiv> (if p \<in> Pos v then intlen (flat (at v p)) else -1)"
 
    69 
    77 
    85 using assms 
    93 using assms 
    86 apply(induct vs arbitrary: n p)
 
    94 apply(induct vs arbitrary: n p)
 
    87 apply(auto simp add: less_Suc_eq_0_disj pflat_len_simps)
 
    95 apply(auto simp add: less_Suc_eq_0_disj pflat_len_simps)
 
    88 done
 
    96 done
 
    89 
    97 
    90 lemma outside_lemma:
 
    98 lemma pflat_len_outside:
 
    91   assumes "p \<notin> Pos v1 \<union> Pos v2"
 
    99   assumes "p \<notin> Pos v1"
 
    92   shows "pflat_len v1 p = pflat_len v2 p"
 
   100   shows "pflat_len v1 p = -1 "
 
    93 using assms by (auto simp add: pflat_len_def)
 
   101 using assms by (auto simp add: pflat_len_def)
 
    94 
   102 
    95 
   103 
    96 section {* Orderings *}
 
   104 section {* Orderings *}
 
    97 
   105 
   119 
   127 
   120 lemma lex_simps [simp]:
 
   128 lemma lex_simps [simp]:
 
   121   fixes xs ys :: "nat list"
 
   129   fixes xs ys :: "nat list"
 
   122   shows "[] \<sqsubset>lex ys \<longleftrightarrow> ys \<noteq> []"
 
   130   shows "[] \<sqsubset>lex ys \<longleftrightarrow> ys \<noteq> []"
 
   123   and   "xs \<sqsubset>lex [] \<longleftrightarrow> False"
 
   131   and   "xs \<sqsubset>lex [] \<longleftrightarrow> False"
 
   124   and   "(x # xs) \<sqsubset>lex (y # ys) \<longleftrightarrow> (x < y \<or> (\<not> y < x \<and> xs \<sqsubset>lex ys))"
 
   132   and   "(x # xs) \<sqsubset>lex (y # ys) \<longleftrightarrow> (x < y \<or> (x = y \<and> xs \<sqsubset>lex ys))"
 
   125 apply(auto elim: lex_list.cases intro: lex_list.intros)
 
   133 by (auto simp add: neq_Nil_conv elim: lex_list.cases intro: lex_list.intros)
 
   126 apply(auto simp add: neq_Nil_conv not_less_iff_gr_or_eq intro: lex_list.intros)
 
       
   127 done
 
       
   128 
   134 
   129 lemma lex_trans:
 
   135 lemma lex_trans:
 
   130   fixes ps1 ps2 ps3 :: "nat list"
 
   136   fixes ps1 ps2 ps3 :: "nat list"
 
   131   assumes "ps1 \<sqsubset>lex ps2" "ps2 \<sqsubset>lex ps3"
 
   137   assumes "ps1 \<sqsubset>lex ps2" "ps2 \<sqsubset>lex ps3"
 
   132   shows "ps1 \<sqsubset>lex ps3"
 
   138   shows "ps1 \<sqsubset>lex ps3"
 
   137 
   143 
   138 lemma lex_trichotomous:
 
   144 lemma lex_trichotomous:
 
   139   fixes p q :: "nat list"
 
   145   fixes p q :: "nat list"
 
   140   shows "p = q \<or> p \<sqsubset>lex q \<or> q \<sqsubset>lex p"
 
   146   shows "p = q \<or> p \<sqsubset>lex q \<or> q \<sqsubset>lex p"
 
   141 apply(induct p arbitrary: q)
 
   147 apply(induct p arbitrary: q)
 
   142 apply(auto)
 
   148 apply(auto elim: lex_list.cases)
 
   143 apply(case_tac q)
 
   149 apply(case_tac q)
 
   144 apply(auto)
 
   150 apply(auto)
 
   145 done
 
   151 done
 
   146 
   152 
   147 
   153 
   148 
   154 
   149 
   155 
   150 section {* Ordering of values according to Okui & Suzuki *}
 
   156 section {* POSIX Ordering of Values According to Okui & Suzuki *}
 
   151 
   157 
   152 
   158 
   153 definition PosOrd:: "val \<Rightarrow> nat list \<Rightarrow> val \<Rightarrow> bool" ("_ \<sqsubset>val _ _" [60, 60, 59] 60)
 
   159 definition PosOrd:: "val \<Rightarrow> nat list \<Rightarrow> val \<Rightarrow> bool" ("_ \<sqsubset>val _ _" [60, 60, 59] 60)
 
   154 where
 
   160 where
 
   155   "v1 \<sqsubset>val p v2 \<equiv> pflat_len v1 p > pflat_len v2 p \<and>
 
   161   "v1 \<sqsubset>val p v2 \<equiv> pflat_len v1 p > pflat_len v2 p \<and>
 
   156                    (\<forall>q \<in> Pos v1 \<union> Pos v2. q \<sqsubset>lex p \<longrightarrow> pflat_len v1 q = pflat_len v2 q)"
 
   162                    (\<forall>q \<in> Pos v1 \<union> Pos v2. q \<sqsubset>lex p \<longrightarrow> pflat_len v1 q = pflat_len v2 q)"
 
   157 
   163 
       
   164 
       
   165 
       
   166 definition pflat_len2 :: "val \<Rightarrow> nat list => (bool * nat)"
 
       
   167 where
 
       
   168   "pflat_len2 v p \<equiv> (if p \<in> Pos v then (True, length (flat (at v p))) else (False, 0))"
 
       
   169 
       
   170 instance prod :: (ord, ord) ord
 
       
   171   by (rule Orderings.class.Orderings.ord.of_class.intro)
 
       
   172 
       
   173 
       
   174 lemma "(0, 0) < (3::nat, 2::nat)"
 
       
   175 
       
   176 
       
   177 
       
   178 
   158 definition PosOrd2:: "val \<Rightarrow> nat list \<Rightarrow> val \<Rightarrow> bool" ("_ \<sqsubset>val2 _ _" [60, 60, 59] 60)
 
   179 definition PosOrd2:: "val \<Rightarrow> nat list \<Rightarrow> val \<Rightarrow> bool" ("_ \<sqsubset>val2 _ _" [60, 60, 59] 60)
 
   159 where
 
   180 where
 
   160   "v1 \<sqsubset>val2 p v2 \<equiv> p \<in> Pos v1 \<and> 
   181   "v1 \<sqsubset>val2 p v2 \<equiv> (fst (pflat_len2 v1 p) > fst (pflat_len2 v2 p) \<or>
 
   161                    pflat_len v1 p > pflat_len v2 p \<and>
 
   182                      snd (pflat_len2 v1 p) > fst (pflat_len2 v2 p)) \<and>
 
   162                    (\<forall>q \<in> Pos v1 \<union> Pos v2. q \<sqsubset>lex p \<longrightarrow> pflat_len v1 q = pflat_len v2 q)"
 
   183                     (\<forall>q \<in> Pos v1 \<union> Pos v2. q \<sqsubset>lex p \<longrightarrow> pflat_len v1 q = pflat_len v2 q)"
 
   163 
       
   164 lemma XXX:
 
       
   165   "v1 \<sqsubset>val p v2 \<longleftrightarrow> v1 \<sqsubset>val2 p v2"
 
       
   166 apply(auto simp add: PosOrd_def PosOrd2_def)
 
       
   167 apply(auto simp add: pflat_len_def split: if_splits)
 
       
   168 by (smt intlen_bigger)
 
       
   169 
       
   170 
       
   171 (* some tests *)
 
       
   172 
       
   173 definition ValFlat_ord:: "val \<Rightarrow> nat list \<Rightarrow> val \<Rightarrow> bool" ("_ \<sqsubset>fval _ _")
 
       
   174 where
 
       
   175   "v1 \<sqsubset>fval p v2 \<equiv> p \<in> Pos v1 \<and> 
       
   176                     (p \<notin> Pos v2 \<or> flat (at v2 p) \<sqsubset>spre flat (at v1 p)) \<and>
 
       
   177                     (\<forall>q \<in> Pos v1 \<union> Pos v2. q \<sqsubset>lex p \<longrightarrow> (pflat_len v1 q = pflat_len v2 q))"
 
       
   178 
       
   179 lemma 
       
   180   assumes "v1 \<sqsubset>fval p v2" 
       
   181   shows "v1 \<sqsubset>val p v2"
 
       
   182 using assms
 
       
   183 unfolding ValFlat_ord_def PosOrd_def
 
       
   184 apply(clarify)
 
       
   185 apply(simp add: pflat_len_def)
 
       
   186 apply(auto)[1]
 
       
   187 apply(smt intlen_bigger)
 
       
   188 apply(simp add: sprefix_list_def prefix_list_def)
 
       
   189 apply(auto)[1]
 
       
   190 apply(drule sym)
 
       
   191 apply(simp add: intlen_append)
 
       
   192 apply (metis intlen.simps(1) intlen_length length_greater_0_conv list.size(3))
 
       
   193 apply(smt intlen_bigger)
 
       
   194 done
 
       
   195 
       
   196 lemma 
       
   197   assumes "v1 \<sqsubset>val p v2" "flat (at v2 p) \<sqsubset>spre flat (at v1 p)"
 
       
   198   shows "v1 \<sqsubset>fval p v2"
 
       
   199 using assms
 
       
   200 unfolding ValFlat_ord_def PosOrd_def
 
       
   201 apply(clarify)
 
       
   202 oops
 
       
   203 
   184 
   204 
   185 
   205 definition PosOrd_ex:: "val \<Rightarrow> val \<Rightarrow> bool" ("_ :\<sqsubset>val _" [60, 59] 60)
 
   186 definition PosOrd_ex:: "val \<Rightarrow> val \<Rightarrow> bool" ("_ :\<sqsubset>val _" [60, 59] 60)
 
   206 where
 
   187 where
 
   207   "v1 :\<sqsubset>val v2 \<equiv> (\<exists>p. v1 \<sqsubset>val p v2)"
 
   188   "v1 :\<sqsubset>val v2 \<equiv> \<exists>p. v1 \<sqsubset>val p v2"
 
   208 
   189 
   209 definition PosOrd_ex1:: "val \<Rightarrow> val \<Rightarrow> bool" ("_ :\<sqsubseteq>val _" [60, 59] 60)
 
   190 definition PosOrd_ex_eq:: "val \<Rightarrow> val \<Rightarrow> bool" ("_ :\<sqsubseteq>val _" [60, 59] 60)
 
   210 where
 
   191 where
 
   211   "v1 :\<sqsubseteq>val v2 \<equiv> v1 :\<sqsubset>val v2 \<or> v1 = v2"
 
   192   "v1 :\<sqsubseteq>val v2 \<equiv> v1 :\<sqsubset>val v2 \<or> v1 = v2"
 
       
   193 
   212 
   194 
   213 lemma PosOrd_shorterE:
 
   195 lemma PosOrd_shorterE:
 
   214   assumes "v1 :\<sqsubset>val v2" 
   196   assumes "v1 :\<sqsubset>val v2" 
   215   shows "length (flat v2) \<le> length (flat v1)"
 
   197   shows "length (flat v2) \<le> length (flat v1)"
 
   216 using assms
 
   198 using assms
 
   217 apply(auto simp add: PosOrd_ex_def PosOrd_def)
 
   199 apply(auto simp add: pflat_len_simps PosOrd_ex_def PosOrd_def)
 
   218 apply(case_tac p)
 
   200 apply(case_tac p)
 
   219 apply(simp add: pflat_len_simps)
 
   201 apply(simp add: pflat_len_simps intlen_length)
 
   220 apply(simp add: intlen_length)
 
       
   221 apply(simp)
 
   202 apply(simp)
 
   222 apply(drule_tac x="[]" in bspec)
 
   203 apply(drule_tac x="[]" in bspec)
 
   223 apply(simp add: Pos_empty)
 
   204 apply(simp add: Pos_empty)
 
   224 apply(simp add: pflat_len_simps)
 
   205 apply(simp add: pflat_len_simps le_less intlen_length_eq)
 
   225 by (metis intlen_length le_less less_irrefl linear)
 
   206 done
 
   226 
       
   227 
   207 
   228 lemma PosOrd_shorterI:
 
   208 lemma PosOrd_shorterI:
 
   229   assumes "length (flat v') < length (flat v)"
 
   209   assumes "length (flat v2) < length (flat v1)"
 
   230   shows "v :\<sqsubset>val v'" 
   210   shows "v1 :\<sqsubset>val v2" 
   231 using assms
 
   211 using assms
 
   232 unfolding PosOrd_ex_def
 
   212 unfolding PosOrd_ex_def
 
   233 by (metis intlen_length lex_simps(2) pflat_len_simps(9) PosOrd_def)
 
   213 by (metis intlen_length lex_simps(2) pflat_len_simps(9) PosOrd_def)
 
   234 
   214 
   235 lemma PosOrd_spreI:
 
   215 lemma PosOrd_spreI:
 
   236   assumes "(flat v') \<sqsubset>spre (flat v)"
 
   216   assumes "flat v' \<sqsubset>spre flat v"
 
   237   shows "v :\<sqsubset>val v'" 
   217   shows "v :\<sqsubset>val v'" 
   238 using assms
 
   218 using assms
 
   239 apply(rule_tac PosOrd_shorterI)
 
   219 apply(rule_tac PosOrd_shorterI)
 
   240 by (metis append_eq_conv_conj le_less_linear prefix_list_def sprefix_list_def take_all)
 
   220 by (metis append_eq_conv_conj le_less_linear prefix_list_def sprefix_list_def take_all)
 
       
   221 
   241 
   222 
   242 lemma PosOrd_Left_Right:
 
   223 lemma PosOrd_Left_Right:
 
   243   assumes "flat v1 = flat v2"
 
   224   assumes "flat v1 = flat v2"
 
   244   shows "Left v1 :\<sqsubset>val Right v2" 
   225   shows "Left v1 :\<sqsubset>val Right v2" 
   245 unfolding PosOrd_ex_def
 
   226 unfolding PosOrd_ex_def
 
   246 apply(rule_tac x="[0]" in exI)
 
   227 apply(rule_tac x="[0]" in exI)
 
   247 using assms
 
   228 using assms 
   248 apply(auto simp add: PosOrd_def pflat_len_simps)
 
   229 apply(auto simp add: PosOrd_def pflat_len_simps)
 
   249 apply(smt intlen_bigger)
 
   230 apply(smt intlen_bigger)
 
   250 done
 
   231 done
 
   251 
   232 
   252 lemma PosOrd_LeftI:
 
   233 lemma PosOrd_Left_eq:
 
   253   assumes "v :\<sqsubset>val v'" "flat v = flat v'"
 
   234   assumes "flat v = flat v'"
 
   254   shows "(Left v) :\<sqsubset>val (Left v')" 
   235   shows "Left v :\<sqsubset>val Left v' \<longleftrightarrow> v :\<sqsubset>val v'" 
   255 using assms(1)
 
   236 using assms
 
   256 unfolding PosOrd_ex_def
 
   237 unfolding PosOrd_ex_def
 
   257 apply(auto)
 
   238 apply(auto)
 
       
   239 apply(case_tac p)
 
       
   240 apply(simp add: PosOrd_def pflat_len_simps)
 
       
   241 apply(case_tac a)
 
       
   242 apply(simp add: PosOrd_def pflat_len_simps)
 
       
   243 apply(rule_tac x="list" in exI)
 
       
   244 apply(auto simp add: PosOrd_def pflat_len_simps)[1]
 
       
   245 apply (smt Un_def lex_list.intros(2) mem_Collect_eq pflat_len_simps(3))
 
       
   246 apply (smt Collect_disj_eq lex_list.intros(2) mem_Collect_eq pflat_len_simps(3))
 
       
   247 apply(auto simp add: PosOrd_def pflat_len_outside)[1]
 
   258 apply(rule_tac x="0#p" in exI)
 
   248 apply(rule_tac x="0#p" in exI)
 
   259 using assms(2)
 
       
   260 apply(auto simp add: PosOrd_def pflat_len_simps)
 
   249 apply(auto simp add: PosOrd_def pflat_len_simps)
 
   261 done
 
   250 done
 
       
   251 
   262 
   252 
   263 lemma PosOrd_RightI:
 
   253 lemma PosOrd_RightI:
 
   264   assumes "v :\<sqsubset>val v'" "flat v = flat v'"
 
   254   assumes "v :\<sqsubset>val v'" "flat v = flat v'"
 
   265   shows "(Right v) :\<sqsubset>val (Right v')" 
   255   shows "(Right v) :\<sqsubset>val (Right v')" 
   266 using assms(1)
 
   256 using assms(1)
 
   267 unfolding PosOrd_ex_def
 
   257 unfolding PosOrd_ex_def
 
   268 apply(auto)
 
   258 apply(auto)
 
   269 apply(rule_tac x="Suc 0#p" in exI)
 
   259 apply(rule_tac x="Suc 0#p" in exI)
 
   270 using assms(2)
 
   260 using assms(2)
 
   271 apply(auto simp add: PosOrd_def pflat_len_simps)
 
   261 apply(auto simp add: PosOrd_def pflat_len_simps)
 
   272 done
 
       
   273 
       
   274 lemma PosOrd_LeftE:
 
       
   275   assumes "(Left v1) :\<sqsubset>val (Left v2)"
 
       
   276   shows "v1 :\<sqsubset>val v2"
 
       
   277 using assms
 
       
   278 apply(simp add: PosOrd_ex_def)
 
       
   279 apply(erule exE)
 
       
   280 apply(case_tac p)
 
       
   281 apply(simp add: PosOrd_def)
 
       
   282 apply(auto simp add: pflat_len_simps)
 
       
   283 apply(rule_tac x="[]" in exI)
 
       
   284 apply(simp add: Pos_empty pflat_len_simps)
 
       
   285 apply(auto simp add: pflat_len_simps PosOrd_def)
 
       
   286 apply(case_tac a)
 
       
   287 apply(auto simp add: pflat_len_simps)[1]
 
       
   288 apply(rule_tac x="list" in exI)
 
       
   289 apply(auto)
 
       
   290 apply(drule_tac x="0#q" in bspec)
 
       
   291 apply(simp)
 
       
   292 apply(simp add: pflat_len_simps)
 
       
   293 apply(drule_tac x="0#q" in bspec)
 
       
   294 apply(simp)
 
       
   295 apply(simp add: pflat_len_simps)
 
       
   296 apply(simp add: pflat_len_def)
 
       
   297 done
 
   262 done
 
   298 
   263 
   299 lemma PosOrd_RightE:
 
   264 lemma PosOrd_RightE:
 
   300   assumes "(Right v1) :\<sqsubset>val (Right v2)"
 
   265   assumes "(Right v1) :\<sqsubset>val (Right v2)"
 
   301   shows "v1 :\<sqsubset>val v2"
 
   266   shows "v1 :\<sqsubset>val v2"
 
   515     where as: "v1 \<sqsubset>val p v2" "v2 \<sqsubset>val p' v3" unfolding PosOrd_ex_def by blast
 
   480     where as: "v1 \<sqsubset>val p v2" "v2 \<sqsubset>val p' v3" unfolding PosOrd_ex_def by blast
 
   516   have "p = p' \<or> p \<sqsubset>lex p' \<or> p' \<sqsubset>lex p"
 
   481   have "p = p' \<or> p \<sqsubset>lex p' \<or> p' \<sqsubset>lex p"
 
   517     by (rule lex_trichotomous)
 
   482     by (rule lex_trichotomous)
 
   518   moreover
 
   483   moreover
 
   519     { assume "p = p'"
 
   484     { assume "p = p'"
 
   520       with as have "v1 \<sqsubset>val p v3" unfolding PosOrd_def
 
   485       with as have "v1 \<sqsubset>val p v3" unfolding PosOrd_def pflat_len_def
 
   521       by (smt outside_lemma)
 
   486       by fastforce
 
   522       then have " v1 :\<sqsubset>val v3" unfolding PosOrd_ex_def by blast
 
   487       then have " v1 :\<sqsubset>val v3" unfolding PosOrd_ex_def by blast
 
   523     }   
   488     }   
   524   moreover
 
   489   moreover
 
   525     { assume "p \<sqsubset>lex p'"
 
   490     { assume "p \<sqsubset>lex p'"
 
   526       with as have "v1 \<sqsubset>val p v3" unfolding PosOrd_def
 
   491       with as have "v1 \<sqsubset>val p v3" unfolding PosOrd_def pflat_len_def
 
   527       by (metis lex_trans outside_lemma)
 
   492       by (smt Un_iff lex_trans)
 
   528       then have " v1 :\<sqsubset>val v3" unfolding PosOrd_ex_def by blast
 
   493       then have " v1 :\<sqsubset>val v3" unfolding PosOrd_ex_def by blast
 
   529     }
 
   494     }
 
   530   moreover
 
   495   moreover
 
   531     { assume "p' \<sqsubset>lex p"
 
   496     { assume "p' \<sqsubset>lex p"
 
   532       with as have "v1 \<sqsubset>val p' v3" unfolding PosOrd_def
 
   497       with as have "v1 \<sqsubset>val p' v3" unfolding PosOrd_def
 
   558   shows "False"
 
   523   shows "False"
 
   559 using assms
 
   524 using assms
 
   560 apply(auto simp add: PosOrd_ex_def PosOrd_def)
 
   525 apply(auto simp add: PosOrd_ex_def PosOrd_def)
 
   561 using assms PosOrd_irrefl PosOrd_trans by blast
 
   526 using assms PosOrd_irrefl PosOrd_trans by blast
 
   562 
   527 
   563 lemma WW2:
 
       
   564   assumes "\<not>(v1 :\<sqsubset>val v2)" 
       
   565   shows "v1 = v2 \<or> v2 :\<sqsubset>val v1"
 
       
   566 using assms
 
       
   567 oops
 
       
   568 
       
   569 lemma PosOrd_SeqE2:
 
   528 lemma PosOrd_SeqE2:
 
   570   assumes "(Seq v1 v2) :\<sqsubset>val (Seq v1' v2')" 
   529   assumes "(Seq v1 v2) :\<sqsubset>val (Seq v1' v2')" "flat (Seq v1 v2) = flat (Seq v1' v2')"
 
   571   shows "v1 :\<sqsubset>val v1' \<or> (v1 = v1' \<and> v2 :\<sqsubset>val v2')"
 
   530   shows "v1 :\<sqsubset>val v1' \<or> (intlen (flat v1) = intlen (flat v1') \<and> v2 :\<sqsubset>val v2')"
 
   572 using assms 
   531 using assms 
   573 apply(frule_tac PosOrd_SeqE)
 
   532 apply(frule_tac PosOrd_SeqE)
 
   574 apply(erule disjE)
 
   533 apply(erule disjE)
 
   575 apply(simp)
 
   534 apply(simp)
 
       
   535 apply(case_tac "v1 :\<sqsubset>val v1'")
 
       
   536 apply(simp)
 
       
   537 apply(rule disjI2)
 
       
   538 apply(rule conjI)
 
       
   539 prefer 2
 
       
   540 apply(simp)
 
   576 apply(auto)
 
   541 apply(auto)
 
       
   542 apply(auto simp add: PosOrd_ex_def)
 
       
   543 apply(auto simp add: PosOrd_def pflat_len_simps)
 
       
   544 apply(case_tac p)
 
       
   545 apply(auto simp add: PosOrd_def pflat_len_simps)
 
       
   546 apply(case_tac a)
 
       
   547 apply(auto simp add: PosOrd_def pflat_len_simps)
 
       
   548 apply (metis PosOrd_SeqI1 PosOrd_almost_trichotomous PosOrd_def PosOrd_ex_def WW1 assms(1) assms(2))
 
       
   549 by (metis PosOrd_SeqI1 PosOrd_almost_trichotomous PosOrd_def PosOrd_ex_def WW1 assms(1) assms(2))
 
       
   550 
       
   551 lemma PosOrd_SeqE4:
 
       
   552   assumes "(Seq v1 v2) :\<sqsubset>val (Seq v1' v2')" "flat (Seq v1 v2) = flat (Seq v1' v2')"
 
       
   553   shows "v1 :\<sqsubset>val v1' \<or> (flat v1 = flat v1' \<and> v2 :\<sqsubset>val v2')"
 
       
   554 using assms 
       
   555 apply(frule_tac PosOrd_SeqE)
 
       
   556 apply(erule disjE)
 
       
   557 apply(simp)
 
   577 apply(case_tac "v1 :\<sqsubset>val v1'")
 
   558 apply(case_tac "v1 :\<sqsubset>val v1'")
 
   578 apply(simp)
 
   559 apply(simp)
 
   579 apply(auto simp add: PosOrd_ex_def)
 
   560 apply(rule disjI2)
 
   580 apply(case_tac "v1 = v1'")
 
   561 apply(rule conjI)
 
   581 apply(simp)
 
   562 prefer 2
 
   582 oops
 
   563 apply(simp)
 
       
   564 apply(auto)
 
       
   565 apply(case_tac "length (flat v1') < length (flat v1)")
 
       
   566 using PosOrd_shorterI apply blast
 
       
   567 by (metis PosOrd_SeqI1 PosOrd_shorterI WW1 antisym_conv3 append_eq_append_conv assms(2))
 
       
   568 
   583 
   569 
   584 section {* CPT and CPTpre *}
 
   570 section {* CPT and CPTpre *}
 
   585 
   571 
   586 
   572 
   587 inductive 
   573 inductive 
   590  "\<lbrakk>\<Turnstile> v1 : r1; \<Turnstile> v2 : r2\<rbrakk> \<Longrightarrow> \<Turnstile>  Seq v1 v2 : SEQ r1 r2"
 
   576  "\<lbrakk>\<Turnstile> v1 : r1; \<Turnstile> v2 : r2\<rbrakk> \<Longrightarrow> \<Turnstile>  Seq v1 v2 : SEQ r1 r2"
 
   591 | "\<Turnstile> v1 : r1 \<Longrightarrow> \<Turnstile> Left v1 : ALT r1 r2"
 
   577 | "\<Turnstile> v1 : r1 \<Longrightarrow> \<Turnstile> Left v1 : ALT r1 r2"
 
   592 | "\<Turnstile> v2 : r2 \<Longrightarrow> \<Turnstile> Right v2 : ALT r1 r2"
 
   578 | "\<Turnstile> v2 : r2 \<Longrightarrow> \<Turnstile> Right v2 : ALT r1 r2"
 
   593 | "\<Turnstile> Void : ONE"
 
   579 | "\<Turnstile> Void : ONE"
 
   594 | "\<Turnstile> Char c : CHAR c"
 
   580 | "\<Turnstile> Char c : CHAR c"
 
   595 | "\<Turnstile> Stars [] : STAR r"
 
   581 | "\<forall>v \<in> set vs. \<Turnstile> v : r \<and> flat v \<noteq> [] \<Longrightarrow> \<Turnstile> Stars vs : STAR r"
 
   596 | "\<lbrakk>\<Turnstile> v : r; flat v \<noteq> []; \<Turnstile> Stars vs : STAR r\<rbrakk> \<Longrightarrow> \<Turnstile> Stars (v # vs) : STAR r"
 
       
   597 
   582 
   598 lemma Prf_CPrf:
 
   583 lemma Prf_CPrf:
 
   599   assumes "\<Turnstile> v : r"
 
   584   assumes "\<Turnstile> v : r"
 
   600   shows "\<turnstile> v : r"
 
   585   shows "\<turnstile> v : r"
 
   601 using assms
 
   586 using assms
 
   602 by (induct) (auto intro: Prf.intros)
 
   587 by (induct)(auto intro: Prf.intros)
 
   603 
       
   604 lemma pflat_len_equal_iff:
 
       
   605   assumes "\<Turnstile> v1 : r" "\<Turnstile> v2 : r"
 
       
   606   and "\<forall>p. pflat_len v1 p = pflat_len v2 p"
 
       
   607   shows "v1 = v2"
 
       
   608 using assms
 
       
   609 apply(induct v1 r arbitrary: v2 rule: CPrf.induct)
 
       
   610 apply(rotate_tac 4)
 
       
   611 apply(erule CPrf.cases)
 
       
   612 apply(simp_all)[7]
 
       
   613 apply (metis pflat_len_simps(1) pflat_len_simps(2))
 
       
   614 apply(rotate_tac 2)
 
       
   615 apply(erule CPrf.cases)
 
       
   616 apply(simp_all)[7]
 
       
   617 apply (metis pflat_len_simps(3))
 
       
   618 apply (metis intlen.simps(1) intlen_length length_greater_0_conv list.size(3) neg_0_le_iff_le not_less not_less_iff_gr_or_eq not_one_le_zero pflat_len_simps(3) pflat_len_simps(6) pflat_len_simps(9))
 
       
   619 apply(rotate_tac 2)
 
       
   620 apply(erule CPrf.cases)
 
       
   621 apply(simp_all)[7]
 
       
   622 apply (metis intlen.simps(1) intlen_length length_greater_0_conv list.size(3) neg_0_le_iff_le not_less not_less_iff_gr_or_eq not_one_le_zero pflat_len_simps(3) pflat_len_simps(6) pflat_len_simps(9))
 
       
   623 apply (metis pflat_len_simps(5))
 
       
   624 apply(erule CPrf.cases)
 
       
   625 apply(simp_all)[7]
 
       
   626 apply(erule CPrf.cases)
 
       
   627 apply(simp_all)[7]
 
       
   628 apply(erule CPrf.cases)
 
       
   629 apply(simp_all)[7]
 
       
   630 apply (metis append_Cons flat.simps(6) flat.simps(7) intlen_length length_greater_0_conv neq_Nil_conv not_less_iff_gr_or_eq pflat_len_simps(9))
 
       
   631 apply(rotate_tac 5)
 
       
   632 apply(erule CPrf.cases)
 
       
   633 apply(simp_all)[7]
 
       
   634 apply (metis append_Cons flat.simps(6) flat.simps(7) intlen_length length_greater_0_conv list.distinct(1) list.exhaust not_less_iff_gr_or_eq pflat_len_simps(9))
 
       
   635 apply(auto)
 
       
   636 apply (metis pflat_len_simps(8))
 
       
   637 apply(subgoal_tac "v = va")
 
       
   638 prefer 2
 
       
   639 apply (metis pflat_len_simps(8))
 
       
   640 apply(simp)
 
       
   641 apply(rotate_tac 3)
 
       
   642 apply(drule_tac x="Stars vsa" in meta_spec)
 
       
   643 apply(simp)
 
       
   644 apply(drule_tac meta_mp)
 
       
   645 apply(rule allI)
 
       
   646 apply(case_tac p)
 
       
   647 apply(simp add: pflat_len_simps)
 
       
   648 apply(drule_tac x="[]" in spec)
 
       
   649 apply(simp add: pflat_len_simps intlen_append)
 
       
   650 apply(drule_tac x="Suc a#list" in spec)
 
       
   651 apply(simp add: pflat_len_simps intlen_append)
 
       
   652 apply(simp)
 
       
   653 done
 
       
   654 
       
   655 lemma PosOrd_trichotomous_stronger:
 
       
   656   assumes "\<Turnstile> v1 : r" "\<Turnstile> v2 : r"
 
       
   657   shows "v1 :\<sqsubset>val v2 \<or> v2 :\<sqsubset>val v1 \<or> (v1 = v2)"
 
       
   658 oops
 
       
   659 
   588 
   660 lemma CPrf_stars:
 
   589 lemma CPrf_stars:
 
   661   assumes "\<Turnstile> Stars vs : STAR r"
 
   590   assumes "\<Turnstile> Stars vs : STAR r"
 
   662   shows "\<forall>v \<in> set vs. flat v \<noteq> [] \<and> \<Turnstile> v : r"
 
   591   shows "\<forall>v \<in> set vs. flat v \<noteq> [] \<and> \<Turnstile> v : r"
 
   663 using assms
 
   592 using assms
 
   664 apply(induct vs)
 
   593 apply(erule_tac CPrf.cases)
 
   665 apply(auto)
 
       
   666 apply(erule CPrf.cases)
 
       
   667 apply(simp_all)
 
       
   668 apply(erule CPrf.cases)
 
       
   669 apply(simp_all)
 
       
   670 apply(erule CPrf.cases)
 
       
   671 apply(simp_all)
 
       
   672 apply(erule CPrf.cases)
 
       
   673 apply(simp_all)
 
   594 apply(simp_all)
 
   674 done
 
   595 done
 
   675 
   596 
   676 lemma CPrf_Stars_appendE:
 
   597 lemma CPrf_Stars_appendE:
 
   677   assumes "\<Turnstile> Stars (vs1 @ vs2) : STAR r"
 
   598   assumes "\<Turnstile> Stars (vs1 @ vs2) : STAR r"
 
   678   shows "\<Turnstile> Stars vs1 : STAR r \<and> \<Turnstile> Stars vs2 : STAR r" 
   599   shows "\<Turnstile> Stars vs1 : STAR r \<and> \<Turnstile> Stars vs2 : STAR r" 
   679 using assms
 
   600 using assms
 
   680 apply(induct vs1 arbitrary: vs2)
 
   601 apply(erule_tac CPrf.cases)
 
   681 apply(auto intro: CPrf.intros)[1]
 
   602 apply(auto intro: CPrf.intros elim: Prf.cases)
 
   682 apply(erule CPrf.cases)
 
       
   683 apply(simp_all)
 
       
   684 apply(auto intro: CPrf.intros)
 
       
   685 done
 
   603 done
 
   686 
   604 
   687 definition PT :: "rexp \<Rightarrow> string \<Rightarrow> val set"
 
   605 definition PT :: "rexp \<Rightarrow> string \<Rightarrow> val set"
 
   688 where "PT r s \<equiv> {v. flat v = s \<and> \<turnstile> v : r}"
 
   606 where "PT r s \<equiv> {v. flat v = s \<and> \<turnstile> v : r}"
 
   689 
   607 
   694   "CPTpre r s = {v. \<exists>s'. flat v @ s' = s \<and> \<Turnstile> v : r}"
 
   612   "CPTpre r s = {v. \<exists>s'. flat v @ s' = s \<and> \<Turnstile> v : r}"
 
   695 
   613 
   696 lemma CPT_CPTpre_subset:
 
   614 lemma CPT_CPTpre_subset:
 
   697   shows "CPT r s \<subseteq> CPTpre r s"
 
   615   shows "CPT r s \<subseteq> CPTpre r s"
 
   698 by(auto simp add: CPT_def CPTpre_def)
 
   616 by(auto simp add: CPT_def CPTpre_def)
 
       
   617 
       
   618 lemma CPT_simps:
 
       
   619   shows "CPT ZERO s = {}"
 
       
   620   and   "CPT ONE s = (if s = [] then {Void} else {})"
 
       
   621   and   "CPT (CHAR c) s = (if s = [c] then {Char c} else {})"
 
       
   622   and   "CPT (ALT r1 r2) s = Left ` CPT r1 s \<union> Right ` CPT r2 s"
 
       
   623   and   "CPT (SEQ r1 r2) s = 
       
   624           {Seq v1 v2 | v1 v2. flat v1 @ flat v2 = s \<and> v1 \<in> CPT r1 (flat v1) \<and> v2 \<in> CPT r2 (flat v2)}"
 
       
   625   and   "CPT (STAR r) s = 
       
   626           Stars ` {vs. concat (map flat vs) = s \<and> (\<forall>v \<in> set vs. v \<in> CPT r (flat v) \<and> flat v \<noteq> [])}"
 
       
   627 apply -
 
       
   628 apply(auto simp add: CPT_def intro: CPrf.intros)[1]
 
       
   629 apply(erule CPrf.cases)
 
       
   630 apply(simp_all)[6]
 
       
   631 apply(auto simp add: CPT_def intro: CPrf.intros)[1]
 
       
   632 apply(erule CPrf.cases)
 
       
   633 apply(simp_all)[6]
 
       
   634 apply(erule CPrf.cases)
 
       
   635 apply(simp_all)[6]
 
       
   636 apply(auto simp add: CPT_def intro: CPrf.intros)[1]
 
       
   637 apply(erule CPrf.cases)
 
       
   638 apply(simp_all)[6]
 
       
   639 apply(erule CPrf.cases)
 
       
   640 apply(simp_all)[6]
 
       
   641 apply(auto simp add: CPT_def intro: CPrf.intros)[1]
 
       
   642 apply(erule CPrf.cases)
 
       
   643 apply(simp_all)[6]
 
       
   644 apply(auto simp add: CPT_def intro: CPrf.intros)[1]
 
       
   645 apply(erule CPrf.cases)
 
       
   646 apply(simp_all)[6]
 
       
   647 (* STAR case *)
 
       
   648 apply(auto simp add: CPT_def intro: CPrf.intros)[1]
 
       
   649 apply(erule CPrf.cases)
 
       
   650 apply(simp_all)[6]
 
       
   651 done
 
       
   652 
       
   653 (*
 
       
   654 lemma CPTpre_STAR_finite:
 
       
   655   assumes "\<And>s. finite (CPT r s)"
 
       
   656   shows "finite (CPT (STAR r) s)"
 
       
   657 apply(induct s rule: length_induct)
 
       
   658 apply(case_tac xs)
 
       
   659 apply(simp)
 
       
   660 apply(simp add: CPT_simps)
 
       
   661 apply(auto)
 
       
   662 apply(rule finite_imageI)
 
       
   663 using assms
 
       
   664 thm finite_Un
 
       
   665 prefer 2
 
       
   666 apply(simp add: CPT_simps)
 
       
   667 apply(rule finite_imageI)
 
       
   668 apply(rule finite_subset)
 
       
   669 apply(rule CPTpre_subsets)
 
       
   670 apply(simp)
 
       
   671 apply(rule_tac B="(\<lambda>(v, vs). Stars (v#vs)) ` {(v, vs). v \<in> CPTpre r (a#list) \<and> flat v \<noteq> [] \<and> Stars vs \<in> CPTpre (STAR r) (drop (length (flat v)) (a#list))}" in finite_subset)
 
       
   672 apply(auto)[1]
 
       
   673 apply(rule finite_imageI)
 
       
   674 apply(simp add: Collect_case_prod_Sigma)
 
       
   675 apply(rule finite_SigmaI)
 
       
   676 apply(rule assms)
 
       
   677 apply(case_tac "flat v = []")
 
       
   678 apply(simp)
 
       
   679 apply(drule_tac x="drop (length (flat v)) (a # list)" in spec)
 
       
   680 apply(simp)
 
       
   681 apply(auto)[1]
 
       
   682 apply(rule test)
 
       
   683 apply(simp)
 
       
   684 done
 
   699 
   685 
   700 lemma CPTpre_subsets:
 
   686 lemma CPTpre_subsets:
 
   701   "CPTpre ZERO s = {}"
 
   687   "CPTpre ZERO s = {}"
 
   702   "CPTpre ONE s \<subseteq> {Void}"
 
   688   "CPTpre ONE s \<subseteq> {Void}"
 
   703   "CPTpre (CHAR c) s \<subseteq> {Char c}"
 
   689   "CPTpre (CHAR c) s \<subseteq> {Char c}"
 
   715 apply(simp_all)
 
   701 apply(simp_all)
 
   716 apply(erule CPrf.cases)
 
   702 apply(erule CPrf.cases)
 
   717 apply(simp_all)
 
   703 apply(simp_all)
 
   718 apply(erule CPrf.cases)
 
   704 apply(erule CPrf.cases)
 
   719 apply(simp_all)
 
   705 apply(simp_all)
 
       
   706 
   720 apply(erule CPrf.cases)
 
   707 apply(erule CPrf.cases)
 
   721 apply(simp_all)
 
   708 apply(simp_all)
 
   722 apply(erule CPrf.cases)
 
   709 apply(erule CPrf.cases)
 
   723 apply(simp_all)
 
   710 apply(simp_all)
 
   724 apply(rule CPrf.intros)
 
   711 apply(rule CPrf.intros)
 
   843   shows "finite (CPT r s)"
 
   830   shows "finite (CPT r s)"
 
   844 apply(rule finite_subset)
 
   831 apply(rule finite_subset)
 
   845 apply(rule CPT_CPTpre_subset)
 
   832 apply(rule CPT_CPTpre_subset)
 
   846 apply(rule CPTpre_finite)
 
   833 apply(rule CPTpre_finite)
 
   847 done
 
   834 done
 
       
   835 *)
 
   848 
   836 
   849 lemma Posix_CPT:
 
   837 lemma Posix_CPT:
 
   850   assumes "s \<in> r \<rightarrow> v"
 
   838   assumes "s \<in> r \<rightarrow> v"
 
   851   shows "v \<in> CPT r s"
 
   839   shows "v \<in> CPT r s"
 
   852 using assms
 
   840 using assms
 
   853 by (induct rule: Posix.induct)
 
   841 apply(induct rule: Posix.induct)
 
   854    (auto simp add: CPT_def intro: CPrf.intros)
 
   842 apply(auto simp add: CPT_def intro: CPrf.intros elim: CPrf.cases)
 
       
   843 apply(rotate_tac 5)
 
       
   844 apply(erule CPrf.cases)
 
       
   845 apply(simp_all)
 
       
   846 apply(rule CPrf.intros)
 
       
   847 apply(simp_all)
 
       
   848 done
 
       
   849 
   855 
   850 
   856 section {* The Posix Value is smaller than any other Value *}
 
   851 section {* The Posix Value is smaller than any other Value *}
 
   857 
   852 
   858 
   853 
   859 lemma Posix_PosOrd:
 
   854 lemma Posix_PosOrd:
 
   864   case (Posix_ONE v)
 
   859   case (Posix_ONE v)
 
   865   have "v \<in> CPT ONE []" by fact
 
   860   have "v \<in> CPT ONE []" by fact
 
   866   then have "v = Void"
 
   861   then have "v = Void"
 
   867     by (simp add: CPT_simps)
 
   862     by (simp add: CPT_simps)
 
   868   then show "Void :\<sqsubseteq>val v"
 
   863   then show "Void :\<sqsubseteq>val v"
 
   869     by (simp add: PosOrd_ex1_def)
 
   864     by (simp add: PosOrd_ex_eq_def)
 
   870 next
 
   865 next
 
   871   case (Posix_CHAR c v)
 
   866   case (Posix_CHAR c v)
 
   872   have "v \<in> CPT (CHAR c) [c]" by fact
 
   867   have "v \<in> CPT (CHAR c) [c]" by fact
 
   873   then have "v = Char c"
 
   868   then have "v = Char c"
 
   874     by (simp add: CPT_simps)
 
   869     by (simp add: CPT_simps)
 
   875   then show "Char c :\<sqsubseteq>val v"
 
   870   then show "Char c :\<sqsubseteq>val v"
 
   876     by (simp add: PosOrd_ex1_def)
 
   871     by (simp add: PosOrd_ex_eq_def)
 
   877 next
 
   872 next
 
   878   case (Posix_ALT1 s r1 v r2 v2)
 
   873   case (Posix_ALT1 s r1 v r2 v2)
 
   879   have as1: "s \<in> r1 \<rightarrow> v" by fact
 
   874   have as1: "s \<in> r1 \<rightarrow> v" by fact
 
   880   have IH: "\<And>v2. v2 \<in> CPT r1 s \<Longrightarrow> v :\<sqsubseteq>val v2" by fact
 
   875   have IH: "\<And>v2. v2 \<in> CPT r1 s \<Longrightarrow> v :\<sqsubseteq>val v2" by fact
 
   881   have "v2 \<in> CPT (ALT r1 r2) s" by fact
 
   876   have "v2 \<in> CPT (ALT r1 r2) s" by fact
 
   893      with IH have "v :\<sqsubseteq>val v3" by simp
 
   888      with IH have "v :\<sqsubseteq>val v3" by simp
 
   894      moreover
 
   889      moreover
 
   895      have "flat v3 = flat v" using as1 Left(3)
 
   890      have "flat v3 = flat v" using as1 Left(3)
 
   896        by (simp add: Posix1(2)) 
   891        by (simp add: Posix1(2)) 
   897      ultimately have "Left v :\<sqsubseteq>val Left v3"
 
   892      ultimately have "Left v :\<sqsubseteq>val Left v3"
 
   898        by (auto simp add: PosOrd_ex1_def PosOrd_LeftI)
 
   893        by (simp add: PosOrd_ex_eq_def PosOrd_Left_eq)
 
   899      then show "Left v :\<sqsubseteq>val v2" unfolding Left .
 
   894      then show "Left v :\<sqsubseteq>val v2" unfolding Left .
 
   900   next
 
   895   next
 
   901      case (Right v3)
 
   896      case (Right v3)
 
   902      have "flat v3 = flat v" using as1 Right(3)
 
   897      have "flat v3 = flat v" using as1 Right(3)
 
   903        by (simp add: Posix1(2)) 
   898        by (simp add: Posix1(2)) 
   904      then have "Left v :\<sqsubseteq>val Right v3" using Right(3) as1 
   899      then have "Left v :\<sqsubseteq>val Right v3" using Right(3) as1 
   905        by (auto simp add: PosOrd_ex1_def PosOrd_Left_Right)
 
   900        by (auto simp add: PosOrd_ex_eq_def PosOrd_Left_Right)
 
   906      then show "Left v :\<sqsubseteq>val v2" unfolding Right .
 
   901      then show "Left v :\<sqsubseteq>val v2" unfolding Right .
 
   907   qed
 
   902   qed
 
   908 next
 
   903 next
 
   909   case (Posix_ALT2 s r2 v r1 v2)
 
   904   case (Posix_ALT2 s r2 v r1 v2)
 
   910   have as1: "s \<in> r2 \<rightarrow> v" by fact
 
   905   have as1: "s \<in> r2 \<rightarrow> v" by fact
 
   925      with IH have "v :\<sqsubseteq>val v3" by simp
 
   920      with IH have "v :\<sqsubseteq>val v3" by simp
 
   926      moreover
 
   921      moreover
 
   927      have "flat v3 = flat v" using as1 Right(3)
 
   922      have "flat v3 = flat v" using as1 Right(3)
 
   928        by (simp add: Posix1(2)) 
   923        by (simp add: Posix1(2)) 
   929      ultimately have "Right v :\<sqsubseteq>val Right v3" 
   924      ultimately have "Right v :\<sqsubseteq>val Right v3" 
   930         by (auto simp add: PosOrd_ex1_def PosOrd_RightI)
 
   925         by (auto simp add: PosOrd_ex_eq_def PosOrd_RightI)
 
   931      then show "Right v :\<sqsubseteq>val v2" unfolding Right .
 
   926      then show "Right v :\<sqsubseteq>val v2" unfolding Right .
 
   932   next
 
   927   next
 
   933      case (Left v3)
 
   928      case (Left v3)
 
   934      have "v3 \<in> CPT r1 s" using Left(2,3) as2  
   929      have "v3 \<in> CPT r1 s" using Left(2,3) as2  
   935        by (auto simp add: CPT_def prefix_list_def)
 
   930        by (auto simp add: CPT_def prefix_list_def)
 
   959     using PosOrd_spreI as1(1) eqs by blast
 
   954     using PosOrd_spreI as1(1) eqs by blast
 
   960   then have "v1 :\<sqsubset>val v3a \<or> (v3a \<in> CPT r1 s1 \<and> v3b \<in> CPT r2 s2)" using eqs(2,3)
 
   955   then have "v1 :\<sqsubset>val v3a \<or> (v3a \<in> CPT r1 s1 \<and> v3b \<in> CPT r2 s2)" using eqs(2,3)
 
   961     by (auto simp add: CPT_def)
 
   956     by (auto simp add: CPT_def)
 
   962   then have "v1 :\<sqsubset>val v3a \<or> (v1 :\<sqsubseteq>val v3a \<and> v2 :\<sqsubseteq>val v3b)" using IH1 IH2 by blast         
   957   then have "v1 :\<sqsubset>val v3a \<or> (v1 :\<sqsubseteq>val v3a \<and> v2 :\<sqsubseteq>val v3b)" using IH1 IH2 by blast         
   963   then have "Seq v1 v2 :\<sqsubseteq>val Seq v3a v3b" using eqs q2 as1
 
   958   then have "Seq v1 v2 :\<sqsubseteq>val Seq v3a v3b" using eqs q2 as1
 
   964     unfolding  PosOrd_ex1_def by (auto simp add: PosOrd_SeqI1 PosOrd_SeqI2) 
   959     unfolding  PosOrd_ex_eq_def by (auto simp add: PosOrd_SeqI1 PosOrd_SeqI2) 
   965   then show "Seq v1 v2 :\<sqsubseteq>val v3" unfolding eqs by blast
 
   960   then show "Seq v1 v2 :\<sqsubseteq>val v3" unfolding eqs by blast
 
   966 next 
   961 next 
   967   case (Posix_STAR1 s1 r v s2 vs v3) 
   962   case (Posix_STAR1 s1 r v s2 vs v3) 
   968   have "s1 \<in> r \<rightarrow> v" "s2 \<in> STAR r \<rightarrow> Stars vs" by fact+
 
   963   have "s1 \<in> r \<rightarrow> v" "s2 \<in> STAR r \<rightarrow> Stars vs" by fact+
 
   969   then have as1: "s1 = flat v" "s2 = flat (Stars vs)" by (auto dest: Posix1(2))
 
   964   then have as1: "s1 = flat v" "s2 = flat (Stars vs)" by (auto dest: Posix1(2))
 
   970   have IH1: "\<And>v3. v3 \<in> CPT r s1 \<Longrightarrow> v :\<sqsubseteq>val v3" by fact
 
   965   have IH1: "\<And>v3. v3 \<in> CPT r s1 \<Longrightarrow> v :\<sqsubseteq>val v3" by fact
 
   971   have IH2: "\<And>v3. v3 \<in> CPT (STAR r) s2 \<Longrightarrow> Stars vs :\<sqsubseteq>val v3" by fact
 
   966   have IH2: "\<And>v3. v3 \<in> CPT (STAR r) s2 \<Longrightarrow> Stars vs :\<sqsubseteq>val v3" by fact
 
   972   have cond: "\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> s1 @ s\<^sub>3 \<in> L r \<and> s\<^sub>4 \<in> L (STAR r))" by fact
 
   967   have cond: "\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> s1 @ s\<^sub>3 \<in> L r \<and> s\<^sub>4 \<in> L (STAR r))" by fact
 
   973   have cond2: "flat v \<noteq> []" by fact
 
   968   have cond2: "flat v \<noteq> []" by fact
 
   974   have "v3 \<in> CPT (STAR r) (s1 @ s2)" by fact
 
   969   have "v3 \<in> CPT (STAR r) (s1 @ s2)" by fact
 
   975   then consider
 
   970   then consider 
   976     (NonEmpty) v3a vs3 where
 
   971     (NonEmpty) v3a vs3 where "v3 = Stars (v3a # vs3)" 
   977     "v3 = Stars (v3a # vs3)" "\<Turnstile> v3a : r" "\<Turnstile> Stars vs3 : STAR r"
 
   972     "\<Turnstile> v3a : r" "\<Turnstile> Stars vs3 : STAR r"
 
   978     "flat (Stars (v3a # vs3)) = s1 @ s2"
 
   973     "flat (Stars (v3a # vs3)) = s1 @ s2"
 
   979   | (Empty) "v3 = Stars []"
 
   974   | (Empty) "v3 = Stars []"
 
   980   by (force simp add: CPT_def elim: CPrf.cases)
 
   975   unfolding CPT_def
 
   981   then show "Stars (v # vs) :\<sqsubseteq>val v3"
 
   976   apply(auto)
 
       
   977   apply(erule CPrf.cases)
 
       
   978   apply(simp_all)
 
       
   979   apply(auto)[1]
 
       
   980   apply(case_tac vs)
 
       
   981   apply(auto)
 
       
   982   using CPrf.intros(6) by blast
 
       
   983   then show "Stars (v # vs) :\<sqsubseteq>val v3" (* HERE *)
 
   982     proof (cases)
 
   984     proof (cases)
 
   983       case (NonEmpty v3a vs3)
 
   985       case (NonEmpty v3a vs3)
 
   984       have "flat (Stars (v3a # vs3)) = s1 @ s2" using NonEmpty(4) . 
   986       have "flat (Stars (v3a # vs3)) = s1 @ s2" using NonEmpty(4) . 
   985       with cond have "flat v3a \<sqsubseteq>pre s1" using NonEmpty(2,3)
 
   987       with cond have "flat v3a \<sqsubseteq>pre s1" using NonEmpty(2,3)
 
   986         unfolding prefix_list_def
 
   988         unfolding prefix_list_def
 
   991         using PosOrd_spreI as1(1) NonEmpty(4) by blast
 
   993         using PosOrd_spreI as1(1) NonEmpty(4) by blast
 
   992       then have "v :\<sqsubset>val v3a \<or> (v3a \<in> CPT r s1 \<and> Stars vs3 \<in> CPT (STAR r) s2)" 
   994       then have "v :\<sqsubset>val v3a \<or> (v3a \<in> CPT r s1 \<and> Stars vs3 \<in> CPT (STAR r) s2)" 
   993         using NonEmpty(2,3) by (auto simp add: CPT_def)
 
   995         using NonEmpty(2,3) by (auto simp add: CPT_def)
 
   994       then have "v :\<sqsubset>val v3a \<or> (v :\<sqsubseteq>val v3a \<and> Stars vs :\<sqsubseteq>val Stars vs3)" using IH1 IH2 by blast
 
   996       then have "v :\<sqsubset>val v3a \<or> (v :\<sqsubseteq>val v3a \<and> Stars vs :\<sqsubseteq>val Stars vs3)" using IH1 IH2 by blast
 
   995       then have "v :\<sqsubset>val v3a \<or> (v = v3a \<and> Stars vs :\<sqsubseteq>val Stars vs3)" 
   997       then have "v :\<sqsubset>val v3a \<or> (v = v3a \<and> Stars vs :\<sqsubseteq>val Stars vs3)" 
   996          unfolding PosOrd_ex1_def by auto     
   998          unfolding PosOrd_ex_eq_def by auto     
   997       then have "Stars (v # vs) :\<sqsubseteq>val Stars (v3a # vs3)" using NonEmpty(4) q2 as1
 
   999       then have "Stars (v # vs) :\<sqsubseteq>val Stars (v3a # vs3)" using NonEmpty(4) q2 as1
 
   998         unfolding  PosOrd_ex1_def
 
  1000         unfolding  PosOrd_ex_eq_def
 
   999         by (metis PosOrd_StarsI PosOrd_StarsI2 flat.simps(7) val.inject(5))
 
  1001         by (metis PosOrd_StarsI PosOrd_StarsI2 flat.simps(7) val.inject(5))
 
  1000       then show "Stars (v # vs) :\<sqsubseteq>val v3" unfolding NonEmpty by blast
 
  1002       then show "Stars (v # vs) :\<sqsubseteq>val v3" unfolding NonEmpty by blast
 
  1001     next 
  1003     next 
  1002       case Empty
 
  1004       case Empty
 
  1003       have "v3 = Stars []" by fact
 
  1005       have "v3 = Stars []" by fact
 
  1004       then show "Stars (v # vs) :\<sqsubseteq>val v3"
 
  1006       then show "Stars (v # vs) :\<sqsubseteq>val v3"
 
  1005       unfolding PosOrd_ex1_def using cond2
 
  1007       unfolding PosOrd_ex_eq_def using cond2
 
  1006       by (simp add: PosOrd_shorterI)
 
  1008       by (simp add: PosOrd_shorterI)
 
  1007     qed      
  1009     qed      
  1008 next 
  1010 next 
  1009   case (Posix_STAR2 r v2)
 
  1011   case (Posix_STAR2 r v2)
 
  1010   have "v2 \<in> CPT (STAR r) []" by fact
 
  1012   have "v2 \<in> CPT (STAR r) []" by fact
 
  1011   then have "v2 = Stars []" 
  1013   then have "v2 = Stars []" 
  1012     unfolding CPT_def by (auto elim: CPrf.cases) 
  1014     unfolding CPT_def by (auto elim: CPrf.cases) 
  1013   then show "Stars [] :\<sqsubseteq>val v2"
 
  1015   then show "Stars [] :\<sqsubseteq>val v2"
 
  1014   by (simp add: PosOrd_ex1_def)
 
  1016   by (simp add: PosOrd_ex_eq_def)
 
  1015 qed
 
  1017 qed
 
  1016 
  1018 
  1017 lemma Posix_PosOrd_stronger:
 
  1019 lemma Posix_PosOrd_stronger:
 
  1018   assumes "s \<in> r \<rightarrow> v1" "v2 \<in> CPTpre r s" 
  1020   assumes "s \<in> r \<rightarrow> v1" "v2 \<in> CPTpre r s" 
  1019   shows "v1 :\<sqsubseteq>val v2"
 
  1021   shows "v1 :\<sqsubseteq>val v2"
 
  1028   moreover
 
  1030   moreover
 
  1029     { assume "flat v2 \<sqsubset>spre s"
 
  1031     { assume "flat v2 \<sqsubset>spre s"
 
  1030       then have "flat v2 \<sqsubset>spre flat v1" using assms(1)
 
  1032       then have "flat v2 \<sqsubset>spre flat v1" using assms(1)
 
  1031         using Posix1(2) by blast
 
  1033         using Posix1(2) by blast
 
  1032       then have "v1 :\<sqsubseteq>val v2"
 
  1034       then have "v1 :\<sqsubseteq>val v2"
 
  1033         by (simp add: PosOrd_ex1_def PosOrd_spreI) 
  1035         by (simp add: PosOrd_ex_eq_def PosOrd_spreI) 
  1034     }
 
  1036     }
 
  1035   ultimately show "v1 :\<sqsubseteq>val v2" by blast
 
  1037   ultimately show "v1 :\<sqsubseteq>val v2" by blast
 
  1036 qed
 
  1038 qed
 
  1037 
  1039 
  1038 lemma Posix_PosOrd_reverse:
 
  1040 lemma Posix_PosOrd_reverse:
 
  1039   assumes "s \<in> r \<rightarrow> v1" 
  1041   assumes "s \<in> r \<rightarrow> v1" 
  1040   shows "\<not>(\<exists>v2 \<in> CPTpre r s. v2 :\<sqsubset>val v1)"
 
  1042   shows "\<not>(\<exists>v2 \<in> CPTpre r s. v2 :\<sqsubset>val v1)"
 
  1041 using assms
 
  1043 using assms
 
  1042 by (metis Posix_PosOrd_stronger less_irrefl PosOrd_def 
  1044 by (metis Posix_PosOrd_stronger less_irrefl PosOrd_def 
  1043     PosOrd_ex1_def PosOrd_ex_def PosOrd_trans)
 
  1045     PosOrd_ex_eq_def PosOrd_ex_def PosOrd_trans)
 
  1044 
  1046 
  1045 
  1047 (*
 
  1046 lemma PosOrd_Posix_Stars:
 
  1048 lemma PosOrd_Posix_Stars:
 
  1047   assumes "(Stars vs) \<in> CPT (STAR r) (flat (Stars vs))" "\<forall>v \<in> set vs. flat v \<in> r \<rightarrow> v"
 
  1049   assumes "(Stars vs) \<in> CPT (STAR r) (flat (Stars vs))" "\<forall>v \<in> set vs. flat v \<in> r \<rightarrow> v"
 
  1048   and "\<not>(\<exists>vs2 \<in> PT (STAR r) (flat (Stars vs)). vs2 :\<sqsubset>val (Stars vs))"
 
  1050   and "\<not>(\<exists>vs2 \<in> PT (STAR r) (flat (Stars vs)). vs2 :\<sqsubset>val (Stars vs))"
 
  1049   shows "(flat (Stars vs)) \<in> (STAR r) \<rightarrow> Stars vs" 
  1051   shows "(flat (Stars vs)) \<in> (STAR r) \<rightarrow> Stars vs" 
  1050 using assms
 
  1052 using assms
 
  1113 apply(simp)
 
  1115 apply(simp)
 
  1114 apply(subst (asm) (2) PosOrd_ex_def)
 
  1116 apply(subst (asm) (2) PosOrd_ex_def)
 
  1115 apply(simp)
 
  1117 apply(simp)
 
  1116 apply (metis flat.simps(7) flat_Stars PosOrd_StarsI2 PosOrd_ex_def)
 
  1118 apply (metis flat.simps(7) flat_Stars PosOrd_StarsI2 PosOrd_ex_def)
 
  1117 by (metis PosOrd_StarsI PosOrd_ex_def PosOrd_spreI append_assoc append_self_conv flat.simps(7) flat_Stars prefix_list_def sprefix_list_def)
 
  1119 by (metis PosOrd_StarsI PosOrd_ex_def PosOrd_spreI append_assoc append_self_conv flat.simps(7) flat_Stars prefix_list_def sprefix_list_def)
 
       
  1120 *)
 
       
  1121 
       
  1122 
       
  1123 lemma test2: 
       
  1124   assumes "\<forall>v \<in> set vs. flat v \<in> r \<rightarrow> v \<and> flat v \<noteq> []"
 
       
  1125   shows "(Stars vs) \<in> CPT (STAR r) (flat (Stars vs))" 
       
  1126 using assms
 
       
  1127 apply(induct vs)
 
       
  1128 apply(auto simp add: CPT_def)
 
       
  1129 apply(rule CPrf.intros)
 
       
  1130 apply(simp)
 
       
  1131 apply(rule CPrf.intros)
 
       
  1132 apply(simp_all)
 
       
  1133 by (metis (no_types, lifting) CPT_def Posix_CPT mem_Collect_eq)
 
       
  1134 
       
  1135 
       
  1136 lemma PosOrd_Posix_Stars:
 
       
  1137   assumes "\<forall>v \<in> set vs. flat v \<in> r \<rightarrow> v \<and> flat v \<noteq> []"
 
       
  1138   and "\<not>(\<exists>vs2 \<in> PT (STAR r) (flat (Stars vs)). vs2 :\<sqsubset>val (Stars vs))"
 
       
  1139   shows "(flat (Stars vs)) \<in> (STAR r) \<rightarrow> Stars vs" 
       
  1140 using assms
 
       
  1141 proof(induct vs)
 
       
  1142   case Nil
 
       
  1143   show "flat (Stars []) \<in> STAR r \<rightarrow> Stars []"
 
       
  1144     by(simp add: Posix.intros)
 
       
  1145 next
 
       
  1146   case (Cons v vs)
 
       
  1147   have IH: "\<lbrakk>\<forall>v\<in>set vs. flat v \<in> r \<rightarrow> v \<and> flat v \<noteq> []; 
       
  1148              \<not> (\<exists>vs2\<in>PT (STAR r) (flat (Stars vs)). vs2 :\<sqsubset>val Stars vs)\<rbrakk>
 
       
  1149              \<Longrightarrow> flat (Stars vs) \<in> STAR r \<rightarrow> Stars vs" by fact
 
       
  1150   have as2: "\<forall>v\<in>set (v # vs). flat v \<in> r \<rightarrow> v \<and> flat v \<noteq> []" by fact
 
       
  1151   have as3: "\<not> (\<exists>vs2\<in>PT (STAR r) (flat (Stars (v # vs))). vs2 :\<sqsubset>val Stars (v # vs))" by fact
 
       
  1152   have "flat v \<in> r \<rightarrow> v" using as2 by simp
 
       
  1153   moreover
 
       
  1154   have  "flat (Stars vs) \<in> STAR r \<rightarrow> Stars vs" 
       
  1155     proof (rule IH)
 
       
  1156       show "\<forall>v\<in>set vs. flat v \<in> r \<rightarrow> v \<and> flat v \<noteq> []" using as2 by simp
 
       
  1157     next 
       
  1158       show "\<not> (\<exists>vs2\<in>PT (STAR r) (flat (Stars vs)). vs2 :\<sqsubset>val Stars vs)" using as3
 
       
  1159         apply(auto)
 
       
  1160         apply(subst (asm) (2) PT_def)
 
       
  1161         apply(auto)
 
       
  1162         apply(erule Prf.cases)
 
       
  1163         apply(simp_all)
 
       
  1164         apply(drule_tac x="Stars (v # vs)" in bspec)
 
       
  1165         apply(simp add: PT_def CPT_def)
 
       
  1166         using Posix1a Prf.intros(6) calculation
 
       
  1167         apply(rule_tac Prf.intros)
 
       
  1168         apply(simp add:)
 
       
  1169         apply (simp add: PosOrd_StarsI2)
 
       
  1170         done
 
       
  1171     qed
 
       
  1172   moreover
 
       
  1173   have "flat v \<noteq> []" using as2 by simp
 
       
  1174   moreover
 
       
  1175   have "\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = flat (Stars vs) \<and> flat v @ s\<^sub>3 \<in> L r \<and> s\<^sub>4 \<in> L (STAR r))" 
       
  1176    using as3
 
       
  1177    apply(auto)
 
       
  1178    apply(drule L_flat_Prf2)
 
       
  1179    apply(erule exE)
 
       
  1180    apply(simp only: L.simps[symmetric])
 
       
  1181    apply(drule L_flat_Prf2)
 
       
  1182    apply(erule exE)
 
       
  1183    apply(clarify)
 
       
  1184    apply(rotate_tac 5)
 
       
  1185    apply(erule Prf.cases)
 
       
  1186    apply(simp_all)
 
       
  1187    apply(clarify)
 
       
  1188    apply(drule_tac x="Stars (va#vs)" in bspec)
 
       
  1189    apply(auto simp add: PT_def)[1]   
       
  1190    apply(rule Prf.intros)
 
       
  1191    apply(simp)
 
       
  1192    by (simp add: PosOrd_StarsI PosOrd_shorterI)
 
       
  1193   ultimately show "flat (Stars (v # vs)) \<in> STAR r \<rightarrow> Stars (v # vs)"
 
       
  1194   by (simp add: Posix.intros)
 
       
  1195 qed
 
       
  1196 
  1118 
  1197 
  1119 
  1198 
  1120 section {* The Smallest Value is indeed the Posix Value *}
 
  1199 section {* The Smallest Value is indeed the Posix Value *}
 
  1121 
  1200 
       
  1201 text {*
 
       
  1202   The next lemma seems to require PT instead of CPT in the Star-case.
 
       
  1203 *}
 
       
  1204 
  1122 lemma PosOrd_Posix:
 
  1205 lemma PosOrd_Posix:
 
  1123   assumes "v1 \<in> CPT r s" "\<forall>v2 \<in> PT r s. \<not> v2 :\<sqsubset>val v1"
 
  1206   assumes "v1 \<in> CPT r s" "\<forall>v\<^sub>2 \<in> PT r s. \<not> v\<^sub>2 :\<sqsubset>val v1"
 
  1124   shows "s \<in> r \<rightarrow> v1" 
  1207   shows "s \<in> r \<rightarrow> v1" 
  1125 using assms
 
  1208 using assms
 
  1126 proof(induct r arbitrary: s v1)
 
  1209 proof(induct r arbitrary: s v1)
 
  1127   case (ZERO s v1)
 
  1210   case (ZERO s v1)
 
  1128   have "v1 \<in> CPT ZERO s" by fact
 
  1211   have "v1 \<in> CPT ZERO s" by fact
 
  1157      case (Left v1')
 
  1240      case (Left v1')
 
  1158      have "v1' \<in> CPT r1 s" using as2
 
  1241      have "v1' \<in> CPT r1 s" using as2
 
  1159        unfolding CPT_def Left by (auto elim: CPrf.cases)
 
  1242        unfolding CPT_def Left by (auto elim: CPrf.cases)
 
  1160      moreover
 
  1243      moreover
 
  1161      have "\<forall>v2 \<in> PT r1 s. \<not> v2 :\<sqsubset>val v1'" using as1
 
  1244      have "\<forall>v2 \<in> PT r1 s. \<not> v2 :\<sqsubset>val v1'" using as1
 
  1162        unfolding PT_def Left using Prf.intros(2) PosOrd_LeftI by force  
  1245        unfolding PT_def Left using Prf.intros(2) PosOrd_Left_eq by force  
  1163      ultimately have "s \<in> r1 \<rightarrow> v1'" using IH1 by simp
 
  1246      ultimately have "s \<in> r1 \<rightarrow> v1'" using IH1 by simp
 
  1164      then have "s \<in> ALT r1 r2 \<rightarrow> Left v1'" by (rule Posix.intros)
 
  1247      then have "s \<in> ALT r1 r2 \<rightarrow> Left v1'" by (rule Posix.intros)
 
  1165      then show "s \<in> ALT r1 r2 \<rightarrow> v1" using Left by simp
 
  1248      then show "s \<in> ALT r1 r2 \<rightarrow> v1" using Left by simp
 
  1166    next
 
  1249    next
 
  1167      case (Right v1')
 
  1250      case (Right v1')
 
  1246    then obtain 
  1329    then obtain 
  1247     vs where eqs:
 
  1330     vs where eqs:
 
  1248         "v1 = Stars vs" "s = flat (Stars vs)"
 
  1331         "v1 = Stars vs" "s = flat (Stars vs)"
 
  1249         "\<forall>v \<in> set vs. v \<in> CPT r (flat v)"
 
  1332         "\<forall>v \<in> set vs. v \<in> CPT r (flat v)"
 
  1250         unfolding CPT_def by (auto elim: CPrf.cases dest!: CPrf_stars)
 
  1333         unfolding CPT_def by (auto elim: CPrf.cases dest!: CPrf_stars)
 
  1251    have "Stars vs \<in> CPT (STAR r) (flat (Stars vs))" 
  1334    have "\<forall>v\<in>set vs. flat v \<in> r \<rightarrow> v \<and> flat v \<noteq> []" 
  1252      using as2 unfolding eqs .
 
       
  1253    moreover
 
       
  1254    have "\<forall>v\<in>set vs. flat v \<in> r \<rightarrow> v" 
       
  1255      proof 
  1335      proof 
  1256         fix v
 
  1336         fix v
 
  1257         assume a: "v \<in> set vs"
 
  1337         assume a: "v \<in> set vs"
 
  1258         then obtain pre post where e: "vs = pre @ [v] @ post"
 
  1338         then obtain pre post where e: "vs = pre @ [v] @ post"
 
  1259           by (metis append_Cons append_Nil in_set_conv_decomp_first)
 
  1339           by (metis append_Cons append_Nil in_set_conv_decomp_first)
 
  1264              fix v2
 
  1344              fix v2
 
  1265              assume w: "v2 :\<sqsubset>val v"
 
  1345              assume w: "v2 :\<sqsubset>val v"
 
  1266              assume "v2 \<in> PT r (flat v)"
 
  1346              assume "v2 \<in> PT r (flat v)"
 
  1267              then have "Stars (pre @ [v2] @ post) \<in> PT (STAR r) s" 
  1347              then have "Stars (pre @ [v2] @ post) \<in> PT (STAR r) s" 
  1268                  using as2 unfolding e eqs
 
  1348                  using as2 unfolding e eqs
 
  1269                  apply(auto simp add: CPT_def PT_def intro!: Prf_Stars)[1]
 
  1349                  apply(auto simp add: CPT_def PT_def intro!: Prf.intros)[1]
 
  1270                  using CPrf_Stars_appendE CPrf_stars Prf_CPrf apply blast
 
  1350                  using CPrf_Stars_appendE CPrf_stars Prf_CPrf apply blast
 
  1271                  by (meson CPrf_Stars_appendE CPrf_stars Prf_CPrf list.set_intros(2))
 
  1351                  by (meson CPrf_Stars_appendE CPrf_stars Prf_CPrf list.set_intros(2))
 
  1272              then have  "\<not> Stars (pre @ [v2] @ post) :\<sqsubset>val Stars (pre @ [v] @ post)"
 
  1352              then have  "\<not> Stars (pre @ [v2] @ post) :\<sqsubset>val Stars (pre @ [v] @ post)"
 
  1273                 using q by simp     
  1353                 using q by simp     
  1274              with w show "False"
 
  1354              with w show "False"
 
  1275                 using PT_def \<open>v2 \<in> PT r (flat v)\<close> append_Cons flat.simps(7) mem_Collect_eq 
  1355                 using PT_def \<open>v2 \<in> PT r (flat v)\<close> append_Cons flat.simps(7) mem_Collect_eq 
  1276                 PosOrd_StarsI PosOrd_Stars_appendI by auto
 
  1356                 PosOrd_StarsI PosOrd_Stars_appendI by auto
 
  1277           qed     
  1357           qed     
  1278         with IH
 
  1358         with IH
 
  1279         show "flat v \<in> r \<rightarrow> v" using a as2 unfolding eqs
 
  1359         show "flat v \<in> r \<rightarrow> v \<and> flat v \<noteq> []" using a as2 unfolding eqs
 
  1280           using eqs(3) by blast
 
  1360           using eqs(3) by (smt CPT_def CPrf_stars mem_Collect_eq) 
  1281      qed
 
  1361      qed
 
  1282    moreover
 
  1362    moreover
 
  1283    have "\<not> (\<exists>vs2\<in>PT (STAR r) (flat (Stars vs)). vs2 :\<sqsubset>val Stars vs)" 
  1363    have "\<not> (\<exists>vs2\<in>PT (STAR r) (flat (Stars vs)). vs2 :\<sqsubset>val Stars vs)" 
  1284      proof 
  1364      proof 
  1285        assume "\<exists>vs2 \<in> PT (STAR r) (flat (Stars vs)). vs2 :\<sqsubset>val Stars vs"
 
  1365        assume "\<exists>vs2 \<in> PT (STAR r) (flat (Stars vs)). vs2 :\<sqsubset>val Stars vs"
 
  1287                              "Stars vs2 :\<sqsubset>val Stars vs" 
  1367                              "Stars vs2 :\<sqsubset>val Stars vs" 
  1288          unfolding PT_def
 
  1368          unfolding PT_def
 
  1289          apply(auto elim: Prf.cases)
 
  1369          apply(auto elim: Prf.cases)
 
  1290          apply(erule Prf.cases)
 
  1370          apply(erule Prf.cases)
 
  1291          apply(auto intro: Prf.intros)
 
  1371          apply(auto intro: Prf.intros)
 
  1292          apply(drule_tac x="[]" in meta_spec) 
       
  1293          apply(simp)
 
       
  1294          apply(drule meta_mp)
 
       
  1295          apply(auto intro: Prf.intros)
 
       
  1296          apply(drule_tac x="(v#vsa)" in meta_spec)
 
       
  1297          apply(auto intro: Prf.intros)
 
       
  1298          done
 
  1372          done
 
  1299        then show "False" using as1 unfolding eqs
 
  1373        then show "False" using as1 unfolding eqs
 
  1300          apply -
 
  1374          apply -
 
  1301          apply(drule_tac x="Stars vs2" in bspec)
 
  1375          apply(drule_tac x="Stars vs2" in bspec)
 
  1302          apply(auto simp add: PT_def)
 
  1376          apply(auto simp add: PT_def)
 
  1303          done
 
  1377          done
 
  1304      qed
 
  1378      qed
 
  1305    ultimately have "flat (Stars vs) \<in> STAR r \<rightarrow> Stars vs" 
  1379    ultimately have "flat (Stars vs) \<in> STAR r \<rightarrow> Stars vs"
 
       
  1380      thm PosOrd_Posix_Stars
 
  1306      by (rule PosOrd_Posix_Stars)
 
  1381      by (rule PosOrd_Posix_Stars)
 
  1307    then show "s \<in> STAR r \<rightarrow> v1" unfolding eqs .
 
  1382    then show "s \<in> STAR r \<rightarrow> v1" unfolding eqs .
 
  1308 qed
 
  1383 qed
 
  1309 
  1384 
  1310 unused_thms
 
  1385 unused_thms
lexing