src/Provers/classical.ML
 author lcp Wed Nov 02 12:48:22 1994 +0100 (1994-11-02 ago) changeset 681 9b02474744ca parent 469 b571d997178d child 747 bdc066781063 permissions -rw-r--r--
Provers/classical: now takes theorem "classical" as argument, proves "swap"
Provers/classical/depth_tac,deepen_tac: new
 clasohm@0 ` 1` ```(* Title: Provers/classical ``` clasohm@0 ` 2` ``` ID: \$Id\$ ``` clasohm@0 ` 3` ``` Author: Lawrence C Paulson, Cambridge University Computer Laboratory ``` clasohm@0 ` 4` ``` Copyright 1992 University of Cambridge ``` clasohm@0 ` 5` clasohm@0 ` 6` ```Theorem prover for classical reasoning, including predicate calculus, set ``` clasohm@0 ` 7` ```theory, etc. ``` clasohm@0 ` 8` clasohm@0 ` 9` ```Rules must be classified as intr, elim, safe, hazardous. ``` clasohm@0 ` 10` clasohm@0 ` 11` ```A rule is unsafe unless it can be applied blindly without harmful results. ``` clasohm@0 ` 12` ```For a rule to be safe, its premises and conclusion should be logically ``` clasohm@0 ` 13` ```equivalent. There should be no variables in the premises that are not in ``` clasohm@0 ` 14` ```the conclusion. ``` clasohm@0 ` 15` ```*) ``` clasohm@0 ` 16` clasohm@0 ` 17` ```signature CLASSICAL_DATA = ``` clasohm@0 ` 18` ``` sig ``` lcp@681 ` 19` ``` val mp : thm (* [| P-->Q; P |] ==> Q *) ``` lcp@681 ` 20` ``` val not_elim : thm (* [| ~P; P |] ==> R *) ``` lcp@681 ` 21` ``` val classical : thm (* (~P ==> P) ==> P *) ``` lcp@681 ` 22` ``` val sizef : thm -> int (* size function for BEST_FIRST *) ``` clasohm@0 ` 23` ``` val hyp_subst_tacs: (int -> tactic) list ``` clasohm@0 ` 24` ``` end; ``` clasohm@0 ` 25` clasohm@0 ` 26` ```(*Higher precedence than := facilitates use of references*) ``` clasohm@0 ` 27` ```infix 4 addSIs addSEs addSDs addIs addEs addDs; ``` clasohm@0 ` 28` clasohm@0 ` 29` clasohm@0 ` 30` ```signature CLASSICAL = ``` clasohm@0 ` 31` ``` sig ``` clasohm@0 ` 32` ``` type claset ``` lcp@681 ` 33` ``` val empty_cs : claset ``` lcp@681 ` 34` ``` val addDs : claset * thm list -> claset ``` lcp@681 ` 35` ``` val addEs : claset * thm list -> claset ``` lcp@681 ` 36` ``` val addIs : claset * thm list -> claset ``` lcp@681 ` 37` ``` val addSDs : claset * thm list -> claset ``` lcp@681 ` 38` ``` val addSEs : claset * thm list -> claset ``` lcp@681 ` 39` ``` val addSIs : claset * thm list -> claset ``` lcp@681 ` 40` ``` val print_cs : claset -> unit ``` lcp@681 ` 41` ``` val rep_claset : claset -> {safeIs: thm list, safeEs: thm list, ``` lcp@681 ` 42` ``` hazIs: thm list, hazEs: thm list} ``` lcp@681 ` 43` ``` val best_tac : claset -> int -> tactic ``` lcp@681 ` 44` ``` val contr_tac : int -> tactic ``` lcp@681 ` 45` ``` val depth_tac : claset -> int -> int -> tactic ``` lcp@681 ` 46` ``` val deepen_tac : claset -> int -> int -> tactic ``` lcp@681 ` 47` ``` val dup_elim : thm -> thm ``` lcp@681 ` 48` ``` val dup_intr : thm -> thm ``` lcp@681 ` 49` ``` val dup_step_tac : claset -> int -> tactic ``` lcp@681 ` 50` ``` val eq_mp_tac : int -> tactic ``` lcp@681 ` 51` ``` val fast_tac : claset -> int -> tactic ``` lcp@681 ` 52` ``` val haz_step_tac : claset -> int -> tactic ``` lcp@681 ` 53` ``` val joinrules : thm list * thm list -> (bool * thm) list ``` lcp@681 ` 54` ``` val mp_tac : int -> tactic ``` lcp@681 ` 55` ``` val safe_tac : claset -> tactic ``` lcp@681 ` 56` ``` val safe_step_tac : claset -> int -> tactic ``` lcp@681 ` 57` ``` val slow_step_tac : claset -> int -> tactic ``` lcp@681 ` 58` ``` val slow_best_tac : claset -> int -> tactic ``` lcp@681 ` 59` ``` val slow_tac : claset -> int -> tactic ``` lcp@681 ` 60` ``` val step_tac : claset -> int -> tactic ``` lcp@681 ` 61` ``` val swap : thm (* ~P ==> (~Q ==> P) ==> Q *) ``` lcp@681 ` 62` ``` val swapify : thm list -> thm list ``` lcp@681 ` 63` ``` val swap_res_tac : thm list -> int -> tactic ``` lcp@681 ` 64` ``` val inst_step_tac : claset -> int -> tactic ``` clasohm@0 ` 65` ``` end; ``` clasohm@0 ` 66` clasohm@0 ` 67` clasohm@0 ` 68` ```functor ClassicalFun(Data: CLASSICAL_DATA): CLASSICAL = ``` clasohm@0 ` 69` ```struct ``` clasohm@0 ` 70` clasohm@0 ` 71` ```local open Data in ``` clasohm@0 ` 72` clasohm@0 ` 73` ```(** Useful tactics for classical reasoning **) ``` clasohm@0 ` 74` clasohm@0 ` 75` ```val imp_elim = make_elim mp; ``` clasohm@0 ` 76` clasohm@0 ` 77` ```(*Solve goal that assumes both P and ~P. *) ``` clasohm@0 ` 78` ```val contr_tac = eresolve_tac [not_elim] THEN' assume_tac; ``` clasohm@0 ` 79` lcp@681 ` 80` ```(*Finds P-->Q and P in the assumptions, replaces implication by Q. ``` lcp@681 ` 81` ``` Could do the same thing for P<->Q and P... *) ``` lcp@681 ` 82` ```fun mp_tac i = eresolve_tac [not_elim, imp_elim] i THEN assume_tac i; ``` clasohm@0 ` 83` clasohm@0 ` 84` ```(*Like mp_tac but instantiates no variables*) ``` lcp@681 ` 85` ```fun eq_mp_tac i = ematch_tac [not_elim, imp_elim] i THEN eq_assume_tac i; ``` lcp@681 ` 86` lcp@681 ` 87` ```val swap = rule_by_tactic (etac thin_rl 1) (not_elim RS classical); ``` clasohm@0 ` 88` clasohm@0 ` 89` ```(*Creates rules to eliminate ~A, from rules to introduce A*) ``` clasohm@0 ` 90` ```fun swapify intrs = intrs RLN (2, [swap]); ``` clasohm@0 ` 91` clasohm@0 ` 92` ```(*Uses introduction rules in the normal way, or on negated assumptions, ``` clasohm@0 ` 93` ``` trying rules in order. *) ``` clasohm@0 ` 94` ```fun swap_res_tac rls = ``` lcp@54 ` 95` ``` let fun addrl (rl,brls) = (false, rl) :: (true, rl RSN (2,swap)) :: brls ``` lcp@54 ` 96` ``` in assume_tac ORELSE' ``` lcp@54 ` 97` ``` contr_tac ORELSE' ``` lcp@54 ` 98` ``` biresolve_tac (foldr addrl (rls,[])) ``` clasohm@0 ` 99` ``` end; ``` clasohm@0 ` 100` lcp@681 ` 101` ```(*Duplication of hazardous rules, for complete provers*) ``` lcp@681 ` 102` ```fun dup_intr th = standard (th RS classical); ``` lcp@681 ` 103` lcp@681 ` 104` ```fun dup_elim th = th RSN (2, revcut_rl) |> assumption 2 |> Sequence.hd |> ``` lcp@681 ` 105` ``` rule_by_tactic (TRYALL (etac revcut_rl)); ``` clasohm@0 ` 106` clasohm@0 ` 107` ```(*** Classical rule sets ***) ``` clasohm@0 ` 108` clasohm@0 ` 109` ```type netpair = (int*(bool*thm)) Net.net * (int*(bool*thm)) Net.net; ``` clasohm@0 ` 110` clasohm@0 ` 111` ```datatype claset = ``` clasohm@0 ` 112` ``` CS of {safeIs : thm list, ``` clasohm@0 ` 113` ``` safeEs : thm list, ``` clasohm@0 ` 114` ``` hazIs : thm list, ``` clasohm@0 ` 115` ``` hazEs : thm list, ``` clasohm@0 ` 116` ``` safe0_netpair : netpair, ``` clasohm@0 ` 117` ``` safep_netpair : netpair, ``` lcp@681 ` 118` ``` haz_netpair : netpair, ``` lcp@681 ` 119` ``` dup_netpair : netpair}; ``` clasohm@0 ` 120` clasohm@0 ` 121` ```fun rep_claset (CS{safeIs,safeEs,hazIs,hazEs,...}) = ``` clasohm@0 ` 122` ``` {safeIs=safeIs, safeEs=safeEs, hazIs=hazIs, hazEs=hazEs}; ``` clasohm@0 ` 123` clasohm@0 ` 124` ```(*For use with biresolve_tac. Combines intrs with swap to catch negated ``` clasohm@0 ` 125` ``` assumptions; pairs elims with true; sorts. *) ``` clasohm@0 ` 126` ```fun joinrules (intrs,elims) = ``` clasohm@0 ` 127` ``` sort lessb ``` clasohm@0 ` 128` ``` (map (pair true) (elims @ swapify intrs) @ ``` clasohm@0 ` 129` ``` map (pair false) intrs); ``` clasohm@0 ` 130` lcp@681 ` 131` ```val build = build_netpair(Net.empty,Net.empty); ``` lcp@681 ` 132` clasohm@0 ` 133` ```(*Make a claset from the four kinds of rules*) ``` clasohm@0 ` 134` ```fun make_cs {safeIs,safeEs,hazIs,hazEs} = ``` clasohm@0 ` 135` ``` let val (safe0_brls, safep_brls) = (*0 subgoals vs 1 or more*) ``` clasohm@0 ` 136` ``` take_prefix (fn brl => subgoals_of_brl brl=0) ``` clasohm@0 ` 137` ``` (joinrules(safeIs, safeEs)) ``` clasohm@0 ` 138` ``` in CS{safeIs = safeIs, ``` clasohm@0 ` 139` ``` safeEs = safeEs, ``` clasohm@0 ` 140` ``` hazIs = hazIs, ``` clasohm@0 ` 141` ``` hazEs = hazEs, ``` lcp@681 ` 142` ``` safe0_netpair = build safe0_brls, ``` lcp@681 ` 143` ``` safep_netpair = build safep_brls, ``` lcp@681 ` 144` ``` haz_netpair = build (joinrules(hazIs, hazEs)), ``` lcp@681 ` 145` ``` dup_netpair = build (joinrules(map dup_intr hazIs, ``` lcp@681 ` 146` ``` map dup_elim hazEs))} ``` clasohm@0 ` 147` ``` end; ``` clasohm@0 ` 148` clasohm@0 ` 149` ```(*** Manipulation of clasets ***) ``` clasohm@0 ` 150` clasohm@0 ` 151` ```val empty_cs = make_cs{safeIs=[], safeEs=[], hazIs=[], hazEs=[]}; ``` clasohm@0 ` 152` clasohm@0 ` 153` ```fun print_cs (CS{safeIs,safeEs,hazIs,hazEs,...}) = ``` clasohm@0 ` 154` ``` (writeln"Introduction rules"; prths hazIs; ``` clasohm@0 ` 155` ``` writeln"Safe introduction rules"; prths safeIs; ``` clasohm@0 ` 156` ``` writeln"Elimination rules"; prths hazEs; ``` clasohm@0 ` 157` ``` writeln"Safe elimination rules"; prths safeEs; ``` clasohm@0 ` 158` ``` ()); ``` clasohm@0 ` 159` clasohm@0 ` 160` ```fun (CS{safeIs,safeEs,hazIs,hazEs,...}) addSIs ths = ``` clasohm@0 ` 161` ``` make_cs {safeIs=ths@safeIs, safeEs=safeEs, hazIs=hazIs, hazEs=hazEs}; ``` clasohm@0 ` 162` clasohm@0 ` 163` ```fun (CS{safeIs,safeEs,hazIs,hazEs,...}) addSEs ths = ``` clasohm@0 ` 164` ``` make_cs {safeIs=safeIs, safeEs=ths@safeEs, hazIs=hazIs, hazEs=hazEs}; ``` clasohm@0 ` 165` clasohm@0 ` 166` ```fun cs addSDs ths = cs addSEs (map make_elim ths); ``` clasohm@0 ` 167` clasohm@0 ` 168` ```fun (CS{safeIs,safeEs,hazIs,hazEs,...}) addIs ths = ``` clasohm@0 ` 169` ``` make_cs {safeIs=safeIs, safeEs=safeEs, hazIs=ths@hazIs, hazEs=hazEs}; ``` clasohm@0 ` 170` clasohm@0 ` 171` ```fun (CS{safeIs,safeEs,hazIs,hazEs,...}) addEs ths = ``` clasohm@0 ` 172` ``` make_cs {safeIs=safeIs, safeEs=safeEs, hazIs=hazIs, hazEs=ths@hazEs}; ``` clasohm@0 ` 173` clasohm@0 ` 174` ```fun cs addDs ths = cs addEs (map make_elim ths); ``` clasohm@0 ` 175` clasohm@0 ` 176` ```(*** Simple tactics for theorem proving ***) ``` clasohm@0 ` 177` clasohm@0 ` 178` ```(*Attack subgoals using safe inferences -- matching, not resolution*) ``` clasohm@0 ` 179` ```fun safe_step_tac (CS{safe0_netpair,safep_netpair,...}) = ``` clasohm@0 ` 180` ``` FIRST' [eq_assume_tac, ``` clasohm@0 ` 181` ``` eq_mp_tac, ``` clasohm@0 ` 182` ``` bimatch_from_nets_tac safe0_netpair, ``` clasohm@0 ` 183` ``` FIRST' hyp_subst_tacs, ``` clasohm@0 ` 184` ``` bimatch_from_nets_tac safep_netpair] ; ``` clasohm@0 ` 185` clasohm@0 ` 186` ```(*Repeatedly attack subgoals using safe inferences -- it's deterministic!*) ``` clasohm@0 ` 187` ```fun safe_tac cs = DETERM (REPEAT_FIRST (safe_step_tac cs)); ``` clasohm@0 ` 188` clasohm@0 ` 189` ```(*These steps could instantiate variables and are therefore unsafe.*) ``` clasohm@0 ` 190` ```fun inst_step_tac (CS{safe0_netpair,safep_netpair,...}) = ``` clasohm@0 ` 191` ``` assume_tac APPEND' ``` clasohm@0 ` 192` ``` contr_tac APPEND' ``` clasohm@0 ` 193` ``` biresolve_from_nets_tac safe0_netpair APPEND' ``` clasohm@0 ` 194` ``` biresolve_from_nets_tac safep_netpair; ``` clasohm@0 ` 195` lcp@681 ` 196` ```fun haz_step_tac (cs as (CS{haz_netpair,...})) = ``` lcp@681 ` 197` ``` biresolve_from_nets_tac haz_netpair; ``` lcp@681 ` 198` clasohm@0 ` 199` ```(*Single step for the prover. FAILS unless it makes progress. *) ``` lcp@681 ` 200` ```fun step_tac cs i = ``` lcp@681 ` 201` ``` FIRST [safe_tac cs, inst_step_tac cs i, haz_step_tac cs i]; ``` clasohm@0 ` 202` clasohm@0 ` 203` ```(*Using a "safe" rule to instantiate variables is unsafe. This tactic ``` clasohm@0 ` 204` ``` allows backtracking from "safe" rules to "unsafe" rules here.*) ``` lcp@681 ` 205` ```fun slow_step_tac cs i = ``` lcp@681 ` 206` ``` safe_tac cs ORELSE (inst_step_tac cs i APPEND haz_step_tac cs i); ``` clasohm@0 ` 207` clasohm@0 ` 208` ```(*** The following tactics all fail unless they solve one goal ***) ``` clasohm@0 ` 209` clasohm@0 ` 210` ```(*Dumb but fast*) ``` clasohm@0 ` 211` ```fun fast_tac cs = SELECT_GOAL (DEPTH_SOLVE (step_tac cs 1)); ``` clasohm@0 ` 212` clasohm@0 ` 213` ```(*Slower but smarter than fast_tac*) ``` clasohm@0 ` 214` ```fun best_tac cs = ``` clasohm@0 ` 215` ``` SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, sizef) (step_tac cs 1)); ``` clasohm@0 ` 216` clasohm@0 ` 217` ```fun slow_tac cs = SELECT_GOAL (DEPTH_SOLVE (slow_step_tac cs 1)); ``` clasohm@0 ` 218` clasohm@0 ` 219` ```fun slow_best_tac cs = ``` clasohm@0 ` 220` ``` SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, sizef) (slow_step_tac cs 1)); ``` clasohm@0 ` 221` lcp@681 ` 222` lcp@681 ` 223` ```(*** Complete(?) tactic, loosely based upon LeanTaP ***) ``` lcp@681 ` 224` lcp@681 ` 225` ```(*Not deterministic. A different approach would always expand the first ``` lcp@681 ` 226` ``` unsafe connective. That's harder in Isabelle because etac can pick up ``` lcp@681 ` 227` ``` any assumption. One way is to express *all* unsafe connectives in terms ``` lcp@681 ` 228` ``` of universal quantification.*) ``` lcp@681 ` 229` ```fun dup_step_tac (cs as (CS{dup_netpair,...})) = ``` lcp@681 ` 230` ``` biresolve_from_nets_tac dup_netpair; ``` lcp@681 ` 231` lcp@681 ` 232` ```(*Searching to depth m of duplicative steps ``` lcp@681 ` 233` ``` Uses DEPTH_SOLVE (tac 1) instead of (ALLGOALS tac) since the latter ``` lcp@681 ` 234` ``` solves the subgoals in reverse order!*) ``` lcp@681 ` 235` ```fun depth_tac cs m = ``` lcp@681 ` 236` ``` SUBGOAL ``` lcp@681 ` 237` ``` (fn (prem,i) => ``` lcp@681 ` 238` ``` let val deti = ``` lcp@681 ` 239` ``` (*No Vars in the goal? No need to backtrack between goals.*) ``` lcp@681 ` 240` ``` case term_vars prem of ``` lcp@681 ` 241` ``` [] => DETERM ``` lcp@681 ` 242` ``` | _::_ => I ``` lcp@681 ` 243` ``` in SELECT_GOAL (TRY (safe_tac cs) THEN ``` lcp@681 ` 244` ``` DEPTH_SOLVE (deti (depth_aux_tac cs m 1))) i ``` lcp@681 ` 245` ``` end) ``` lcp@681 ` 246` ```and depth_aux_tac cs m = ``` lcp@681 ` 247` ``` SELECT_GOAL ``` lcp@681 ` 248` ``` (inst_step_tac cs 1 THEN DEPTH_SOLVE (depth_tac cs m 1) ``` lcp@681 ` 249` ``` APPEND ``` lcp@681 ` 250` ``` COND (K(m=0)) no_tac ``` lcp@681 ` 251` ``` (dup_step_tac cs 1 THEN DEPTH_SOLVE (depth_tac cs (m-1) 1))); ``` lcp@681 ` 252` lcp@681 ` 253` ```fun deepen_tac cs m i = STATE(fn state => ``` lcp@681 ` 254` ``` if has_fewer_prems i state then no_tac ``` lcp@681 ` 255` ``` else (writeln ("Depth = " ^ string_of_int m); ``` lcp@681 ` 256` ``` depth_tac cs m i ORELSE deepen_tac cs (m+1) i)); ``` lcp@681 ` 257` clasohm@0 ` 258` ```end; ``` clasohm@0 ` 259` ```end; ```