author | nipkow |
Tue, 12 Oct 2021 20:57:43 +0200 | |
changeset 74503 | 403ce50e6a2a |
parent 74375 | ba880f3a4e52 |
child 74506 | d97c48dc87fa |
permissions | -rw-r--r-- |
24475
a297ae4ff188
added Hoare/hoare_tac.ML (code from Hoare/Hoare.thy, also required in Isar_examples/Hoare.thy);
wenzelm
parents:
diff
changeset
|
1 |
(* Title: HOL/Hoare/hoare_tac.ML |
a297ae4ff188
added Hoare/hoare_tac.ML (code from Hoare/Hoare.thy, also required in Isar_examples/Hoare.thy);
wenzelm
parents:
diff
changeset
|
2 |
Author: Leonor Prensa Nieto & Tobias Nipkow |
72806
4fa08e083865
Extension of session HOL/Hoare with total correctness proof system by Walter Guttmann
nipkow
parents:
69597
diff
changeset
|
3 |
Author: Walter Guttmann (extension to total-correctness proofs) |
24475
a297ae4ff188
added Hoare/hoare_tac.ML (code from Hoare/Hoare.thy, also required in Isar_examples/Hoare.thy);
wenzelm
parents:
diff
changeset
|
4 |
|
a297ae4ff188
added Hoare/hoare_tac.ML (code from Hoare/Hoare.thy, also required in Isar_examples/Hoare.thy);
wenzelm
parents:
diff
changeset
|
5 |
Derivation of the proof rules and, most importantly, the VCG tactic. |
a297ae4ff188
added Hoare/hoare_tac.ML (code from Hoare/Hoare.thy, also required in Isar_examples/Hoare.thy);
wenzelm
parents:
diff
changeset
|
6 |
*) |
a297ae4ff188
added Hoare/hoare_tac.ML (code from Hoare/Hoare.thy, also required in Isar_examples/Hoare.thy);
wenzelm
parents:
diff
changeset
|
7 |
|
72985
9cc431444435
clarified modules: avoid multiple uses of the same ML file;
wenzelm
parents:
72806
diff
changeset
|
8 |
signature HOARE_TAC = |
55660 | 9 |
sig |
55661 | 10 |
val hoare_rule_tac: Proof.context -> term list * thm -> (int -> tactic) -> bool -> |
11 |
int -> tactic |
|
55660 | 12 |
val hoare_tac: Proof.context -> (int -> tactic) -> int -> tactic |
72806
4fa08e083865
Extension of session HOL/Hoare with total correctness proof system by Walter Guttmann
nipkow
parents:
69597
diff
changeset
|
13 |
val hoare_tc_tac: Proof.context -> (int -> tactic) -> int -> tactic |
55660 | 14 |
end; |
15 |
||
72985
9cc431444435
clarified modules: avoid multiple uses of the same ML file;
wenzelm
parents:
72806
diff
changeset
|
16 |
structure Hoare_Tac: HOARE_TAC = |
55660 | 17 |
struct |
41449 | 18 |
|
24475
a297ae4ff188
added Hoare/hoare_tac.ML (code from Hoare/Hoare.thy, also required in Isar_examples/Hoare.thy);
wenzelm
parents:
diff
changeset
|
19 |
(*** The tactics ***) |
a297ae4ff188
added Hoare/hoare_tac.ML (code from Hoare/Hoare.thy, also required in Isar_examples/Hoare.thy);
wenzelm
parents:
diff
changeset
|
20 |
|
a297ae4ff188
added Hoare/hoare_tac.ML (code from Hoare/Hoare.thy, also required in Isar_examples/Hoare.thy);
wenzelm
parents:
diff
changeset
|
21 |
(*****************************************************************************) |
a297ae4ff188
added Hoare/hoare_tac.ML (code from Hoare/Hoare.thy, also required in Isar_examples/Hoare.thy);
wenzelm
parents:
diff
changeset
|
22 |
(** The function Mset makes the theorem **) |
a297ae4ff188
added Hoare/hoare_tac.ML (code from Hoare/Hoare.thy, also required in Isar_examples/Hoare.thy);
wenzelm
parents:
diff
changeset
|
23 |
(** "?Mset <= {(x1,...,xn). ?P (x1,...,xn)} ==> ?Mset <= {s. ?P s}", **) |
a297ae4ff188
added Hoare/hoare_tac.ML (code from Hoare/Hoare.thy, also required in Isar_examples/Hoare.thy);
wenzelm
parents:
diff
changeset
|
24 |
(** where (x1,...,xn) are the variables of the particular program we are **) |
a297ae4ff188
added Hoare/hoare_tac.ML (code from Hoare/Hoare.thy, also required in Isar_examples/Hoare.thy);
wenzelm
parents:
diff
changeset
|
25 |
(** working on at the moment of the call **) |
a297ae4ff188
added Hoare/hoare_tac.ML (code from Hoare/Hoare.thy, also required in Isar_examples/Hoare.thy);
wenzelm
parents:
diff
changeset
|
26 |
(*****************************************************************************) |
a297ae4ff188
added Hoare/hoare_tac.ML (code from Hoare/Hoare.thy, also required in Isar_examples/Hoare.thy);
wenzelm
parents:
diff
changeset
|
27 |
|
41449 | 28 |
local |
24475
a297ae4ff188
added Hoare/hoare_tac.ML (code from Hoare/Hoare.thy, also required in Isar_examples/Hoare.thy);
wenzelm
parents:
diff
changeset
|
29 |
|
a297ae4ff188
added Hoare/hoare_tac.ML (code from Hoare/Hoare.thy, also required in Isar_examples/Hoare.thy);
wenzelm
parents:
diff
changeset
|
30 |
(** maps (%x1 ... xn. t) to [x1,...,xn] **) |
74304 | 31 |
fun abs2list \<^Const_>\<open>case_prod _ _ _ for \<open>Abs (x, T, t)\<close>\<close> = Free (x, T) :: abs2list t |
55659 | 32 |
| abs2list (Abs (x, T, _)) = [Free (x, T)] |
24475
a297ae4ff188
added Hoare/hoare_tac.ML (code from Hoare/Hoare.thy, also required in Isar_examples/Hoare.thy);
wenzelm
parents:
diff
changeset
|
33 |
| abs2list _ = []; |
a297ae4ff188
added Hoare/hoare_tac.ML (code from Hoare/Hoare.thy, also required in Isar_examples/Hoare.thy);
wenzelm
parents:
diff
changeset
|
34 |
|
a297ae4ff188
added Hoare/hoare_tac.ML (code from Hoare/Hoare.thy, also required in Isar_examples/Hoare.thy);
wenzelm
parents:
diff
changeset
|
35 |
(** maps {(x1,...,xn). t} to [x1,...,xn] **) |
74304 | 36 |
fun mk_vars \<^Const_>\<open>Collect _ for T\<close> = abs2list T |
24475
a297ae4ff188
added Hoare/hoare_tac.ML (code from Hoare/Hoare.thy, also required in Isar_examples/Hoare.thy);
wenzelm
parents:
diff
changeset
|
37 |
| mk_vars _ = []; |
a297ae4ff188
added Hoare/hoare_tac.ML (code from Hoare/Hoare.thy, also required in Isar_examples/Hoare.thy);
wenzelm
parents:
diff
changeset
|
38 |
|
28457
25669513fd4c
major cleanup of hoare_tac.ML: just one copy for Hoare.thy and HoareAbort.thy (only 1 line different), refrain from inspecting the main goal, proper context;
wenzelm
parents:
27330
diff
changeset
|
39 |
(** abstraction of body over a tuple formed from a list of free variables. |
24475
a297ae4ff188
added Hoare/hoare_tac.ML (code from Hoare/Hoare.thy, also required in Isar_examples/Hoare.thy);
wenzelm
parents:
diff
changeset
|
40 |
Types are also built **) |
74304 | 41 |
fun mk_abstupleC [] body = absfree ("x", \<^Type>\<open>unit\<close>) body |
44241 | 42 |
| mk_abstupleC [v] body = absfree (dest_Free v) body |
43 |
| mk_abstupleC (v :: w) body = |
|
44 |
let |
|
45 |
val (x, T) = dest_Free v; |
|
46 |
val z = mk_abstupleC w body; |
|
47 |
val T2 = |
|
48 |
(case z of |
|
49 |
Abs (_, T, _) => T |
|
50 |
| Const (_, Type (_, [_, Type (_, [T, _])])) $ _ => T); |
|
51 |
in |
|
74375 | 52 |
\<^Const>\<open>case_prod T T2 \<^Type>\<open>bool\<close> for \<open>absfree (x, T) z\<close>\<close> |
44241 | 53 |
end; |
24475
a297ae4ff188
added Hoare/hoare_tac.ML (code from Hoare/Hoare.thy, also required in Isar_examples/Hoare.thy);
wenzelm
parents:
diff
changeset
|
54 |
|
a297ae4ff188
added Hoare/hoare_tac.ML (code from Hoare/Hoare.thy, also required in Isar_examples/Hoare.thy);
wenzelm
parents:
diff
changeset
|
55 |
(** maps [x1,...,xn] to (x1,...,xn) and types**) |
74304 | 56 |
fun mk_bodyC [] = \<^Const>\<open>Unity\<close> |
55661 | 57 |
| mk_bodyC [x] = x |
58 |
| mk_bodyC (x :: xs) = |
|
59 |
let |
|
60 |
val (_, T) = dest_Free x; |
|
61 |
val z = mk_bodyC xs; |
|
62 |
val T2 = |
|
63 |
(case z of |
|
64 |
Free (_, T) => T |
|
74304 | 65 |
| \<^Const_>\<open>Pair A B for _ _\<close> => \<^Type>\<open>prod A B\<close>); |
66 |
in \<^Const>\<open>Pair T T2 for x z\<close> end; |
|
24475
a297ae4ff188
added Hoare/hoare_tac.ML (code from Hoare/Hoare.thy, also required in Isar_examples/Hoare.thy);
wenzelm
parents:
diff
changeset
|
67 |
|
28457
25669513fd4c
major cleanup of hoare_tac.ML: just one copy for Hoare.thy and HoareAbort.thy (only 1 line different), refrain from inspecting the main goal, proper context;
wenzelm
parents:
27330
diff
changeset
|
68 |
(** maps a subgoal of the form: |
55661 | 69 |
VARS x1 ... xn {._.} _ {._.} or to [x1,...,xn] |
70 |
**) |
|
28457
25669513fd4c
major cleanup of hoare_tac.ML: just one copy for Hoare.thy and HoareAbort.thy (only 1 line different), refrain from inspecting the main goal, proper context;
wenzelm
parents:
27330
diff
changeset
|
71 |
fun get_vars c = |
25669513fd4c
major cleanup of hoare_tac.ML: just one copy for Hoare.thy and HoareAbort.thy (only 1 line different), refrain from inspecting the main goal, proper context;
wenzelm
parents:
27330
diff
changeset
|
72 |
let |
25669513fd4c
major cleanup of hoare_tac.ML: just one copy for Hoare.thy and HoareAbort.thy (only 1 line different), refrain from inspecting the main goal, proper context;
wenzelm
parents:
27330
diff
changeset
|
73 |
val d = Logic.strip_assums_concl c; |
74503
403ce50e6a2a
separated commands from annotations to be able to abstract about the latter only
nipkow
parents:
74375
diff
changeset
|
74 |
val Const _ $ pre $ _ $ _ $ _ = HOLogic.dest_Trueprop d; |
28457
25669513fd4c
major cleanup of hoare_tac.ML: just one copy for Hoare.thy and HoareAbort.thy (only 1 line different), refrain from inspecting the main goal, proper context;
wenzelm
parents:
27330
diff
changeset
|
75 |
in mk_vars pre end; |
24475
a297ae4ff188
added Hoare/hoare_tac.ML (code from Hoare/Hoare.thy, also required in Isar_examples/Hoare.thy);
wenzelm
parents:
diff
changeset
|
76 |
|
55661 | 77 |
fun mk_CollectC tm = |
74304 | 78 |
let val \<^Type>\<open>fun t _\<close> = fastype_of tm; |
79 |
in \<^Const>\<open>Collect t for tm\<close> end; |
|
24475
a297ae4ff188
added Hoare/hoare_tac.ML (code from Hoare/Hoare.thy, also required in Isar_examples/Hoare.thy);
wenzelm
parents:
diff
changeset
|
80 |
|
74304 | 81 |
fun inclt ty = \<^Const>\<open>less_eq ty\<close>; |
24475
a297ae4ff188
added Hoare/hoare_tac.ML (code from Hoare/Hoare.thy, also required in Isar_examples/Hoare.thy);
wenzelm
parents:
diff
changeset
|
82 |
|
41449 | 83 |
in |
24475
a297ae4ff188
added Hoare/hoare_tac.ML (code from Hoare/Hoare.thy, also required in Isar_examples/Hoare.thy);
wenzelm
parents:
diff
changeset
|
84 |
|
28457
25669513fd4c
major cleanup of hoare_tac.ML: just one copy for Hoare.thy and HoareAbort.thy (only 1 line different), refrain from inspecting the main goal, proper context;
wenzelm
parents:
27330
diff
changeset
|
85 |
fun Mset ctxt prop = |
25669513fd4c
major cleanup of hoare_tac.ML: just one copy for Hoare.thy and HoareAbort.thy (only 1 line different), refrain from inspecting the main goal, proper context;
wenzelm
parents:
27330
diff
changeset
|
86 |
let |
25669513fd4c
major cleanup of hoare_tac.ML: just one copy for Hoare.thy and HoareAbort.thy (only 1 line different), refrain from inspecting the main goal, proper context;
wenzelm
parents:
27330
diff
changeset
|
87 |
val [(Mset, _), (P, _)] = Variable.variant_frees ctxt [] [("Mset", ()), ("P", ())]; |
24475
a297ae4ff188
added Hoare/hoare_tac.ML (code from Hoare/Hoare.thy, also required in Isar_examples/Hoare.thy);
wenzelm
parents:
diff
changeset
|
88 |
|
28457
25669513fd4c
major cleanup of hoare_tac.ML: just one copy for Hoare.thy and HoareAbort.thy (only 1 line different), refrain from inspecting the main goal, proper context;
wenzelm
parents:
27330
diff
changeset
|
89 |
val vars = get_vars prop; |
25669513fd4c
major cleanup of hoare_tac.ML: just one copy for Hoare.thy and HoareAbort.thy (only 1 line different), refrain from inspecting the main goal, proper context;
wenzelm
parents:
27330
diff
changeset
|
90 |
val varsT = fastype_of (mk_bodyC vars); |
55661 | 91 |
val big_Collect = |
74304 | 92 |
mk_CollectC (mk_abstupleC vars (Free (P, varsT --> \<^Type>\<open>bool\<close>) $ mk_bodyC vars)); |
55661 | 93 |
val small_Collect = |
74304 | 94 |
mk_CollectC (Abs ("x", varsT, Free (P, varsT --> \<^Type>\<open>bool\<close>) $ Bound 0)); |
28457
25669513fd4c
major cleanup of hoare_tac.ML: just one copy for Hoare.thy and HoareAbort.thy (only 1 line different), refrain from inspecting the main goal, proper context;
wenzelm
parents:
27330
diff
changeset
|
95 |
|
25669513fd4c
major cleanup of hoare_tac.ML: just one copy for Hoare.thy and HoareAbort.thy (only 1 line different), refrain from inspecting the main goal, proper context;
wenzelm
parents:
27330
diff
changeset
|
96 |
val MsetT = fastype_of big_Collect; |
41449 | 97 |
fun Mset_incl t = HOLogic.mk_Trueprop (inclt MsetT $ Free (Mset, MsetT) $ t); |
28457
25669513fd4c
major cleanup of hoare_tac.ML: just one copy for Hoare.thy and HoareAbort.thy (only 1 line different), refrain from inspecting the main goal, proper context;
wenzelm
parents:
27330
diff
changeset
|
98 |
val impl = Logic.mk_implies (Mset_incl big_Collect, Mset_incl small_Collect); |
42793 | 99 |
val th = Goal.prove ctxt [Mset, P] [] impl (fn _ => blast_tac ctxt 1); |
28457
25669513fd4c
major cleanup of hoare_tac.ML: just one copy for Hoare.thy and HoareAbort.thy (only 1 line different), refrain from inspecting the main goal, proper context;
wenzelm
parents:
27330
diff
changeset
|
100 |
in (vars, th) end; |
24475
a297ae4ff188
added Hoare/hoare_tac.ML (code from Hoare/Hoare.thy, also required in Isar_examples/Hoare.thy);
wenzelm
parents:
diff
changeset
|
101 |
|
a297ae4ff188
added Hoare/hoare_tac.ML (code from Hoare/Hoare.thy, also required in Isar_examples/Hoare.thy);
wenzelm
parents:
diff
changeset
|
102 |
end; |
a297ae4ff188
added Hoare/hoare_tac.ML (code from Hoare/Hoare.thy, also required in Isar_examples/Hoare.thy);
wenzelm
parents:
diff
changeset
|
103 |
|
a297ae4ff188
added Hoare/hoare_tac.ML (code from Hoare/Hoare.thy, also required in Isar_examples/Hoare.thy);
wenzelm
parents:
diff
changeset
|
104 |
|
a297ae4ff188
added Hoare/hoare_tac.ML (code from Hoare/Hoare.thy, also required in Isar_examples/Hoare.thy);
wenzelm
parents:
diff
changeset
|
105 |
(*****************************************************************************) |
a297ae4ff188
added Hoare/hoare_tac.ML (code from Hoare/Hoare.thy, also required in Isar_examples/Hoare.thy);
wenzelm
parents:
diff
changeset
|
106 |
(** Simplifying: **) |
a297ae4ff188
added Hoare/hoare_tac.ML (code from Hoare/Hoare.thy, also required in Isar_examples/Hoare.thy);
wenzelm
parents:
diff
changeset
|
107 |
(** Some useful lemmata, lists and simplification tactics to control which **) |
a297ae4ff188
added Hoare/hoare_tac.ML (code from Hoare/Hoare.thy, also required in Isar_examples/Hoare.thy);
wenzelm
parents:
diff
changeset
|
108 |
(** theorems are used to simplify at each moment, so that the original **) |
a297ae4ff188
added Hoare/hoare_tac.ML (code from Hoare/Hoare.thy, also required in Isar_examples/Hoare.thy);
wenzelm
parents:
diff
changeset
|
109 |
(** input does not suffer any unexpected transformation **) |
a297ae4ff188
added Hoare/hoare_tac.ML (code from Hoare/Hoare.thy, also required in Isar_examples/Hoare.thy);
wenzelm
parents:
diff
changeset
|
110 |
(*****************************************************************************) |
a297ae4ff188
added Hoare/hoare_tac.ML (code from Hoare/Hoare.thy, also required in Isar_examples/Hoare.thy);
wenzelm
parents:
diff
changeset
|
111 |
|
a297ae4ff188
added Hoare/hoare_tac.ML (code from Hoare/Hoare.thy, also required in Isar_examples/Hoare.thy);
wenzelm
parents:
diff
changeset
|
112 |
(**Simp_tacs**) |
a297ae4ff188
added Hoare/hoare_tac.ML (code from Hoare/Hoare.thy, also required in Isar_examples/Hoare.thy);
wenzelm
parents:
diff
changeset
|
113 |
|
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
44241
diff
changeset
|
114 |
fun before_set2pred_simp_tac ctxt = |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
44241
diff
changeset
|
115 |
simp_tac (put_simpset HOL_basic_ss ctxt addsimps [Collect_conj_eq RS sym, @{thm Compl_Collect}]); |
24475
a297ae4ff188
added Hoare/hoare_tac.ML (code from Hoare/Hoare.thy, also required in Isar_examples/Hoare.thy);
wenzelm
parents:
diff
changeset
|
116 |
|
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
44241
diff
changeset
|
117 |
fun split_simp_tac ctxt = |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
44241
diff
changeset
|
118 |
simp_tac (put_simpset HOL_basic_ss ctxt addsimps [@{thm split_conv}]); |
24475
a297ae4ff188
added Hoare/hoare_tac.ML (code from Hoare/Hoare.thy, also required in Isar_examples/Hoare.thy);
wenzelm
parents:
diff
changeset
|
119 |
|
a297ae4ff188
added Hoare/hoare_tac.ML (code from Hoare/Hoare.thy, also required in Isar_examples/Hoare.thy);
wenzelm
parents:
diff
changeset
|
120 |
(*****************************************************************************) |
55661 | 121 |
(** set_to_pred_tac transforms sets inclusion into predicates implication, **) |
24475
a297ae4ff188
added Hoare/hoare_tac.ML (code from Hoare/Hoare.thy, also required in Isar_examples/Hoare.thy);
wenzelm
parents:
diff
changeset
|
122 |
(** maintaining the original variable names. **) |
a297ae4ff188
added Hoare/hoare_tac.ML (code from Hoare/Hoare.thy, also required in Isar_examples/Hoare.thy);
wenzelm
parents:
diff
changeset
|
123 |
(** Ex. "{x. x=0} <= {x. x <= 1}" -set2pred-> "x=0 --> x <= 1" **) |
a297ae4ff188
added Hoare/hoare_tac.ML (code from Hoare/Hoare.thy, also required in Isar_examples/Hoare.thy);
wenzelm
parents:
diff
changeset
|
124 |
(** Subgoals containing intersections (A Int B) or complement sets (-A) **) |
a297ae4ff188
added Hoare/hoare_tac.ML (code from Hoare/Hoare.thy, also required in Isar_examples/Hoare.thy);
wenzelm
parents:
diff
changeset
|
125 |
(** are first simplified by "before_set2pred_simp_tac", that returns only **) |
a297ae4ff188
added Hoare/hoare_tac.ML (code from Hoare/Hoare.thy, also required in Isar_examples/Hoare.thy);
wenzelm
parents:
diff
changeset
|
126 |
(** subgoals of the form "{x. P x} <= {x. Q x}", which are easily **) |
a297ae4ff188
added Hoare/hoare_tac.ML (code from Hoare/Hoare.thy, also required in Isar_examples/Hoare.thy);
wenzelm
parents:
diff
changeset
|
127 |
(** transformed. **) |
a297ae4ff188
added Hoare/hoare_tac.ML (code from Hoare/Hoare.thy, also required in Isar_examples/Hoare.thy);
wenzelm
parents:
diff
changeset
|
128 |
(** This transformation may solve very easy subgoals due to a ligth **) |
a297ae4ff188
added Hoare/hoare_tac.ML (code from Hoare/Hoare.thy, also required in Isar_examples/Hoare.thy);
wenzelm
parents:
diff
changeset
|
129 |
(** simplification done by (split_all_tac) **) |
a297ae4ff188
added Hoare/hoare_tac.ML (code from Hoare/Hoare.thy, also required in Isar_examples/Hoare.thy);
wenzelm
parents:
diff
changeset
|
130 |
(*****************************************************************************) |
a297ae4ff188
added Hoare/hoare_tac.ML (code from Hoare/Hoare.thy, also required in Isar_examples/Hoare.thy);
wenzelm
parents:
diff
changeset
|
131 |
|
55661 | 132 |
fun set_to_pred_tac ctxt var_names = SUBGOAL (fn (_, i) => |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
44241
diff
changeset
|
133 |
before_set2pred_simp_tac ctxt i THEN_MAYBE |
28457
25669513fd4c
major cleanup of hoare_tac.ML: just one copy for Hoare.thy and HoareAbort.thy (only 1 line different), refrain from inspecting the main goal, proper context;
wenzelm
parents:
27330
diff
changeset
|
134 |
EVERY [ |
60754 | 135 |
resolve_tac ctxt [subsetI] i, |
136 |
resolve_tac ctxt [CollectI] i, |
|
137 |
dresolve_tac ctxt [CollectD] i, |
|
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
44241
diff
changeset
|
138 |
TRY (split_all_tac ctxt i) THEN_MAYBE |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
44241
diff
changeset
|
139 |
(rename_tac var_names i THEN |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
44241
diff
changeset
|
140 |
full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps [@{thm split_conv}]) i)]); |
24475
a297ae4ff188
added Hoare/hoare_tac.ML (code from Hoare/Hoare.thy, also required in Isar_examples/Hoare.thy);
wenzelm
parents:
diff
changeset
|
141 |
|
55661 | 142 |
(*******************************************************************************) |
143 |
(** basic_simp_tac is called to simplify all verification conditions. It does **) |
|
144 |
(** a light simplification by applying "mem_Collect_eq", then it calls **) |
|
145 |
(** max_simp_tac, which solves subgoals of the form "A <= A", **) |
|
146 |
(** and transforms any other into predicates, applying then **) |
|
147 |
(** the tactic chosen by the user, which may solve the subgoal completely. **) |
|
148 |
(*******************************************************************************) |
|
24475
a297ae4ff188
added Hoare/hoare_tac.ML (code from Hoare/Hoare.thy, also required in Isar_examples/Hoare.thy);
wenzelm
parents:
diff
changeset
|
149 |
|
55661 | 150 |
fun max_simp_tac ctxt var_names tac = |
60754 | 151 |
FIRST' [resolve_tac ctxt [subset_refl], |
152 |
set_to_pred_tac ctxt var_names THEN_MAYBE' tac]; |
|
24475
a297ae4ff188
added Hoare/hoare_tac.ML (code from Hoare/Hoare.thy, also required in Isar_examples/Hoare.thy);
wenzelm
parents:
diff
changeset
|
153 |
|
55661 | 154 |
fun basic_simp_tac ctxt var_names tac = |
28457
25669513fd4c
major cleanup of hoare_tac.ML: just one copy for Hoare.thy and HoareAbort.thy (only 1 line different), refrain from inspecting the main goal, proper context;
wenzelm
parents:
27330
diff
changeset
|
155 |
simp_tac |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
44241
diff
changeset
|
156 |
(put_simpset HOL_basic_ss ctxt |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
44241
diff
changeset
|
157 |
addsimps [mem_Collect_eq, @{thm split_conv}] addsimprocs [Record.simproc]) |
55661 | 158 |
THEN_MAYBE' max_simp_tac ctxt var_names tac; |
24475
a297ae4ff188
added Hoare/hoare_tac.ML (code from Hoare/Hoare.thy, also required in Isar_examples/Hoare.thy);
wenzelm
parents:
diff
changeset
|
159 |
|
a297ae4ff188
added Hoare/hoare_tac.ML (code from Hoare/Hoare.thy, also required in Isar_examples/Hoare.thy);
wenzelm
parents:
diff
changeset
|
160 |
|
28457
25669513fd4c
major cleanup of hoare_tac.ML: just one copy for Hoare.thy and HoareAbort.thy (only 1 line different), refrain from inspecting the main goal, proper context;
wenzelm
parents:
27330
diff
changeset
|
161 |
(** hoare_rule_tac **) |
25669513fd4c
major cleanup of hoare_tac.ML: just one copy for Hoare.thy and HoareAbort.thy (only 1 line different), refrain from inspecting the main goal, proper context;
wenzelm
parents:
27330
diff
changeset
|
162 |
|
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
44241
diff
changeset
|
163 |
fun hoare_rule_tac ctxt (vars, Mlem) tac = |
28457
25669513fd4c
major cleanup of hoare_tac.ML: just one copy for Hoare.thy and HoareAbort.thy (only 1 line different), refrain from inspecting the main goal, proper context;
wenzelm
parents:
27330
diff
changeset
|
164 |
let |
72985
9cc431444435
clarified modules: avoid multiple uses of the same ML file;
wenzelm
parents:
72806
diff
changeset
|
165 |
val get_thms = Proof_Context.get_thms ctxt; |
28457
25669513fd4c
major cleanup of hoare_tac.ML: just one copy for Hoare.thy and HoareAbort.thy (only 1 line different), refrain from inspecting the main goal, proper context;
wenzelm
parents:
27330
diff
changeset
|
166 |
val var_names = map (fst o dest_Free) vars; |
25669513fd4c
major cleanup of hoare_tac.ML: just one copy for Hoare.thy and HoareAbort.thy (only 1 line different), refrain from inspecting the main goal, proper context;
wenzelm
parents:
27330
diff
changeset
|
167 |
fun wlp_tac i = |
72985
9cc431444435
clarified modules: avoid multiple uses of the same ML file;
wenzelm
parents:
72806
diff
changeset
|
168 |
resolve_tac ctxt (get_thms \<^named_theorems>\<open>SeqRule\<close>) i THEN rule_tac false (i + 1) |
28457
25669513fd4c
major cleanup of hoare_tac.ML: just one copy for Hoare.thy and HoareAbort.thy (only 1 line different), refrain from inspecting the main goal, proper context;
wenzelm
parents:
27330
diff
changeset
|
169 |
and rule_tac pre_cond i st = st |> (*abstraction over st prevents looping*) |
25669513fd4c
major cleanup of hoare_tac.ML: just one copy for Hoare.thy and HoareAbort.thy (only 1 line different), refrain from inspecting the main goal, proper context;
wenzelm
parents:
27330
diff
changeset
|
170 |
((wlp_tac i THEN rule_tac pre_cond i) |
25669513fd4c
major cleanup of hoare_tac.ML: just one copy for Hoare.thy and HoareAbort.thy (only 1 line different), refrain from inspecting the main goal, proper context;
wenzelm
parents:
27330
diff
changeset
|
171 |
ORELSE |
25669513fd4c
major cleanup of hoare_tac.ML: just one copy for Hoare.thy and HoareAbort.thy (only 1 line different), refrain from inspecting the main goal, proper context;
wenzelm
parents:
27330
diff
changeset
|
172 |
(FIRST [ |
72985
9cc431444435
clarified modules: avoid multiple uses of the same ML file;
wenzelm
parents:
72806
diff
changeset
|
173 |
resolve_tac ctxt (get_thms \<^named_theorems>\<open>SkipRule\<close>) i, |
9cc431444435
clarified modules: avoid multiple uses of the same ML file;
wenzelm
parents:
72806
diff
changeset
|
174 |
resolve_tac ctxt (get_thms \<^named_theorems>\<open>AbortRule\<close>) i, |
28457
25669513fd4c
major cleanup of hoare_tac.ML: just one copy for Hoare.thy and HoareAbort.thy (only 1 line different), refrain from inspecting the main goal, proper context;
wenzelm
parents:
27330
diff
changeset
|
175 |
EVERY [ |
72985
9cc431444435
clarified modules: avoid multiple uses of the same ML file;
wenzelm
parents:
72806
diff
changeset
|
176 |
resolve_tac ctxt (get_thms \<^named_theorems>\<open>BasicRule\<close>) i, |
60754 | 177 |
resolve_tac ctxt [Mlem] i, |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
44241
diff
changeset
|
178 |
split_simp_tac ctxt i], |
28457
25669513fd4c
major cleanup of hoare_tac.ML: just one copy for Hoare.thy and HoareAbort.thy (only 1 line different), refrain from inspecting the main goal, proper context;
wenzelm
parents:
27330
diff
changeset
|
179 |
EVERY [ |
72985
9cc431444435
clarified modules: avoid multiple uses of the same ML file;
wenzelm
parents:
72806
diff
changeset
|
180 |
resolve_tac ctxt (get_thms \<^named_theorems>\<open>CondRule\<close>) i, |
28457
25669513fd4c
major cleanup of hoare_tac.ML: just one copy for Hoare.thy and HoareAbort.thy (only 1 line different), refrain from inspecting the main goal, proper context;
wenzelm
parents:
27330
diff
changeset
|
181 |
rule_tac false (i + 2), |
25669513fd4c
major cleanup of hoare_tac.ML: just one copy for Hoare.thy and HoareAbort.thy (only 1 line different), refrain from inspecting the main goal, proper context;
wenzelm
parents:
27330
diff
changeset
|
182 |
rule_tac false (i + 1)], |
25669513fd4c
major cleanup of hoare_tac.ML: just one copy for Hoare.thy and HoareAbort.thy (only 1 line different), refrain from inspecting the main goal, proper context;
wenzelm
parents:
27330
diff
changeset
|
183 |
EVERY [ |
72985
9cc431444435
clarified modules: avoid multiple uses of the same ML file;
wenzelm
parents:
72806
diff
changeset
|
184 |
resolve_tac ctxt (get_thms \<^named_theorems>\<open>WhileRule\<close>) i, |
55661 | 185 |
basic_simp_tac ctxt var_names tac (i + 2), |
28457
25669513fd4c
major cleanup of hoare_tac.ML: just one copy for Hoare.thy and HoareAbort.thy (only 1 line different), refrain from inspecting the main goal, proper context;
wenzelm
parents:
27330
diff
changeset
|
186 |
rule_tac true (i + 1)]] |
60754 | 187 |
THEN ( |
188 |
if pre_cond then basic_simp_tac ctxt var_names tac i |
|
189 |
else resolve_tac ctxt [subset_refl] i))); |
|
28457
25669513fd4c
major cleanup of hoare_tac.ML: just one copy for Hoare.thy and HoareAbort.thy (only 1 line different), refrain from inspecting the main goal, proper context;
wenzelm
parents:
27330
diff
changeset
|
190 |
in rule_tac end; |
25669513fd4c
major cleanup of hoare_tac.ML: just one copy for Hoare.thy and HoareAbort.thy (only 1 line different), refrain from inspecting the main goal, proper context;
wenzelm
parents:
27330
diff
changeset
|
191 |
|
25669513fd4c
major cleanup of hoare_tac.ML: just one copy for Hoare.thy and HoareAbort.thy (only 1 line different), refrain from inspecting the main goal, proper context;
wenzelm
parents:
27330
diff
changeset
|
192 |
|
25669513fd4c
major cleanup of hoare_tac.ML: just one copy for Hoare.thy and HoareAbort.thy (only 1 line different), refrain from inspecting the main goal, proper context;
wenzelm
parents:
27330
diff
changeset
|
193 |
(** tac is the tactic the user chooses to solve or simplify **) |
25669513fd4c
major cleanup of hoare_tac.ML: just one copy for Hoare.thy and HoareAbort.thy (only 1 line different), refrain from inspecting the main goal, proper context;
wenzelm
parents:
27330
diff
changeset
|
194 |
(** the final verification conditions **) |
25669513fd4c
major cleanup of hoare_tac.ML: just one copy for Hoare.thy and HoareAbort.thy (only 1 line different), refrain from inspecting the main goal, proper context;
wenzelm
parents:
27330
diff
changeset
|
195 |
|
55659 | 196 |
fun hoare_tac ctxt tac = SUBGOAL (fn (goal, i) => |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
44241
diff
changeset
|
197 |
SELECT_GOAL (hoare_rule_tac ctxt (Mset ctxt goal) tac true 1) i); |
28457
25669513fd4c
major cleanup of hoare_tac.ML: just one copy for Hoare.thy and HoareAbort.thy (only 1 line different), refrain from inspecting the main goal, proper context;
wenzelm
parents:
27330
diff
changeset
|
198 |
|
72806
4fa08e083865
Extension of session HOL/Hoare with total correctness proof system by Walter Guttmann
nipkow
parents:
69597
diff
changeset
|
199 |
|
4fa08e083865
Extension of session HOL/Hoare with total correctness proof system by Walter Guttmann
nipkow
parents:
69597
diff
changeset
|
200 |
(* total correctness rules *) |
4fa08e083865
Extension of session HOL/Hoare with total correctness proof system by Walter Guttmann
nipkow
parents:
69597
diff
changeset
|
201 |
|
4fa08e083865
Extension of session HOL/Hoare with total correctness proof system by Walter Guttmann
nipkow
parents:
69597
diff
changeset
|
202 |
fun hoare_tc_rule_tac ctxt (vars, Mlem) tac = |
4fa08e083865
Extension of session HOL/Hoare with total correctness proof system by Walter Guttmann
nipkow
parents:
69597
diff
changeset
|
203 |
let |
72985
9cc431444435
clarified modules: avoid multiple uses of the same ML file;
wenzelm
parents:
72806
diff
changeset
|
204 |
val get_thms = Proof_Context.get_thms ctxt; |
72806
4fa08e083865
Extension of session HOL/Hoare with total correctness proof system by Walter Guttmann
nipkow
parents:
69597
diff
changeset
|
205 |
val var_names = map (fst o dest_Free) vars; |
4fa08e083865
Extension of session HOL/Hoare with total correctness proof system by Walter Guttmann
nipkow
parents:
69597
diff
changeset
|
206 |
fun wlp_tac i = |
72985
9cc431444435
clarified modules: avoid multiple uses of the same ML file;
wenzelm
parents:
72806
diff
changeset
|
207 |
resolve_tac ctxt (get_thms \<^named_theorems>\<open>SeqRuleTC\<close>) i THEN rule_tac false (i + 1) |
72806
4fa08e083865
Extension of session HOL/Hoare with total correctness proof system by Walter Guttmann
nipkow
parents:
69597
diff
changeset
|
208 |
and rule_tac pre_cond i st = st |> (*abstraction over st prevents looping*) |
4fa08e083865
Extension of session HOL/Hoare with total correctness proof system by Walter Guttmann
nipkow
parents:
69597
diff
changeset
|
209 |
((wlp_tac i THEN rule_tac pre_cond i) |
4fa08e083865
Extension of session HOL/Hoare with total correctness proof system by Walter Guttmann
nipkow
parents:
69597
diff
changeset
|
210 |
ORELSE |
4fa08e083865
Extension of session HOL/Hoare with total correctness proof system by Walter Guttmann
nipkow
parents:
69597
diff
changeset
|
211 |
(FIRST [ |
72985
9cc431444435
clarified modules: avoid multiple uses of the same ML file;
wenzelm
parents:
72806
diff
changeset
|
212 |
resolve_tac ctxt (get_thms \<^named_theorems>\<open>SkipRuleTC\<close>) i, |
72806
4fa08e083865
Extension of session HOL/Hoare with total correctness proof system by Walter Guttmann
nipkow
parents:
69597
diff
changeset
|
213 |
EVERY [ |
72985
9cc431444435
clarified modules: avoid multiple uses of the same ML file;
wenzelm
parents:
72806
diff
changeset
|
214 |
resolve_tac ctxt (get_thms \<^named_theorems>\<open>BasicRuleTC\<close>) i, |
72806
4fa08e083865
Extension of session HOL/Hoare with total correctness proof system by Walter Guttmann
nipkow
parents:
69597
diff
changeset
|
215 |
resolve_tac ctxt [Mlem] i, |
4fa08e083865
Extension of session HOL/Hoare with total correctness proof system by Walter Guttmann
nipkow
parents:
69597
diff
changeset
|
216 |
split_simp_tac ctxt i], |
4fa08e083865
Extension of session HOL/Hoare with total correctness proof system by Walter Guttmann
nipkow
parents:
69597
diff
changeset
|
217 |
EVERY [ |
72985
9cc431444435
clarified modules: avoid multiple uses of the same ML file;
wenzelm
parents:
72806
diff
changeset
|
218 |
resolve_tac ctxt (get_thms \<^named_theorems>\<open>CondRuleTC\<close>) i, |
72806
4fa08e083865
Extension of session HOL/Hoare with total correctness proof system by Walter Guttmann
nipkow
parents:
69597
diff
changeset
|
219 |
rule_tac false (i + 2), |
4fa08e083865
Extension of session HOL/Hoare with total correctness proof system by Walter Guttmann
nipkow
parents:
69597
diff
changeset
|
220 |
rule_tac false (i + 1)], |
4fa08e083865
Extension of session HOL/Hoare with total correctness proof system by Walter Guttmann
nipkow
parents:
69597
diff
changeset
|
221 |
EVERY [ |
72985
9cc431444435
clarified modules: avoid multiple uses of the same ML file;
wenzelm
parents:
72806
diff
changeset
|
222 |
resolve_tac ctxt (get_thms \<^named_theorems>\<open>WhileRuleTC\<close>) i, |
72806
4fa08e083865
Extension of session HOL/Hoare with total correctness proof system by Walter Guttmann
nipkow
parents:
69597
diff
changeset
|
223 |
basic_simp_tac ctxt var_names tac (i + 2), |
4fa08e083865
Extension of session HOL/Hoare with total correctness proof system by Walter Guttmann
nipkow
parents:
69597
diff
changeset
|
224 |
rule_tac true (i + 1)]] |
4fa08e083865
Extension of session HOL/Hoare with total correctness proof system by Walter Guttmann
nipkow
parents:
69597
diff
changeset
|
225 |
THEN ( |
4fa08e083865
Extension of session HOL/Hoare with total correctness proof system by Walter Guttmann
nipkow
parents:
69597
diff
changeset
|
226 |
if pre_cond then basic_simp_tac ctxt var_names tac i |
4fa08e083865
Extension of session HOL/Hoare with total correctness proof system by Walter Guttmann
nipkow
parents:
69597
diff
changeset
|
227 |
else resolve_tac ctxt [subset_refl] i))); |
4fa08e083865
Extension of session HOL/Hoare with total correctness proof system by Walter Guttmann
nipkow
parents:
69597
diff
changeset
|
228 |
in rule_tac end; |
4fa08e083865
Extension of session HOL/Hoare with total correctness proof system by Walter Guttmann
nipkow
parents:
69597
diff
changeset
|
229 |
|
4fa08e083865
Extension of session HOL/Hoare with total correctness proof system by Walter Guttmann
nipkow
parents:
69597
diff
changeset
|
230 |
|
4fa08e083865
Extension of session HOL/Hoare with total correctness proof system by Walter Guttmann
nipkow
parents:
69597
diff
changeset
|
231 |
fun hoare_tc_tac ctxt tac = SUBGOAL (fn (goal, i) => |
4fa08e083865
Extension of session HOL/Hoare with total correctness proof system by Walter Guttmann
nipkow
parents:
69597
diff
changeset
|
232 |
SELECT_GOAL (hoare_tc_rule_tac ctxt (Mset ctxt goal) tac true 1) i); |
4fa08e083865
Extension of session HOL/Hoare with total correctness proof system by Walter Guttmann
nipkow
parents:
69597
diff
changeset
|
233 |
|
55660 | 234 |
end; |