1.1 --- a/thys/Program-Conflict-Analysis/AcquisitionHistory.thy Mon Nov 02 18:43:26 2009 +0100
1.2 +++ b/thys/Program-Conflict-Analysis/AcquisitionHistory.thy Wed Nov 04 09:19:37 2009 +0100
1.3 @@ -111,10 +111,10 @@
1.4
1.5 -- {* Subwords generate smaller acquisition histories *}
1.6 lemma \<alpha>ah_ileq: "w1\<preceq>w2 \<Longrightarrow> \<alpha>ah w1 \<le> \<alpha>ah w2"
1.7 -proof (induct rule: ileq_induct)
1.8 +proof (induct rule: less_eq_list.induct)
1.9 case empty thus ?case by (unfold le_fun_def [where 'b="'a \<Rightarrow> bool"], simp)
1.10 next
1.11 - case (drop a l l') show ?case
1.12 + case (drop l' l a) show ?case
1.13 proof (unfold le_fun_def [where 'b="'a \<Rightarrow> bool"], intro allI subsetI)
1.14 fix m x
1.15 assume A: "x \<in> \<alpha>ah l' m"
1.16 @@ -123,7 +123,7 @@
1.17 ultimately show "x\<in>\<alpha>ah (a # l) m" by auto
1.18 qed
1.19 next
1.20 - case (take a l l') show ?case
1.21 + case (take l' l a) show ?case
1.22 proof (unfold le_fun_def [where 'b="'a \<Rightarrow> bool"], intro allI subsetI)
1.23 fix m x
1.24 assume A: "x\<in>\<alpha>ah (a#l') m"
1.25 @@ -211,7 +211,7 @@
1.26 case True -- "The first step of the first word can safely be executed"
1.27 -- "From the induction hypothesis, we get that there is a consistent interleaving of the rest of the first word and the second word"
1.28 have "w1'\<otimes>\<^bsub>\<alpha>\<^esub>w2 \<noteq> {}" proof -
1.29 - from I.prems(1) CONS1 ah_leq_il_left[OF _ \<alpha>ah_ileq[OF ileq_map, OF ileq_drop[OF order_refl]]] have "\<alpha>ah (map \<alpha> w1') [*] \<alpha>ah (map \<alpha> w2)" by fast
1.30 + from I.prems(1) CONS1 ah_leq_il_left[OF _ \<alpha>ah_ileq[OF le_list_map, OF less_eq_list.drop[OF order_refl]]] have "\<alpha>ah (map \<alpha> w1') [*] \<alpha>ah (map \<alpha> w2)" by fast
1.31 moreover from CONS1 I.prems(2) have "length w1'+length w2 < n" by simp
1.32 ultimately show ?thesis using I.hyps by blast
1.33 qed
1.34 @@ -223,7 +223,7 @@
1.35 case True -- "The first step of the second word can safely be executed"
1.36 -- "This case is shown analogously to the latter one"
1.37 have "w1\<otimes>\<^bsub>\<alpha>\<^esub>w2' \<noteq> {}" proof -
1.38 - from I.prems(1) CONS2 ah_leq_il_right[OF _ \<alpha>ah_ileq[OF ileq_map, OF ileq_drop[OF order_refl]]] have "\<alpha>ah (map \<alpha> w1) [*] \<alpha>ah (map \<alpha> w2')" by fast
1.39 + from I.prems(1) CONS2 ah_leq_il_right[OF _ \<alpha>ah_ileq[OF le_list_map, OF less_eq_list.drop[OF order_refl]]] have "\<alpha>ah (map \<alpha> w1) [*] \<alpha>ah (map \<alpha> w2')" by fast
1.40 moreover from CONS2 I.prems(2) have "length w1+length w2' < n" by simp
1.41 ultimately show ?thesis using I.hyps by blast
1.42 qed
2.1 --- a/thys/Program-Conflict-Analysis/ConsInterleave.thy Mon Nov 02 18:43:26 2009 +0100
2.2 +++ b/thys/Program-Conflict-Analysis/ConsInterleave.thy Wed Nov 04 09:19:37 2009 +0100
2.3 @@ -28,7 +28,7 @@
2.4 by (induct a) auto
2.5
2.6 lemma mon_pl_ileq: "w\<preceq>w' \<Longrightarrow> mon_pl w \<subseteq> mon_pl w'"
2.7 - by (induct rule: ileq_induct) auto
2.8 + by (induct rule: less_eq_list.induct) auto
2.9
2.10 lemma mon_pl_set: "mon_pl w = \<Union>{ fst e \<union> snd e | e. e\<in>set w }"
2.11 by (unfold mon_pl_def) (safe, auto simp add: Bex_def foldl_set)
3.1 --- a/thys/Program-Conflict-Analysis/ConstraintSystems.thy Mon Nov 02 18:43:26 2009 +0100
3.2 +++ b/thys/Program-Conflict-Analysis/ConstraintSystems.thy Wed Nov 04 09:19:37 2009 +0100
3.3 @@ -387,7 +387,7 @@
3.4 from Cons.prems(2) LESPLIT(2) have "atU U (({#s'#}+c1') + c2')" by (auto simp add: union_ac)
3.5 thus ?case proof (cases rule: atU_union_cases)
3.6 case left -- {* @{term U} was reached from the local thread *}
3.7 - from cil_ileq[OF LESPLIT(1)] have ILEQ: "w1\<preceq>wwl" and LEN: "length w1 \<le> length wwl" by (auto simp add: ileq_length)
3.8 + from cil_ileq[OF LESPLIT(1)] have ILEQ: "w1\<preceq>wwl" and LEN: "length w1 \<le> length wwl" by (auto simp add: le_list_length)
3.9 -- "We can cut off the bottom stack symbol from the reaching path (as always possible for normalized paths)"
3.10 from FS_FMT(3) LESPLIT(3) ntrp_stack_decomp[of v "[]" "[u']" "{#}" w1 s' c1' fg, simplified] obtain v' rr where DECOMP: "s'=v'#rr@[u']" "(([v],{#}),w1,(v'#rr,c1'))\<in>trcl (ntrp fg)" by auto
3.11 -- "This does not affect the configuration being at @{term U}"
3.12 @@ -407,26 +407,26 @@
3.13 moreover have "ah_update h (mon fg p, mon_w fg w) (Ml \<union> Me) \<le> \<alpha>ah (map (\<alpha>nl fg) (eel#wwl))" proof (simp add: ah_update_cons)
3.14 show "ah_update h (mon fg p, mon_w fg w) (Ml \<union> Me) \<le> ah_update (\<alpha>ah (map (\<alpha>nl fg) wwl)) (\<alpha>nl fg eel) (mon_pl (map (\<alpha>nl fg) wwl))" proof (rule ah_update_mono)
3.15 from IHAPP(4) have "h \<le> \<alpha>ah (map (\<alpha>nl fg) w1)" .
3.16 - also from \<alpha>ah_ileq[OF ileq_map[OF ILEQ]] have "\<alpha>ah (map (\<alpha>nl fg) w1) \<le> \<alpha>ah (map (\<alpha>nl fg) wwl)" .
3.17 + also from \<alpha>ah_ileq[OF le_list_map[OF ILEQ]] have "\<alpha>ah (map (\<alpha>nl fg) w1) \<le> \<alpha>ah (map (\<alpha>nl fg) wwl)" .
3.18 finally show "h \<le> \<alpha>ah (map (\<alpha>nl fg) wwl)" .
3.19 next
3.20 from FS_FMT(1) show "(mon fg p, mon_w fg w) = \<alpha>nl fg eel" by auto
3.21 next
3.22 from IHAPP(2,3) have "(Ml \<union> Me) \<subseteq> mon_pl (map (\<alpha>nl fg) w1)" by (auto simp add: mon_pl_of_\<alpha>nl)
3.23 - also from mon_pl_ileq[OF ileq_map[OF ILEQ]] have "\<dots> \<subseteq> mon_pl (map (\<alpha>nl fg) wwl)" .
3.24 + also from mon_pl_ileq[OF le_list_map[OF ILEQ]] have "\<dots> \<subseteq> mon_pl (map (\<alpha>nl fg) wwl)" .
3.25 finally show "(Ml \<union> Me) \<subseteq> mon_pl (map (\<alpha>nl fg) wwl)" .
3.26 qed
3.27 qed
3.28 ultimately show ?thesis by blast
3.29 next
3.30 case right -- {* @{term U} was reached from the spawned threads *}
3.31 - from cil_ileq[OF LESPLIT(1)] ileq_length[of "map ENV w2" "wwl"] have ILEQ: "map ENV w2\<preceq>wwl" and LEN: "length w2 \<le> length wwl" by (auto)
3.32 + from cil_ileq[OF LESPLIT(1)] le_list_length[of "map ENV w2" "wwl"] have ILEQ: "map ENV w2\<preceq>wwl" and LEN: "length w2 \<le> length wwl" by (auto)
3.33 from HVALID have CHVALID: "valid fg ch" "mon_s fg sh \<inter> mon_c fg ch = {}" by (auto simp add: valid_unconc)
3.34 -- {* We first identify the actual thread from that @{term U} was reached *}
3.35 from ntr_reverse_split_atU[OF CHVALID(1) right LESPLIT(4)] obtain q wr cr' where RI: "[entry fg q] :# ch" "wr\<preceq>w2" "cr'\<le>#c2'" "atU U cr'" "({#[entry fg q]#},wr,cr')\<in>trcl (ntr fg)" by (blast dest: CHFMT)
3.36 -- "In order to apply the induction hypothesis, we have to convert the reaching path to loc/env semantics"
3.37 from ntrs.gtr2gtrp[where c="{#}", simplified, OF RI(5)] obtain sr' cre' wwr where RI_NTRP: "cr'={#sr'#}+cre'" "wr=map le_rem_s wwr" "(([entry fg q],{#}),wwr,(sr',cre'))\<in>trcl (ntrp fg)" by blast
3.38 - from LEN ileq_length[OF RI(2)] RI_NTRP(2) have LEN': "length wwr \<le> length wwl" by simp
3.39 + from LEN le_list_length[OF RI(2)] RI_NTRP(2) have LEN': "length wwr \<le> length wwl" by simp
3.40 -- "The induction hypothesis yields a constraint system entry"
3.41 from Cons.hyps[OF LEN' RI_NTRP(3)] RI_NTRP(1) RI(4) obtain Ml Me h where IHAPP: "(entry fg q, Ml, Me, h)\<in>RU_cs fg U" "Ml \<subseteq> mon_loc fg wwr" "Me \<subseteq> mon_env fg wwr" "h \<le> \<alpha>ah (map (\<alpha>nl fg) wwr)" by auto
3.42 -- {* We also have an entry in the same-level path constraint system that contains the thread from that @{term U} was reached *}
3.43 @@ -451,9 +451,9 @@
3.44 proof (simp add: ah_update_cons)
3.45 have MAP_HELPER: "map (\<alpha>nl fg) wwr \<preceq> map (\<alpha>nl fg) wwl" proof -
3.46 from RI_NTRP(2) have "map (\<alpha>nl fg) wwr = map (\<alpha>n fg) wr" by (simp add: \<alpha>n_map2_\<alpha>nl)
3.47 - also from ileq_map[OF RI(2)] have "\<dots> \<preceq> map (\<alpha>n fg) w2" .
3.48 + also from le_list_map[OF RI(2)] have "\<dots> \<preceq> map (\<alpha>n fg) w2" .
3.49 also have "\<dots> = map (\<alpha>nl fg) (map ENV w2)" by simp
3.50 - also from ileq_map[OF ILEQ] have "\<dots> \<preceq> map (\<alpha>nl fg) wwl" .
3.51 + also from le_list_map[OF ILEQ] have "\<dots> \<preceq> map (\<alpha>nl fg) wwl" .
3.52 finally show "?thesis" .
3.53 qed
3.54 show "ah_update h (mon fg p, mon_w fg w) (Ml \<union> Me) \<le> ah_update (\<alpha>ah (map (\<alpha>nl fg) wwl)) (\<alpha>nl fg eel) (mon_pl (map (\<alpha>nl fg) wwl))" proof (rule ah_update_mono)
3.55 @@ -717,7 +717,7 @@
3.56 finally show "h \<le> \<alpha>ah (map (\<alpha>n fg) w21)" .
3.57 next
3.58 note RV(4)
3.59 - also have "map (\<alpha>nl fg) ww22' \<preceq> map (\<alpha>n fg) w22" using R_CONV'(2) REVSPLIT'(2) by (simp add: \<alpha>n_map2_\<alpha>nl[symmetric] ileq_map)
3.60 + also have "map (\<alpha>nl fg) ww22' \<preceq> map (\<alpha>n fg) w22" using R_CONV'(2) REVSPLIT'(2) by (simp add: \<alpha>n_map2_\<alpha>nl[symmetric] le_list_map)
3.61 hence "\<alpha>ah (map (\<alpha>nl fg) ww22') \<le> \<alpha>ah (map (\<alpha>n fg) w22)" by (rule \<alpha>ah_ileq)
3.62 finally show "h' \<le> \<alpha>ah (map (\<alpha>n fg) w22)" .
3.63 qed
3.64 @@ -737,7 +737,7 @@
3.65 from ntrs.gtr2gtrp[where c="{#}", simplified, OF REVSPLIT(5)] obtain s2i' c2ie' ww2' where R_CONV: "c2i'={#s2i'#}+c2ie'" "w2'=map le_rem_s ww2'" "(([entry fg q'], {#}), ww2', s2i', c2ie') \<in> trcl (ntrp fg)" .
3.66 from RU_sound[OF R_CONV(3), of V] REVSPLIT(4) R_CONV(1) obtain Ml' Me' h' where RV: "(entry fg q', Ml', Me', h') \<in> RU_cs fg V" "Ml' \<subseteq> mon_loc fg ww2'" "Me' \<subseteq> mon_env fg ww2'" "h' \<le> \<alpha>ah (map (\<alpha>nl fg) ww2')" by auto
3.67 moreover have "mon_loc fg ww2' \<subseteq> mon_ww fg w2" "mon_env fg ww2' \<subseteq> mon_ww fg w2" using mon_ww_ileq[OF REVSPLIT(2), of fg] R_CONV(2) by (auto simp add: mon_ww_of_le_rem)
3.68 - moreover have "\<alpha>ah (map (\<alpha>nl fg) ww2') \<le> \<alpha>ah (map (\<alpha>n fg) w2)" using REVSPLIT(2) R_CONV(2) by (auto simp add: \<alpha>n_map2_\<alpha>nl[symmetric] ileq_map intro: \<alpha>ah_ileq del: predicate2I)
3.69 + moreover have "\<alpha>ah (map (\<alpha>nl fg) ww2') \<le> \<alpha>ah (map (\<alpha>n fg) w2)" using REVSPLIT(2) R_CONV(2) by (auto simp add: \<alpha>n_map2_\<alpha>nl[symmetric] le_list_map intro: \<alpha>ah_ileq del: predicate2I)
3.70 ultimately show ?thesis using goal1 REVSPLIT(1) by (blast intro: order_trans)
3.71 qed
3.72 from S_ENTRY_PAT[of "{#q'#}", simplified] RV(1) have S_ENTRY: "(v, mon_w fg w, {#q'#}) \<in> S_cs fg 1" by simp
3.73 @@ -761,7 +761,7 @@
3.74 from ntrs.gtr2gtrp[where c="{#}", simplified, OF REVSPLIT(5)] obtain s2i' c2ie' ww2' where R_CONV: "c2i'={#s2i'#}+c2ie'" "w2'=map le_rem_s ww2'" "(([entry fg q'], {#}), ww2', s2i', c2ie') \<in> trcl (ntrp fg)" .
3.75 from RU_sound[OF R_CONV(3), of U] REVSPLIT(4) R_CONV(1) obtain Ml' Me' h' where RU: "(entry fg q', Ml', Me', h') \<in> RU_cs fg U" "Ml' \<subseteq> mon_loc fg ww2'" "Me' \<subseteq> mon_env fg ww2'" "h' \<le> \<alpha>ah (map (\<alpha>nl fg) ww2')" by auto
3.76 moreover have "mon_loc fg ww2' \<subseteq> mon_ww fg w2" "mon_env fg ww2' \<subseteq> mon_ww fg w2" using mon_ww_ileq[OF REVSPLIT(2), of fg] R_CONV(2) by (auto simp add: mon_ww_of_le_rem)
3.77 - moreover have "\<alpha>ah (map (\<alpha>nl fg) ww2') \<le> \<alpha>ah (map (\<alpha>n fg) w2)" using REVSPLIT(2) R_CONV(2) by (auto simp add: \<alpha>n_map2_\<alpha>nl[symmetric] ileq_map intro: \<alpha>ah_ileq del: predicate2I)
3.78 + moreover have "\<alpha>ah (map (\<alpha>nl fg) ww2') \<le> \<alpha>ah (map (\<alpha>n fg) w2)" using REVSPLIT(2) R_CONV(2) by (auto simp add: \<alpha>n_map2_\<alpha>nl[symmetric] le_list_map intro: \<alpha>ah_ileq del: predicate2I)
3.79 ultimately show ?thesis using goal1 REVSPLIT(1) by (blast intro: order_trans)
3.80 qed
3.81 from S_ENTRY_PAT[of "{#q'#}", simplified] RU(1) have S_ENTRY: "(v, mon_w fg w, {#q'#}) \<in> S_cs fg 1" by simp
4.1 --- a/thys/Program-Conflict-Analysis/Interleave.thy Mon Nov 02 18:43:26 2009 +0100
4.2 +++ b/thys/Program-Conflict-Analysis/Interleave.thy Wed Nov 04 09:19:37 2009 +0100
4.3 @@ -303,8 +303,8 @@
4.4 subsubsection "Relation to sublist order"
4.5
4.6 lemma ileq_interleave_alt: "l'\<preceq>l == \<exists>lb. l\<in>lb \<otimes> l'" proof (rule eq_reflection)
4.7 - {fix l' l have "l'\<preceq>l \<Longrightarrow> \<exists>lb. l\<in>lb \<otimes> l'" by (induct rule: ileq_induct) (simp, (blast intro: interleave_cons)+)}
4.8 - moreover {fix l have "!!lb l'. l\<in>lb\<otimes>l' \<Longrightarrow> l'\<preceq>l" by (induct l) (auto intro: ileq_intros elim!: cons_interleave_cases)}
4.9 + {fix l' l have "l'\<preceq>l \<Longrightarrow> \<exists>lb. l\<in>lb \<otimes> l'" by (induct rule: less_eq_list.induct) (simp, (blast intro: interleave_cons)+)}
4.10 + moreover {fix l have "!!lb l'. l\<in>lb\<otimes>l' \<Longrightarrow> l'\<preceq>l" by (induct l) (auto intro: less_eq_list.drop elim!: cons_interleave_cases)}
4.11 ultimately show "(l'\<preceq>l) = (\<exists>lb. l\<in>lb \<otimes> l')" by blast
4.12 qed
4.13
5.1 --- a/thys/Program-Conflict-Analysis/Normalization.thy Mon Nov 02 18:43:26 2009 +0100
5.2 +++ b/thys/Program-Conflict-Analysis/Normalization.thy Wed Nov 04 09:19:37 2009 +0100
5.3 @@ -439,7 +439,7 @@
5.4 done
5.5
5.6 lemma mon_ww_ileq: "w\<preceq>w' \<Longrightarrow> mon_ww fg w \<subseteq> mon_ww fg w'"
5.7 - by (induct rule: ileq_induct) auto
5.8 + by (induct rule: less_eq_list.induct) auto
5.9
5.10 (* TODO: Find some general statement about the property that monitors are computed element-wise and pslit this lemma and move the essential part to ConsInterleave.thy. Maybe the essential part is cil_set ?*)
5.11 lemma mon_ww_cil:
5.12 @@ -457,9 +457,9 @@
5.13 by (induct w) (auto split: el_step.split)
5.14
5.15 lemma mon_env_ileq: "w\<preceq>w' \<Longrightarrow> mon_env fg w \<subseteq> mon_env fg w'"
5.16 - by (induct rule: ileq_induct) auto
5.17 + by (induct rule: less_eq_list.induct) auto
5.18 lemma mon_loc_ileq: "w\<preceq>w' \<Longrightarrow> mon_loc fg w \<subseteq> mon_loc fg w'"
5.19 - by (induct rule: ileq_induct) auto
5.20 + by (induct rule: less_eq_list.induct) auto
5.21
5.22 lemma mon_loc_map_loc[simp]: "mon_loc fg (map LOC w) = mon_ww fg w"
5.23 by (unfold mon_loc_def) simp
5.24 @@ -1015,9 +1015,9 @@
5.25 from ntrp_mon_env_w_no_ctx[OF SPLIT(2), unfolded mon_env_def] have "mon_ww fg (map le_rem_s (env w)) \<inter> mon_s fg sh = {}" .
5.26 moreover have "mon_ww fg w2 \<subseteq> mon_ww fg (map le_rem_s (env w))" proof - (* TODO: This proof should be shorter and more straightforward *)
5.27 from cil_subset_il IHAPP(1) ileq_interleave have "map ENV w2 \<preceq> w" by blast
5.28 - from ileq_filter[OF this] have "env (map ENV w2) \<preceq> env w" by (unfold env_def) blast
5.29 + from le_list_filter[OF this] have "env (map ENV w2) \<preceq> env w" by (unfold env_def) blast
5.30 hence "map ENV w2 \<preceq> env w" by (unfold env_def) simp
5.31 - from ileq_map[OF this, of le_rem_s] have "w2 \<preceq> map le_rem_s (env w)" by simp
5.32 + from le_list_map[OF this, of le_rem_s] have "w2 \<preceq> map le_rem_s (env w)" by simp
5.33 thus ?thesis by (rule mon_ww_ileq)
5.34 qed
5.35 ultimately have "mon_ww fg w2 \<inter> mon_s fg sh = {}" by blast
6.1 --- a/thys/Program-Conflict-Analysis/Semantics.thy Mon Nov 02 18:43:26 2009 +0100
6.2 +++ b/thys/Program-Conflict-Analysis/Semantics.thy Wed Nov 04 09:19:37 2009 +0100
6.3 @@ -114,7 +114,7 @@
6.4 lemma mon_w_uncons[simp]: "mon_w fg (e#w) = mon_e fg e \<union> mon_w fg w"
6.5 by (rule mon_w_unconc[where wa="[e]", simplified])
6.6 lemma mon_w_ileq: "w\<preceq>w' \<Longrightarrow> mon_w fg w \<subseteq> mon_w fg w'"
6.7 - by (induct rule: ileq_induct) auto
6.8 + by (induct rule: less_eq_list.induct) auto
6.9
6.10
6.11