1structure BackchainingLib :> BackchainingLib =
2struct
3
4open HolKernel Parse Drule ConseqConv simpLib Conv Tactic Tactical boolSyntax boolTheory
5
6local
7
8fun RESTRICTED_RES_CANON_WITH_MARK thm = let
9  val _ = dest_imp_only (snd (strip_forall (concl thm)))
10
11  (* Mark thm so it does not get changed below*)
12  val thm' = CONV_RULE (STRIP_QUANT_CONV (RAND_CONV (markerLib.stmark_term))) thm
13in
14  List.map GEN_ALL (IMP_CANON thm')
15end handle HOL_ERR _ => [];
16
17fun RES_ALL_PRECONDS_WITH_MARK asms results [] = results
18  | RES_ALL_PRECONDS_WITH_MARK asms results (thm::thms) =
19  if is_imp_only (snd (strip_forall (concl thm))) then
20  let
21     val new_thms  = mapfilter (MATCH_MP thm) asms
22  in
23     RES_ALL_PRECONDS_WITH_MARK asms results (append new_thms thms)
24  end else let
25    val thm' = CONV_RULE (STRIP_QUANT_CONV (REWR_CONV markerTheory.stmarker_def)) thm
26    val is_old = List.exists (fn thm'' => aconv (concl thm') (concl thm'')) results
27    val results' = if is_old then results else thm'::results
28  in
29    RES_ALL_PRECONDS_WITH_MARK asms results' thms
30  end handle HOL_ERR _ =>
31    RES_ALL_PRECONDS_WITH_MARK asms results thms
32
33in
34
35fun BACKCHAIN_THEN ttac input_thms = let
36  val thms0 = Lib.flatten (List.map BODY_CONJUNCTS input_thms)
37  val thms1 = Lib.flatten (List.map RESTRICTED_RES_CANON_WITH_MARK thms0)
38in
39  Tactical.ASSUM_LIST (fn asms =>
40    ttac (RES_ALL_PRECONDS_WITH_MARK asms [] thms1))
41end
42
43end
44
45
46fun BACKCHAIN_EVERY_THEN ttac =
47  BACKCHAIN_THEN (fn thms => EVERY (List.map (fn thm => (TRY (ttac thm))) thms))
48
49val BACKCHAIN_ASSUME_TAC =
50  BACKCHAIN_EVERY_THEN STRIP_ASSUME_TAC
51
52val BACKCHAIN_MP_TAC =
53  BACKCHAIN_EVERY_THEN MP_TAC
54
55val BACKCHAIN_TAC =
56  BACKCHAIN_THEN (fn thms => ConseqConv.CONSEQ_REWRITE_TAC (thms, [], []))
57
58
59fun BC_SIMP_TAC ss gthms thms' =
60  BACKCHAIN_THEN (fn thms => SIMP_TAC ss (thms @ thms')) gthms
61
62fun ASM_BC_SIMP_TAC ss gthms thms' =
63  BACKCHAIN_THEN (fn thms => ASM_SIMP_TAC ss (thms @ thms')) gthms
64
65fun FULL_BC_SIMP_TAC ss gthms thms' =
66  BACKCHAIN_THEN (fn thms => FULL_SIMP_TAC ss (thms @ thms')) gthms
67
68
69(************************************************************)
70(* Some demo
71
72val R_def = Define `R x y = (x:num) > y`
73
74val R1 = prove (``R x y ==> x <= x' /\ y' <= y ==> R x' y'``,
75  SIMP_TAC arith_ss [R_def])
76
77(* As a first simple test prove just R1 again. *)
78
79``R x y ==> x <= x' /\ y' <= y ==> R x' y'``,
80
81REPEAT STRIP_TAC THEN
82
83(* METIS does of course the trick.
84METIS_TAC[R1]
85*)
86
87(* Conditional rewriting does not manage to do it
88ASM_SIMP_TAC std_ss [R1]
89
90It needs to solve the following precondition
91
92?y x. R x y /\ x <= x' /\ y' <= y
93
94in order to apply the conditional rewrite. This however, requires
95instantiating x and, which it does not manage. Even using tools
96like QI_ss does not help since two vars need instantiating at once.
97
98set_trace "simplifier" 1
99ASM_SIMP_TAC (std_ss++QI_ss) [R1]
100*)
101
102(* One can of course apply the rule manually backwards using MATCH_MP_TAC.
103
104val R1' = IRULE_CANON R1
105MATCH_MP_TAC R1'
106
107This is however applicable only at toplevel. Consequence rewrites are handy,
108but easily loop.
109
110ConseqConv.ONCE_CONSEQ_REWRITE_TAC ([R1'], [], []) THEN
111ConseqConv.ONCE_CONSEQ_REWRITE_TAC ([R1'], [], []) THEN
112ConseqConv.ONCE_CONSEQ_REWRITE_TAC ([R1'], [], [])
113
114ConseqConv.CONSEQ_REWRITE_TAC ([R1'], [], [])
115
116*)
117
118(* IMP_RES_TAC works in this simple case, but often produces a lot of clutter (see later)
119
120IMP_RES_TAC R1
121
122*)
123
124(* So lets try the new stuff. *)
125
126BACKCHAIN_TAC [R1]
127BACKCHAIN_MP_TAC [R1]
128BACKCHAIN_ASSUME_TAC [R1]
129ASM_BC_SIMP_TAC std_ss [R1] []
130
131
132Now let's look at more interesting examples:
133
134``R x y ==> x <= 10 /\ x < 20 /\ x' > 15 /\ y' <= 20 /\ 21 <= y ==>
135  (R x' y' /\ R 10 y' /\ (x < 12))``,
136
137STRIP_TAC THEN STRIP_TAC
138
139(* No IMP_RES_TAC produces a lot of not useful stuff.
140   More importantly, the real interesting instances are not produced!
141 *)
142IMP_RES_TAC R1
143
144(* Metis fails as well, since some arithmetic reasoning is needed *)
145METIS_TAC[R1]
146
147(* MATCH_MP_TAC is painful since it requires splitting the goal,
148   BACKCHAIN_TAC is more handy. *)
149
150BACKCHAIN_TAC [R1]
151DECIDE_TAC
152
153(* Combined with the simplifier, it is immediately solved *)
154ASM_BC_SIMP_TAC arith_ss [R1] []
155
156
157(* This is useful, if some goals cannot be solved completely.
158
159``R x y /\ x <= 10 /\ x < 20 /\ x' > 15 /\ y' <= 20 /\ 21 <= y ==>
160  (R x' y' /\ QQ x y y' /\ R 5 x' /\ (x < 12))``,
161
162
163STRIP_TAC
164ASM_BC_SIMP_TAC arith_ss [R1] []
165
166
167One can use more interesting preconditions as well.
168
169val R2 = prove (``(R x y \/ x > y \/ y < x) ==> x <= x' /\ y' <= y ==> R x' y'``,
170  SIMP_TAC arith_ss [R_def])
171
172
173``6 > 5 /\ 10 < x /\ 10 < x' /\ 30 < x /\ y <= 20 /\ x < 100 /\ 100 <= x' ==>
174  R x' y /\ QQ x' y``,
175
176STRIP_TAC
177
178(* Now there are multiple theorems produced. BACKCHAIN_TAC picks the wrong
179   instantiation and one cannot solve the resulting goal :-( *)
180BACKCHAIN_TAC [R2] THEN
181ASM_SIMP_TAC arith_ss []
182
183(* If one instead checks all possible instances, it can be solved *)
184BACKCHAIN_MP_TAC [R2] THEN
185ASM_SIMP_TAC arith_ss []
186
187(* XXX *)
188IMP_RES_THEN MP_TAC R2
189
190(* In combination with conditional rewriting, this leads to a nice user experience
191   neither cluttering the state nor picking unsuited instances. *)
192
193ASM_BC_SIMP_TAC arith_ss [R2] []
194
195*)
196*)
197
198
199end
200