# Theory RefCorrectness

Up to index of Isabelle/HOL/HOLCF/Abortable_Linearizable_Modules

theory RefCorrectness
imports RefMappings
`(*  Title:      HOL/HOLCF/IOA/meta_theory/RefCorrectness.thy    Author:     Olaf MÃ¼ller*)header {* Correctness of Refinement Mappings in HOLCF/IOA *}theory RefCorrectnessimports RefMappingsbegindefinition  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  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)))"(* Axioms for fair trace inclusion proof support, not for the correctness proof   of refinement mappings!   Note: Everything is superseded by LiveIOA.thy! *)axiomatization wherecorresp_laststate:  "Finite ex ==> laststate (corresp_ex A f (s,ex)) = f (laststate (s,ex))"axiomatization wherecorresp_Finite:  "Finite (snd (corresp_ex A f (s,ex))) = Finite ex"axiomatization whereFromAtoC:  "fin_often (%x. P (snd x)) (snd (corresp_ex A f (s,ex))) ==> fin_often (%y. P (f (snd y))) ex"axiomatization whereFromCtoA:  "inf_often (%y. P (fst y)) ex ==> inf_often (%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 wherepersistent:  "[|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"axiomatization whereinfpostcond:  "[| is_exec_frag A (s,ex); inf_often (%x. fst x:W) ex|]    ==> inf_often (% x. set_was_enabled A W (snd x)) ex"subsection "corresp_ex"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)donelemma corresp_exC_UU: "(corresp_exC A f\$UU) s=UU"apply (subst corresp_exC_unfold)apply simpdonelemma corresp_exC_nil: "(corresp_exC A f\$nil) s = nil"apply (subst corresp_exC_unfold)apply simpdonelemma corresp_exC_cons: "(corresp_exC A f\$(at>>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 simpdonedeclare corresp_exC_UU [simp] corresp_exC_nil [simp] corresp_exC_cons [simp]subsection "properties of move"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 2apply simpapply (erule exE)apply (rule someI)apply assumptiondonelemma 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)deferapply assumption+apply (simp add: move_def)donelemma 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)deferapply assumption+apply (simp add: move_def)donelemma move_subprop3:   "[|is_ref_map f C A; reachable C s; (s,a,t):trans_of C|] ==>     laststate (f s,@x. move A x (f s) a (f t)) = (f t)"apply (cut_tac move_is_move)deferapply assumption+apply (simp add: move_def)donelemma 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>>nil else nil)"apply (cut_tac move_is_move)deferapply assumption+apply (simp add: move_def)done(* ------------------------------------------------------------------ *)(*                   The following lemmata contribute to              *)(*                 TRACE INCLUSION Part 1: Traces coincide            *)(* ------------------------------------------------------------------ *)section "Lemmata for <=="(* --------------------------------------------------- *)(*   Lemma 1.1: Distribution of mk_trace and @@        *)(* --------------------------------------------------- *)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 1 :Traces coincide   ------------------------------------------------------- *)declare split_if [split del]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 {* pair_induct_tac @{context} "xs" [@{thm is_exec_frag_def}] 1 *})(* cons case *)apply (auto simp add: mk_traceConc)apply (frule reachable.reachable_n)apply assumptionapply (erule_tac x = "y" in allE)apply (simp add: move_subprop4 split add: split_if)donedeclare 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 {* Seq_Finite_induct_tac @{context} 1 *})(* main case *)apply (auto simp add: split_paired_all)done(* ----------------------------------------------------------- *)(*               Lemma 2 : corresp_ex is execution             *)(* ----------------------------------------------------------- *)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))"apply (unfold corresp_ex_def)apply simpapply (tactic {* pair_induct_tac @{context} "xs" [@{thm is_exec_frag_def}] 1 *})(* main case *)apply autoapply (rule_tac t = "f y" in lemma_2_1)(* Finite *)apply (erule move_subprop2)apply assumption+apply (rule conjI)(* is_exec_frag *)apply (erule move_subprop1)apply assumption+apply (rule conjI)(* Induction hypothesis  *)(* reachable_n looping, therefore apply it manually *)apply (erule_tac x = "y" in allE)apply simpapply (frule reachable.reachable_n)apply assumptionapply simp(* laststate *)apply (erule move_subprop3 [symmetric])apply assumption+donesubsection "Main Theorem: TRACE - INCLUSION"lemma trace_inclusion:  "[| ext C = ext A; is_ref_map f C A |]           ==> traces C <= traces A"  apply (unfold traces_def)  apply (simp (no_asm) add: has_trace_def2)  apply auto  (* give execution of abstract automata *)  apply (rule_tac x = "corresp_ex A f ex" in bexI)  (* Traces coincide, Lemma 1 *)  apply (tactic {* pair_tac @{context} "ex" 1 *})  apply (erule lemma_1 [THEN spec, THEN mp])  apply assumption+  apply (simp add: executions_def reachable.reachable_0)  (* corresp_ex is execution, Lemma 2 *)  apply (tactic {* pair_tac @{context} "ex" 1 *})  apply (simp add: executions_def)  (* start state *)  apply (rule conjI)  apply (simp add: is_ref_map_def corresp_ex_def)  (* is-execution-fragment *)  apply (erule lemma_2 [THEN spec, THEN mp])  apply (simp add: reachable.reachable_0)  donesubsection "Corollary:  FAIR TRACE - INCLUSION"lemma fininf: "(~inf_often P s) = fin_often P s"apply (unfold fin_often_def)apply autodonelemma 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 autodonelemma 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 assumptionapply (simp add: WF_alt)apply autodonelemma 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 autoapply (rule_tac x = "corresp_ex A f ex" in exI)apply auto  (* Traces coincide, Lemma 1 *)  apply (tactic {* pair_tac @{context} "ex" 1 *})  apply (erule lemma_1 [THEN spec, THEN mp])  apply assumption+  apply (simp add: executions_def reachable.reachable_0)  (* corresp_ex is execution, Lemma 2 *)  apply (tactic {* pair_tac @{context} "ex" 1 *})  apply (simp add: executions_def)  (* start state *)  apply (rule conjI)  apply (simp add: is_ref_map_def corresp_ex_def)  (* is-execution-fragment *)  apply (erule lemma_2 [THEN spec, THEN mp])  apply (simp add: reachable.reachable_0)donelemma 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 autoapply (rule_tac x = "corresp_ex A f ex" in exI)apply auto  (* Traces coincide, Lemma 1 *)  apply (tactic {* pair_tac @{context} "ex" 1 *})  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 *)  apply (tactic {* pair_tac @{context} "ex" 1 *})  apply (simp add: executions_def)  (* start state *)  apply (rule conjI)  apply (simp add: is_ref_map_def corresp_ex_def)  (* is-execution-fragment *)  apply (erule lemma_2 [THEN spec, THEN mp])  apply (simp add: reachable.reachable_0)doneend`