1(* Title: Sequents/prover.ML 2 Author: Lawrence C Paulson, Cambridge University Computer Laboratory 3 Copyright 1992 University of Cambridge 4 5Simple classical reasoner for the sequent calculus, based on "theorem packs". 6*) 7 8signature CLA = 9sig 10 type pack 11 val empty_pack: pack 12 val get_pack: Proof.context -> pack 13 val put_pack: pack -> Proof.context -> Proof.context 14 val pretty_pack: Proof.context -> Pretty.T 15 val add_safe: thm -> Proof.context -> Proof.context 16 val add_unsafe: thm -> Proof.context -> Proof.context 17 val safe_add: attribute 18 val unsafe_add: attribute 19 val method: (Proof.context -> int -> tactic) -> (Proof.context -> Proof.method) context_parser 20 val trace: bool Config.T 21 val forms_of_seq: term -> term list 22 val safe_tac: Proof.context -> int -> tactic 23 val step_tac: Proof.context -> int -> tactic 24 val pc_tac: Proof.context -> int -> tactic 25 val fast_tac: Proof.context -> int -> tactic 26 val best_tac: Proof.context -> int -> tactic 27end; 28 29structure Cla: CLA = 30struct 31 32(** rule declarations **) 33 34(*A theorem pack has the form (safe rules, unsafe rules) 35 An unsafe rule is incomplete or introduces variables in subgoals, 36 and is tried only when the safe rules are not applicable. *) 37 38fun less (rl1, rl2) = Thm.nprems_of rl1 < Thm.nprems_of rl2; 39val sort_rules = sort (make_ord less); 40 41datatype pack = Pack of thm list * thm list; 42 43val empty_pack = Pack ([], []); 44 45structure Pack = Generic_Data 46( 47 type T = pack; 48 val empty = empty_pack; 49 val extend = I; 50 fun merge (Pack (safes, unsafes), Pack (safes', unsafes')) = 51 Pack 52 (sort_rules (Thm.merge_thms (safes, safes')), 53 sort_rules (Thm.merge_thms (unsafes, unsafes'))); 54); 55 56val put_pack = Context.proof_map o Pack.put; 57val get_pack = Pack.get o Context.Proof; 58fun get_rules ctxt = let val Pack rules = get_pack ctxt in rules end; 59 60 61(* print pack *) 62 63fun pretty_pack ctxt = 64 let val (safes, unsafes) = get_rules ctxt in 65 Pretty.chunks 66 [Pretty.big_list "safe rules:" (map (Thm.pretty_thm ctxt) safes), 67 Pretty.big_list "unsafe rules:" (map (Thm.pretty_thm ctxt) unsafes)] 68 end; 69 70val _ = 71 Outer_Syntax.command \<^command_keyword>\<open>print_pack\<close> "print pack of classical rules" 72 (Scan.succeed (Toplevel.keep (Pretty.writeln o pretty_pack o Toplevel.context_of))); 73 74 75(* declare rules *) 76 77fun add_rule which th context = context |> Pack.map (fn Pack rules => 78 Pack (rules |> which (fn ths => 79 if member Thm.eq_thm_prop ths th then 80 let 81 val _ = 82 (case context of 83 Context.Proof ctxt => 84 if Context_Position.is_really_visible ctxt then 85 warning ("Ignoring duplicate theorems:\n" ^ Thm.string_of_thm ctxt th) 86 else () 87 | _ => ()); 88 in ths end 89 else sort_rules (th :: ths)))); 90 91val add_safe = Context.proof_map o add_rule apfst; 92val add_unsafe = Context.proof_map o add_rule apsnd; 93 94 95(* attributes *) 96 97val safe_add = Thm.declaration_attribute (add_rule apfst); 98val unsafe_add = Thm.declaration_attribute (add_rule apsnd); 99 100val _ = Theory.setup 101 (Attrib.setup \<^binding>\<open>safe\<close> (Scan.succeed safe_add) "" #> 102 Attrib.setup \<^binding>\<open>unsafe\<close> (Scan.succeed unsafe_add) ""); 103 104 105(* proof method syntax *) 106 107fun method tac = 108 Method.sections 109 [Args.$$$ "add" -- Args.bang_colon >> K (Method.modifier safe_add \<^here>), 110 Args.$$$ "add" -- Args.colon >> K (Method.modifier unsafe_add \<^here>)] 111 >> K (SIMPLE_METHOD' o tac); 112 113 114(** tactics **) 115 116val trace = Attrib.setup_config_bool \<^binding>\<open>cla_trace\<close> (K false); 117 118 119(*Returns the list of all formulas in the sequent*) 120fun forms_of_seq (Const(\<^const_name>\<open>SeqO'\<close>,_) $ P $ u) = P :: forms_of_seq u 121 | forms_of_seq (H $ u) = forms_of_seq u 122 | forms_of_seq _ = []; 123 124(*Tests whether two sequences (left or right sides) could be resolved. 125 seqp is a premise (subgoal), seqc is a conclusion of an object-rule. 126 Assumes each formula in seqc is surrounded by sequence variables 127 -- checks that each concl formula looks like some subgoal formula. 128 It SHOULD check order as well, using recursion rather than forall/exists*) 129fun could_res (seqp,seqc) = 130 forall (fn Qc => exists (fn Qp => Term.could_unify (Qp,Qc)) 131 (forms_of_seq seqp)) 132 (forms_of_seq seqc); 133 134(*Tests whether two sequents or pairs of sequents could be resolved*) 135fun could_resolve_seq (prem,conc) = 136 case (prem,conc) of 137 (_ $ Abs(_,_,leftp) $ Abs(_,_,rightp), 138 _ $ Abs(_,_,leftc) $ Abs(_,_,rightc)) => 139 could_res (leftp,leftc) andalso could_res (rightp,rightc) 140 | (_ $ Abs(_,_,leftp) $ rightp, 141 _ $ Abs(_,_,leftc) $ rightc) => 142 could_res (leftp,leftc) andalso Term.could_unify (rightp,rightc) 143 | _ => false; 144 145 146(*Like filt_resolve_tac, using could_resolve_seq 147 Much faster than resolve_tac when there are many rules. 148 Resolve subgoal i using the rules, unless more than maxr are compatible. *) 149fun filseq_resolve_tac ctxt rules maxr = SUBGOAL(fn (prem,i) => 150 let val rls = filter_thms could_resolve_seq (maxr+1, prem, rules) 151 in if length rls > maxr then no_tac 152 else (*((rtac derelict 1 THEN rtac impl 1 153 THEN (rtac identity 2 ORELSE rtac ll_mp 2) 154 THEN rtac context1 1) 155 ORELSE *) resolve_tac ctxt rls i 156 end); 157 158 159(*Predicate: does the rule have n premises? *) 160fun has_prems n rule = (Thm.nprems_of rule = n); 161 162(*Continuation-style tactical for resolution. 163 The list of rules is partitioned into 0, 1, 2 premises. 164 The resulting tactic, gtac, tries to resolve with rules. 165 If successful, it recursively applies nextac to the new subgoals only. 166 Else fails. (Treatment of goals due to Ph. de Groote) 167 Bind (RESOLVE_THEN rules) to a variable: it preprocesses the rules. *) 168 169(*Takes rule lists separated in to 0, 1, 2, >2 premises. 170 The abstraction over state prevents needless divergence in recursion. 171 The 9999 should be a parameter, to delay treatment of flexible goals. *) 172 173fun RESOLVE_THEN ctxt rules = 174 let val [rls0,rls1,rls2] = partition_list has_prems 0 2 rules; 175 fun tac nextac i state = state |> 176 (filseq_resolve_tac ctxt rls0 9999 i 177 ORELSE 178 (DETERM(filseq_resolve_tac ctxt rls1 9999 i) THEN TRY(nextac i)) 179 ORELSE 180 (DETERM(filseq_resolve_tac ctxt rls2 9999 i) THEN TRY(nextac(i+1)) 181 THEN TRY(nextac i))) 182 in tac end; 183 184 185 186(*repeated resolution applied to the designated goal*) 187fun reresolve_tac ctxt rules = 188 let 189 val restac = RESOLVE_THEN ctxt rules; (*preprocessing done now*) 190 fun gtac i = restac gtac i; 191 in gtac end; 192 193(*tries the safe rules repeatedly before the unsafe rules. *) 194fun repeat_goal_tac ctxt = 195 let 196 val (safes, unsafes) = get_rules ctxt; 197 val restac = RESOLVE_THEN ctxt safes; 198 val lastrestac = RESOLVE_THEN ctxt unsafes; 199 fun gtac i = 200 restac gtac i ORELSE 201 (if Config.get ctxt trace then print_tac ctxt "" THEN lastrestac gtac i 202 else lastrestac gtac i) 203 in gtac end; 204 205 206(*Tries safe rules only*) 207fun safe_tac ctxt = reresolve_tac ctxt (#1 (get_rules ctxt)); 208 209(*Tries a safe rule or else a unsafe rule. Single-step for tracing. *) 210fun step_tac ctxt = 211 safe_tac ctxt ORELSE' filseq_resolve_tac ctxt (#2 (get_rules ctxt)) 9999; 212 213 214(* Tactic for reducing a goal, using Predicate Calculus rules. 215 A decision procedure for Propositional Calculus, it is incomplete 216 for Predicate-Calculus because of allL_thin and exR_thin. 217 Fails if it can do nothing. *) 218fun pc_tac ctxt = SELECT_GOAL (DEPTH_SOLVE (repeat_goal_tac ctxt 1)); 219 220 221(*The following two tactics are analogous to those provided by 222 Provers/classical. In fact, pc_tac is usually FASTER than fast_tac!*) 223fun fast_tac ctxt = 224 SELECT_GOAL (DEPTH_SOLVE (step_tac ctxt 1)); 225 226fun best_tac ctxt = 227 SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, size_of_thm) (step_tac ctxt 1)); 228 229val _ = Theory.setup 230 (Method.setup \<^binding>\<open>safe\<close> (method safe_tac) "" #> 231 Method.setup \<^binding>\<open>step\<close> (method step_tac) "" #> 232 Method.setup \<^binding>\<open>pc\<close> (method pc_tac) "" #> 233 Method.setup \<^binding>\<open>fast\<close> (method fast_tac) "" #> 234 Method.setup \<^binding>\<open>best\<close> (method best_tac) ""); 235 236end; 237 238