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