src/Sequents/prover.ML
 changeset 7097 5ab37ed3d53c parent 6054 4a4f6ad607a1 child 7122 87b233b31889
equal inserted replaced
7096:8c9278991d9c 7097:5ab37ed3d53c
`     1 (*  Title:      LK/LK.ML`
`     1 (*  Title:      LK/LK.ML`
`     2     ID:         \$Id\$`
`     2     ID:         \$Id\$`
`     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory`
`     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory`
`     4     Copyright   1992  University of Cambridge`
`     4     Copyright   1992  University of Cambridge`
`       `
`     5 `
`       `
`     6 Simple classical reasoner for the sequent calculus, based on "theorem packs"`
`     5 *)`
`     7 *)`
`     6 `
`     8 `
`     7 `
`     9 `
`     9 `
`    10 `
`    10 (* based largely on LK *)`
`    11 (*Higher precedence than := facilitates use of references*)`
`       `
`    12 infix 4 add_safes add_unsafes;`
`    11 `
`    13 `
`    12 datatype pack = Pack of thm list * thm list;`
`    14 datatype pack = Pack of thm list * thm list;`
`    13 `
`    15 `
`    14 (*A theorem pack has the form  (safe rules, unsafe rules)`
`    16 (*A theorem pack has the form  (safe rules, unsafe rules)`
`    15   An unsafe rule is incomplete or introduces variables in subgoals,`
`    17   An unsafe rule is incomplete or introduces variables in subgoals,`
`    17 `
`    19 `
`    18 fun less (rl1,rl2) = (nprems_of rl1) < (nprems_of rl2);`
`    20 fun less (rl1,rl2) = (nprems_of rl1) < (nprems_of rl2);`
`    19 `
`    21 `
`    20 val empty_pack = Pack([],[]);`
`    22 val empty_pack = Pack([],[]);`
`    21 `
`    23 `
`    22 infix 4 add_safes add_unsafes;`
`    24 fun warn_duplicates [] = []`
`       `
`    25   | warn_duplicates dups =`
`       `
`    26       (warning (String.concat ("Ignoring duplicate theorems:\n"::`
`       `
`    27 			       map (suffix "\n" o string_of_thm) dups));`
`       `
`    28        dups);`
`    23 `
`    29 `
`    24 fun (Pack(safes,unsafes)) add_safes ths   = `
`    30 fun (Pack(safes,unsafes)) add_safes ths   = `
`    25     Pack(sort (make_ord less) (ths@safes), unsafes);`
`    31     let val dups = warn_duplicates (gen_inter eq_thm (ths,safes))`
`       `
`    32 	val ths' = gen_rems eq_thm (ths,dups)`
`       `
`    33     in`
`       `
`    34         Pack(sort (make_ord less) (ths'@safes), unsafes)`
`       `
`    35     end;`
`    26 `
`    36 `
`    27 fun (Pack(safes,unsafes)) add_unsafes ths = `
`    37 fun (Pack(safes,unsafes)) add_unsafes ths = `
`    28     Pack(safes, sort (make_ord less) (ths@unsafes));`
`    38     let val dups = warn_duplicates (gen_inter eq_thm (ths,unsafes))`
`       `
`    39 	val ths' = gen_rems eq_thm (ths,dups)`
`       `
`    40     in`
`       `
`    41 	Pack(safes, sort (make_ord less) (ths'@unsafes))`
`       `
`    42     end;`
`       `
`    43 `
`       `
`    44 fun merge_pack (Pack(safes,unsafes), Pack(safes',unsafes')) =`
`       `
`    45         Pack(sort (make_ord less) (safes@safes'), `
`       `
`    46 	     sort (make_ord less) (unsafes@unsafes'));`
`    29 `
`    47 `
`    30 `
`    48 `
`       `
`    49 fun print_pack (Pack(safes,unsafes)) =`
`       `
`    50     (writeln "Safe rules:";  print_thms safes;`
`       `
`    51      writeln "Unsafe rules:"; print_thms unsafes);`
`       `
`    52 `
`    31 (*Returns the list of all formulas in the sequent*)`
`    53 (*Returns the list of all formulas in the sequent*)`
`    32 fun forms_of_seq (Const("Sequents.SeqO'",_) \$ P \$ u) = P :: forms_of_seq u`
`    54 fun forms_of_seq (Const("SeqO'",_) \$ P \$ u) = P :: forms_of_seq u`
`    33   | forms_of_seq (H \$ u) = forms_of_seq u`
`    55   | forms_of_seq (H \$ u) = forms_of_seq u`
`    34   | forms_of_seq _ = [];`
`    56   | forms_of_seq _ = [];`
`    35 `
`    57 `
`    36 (*Tests whether two sequences (left or right sides) could be resolved.`
`    58 (*Tests whether two sequences (left or right sides) could be resolved.`
`    37   seqp is a premise (subgoal), seqc is a conclusion of an object-rule.`
`    59   seqp is a premise (subgoal), seqc is a conclusion of an object-rule.`
`   110 	           ORELSE  (print_tac "" THEN lastrestac gtac i)`
`   132 	           ORELSE  (print_tac "" THEN lastrestac gtac i)`
`   111   in  gtac  end; `
`   133   in  gtac  end; `
`   112 `
`   134 `
`   113 `
`   135 `
`   114 (*Tries safe rules only*)`
`   136 (*Tries safe rules only*)`
`   115 fun safe_goal_tac (Pack(safes,unsafes)) = reresolve_tac safes;`
`   137 fun safe_tac (Pack(safes,unsafes)) = reresolve_tac safes;`
`       `
`   138 `
`       `
`   139 val safe_goal_tac = safe_tac;   (*backwards compatibility*)`
`   116 `
`   140 `
`   117 (*Tries a safe rule or else a unsafe rule.  Single-step for tracing. *)`
`   141 (*Tries a safe rule or else a unsafe rule.  Single-step for tracing. *)`
`   118 fun step_tac (thm_pack as Pack(safes,unsafes)) =`
`   142 fun step_tac (thm_pack as Pack(safes,unsafes)) =`
`   119     safe_goal_tac thm_pack  ORELSE'`
`   143     safe_tac thm_pack  ORELSE'`
`   120     filseq_resolve_tac unsafes 9999;`
`   144     filseq_resolve_tac unsafes 9999;`
`   121 `
`   145 `
`   122 `
`   146 `
`   123 (* Tactic for reducing a goal, using Predicate Calculus rules.`
`   147 (* Tactic for reducing a goal, using Predicate Calculus rules.`
`   124    A decision procedure for Propositional Calculus, it is incomplete`
`   148    A decision procedure for Propositional Calculus, it is incomplete`
`   136   SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, size_of_thm) `
`   160   SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, size_of_thm) `
`   137 	       (step_tac thm_pack 1));`
`   161 	       (step_tac thm_pack 1));`
`   138 `
`   162 `
`   139 `
`   163 `
`   140 `
`   164 `
`   141 signature MODAL_PROVER_RULE =`
`   165 structure ProverArgs =`
`   142 sig`
`   166   struct`
`   143     val rewrite_rls      : thm list`
`   167   val name = "Sequents/prover";`
`   144     val safe_rls         : thm list`
`   168   type T = pack ref;`
`   145     val unsafe_rls       : thm list`
`   169   val empty = ref empty_pack`
`   146     val bound_rls        : thm list`
`   170   fun copy (ref pack) = ref pack;`
`   147     val aside_rls        : thm list`
`   171   val prep_ext = copy;`
`   148 end;`
`   172   fun merge (ref pack1, ref pack2) = ref (merge_pack (pack1, pack2));`
`       `
`   173   fun print _ (ref pack) = print_pack pack;`
`       `
`   174   end;`
`   149 `
`   175 `
`   150 signature MODAL_PROVER = `
`   176 structure ProverData = TheoryDataFun(ProverArgs);`
`   151 sig`
`       `
`   152     val rule_tac   : thm list -> int ->tactic`
`       `
`   153     val step_tac   : int -> tactic`
`       `
`   154     val solven_tac : int -> int -> tactic`
`       `
`   155     val solve_tac  : int -> tactic`
`       `
`   156 end;`
`       `
`   157 `
`   177 `
`   158 functor Modal_ProverFun (Modal_Rule: MODAL_PROVER_RULE) : MODAL_PROVER = `
`   178 val prover_setup = [ProverData.init];`
`   159 struct`
`       `
`   160 local open Modal_Rule`
`       `
`   161 in `
`       `
`   162 `
`   179 `
`   163 (*Returns the list of all formulas in the sequent*)`
`   180 val print_thm_pack = ProverData.print;`
`   164 fun forms_of_seq (Const("Sequents.SeqO",_) \$ P \$ u) = P :: forms_of_seq u`
`   181 val thm_pack_ref_of_sg = ProverData.get_sg;`
`   165   | forms_of_seq (H \$ u) = forms_of_seq u`
`   182 val thm_pack_ref_of = ProverData.get;`
`   166   | forms_of_seq _ = [];`
`       `
`   167 `
`   183 `
`   168 (*Tests whether two sequences (left or right sides) could be resolved.`
`   184 (* access global thm_pack *)`
`   169   seqp is a premise (subgoal), seqc is a conclusion of an object-rule.`
`       `
`   170   Assumes each formula in seqc is surrounded by sequence variables`
`       `
`   171   -- checks that each concl formula looks like some subgoal formula.*)`
`       `
`   172 fun could_res (seqp,seqc) =`
`       `
`   173       forall (fn Qc => exists (fn Qp => could_unify (Qp,Qc)) `
`       `
`   174                               (forms_of_seq seqp))`
`       `
`   175              (forms_of_seq seqc);`
`       `
`   176 `
`   185 `
`   177 (*Tests whether two sequents G|-H could be resolved, comparing each side.*)`
`   186 val thm_pack_of_sg = ! o thm_pack_ref_of_sg;`
`   178 fun could_resolve_seq (prem,conc) =`
`   187 val thm_pack_of = thm_pack_of_sg o sign_of;`
`   179   case (prem,conc) of`
`       `
`   180       (_ \$ Abs(_,_,leftp) \$ Abs(_,_,rightp),`
`       `
`   181        _ \$ Abs(_,_,leftc) \$ Abs(_,_,rightc)) =>`
`       `
`   182           could_res (leftp,leftc)  andalso  could_res (rightp,rightc)`
`       `
`   183     | _ => false;`
`       `
`   184 `
`   188 `
`   185 (*Like filt_resolve_tac, using could_resolve_seq`
`   189 val thm_pack = thm_pack_of o Context.the_context;`
`   186   Much faster than resolve_tac when there are many rules.`
`   190 val thm_pack_ref = thm_pack_ref_of_sg o sign_of o Context.the_context;`
`   187   Resolve subgoal i using the rules, unless more than maxr are compatible. *)`
`       `
`   188 fun filseq_resolve_tac rules maxr = SUBGOAL(fn (prem,i) =>`
`       `
`   189   let val rls = filter_thms could_resolve_seq (maxr+1, prem, rules)`
`       `
`   190   in  if length rls > maxr  then  no_tac  else resolve_tac rls i`
`       `
`   191   end);`
`       `
`   192 `
`   191 `
`   194 `
`   192 `
`   195 (* NB No back tracking possible with aside rules *)`
`   193 (* change global thm_pack *)`
`   196 `
`   194 `
`   197 fun aside_tac n = DETERM(REPEAT (filt_resolve_tac aside_rls 999 n));`
`   195 fun change_thm_pack f x = thm_pack_ref () := (f (thm_pack (), x));`
`   198 fun rule_tac rls n = fresolve_tac rls n THEN aside_tac n;`
`       `
`   199 `
`   196 `
`   200 val fres_safe_tac = fresolve_tac safe_rls;`
`   197 val Add_safes = change_thm_pack (op add_safes);`
`   201 val fres_unsafe_tac = fresolve_tac unsafe_rls THEN' aside_tac;`
`   198 val Add_unsafes = change_thm_pack (op add_unsafes);`
`   202 val fres_bound_tac = fresolve_tac bound_rls;`
`       `
`   203 `
`   199 `