# HG changeset patch # User wenzelm # Date 1752269773 -7200 # Node ID b816f10aed31a7126a2245e2db7764dfbbd70221 # Parent 7f9c4466c6a550f6c6f1d77215b7cea8753b6c08 tuned comments: more formal sections; diff -r 7f9c4466c6a5 -r b816f10aed31 src/Provers/classical.ML --- a/src/Provers/classical.ML Fri Jul 11 23:03:49 2025 +0200 +++ b/src/Provers/classical.ML Fri Jul 11 23:36:13 2025 +0200 @@ -1,5 +1,6 @@ (* Title: Provers/classical.ML Author: Lawrence C Paulson, Cambridge University Computer Laboratory + Author: Makarius Theorem prover for classical reasoning, including predicate calculus, set theory, etc. @@ -10,6 +11,9 @@ For a rule to be safe, its premises and conclusion should be logically equivalent. There should be no variables in the premises that are not in the conclusion. + +Rules are maintained in "canonical reverse order", meaning that later +declarations take precedence. *) (*higher precedence than := facilitates use of references*) @@ -20,13 +24,13 @@ signature CLASSICAL_DATA = sig - val imp_elim: thm (* P --> Q ==> (~ R ==> P) ==> (Q ==> R) ==> R *) - val not_elim: thm (* ~P ==> P ==> R *) - val swap: thm (* ~ P ==> (~ R ==> P) ==> R *) - val classical: thm (* (~ P ==> P) ==> P *) - val sizef: thm -> int (* size function for BEST_FIRST, typically size_of_thm *) - val hyp_subst_tacs: (Proof.context -> int -> tactic) list (* optional tactics for - substitution in the hypotheses; assumed to be safe! *) + val imp_elim: thm (* P \ Q \ (\ R \ P) \ (Q \ R) \ R *) + val not_elim: thm (* \ P \ P \ R *) + val swap: thm (* \ P \ (\ R \ P) \ R *) + val classical: thm (* (\ P \ P) \ P *) + val sizef: thm -> int (*size function for BEST_FIRST, typically size_of_thm*) + val hyp_subst_tacs: (Proof.context -> int -> tactic) list + (*optional tactics for substitution in the hypotheses; assumed to be safe!*) end; signature BASIC_CLASSICAL = @@ -127,18 +131,19 @@ functor Classical(Data: CLASSICAL_DATA): CLASSICAL = struct -(** classical elimination rules **) +(** Support for classical reasoning **) -(* -Classical reasoning requires stronger elimination rules. For -instance, make_elim of Pure transforms the HOL rule injD into +(* classical elimination rules *) + +(*Classical reasoning requires stronger elimination rules. For + instance, make_elim of Pure transforms the HOL rule injD into - [| inj f; f x = f y; x = y ==> PROP W |] ==> PROP W + \inj f; f x = f y; x = y \ PROP W\ \ PROP W -Such rules can cause fast_tac to fail and blast_tac to report "PROOF -FAILED"; classical_rule will strengthen this to + Such rules can cause fast_tac to fail and blast_tac to report "PROOF + FAILED"; classical_rule will strengthen this to - [| inj f; ~ W ==> f x = f y; x = y ==> W |] ==> W + \inj f; \ W \ f x = f y; x = y \ W\ \ W *) fun classical_rule ctxt rule = @@ -162,28 +167,30 @@ in if Thm.equiv_thm thy (rule, rule'') then rule else rule'' end else rule; -(*flatten nested meta connectives in prems*) + +(* flatten nested meta connectives in prems *) + fun flat_rule ctxt = Conv.fconv_rule (Conv.prems_conv ~1 (Object_Logic.atomize_prems ctxt)); -(*** Useful tactics for classical reasoning ***) +(* Useful tactics for classical reasoning *) -(*Prove goal that assumes both P and ~P. +(*Prove goal that assumes both P and \ P. No backtracking if it finds an equal assumption. Perhaps should call ematch_tac instead of eresolve_tac, but then cannot prove ZF/cantor.*) fun contr_tac ctxt = eresolve_tac ctxt [Data.not_elim] THEN' (eq_assume_tac ORELSE' assume_tac ctxt); -(*Finds P-->Q and P in the assumptions, replaces implication by Q. - Could do the same thing for P<->Q and P... *) +(*Finds P \ Q and P in the assumptions, replaces implication by Q. + Could do the same thing for P \ Q and P.*) fun mp_tac ctxt i = eresolve_tac ctxt [Data.not_elim, Data.imp_elim] i THEN assume_tac ctxt i; (*Like mp_tac but instantiates no variables*) fun eq_mp_tac ctxt i = ematch_tac ctxt [Data.not_elim, Data.imp_elim] i THEN eq_assume_tac i; -(*Creates rules to eliminate ~A, from rules to introduce A*) +(*Creates rules to eliminate \ A, from rules to introduce A*) fun maybe_swap_rule th = (case [th] RLN (2, [Data.swap]) of [] => NONE @@ -212,7 +219,8 @@ in rule_by_tactic ctxt (TRYALL (eresolve_tac ctxt [revcut_rl])) rl end; -(**** Classical rule sets ****) + +(** Classical rule sets **) type rl = thm * thm option; (*internal form, with possibly swapped version*) type info = {rl: rl, dup_rl: rl, plain: thm}; @@ -254,10 +262,7 @@ fun rep_cs (CS args) = args; -(*** Adding (un)safe introduction or elimination rules. - - In case of overlap, new rules are tried BEFORE old ones!! -***) +(* insert / delete rules in underlying netpairs *) fun insert_brl i brl = Bires.insert_tagged_rule ({weight = Bires.subgoals_of brl, index = i}, brl); @@ -306,7 +311,7 @@ end; -(* wrappers *) +(* update wrappers *) fun map_swrappers f (CS {decls, swrappers, uwrappers, @@ -323,7 +328,7 @@ unsafe_netpair = unsafe_netpair, dup_netpair = dup_netpair, extra_netpair = extra_netpair}; -(*** extend and merge rules ***) +(* extend and merge rules *) local @@ -440,7 +445,7 @@ end; -(*** delete rules ***) +(* delete rules *) fun delrule ctxt th cs = let @@ -472,7 +477,7 @@ end; -(** context data **) +(* Claset context data *) structure Claset = Generic_Data ( @@ -530,7 +535,7 @@ -(*** Modifying the wrapper tacticals ***) +(** Modifying the wrapper tacticals **) fun appSWrappers ctxt = fold (fn (_, w) => w ctxt) (#swrappers (rep_claset_of ctxt)); fun appWrappers ctxt = fold (fn (_, w) => w ctxt) (#uwrappers (rep_claset_of ctxt)); @@ -558,13 +563,13 @@ fun ctxt delWrapper name = ctxt |> map_claset (map_uwrappers (delete_warn ("No such unsafe wrapper in claset: " ^ name) name)); -(* compose a safe tactic alternatively before/after safe_step_tac *) +(*compose a safe tactic alternatively before/after safe_step_tac*) fun ctxt addSbefore (name, tac1) = ctxt addSWrapper (name, fn ctxt => fn tac2 => tac1 ctxt ORELSE' tac2); fun ctxt addSafter (name, tac2) = ctxt addSWrapper (name, fn ctxt => fn tac1 => tac1 ORELSE' tac2 ctxt); -(*compose a tactic alternatively before/after the step tactic *) +(*compose a tactic alternatively before/after the step tactic*) fun ctxt addbefore (name, tac1) = ctxt addWrapper (name, fn ctxt => fn tac2 => tac1 ctxt APPEND' tac2); fun ctxt addafter (name, tac2) = @@ -581,7 +586,7 @@ -(**** Simple tactics for theorem proving ****) +(** Simple tactics for theorem proving **) (*Attack subgoals using safe inferences -- matching, not resolution*) fun safe_step_tac ctxt = @@ -601,7 +606,8 @@ fun safe_tac ctxt = REPEAT_DETERM1 (FIRSTGOAL (safe_steps_tac ctxt)); -(*** Clarify_tac: do safe steps without causing branching ***) + +(** Clarify_tac: do safe steps without causing branching **) (*version of Bires.bimatch_from_nets_tac that only applies rules that create precisely n subgoals.*) @@ -630,7 +636,8 @@ fun clarify_tac ctxt = SELECT_GOAL (REPEAT_DETERM (clarify_step_tac ctxt 1)); -(*** Unsafe steps instantiate variables or lose information ***) + +(** Unsafe steps instantiate variables or lose information **) (*Backtracking is allowed among the various these unsafe ways of proving a subgoal. *) @@ -659,7 +666,7 @@ safe_tac ctxt ORELSE appWrappers ctxt (inst_step_tac ctxt APPEND' unsafe_step_tac ctxt) i; -(**** The following tactics all fail unless they solve one goal ****) +(** The following tactics all fail unless they solve one goal **) (*Dumb but fast*) fun fast_tac ctxt = @@ -684,7 +691,7 @@ SELECT_GOAL (BEST_FIRST (Thm.no_prems, Data.sizef) (slow_step_tac ctxt 1)); -(***ASTAR with weight weight_ASTAR, by Norbert Voelker*) +(** ASTAR with weight weight_ASTAR, by Norbert Voelker **) val weight_ASTAR = 5; @@ -701,10 +708,10 @@ (slow_step_tac ctxt 1)); -(**** Complete tactic, loosely based upon LeanTaP. This tactic is the outcome +(** Complete tactic, loosely based upon LeanTaP. This tactic is the outcome of much experimentation! Changing APPEND to ORELSE below would prove easy theorems faster, but loses completeness -- and many of the harder - theorems such as 43. ****) + theorems such as 43. **) (*Non-deterministic! Could always expand the first unsafe connective. That's hard to implement and did not perform better in experiments, due to @@ -736,7 +743,10 @@ fun deepen_tac ctxt = DEEPEN (2, 10) (safe_depth_tac ctxt); -(* attributes *) + +(** attributes **) + +(* declarations *) fun attrib f = Thm.declaration_attribute (fn th => fn context => @@ -756,8 +766,7 @@ |> Thm.attribute_declaration Context_Rules.rule_del th); - -(** concrete syntax of attributes **) +(* concrete syntax *) val introN = "intro"; val elimN = "elim"; @@ -821,8 +830,7 @@ fun cla_method' tac = Method.sections cla_modifiers >> K (SIMPLE_METHOD' o tac); - -(** method setup **) +(* method setup *) val _ = Theory.setup @@ -857,7 +865,8 @@ "single classical step (safe rules, without splitting)"); -(** outer syntax **) + +(** outer syntax commands **) val _ = Outer_Syntax.command \<^command_keyword>\print_claset\ "print context of Classical Reasoner"