1(* Title: FOLP/classical.ML 2 Author: Lawrence C Paulson, Cambridge University Computer Laboratory 3 Copyright 1992 University of Cambridge 4 5Like Provers/classical but modified because match_tac is unsuitable for 6proof objects. 7 8Theorem prover for classical reasoning, including predicate calculus, set 9theory, etc. 10 11Rules must be classified as intr, elim, safe, hazardous. 12 13A rule is unsafe unless it can be applied blindly without harmful results. 14For a rule to be safe, its premises and conclusion should be logically 15equivalent. There should be no variables in the premises that are not in 16the conclusion. 17*) 18 19signature CLASSICAL_DATA = 20 sig 21 val mp: thm (* [| P-->Q; P |] ==> Q *) 22 val not_elim: thm (* [| ~P; P |] ==> R *) 23 val swap: thm (* ~P ==> (~Q ==> P) ==> Q *) 24 val sizef : thm -> int (* size function for BEST_FIRST *) 25 val hyp_subst_tacs: Proof.context -> (int -> tactic) list 26 end; 27 28(*Higher precedence than := facilitates use of references*) 29infix 4 addSIs addSEs addSDs addIs addEs addDs; 30 31 32signature CLASSICAL = 33 sig 34 type claset 35 val empty_cs: claset 36 val addDs : claset * thm list -> claset 37 val addEs : claset * thm list -> claset 38 val addIs : claset * thm list -> claset 39 val addSDs: claset * thm list -> claset 40 val addSEs: claset * thm list -> claset 41 val addSIs: claset * thm list -> claset 42 val print_cs: Proof.context -> claset -> unit 43 val rep_cs: claset -> 44 {safeIs: thm list, safeEs: thm list, hazIs: thm list, hazEs: thm list, 45 safe0_brls:(bool*thm)list, safep_brls: (bool*thm)list, 46 haz_brls: (bool*thm)list} 47 val best_tac : Proof.context -> claset -> int -> tactic 48 val contr_tac : Proof.context -> int -> tactic 49 val fast_tac : Proof.context -> claset -> int -> tactic 50 val inst_step_tac : Proof.context -> int -> tactic 51 val joinrules : thm list * thm list -> (bool * thm) list 52 val mp_tac: Proof.context -> int -> tactic 53 val safe_tac : Proof.context -> claset -> tactic 54 val safe_step_tac : Proof.context -> claset -> int -> tactic 55 val slow_step_tac : Proof.context -> claset -> int -> tactic 56 val step_tac : Proof.context -> claset -> int -> tactic 57 val swapify : thm list -> thm list 58 val swap_res_tac : Proof.context -> thm list -> int -> tactic 59 val uniq_mp_tac: Proof.context -> int -> tactic 60 end; 61 62 63functor Classical(Data: CLASSICAL_DATA): CLASSICAL = 64struct 65 66local open Data in 67 68(** Useful tactics for classical reasoning **) 69 70val imp_elim = make_elim mp; 71 72(*Solve goal that assumes both P and ~P. *) 73fun contr_tac ctxt = eresolve_tac ctxt [not_elim] THEN' assume_tac ctxt; 74 75(*Finds P-->Q and P in the assumptions, replaces implication by Q *) 76fun mp_tac ctxt i = eresolve_tac ctxt ([not_elim,imp_elim]) i THEN assume_tac ctxt i; 77 78(*Like mp_tac but instantiates no variables*) 79fun uniq_mp_tac ctxt i = ematch_tac ctxt ([not_elim,imp_elim]) i THEN uniq_assume_tac ctxt i; 80 81(*Creates rules to eliminate ~A, from rules to introduce A*) 82fun swapify intrs = intrs RLN (2, [swap]); 83 84(*Uses introduction rules in the normal way, or on negated assumptions, 85 trying rules in order. *) 86fun swap_res_tac ctxt rls = 87 let fun tacf rl = resolve_tac ctxt [rl] ORELSE' eresolve_tac ctxt [rl RSN (2, swap)] 88 in assume_tac ctxt ORELSE' contr_tac ctxt ORELSE' FIRST' (map tacf rls) 89 end; 90 91 92(*** Classical rule sets ***) 93 94datatype claset = 95 CS of {safeIs: thm list, 96 safeEs: thm list, 97 hazIs: thm list, 98 hazEs: thm list, 99 (*the following are computed from the above*) 100 safe0_brls: (bool*thm)list, 101 safep_brls: (bool*thm)list, 102 haz_brls: (bool*thm)list}; 103 104fun rep_cs (CS x) = x; 105 106(*For use with biresolve_tac. Combines intrs with swap to catch negated 107 assumptions. Also pairs elims with true. *) 108fun joinrules (intrs,elims) = 109 map (pair true) (elims @ swapify intrs) @ map (pair false) intrs; 110 111(*Note that allE precedes exI in haz_brls*) 112fun make_cs {safeIs,safeEs,hazIs,hazEs} = 113 let val (safe0_brls, safep_brls) = (*0 subgoals vs 1 or more*) 114 List.partition (curry (op =) 0 o subgoals_of_brl) 115 (sort (make_ord lessb) (joinrules(safeIs, safeEs))) 116 in CS{safeIs=safeIs, safeEs=safeEs, hazIs=hazIs, hazEs=hazEs, 117 safe0_brls=safe0_brls, safep_brls=safep_brls, 118 haz_brls = sort (make_ord lessb) (joinrules(hazIs, hazEs))} 119 end; 120 121(*** Manipulation of clasets ***) 122 123val empty_cs = make_cs{safeIs=[], safeEs=[], hazIs=[], hazEs=[]}; 124 125fun print_cs ctxt (CS{safeIs,safeEs,hazIs,hazEs,...}) = 126 writeln (cat_lines 127 (["Introduction rules"] @ map (Thm.string_of_thm ctxt) hazIs @ 128 ["Safe introduction rules"] @ map (Thm.string_of_thm ctxt) safeIs @ 129 ["Elimination rules"] @ map (Thm.string_of_thm ctxt) hazEs @ 130 ["Safe elimination rules"] @ map (Thm.string_of_thm ctxt) safeEs)); 131 132fun (CS{safeIs,safeEs,hazIs,hazEs,...}) addSIs ths = 133 make_cs {safeIs=ths@safeIs, safeEs=safeEs, hazIs=hazIs, hazEs=hazEs}; 134 135fun (CS{safeIs,safeEs,hazIs,hazEs,...}) addSEs ths = 136 make_cs {safeIs=safeIs, safeEs=ths@safeEs, hazIs=hazIs, hazEs=hazEs}; 137 138fun cs addSDs ths = cs addSEs (map make_elim ths); 139 140fun (CS{safeIs,safeEs,hazIs,hazEs,...}) addIs ths = 141 make_cs {safeIs=safeIs, safeEs=safeEs, hazIs=ths@hazIs, hazEs=hazEs}; 142 143fun (CS{safeIs,safeEs,hazIs,hazEs,...}) addEs ths = 144 make_cs {safeIs=safeIs, safeEs=safeEs, hazIs=hazIs, hazEs=ths@hazEs}; 145 146fun cs addDs ths = cs addEs (map make_elim ths); 147 148(*** Simple tactics for theorem proving ***) 149 150(*Attack subgoals using safe inferences*) 151fun safe_step_tac ctxt (CS{safe0_brls,safep_brls,...}) = 152 FIRST' [uniq_assume_tac ctxt, 153 uniq_mp_tac ctxt, 154 biresolve_tac ctxt safe0_brls, 155 FIRST' (hyp_subst_tacs ctxt), 156 biresolve_tac ctxt safep_brls] ; 157 158(*Repeatedly attack subgoals using safe inferences*) 159fun safe_tac ctxt cs = DETERM (REPEAT_FIRST (safe_step_tac ctxt cs)); 160 161(*These steps could instantiate variables and are therefore unsafe.*) 162fun inst_step_tac ctxt = assume_tac ctxt APPEND' contr_tac ctxt; 163 164(*Single step for the prover. FAILS unless it makes progress. *) 165fun step_tac ctxt (cs as (CS{haz_brls,...})) i = 166 FIRST [safe_tac ctxt cs, 167 inst_step_tac ctxt i, 168 biresolve_tac ctxt haz_brls i]; 169 170(*** The following tactics all fail unless they solve one goal ***) 171 172(*Dumb but fast*) 173fun fast_tac ctxt cs = SELECT_GOAL (DEPTH_SOLVE (step_tac ctxt cs 1)); 174 175(*Slower but smarter than fast_tac*) 176fun best_tac ctxt cs = 177 SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, sizef) (step_tac ctxt cs 1)); 178 179(*Using a "safe" rule to instantiate variables is unsafe. This tactic 180 allows backtracking from "safe" rules to "unsafe" rules here.*) 181fun slow_step_tac ctxt (cs as (CS{haz_brls,...})) i = 182 safe_tac ctxt cs ORELSE (assume_tac ctxt i APPEND biresolve_tac ctxt haz_brls i); 183 184end; 185end; 186