1(* 2 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230) 3 * 4 * SPDX-License-Identifier: BSD-2-Clause 5 *) 6 7theory ExtraSpecs 8 9imports 10 "CLib.TypHeapLib" 11 12begin 13 14definition 15 "simple_simpl_refines \<Gamma> com com' 16 = (\<forall>s. (\<exists>ft. \<Gamma> \<turnstile> \<langle>com', Normal s\<rangle> \<Rightarrow> Fault ft) 17 \<or> ((\<forall>xs. \<Gamma> \<turnstile> \<langle>com, Normal s\<rangle> \<Rightarrow> xs \<longrightarrow> \<Gamma> \<turnstile> \<langle>com', Normal s\<rangle> \<Rightarrow> xs) 18 \<and> (\<not> terminates \<Gamma> com (Normal s) \<longrightarrow> \<not> terminates \<Gamma> com' (Normal s))))" 19 20lemma simple_simpl_refines_no_fault_execD: 21 "\<Gamma> \<turnstile> \<langle>com,Normal s\<rangle> \<Rightarrow> xs 22 \<Longrightarrow> simple_simpl_refines \<Gamma> com com' 23 \<Longrightarrow> (\<forall>ft. \<not> \<Gamma> \<turnstile> \<langle>com',Normal s\<rangle> \<Rightarrow> Fault ft) 24 \<Longrightarrow> \<Gamma> \<turnstile> \<langle>com', Normal s\<rangle> \<Rightarrow> xs" 25 by (auto simp add: simple_simpl_refines_def) 26 27lemma simple_simpl_refines_no_fault_terminatesD: 28 "simple_simpl_refines \<Gamma> com com' 29 \<Longrightarrow> (\<forall>ft. \<not> \<Gamma> \<turnstile> \<langle>com',Normal s\<rangle> \<Rightarrow> Fault ft) 30 \<Longrightarrow> \<not> terminates \<Gamma> com (Normal s) \<longrightarrow> \<not> terminates \<Gamma> com' (Normal s)" 31 by (auto simp add: simple_simpl_refines_def) 32 33lemma simple_simpl_refines_refl: 34 "simple_simpl_refines \<Gamma> com com" 35 by (auto simp add: simple_simpl_refines_def) 36 37lemma simple_simpl_refines_from_def_eq: 38 "body \<equiv> body' \<Longrightarrow> simple_simpl_refines \<Gamma> body' body" 39 (* these are flipped, because the "implementation" is on the rhs of 40 definitional equalities, but the lhs of refinement thms. *) 41 by (simp add: simple_simpl_refines_def) 42 43lemma simple_simpl_refines_trans: 44 "simple_simpl_refines \<Gamma> com com' \<Longrightarrow> simple_simpl_refines \<Gamma> com' com'' 45 \<Longrightarrow> simple_simpl_refines \<Gamma> com com''" 46 by (simp add: simple_simpl_refines_def, metis) 47 48lemma simple_simpl_refines_drop_Guard: 49 "simple_simpl_refines \<Gamma> com (Guard F G com)" 50 apply (clarsimp simp add: simple_simpl_refines_def) 51 apply (case_tac "s \<in> G") 52 apply (auto intro: exec.Guard exec.GuardFault 53 elim!: terminates_Normal_elim_cases) 54 done 55 56lemma simple_simpl_refines_guarded_Basic_guarded_spec_body: 57 "(\<forall>s s'. (s, s') \<in> R \<longrightarrow> (s \<in> G \<and> (s, f s) \<in> R)) 58 \<Longrightarrow> simple_simpl_refines \<Gamma> (Guard F' G (Basic f)) (guarded_spec_body F R)" 59 apply (simp add: guarded_spec_body_def simple_simpl_refines_def) 60 apply (intro allI, drule_tac x=s in spec) 61 apply (erule impCE) 62 apply (rule disjI1) 63 apply (fastforce intro: exec.GuardFault) 64 apply (rule disjI2) 65 apply (auto intro!: exec.Guard terminates.Guard 66 intro: exec.GuardFault exec.Spec terminates.Basic image_eqI[rotated] 67 elim!: exec_Normal_elim_cases terminates_Normal_elim_cases) 68 done 69 70lemmas simple_simpl_refines_Basic_guarded_spec_body 71 = simple_simpl_refines_trans[OF 72 simple_simpl_refines_drop_Guard[where G=UNIV] 73 simple_simpl_refines_guarded_Basic_guarded_spec_body 74 ] 75 76ML \<open> 77structure Get_Body_Refines = struct 78 79fun get ctxt name = let 80 fun pget sfx = try (Proof_Context.get_thm ctxt o suffix sfx) name 81 val eqv = pget "_body_refines" 82 val def = pget "_body_def" 83 in case (eqv, def) of 84 (SOME eqvt, _) => eqvt 85 | (_, SOME deft) => (deft RS @{thm simple_simpl_refines_from_def_eq}) 86 | _ => raise THM ("Get_Body_Refines.get: " 87 ^ "no body_def or body_refines: " ^ name, 1, []) 88 end 89 90end 91\<close> 92 93end 94