--- a/src/HOL/HOLCF/IOA/CompoTraces.thy Tue Jan 12 20:05:53 2016 +0100
+++ b/src/HOL/HOLCF/IOA/CompoTraces.thy Tue Jan 12 23:40:33 2016 +0100
@@ -8,58 +8,47 @@
imports CompoScheds ShortExecutions
begin
-definition mksch :: "('a,'s)ioa => ('a,'t)ioa => 'a Seq -> 'a Seq -> 'a Seq -> 'a Seq"
-where
- "mksch A B = (fix$(LAM h tr schA schB. case tr of
- nil => nil
- | x##xs =>
- (case x of
- UU => UU
- | Def y =>
- (if y:act A then
- (if y:act B then
- ((Takewhile (%a. a:int A)$schA)
- @@ (Takewhile (%a. a:int B)$schB)
- @@ (y\<leadsto>(h$xs
- $(TL$(Dropwhile (%a. a:int A)$schA))
- $(TL$(Dropwhile (%a. a:int B)$schB))
- )))
- else
- ((Takewhile (%a. a:int A)$schA)
- @@ (y\<leadsto>(h$xs
- $(TL$(Dropwhile (%a. a:int A)$schA))
- $schB)))
- )
- else
- (if y:act B then
- ((Takewhile (%a. a:int B)$schB)
- @@ (y\<leadsto>(h$xs
- $schA
- $(TL$(Dropwhile (%a. a:int B)$schB))
- )))
- else
- UU
- )
- )
- )))"
+definition mksch ::
+ "('a, 's) ioa \<Rightarrow> ('a, 't) ioa \<Rightarrow> 'a Seq \<rightarrow> 'a Seq \<rightarrow> 'a Seq \<rightarrow> 'a Seq"
+ where "mksch A B =
+ (fix $
+ (LAM h tr schA schB.
+ case tr of
+ nil \<Rightarrow> nil
+ | x ## xs \<Rightarrow>
+ (case x of
+ UU \<Rightarrow> UU
+ | Def y \<Rightarrow>
+ (if y \<in> act A then
+ (if y \<in> act B then
+ ((Takewhile (\<lambda>a. a \<in> int A) $ schA) @@
+ (Takewhile (\<lambda>a. a \<in> int B) $ schB) @@
+ (y \<leadsto> (h $ xs $ (TL $ (Dropwhile (\<lambda>a. a \<in> int A) $ schA))
+ $ (TL $ (Dropwhile (\<lambda>a. a \<in> int B) $ schB)))))
+ else
+ ((Takewhile (\<lambda>a. a \<in> int A) $ schA) @@
+ (y \<leadsto> (h $ xs $ (TL $ (Dropwhile (\<lambda>a. a \<in> int A) $ schA)) $ schB))))
+ else
+ (if y \<in> act B then
+ ((Takewhile (\<lambda>a. a \<in> int B) $ schB) @@
+ (y \<leadsto> (h $ xs $ schA $ (TL $ (Dropwhile (\<lambda>a. a \<in> int B) $ schB)))))
+ else UU)))))"
-definition par_traces ::"['a trace_module,'a trace_module] => 'a trace_module"
-where
- "par_traces TracesA TracesB =
- (let trA = fst TracesA; sigA = snd TracesA;
- trB = fst TracesB; sigB = snd TracesB
- in
- ( {tr. Filter (%a. a:actions sigA)$tr : trA}
- Int {tr. Filter (%a. a:actions sigB)$tr : trB}
- Int {tr. Forall (%x. x:(externals sigA Un externals sigB)) tr},
+definition par_traces :: "'a trace_module \<Rightarrow> 'a trace_module \<Rightarrow> 'a trace_module"
+ where "par_traces TracesA TracesB =
+ (let
+ trA = fst TracesA; sigA = snd TracesA;
+ trB = fst TracesB; sigB = snd TracesB
+ in
+ ({tr. Filter (\<lambda>a. a \<in> actions sigA) $ tr \<in> trA} \<inter>
+ {tr. Filter (\<lambda>a. a \<in> actions sigB) $ tr \<in> trB} \<inter>
+ {tr. Forall (\<lambda>x. x \<in> externals sigA \<union> externals sigB) tr},
asig_comp sigA sigB))"
-axiomatization
-where
- finiteR_mksch:
- "Finite (mksch A B$tr$x$y) \<Longrightarrow> Finite tr"
+axiomatization where
+ finiteR_mksch: "Finite (mksch A B $ tr $ x $ y) \<Longrightarrow> Finite tr"
-lemma finiteR_mksch': "\<not> Finite tr \<Longrightarrow> \<not> Finite (mksch A B$tr$x$y)"
+lemma finiteR_mksch': "\<not> Finite tr \<Longrightarrow> \<not> Finite (mksch A B $ tr $ x $ y)"
by (blast intro: finiteR_mksch)
@@ -69,89 +58,79 @@
subsection "mksch rewrite rules"
lemma mksch_unfold:
-"mksch A B = (LAM tr schA schB. case tr of
- nil => nil
- | x##xs =>
- (case x of
- UU => UU
- | Def y =>
- (if y:act A then
- (if y:act B then
- ((Takewhile (%a. a:int A)$schA)
- @@(Takewhile (%a. a:int B)$schB)
- @@(y\<leadsto>(mksch A B$xs
- $(TL$(Dropwhile (%a. a:int A)$schA))
- $(TL$(Dropwhile (%a. a:int B)$schB))
- )))
- else
- ((Takewhile (%a. a:int A)$schA)
- @@ (y\<leadsto>(mksch A B$xs
- $(TL$(Dropwhile (%a. a:int A)$schA))
- $schB)))
- )
- else
- (if y:act B then
- ((Takewhile (%a. a:int B)$schB)
- @@ (y\<leadsto>(mksch A B$xs
- $schA
- $(TL$(Dropwhile (%a. a:int B)$schB))
- )))
- else
- UU
- )
- )
- ))"
-apply (rule trans)
-apply (rule fix_eq4)
-apply (rule mksch_def)
-apply (rule beta_cfun)
-apply simp
-done
+ "mksch A B =
+ (LAM tr schA schB.
+ case tr of
+ nil \<Rightarrow> nil
+ | x ## xs \<Rightarrow>
+ (case x of
+ UU \<Rightarrow> UU
+ | Def y \<Rightarrow>
+ (if y \<in> act A then
+ (if y \<in> act B then
+ ((Takewhile (\<lambda>a. a \<in> int A) $ schA) @@
+ (Takewhile (\<lambda>a. a \<in> int B) $ schB) @@
+ (y \<leadsto> (mksch A B $ xs $(TL $ (Dropwhile (\<lambda>a. a \<in> int A) $ schA))
+ $(TL $ (Dropwhile (\<lambda>a. a \<in> int B) $ schB)))))
+ else
+ ((Takewhile (\<lambda>a. a \<in> int A) $ schA) @@
+ (y \<leadsto> (mksch A B $ xs $ (TL $ (Dropwhile (\<lambda>a. a \<in> int A) $ schA)) $ schB))))
+ else
+ (if y \<in> act B then
+ ((Takewhile (\<lambda>a. a \<in> int B) $ schB) @@
+ (y \<leadsto> (mksch A B $ xs $ schA $ (TL $ (Dropwhile (\<lambda>a. a \<in> int B) $ schB)))))
+ else UU))))"
+ apply (rule trans)
+ apply (rule fix_eq4)
+ apply (rule mksch_def)
+ apply (rule beta_cfun)
+ apply simp
+ done
+
+lemma mksch_UU: "mksch A B $ UU $ schA $ schB = UU"
+ apply (subst mksch_unfold)
+ apply simp
+ done
-lemma mksch_UU: "mksch A B$UU$schA$schB = UU"
-apply (subst mksch_unfold)
-apply simp
-done
-
-lemma mksch_nil: "mksch A B$nil$schA$schB = nil"
-apply (subst mksch_unfold)
-apply simp
-done
+lemma mksch_nil: "mksch A B $ nil $ schA $ schB = nil"
+ apply (subst mksch_unfold)
+ apply simp
+ done
-lemma mksch_cons1: "[|x:act A;x~:act B|]
- ==> mksch A B$(x\<leadsto>tr)$schA$schB =
- (Takewhile (%a. a:int A)$schA)
- @@ (x\<leadsto>(mksch A B$tr$(TL$(Dropwhile (%a. a:int A)$schA))
- $schB))"
-apply (rule trans)
-apply (subst mksch_unfold)
-apply (simp add: Consq_def If_and_if)
-apply (simp add: Consq_def)
-done
+lemma mksch_cons1:
+ "x \<in> act A \<Longrightarrow> x \<notin> act B \<Longrightarrow>
+ mksch A B $ (x \<leadsto> tr) $ schA $ schB =
+ (Takewhile (\<lambda>a. a \<in> int A) $ schA) @@
+ (x \<leadsto> (mksch A B $ tr $ (TL $ (Dropwhile (\<lambda>a. a \<in> int A) $ schA)) $ schB))"
+ apply (rule trans)
+ apply (subst mksch_unfold)
+ apply (simp add: Consq_def If_and_if)
+ apply (simp add: Consq_def)
+ done
-lemma mksch_cons2: "[|x~:act A;x:act B|]
- ==> mksch A B$(x\<leadsto>tr)$schA$schB =
- (Takewhile (%a. a:int B)$schB)
- @@ (x\<leadsto>(mksch A B$tr$schA$(TL$(Dropwhile (%a. a:int B)$schB))
- ))"
-apply (rule trans)
-apply (subst mksch_unfold)
-apply (simp add: Consq_def If_and_if)
-apply (simp add: Consq_def)
-done
+lemma mksch_cons2:
+ "x \<notin> act A \<Longrightarrow> x \<in> act B \<Longrightarrow>
+ mksch A B $ (x \<leadsto> tr) $ schA $ schB =
+ (Takewhile (\<lambda>a. a \<in> int B) $ schB) @@
+ (x \<leadsto> (mksch A B $ tr $ schA $ (TL $ (Dropwhile (\<lambda>a. a \<in> int B) $ schB))))"
+ apply (rule trans)
+ apply (subst mksch_unfold)
+ apply (simp add: Consq_def If_and_if)
+ apply (simp add: Consq_def)
+ done
-lemma mksch_cons3: "[|x:act A;x:act B|]
- ==> mksch A B$(x\<leadsto>tr)$schA$schB =
- (Takewhile (%a. a:int A)$schA)
- @@ ((Takewhile (%a. a:int B)$schB)
- @@ (x\<leadsto>(mksch A B$tr$(TL$(Dropwhile (%a. a:int A)$schA))
- $(TL$(Dropwhile (%a. a:int B)$schB))))
- )"
-apply (rule trans)
-apply (subst mksch_unfold)
-apply (simp add: Consq_def If_and_if)
-apply (simp add: Consq_def)
-done
+lemma mksch_cons3:
+ "x \<in> act A \<Longrightarrow> x \<in> act B \<Longrightarrow>
+ mksch A B $ (x \<leadsto> tr) $ schA $ schB =
+ (Takewhile (\<lambda>a. a \<in> int A) $ schA) @@
+ ((Takewhile (\<lambda>a. a \<in> int B) $ schB) @@
+ (x \<leadsto> (mksch A B $ tr $ (TL $ (Dropwhile (\<lambda>a. a \<in> int A) $ schA))
+ $ (TL $ (Dropwhile (\<lambda>a. a \<in> int B) $ schB)))))"
+ apply (rule trans)
+ apply (subst mksch_unfold)
+ apply (simp add: Consq_def If_and_if)
+ apply (simp add: Consq_def)
+ done
lemmas compotr_simps = mksch_UU mksch_nil mksch_cons1 mksch_cons2 mksch_cons3
@@ -160,810 +139,802 @@
subsection \<open>COMPOSITIONALITY on TRACE Level\<close>
-subsubsection "Lemmata for ==>"
+subsubsection "Lemmata for \<open>\<Longrightarrow>\<close>"
-(* Consequence out of ext1_ext2_is_not_act1(2), which in turn are consequences out of
- the compatibility of IOA, in particular out of the condition that internals are
- really hidden. *)
+text \<open>
+ Consequence out of \<open>ext1_ext2_is_not_act1(2)\<close>, which in turn are
+ consequences out of the compatibility of IOA, in particular out of the
+ condition that internals are really hidden.
+\<close>
-lemma compatibility_consequence1: "(eB & ~eA --> ~A) -->
- (A & (eA | eB)) = (eA & A)"
-apply fast
-done
+lemma compatibility_consequence1: "(eB \<and> \<not> eA \<longrightarrow> \<not> A) \<longrightarrow> A \<and> (eA \<or> eB) \<longleftrightarrow> eA \<and> A"
+ by fast
(* very similar to above, only the commutativity of | is used to make a slight change *)
-
-lemma compatibility_consequence2: "(eB & ~eA --> ~A) -->
- (A & (eB | eA)) = (eA & A)"
-apply fast
-done
+lemma compatibility_consequence2: "(eB \<and> \<not> eA \<longrightarrow> \<not> A) \<longrightarrow> A \<and> (eB \<or> eA) \<longleftrightarrow> eA \<and> A"
+ by fast
-subsubsection "Lemmata for <=="
+subsubsection \<open>Lemmata for \<open>\<Longleftarrow>\<close>\<close>
(* Lemma for substitution of looping assumption in another specific assumption *)
-lemma subst_lemma1: "[| f << (g x) ; x=(h x) |] ==> f << g (h x)"
-by (erule subst)
+lemma subst_lemma1: "f \<sqsubseteq> g x \<Longrightarrow> x = h x \<Longrightarrow> f \<sqsubseteq> g (h x)"
+ by (erule subst)
(* Lemma for substitution of looping assumption in another specific assumption *)
-lemma subst_lemma2: "[| (f x) = y \<leadsto> g; x=(h x) |] ==> (f (h x)) = y \<leadsto> g"
-by (erule subst)
+lemma subst_lemma2: "(f x) = y \<leadsto> g \<Longrightarrow> x = h x \<Longrightarrow> f (h x) = y \<leadsto> g"
+ by (erule subst)
lemma ForallAorB_mksch [rule_format]:
- "!!A B. compatible A B ==>
- ! schA schB. Forall (%x. x:act (A\<parallel>B)) tr
- --> Forall (%x. x:act (A\<parallel>B)) (mksch A B$tr$schA$schB)"
-apply (tactic \<open>Seq_induct_tac @{context} "tr"
- [@{thm Forall_def}, @{thm sforall_def}, @{thm mksch_def}] 1\<close>)
-apply auto
-apply (simp add: actions_of_par)
-apply (case_tac "a:act A")
-apply (case_tac "a:act B")
-(* a:A, a:B *)
-apply simp
-apply (rule Forall_Conc_impl [THEN mp])
-apply (simp add: intA_is_not_actB int_is_act)
-apply (rule Forall_Conc_impl [THEN mp])
-apply (simp add: intA_is_not_actB int_is_act)
-(* a:A,a~:B *)
-apply simp
-apply (rule Forall_Conc_impl [THEN mp])
-apply (simp add: intA_is_not_actB int_is_act)
-apply (case_tac "a:act B")
-(* a~:A, a:B *)
-apply simp
-apply (rule Forall_Conc_impl [THEN mp])
-apply (simp add: intA_is_not_actB int_is_act)
-(* a~:A,a~:B *)
-apply auto
-done
+ "compatible A B \<Longrightarrow>
+ \<forall>schA schB. Forall (\<lambda>x. x \<in> act (A \<parallel> B)) tr \<longrightarrow>
+ Forall (\<lambda>x. x \<in> act (A \<parallel> B)) (mksch A B $ tr $ schA $ schB)"
+ apply (tactic \<open>Seq_induct_tac @{context} "tr" @{thms Forall_def sforall_def mksch_def} 1\<close>)
+ apply auto
+ apply (simp add: actions_of_par)
+ apply (case_tac "a \<in> act A")
+ apply (case_tac "a \<in> act B")
+ text \<open>\<open>a \<in> A\<close>, \<open>a \<in> B\<close>\<close>
+ apply simp
+ apply (rule Forall_Conc_impl [THEN mp])
+ apply (simp add: intA_is_not_actB int_is_act)
+ apply (rule Forall_Conc_impl [THEN mp])
+ apply (simp add: intA_is_not_actB int_is_act)
+ text \<open>\<open>a \<in> A\<close>, \<open>a \<notin> B\<close>\<close>
+ apply simp
+ apply (rule Forall_Conc_impl [THEN mp])
+ apply (simp add: intA_is_not_actB int_is_act)
+ apply (case_tac "a:act B")
+ text \<open>\<open>a \<notin> A\<close>, \<open>a \<in> B\<close>\<close>
+ apply simp
+ apply (rule Forall_Conc_impl [THEN mp])
+ apply (simp add: intA_is_not_actB int_is_act)
+ text \<open>\<open>a \<notin> A\<close>, \<open>a \<notin> B\<close>\<close>
+ apply auto
+ done
-lemma ForallBnAmksch [rule_format (no_asm)]: "!!A B. compatible B A ==>
- ! schA schB. (Forall (%x. x:act B & x~:act A) tr
- --> Forall (%x. x:act B & x~:act A) (mksch A B$tr$schA$schB))"
-apply (tactic \<open>Seq_induct_tac @{context} "tr"
- [@{thm Forall_def}, @{thm sforall_def}, @{thm mksch_def}] 1\<close>)
-apply auto
-apply (rule Forall_Conc_impl [THEN mp])
-apply (simp add: intA_is_not_actB int_is_act)
-done
+lemma ForallBnAmksch [rule_format]:
+ "compatible B A \<Longrightarrow>
+ \<forall>schA schB. Forall (\<lambda>x. x \<in> act B \<and> x \<notin> act A) tr \<longrightarrow>
+ Forall (\<lambda>x. x \<in> act B \<and> x \<notin> act A) (mksch A B $ tr $ schA $ schB)"
+ apply (tactic \<open>Seq_induct_tac @{context} "tr" @{thms Forall_def sforall_def mksch_def} 1\<close>)
+ apply auto
+ apply (rule Forall_Conc_impl [THEN mp])
+ apply (simp add: intA_is_not_actB int_is_act)
+ done
-lemma ForallAnBmksch [rule_format (no_asm)]: "!!A B. compatible A B ==>
- ! schA schB. (Forall (%x. x:act A & x~:act B) tr
- --> Forall (%x. x:act A & x~:act B) (mksch A B$tr$schA$schB))"
-apply (tactic \<open>Seq_induct_tac @{context} "tr"
- [@{thm Forall_def}, @{thm sforall_def}, @{thm mksch_def}] 1\<close>)
-apply auto
-apply (rule Forall_Conc_impl [THEN mp])
-apply (simp add: intA_is_not_actB int_is_act)
-done
+lemma ForallAnBmksch [rule_format]:
+ "compatible A B \<Longrightarrow>
+ \<forall>schA schB. Forall (\<lambda>x. x \<in> act A \<and> x \<notin> act B) tr \<longrightarrow>
+ Forall (\<lambda>x. x \<in> act A \<and> x \<notin> act B) (mksch A B $ tr $ schA $ schB)"
+ apply (tactic \<open>Seq_induct_tac @{context} "tr" @{thms Forall_def sforall_def mksch_def} 1\<close>)
+ apply auto
+ apply (rule Forall_Conc_impl [THEN mp])
+ apply (simp add: intA_is_not_actB int_is_act)
+ done
-(* safe-tac makes too many case distinctions with this lemma in the next proof *)
+(* safe_tac makes too many case distinctions with this lemma in the next proof *)
declare FiniteConc [simp del]
-lemma FiniteL_mksch [rule_format (no_asm)]: "[| Finite tr; is_asig(asig_of A); is_asig(asig_of B) |] ==>
- ! x y. Forall (%x. x:act A) x & Forall (%x. x:act B) y &
- Filter (%a. a:ext A)$x = Filter (%a. a:act A)$tr &
- Filter (%a. a:ext B)$y = Filter (%a. a:act B)$tr &
- Forall (%x. x:ext (A\<parallel>B)) tr
- --> Finite (mksch A B$tr$x$y)"
-
-apply (erule Seq_Finite_ind)
-apply simp
-(* main case *)
-apply simp
-apply auto
+lemma FiniteL_mksch [rule_format]:
+ "Finite tr \<Longrightarrow> is_asig (asig_of A) \<Longrightarrow> is_asig (asig_of B) \<Longrightarrow>
+ \<forall>x y.
+ Forall (\<lambda>x. x \<in> act A) x \<and> Forall (\<lambda>x. x \<in> act B) y \<and>
+ Filter (\<lambda>a. a \<in> ext A) $ x = Filter (\<lambda>a. a \<in> act A) $ tr \<and>
+ Filter (\<lambda>a. a \<in> ext B) $ y = Filter (\<lambda>a. a \<in> act B) $ tr \<and>
+ Forall (\<lambda>x. x \<in> ext (A \<parallel> B)) tr \<longrightarrow> Finite (mksch A B $ tr $ x $ y)"
+ apply (erule Seq_Finite_ind)
+ apply simp
+ text \<open>main case\<close>
+ apply simp
+ apply auto
-(* a: act A; a: act B *)
-apply (frule sym [THEN eq_imp_below, THEN divide_Seq])
-apply (frule sym [THEN eq_imp_below, THEN divide_Seq])
-back
-apply (erule conjE)+
-(* Finite (tw iA x) and Finite (tw iB y) *)
-apply (simp add: not_ext_is_int_or_not_act FiniteConc)
-(* now for conclusion IH applicable, but assumptions have to be transformed *)
-apply (drule_tac x = "x" and g = "Filter (%a. a:act A) $s" in subst_lemma2)
-apply assumption
-apply (drule_tac x = "y" and g = "Filter (%a. a:act B) $s" in subst_lemma2)
-apply assumption
-(* IH *)
-apply (simp add: not_ext_is_int_or_not_act ForallTL ForallDropwhile)
+ text \<open>\<open>a \<in> act A\<close>; \<open>a \<in> act B\<close>\<close>
+ apply (frule sym [THEN eq_imp_below, THEN divide_Seq])
+ apply (frule sym [THEN eq_imp_below, THEN divide_Seq])
+ back
+ apply (erule conjE)+
+ text \<open>\<open>Finite (tw iA x)\<close> and \<open>Finite (tw iB y)\<close>\<close>
+ apply (simp add: not_ext_is_int_or_not_act FiniteConc)
+ text \<open>now for conclusion IH applicable, but assumptions have to be transformed\<close>
+ apply (drule_tac x = "x" and g = "Filter (\<lambda>a. a \<in> act A) $ s" in subst_lemma2)
+ apply assumption
+ apply (drule_tac x = "y" and g = "Filter (\<lambda>a. a \<in> act B) $ s" in subst_lemma2)
+ apply assumption
+ text \<open>IH\<close>
+ apply (simp add: not_ext_is_int_or_not_act ForallTL ForallDropwhile)
-(* a: act B; a~: act A *)
-apply (frule sym [THEN eq_imp_below, THEN divide_Seq])
+ text \<open>\<open>a \<in> act B\<close>; \<open>a \<notin> act A\<close>\<close>
+ apply (frule sym [THEN eq_imp_below, THEN divide_Seq])
-apply (erule conjE)+
-(* Finite (tw iB y) *)
-apply (simp add: not_ext_is_int_or_not_act FiniteConc)
-(* now for conclusion IH applicable, but assumptions have to be transformed *)
-apply (drule_tac x = "y" and g = "Filter (%a. a:act B) $s" in subst_lemma2)
-apply assumption
-(* IH *)
-apply (simp add: not_ext_is_int_or_not_act ForallTL ForallDropwhile)
+ apply (erule conjE)+
+ text \<open>\<open>Finite (tw iB y)\<close>\<close>
+ apply (simp add: not_ext_is_int_or_not_act FiniteConc)
+ text \<open>now for conclusion IH applicable, but assumptions have to be transformed\<close>
+ apply (drule_tac x = "y" and g = "Filter (\<lambda>a. a \<in> act B) $ s" in subst_lemma2)
+ apply assumption
+ text \<open>IH\<close>
+ apply (simp add: not_ext_is_int_or_not_act ForallTL ForallDropwhile)
-(* a~: act B; a: act A *)
-apply (frule sym [THEN eq_imp_below, THEN divide_Seq])
+ text \<open>\<open>a \<notin> act B\<close>; \<open>a \<in> act A\<close>\<close>
+ apply (frule sym [THEN eq_imp_below, THEN divide_Seq])
-apply (erule conjE)+
-(* Finite (tw iA x) *)
-apply (simp add: not_ext_is_int_or_not_act FiniteConc)
-(* now for conclusion IH applicable, but assumptions have to be transformed *)
-apply (drule_tac x = "x" and g = "Filter (%a. a:act A) $s" in subst_lemma2)
-apply assumption
-(* IH *)
-apply (simp add: not_ext_is_int_or_not_act ForallTL ForallDropwhile)
+ apply (erule conjE)+
+ text \<open>\<open>Finite (tw iA x)\<close>\<close>
+ apply (simp add: not_ext_is_int_or_not_act FiniteConc)
+ text \<open>now for conclusion IH applicable, but assumptions have to be transformed\<close>
+ apply (drule_tac x = "x" and g = "Filter (\<lambda>a. a \<in> act A) $ s" in subst_lemma2)
+ apply assumption
+ text \<open>IH\<close>
+ apply (simp add: not_ext_is_int_or_not_act ForallTL ForallDropwhile)
-(* a~: act B; a~: act A *)
-apply (fastforce intro!: ext_is_act simp: externals_of_par)
-done
+ text \<open>\<open>a \<notin> act B\<close>; \<open>a \<notin> act A\<close>\<close>
+ apply (fastforce intro!: ext_is_act simp: externals_of_par)
+ done
declare FiniteConc [simp]
declare FilterConc [simp del]
-lemma reduceA_mksch1 [rule_format (no_asm)]: " [| Finite bs; is_asig(asig_of A); is_asig(asig_of B);compatible A B|] ==>
- ! y. Forall (%x. x:act B) y & Forall (%x. x:act B & x~:act A) bs &
- Filter (%a. a:ext B)$y = Filter (%a. a:act B)$(bs @@ z)
- --> (? y1 y2. (mksch A B$(bs @@ z)$x$y) = (y1 @@ (mksch A B$z$x$y2)) &
- Forall (%x. x:act B & x~:act A) y1 &
- Finite y1 & y = (y1 @@ y2) &
- Filter (%a. a:ext B)$y1 = bs)"
-apply (frule_tac A1 = "A" in compat_commute [THEN iffD1])
-apply (erule Seq_Finite_ind)
-apply (rule allI)+
-apply (rule impI)
-apply (rule_tac x = "nil" in exI)
-apply (rule_tac x = "y" in exI)
-apply simp
-(* main case *)
-apply (rule allI)+
-apply (rule impI)
-apply simp
-apply (erule conjE)+
-apply simp
-(* divide_Seq on s *)
-apply (frule sym [THEN eq_imp_below, THEN divide_Seq])
-apply (erule conjE)+
-(* transform assumption f eB y = f B (s@z) *)
-apply (drule_tac x = "y" and g = "Filter (%a. a:act B) $ (s@@z) " in subst_lemma2)
-apply assumption
-apply (simp add: not_ext_is_int_or_not_act FilterConc)
-(* apply IH *)
-apply (erule_tac x = "TL$ (Dropwhile (%a. a:int B) $y) " in allE)
-apply (simp add: ForallTL ForallDropwhile FilterConc)
-apply (erule exE)+
-apply (erule conjE)+
-apply (simp add: FilterConc)
-(* for replacing IH in conclusion *)
-apply (rotate_tac -2)
-(* instantiate y1a and y2a *)
-apply (rule_tac x = "Takewhile (%a. a:int B) $y @@ a\<leadsto>y1" in exI)
-apply (rule_tac x = "y2" in exI)
-(* elminate all obligations up to two depending on Conc_assoc *)
-apply (simp add: intA_is_not_actB int_is_act int_is_not_ext FilterConc)
-apply (simp (no_asm) add: Conc_assoc FilterConc)
-done
+lemma reduceA_mksch1 [rule_format]:
+ "Finite bs \<Longrightarrow> is_asig (asig_of A) \<Longrightarrow> is_asig (asig_of B) \<Longrightarrow> compatible A B \<Longrightarrow>
+ \<forall>y. Forall (\<lambda>x. x \<in> act B) y \<and> Forall (\<lambda>x. x \<in> act B \<and> x \<notin> act A) bs \<and>
+ Filter (\<lambda>a. a \<in> ext B) $ y = Filter (\<lambda>a. a \<in> act B) $ (bs @@ z) \<longrightarrow>
+ (\<exists>y1 y2.
+ (mksch A B $ (bs @@ z) $ x $ y) = (y1 @@ (mksch A B $ z $ x $ y2)) \<and>
+ Forall (\<lambda>x. x \<in> act B \<and> x \<notin> act A) y1 \<and>
+ Finite y1 \<and> y = (y1 @@ y2) \<and>
+ Filter (\<lambda>a. a \<in> ext B) $ y1 = bs)"
+ apply (frule_tac A1 = "A" in compat_commute [THEN iffD1])
+ apply (erule Seq_Finite_ind)
+ apply (rule allI)+
+ apply (rule impI)
+ apply (rule_tac x = "nil" in exI)
+ apply (rule_tac x = "y" in exI)
+ apply simp
+ text \<open>main case\<close>
+ apply (rule allI)+
+ apply (rule impI)
+ apply simp
+ apply (erule conjE)+
+ apply simp
+ text \<open>\<open>divide_Seq\<close> on \<open>s\<close>\<close>
+ apply (frule sym [THEN eq_imp_below, THEN divide_Seq])
+ apply (erule conjE)+
+ text \<open>transform assumption \<open>f eB y = f B (s @ z)\<close>\<close>
+ apply (drule_tac x = "y" and g = "Filter (\<lambda>a. a \<in> act B) $ (s @@ z) " in subst_lemma2)
+ apply assumption
+ apply (simp add: not_ext_is_int_or_not_act FilterConc)
+ text \<open>apply IH\<close>
+ apply (erule_tac x = "TL $ (Dropwhile (\<lambda>a. a \<in> int B) $ y)" in allE)
+ apply (simp add: ForallTL ForallDropwhile FilterConc)
+ apply (erule exE)+
+ apply (erule conjE)+
+ apply (simp add: FilterConc)
+ text \<open>for replacing IH in conclusion\<close>
+ apply (rotate_tac -2)
+ text \<open>instantiate \<open>y1a\<close> and \<open>y2a\<close>\<close>
+ apply (rule_tac x = "Takewhile (\<lambda>a. a \<in> int B) $ y @@ a \<leadsto> y1" in exI)
+ apply (rule_tac x = "y2" in exI)
+ text \<open>elminate all obligations up to two depending on \<open>Conc_assoc\<close>\<close>
+ apply (simp add: intA_is_not_actB int_is_act int_is_not_ext FilterConc)
+ apply (simp add: Conc_assoc FilterConc)
+ done
lemmas reduceA_mksch = conjI [THEN [6] conjI [THEN [5] reduceA_mksch1]]
lemma reduceB_mksch1 [rule_format]:
-" [| Finite a_s; is_asig(asig_of A); is_asig(asig_of B);compatible A B|] ==>
- ! x. Forall (%x. x:act A) x & Forall (%x. x:act A & x~:act B) a_s &
- Filter (%a. a:ext A)$x = Filter (%a. a:act A)$(a_s @@ z)
- --> (? x1 x2. (mksch A B$(a_s @@ z)$x$y) = (x1 @@ (mksch A B$z$x2$y)) &
- Forall (%x. x:act A & x~:act B) x1 &
- Finite x1 & x = (x1 @@ x2) &
- Filter (%a. a:ext A)$x1 = a_s)"
-apply (frule_tac A1 = "A" in compat_commute [THEN iffD1])
-apply (erule Seq_Finite_ind)
-apply (rule allI)+
-apply (rule impI)
-apply (rule_tac x = "nil" in exI)
-apply (rule_tac x = "x" in exI)
-apply simp
-(* main case *)
-apply (rule allI)+
-apply (rule impI)
-apply simp
-apply (erule conjE)+
-apply simp
-(* divide_Seq on s *)
-apply (frule sym [THEN eq_imp_below, THEN divide_Seq])
-apply (erule conjE)+
-(* transform assumption f eA x = f A (s@z) *)
-apply (drule_tac x = "x" and g = "Filter (%a. a:act A) $ (s@@z) " in subst_lemma2)
-apply assumption
-apply (simp add: not_ext_is_int_or_not_act FilterConc)
-(* apply IH *)
-apply (erule_tac x = "TL$ (Dropwhile (%a. a:int A) $x) " in allE)
-apply (simp add: ForallTL ForallDropwhile FilterConc)
-apply (erule exE)+
-apply (erule conjE)+
-apply (simp add: FilterConc)
-(* for replacing IH in conclusion *)
-apply (rotate_tac -2)
-(* instantiate y1a and y2a *)
-apply (rule_tac x = "Takewhile (%a. a:int A) $x @@ a\<leadsto>x1" in exI)
-apply (rule_tac x = "x2" in exI)
-(* elminate all obligations up to two depending on Conc_assoc *)
-apply (simp add: intA_is_not_actB int_is_act int_is_not_ext FilterConc)
-apply (simp (no_asm) add: Conc_assoc FilterConc)
-done
+ "Finite a_s \<Longrightarrow> is_asig (asig_of A) \<Longrightarrow> is_asig (asig_of B) \<Longrightarrow> compatible A B \<Longrightarrow>
+ \<forall>x. Forall (\<lambda>x. x \<in> act A) x \<and> Forall (\<lambda>x. x \<in> act A \<and> x \<notin> act B) a_s \<and>
+ Filter (\<lambda>a. a \<in> ext A) $ x = Filter (\<lambda>a. a \<in> act A) $ (a_s @@ z) \<longrightarrow>
+ (\<exists>x1 x2.
+ (mksch A B $ (a_s @@ z) $ x $ y) = (x1 @@ (mksch A B $ z $ x2 $ y)) \<and>
+ Forall (\<lambda>x. x \<in> act A \<and> x \<notin> act B) x1 \<and>
+ Finite x1 \<and> x = (x1 @@ x2) \<and>
+ Filter (\<lambda>a. a \<in> ext A) $ x1 = a_s)"
+ apply (frule_tac A1 = "A" in compat_commute [THEN iffD1])
+ apply (erule Seq_Finite_ind)
+ apply (rule allI)+
+ apply (rule impI)
+ apply (rule_tac x = "nil" in exI)
+ apply (rule_tac x = "x" in exI)
+ apply simp
+ text \<open>main case\<close>
+ apply (rule allI)+
+ apply (rule impI)
+ apply simp
+ apply (erule conjE)+
+ apply simp
+ text \<open>\<open>divide_Seq\<close> on \<open>s\<close>\<close>
+ apply (frule sym [THEN eq_imp_below, THEN divide_Seq])
+ apply (erule conjE)+
+ text \<open>transform assumption \<open>f eA x = f A (s @ z)\<close>\<close>
+ apply (drule_tac x = "x" and g = "Filter (\<lambda>a. a \<in> act A) $ (s @@ z)" in subst_lemma2)
+ apply assumption
+ apply (simp add: not_ext_is_int_or_not_act FilterConc)
+ text \<open>apply IH\<close>
+ apply (erule_tac x = "TL $ (Dropwhile (\<lambda>a. a \<in> int A) $ x)" in allE)
+ apply (simp add: ForallTL ForallDropwhile FilterConc)
+ apply (erule exE)+
+ apply (erule conjE)+
+ apply (simp add: FilterConc)
+ text \<open>for replacing IH in conclusion\<close>
+ apply (rotate_tac -2)
+ text \<open>instantiate \<open>y1a\<close> and \<open>y2a\<close>\<close>
+ apply (rule_tac x = "Takewhile (\<lambda>a. a \<in> int A) $ x @@ a \<leadsto> x1" in exI)
+ apply (rule_tac x = "x2" in exI)
+ text \<open>eliminate all obligations up to two depending on \<open>Conc_assoc\<close>\<close>
+ apply (simp add: intA_is_not_actB int_is_act int_is_not_ext FilterConc)
+ apply (simp add: Conc_assoc FilterConc)
+ done
lemmas reduceB_mksch = conjI [THEN [6] conjI [THEN [5] reduceB_mksch1]]
declare FilterConc [simp]
-subsection "Filtering external actions out of mksch(tr,schA,schB) yields the oracle tr"
+subsection \<open>Filtering external actions out of \<open>mksch (tr, schA, schB)\<close> yields the oracle \<open>tr\<close>\<close>
lemma FilterA_mksch_is_tr:
-"!! A B. [| compatible A B; compatible B A;
- is_asig(asig_of A); is_asig(asig_of B) |] ==>
- ! schA schB. Forall (%x. x:act A) schA & Forall (%x. x:act B) schB &
- Forall (%x. x:ext (A\<parallel>B)) tr &
- Filter (%a. a:act A)$tr << Filter (%a. a:ext A)$schA &
- Filter (%a. a:act B)$tr << Filter (%a. a:ext B)$schB
- --> Filter (%a. a:ext (A\<parallel>B))$(mksch A B$tr$schA$schB) = tr"
-
-apply (tactic \<open>Seq_induct_tac @{context} "tr"
- [@{thm Forall_def}, @{thm sforall_def}, @{thm mksch_def}] 1\<close>)
-(* main case *)
-(* splitting into 4 cases according to a:A, a:B *)
-apply auto
+ "compatible A B \<Longrightarrow> compatible B A \<Longrightarrow> is_asig (asig_of A) \<Longrightarrow> is_asig (asig_of B) \<Longrightarrow>
+ \<forall>schA schB.
+ Forall (\<lambda>x. x \<in> act A) schA \<and>
+ Forall (\<lambda>x. x \<in> act B) schB \<and>
+ Forall (\<lambda>x. x \<in> ext (A \<parallel> B)) tr \<and>
+ Filter (\<lambda>a. a \<in> act A) $ tr \<sqsubseteq> Filter (\<lambda>a. a \<in> ext A) $ schA \<and>
+ Filter (\<lambda>a. a \<in> act B) $ tr \<sqsubseteq> Filter (\<lambda>a. a \<in> ext B) $ schB
+ \<longrightarrow> Filter (\<lambda>a. a \<in> ext (A \<parallel> B)) $ (mksch A B $ tr $ schA $ schB) = tr"
+ apply (tactic \<open>Seq_induct_tac @{context} "tr" @{thms Forall_def sforall_def mksch_def} 1\<close>)
+ text \<open>main case\<close>
+ text \<open>splitting into 4 cases according to \<open>a \<in> A\<close>, \<open>a \<in> B\<close>\<close>
+ apply auto
-(* Case a:A, a:B *)
-apply (frule divide_Seq)
-apply (frule divide_Seq)
-back
-apply (erule conjE)+
-(* filtering internals of A in schA and of B in schB is nil *)
-apply (simp add: not_ext_is_int_or_not_act externals_of_par intA_is_not_extB int_is_not_ext)
-(* conclusion of IH ok, but assumptions of IH have to be transformed *)
-apply (drule_tac x = "schA" in subst_lemma1)
-apply assumption
-apply (drule_tac x = "schB" in subst_lemma1)
-apply assumption
-(* IH *)
-apply (simp add: not_ext_is_int_or_not_act ForallTL ForallDropwhile)
+ text \<open>Case \<open>a \<in> A\<close>, \<open>a \<in> B\<close>\<close>
+ apply (frule divide_Seq)
+ apply (frule divide_Seq)
+ back
+ apply (erule conjE)+
+ text \<open>filtering internals of \<open>A\<close> in \<open>schA\<close> and of \<open>B\<close> in \<open>schB\<close> is \<open>nil\<close>\<close>
+ apply (simp add: not_ext_is_int_or_not_act externals_of_par intA_is_not_extB int_is_not_ext)
+ text \<open>conclusion of IH ok, but assumptions of IH have to be transformed\<close>
+ apply (drule_tac x = "schA" in subst_lemma1)
+ apply assumption
+ apply (drule_tac x = "schB" in subst_lemma1)
+ apply assumption
+ text \<open>IH\<close>
+ apply (simp add: not_ext_is_int_or_not_act ForallTL ForallDropwhile)
-(* Case a:A, a~:B *)
-apply (frule divide_Seq)
-apply (erule conjE)+
-(* filtering internals of A is nil *)
-apply (simp add: not_ext_is_int_or_not_act externals_of_par intA_is_not_extB int_is_not_ext)
-apply (drule_tac x = "schA" in subst_lemma1)
-apply assumption
-apply (simp add: not_ext_is_int_or_not_act ForallTL ForallDropwhile)
+ text \<open>Case \<open>a \<in> A\<close>, \<open>a \<notin> B\<close>\<close>
+ apply (frule divide_Seq)
+ apply (erule conjE)+
+ text \<open>filtering internals of \<open>A\<close> is \<open>nil\<close>\<close>
+ apply (simp add: not_ext_is_int_or_not_act externals_of_par intA_is_not_extB int_is_not_ext)
+ apply (drule_tac x = "schA" in subst_lemma1)
+ apply assumption
+ apply (simp add: not_ext_is_int_or_not_act ForallTL ForallDropwhile)
-(* Case a:B, a~:A *)
-apply (frule divide_Seq)
-apply (erule conjE)+
-(* filtering internals of A is nil *)
-apply (simp add: not_ext_is_int_or_not_act externals_of_par intA_is_not_extB int_is_not_ext)
-apply (drule_tac x = "schB" in subst_lemma1)
-back
-apply assumption
-apply (simp add: not_ext_is_int_or_not_act ForallTL ForallDropwhile)
+ text \<open>Case \<open>a \<in> B\<close>, \<open>a \<notin> A\<close>\<close>
+ apply (frule divide_Seq)
+ apply (erule conjE)+
+ text \<open>filtering internals of \<open>A\<close> is \<open>nil\<close>\<close>
+ apply (simp add: not_ext_is_int_or_not_act externals_of_par intA_is_not_extB int_is_not_ext)
+ apply (drule_tac x = "schB" in subst_lemma1)
+ back
+ apply assumption
+ apply (simp add: not_ext_is_int_or_not_act ForallTL ForallDropwhile)
-(* Case a~:A, a~:B *)
-apply (fastforce intro!: ext_is_act simp: externals_of_par)
-done
+ text \<open>Case \<open>a \<notin> A\<close>, \<open>a \<notin> B\<close>\<close>
+ apply (fastforce intro!: ext_is_act simp: externals_of_par)
+ done
subsection" Filter of mksch(tr,schA,schB) to A is schA -- take lemma proof"
-lemma FilterAmksch_is_schA: "!! A B. [| compatible A B; compatible B A;
- is_asig(asig_of A); is_asig(asig_of B) |] ==>
- Forall (%x. x:ext (A\<parallel>B)) tr &
- Forall (%x. x:act A) schA & Forall (%x. x:act B) schB &
- Filter (%a. a:ext A)$schA = Filter (%a. a:act A)$tr &
- Filter (%a. a:ext B)$schB = Filter (%a. a:act B)$tr &
- LastActExtsch A schA & LastActExtsch B schB
- --> Filter (%a. a:act A)$(mksch A B$tr$schA$schB) = schA"
-apply (intro strip)
-apply (rule seq.take_lemma)
-apply (rule mp)
-prefer 2 apply assumption
-back back back back
-apply (rule_tac x = "schA" in spec)
-apply (rule_tac x = "schB" in spec)
-apply (rule_tac x = "tr" in spec)
-apply (tactic "thin_tac' @{context} 5 1")
-apply (rule nat_less_induct)
-apply (rule allI)+
-apply (rename_tac tr schB schA)
-apply (intro strip)
-apply (erule conjE)+
+lemma FilterAmksch_is_schA:
+ "compatible A B \<Longrightarrow> compatible B A \<Longrightarrow> is_asig (asig_of A) \<Longrightarrow> is_asig (asig_of B) \<Longrightarrow>
+ Forall (\<lambda>x. x \<in> ext (A \<parallel> B)) tr \<and>
+ Forall (\<lambda>x. x \<in> act A) schA \<and>
+ Forall (\<lambda>x. x \<in> act B) schB \<and>
+ Filter (\<lambda>a. a \<in> ext A) $ schA = Filter (\<lambda>a. a \<in> act A) $ tr \<and>
+ Filter (\<lambda>a. a \<in> ext B) $ schB = Filter (\<lambda>a. a \<in> act B) $ tr \<and>
+ LastActExtsch A schA \<and> LastActExtsch B schB
+ \<longrightarrow> Filter (\<lambda>a. a \<in> act A) $ (mksch A B $ tr $ schA $ schB) = schA"
+ apply (intro strip)
+ apply (rule seq.take_lemma)
+ apply (rule mp)
+ prefer 2 apply assumption
+ back back back back
+ apply (rule_tac x = "schA" in spec)
+ apply (rule_tac x = "schB" in spec)
+ apply (rule_tac x = "tr" in spec)
+ apply (tactic "thin_tac' @{context} 5 1")
+ apply (rule nat_less_induct)
+ apply (rule allI)+
+ apply (rename_tac tr schB schA)
+ apply (intro strip)
+ apply (erule conjE)+
-apply (case_tac "Forall (%x. x:act B & x~:act A) tr")
+ apply (case_tac "Forall (\<lambda>x. x \<in> act B \<and> x \<notin> act A) tr")
-apply (rule seq_take_lemma [THEN iffD2, THEN spec])
-apply (tactic "thin_tac' @{context} 5 1")
+ apply (rule seq_take_lemma [THEN iffD2, THEN spec])
+ apply (tactic "thin_tac' @{context} 5 1")
-apply (case_tac "Finite tr")
+ apply (case_tac "Finite tr")
-(* both sides of this equation are nil *)
-apply (subgoal_tac "schA=nil")
-apply (simp (no_asm_simp))
-(* first side: mksch = nil *)
-apply (auto intro!: ForallQFilterPnil ForallBnAmksch FiniteL_mksch)[1]
-(* second side: schA = nil *)
-apply (erule_tac A = "A" in LastActExtimplnil)
-apply (simp (no_asm_simp))
-apply (erule_tac Q = "%x. x:act B & x~:act A" in ForallQFilterPnil)
-apply assumption
-apply fast
+ text \<open>both sides of this equation are \<open>nil\<close>\<close>
+ apply (subgoal_tac "schA = nil")
+ apply simp
+ text \<open>first side: \<open>mksch = nil\<close>\<close>
+ apply (auto intro!: ForallQFilterPnil ForallBnAmksch FiniteL_mksch)[1]
+ text \<open>second side: \<open>schA = nil\<close>\<close>
+ apply (erule_tac A = "A" in LastActExtimplnil)
+ apply simp
+ apply (erule_tac Q = "\<lambda>x. x \<in> act B \<and> x \<notin> act A" in ForallQFilterPnil)
+ apply assumption
+ apply fast
-(* case ~ Finite s *)
+ text \<open>case \<open>\<not> Finite s\<close>\<close>
-(* both sides of this equation are UU *)
-apply (subgoal_tac "schA=UU")
-apply (simp (no_asm_simp))
-(* first side: mksch = UU *)
-apply (auto intro!: ForallQFilterPUU finiteR_mksch' ForallBnAmksch)[1]
-(* schA = UU *)
-apply (erule_tac A = "A" in LastActExtimplUU)
-apply (simp (no_asm_simp))
-apply (erule_tac Q = "%x. x:act B & x~:act A" in ForallQFilterPUU)
-apply assumption
-apply fast
+ text \<open>both sides of this equation are \<open>UU\<close>\<close>
+ apply (subgoal_tac "schA = UU")
+ apply simp
+ text \<open>first side: \<open>mksch = UU\<close>\<close>
+ apply (auto intro!: ForallQFilterPUU finiteR_mksch' ForallBnAmksch)[1]
+ text \<open>\<open>schA = UU\<close>\<close>
+ apply (erule_tac A = "A" in LastActExtimplUU)
+ apply simp
+ apply (erule_tac Q = "\<lambda>x. x \<in> act B \<and> x \<notin> act A" in ForallQFilterPUU)
+ apply assumption
+ apply fast
-(* case" ~ Forall (%x.x:act B & x~:act A) s" *)
+ text \<open>case \<open>\<not> Forall (\<lambda>x. x \<in> act B \<and> x \<notin> act A) s\<close>\<close>
-apply (drule divide_Seq3)
+ apply (drule divide_Seq3)
-apply (erule exE)+
-apply (erule conjE)+
-apply hypsubst
+ apply (erule exE)+
+ apply (erule conjE)+
+ apply hypsubst
-(* bring in lemma reduceA_mksch *)
-apply (frule_tac x = "schA" and y = "schB" and A = "A" and B = "B" in reduceA_mksch)
-apply assumption+
-apply (erule exE)+
-apply (erule conjE)+
+ text \<open>bring in lemma \<open>reduceA_mksch\<close>\<close>
+ apply (frule_tac x = "schA" and y = "schB" and A = "A" and B = "B" in reduceA_mksch)
+ apply assumption+
+ apply (erule exE)+
+ apply (erule conjE)+
-(* use reduceA_mksch to rewrite conclusion *)
-apply hypsubst
-apply simp
+ text \<open>use \<open>reduceA_mksch\<close> to rewrite conclusion\<close>
+ apply hypsubst
+ apply simp
-(* eliminate the B-only prefix *)
+ text \<open>eliminate the \<open>B\<close>-only prefix\<close>
-apply (subgoal_tac " (Filter (%a. a :act A) $y1) = nil")
-apply (erule_tac [2] ForallQFilterPnil)
-prefer 2 apply assumption
-prefer 2 apply fast
+ apply (subgoal_tac "(Filter (\<lambda>a. a \<in> act A) $ y1) = nil")
+ apply (erule_tac [2] ForallQFilterPnil)
+ prefer 2 apply assumption
+ prefer 2 apply fast
-(* Now real recursive step follows (in y) *)
+ text \<open>Now real recursive step follows (in \<open>y\<close>)\<close>
-apply simp
-apply (case_tac "x:act A")
-apply (case_tac "x~:act B")
-apply (rotate_tac -2)
-apply simp
+ apply simp
+ apply (case_tac "x \<in> act A")
+ apply (case_tac "x \<notin> act B")
+ apply (rotate_tac -2)
+ apply simp
-apply (subgoal_tac "Filter (%a. a:act A & a:ext B) $y1=nil")
-apply (rotate_tac -1)
-apply simp
-(* eliminate introduced subgoal 2 *)
-apply (erule_tac [2] ForallQFilterPnil)
-prefer 2 apply assumption
-prefer 2 apply fast
+ apply (subgoal_tac "Filter (\<lambda>a. a \<in> act A \<and> a \<in> ext B) $ y1 = nil")
+ apply (rotate_tac -1)
+ apply simp
+ text \<open>eliminate introduced subgoal 2\<close>
+ apply (erule_tac [2] ForallQFilterPnil)
+ prefer 2 apply assumption
+ prefer 2 apply fast
-(* bring in divide Seq for s *)
-apply (frule sym [THEN eq_imp_below, THEN divide_Seq])
-apply (erule conjE)+
+ text \<open>bring in \<open>divide_Seq\<close> for \<open>s\<close>\<close>
+ apply (frule sym [THEN eq_imp_below, THEN divide_Seq])
+ apply (erule conjE)+
-(* subst divide_Seq in conclusion, but only at the righest occurrence *)
-apply (rule_tac t = "schA" in ssubst)
-back
-back
-back
-apply assumption
+ text \<open>subst \<open>divide_Seq\<close> in conclusion, but only at the rightest occurrence\<close>
+ apply (rule_tac t = "schA" in ssubst)
+ back
+ back
+ back
+ apply assumption
-(* reduce trace_takes from n to strictly smaller k *)
-apply (rule take_reduction)
+ text \<open>reduce trace_takes from \<open>n\<close> to strictly smaller \<open>k\<close>\<close>
+ apply (rule take_reduction)
-(* f A (tw iA) = tw ~eA *)
-apply (simp add: int_is_act not_ext_is_int_or_not_act)
-apply (rule refl)
-apply (simp add: int_is_act not_ext_is_int_or_not_act)
-apply (rotate_tac -11)
+ text \<open>\<open>f A (tw iA) = tw \<not> eA\<close>\<close>
+ apply (simp add: int_is_act not_ext_is_int_or_not_act)
+ apply (rule refl)
+ apply (simp add: int_is_act not_ext_is_int_or_not_act)
+ apply (rotate_tac -11)
-(* now conclusion fulfills induction hypothesis, but assumptions are not ready *)
+ text \<open>now conclusion fulfills induction hypothesis, but assumptions are not ready\<close>
-(* assumption Forall tr *)
-(* assumption schB *)
-apply (simp add: ext_and_act)
-(* assumption schA *)
-apply (drule_tac x = "schA" and g = "Filter (%a. a:act A) $rs" in subst_lemma2)
-apply assumption
-apply (simp add: int_is_not_ext)
-(* assumptions concerning LastActExtsch, cannot be rewritten, as LastActExtsmalli are looping *)
-apply (drule_tac sch = "schA" and P = "%a. a:int A" in LastActExtsmall1)
-apply (frule_tac ?sch1.0 = "y1" in LastActExtsmall2)
-apply assumption
+ text \<open>assumption \<open>Forall tr\<close>\<close>
+ text \<open>assumption \<open>schB\<close>\<close>
+ apply (simp add: ext_and_act)
+ text \<open>assumption \<open>schA\<close>\<close>
+ apply (drule_tac x = "schA" and g = "Filter (\<lambda>a. a \<in> act A) $ rs" in subst_lemma2)
+ apply assumption
+ apply (simp add: int_is_not_ext)
+ text \<open>assumptions concerning \<open>LastActExtsch\<close>, cannot be rewritten, as \<open>LastActExtsmalli\<close> are looping\<close>
+ apply (drule_tac sch = "schA" and P = "\<lambda>a. a \<in> int A" in LastActExtsmall1)
+ apply (frule_tac ?sch1.0 = "y1" in LastActExtsmall2)
+ apply assumption
-(* assumption Forall schA *)
-apply (drule_tac s = "schA" and P = "Forall (%x. x:act A) " in subst)
-apply assumption
-apply (simp add: int_is_act)
+ text \<open>assumption \<open>Forall schA\<close>\<close>
+ apply (drule_tac s = "schA" and P = "Forall (\<lambda>x. x \<in> act A) " in subst)
+ apply assumption
+ apply (simp add: int_is_act)
-(* case x:actions(asig_of A) & x: actions(asig_of B) *)
-
+ text \<open>case \<open>x \<in> actions (asig_of A) \<and> x \<in> actions (asig_of B)\<close>\<close>
-apply (rotate_tac -2)
-apply simp
+ apply (rotate_tac -2)
+ apply simp
-apply (subgoal_tac "Filter (%a. a:act A & a:ext B) $y1=nil")
-apply (rotate_tac -1)
-apply simp
-(* eliminate introduced subgoal 2 *)
-apply (erule_tac [2] ForallQFilterPnil)
-prefer 2 apply (assumption)
-prefer 2 apply (fast)
+ apply (subgoal_tac "Filter (\<lambda>a. a \<in> act A \<and> a \<in> ext B) $ y1 = nil")
+ apply (rotate_tac -1)
+ apply simp
+ text \<open>eliminate introduced subgoal 2\<close>
+ apply (erule_tac [2] ForallQFilterPnil)
+ prefer 2 apply assumption
+ prefer 2 apply fast
-(* bring in divide Seq for s *)
-apply (frule sym [THEN eq_imp_below, THEN divide_Seq])
-apply (erule conjE)+
+ text \<open>bring in \<open>divide_Seq\<close> for \<open>s\<close>\<close>
+ apply (frule sym [THEN eq_imp_below, THEN divide_Seq])
+ apply (erule conjE)+
-(* subst divide_Seq in conclusion, but only at the rightmost occurrence *)
-apply (rule_tac t = "schA" in ssubst)
-back
-back
-back
-apply assumption
+ text \<open>subst \<open>divide_Seq\<close> in conclusion, but only at the rightmost occurrence\<close>
+ apply (rule_tac t = "schA" in ssubst)
+ back
+ back
+ back
+ apply assumption
-(* f A (tw iA) = tw ~eA *)
-apply (simp add: int_is_act not_ext_is_int_or_not_act)
+ text \<open>\<open>f A (tw iA) = tw \<not> eA\<close>\<close>
+ apply (simp add: int_is_act not_ext_is_int_or_not_act)
-(* rewrite assumption forall and schB *)
-apply (rotate_tac 13)
-apply (simp add: ext_and_act)
+ text \<open>rewrite assumption forall and \<open>schB\<close>\<close>
+ apply (rotate_tac 13)
+ apply (simp add: ext_and_act)
-(* divide_Seq for schB2 *)
-apply (frule_tac y = "y2" in sym [THEN eq_imp_below, THEN divide_Seq])
-apply (erule conjE)+
-(* assumption schA *)
-apply (drule_tac x = "schA" and g = "Filter (%a. a:act A) $rs" in subst_lemma2)
-apply assumption
-apply (simp add: int_is_not_ext)
+ text \<open>\<open>divide_Seq\<close> for \<open>schB2\<close>\<close>
+ apply (frule_tac y = "y2" in sym [THEN eq_imp_below, THEN divide_Seq])
+ apply (erule conjE)+
+ text \<open>assumption \<open>schA\<close>\<close>
+ apply (drule_tac x = "schA" and g = "Filter (%a. a:act A) $rs" in subst_lemma2)
+ apply assumption
+ apply (simp add: int_is_not_ext)
-(* f A (tw iB schB2) = nil *)
-apply (simp add: int_is_not_ext not_ext_is_int_or_not_act intA_is_not_actB)
+ text \<open>\<open>f A (tw iB schB2) = nil\<close>\<close>
+ apply (simp add: int_is_not_ext not_ext_is_int_or_not_act intA_is_not_actB)
-(* reduce trace_takes from n to strictly smaller k *)
-apply (rule take_reduction)
-apply (rule refl)
-apply (rule refl)
-
-(* now conclusion fulfills induction hypothesis, but assumptions are not all ready *)
+ text \<open>reduce trace_takes from \<open>n\<close> to strictly smaller \<open>k\<close>\<close>
+ apply (rule take_reduction)
+ apply (rule refl)
+ apply (rule refl)
-(* assumption schB *)
-apply (drule_tac x = "y2" and g = "Filter (%a. a:act B) $rs" in subst_lemma2)
-apply assumption
-apply (simp add: intA_is_not_actB int_is_not_ext)
+ text \<open>now conclusion fulfills induction hypothesis, but assumptions are not all ready\<close>
-(* conclusions concerning LastActExtsch, cannot be rewritten, as LastActExtsmalli are looping *)
-apply (drule_tac sch = "schA" and P = "%a. a:int A" in LastActExtsmall1)
-apply (frule_tac ?sch1.0 = "y1" in LastActExtsmall2)
-apply assumption
-apply (drule_tac sch = "y2" and P = "%a. a:int B" in LastActExtsmall1)
+ text \<open>assumption \<open>schB\<close>\<close>
+ apply (drule_tac x = "y2" and g = "Filter (\<lambda>a. a \<in> act B) $ rs" in subst_lemma2)
+ apply assumption
+ apply (simp add: intA_is_not_actB int_is_not_ext)
-(* assumption Forall schA, and Forall schA are performed by ForallTL,ForallDropwhile *)
-apply (simp add: ForallTL ForallDropwhile)
+ text \<open>conclusions concerning \<open>LastActExtsch\<close>, cannot be rewritten, as \<open>LastActExtsmalli\<close> are looping\<close>
+ apply (drule_tac sch = "schA" and P = "\<lambda>a. a \<in> int A" in LastActExtsmall1)
+ apply (frule_tac ?sch1.0 = "y1" in LastActExtsmall2)
+ apply assumption
+ apply (drule_tac sch = "y2" and P = "\<lambda>a. a \<in> int B" in LastActExtsmall1)
-(* case x~:A & x:B *)
-(* cannot occur, as just this case has been scheduled out before as the B-only prefix *)
-apply (case_tac "x:act B")
-apply fast
+ text \<open>assumption \<open>Forall schA\<close>, and \<open>Forall schA\<close> are performed by \<open>ForallTL\<close>, \<open>ForallDropwhile\<close>\<close>
+ apply (simp add: ForallTL ForallDropwhile)
-(* case x~:A & x~:B *)
-(* cannot occur because of assumption: Forall (a:ext A | a:ext B) *)
-apply (rotate_tac -9)
-(* reduce forall assumption from tr to (x\<leadsto>rs) *)
-apply (simp add: externals_of_par)
-apply (fast intro!: ext_is_act)
+ text \<open>case \<open>x \<notin> A \<and> x \<in> B\<close>\<close>
+ text \<open>cannot occur, as just this case has been scheduled out before as the \<open>B\<close>-only prefix\<close>
+ apply (case_tac "x \<in> act B")
+ apply fast
-done
-
+ text \<open>case \<open>x \<notin> A \<and> x \<notin> B\<close>\<close>
+ text \<open>cannot occur because of assumption: \<open>Forall (a \<in> ext A \<or> a \<in> ext B)\<close>\<close>
+ apply (rotate_tac -9)
+ text \<open>reduce forall assumption from \<open>tr\<close> to \<open>x \<leadsto> rs\<close>\<close>
+ apply (simp add: externals_of_par)
+ apply (fast intro!: ext_is_act)
+ done
-subsection" Filter of mksch(tr,schA,schB) to B is schB -- take lemma proof"
+subsection \<open>Filter of \<open>mksch (tr, schA, schB)\<close> to \<open>B\<close> is \<open>schB\<close> -- take lemma proof\<close>
-lemma FilterBmksch_is_schB: "!! A B. [| compatible A B; compatible B A;
- is_asig(asig_of A); is_asig(asig_of B) |] ==>
- Forall (%x. x:ext (A\<parallel>B)) tr &
- Forall (%x. x:act A) schA & Forall (%x. x:act B) schB &
- Filter (%a. a:ext A)$schA = Filter (%a. a:act A)$tr &
- Filter (%a. a:ext B)$schB = Filter (%a. a:act B)$tr &
- LastActExtsch A schA & LastActExtsch B schB
- --> Filter (%a. a:act B)$(mksch A B$tr$schA$schB) = schB"
-apply (intro strip)
-apply (rule seq.take_lemma)
-apply (rule mp)
-prefer 2 apply assumption
-back back back back
-apply (rule_tac x = "schA" in spec)
-apply (rule_tac x = "schB" in spec)
-apply (rule_tac x = "tr" in spec)
-apply (tactic "thin_tac' @{context} 5 1")
-apply (rule nat_less_induct)
-apply (rule allI)+
-apply (rename_tac tr schB schA)
-apply (intro strip)
-apply (erule conjE)+
+lemma FilterBmksch_is_schB:
+ "compatible A B \<Longrightarrow> compatible B A \<Longrightarrow> is_asig (asig_of A) \<Longrightarrow> is_asig (asig_of B) \<Longrightarrow>
+ Forall (\<lambda>x. x \<in> ext (A \<parallel> B)) tr \<and>
+ Forall (\<lambda>x. x \<in> act A) schA \<and>
+ Forall (\<lambda>x. x \<in> act B) schB \<and>
+ Filter (\<lambda>a. a \<in> ext A) $ schA = Filter (\<lambda>a. a \<in> act A) $ tr \<and>
+ Filter (\<lambda>a. a \<in> ext B) $ schB = Filter (\<lambda>a. a \<in> act B) $ tr \<and>
+ LastActExtsch A schA \<and> LastActExtsch B schB
+ \<longrightarrow> Filter (\<lambda>a. a \<in> act B) $ (mksch A B $ tr $ schA $ schB) = schB"
+ apply (intro strip)
+ apply (rule seq.take_lemma)
+ apply (rule mp)
+ prefer 2 apply assumption
+ back back back back
+ apply (rule_tac x = "schA" in spec)
+ apply (rule_tac x = "schB" in spec)
+ apply (rule_tac x = "tr" in spec)
+ apply (tactic "thin_tac' @{context} 5 1")
+ apply (rule nat_less_induct)
+ apply (rule allI)+
+ apply (rename_tac tr schB schA)
+ apply (intro strip)
+ apply (erule conjE)+
-apply (case_tac "Forall (%x. x:act A & x~:act B) tr")
+ apply (case_tac "Forall (\<lambda>x. x \<in> act A \<and> x \<notin> act B) tr")
-apply (rule seq_take_lemma [THEN iffD2, THEN spec])
-apply (tactic "thin_tac' @{context} 5 1")
+ apply (rule seq_take_lemma [THEN iffD2, THEN spec])
+ apply (tactic "thin_tac' @{context} 5 1")
-apply (case_tac "Finite tr")
+ apply (case_tac "Finite tr")
-(* both sides of this equation are nil *)
-apply (subgoal_tac "schB=nil")
-apply (simp (no_asm_simp))
-(* first side: mksch = nil *)
-apply (auto intro!: ForallQFilterPnil ForallAnBmksch FiniteL_mksch)[1]
-(* second side: schA = nil *)
-apply (erule_tac A = "B" in LastActExtimplnil)
-apply (simp (no_asm_simp))
-apply (erule_tac Q = "%x. x:act A & x~:act B" in ForallQFilterPnil)
-apply assumption
-apply fast
+ text \<open>both sides of this equation are \<open>nil\<close>\<close>
+ apply (subgoal_tac "schB = nil")
+ apply simp
+ text \<open>first side: \<open>mksch = nil\<close>\<close>
+ apply (auto intro!: ForallQFilterPnil ForallAnBmksch FiniteL_mksch)[1]
+ text \<open>second side: \<open>schA = nil\<close>\<close>
+ apply (erule_tac A = "B" in LastActExtimplnil)
+ apply (simp (no_asm_simp))
+ apply (erule_tac Q = "\<lambda>x. x \<in> act A \<and> x \<notin> act B" in ForallQFilterPnil)
+ apply assumption
+ apply fast
-(* case ~ Finite tr *)
+ text \<open>case \<open>\<not> Finite tr\<close>\<close>
-(* both sides of this equation are UU *)
-apply (subgoal_tac "schB=UU")
-apply (simp (no_asm_simp))
-(* first side: mksch = UU *)
-apply (force intro!: ForallQFilterPUU finiteR_mksch' ForallAnBmksch)
-(* schA = UU *)
-apply (erule_tac A = "B" in LastActExtimplUU)
-apply (simp (no_asm_simp))
-apply (erule_tac Q = "%x. x:act A & x~:act B" in ForallQFilterPUU)
-apply assumption
-apply fast
+ text \<open>both sides of this equation are \<open>UU\<close>\<close>
+ apply (subgoal_tac "schB = UU")
+ apply simp
+ text \<open>first side: \<open>mksch = UU\<close>\<close>
+ apply (force intro!: ForallQFilterPUU finiteR_mksch' ForallAnBmksch)
+ text \<open>\<open>schA = UU\<close>\<close>
+ apply (erule_tac A = "B" in LastActExtimplUU)
+ apply simp
+ apply (erule_tac Q = "\<lambda>x. x \<in> act A \<and> x \<notin> act B" in ForallQFilterPUU)
+ apply assumption
+ apply fast
-(* case" ~ Forall (%x.x:act B & x~:act A) s" *)
+ text \<open>case \<open>\<not> Forall (\<lambda>x. x \<in> act B \<and> x \<notin> act A) s\<close>\<close>
-apply (drule divide_Seq3)
+ apply (drule divide_Seq3)
-apply (erule exE)+
-apply (erule conjE)+
-apply hypsubst
+ apply (erule exE)+
+ apply (erule conjE)+
+ apply hypsubst
-(* bring in lemma reduceB_mksch *)
-apply (frule_tac y = "schB" and x = "schA" and A = "A" and B = "B" in reduceB_mksch)
-apply assumption+
-apply (erule exE)+
-apply (erule conjE)+
+ text \<open>bring in lemma \<open>reduceB_mksch\<close>\<close>
+ apply (frule_tac y = "schB" and x = "schA" and A = "A" and B = "B" in reduceB_mksch)
+ apply assumption+
+ apply (erule exE)+
+ apply (erule conjE)+
-(* use reduceB_mksch to rewrite conclusion *)
-apply hypsubst
-apply simp
+ text \<open>use \<open>reduceB_mksch\<close> to rewrite conclusion\<close>
+ apply hypsubst
+ apply simp
-(* eliminate the A-only prefix *)
+ text \<open>eliminate the \<open>A\<close>-only prefix\<close>
-apply (subgoal_tac "(Filter (%a. a :act B) $x1) = nil")
-apply (erule_tac [2] ForallQFilterPnil)
-prefer 2 apply (assumption)
-prefer 2 apply (fast)
+ apply (subgoal_tac "(Filter (\<lambda>a. a \<in> act B) $ x1) = nil")
+ apply (erule_tac [2] ForallQFilterPnil)
+ prefer 2 apply (assumption)
+ prefer 2 apply (fast)
-(* Now real recursive step follows (in x) *)
+ text \<open>Now real recursive step follows (in \<open>x\<close>)\<close>
-apply simp
-apply (case_tac "x:act B")
-apply (case_tac "x~:act A")
-apply (rotate_tac -2)
-apply simp
+ apply simp
+ apply (case_tac "x \<in> act B")
+ apply (case_tac "x \<notin> act A")
+ apply (rotate_tac -2)
+ apply simp
-apply (subgoal_tac "Filter (%a. a:act B & a:ext A) $x1=nil")
-apply (rotate_tac -1)
-apply simp
-(* eliminate introduced subgoal 2 *)
-apply (erule_tac [2] ForallQFilterPnil)
-prefer 2 apply (assumption)
-prefer 2 apply (fast)
+ apply (subgoal_tac "Filter (\<lambda>a. a \<in> act B \<and> a \<in> ext A) $ x1 = nil")
+ apply (rotate_tac -1)
+ apply simp
+ text \<open>eliminate introduced subgoal 2\<close>
+ apply (erule_tac [2] ForallQFilterPnil)
+ prefer 2 apply assumption
+ prefer 2 apply fast
-(* bring in divide Seq for s *)
-apply (frule sym [THEN eq_imp_below, THEN divide_Seq])
-apply (erule conjE)+
+ text \<open>bring in \<open>divide_Seq\<close> for \<open>s\<close>\<close>
+ apply (frule sym [THEN eq_imp_below, THEN divide_Seq])
+ apply (erule conjE)+
-(* subst divide_Seq in conclusion, but only at the rightmost occurrence *)
-apply (rule_tac t = "schB" in ssubst)
-back
-back
-back
-apply assumption
+ text \<open>subst \<open>divide_Seq\<close> in conclusion, but only at the rightmost occurrence\<close>
+ apply (rule_tac t = "schB" in ssubst)
+ back
+ back
+ back
+ apply assumption
-(* reduce trace_takes from n to strictly smaller k *)
-apply (rule take_reduction)
+ text \<open>reduce \<open>trace_takes\<close> from \<open>n\<close> to strictly smaller \<open>k\<close>\<close>
+ apply (rule take_reduction)
-(* f B (tw iB) = tw ~eB *)
-apply (simp add: int_is_act not_ext_is_int_or_not_act)
-apply (rule refl)
-apply (simp add: int_is_act not_ext_is_int_or_not_act)
-apply (rotate_tac -11)
+ text \<open>\<open>f B (tw iB) = tw \<not> eB\<close>\<close>
+ apply (simp add: int_is_act not_ext_is_int_or_not_act)
+ apply (rule refl)
+ apply (simp add: int_is_act not_ext_is_int_or_not_act)
+ apply (rotate_tac -11)
-(* now conclusion fulfills induction hypothesis, but assumptions are not ready *)
+ text \<open>now conclusion fulfills induction hypothesis, but assumptions are not ready\<close>
-(* assumption schA *)
-apply (simp add: ext_and_act)
-(* assumption schB *)
-apply (drule_tac x = "schB" and g = "Filter (%a. a:act B) $rs" in subst_lemma2)
-apply assumption
-apply (simp add: int_is_not_ext)
-(* assumptions concerning LastActExtsch, cannot be rewritten, as LastActExtsmalli are looping *)
-apply (drule_tac sch = "schB" and P = "%a. a:int B" in LastActExtsmall1)
-apply (frule_tac ?sch1.0 = "x1" in LastActExtsmall2)
-apply assumption
+ text \<open>assumption \<open>schA\<close>\<close>
+ apply (simp add: ext_and_act)
+ text \<open>assumption \<open>schB\<close>\<close>
+ apply (drule_tac x = "schB" and g = "Filter (\<lambda>a. a \<in> act B) $ rs" in subst_lemma2)
+ apply assumption
+ apply (simp add: int_is_not_ext)
+ text \<open>assumptions concerning \<open>LastActExtsch\<close>, cannot be rewritten, as \<open>LastActExtsmalli\<close> are looping\<close>
+ apply (drule_tac sch = "schB" and P = "\<lambda>a. a \<in> int B" in LastActExtsmall1)
+ apply (frule_tac ?sch1.0 = "x1" in LastActExtsmall2)
+ apply assumption
-(* assumption Forall schB *)
-apply (drule_tac s = "schB" and P = "Forall (%x. x:act B) " in subst)
-apply assumption
-apply (simp add: int_is_act)
+ text \<open>assumption \<open>Forall schB\<close>\<close>
+ apply (drule_tac s = "schB" and P = "Forall (\<lambda>x. x \<in> act B)" in subst)
+ apply assumption
+ apply (simp add: int_is_act)
-(* case x:actions(asig_of A) & x: actions(asig_of B) *)
+ text \<open>case \<open>x \<in> actions (asig_of A) \<and> x \<in> actions (asig_of B)\<close>\<close>
-apply (rotate_tac -2)
-apply simp
+ apply (rotate_tac -2)
+ apply simp
-apply (subgoal_tac "Filter (%a. a:act B & a:ext A) $x1=nil")
-apply (rotate_tac -1)
-apply simp
-(* eliminate introduced subgoal 2 *)
-apply (erule_tac [2] ForallQFilterPnil)
-prefer 2 apply (assumption)
-prefer 2 apply (fast)
+ apply (subgoal_tac "Filter (\<lambda>a. a \<in> act B \<and> a \<in> ext A) $ x1 = nil")
+ apply (rotate_tac -1)
+ apply simp
+ text \<open>eliminate introduced subgoal 2\<close>
+ apply (erule_tac [2] ForallQFilterPnil)
+ prefer 2 apply assumption
+ prefer 2 apply fast
-(* bring in divide Seq for s *)
-apply (frule sym [THEN eq_imp_below, THEN divide_Seq])
-apply (erule conjE)+
+ text \<open>bring in \<open>divide_Seq\<close> for \<open>s\<close>\<close>
+ apply (frule sym [THEN eq_imp_below, THEN divide_Seq])
+ apply (erule conjE)+
-(* subst divide_Seq in conclusion, but only at the rightmost occurrence *)
-apply (rule_tac t = "schB" in ssubst)
-back
-back
-back
-apply assumption
+ text \<open>subst \<open>divide_Seq\<close> in conclusion, but only at the rightmost occurrence\<close>
+ apply (rule_tac t = "schB" in ssubst)
+ back
+ back
+ back
+ apply assumption
-(* f B (tw iB) = tw ~eB *)
-apply (simp add: int_is_act not_ext_is_int_or_not_act)
+ text \<open>\<open>f B (tw iB) = tw \<not> eB\<close>\<close>
+ apply (simp add: int_is_act not_ext_is_int_or_not_act)
-(* rewrite assumption forall and schB *)
-apply (rotate_tac 13)
-apply (simp add: ext_and_act)
+ text \<open>rewrite assumption forall and \<open>schB\<close>\<close>
+ apply (rotate_tac 13)
+ apply (simp add: ext_and_act)
-(* divide_Seq for schB2 *)
-apply (frule_tac y = "x2" in sym [THEN eq_imp_below, THEN divide_Seq])
-apply (erule conjE)+
-(* assumption schA *)
-apply (drule_tac x = "schB" and g = "Filter (%a. a:act B) $rs" in subst_lemma2)
-apply assumption
-apply (simp add: int_is_not_ext)
+ text \<open>\<open>divide_Seq\<close> for \<open>schB2\<close>\<close>
+ apply (frule_tac y = "x2" in sym [THEN eq_imp_below, THEN divide_Seq])
+ apply (erule conjE)+
+ text \<open>assumption \<open>schA\<close>\<close>
+ apply (drule_tac x = "schB" and g = "Filter (\<lambda>a. a \<in> act B) $ rs" in subst_lemma2)
+ apply assumption
+ apply (simp add: int_is_not_ext)
-(* f B (tw iA schA2) = nil *)
-apply (simp add: int_is_not_ext not_ext_is_int_or_not_act intA_is_not_actB)
+ text \<open>\<open>f B (tw iA schA2) = nil\<close>\<close>
+ apply (simp add: int_is_not_ext not_ext_is_int_or_not_act intA_is_not_actB)
-(* reduce trace_takes from n to strictly smaller k *)
-apply (rule take_reduction)
-apply (rule refl)
-apply (rule refl)
+ text \<open>reduce \<open>trace_takes from \<open>n\<close> to strictly smaller \<open>k\<close>\<close>\<close>
+ apply (rule take_reduction)
+ apply (rule refl)
+ apply (rule refl)
-(* now conclusion fulfills induction hypothesis, but assumptions are not all ready *)
+ text \<open>now conclusion fulfills induction hypothesis, but assumptions are not all ready\<close>
-(* assumption schA *)
-apply (drule_tac x = "x2" and g = "Filter (%a. a:act A) $rs" in subst_lemma2)
-apply assumption
-apply (simp add: intA_is_not_actB int_is_not_ext)
+ text \<open>assumption \<open>schA\<close>\<close>
+ apply (drule_tac x = "x2" and g = "Filter (\<lambda>a. a \<in> act A) $ rs" in subst_lemma2)
+ apply assumption
+ apply (simp add: intA_is_not_actB int_is_not_ext)
-(* conclusions concerning LastActExtsch, cannot be rewritten, as LastActExtsmalli are looping *)
-apply (drule_tac sch = "schB" and P = "%a. a:int B" in LastActExtsmall1)
-apply (frule_tac ?sch1.0 = "x1" in LastActExtsmall2)
-apply assumption
-apply (drule_tac sch = "x2" and P = "%a. a:int A" in LastActExtsmall1)
+ text \<open>conclusions concerning \<open>LastActExtsch\<close>, cannot be rewritten, as \<open>LastActExtsmalli\<close> are looping\<close>
+ apply (drule_tac sch = "schB" and P = "%a. a:int B" in LastActExtsmall1)
+ apply (frule_tac ?sch1.0 = "x1" in LastActExtsmall2)
+ apply assumption
+ apply (drule_tac sch = "x2" and P = "%a. a:int A" in LastActExtsmall1)
-(* assumption Forall schA, and Forall schA are performed by ForallTL,ForallDropwhile *)
-apply (simp add: ForallTL ForallDropwhile)
+ text \<open>assumption \<open>Forall schA\<close>, and \<open>Forall schA\<close> are performed by \<open>ForallTL\<close>, \<open>ForallDropwhile\<close>\<close>
+ apply (simp add: ForallTL ForallDropwhile)
-(* case x~:B & x:A *)
-(* cannot occur, as just this case has been scheduled out before as the B-only prefix *)
-apply (case_tac "x:act A")
-apply fast
+ text \<open>case \<open>x \<notin> B \<and> x \<in> A\<close>\<close>
+ text \<open>cannot occur, as just this case has been scheduled out before as the \<open>B\<close>-only prefix\<close>
+ apply (case_tac "x \<in> act A")
+ apply fast
-(* case x~:B & x~:A *)
-(* cannot occur because of assumption: Forall (a:ext A | a:ext B) *)
-apply (rotate_tac -9)
-(* reduce forall assumption from tr to (x\<leadsto>rs) *)
-apply (simp add: externals_of_par)
-apply (fast intro!: ext_is_act)
-
-done
+ text \<open>case \<open>x \<notin> B \<and> x \<notin> A\<close>\<close>
+ text \<open>cannot occur because of assumption: \<open>Forall (a \<in> ext A \<or> a \<in> ext B)\<close>\<close>
+ apply (rotate_tac -9)
+ text \<open>reduce forall assumption from \<open>tr\<close> to \<open>x \<leadsto> rs\<close>\<close>
+ apply (simp add: externals_of_par)
+ apply (fast intro!: ext_is_act)
+ done
subsection "COMPOSITIONALITY on TRACE Level -- Main Theorem"
-lemma compositionality_tr:
-"!! A B. [| is_trans_of A; is_trans_of B; compatible A B; compatible B A;
- is_asig(asig_of A); is_asig(asig_of B)|]
- ==> (tr: traces(A\<parallel>B)) =
- (Filter (%a. a:act A)$tr : traces A &
- Filter (%a. a:act B)$tr : traces B &
- Forall (%x. x:ext(A\<parallel>B)) tr)"
-
-apply (simp (no_asm) add: traces_def has_trace_def)
-apply auto
+theorem compositionality_tr:
+ "is_trans_of A \<Longrightarrow> is_trans_of B \<Longrightarrow> compatible A B \<Longrightarrow> compatible B A \<Longrightarrow>
+ is_asig (asig_of A) \<Longrightarrow> is_asig (asig_of B) \<Longrightarrow>
+ tr \<in> traces (A \<parallel> B) \<longleftrightarrow>
+ Filter (\<lambda>a. a \<in> act A) $ tr \<in> traces A \<and>
+ Filter (\<lambda>a. a \<in> act B) $ tr \<in> traces B \<and>
+ Forall (\<lambda>x. x \<in> ext(A \<parallel> B)) tr"
+ apply (simp add: traces_def has_trace_def)
+ apply auto
-(* ==> *)
-(* There is a schedule of A *)
-apply (rule_tac x = "Filter (%a. a:act A) $sch" in bexI)
-prefer 2
-apply (simp add: compositionality_sch)
-apply (simp add: compatibility_consequence1 externals_of_par ext1_ext2_is_not_act1)
-(* There is a schedule of B *)
-apply (rule_tac x = "Filter (%a. a:act B) $sch" in bexI)
-prefer 2
-apply (simp add: compositionality_sch)
-apply (simp add: compatibility_consequence2 externals_of_par ext1_ext2_is_not_act2)
-(* Traces of A\<parallel>B have only external actions from A or B *)
-apply (rule ForallPFilterP)
+ text \<open>\<open>\<Longrightarrow>\<close>\<close>
+ text \<open>There is a schedule of \<open>A\<close>\<close>
+ apply (rule_tac x = "Filter (\<lambda>a. a \<in> act A) $ sch" in bexI)
+ prefer 2
+ apply (simp add: compositionality_sch)
+ apply (simp add: compatibility_consequence1 externals_of_par ext1_ext2_is_not_act1)
+ text \<open>There is a schedule of \<open>B\<close>\<close>
+ apply (rule_tac x = "Filter (\<lambda>a. a \<in> act B) $ sch" in bexI)
+ prefer 2
+ apply (simp add: compositionality_sch)
+ apply (simp add: compatibility_consequence2 externals_of_par ext1_ext2_is_not_act2)
+ text \<open>Traces of \<open>A \<parallel> B\<close> have only external actions from \<open>A\<close> or \<open>B\<close>\<close>
+ apply (rule ForallPFilterP)
-(* <== *)
+ text \<open>\<open>\<Longleftarrow>\<close>\<close>
-(* replace schA and schB by Cut(schA) and Cut(schB) *)
-apply (drule exists_LastActExtsch)
-apply assumption
-apply (drule exists_LastActExtsch)
-apply assumption
-apply (erule exE)+
-apply (erule conjE)+
-(* Schedules of A(B) have only actions of A(B) *)
-apply (drule scheds_in_sig)
-apply assumption
-apply (drule scheds_in_sig)
-apply assumption
+ text \<open>replace \<open>schA\<close> and \<open>schB\<close> by \<open>Cut schA\<close> and \<open>Cut schB\<close>\<close>
+ apply (drule exists_LastActExtsch)
+ apply assumption
+ apply (drule exists_LastActExtsch)
+ apply assumption
+ apply (erule exE)+
+ apply (erule conjE)+
+ text \<open>Schedules of A(B) have only actions of A(B)\<close>
+ apply (drule scheds_in_sig)
+ apply assumption
+ apply (drule scheds_in_sig)
+ apply assumption
-apply (rename_tac h1 h2 schA schB)
-(* mksch is exactly the construction of trA\<parallel>B out of schA, schB, and the oracle tr,
- we need here *)
-apply (rule_tac x = "mksch A B$tr$schA$schB" in bexI)
+ apply (rename_tac h1 h2 schA schB)
+ text \<open>\<open>mksch\<close> is exactly the construction of \<open>trA\<parallel>B\<close> out of \<open>schA\<close>, \<open>schB\<close>, and the oracle \<open>tr\<close>,
+ we need here\<close>
+ apply (rule_tac x = "mksch A B $ tr $ schA $ schB" in bexI)
-(* External actions of mksch are just the oracle *)
-apply (simp add: FilterA_mksch_is_tr)
+ text \<open>External actions of mksch are just the oracle\<close>
+ apply (simp add: FilterA_mksch_is_tr)
-(* mksch is a schedule -- use compositionality on sch-level *)
-apply (simp add: compositionality_sch)
-apply (simp add: FilterAmksch_is_schA FilterBmksch_is_schB)
-apply (erule ForallAorB_mksch)
-apply (erule ForallPForallQ)
-apply (erule ext_is_act)
-done
+ text \<open>\<open>mksch\<close> is a schedule -- use compositionality on sch-level\<close>
+ apply (simp add: compositionality_sch)
+ apply (simp add: FilterAmksch_is_schA FilterBmksch_is_schB)
+ apply (erule ForallAorB_mksch)
+ apply (erule ForallPForallQ)
+ apply (erule ext_is_act)
+ done
subsection \<open>COMPOSITIONALITY on TRACE Level -- for Modules\<close>
lemma compositionality_tr_modules:
-
-"!! A B. [| is_trans_of A; is_trans_of B; compatible A B; compatible B A;
- is_asig(asig_of A); is_asig(asig_of B)|]
- ==> Traces (A\<parallel>B) = par_traces (Traces A) (Traces B)"
-
-apply (unfold Traces_def par_traces_def)
-apply (simp add: asig_of_par)
-apply (rule set_eqI)
-apply (simp add: compositionality_tr externals_of_par)
-done
+ "is_trans_of A \<Longrightarrow> is_trans_of B \<Longrightarrow> compatible A B \<Longrightarrow> compatible B A \<Longrightarrow>
+ is_asig(asig_of A) \<Longrightarrow> is_asig(asig_of B) \<Longrightarrow>
+ Traces (A\<parallel>B) = par_traces (Traces A) (Traces B)"
+ apply (unfold Traces_def par_traces_def)
+ apply (simp add: asig_of_par)
+ apply (rule set_eqI)
+ apply (simp add: compositionality_tr externals_of_par)
+ done
declaration \<open>fn _ => Simplifier.map_ss (Simplifier.set_mksym Simplifier.default_mk_sym)\<close>
-
end
--- a/src/HOL/HOLCF/IOA/Deadlock.thy Tue Jan 12 20:05:53 2016 +0100
+++ b/src/HOL/HOLCF/IOA/Deadlock.thy Tue Jan 12 23:40:33 2016 +0100
@@ -8,85 +8,91 @@
imports RefCorrectness CompoScheds
begin
-text \<open>input actions may always be added to a schedule\<close>
+text \<open>Input actions may always be added to a schedule.\<close>
lemma scheds_input_enabled:
- "[| Filter (%x. x:act A)$sch : schedules A; a:inp A; input_enabled A; Finite sch|]
- ==> Filter (%x. x:act A)$sch @@ a\<leadsto>nil : schedules A"
-apply (simp add: schedules_def has_schedule_def)
-apply auto
-apply (frule inp_is_act)
-apply (simp add: executions_def)
-apply (tactic \<open>pair_tac @{context} "ex" 1\<close>)
-apply (rename_tac s ex)
-apply (subgoal_tac "Finite ex")
-prefer 2
-apply (simp add: filter_act_def)
-defer
-apply (rule_tac [2] Map2Finite [THEN iffD1])
-apply (rule_tac [2] t = "Map fst$ex" in subst)
-prefer 2 apply (assumption)
-apply (erule_tac [2] FiniteFilter)
-(* subgoal 1 *)
-apply (frule exists_laststate)
-apply (erule allE)
-apply (erule exE)
-(* using input-enabledness *)
-apply (simp add: input_enabled_def)
-apply (erule conjE)+
-apply (erule_tac x = "a" in allE)
-apply simp
-apply (erule_tac x = "u" in allE)
-apply (erule exE)
-(* instantiate execution *)
-apply (rule_tac x = " (s,ex @@ (a,s2) \<leadsto>nil) " in exI)
-apply (simp add: filter_act_def MapConc)
-apply (erule_tac t = "u" in lemma_2_1)
-apply simp
-apply (rule sym)
-apply assumption
-done
+ "Filter (\<lambda>x. x \<in> act A) $ sch \<in> schedules A \<Longrightarrow> a \<in> inp A \<Longrightarrow> input_enabled A \<Longrightarrow> Finite sch
+ \<Longrightarrow> Filter (\<lambda>x. x \<in> act A) $ sch @@ a \<leadsto> nil \<in> schedules A"
+ apply (simp add: schedules_def has_schedule_def)
+ apply auto
+ apply (frule inp_is_act)
+ apply (simp add: executions_def)
+ apply (tactic \<open>pair_tac @{context} "ex" 1\<close>)
+ apply (rename_tac s ex)
+ apply (subgoal_tac "Finite ex")
+ prefer 2
+ apply (simp add: filter_act_def)
+ defer
+ apply (rule_tac [2] Map2Finite [THEN iffD1])
+ apply (rule_tac [2] t = "Map fst $ ex" in subst)
+ prefer 2
+ apply assumption
+ apply (erule_tac [2] FiniteFilter)
+ text \<open>subgoal 1\<close>
+ apply (frule exists_laststate)
+ apply (erule allE)
+ apply (erule exE)
+ text \<open>using input-enabledness\<close>
+ apply (simp add: input_enabled_def)
+ apply (erule conjE)+
+ apply (erule_tac x = "a" in allE)
+ apply simp
+ apply (erule_tac x = "u" in allE)
+ apply (erule exE)
+ text \<open>instantiate execution\<close>
+ apply (rule_tac x = " (s, ex @@ (a, s2) \<leadsto> nil) " in exI)
+ apply (simp add: filter_act_def MapConc)
+ apply (erule_tac t = "u" in lemma_2_1)
+ apply simp
+ apply (rule sym)
+ apply assumption
+ done
text \<open>
- Deadlock freedom: component B cannot block an out or int action
- of component A in every schedule.
- Needs compositionality on schedule level, input-enabledness, compatibility
- and distributivity of is_exec_frag over @@
+ Deadlock freedom: component B cannot block an out or int action of component
+ A in every schedule.
+
+ Needs compositionality on schedule level, input-enabledness, compatibility
+ and distributivity of \<open>is_exec_frag\<close> over \<open>@@\<close>.
\<close>
-declare split_if [split del]
-lemma IOA_deadlock_free: "[| a : local A; Finite sch; sch : schedules (A\<parallel>B);
- Filter (%x. x:act A)$(sch @@ a\<leadsto>nil) : schedules A; compatible A B; input_enabled B |]
- ==> (sch @@ a\<leadsto>nil) : schedules (A\<parallel>B)"
-apply (simp add: compositionality_sch locals_def)
-apply (rule conjI)
-(* a : act (A\<parallel>B) *)
-prefer 2
-apply (simp add: actions_of_par)
-apply (blast dest: int_is_act out_is_act)
-
-(* Filter B (sch@@[a]) : schedules B *)
+lemma IOA_deadlock_free:
+ assumes "a \<in> local A"
+ and "Finite sch"
+ and "sch \<in> schedules (A \<parallel> B)"
+ and "Filter (\<lambda>x. x \<in> act A) $ (sch @@ a \<leadsto> nil) \<in> schedules A"
+ and "compatible A B"
+ and "input_enabled B"
+ shows "(sch @@ a \<leadsto> nil) \<in> schedules (A \<parallel> B)"
+ supply split_if [split del]
+ apply (insert assms)
+ apply (simp add: compositionality_sch locals_def)
+ apply (rule conjI)
+ text \<open>\<open>a \<in> act (A \<parallel> B)\<close>\<close>
+ prefer 2
+ apply (simp add: actions_of_par)
+ apply (blast dest: int_is_act out_is_act)
-apply (case_tac "a:int A")
-apply (drule intA_is_not_actB)
-apply (assumption) (* --> a~:act B *)
-apply simp
+ text \<open>\<open>Filter B (sch @@ [a]) \<in> schedules B\<close>\<close>
+ apply (case_tac "a \<in> int A")
+ apply (drule intA_is_not_actB)
+ apply (assumption) (* \<longrightarrow> a \<notin> act B *)
+ apply simp
-(* case a~:int A , i.e. a:out A *)
-apply (case_tac "a~:act B")
-apply simp
-(* case a:act B *)
-apply simp
-apply (subgoal_tac "a:out A")
-prefer 2 apply (blast)
-apply (drule outAactB_is_inpB)
-apply assumption
-apply assumption
-apply (rule scheds_input_enabled)
-apply simp
-apply assumption+
-done
-
-declare split_if [split]
+ text \<open>case \<open>a \<notin> int A\<close>, i.e. \<open>a \<in> out A\<close>\<close>
+ apply (case_tac "a \<notin> act B")
+ apply simp
+ text \<open>case \<open>a \<in> act B\<close>\<close>
+ apply simp
+ apply (subgoal_tac "a \<in> out A")
+ prefer 2
+ apply blast
+ apply (drule outAactB_is_inpB)
+ apply assumption
+ apply assumption
+ apply (rule scheds_input_enabled)
+ apply simp
+ apply assumption+
+ done
end
--- a/src/HOL/HOLCF/IOA/RefCorrectness.thy Tue Jan 12 20:05:53 2016 +0100
+++ b/src/HOL/HOLCF/IOA/RefCorrectness.thy Tue Jan 12 23:40:33 2016 +0100
@@ -8,363 +8,349 @@
imports RefMappings
begin
-definition
- corresp_exC :: "('a,'s2)ioa => ('s1 => 's2) => ('a,'s1)pairs
- -> ('s1 => ('a,'s2)pairs)" where
- "corresp_exC A f = (fix$(LAM h ex. (%s. case ex of
- nil => nil
- | x##xs => (flift1 (%pr. (@cex. move A cex (f s) (fst pr) (f (snd pr)))
- @@ ((h$xs) (snd pr)))
- $x) )))"
-definition
- corresp_ex :: "('a,'s2)ioa => ('s1 => 's2) =>
- ('a,'s1)execution => ('a,'s2)execution" where
- "corresp_ex A f ex = (f (fst ex),(corresp_exC A f$(snd ex)) (fst ex))"
+definition corresp_exC ::
+ "('a, 's2) ioa \<Rightarrow> ('s1 \<Rightarrow> 's2) \<Rightarrow> ('a, 's1) pairs \<rightarrow> ('s1 \<Rightarrow> ('a, 's2) pairs)"
+ where "corresp_exC A f =
+ (fix $
+ (LAM h ex.
+ (\<lambda>s. case ex of
+ nil \<Rightarrow> nil
+ | x ## xs \<Rightarrow>
+ flift1 (\<lambda>pr.
+ (SOME cex. move A cex (f s) (fst pr) (f (snd pr))) @@ ((h $ xs) (snd pr))) $ x)))"
-definition
- is_fair_ref_map :: "('s1 => 's2) => ('a,'s1)ioa => ('a,'s2)ioa => bool" where
- "is_fair_ref_map f C A =
- (is_ref_map f C A &
- (! ex : executions(C). fair_ex C ex --> fair_ex A (corresp_ex A f ex)))"
+definition corresp_ex ::
+ "('a, 's2) ioa \<Rightarrow> ('s1 \<Rightarrow> 's2) \<Rightarrow> ('a, 's1) execution \<Rightarrow> ('a, 's2) execution"
+ where "corresp_ex A f ex = (f (fst ex), (corresp_exC A f $ (snd ex)) (fst ex))"
-(* Axioms for fair trace inclusion proof support, not for the correctness proof
- of refinement mappings!
- Note: Everything is superseded by LiveIOA.thy! *)
+definition is_fair_ref_map ::
+ "('s1 \<Rightarrow> 's2) \<Rightarrow> ('a, 's1) ioa \<Rightarrow> ('a, 's2) ioa \<Rightarrow> bool"
+ where "is_fair_ref_map f C A \<longleftrightarrow>
+ is_ref_map f C A \<and> (\<forall>ex \<in> executions C. fair_ex C ex \<longrightarrow> fair_ex A (corresp_ex A f ex))"
+
+text \<open>
+ Axioms for fair trace inclusion proof support, not for the correctness proof
+ of refinement mappings!
+
+ Note: Everything is superseded by @{file "LiveIOA.thy"}.
+\<close>
axiomatization where
-corresp_laststate:
- "Finite ex ==> laststate (corresp_ex A f (s,ex)) = f (laststate (s,ex))"
+ corresp_laststate:
+ "Finite ex \<Longrightarrow> laststate (corresp_ex A f (s, ex)) = f (laststate (s, ex))"
+
+axiomatization where
+ corresp_Finite: "Finite (snd (corresp_ex A f (s, ex))) = Finite ex"
axiomatization where
-corresp_Finite:
- "Finite (snd (corresp_ex A f (s,ex))) = Finite ex"
+ FromAtoC:
+ "fin_often (\<lambda>x. P (snd x)) (snd (corresp_ex A f (s, ex))) \<Longrightarrow>
+ fin_often (\<lambda>y. P (f (snd y))) ex"
axiomatization where
-FromAtoC:
- "fin_often (%x. P (snd x)) (snd (corresp_ex A f (s,ex))) ==> fin_often (%y. P (f (snd y))) ex"
-
-axiomatization where
-FromCtoA:
- "inf_often (%y. P (fst y)) ex ==> inf_often (%x. P (fst x)) (snd (corresp_ex A f (s,ex)))"
+ FromCtoA:
+ "inf_often (\<lambda>y. P (fst y)) ex \<Longrightarrow>
+ inf_often (\<lambda>x. P (fst x)) (snd (corresp_ex A f (s,ex)))"
-(* Proof by case on inf W in ex: If so, ok. If not, only fin W in ex, ie there is
- an index i from which on no W in ex. But W inf enabled, ie at least once after i
- W is enabled. As W does not occur after i and W is enabling_persistent, W keeps
- enabled until infinity, ie. indefinitely *)
-axiomatization where
-persistent:
- "[|inf_often (%x. Enabled A W (snd x)) ex; en_persistent A W|]
- ==> inf_often (%x. fst x :W) ex | fin_often (%x. ~Enabled A W (snd x)) ex"
+text \<open>
+ Proof by case on \<open>inf W\<close> in ex: If so, ok. If not, only \<open>fin W\<close> in ex, ie.
+ there is an index \<open>i\<close> from which on no \<open>W\<close> in ex. But \<open>W\<close> inf enabled, ie at
+ least once after \<open>i\<close> \<open>W\<close> is enabled. As \<open>W\<close> does not occur after \<open>i\<close> and \<open>W\<close>
+ is \<open>enabling_persistent\<close>, \<open>W\<close> keeps enabled until infinity, ie. indefinitely
+\<close>
axiomatization where
-infpostcond:
- "[| is_exec_frag A (s,ex); inf_often (%x. fst x:W) ex|]
- ==> inf_often (% x. set_was_enabled A W (snd x)) ex"
+ persistent:
+ "inf_often (\<lambda>x. Enabled A W (snd x)) ex \<Longrightarrow> en_persistent A W \<Longrightarrow>
+ inf_often (\<lambda>x. fst x \<in> W) ex \<or> fin_often (\<lambda>x. \<not> Enabled A W (snd x)) ex"
+
+axiomatization where
+ infpostcond:
+ "is_exec_frag A (s,ex) \<Longrightarrow> inf_often (\<lambda>x. fst x \<in> W) ex \<Longrightarrow>
+ inf_often (\<lambda>x. set_was_enabled A W (snd x)) ex"
-subsection "corresp_ex"
+subsection \<open>\<open>corresp_ex\<close>\<close>
-lemma corresp_exC_unfold: "corresp_exC A f = (LAM ex. (%s. case ex of
- nil => nil
- | x##xs => (flift1 (%pr. (@cex. move A cex (f s) (fst pr) (f (snd pr)))
- @@ ((corresp_exC A f $xs) (snd pr)))
- $x) ))"
-apply (rule trans)
-apply (rule fix_eq2)
-apply (simp only: corresp_exC_def)
-apply (rule beta_cfun)
-apply (simp add: flift1_def)
-done
+lemma corresp_exC_unfold:
+ "corresp_exC A f =
+ (LAM ex.
+ (\<lambda>s.
+ case ex of
+ nil \<Rightarrow> nil
+ | x ## xs \<Rightarrow>
+ (flift1 (\<lambda>pr.
+ (SOME cex. move A cex (f s) (fst pr) (f (snd pr))) @@
+ ((corresp_exC A f $ xs) (snd pr))) $ x)))"
+ apply (rule trans)
+ apply (rule fix_eq2)
+ apply (simp only: corresp_exC_def)
+ apply (rule beta_cfun)
+ apply (simp add: flift1_def)
+ done
-lemma corresp_exC_UU: "(corresp_exC A f$UU) s=UU"
-apply (subst corresp_exC_unfold)
-apply simp
-done
+lemma corresp_exC_UU: "(corresp_exC A f $ UU) s = UU"
+ apply (subst corresp_exC_unfold)
+ apply simp
+ done
-lemma corresp_exC_nil: "(corresp_exC A f$nil) s = nil"
-apply (subst corresp_exC_unfold)
-apply simp
-done
+lemma corresp_exC_nil: "(corresp_exC A f $ nil) s = nil"
+ apply (subst corresp_exC_unfold)
+ apply simp
+ done
-lemma corresp_exC_cons: "(corresp_exC A f$(at\<leadsto>xs)) s =
- (@cex. move A cex (f s) (fst at) (f (snd at)))
- @@ ((corresp_exC A f$xs) (snd at))"
-apply (rule trans)
-apply (subst corresp_exC_unfold)
-apply (simp add: Consq_def flift1_def)
-apply simp
-done
-
+lemma corresp_exC_cons:
+ "(corresp_exC A f $ (at \<leadsto> xs)) s =
+ (SOME cex. move A cex (f s) (fst at) (f (snd at))) @@
+ ((corresp_exC A f $ xs) (snd at))"
+ apply (rule trans)
+ apply (subst corresp_exC_unfold)
+ apply (simp add: Consq_def flift1_def)
+ apply simp
+ done
declare corresp_exC_UU [simp] corresp_exC_nil [simp] corresp_exC_cons [simp]
-
-subsection "properties of move"
+subsection \<open>Properties of move\<close>
lemma move_is_move:
- "[|is_ref_map f C A; reachable C s; (s,a,t):trans_of C|] ==>
- move A (@x. move A x (f s) a (f t)) (f s) a (f t)"
-apply (unfold is_ref_map_def)
-apply (subgoal_tac "? ex. move A ex (f s) a (f t) ")
-prefer 2
-apply simp
-apply (erule exE)
-apply (rule someI)
-apply assumption
-done
+ "is_ref_map f C A \<Longrightarrow> reachable C s \<Longrightarrow> (s, a, t) \<in> trans_of C \<Longrightarrow>
+ move A (SOME x. move A x (f s) a (f t)) (f s) a (f t)"
+ apply (unfold is_ref_map_def)
+ apply (subgoal_tac "\<exists>ex. move A ex (f s) a (f t) ")
+ prefer 2
+ apply simp
+ apply (erule exE)
+ apply (rule someI)
+ apply assumption
+ done
lemma move_subprop1:
- "[|is_ref_map f C A; reachable C s; (s,a,t):trans_of C|] ==>
- is_exec_frag A (f s,@x. move A x (f s) a (f t))"
-apply (cut_tac move_is_move)
-defer
-apply assumption+
-apply (simp add: move_def)
-done
+ "is_ref_map f C A \<Longrightarrow> reachable C s \<Longrightarrow> (s, a, t) \<in> trans_of C \<Longrightarrow>
+ is_exec_frag A (f s, SOME x. move A x (f s) a (f t))"
+ apply (cut_tac move_is_move)
+ defer
+ apply assumption+
+ apply (simp add: move_def)
+ done
lemma move_subprop2:
- "[|is_ref_map f C A; reachable C s; (s,a,t):trans_of C|] ==>
- Finite ((@x. move A x (f s) a (f t)))"
-apply (cut_tac move_is_move)
-defer
-apply assumption+
-apply (simp add: move_def)
-done
+ "is_ref_map f C A \<Longrightarrow> reachable C s \<Longrightarrow> (s, a, t) \<in> trans_of C \<Longrightarrow>
+ Finite ((SOME x. move A x (f s) a (f t)))"
+ apply (cut_tac move_is_move)
+ defer
+ apply assumption+
+ apply (simp add: move_def)
+ done
lemma move_subprop3:
- "[|is_ref_map f C A; reachable C s; (s,a,t):trans_of C|] ==>
+ "is_ref_map f C A \<Longrightarrow> reachable C s \<Longrightarrow> (s, a, t) \<in> trans_of C \<Longrightarrow>
laststate (f s,@x. move A x (f s) a (f t)) = (f t)"
-apply (cut_tac move_is_move)
-defer
-apply assumption+
-apply (simp add: move_def)
-done
+ apply (cut_tac move_is_move)
+ defer
+ apply assumption+
+ apply (simp add: move_def)
+ done
lemma move_subprop4:
- "[|is_ref_map f C A; reachable C s; (s,a,t):trans_of C|] ==>
- mk_trace A$((@x. move A x (f s) a (f t))) =
- (if a:ext A then a\<leadsto>nil else nil)"
-apply (cut_tac move_is_move)
-defer
-apply assumption+
-apply (simp add: move_def)
-done
+ "is_ref_map f C A \<Longrightarrow> reachable C s \<Longrightarrow> (s, a, t) \<in> trans_of C \<Longrightarrow>
+ mk_trace A $ ((SOME x. move A x (f s) a (f t))) =
+ (if a \<in> ext A then a \<leadsto> nil else nil)"
+ apply (cut_tac move_is_move)
+ defer
+ apply assumption+
+ apply (simp add: move_def)
+ done
-(* ------------------------------------------------------------------ *)
-(* The following lemmata contribute to *)
-(* TRACE INCLUSION Part 1: Traces coincide *)
-(* ------------------------------------------------------------------ *)
+subsection \<open>TRACE INCLUSION Part 1: Traces coincide\<close>
-section "Lemmata for <=="
+subsubsection \<open>Lemmata for \<open>\<Longleftarrow>\<close>\<close>
-(* --------------------------------------------------- *)
-(* Lemma 1.1: Distribution of mk_trace and @@ *)
-(* --------------------------------------------------- *)
+text \<open>Lemma 1.1: Distribution of \<open>mk_trace\<close> and \<open>@@\<close>\<close>
-lemma mk_traceConc: "mk_trace C$(ex1 @@ ex2)= (mk_trace C$ex1) @@ (mk_trace C$ex2)"
-apply (simp add: mk_trace_def filter_act_def MapConc)
-done
+lemma mk_traceConc:
+ "mk_trace C $ (ex1 @@ ex2) = (mk_trace C $ ex1) @@ (mk_trace C $ ex2)"
+ by (simp add: mk_trace_def filter_act_def MapConc)
-
-(* ------------------------------------------------------
- Lemma 1 :Traces coincide
- ------------------------------------------------------- *)
-declare split_if [split del]
+text \<open>Lemma 1 : Traces coincide\<close>
lemma lemma_1:
- "[|is_ref_map f C A; ext C = ext A|] ==>
- !s. reachable C s & is_exec_frag C (s,xs) -->
- mk_trace C$xs = mk_trace A$(snd (corresp_ex A f (s,xs)))"
-apply (unfold corresp_ex_def)
-apply (tactic \<open>pair_induct_tac @{context} "xs" [@{thm is_exec_frag_def}] 1\<close>)
-(* cons case *)
-apply (auto simp add: mk_traceConc)
-apply (frule reachable.reachable_n)
-apply assumption
-apply (auto simp add: move_subprop4 split add: split_if)
-done
-
-declare split_if [split]
-
-(* ------------------------------------------------------------------ *)
-(* The following lemmata contribute to *)
-(* TRACE INCLUSION Part 2: corresp_ex is execution *)
-(* ------------------------------------------------------------------ *)
-
-section "Lemmata for ==>"
-
-(* -------------------------------------------------- *)
-(* Lemma 2.1 *)
-(* -------------------------------------------------- *)
-
-lemma lemma_2_1 [rule_format (no_asm)]:
-"Finite xs -->
- (!s .is_exec_frag A (s,xs) & is_exec_frag A (t,ys) &
- t = laststate (s,xs)
- --> is_exec_frag A (s,xs @@ ys))"
-
-apply (rule impI)
-apply (tactic \<open>Seq_Finite_induct_tac @{context} 1\<close>)
-(* main case *)
-apply (auto simp add: split_paired_all)
-done
+ "is_ref_map f C A \<Longrightarrow> ext C = ext A \<Longrightarrow>
+ \<forall>s. reachable C s \<and> is_exec_frag C (s, xs) \<longrightarrow>
+ mk_trace C $ xs = mk_trace A $ (snd (corresp_ex A f (s, xs)))"
+ supply split_if [split del]
+ apply (unfold corresp_ex_def)
+ apply (tactic \<open>pair_induct_tac @{context} "xs" [@{thm is_exec_frag_def}] 1\<close>)
+ text \<open>cons case\<close>
+ apply (auto simp add: mk_traceConc)
+ apply (frule reachable.reachable_n)
+ apply assumption
+ apply (auto simp add: move_subprop4 split add: split_if)
+ done
-(* ----------------------------------------------------------- *)
-(* Lemma 2 : corresp_ex is execution *)
-(* ----------------------------------------------------------- *)
+subsection \<open>TRACE INCLUSION Part 2: corresp_ex is execution\<close>
+
+subsubsection \<open>Lemmata for \<open>==>\<close>\<close>
+
+text \<open>Lemma 2.1\<close>
+
+lemma lemma_2_1 [rule_format]:
+ "Finite xs \<longrightarrow>
+ (\<forall>s. is_exec_frag A (s, xs) \<and> is_exec_frag A (t, ys) \<and>
+ t = laststate (s, xs) \<longrightarrow> is_exec_frag A (s, xs @@ ys))"
+ apply (rule impI)
+ apply (tactic \<open>Seq_Finite_induct_tac @{context} 1\<close>)
+ text \<open>main case\<close>
+ apply (auto simp add: split_paired_all)
+ done
+text \<open>Lemma 2 : \<open>corresp_ex\<close> is execution\<close>
lemma lemma_2:
- "[| is_ref_map f C A |] ==>
- !s. reachable C s & is_exec_frag C (s,xs)
- --> is_exec_frag A (corresp_ex A f (s,xs))"
+ "is_ref_map f C A \<Longrightarrow>
+ \<forall>s. reachable C s \<and> is_exec_frag C (s, xs) \<longrightarrow>
+ is_exec_frag A (corresp_ex A f (s, xs))"
+ apply (unfold corresp_ex_def)
-apply (unfold corresp_ex_def)
+ apply simp
+ apply (tactic \<open>pair_induct_tac @{context} "xs" [@{thm is_exec_frag_def}] 1\<close>)
-apply simp
-apply (tactic \<open>pair_induct_tac @{context} "xs" [@{thm is_exec_frag_def}] 1\<close>)
-(* main case *)
-apply auto
-apply (rule_tac t = "f x2" in lemma_2_1)
+ text \<open>main case\<close>
+ apply auto
+ apply (rule_tac t = "f x2" in lemma_2_1)
-(* Finite *)
-apply (erule move_subprop2)
-apply assumption+
-apply (rule conjI)
+ text \<open>\<open>Finite\<close>\<close>
+ apply (erule move_subprop2)
+ apply assumption+
+ apply (rule conjI)
-(* is_exec_frag *)
-apply (erule move_subprop1)
-apply assumption+
-apply (rule conjI)
+ text \<open>\<open>is_exec_frag\<close>\<close>
+ apply (erule move_subprop1)
+ apply assumption+
+ apply (rule conjI)
-(* Induction hypothesis *)
-(* reachable_n looping, therefore apply it manually *)
-apply (erule_tac x = "x2" in allE)
-apply simp
-apply (frule reachable.reachable_n)
-apply assumption
-apply simp
-(* laststate *)
-apply (erule move_subprop3 [symmetric])
-apply assumption+
-done
+ text \<open>Induction hypothesis\<close>
+ text \<open>\<open>reachable_n\<close> looping, therefore apply it manually\<close>
+ apply (erule_tac x = "x2" in allE)
+ apply simp
+ apply (frule reachable.reachable_n)
+ apply assumption
+ apply simp
+
+ text \<open>\<open>laststate\<close>\<close>
+ apply (erule move_subprop3 [symmetric])
+ apply assumption+
+ done
-subsection "Main Theorem: TRACE - INCLUSION"
+subsection \<open>Main Theorem: TRACE -- INCLUSION\<close>
-lemma trace_inclusion:
- "[| ext C = ext A; is_ref_map f C A |]
- ==> traces C <= traces A"
+theorem trace_inclusion:
+ "ext C = ext A \<Longrightarrow> is_ref_map f C A \<Longrightarrow> traces C \<subseteq> traces A"
apply (unfold traces_def)
- apply (simp (no_asm) add: has_trace_def2)
+ apply (simp add: has_trace_def2)
apply auto
- (* give execution of abstract automata *)
+ text \<open>give execution of abstract automata\<close>
apply (rule_tac x = "corresp_ex A f ex" in bexI)
- (* Traces coincide, Lemma 1 *)
+ text \<open>Traces coincide, Lemma 1\<close>
apply (tactic \<open>pair_tac @{context} "ex" 1\<close>)
apply (erule lemma_1 [THEN spec, THEN mp])
apply assumption+
apply (simp add: executions_def reachable.reachable_0)
- (* corresp_ex is execution, Lemma 2 *)
+ text \<open>\<open>corresp_ex\<close> is execution, Lemma 2\<close>
apply (tactic \<open>pair_tac @{context} "ex" 1\<close>)
apply (simp add: executions_def)
- (* start state *)
+ text \<open>start state\<close>
apply (rule conjI)
apply (simp add: is_ref_map_def corresp_ex_def)
- (* is-execution-fragment *)
+ text \<open>\<open>is_execution_fragment\<close>\<close>
apply (erule lemma_2 [THEN spec, THEN mp])
apply (simp add: reachable.reachable_0)
done
-subsection "Corollary: FAIR TRACE - INCLUSION"
+subsection \<open>Corollary: FAIR TRACE -- INCLUSION\<close>
lemma fininf: "(~inf_often P s) = fin_often P s"
-apply (unfold fin_often_def)
-apply auto
-done
-
+ by (auto simp: fin_often_def)
-lemma WF_alt: "is_wfair A W (s,ex) =
- (fin_often (%x. ~Enabled A W (snd x)) ex --> inf_often (%x. fst x :W) ex)"
-apply (simp add: is_wfair_def fin_often_def)
-apply auto
-done
+lemma WF_alt: "is_wfair A W (s, ex) =
+ (fin_often (\<lambda>x. \<not> Enabled A W (snd x)) ex \<longrightarrow> inf_often (\<lambda>x. fst x \<in> W) ex)"
+ by (auto simp add: is_wfair_def fin_often_def)
-lemma WF_persistent: "[|is_wfair A W (s,ex); inf_often (%x. Enabled A W (snd x)) ex;
- en_persistent A W|]
- ==> inf_often (%x. fst x :W) ex"
-apply (drule persistent)
-apply assumption
-apply (simp add: WF_alt)
-apply auto
-done
-
+lemma WF_persistent:
+ "is_wfair A W (s, ex) \<Longrightarrow> inf_often (\<lambda>x. Enabled A W (snd x)) ex \<Longrightarrow>
+ en_persistent A W \<Longrightarrow> inf_often (\<lambda>x. fst x \<in> W) ex"
+ apply (drule persistent)
+ apply assumption
+ apply (simp add: WF_alt)
+ apply auto
+ done
-lemma fair_trace_inclusion: "!! C A.
- [| is_ref_map f C A; ext C = ext A;
- !! ex. [| ex:executions C; fair_ex C ex|] ==> fair_ex A (corresp_ex A f ex) |]
- ==> fairtraces C <= fairtraces A"
-apply (simp (no_asm) add: fairtraces_def fairexecutions_def)
-apply auto
-apply (rule_tac x = "corresp_ex A f ex" in exI)
-apply auto
+lemma fair_trace_inclusion:
+ assumes "is_ref_map f C A"
+ and "ext C = ext A"
+ and "\<And>ex. ex \<in> executions C \<Longrightarrow> fair_ex C ex \<Longrightarrow>
+ fair_ex A (corresp_ex A f ex)"
+ shows "fairtraces C \<subseteq> fairtraces A"
+ apply (insert assms)
+ apply (simp add: fairtraces_def fairexecutions_def)
+ apply auto
+ apply (rule_tac x = "corresp_ex A f ex" in exI)
+ apply auto
- (* Traces coincide, Lemma 1 *)
+ text \<open>Traces coincide, Lemma 1\<close>
apply (tactic \<open>pair_tac @{context} "ex" 1\<close>)
apply (erule lemma_1 [THEN spec, THEN mp])
apply assumption+
apply (simp add: executions_def reachable.reachable_0)
- (* corresp_ex is execution, Lemma 2 *)
+ text \<open>\<open>corresp_ex\<close> is execution, Lemma 2\<close>
apply (tactic \<open>pair_tac @{context} "ex" 1\<close>)
apply (simp add: executions_def)
- (* start state *)
+ text \<open>start state\<close>
apply (rule conjI)
apply (simp add: is_ref_map_def corresp_ex_def)
- (* is-execution-fragment *)
+ text \<open>\<open>is_execution_fragment\<close>\<close>
apply (erule lemma_2 [THEN spec, THEN mp])
apply (simp add: reachable.reachable_0)
-
-done
+ done
-lemma fair_trace_inclusion2: "!! C A.
- [| inp(C) = inp(A); out(C)=out(A);
- is_fair_ref_map f C A |]
- ==> fair_implements C A"
-apply (simp add: is_fair_ref_map_def fair_implements_def fairtraces_def fairexecutions_def)
-apply auto
-apply (rule_tac x = "corresp_ex A f ex" in exI)
-apply auto
+lemma fair_trace_inclusion2:
+ "inp C = inp A \<Longrightarrow> out C = out A \<Longrightarrow> is_fair_ref_map f C A \<Longrightarrow>
+ fair_implements C A"
+ apply (simp add: is_fair_ref_map_def fair_implements_def fairtraces_def fairexecutions_def)
+ apply auto
+ apply (rule_tac x = "corresp_ex A f ex" in exI)
+ apply auto
- (* Traces coincide, Lemma 1 *)
+ text \<open>Traces coincide, Lemma 1\<close>
apply (tactic \<open>pair_tac @{context} "ex" 1\<close>)
apply (erule lemma_1 [THEN spec, THEN mp])
apply (simp (no_asm) add: externals_def)
apply (auto)[1]
apply (simp add: executions_def reachable.reachable_0)
- (* corresp_ex is execution, Lemma 2 *)
+ text \<open>\<open>corresp_ex\<close> is execution, Lemma 2\<close>
apply (tactic \<open>pair_tac @{context} "ex" 1\<close>)
apply (simp add: executions_def)
- (* start state *)
+ text \<open>start state\<close>
apply (rule conjI)
apply (simp add: is_ref_map_def corresp_ex_def)
- (* is-execution-fragment *)
+ text \<open>\<open>is_execution_fragment\<close>\<close>
apply (erule lemma_2 [THEN spec, THEN mp])
apply (simp add: reachable.reachable_0)
-
-done
+ done
end
--- a/src/HOL/HOLCF/IOA/ShortExecutions.thy Tue Jan 12 20:05:53 2016 +0100
+++ b/src/HOL/HOLCF/IOA/ShortExecutions.thy Tue Jan 12 23:40:33 2016 +0100
@@ -13,39 +13,33 @@
that has the same trace as ex, but its schedule ends with an external action.
\<close>
-definition
- oraclebuild :: "('a => bool) => 'a Seq -> 'a Seq -> 'a Seq" where
- "oraclebuild P = (fix$(LAM h s t. case t of
- nil => nil
- | x##xs =>
- (case x of
- UU => UU
- | Def y => (Takewhile (%x. \<not>P x)$s)
- @@ (y\<leadsto>(h$(TL$(Dropwhile (%x. \<not> P x)$s))$xs))
- )
- ))"
+definition oraclebuild :: "('a \<Rightarrow> bool) \<Rightarrow> 'a Seq \<rightarrow> 'a Seq \<rightarrow> 'a Seq"
+ where "oraclebuild P =
+ (fix $
+ (LAM h s t.
+ case t of
+ nil \<Rightarrow> nil
+ | x ## xs \<Rightarrow>
+ (case x of
+ UU \<Rightarrow> UU
+ | Def y \<Rightarrow>
+ (Takewhile (\<lambda>x. \<not> P x) $ s) @@
+ (y \<leadsto> (h $ (TL $ (Dropwhile (\<lambda>x. \<not> P x) $ s)) $ xs)))))"
-definition
- Cut :: "('a => bool) => 'a Seq => 'a Seq" where
- "Cut P s = oraclebuild P$s$(Filter P$s)"
+definition Cut :: "('a \<Rightarrow> bool) \<Rightarrow> 'a Seq \<Rightarrow> 'a Seq"
+ where "Cut P s = oraclebuild P $ s $ (Filter P $ s)"
-definition
- LastActExtsch :: "('a,'s)ioa => 'a Seq => bool" where
- "LastActExtsch A sch = (Cut (%x. x: ext A) sch = sch)"
-
-(* LastActExtex ::"('a,'s)ioa => ('a,'s) pairs => bool"*)
-(* LastActExtex_def:
- "LastActExtex A ex == LastActExtsch A (filter_act$ex)" *)
+definition LastActExtsch :: "('a,'s) ioa \<Rightarrow> 'a Seq \<Rightarrow> bool"
+ where "LastActExtsch A sch \<longleftrightarrow> Cut (\<lambda>x. x \<in> ext A) sch = sch"
axiomatization where
- Cut_prefixcl_Finite: "Finite s ==> (? y. s = Cut P s @@ y)"
+ Cut_prefixcl_Finite: "Finite s \<Longrightarrow> \<exists>y. s = Cut P s @@ y"
axiomatization where
- LastActExtsmall1: "LastActExtsch A sch ==> LastActExtsch A (TL$(Dropwhile P$sch))"
+ LastActExtsmall1: "LastActExtsch A sch \<Longrightarrow> LastActExtsch A (TL $ (Dropwhile P $ sch))"
axiomatization where
- LastActExtsmall2: "[| Finite sch1; LastActExtsch A (sch1 @@ sch2) |] ==> LastActExtsch A sch2"
-
+ LastActExtsmall2: "Finite sch1 \<Longrightarrow> LastActExtsch A (sch1 @@ sch2) \<Longrightarrow> LastActExtsch A sch2"
ML \<open>
fun thin_tac' ctxt j =
@@ -55,224 +49,209 @@
\<close>
-subsection "oraclebuild rewrite rules"
-
+subsection \<open>\<open>oraclebuild\<close> rewrite rules\<close>
lemma oraclebuild_unfold:
-"oraclebuild P = (LAM s t. case t of
- nil => nil
- | x##xs =>
- (case x of
- UU => UU
- | Def y => (Takewhile (%a. \<not> P a)$s)
- @@ (y\<leadsto>(oraclebuild P$(TL$(Dropwhile (%a. \<not> P a)$s))$xs))
- )
- )"
-apply (rule trans)
-apply (rule fix_eq2)
-apply (simp only: oraclebuild_def)
-apply (rule beta_cfun)
-apply simp
-done
+ "oraclebuild P =
+ (LAM s t.
+ case t of
+ nil \<Rightarrow> nil
+ | x ## xs \<Rightarrow>
+ (case x of
+ UU \<Rightarrow> UU
+ | Def y \<Rightarrow>
+ (Takewhile (\<lambda>a. \<not> P a) $ s) @@
+ (y \<leadsto> (oraclebuild P $ (TL $ (Dropwhile (\<lambda>a. \<not> P a) $ s)) $ xs))))"
+ apply (rule trans)
+ apply (rule fix_eq2)
+ apply (simp only: oraclebuild_def)
+ apply (rule beta_cfun)
+ apply simp
+ done
-lemma oraclebuild_UU: "oraclebuild P$sch$UU = UU"
-apply (subst oraclebuild_unfold)
-apply simp
-done
+lemma oraclebuild_UU: "oraclebuild P $ sch $ UU = UU"
+ apply (subst oraclebuild_unfold)
+ apply simp
+ done
+
+lemma oraclebuild_nil: "oraclebuild P $ sch $ nil = nil"
+ apply (subst oraclebuild_unfold)
+ apply simp
+ done
-lemma oraclebuild_nil: "oraclebuild P$sch$nil = nil"
-apply (subst oraclebuild_unfold)
-apply simp
-done
-
-lemma oraclebuild_cons: "oraclebuild P$s$(x\<leadsto>t) =
- (Takewhile (%a. \<not> P a)$s)
- @@ (x\<leadsto>(oraclebuild P$(TL$(Dropwhile (%a. \<not> P a)$s))$t))"
-apply (rule trans)
-apply (subst oraclebuild_unfold)
-apply (simp add: Consq_def)
-apply (simp add: Consq_def)
-done
+lemma oraclebuild_cons:
+ "oraclebuild P $ s $ (x \<leadsto> t) =
+ (Takewhile (\<lambda>a. \<not> P a) $ s) @@
+ (x \<leadsto> (oraclebuild P $ (TL $ (Dropwhile (\<lambda>a. \<not> P a) $ s)) $ t))"
+ apply (rule trans)
+ apply (subst oraclebuild_unfold)
+ apply (simp add: Consq_def)
+ apply (simp add: Consq_def)
+ done
-subsection "Cut rewrite rules"
+subsection \<open>Cut rewrite rules\<close>
-lemma Cut_nil:
-"[| Forall (%a. \<not> P a) s; Finite s|]
- ==> Cut P s =nil"
-apply (unfold Cut_def)
-apply (subgoal_tac "Filter P$s = nil")
-apply (simp (no_asm_simp) add: oraclebuild_nil)
-apply (rule ForallQFilterPnil)
-apply assumption+
-done
+lemma Cut_nil: "Forall (\<lambda>a. \<not> P a) s \<Longrightarrow> Finite s \<Longrightarrow> Cut P s = nil"
+ apply (unfold Cut_def)
+ apply (subgoal_tac "Filter P $ s = nil")
+ apply (simp add: oraclebuild_nil)
+ apply (rule ForallQFilterPnil)
+ apply assumption+
+ done
-lemma Cut_UU:
-"[| Forall (%a. \<not> P a) s; ~Finite s|]
- ==> Cut P s =UU"
-apply (unfold Cut_def)
-apply (subgoal_tac "Filter P$s= UU")
-apply (simp (no_asm_simp) add: oraclebuild_UU)
-apply (rule ForallQFilterPUU)
-apply assumption+
-done
+lemma Cut_UU: "Forall (\<lambda>a. \<not> P a) s \<Longrightarrow> \<not> Finite s \<Longrightarrow> Cut P s = UU"
+ apply (unfold Cut_def)
+ apply (subgoal_tac "Filter P $ s = UU")
+ apply (simp add: oraclebuild_UU)
+ apply (rule ForallQFilterPUU)
+ apply assumption+
+ done
lemma Cut_Cons:
-"[| P t; Forall (%x. \<not> P x) ss; Finite ss|]
- ==> Cut P (ss @@ (t\<leadsto> rs))
- = ss @@ (t \<leadsto> Cut P rs)"
-apply (unfold Cut_def)
-apply (simp add: ForallQFilterPnil oraclebuild_cons TakewhileConc DropwhileConc)
-done
+ "P t \<Longrightarrow> Forall (\<lambda>x. \<not> P x) ss \<Longrightarrow> Finite ss \<Longrightarrow>
+ Cut P (ss @@ (t \<leadsto> rs)) = ss @@ (t \<leadsto> Cut P rs)"
+ apply (unfold Cut_def)
+ apply (simp add: ForallQFilterPnil oraclebuild_cons TakewhileConc DropwhileConc)
+ done
-subsection "Cut lemmas for main theorem"
+subsection \<open>Cut lemmas for main theorem\<close>
-lemma FilterCut: "Filter P$s = Filter P$(Cut P s)"
-apply (rule_tac A1 = "%x. True" and Q1 = "%x. \<not> P x" and x1 = "s" in take_lemma_induct [THEN mp])
-prefer 3 apply (fast)
-apply (case_tac "Finite s")
-apply (simp add: Cut_nil ForallQFilterPnil)
-apply (simp add: Cut_UU ForallQFilterPUU)
-(* main case *)
-apply (simp add: Cut_Cons ForallQFilterPnil)
-done
-
+lemma FilterCut: "Filter P $ s = Filter P $ (Cut P s)"
+ apply (rule_tac A1 = "\<lambda>x. True" and Q1 = "\<lambda>x. \<not> P x" and x1 = "s" in take_lemma_induct [THEN mp])
+ prefer 3
+ apply fast
+ apply (case_tac "Finite s")
+ apply (simp add: Cut_nil ForallQFilterPnil)
+ apply (simp add: Cut_UU ForallQFilterPUU)
+ text \<open>main case\<close>
+ apply (simp add: Cut_Cons ForallQFilterPnil)
+ done
lemma Cut_idemp: "Cut P (Cut P s) = (Cut P s)"
-apply (rule_tac A1 = "%x. True" and Q1 = "%x. \<not> P x" and x1 = "s" in
- take_lemma_less_induct [THEN mp])
-prefer 3 apply (fast)
-apply (case_tac "Finite s")
-apply (simp add: Cut_nil ForallQFilterPnil)
-apply (simp add: Cut_UU ForallQFilterPUU)
-(* main case *)
-apply (simp add: Cut_Cons ForallQFilterPnil)
-apply (rule take_reduction)
-apply auto
-done
-
+ apply (rule_tac A1 = "\<lambda>x. True" and Q1 = "\<lambda>x. \<not> P x" and x1 = "s" in
+ take_lemma_less_induct [THEN mp])
+ prefer 3
+ apply fast
+ apply (case_tac "Finite s")
+ apply (simp add: Cut_nil ForallQFilterPnil)
+ apply (simp add: Cut_UU ForallQFilterPUU)
+ text \<open>main case\<close>
+ apply (simp add: Cut_Cons ForallQFilterPnil)
+ apply (rule take_reduction)
+ apply auto
+ done
lemma MapCut: "Map f$(Cut (P \<circ> f) s) = Cut P (Map f$s)"
-apply (rule_tac A1 = "%x. True" and Q1 = "%x. \<not> P (f x) " and x1 = "s" in
- take_lemma_less_induct [THEN mp])
-prefer 3 apply (fast)
-apply (case_tac "Finite s")
-apply (simp add: Cut_nil)
-apply (rule Cut_nil [symmetric])
-apply (simp add: ForallMap o_def)
-apply (simp add: Map2Finite)
-(* csae ~ Finite s *)
-apply (simp add: Cut_UU)
-apply (rule Cut_UU)
-apply (simp add: ForallMap o_def)
-apply (simp add: Map2Finite)
-(* main case *)
-apply (simp add: Cut_Cons MapConc ForallMap FiniteMap1 o_def)
-apply (rule take_reduction)
-apply auto
-done
-
+ apply (rule_tac A1 = "\<lambda>x. True" and Q1 = "\<lambda>x. \<not> P (f x) " and x1 = "s" in
+ take_lemma_less_induct [THEN mp])
+ prefer 3
+ apply fast
+ apply (case_tac "Finite s")
+ apply (simp add: Cut_nil)
+ apply (rule Cut_nil [symmetric])
+ apply (simp add: ForallMap o_def)
+ apply (simp add: Map2Finite)
+ text \<open>case \<open>\<not> Finite s\<close>\<close>
+ apply (simp add: Cut_UU)
+ apply (rule Cut_UU)
+ apply (simp add: ForallMap o_def)
+ apply (simp add: Map2Finite)
+ text \<open>main case\<close>
+ apply (simp add: Cut_Cons MapConc ForallMap FiniteMap1 o_def)
+ apply (rule take_reduction)
+ apply auto
+ done
-lemma Cut_prefixcl_nFinite [rule_format (no_asm)]: "~Finite s --> Cut P s << s"
-apply (intro strip)
-apply (rule take_lemma_less [THEN iffD1])
-apply (intro strip)
-apply (rule mp)
-prefer 2 apply (assumption)
-apply (tactic "thin_tac' @{context} 1 1")
-apply (rule_tac x = "s" in spec)
-apply (rule nat_less_induct)
-apply (intro strip)
-apply (rename_tac na n s)
-apply (case_tac "Forall (%x. ~ P x) s")
-apply (rule take_lemma_less [THEN iffD2, THEN spec])
-apply (simp add: Cut_UU)
-(* main case *)
-apply (drule divide_Seq3)
-apply (erule exE)+
-apply (erule conjE)+
-apply hypsubst
-apply (simp add: Cut_Cons)
-apply (rule take_reduction_less)
-(* auto makes also reasoning about Finiteness of parts of s ! *)
-apply auto
-done
+lemma Cut_prefixcl_nFinite [rule_format]: "\<not> Finite s \<longrightarrow> Cut P s \<sqsubseteq> s"
+ apply (intro strip)
+ apply (rule take_lemma_less [THEN iffD1])
+ apply (intro strip)
+ apply (rule mp)
+ prefer 2
+ apply assumption
+ apply (tactic "thin_tac' @{context} 1 1")
+ apply (rule_tac x = "s" in spec)
+ apply (rule nat_less_induct)
+ apply (intro strip)
+ apply (rename_tac na n s)
+ apply (case_tac "Forall (\<lambda>x. \<not> P x) s")
+ apply (rule take_lemma_less [THEN iffD2, THEN spec])
+ apply (simp add: Cut_UU)
+ text \<open>main case\<close>
+ apply (drule divide_Seq3)
+ apply (erule exE)+
+ apply (erule conjE)+
+ apply hypsubst
+ apply (simp add: Cut_Cons)
+ apply (rule take_reduction_less)
+ text \<open>auto makes also reasoning about Finiteness of parts of \<open>s\<close>!\<close>
+ apply auto
+ done
-
-lemma execThruCut: "!!ex .is_exec_frag A (s,ex) ==> is_exec_frag A (s,Cut P ex)"
-apply (case_tac "Finite ex")
-apply (cut_tac s = "ex" and P = "P" in Cut_prefixcl_Finite)
-apply assumption
-apply (erule exE)
-apply (rule exec_prefix2closed)
-apply (erule_tac s = "ex" and t = "Cut P ex @@ y" in subst)
-apply assumption
-apply (erule exec_prefixclosed)
-apply (erule Cut_prefixcl_nFinite)
-done
+lemma execThruCut: "is_exec_frag A (s, ex) \<Longrightarrow> is_exec_frag A (s, Cut P ex)"
+ apply (case_tac "Finite ex")
+ apply (cut_tac s = "ex" and P = "P" in Cut_prefixcl_Finite)
+ apply assumption
+ apply (erule exE)
+ apply (rule exec_prefix2closed)
+ apply (erule_tac s = "ex" and t = "Cut P ex @@ y" in subst)
+ apply assumption
+ apply (erule exec_prefixclosed)
+ apply (erule Cut_prefixcl_nFinite)
+ done
-subsection "Main Cut Theorem"
+subsection \<open>Main Cut Theorem\<close>
lemma exists_LastActExtsch:
- "[|sch : schedules A ; tr = Filter (%a. a:ext A)$sch|]
- ==> ? sch. sch : schedules A &
- tr = Filter (%a. a:ext A)$sch &
- LastActExtsch A sch"
-
-apply (unfold schedules_def has_schedule_def [abs_def])
-apply auto
-apply (rule_tac x = "filter_act$ (Cut (%a. fst a:ext A) (snd ex))" in exI)
-apply (simp add: executions_def)
-apply (tactic \<open>pair_tac @{context} "ex" 1\<close>)
-apply auto
-apply (rule_tac x = " (x1,Cut (%a. fst a:ext A) x2) " in exI)
-apply (simp (no_asm_simp))
-
-(* Subgoal 1: Lemma: propagation of execution through Cut *)
+ "sch \<in> schedules A \<Longrightarrow> tr = Filter (\<lambda>a. a \<in> ext A) $ sch \<Longrightarrow>
+ \<exists>sch. sch \<in> schedules A \<and> tr = Filter (\<lambda>a. a \<in> ext A) $ sch \<and> LastActExtsch A sch"
+ apply (unfold schedules_def has_schedule_def [abs_def])
+ apply auto
+ apply (rule_tac x = "filter_act $ (Cut (\<lambda>a. fst a \<in> ext A) (snd ex))" in exI)
+ apply (simp add: executions_def)
+ apply (tactic \<open>pair_tac @{context} "ex" 1\<close>)
+ apply auto
+ apply (rule_tac x = "(x1, Cut (\<lambda>a. fst a \<in> ext A) x2)" in exI)
+ apply simp
-apply (simp add: execThruCut)
-
-(* Subgoal 2: Lemma: Filter P s = Filter P (Cut P s) *)
-
-apply (simp (no_asm) add: filter_act_def)
-apply (subgoal_tac "Map fst$ (Cut (%a. fst a: ext A) x2) = Cut (%a. a:ext A) (Map fst$x2) ")
+ text \<open>Subgoal 1: Lemma: propagation of execution through \<open>Cut\<close>\<close>
+ apply (simp add: execThruCut)
-apply (rule_tac [2] MapCut [unfolded o_def])
-apply (simp add: FilterCut [symmetric])
-
-(* Subgoal 3: Lemma: Cut idempotent *)
+ text \<open>Subgoal 2: Lemma: \<open>Filter P s = Filter P (Cut P s)\<close>\<close>
+ apply (simp add: filter_act_def)
+ apply (subgoal_tac "Map fst $ (Cut (\<lambda>a. fst a \<in> ext A) x2) = Cut (\<lambda>a. a \<in> ext A) (Map fst $ x2)")
+ apply (rule_tac [2] MapCut [unfolded o_def])
+ apply (simp add: FilterCut [symmetric])
-apply (simp (no_asm) add: LastActExtsch_def filter_act_def)
-apply (subgoal_tac "Map fst$ (Cut (%a. fst a: ext A) x2) = Cut (%a. a:ext A) (Map fst$x2) ")
-apply (rule_tac [2] MapCut [unfolded o_def])
-apply (simp add: Cut_idemp)
-done
+ text \<open>Subgoal 3: Lemma: \<open>Cut\<close> idempotent\<close>
+ apply (simp add: LastActExtsch_def filter_act_def)
+ apply (subgoal_tac "Map fst $ (Cut (\<lambda>a. fst a \<in> ext A) x2) = Cut (\<lambda>a. a \<in> ext A) (Map fst $ x2)")
+ apply (rule_tac [2] MapCut [unfolded o_def])
+ apply (simp add: Cut_idemp)
+ done
-subsection "Further Cut lemmas"
+subsection \<open>Further Cut lemmas\<close>
-lemma LastActExtimplnil:
- "[| LastActExtsch A sch; Filter (%x. x:ext A)$sch = nil |]
- ==> sch=nil"
-apply (unfold LastActExtsch_def)
-apply (drule FilternPnilForallP)
-apply (erule conjE)
-apply (drule Cut_nil)
-apply assumption
-apply simp
-done
+lemma LastActExtimplnil: "LastActExtsch A sch \<Longrightarrow> Filter (\<lambda>x. x \<in> ext A) $ sch = nil \<Longrightarrow> sch = nil"
+ apply (unfold LastActExtsch_def)
+ apply (drule FilternPnilForallP)
+ apply (erule conjE)
+ apply (drule Cut_nil)
+ apply assumption
+ apply simp
+ done
-lemma LastActExtimplUU:
- "[| LastActExtsch A sch; Filter (%x. x:ext A)$sch = UU |]
- ==> sch=UU"
-apply (unfold LastActExtsch_def)
-apply (drule FilternPUUForallP)
-apply (erule conjE)
-apply (drule Cut_UU)
-apply assumption
-apply simp
-done
+lemma LastActExtimplUU: "LastActExtsch A sch \<Longrightarrow> Filter (\<lambda>x. x \<in> ext A) $ sch = UU \<Longrightarrow> sch = UU"
+ apply (unfold LastActExtsch_def)
+ apply (drule FilternPUUForallP)
+ apply (erule conjE)
+ apply (drule Cut_UU)
+ apply assumption
+ apply simp
+ done
end