--- 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