1(*
2 *
3 * Copyright 2017, Data61, CSIRO
4 *
5 * This software may be distributed and modified according to the terms of
6 * the BSD 2-Clause license. Note that NO WARRANTY is provided.
7 * See "LICENSE_BSD2.txt" for details.
8 *
9 * @TAG(DATA61_BSD)
10 *)
11
12theory Corres_Adjust_Preconds
13
14imports
15  "Corres_UL"
16
17begin
18
19text {*
20Gadget for adjusting preconditions in a corres rule or similar.
21
22Probably only useful for predicates with two or more related
23preconditions, such as corres.
24
25Used to do some_corres_rule[adj_corres some_intro_rule],
26given e.g. some_intro_rule: @{prop "(s, t) \<in> sr \<Longrightarrow> P s \<Longrightarrow> Q t"}
27Will apply this rule to solve @{prop "Q t"} components in either
28precondition or any sub-conjunct, and will then try to put the
29assumptions @{prop "P s"}, @{prop "(s, t) \<in> sr"} into the right
30places. The premises of the rule can be in any given order.
31
32Concrete example at the bottom.
33*}
34
35named_theorems corres_adjust_precond_structures
36
37locale corres_adjust_preconds begin
38
39text {* Worker predicates. Broadly speaking, a goal
40of the form "preconds ?A ?B ?C ?D ==> P" expects to
41establish P by instantiating ?A, or failing that ?B,
42etc.
43
44A goal of the form finalise_preconds A exists to
45make sure that schematic conjuncts of A are resolved
46to True. *}
47definition
48  preconds :: "bool \<Rightarrow> bool \<Rightarrow> bool \<Rightarrow> bool \<Rightarrow> bool"
49where
50  "preconds A B C D = (A \<and> B \<and> C \<and> D)"
51
52definition
53  finalise_preconds :: "bool \<Rightarrow> bool"
54where
55  "finalise_preconds A = True"
56
57text {* Use a precond directly to establish goal. *}
58lemma consume_preconds:
59  "preconds A True True True \<Longrightarrow> A"
60  "preconds True B True True \<Longrightarrow> B"
61  "preconds True True C True \<Longrightarrow> C"
62  "preconds True True True D \<Longrightarrow> D"
63  by (simp_all add: preconds_def)
64
65lemmas consume_preconds_True = consume_preconds(1)[where A=True]
66
67text {* For use as a drule, split a set of schematic preconds
68to give two sets that can be instantiated separately. *}
69lemma split_preconds_left:
70  "preconds (A \<and> A') (B \<and> B') (C \<and> C') (D \<and> D') \<Longrightarrow> preconds A B C D"
71  "preconds (A \<and> A') (B \<and> B') (C \<and> C') True \<Longrightarrow> preconds A B C True"
72  "preconds (A \<and> A') (B \<and> B') True True \<Longrightarrow> preconds A B True True"
73  "preconds (A \<and> A') True True True \<Longrightarrow> preconds A True True True"
74  by (simp_all add: preconds_def)
75
76lemma split_preconds_right:
77  "preconds (A \<and> A') (B \<and> B') (C \<and> C') (D \<and> D') \<Longrightarrow> preconds A' B' C' D'"
78  "preconds (A \<and> A') (B \<and> B') (C \<and> C') True \<Longrightarrow> preconds A' B' C' True"
79  "preconds (A \<and> A') (B \<and> B') True True \<Longrightarrow> preconds A' B' True True"
80  "preconds (A \<and> A') True True True \<Longrightarrow> preconds A' True True True"
81  by (simp_all add: preconds_def)
82
83text {* For use as an erule. Initiate the precond process,
84creating a finalise goal to be solved later. *}
85lemma preconds_goal_initiate:
86  "preconds A B C D \<Longrightarrow> (preconds A B C D \<Longrightarrow> Q)
87    \<Longrightarrow> finalise_preconds (A \<and> B \<and> C \<and> D) \<Longrightarrow> Q"
88  by simp
89
90text {* Finalise preconds, trying to replace conjuncts with
91True if they are not yet instantiated. *}
92lemma finalise_preconds:
93  "finalise_preconds True"
94  "finalise_preconds A \<Longrightarrow> finalise_preconds B \<Longrightarrow> finalise_preconds (A \<and> B)"
95  "finalise_preconds X"
96  by (simp_all add: finalise_preconds_def)
97
98text {* Shape of the whole process for application to regular corres goals. *}
99lemma corres_adjust_pre:
100  "corres_underlying R nf nf' rs P Q  f f'
101    \<Longrightarrow> (\<And>s s'. (s, s') \<in> R \<Longrightarrow> preconds (P1 s) (Q1 s') True True \<Longrightarrow> P s)
102    \<Longrightarrow> (\<And>s s'. (s, s') \<in> R \<Longrightarrow> preconds (Q2 s') (P2 s) True True \<Longrightarrow> Q s')
103    \<Longrightarrow> corres_underlying R nf nf' rs (\<lambda>s. P1 s \<and> P2 s) (\<lambda>s'. Q1 s' \<and> Q2 s') f f'"
104  apply (erule stronger_corres_guard_imp)
105   apply (simp add: preconds_def)+
106  done
107
108ML {*
109
110structure Corres_Adjust_Preconds = struct
111
112val def_intros = @{thms conjI pred_conj_app[THEN iffD2]
113    bipred_conj_app[THEN fun_cong, THEN iffD2]}
114
115(* apply an intro rule, splitting preconds assumptions to
116   provide unique assumptions for each goal. *)
117fun intro_split ctxt intros i =
118  ((resolve_tac ctxt intros
119        THEN_ALL_NEW (TRY o assume_tac ctxt))
120    THEN_ALL_NEW (fn j => (EVERY (replicate (j - i) (dresolve_tac ctxt @{thms split_preconds_left} j)))
121        THEN dresolve_tac ctxt @{thms split_preconds_right} j)) i
122
123fun handle_preconds ctxt intros =
124  TRY o (eresolve_tac ctxt [@{thm preconds_goal_initiate}]
125    THEN' REPEAT_ALL_NEW (eresolve_tac ctxt @{thms consume_preconds_True}
126        ORELSE' intro_split ctxt (intros @ def_intros)
127        ORELSE' eresolve_tac ctxt @{thms consume_preconds})
128    THEN' REPEAT_ALL_NEW (resolve_tac ctxt @{thms finalise_preconds})
129  )
130
131fun mk_adj_preconds ctxt intros rule = let
132    val xs = [rule] RL (Named_Theorems.get ctxt @{named_theorems corres_adjust_precond_structures})
133    val x = case xs of
134        [] => raise THM ("no unifier with corres_adjust_precond_structures", 1, [rule])
135      | xs => hd xs
136  in x
137    |> ALLGOALS (handle_preconds ctxt intros)
138    |> Seq.hd
139    |> Simplifier.simplify (clear_simpset ctxt addsimps @{thms conj_assoc simp_thms(21-22)})
140  end
141
142val setup =
143      Attrib.setup @{binding "adj_corres"}
144          ((Attrib.thms -- Args.context)
145              >> (fn (intros, ctxt) => Thm.rule_attribute [] (K (mk_adj_preconds ctxt intros))))
146          "use argument theorems to adjust a corres theorem."
147
148end
149
150*}
151
152end
153
154declare corres_adjust_preconds.corres_adjust_pre[corres_adjust_precond_structures]
155
156setup Corres_Adjust_Preconds.setup
157
158experiment begin
159
160definition
161  test_sr :: "(nat \<times> nat) set"
162where
163  "test_sr = {(x, y). y = 2 * x}"
164
165lemma test_corres:
166  "corres_underlying test_sr nf nf' dc (\<lambda>x. x < 40) (\<lambda>y. y < 30 \<and> y = 6)
167    (modify (\<lambda>x. x + 2)) (modify (\<lambda>y. 10))"
168  by (simp add: corres_underlying_def simpler_modify_def test_sr_def)
169
170lemma test_adj_precond:
171  "(x, y) \<in> test_sr \<Longrightarrow> x = 3 \<Longrightarrow> y = 6"
172  by (simp add: test_sr_def)
173
174ML {*
175Corres_Adjust_Preconds.mk_adj_preconds @{context} [@{thm test_adj_precond}] @{thm test_corres}
176*}
177
178lemma foo_adj_corres:
179  "corres_underlying test_sr nf nf' dc (\<lambda>s. s < 40 \<and> s = 3) (\<lambda>s'. s' < 30) (modify (\<lambda>x. x + 2))
180       (modify (\<lambda>y. 10))"
181  by (rule test_corres[adj_corres test_adj_precond])
182
183text {* A more general demo of what it does. *}
184lemma
185  assumes my_corres: "corres_underlying my_sr nf nf' rvrel P Q a c"
186  assumes my_adj: "\<And>s s'. (s,s') \<in> my_sr \<Longrightarrow> P s \<Longrightarrow> Q s'"
187  shows "corres_underlying my_sr nf nf' rvrel (\<lambda>s. P s \<and> P s) (\<lambda>s'. True) a c"
188  apply (rule my_corres[adj_corres my_adj])
189  done
190
191end
192
193end
194