src/Provers/classical.ML
 author clasohm Thu Sep 16 12:20:38 1993 +0200 (1993-09-16 ago) changeset 0 a5a9c433f639 child 54 3dea30013b58 permissions -rw-r--r--
Initial revision
 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 ``` clasohm@0 ` 19` ``` val mp: thm (* [| P-->Q; P |] ==> Q *) ``` clasohm@0 ` 20` ``` val not_elim: thm (* [| ~P; P |] ==> R *) ``` clasohm@0 ` 21` ``` val swap: thm (* ~P ==> (~Q ==> P) ==> Q *) ``` clasohm@0 ` 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 ``` clasohm@0 ` 33` ``` val empty_cs: claset ``` clasohm@0 ` 34` ``` val addDs : claset * thm list -> claset ``` clasohm@0 ` 35` ``` val addEs : claset * thm list -> claset ``` clasohm@0 ` 36` ``` val addIs : claset * thm list -> claset ``` clasohm@0 ` 37` ``` val addSDs: claset * thm list -> claset ``` clasohm@0 ` 38` ``` val addSEs: claset * thm list -> claset ``` clasohm@0 ` 39` ``` val addSIs: claset * thm list -> claset ``` clasohm@0 ` 40` ``` val print_cs: claset -> unit ``` clasohm@0 ` 41` ``` val rep_claset: claset -> ``` clasohm@0 ` 42` ``` {safeIs: thm list, safeEs: thm list, hazIs: thm list, hazEs: thm list} ``` clasohm@0 ` 43` ``` val best_tac : claset -> int -> tactic ``` clasohm@0 ` 44` ``` val chain_tac : int -> tactic ``` clasohm@0 ` 45` ``` val contr_tac : int -> tactic ``` clasohm@0 ` 46` ``` val eq_mp_tac: int -> tactic ``` clasohm@0 ` 47` ``` val fast_tac : claset -> int -> tactic ``` clasohm@0 ` 48` ``` val joinrules : thm list * thm list -> (bool * thm) list ``` clasohm@0 ` 49` ``` val mp_tac: int -> tactic ``` clasohm@0 ` 50` ``` val safe_tac : claset -> tactic ``` clasohm@0 ` 51` ``` val safe_step_tac : claset -> int -> tactic ``` clasohm@0 ` 52` ``` val slow_step_tac : claset -> int -> tactic ``` clasohm@0 ` 53` ``` val slow_best_tac : claset -> int -> tactic ``` clasohm@0 ` 54` ``` val slow_tac : claset -> int -> tactic ``` clasohm@0 ` 55` ``` val step_tac : claset -> int -> tactic ``` clasohm@0 ` 56` ``` val swapify : thm list -> thm list ``` clasohm@0 ` 57` ``` val swap_res_tac : thm list -> int -> tactic ``` clasohm@0 ` 58` ``` val inst_step_tac : claset -> int -> tactic ``` clasohm@0 ` 59` ``` end; ``` clasohm@0 ` 60` clasohm@0 ` 61` clasohm@0 ` 62` ```functor ClassicalFun(Data: CLASSICAL_DATA): CLASSICAL = ``` clasohm@0 ` 63` ```struct ``` clasohm@0 ` 64` clasohm@0 ` 65` ```local open Data in ``` clasohm@0 ` 66` clasohm@0 ` 67` ```(** Useful tactics for classical reasoning **) ``` clasohm@0 ` 68` clasohm@0 ` 69` ```val imp_elim = make_elim mp; ``` clasohm@0 ` 70` clasohm@0 ` 71` ```(*Solve goal that assumes both P and ~P. *) ``` clasohm@0 ` 72` ```val contr_tac = eresolve_tac [not_elim] THEN' assume_tac; ``` clasohm@0 ` 73` clasohm@0 ` 74` ```(*Finds P-->Q and P in the assumptions, replaces implication by Q *) ``` clasohm@0 ` 75` ```fun mp_tac i = eresolve_tac ([not_elim,imp_elim]) i THEN assume_tac i; ``` clasohm@0 ` 76` clasohm@0 ` 77` ```(*Like mp_tac but instantiates no variables*) ``` clasohm@0 ` 78` ```fun eq_mp_tac i = ematch_tac ([not_elim,imp_elim]) i THEN eq_assume_tac i; ``` clasohm@0 ` 79` clasohm@0 ` 80` ```(*Creates rules to eliminate ~A, from rules to introduce A*) ``` clasohm@0 ` 81` ```fun swapify intrs = intrs RLN (2, [swap]); ``` clasohm@0 ` 82` clasohm@0 ` 83` ```(*Uses introduction rules in the normal way, or on negated assumptions, ``` clasohm@0 ` 84` ``` trying rules in order. *) ``` clasohm@0 ` 85` ```fun swap_res_tac rls = ``` clasohm@0 ` 86` ``` let fun tacf rl = rtac rl ORELSE' etac (rl RSN (2,swap)) ``` clasohm@0 ` 87` ``` in assume_tac ORELSE' contr_tac ORELSE' FIRST' (map tacf rls) ``` clasohm@0 ` 88` ``` end; ``` clasohm@0 ` 89` clasohm@0 ` 90` ```(*Given assumption P-->Q, reduces subgoal Q to P [deletes the implication!] *) ``` clasohm@0 ` 91` ```fun chain_tac i = ``` clasohm@0 ` 92` ``` eresolve_tac [imp_elim] i THEN ``` clasohm@0 ` 93` ``` (assume_tac (i+1) ORELSE contr_tac (i+1)); ``` clasohm@0 ` 94` clasohm@0 ` 95` ```(*** Classical rule sets ***) ``` clasohm@0 ` 96` clasohm@0 ` 97` ```type netpair = (int*(bool*thm)) Net.net * (int*(bool*thm)) Net.net; ``` clasohm@0 ` 98` clasohm@0 ` 99` ```datatype claset = ``` clasohm@0 ` 100` ``` CS of {safeIs : thm list, ``` clasohm@0 ` 101` ``` safeEs : thm list, ``` clasohm@0 ` 102` ``` hazIs : thm list, ``` clasohm@0 ` 103` ``` hazEs : thm list, ``` clasohm@0 ` 104` ``` safe0_netpair : netpair, ``` clasohm@0 ` 105` ``` safep_netpair : netpair, ``` clasohm@0 ` 106` ``` haz_netpair : netpair}; ``` clasohm@0 ` 107` clasohm@0 ` 108` ```fun rep_claset (CS{safeIs,safeEs,hazIs,hazEs,...}) = ``` clasohm@0 ` 109` ``` {safeIs=safeIs, safeEs=safeEs, hazIs=hazIs, hazEs=hazEs}; ``` clasohm@0 ` 110` clasohm@0 ` 111` ```(*For use with biresolve_tac. Combines intrs with swap to catch negated ``` clasohm@0 ` 112` ``` assumptions; pairs elims with true; sorts. *) ``` clasohm@0 ` 113` ```fun joinrules (intrs,elims) = ``` clasohm@0 ` 114` ``` sort lessb ``` clasohm@0 ` 115` ``` (map (pair true) (elims @ swapify intrs) @ ``` clasohm@0 ` 116` ``` map (pair false) intrs); ``` clasohm@0 ` 117` clasohm@0 ` 118` ```(*Make a claset from the four kinds of rules*) ``` clasohm@0 ` 119` ```fun make_cs {safeIs,safeEs,hazIs,hazEs} = ``` clasohm@0 ` 120` ``` let val (safe0_brls, safep_brls) = (*0 subgoals vs 1 or more*) ``` clasohm@0 ` 121` ``` take_prefix (fn brl => subgoals_of_brl brl=0) ``` clasohm@0 ` 122` ``` (joinrules(safeIs, safeEs)) ``` clasohm@0 ` 123` ``` in CS{safeIs = safeIs, ``` clasohm@0 ` 124` ``` safeEs = safeEs, ``` clasohm@0 ` 125` ``` hazIs = hazIs, ``` clasohm@0 ` 126` ``` hazEs = hazEs, ``` clasohm@0 ` 127` ``` safe0_netpair = build_netpair safe0_brls, ``` clasohm@0 ` 128` ``` safep_netpair = build_netpair safep_brls, ``` clasohm@0 ` 129` ``` haz_netpair = build_netpair (joinrules(hazIs, hazEs))} ``` clasohm@0 ` 130` ``` end; ``` clasohm@0 ` 131` clasohm@0 ` 132` ```(*** Manipulation of clasets ***) ``` clasohm@0 ` 133` clasohm@0 ` 134` ```val empty_cs = make_cs{safeIs=[], safeEs=[], hazIs=[], hazEs=[]}; ``` clasohm@0 ` 135` clasohm@0 ` 136` ```fun print_cs (CS{safeIs,safeEs,hazIs,hazEs,...}) = ``` clasohm@0 ` 137` ``` (writeln"Introduction rules"; prths hazIs; ``` clasohm@0 ` 138` ``` writeln"Safe introduction rules"; prths safeIs; ``` clasohm@0 ` 139` ``` writeln"Elimination rules"; prths hazEs; ``` clasohm@0 ` 140` ``` writeln"Safe elimination rules"; prths safeEs; ``` clasohm@0 ` 141` ``` ()); ``` clasohm@0 ` 142` clasohm@0 ` 143` ```fun (CS{safeIs,safeEs,hazIs,hazEs,...}) addSIs ths = ``` clasohm@0 ` 144` ``` make_cs {safeIs=ths@safeIs, safeEs=safeEs, hazIs=hazIs, hazEs=hazEs}; ``` clasohm@0 ` 145` clasohm@0 ` 146` ```fun (CS{safeIs,safeEs,hazIs,hazEs,...}) addSEs ths = ``` clasohm@0 ` 147` ``` make_cs {safeIs=safeIs, safeEs=ths@safeEs, hazIs=hazIs, hazEs=hazEs}; ``` clasohm@0 ` 148` clasohm@0 ` 149` ```fun cs addSDs ths = cs addSEs (map make_elim ths); ``` clasohm@0 ` 150` clasohm@0 ` 151` ```fun (CS{safeIs,safeEs,hazIs,hazEs,...}) addIs ths = ``` clasohm@0 ` 152` ``` make_cs {safeIs=safeIs, safeEs=safeEs, hazIs=ths@hazIs, hazEs=hazEs}; ``` clasohm@0 ` 153` clasohm@0 ` 154` ```fun (CS{safeIs,safeEs,hazIs,hazEs,...}) addEs ths = ``` clasohm@0 ` 155` ``` make_cs {safeIs=safeIs, safeEs=safeEs, hazIs=hazIs, hazEs=ths@hazEs}; ``` clasohm@0 ` 156` clasohm@0 ` 157` ```fun cs addDs ths = cs addEs (map make_elim ths); ``` clasohm@0 ` 158` clasohm@0 ` 159` ```(*** Simple tactics for theorem proving ***) ``` clasohm@0 ` 160` clasohm@0 ` 161` ```(*Attack subgoals using safe inferences -- matching, not resolution*) ``` clasohm@0 ` 162` ```fun safe_step_tac (CS{safe0_netpair,safep_netpair,...}) = ``` clasohm@0 ` 163` ``` FIRST' [eq_assume_tac, ``` clasohm@0 ` 164` ``` eq_mp_tac, ``` clasohm@0 ` 165` ``` bimatch_from_nets_tac safe0_netpair, ``` clasohm@0 ` 166` ``` FIRST' hyp_subst_tacs, ``` clasohm@0 ` 167` ``` bimatch_from_nets_tac safep_netpair] ; ``` clasohm@0 ` 168` clasohm@0 ` 169` ```(*Repeatedly attack subgoals using safe inferences -- it's deterministic!*) ``` clasohm@0 ` 170` ```fun safe_tac cs = DETERM (REPEAT_FIRST (safe_step_tac cs)); ``` clasohm@0 ` 171` clasohm@0 ` 172` ```(*These steps could instantiate variables and are therefore unsafe.*) ``` clasohm@0 ` 173` ```fun inst_step_tac (CS{safe0_netpair,safep_netpair,...}) = ``` clasohm@0 ` 174` ``` assume_tac APPEND' ``` clasohm@0 ` 175` ``` contr_tac APPEND' ``` clasohm@0 ` 176` ``` biresolve_from_nets_tac safe0_netpair APPEND' ``` clasohm@0 ` 177` ``` biresolve_from_nets_tac safep_netpair; ``` clasohm@0 ` 178` clasohm@0 ` 179` ```(*Single step for the prover. FAILS unless it makes progress. *) ``` clasohm@0 ` 180` ```fun step_tac (cs as (CS{haz_netpair,...})) i = ``` clasohm@0 ` 181` ``` FIRST [safe_tac cs, ``` clasohm@0 ` 182` ``` inst_step_tac cs i, ``` clasohm@0 ` 183` ``` biresolve_from_nets_tac haz_netpair i]; ``` clasohm@0 ` 184` clasohm@0 ` 185` ```(*Using a "safe" rule to instantiate variables is unsafe. This tactic ``` clasohm@0 ` 186` ``` allows backtracking from "safe" rules to "unsafe" rules here.*) ``` clasohm@0 ` 187` ```fun slow_step_tac (cs as (CS{haz_netpair,...})) i = ``` clasohm@0 ` 188` ``` safe_tac cs ORELSE ``` clasohm@0 ` 189` ``` (inst_step_tac cs i APPEND biresolve_from_nets_tac haz_netpair i); ``` clasohm@0 ` 190` clasohm@0 ` 191` ```(*** The following tactics all fail unless they solve one goal ***) ``` clasohm@0 ` 192` clasohm@0 ` 193` ```(*Dumb but fast*) ``` clasohm@0 ` 194` ```fun fast_tac cs = SELECT_GOAL (DEPTH_SOLVE (step_tac cs 1)); ``` clasohm@0 ` 195` clasohm@0 ` 196` ```(*Slower but smarter than fast_tac*) ``` clasohm@0 ` 197` ```fun best_tac cs = ``` clasohm@0 ` 198` ``` SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, sizef) (step_tac cs 1)); ``` clasohm@0 ` 199` clasohm@0 ` 200` ```fun slow_tac cs = SELECT_GOAL (DEPTH_SOLVE (slow_step_tac cs 1)); ``` clasohm@0 ` 201` clasohm@0 ` 202` ```fun slow_best_tac cs = ``` clasohm@0 ` 203` ``` SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, sizef) (slow_step_tac cs 1)); ``` clasohm@0 ` 204` clasohm@0 ` 205` ```end; ``` clasohm@0 ` 206` ```end; ```