setup for refined facts handling;
authorwenzelm
Tue Sep 21 17:26:50 1999 +0200 (1999-09-21 ago)
changeset 75591d2c099e98f7
parent 7558 08b2d5c94b8a
child 7560 19c3be2d285c
setup for refined facts handling;
Method.bang_sectioned_args / Args.bang_facts;
src/Provers/blast.ML
src/Provers/clasimp.ML
src/Provers/classical.ML
     1.1 --- a/src/Provers/blast.ML	Tue Sep 21 17:26:42 1999 +0200
     1.2 +++ b/src/Provers/blast.ML	Tue Sep 21 17:26:50 1999 +0200
     1.3 @@ -68,7 +68,7 @@
     1.4  		 safe0_netpair: netpair, safep_netpair: netpair,
     1.5  		 haz_netpair: netpair, dup_netpair: netpair, xtra_netpair: netpair}
     1.6    val cla_modifiers: (Args.T list -> (Method.modifier * Args.T list)) list
     1.7 -  val cla_meth': (claset -> int -> tactic) -> Proof.context -> Proof.method
     1.8 +  val cla_meth': (claset -> int -> tactic) -> thm list -> Proof.context -> Proof.method
     1.9    end;
    1.10  
    1.11  
    1.12 @@ -1330,11 +1330,11 @@
    1.13  
    1.14  (** method setup **)
    1.15  
    1.16 -val blast_args =
    1.17 -  Method.sectioned_args (K (Scan.lift (Scan.option Args.nat))) Data.cla_modifiers;
    1.18 +fun blast_args m =
    1.19 +  Method.sectioned_args (K (Args.bang_facts -- Scan.lift (Scan.option Args.nat))) Data.cla_modifiers m;
    1.20  
    1.21 -fun blast_meth None = Data.cla_meth' blast_tac
    1.22 -  | blast_meth (Some lim) = Data.cla_meth' (fn cs => depth_tac cs lim);
    1.23 +fun blast_meth (prems, None) = Data.cla_meth' blast_tac prems
    1.24 +  | blast_meth (prems, Some lim) = Data.cla_meth' (fn cs => depth_tac cs lim) prems;
    1.25  
    1.26  val setup = [Method.add_methods [("blast", blast_args blast_meth, "tableau prover")]];
    1.27  
     2.1 --- a/src/Provers/clasimp.ML	Tue Sep 21 17:26:42 1999 +0200
     2.2 +++ b/src/Provers/clasimp.ML	Tue Sep 21 17:26:50 1999 +0200
     2.3 @@ -153,16 +153,15 @@
     2.4    (Classical.get_local_claset ctxt, Simplifier.get_local_simpset ctxt);
     2.5  
     2.6  val clasimp_modifiers = Classical.cla_modifiers @ Simplifier.simp_modifiers;
     2.7 -val clasimp_args = Method.only_sectioned_args clasimp_modifiers;
     2.8  
     2.9 -fun clasimp_meth tac ctxt = Method.METHOD (fn facts =>
    2.10 -  ALLGOALS (Method.insert_tac facts) THEN tac (get_local_clasimpset ctxt));
    2.11 +fun clasimp_meth tac prems ctxt = Method.METHOD (fn facts =>
    2.12 +  ALLGOALS (Method.insert_tac (prems @ facts)) THEN tac (get_local_clasimpset ctxt));
    2.13  
    2.14 -fun clasimp_meth' tac ctxt = Method.METHOD (fn facts =>
    2.15 -  FIRSTGOAL (Method.insert_tac facts THEN' tac (get_local_clasimpset ctxt)));
    2.16 +fun clasimp_meth' tac prems ctxt = Method.METHOD (fn facts =>
    2.17 +  FIRSTGOAL (Method.insert_tac (prems @ facts) THEN' tac (get_local_clasimpset ctxt)));
    2.18  
    2.19 -val clasimp_method = clasimp_args o clasimp_meth;
    2.20 -val clasimp_method' = clasimp_args o clasimp_meth';
    2.21 +val clasimp_method = Method.bang_sectioned_args clasimp_modifiers o clasimp_meth;
    2.22 +val clasimp_method' = Method.bang_sectioned_args clasimp_modifiers o clasimp_meth';
    2.23  
    2.24  
    2.25  val setup =
     3.1 --- a/src/Provers/classical.ML	Tue Sep 21 17:26:42 1999 +0200
     3.2 +++ b/src/Provers/classical.ML	Tue Sep 21 17:26:50 1999 +0200
     3.3 @@ -162,8 +162,8 @@
     3.4    val xtra_intro_local: Proof.context attribute
     3.5    val delrule_local: Proof.context attribute
     3.6    val cla_modifiers: (Args.T list -> (Method.modifier * Args.T list)) list
     3.7 -  val cla_meth: (claset -> tactic) -> Proof.context -> Proof.method
     3.8 -  val cla_meth': (claset -> int -> tactic) -> Proof.context -> Proof.method
     3.9 +  val cla_meth: (claset -> tactic) -> thm list -> Proof.context -> Proof.method
    3.10 +  val cla_meth': (claset -> int -> tactic) -> thm list -> Proof.context -> Proof.method
    3.11    val cla_method: (claset -> tactic) -> Args.src -> Proof.context -> Proof.method
    3.12    val cla_method': (claset -> int -> tactic) -> Args.src -> Proof.context -> Proof.method
    3.13    val setup: (theory -> theory) list
    3.14 @@ -347,7 +347,7 @@
    3.15  	  cs)
    3.16    else
    3.17    let val (safe0_rls, safep_rls) = (*0 subgoals vs 1 or more*)
    3.18 -          partition (fn rl => nprems_of rl=0) [th]
    3.19 +          partition Thm.no_prems [th]
    3.20        val nI = length safeIs + 1
    3.21        and nE = length safeEs
    3.22    in warn_dup th cs;
    3.23 @@ -530,7 +530,7 @@
    3.24            (cs as CS{safeIs, safeEs, hazIs, hazEs, xtraIs, xtraEs, swrappers, uwrappers,
    3.25  		    safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) =
    3.26   if mem_thm (th, safeIs) then
    3.27 -   let val (safe0_rls, safep_rls) = partition (fn rl => nprems_of rl=0) [th]
    3.28 +   let val (safe0_rls, safep_rls) = partition Thm.no_prems [th]
    3.29     in CS{safe0_netpair = delete (safe0_rls, []) safe0_netpair,
    3.30  	 safep_netpair = delete (safep_rls, []) safep_netpair,
    3.31  	 safeIs	= rem_thm (safeIs,th),
    3.32 @@ -1145,16 +1145,14 @@
    3.33    Args.$$$ introN >> K (I, safe_intro_local),
    3.34    Args.$$$ delN >> K (I, delrule_local)];
    3.35  
    3.36 -val cla_args = Method.only_sectioned_args cla_modifiers;
    3.37 -
    3.38 -fun cla_meth tac ctxt = Method.METHOD (fn facts =>
    3.39 -  ALLGOALS (Method.insert_tac facts) THEN tac (get_local_claset ctxt));
    3.40 +fun cla_meth tac prems ctxt = Method.METHOD (fn facts =>
    3.41 +  ALLGOALS (Method.insert_tac (prems @ facts)) THEN tac (get_local_claset ctxt));
    3.42  
    3.43 -fun cla_meth' tac ctxt = Method.METHOD (fn facts =>
    3.44 -  FIRSTGOAL (Method.insert_tac facts THEN' tac (get_local_claset ctxt)));
    3.45 +fun cla_meth' tac prems ctxt = Method.METHOD (fn facts =>
    3.46 +  FIRSTGOAL (Method.insert_tac (prems @ facts) THEN' tac (get_local_claset ctxt)));
    3.47  
    3.48 -val cla_method = cla_args o cla_meth;
    3.49 -val cla_method' = cla_args o cla_meth';
    3.50 +val cla_method = Method.bang_sectioned_args cla_modifiers o cla_meth;
    3.51 +val cla_method' = Method.bang_sectioned_args cla_modifiers o cla_meth';
    3.52  
    3.53  
    3.54