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