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