simplified Blast setup;
authorwenzelm
Tue Apr 26 21:27:01 2011 +0200 (2011-04-26)
changeset 4247752fa26b6c524
parent 42476 d0bc1268ef09
child 42478 8a526c010c3b
simplified Blast setup;
src/FOL/FOL.thy
src/HOL/HOL.thy
src/Provers/blast.ML
     1.1 --- a/src/FOL/FOL.thy	Tue Apr 26 21:05:52 2011 +0200
     1.2 +++ b/src/FOL/FOL.thy	Tue Apr 26 21:27:01 2011 +0200
     1.3 @@ -174,18 +174,13 @@
     1.4  ML {*
     1.5    structure Blast = Blast
     1.6    (
     1.7 +    structure Classical = Cla
     1.8      val thy = @{theory}
     1.9 -    type claset = Cla.claset
    1.10      val equality_name = @{const_name eq}
    1.11      val not_name = @{const_name Not}
    1.12      val notE = @{thm notE}
    1.13      val ccontr = @{thm ccontr}
    1.14 -    val contr_tac = Cla.contr_tac
    1.15 -    val dup_intr = Cla.dup_intr
    1.16      val hyp_subst_tac = Hypsubst.blast_hyp_subst_tac
    1.17 -    val rep_cs = Cla.rep_cs
    1.18 -    val cla_modifiers = Cla.cla_modifiers
    1.19 -    val cla_meth' = Cla.cla_meth'
    1.20    );
    1.21    val blast_tac = Blast.blast_tac;
    1.22  *}
     2.1 --- a/src/HOL/HOL.thy	Tue Apr 26 21:05:52 2011 +0200
     2.2 +++ b/src/HOL/HOL.thy	Tue Apr 26 21:27:01 2011 +0200
     2.3 @@ -927,22 +927,17 @@
     2.4  done
     2.5  
     2.6  ML {*
     2.7 -structure Blast = Blast
     2.8 -(
     2.9 -  val thy = @{theory}
    2.10 -  type claset = Classical.claset
    2.11 -  val equality_name = @{const_name HOL.eq}
    2.12 -  val not_name = @{const_name Not}
    2.13 -  val notE = @{thm notE}
    2.14 -  val ccontr = @{thm ccontr}
    2.15 -  val contr_tac = Classical.contr_tac
    2.16 -  val dup_intr = Classical.dup_intr
    2.17 -  val hyp_subst_tac = Hypsubst.blast_hyp_subst_tac
    2.18 -  val rep_cs = Classical.rep_cs
    2.19 -  val cla_modifiers = Classical.cla_modifiers
    2.20 -  val cla_meth' = Classical.cla_meth'
    2.21 -);
    2.22 -val blast_tac = Blast.blast_tac;
    2.23 +  structure Blast = Blast
    2.24 +  (
    2.25 +    structure Classical = Classical
    2.26 +    val thy = @{theory}
    2.27 +    val equality_name = @{const_name HOL.eq}
    2.28 +    val not_name = @{const_name Not}
    2.29 +    val notE = @{thm notE}
    2.30 +    val ccontr = @{thm ccontr}
    2.31 +    val hyp_subst_tac = Hypsubst.blast_hyp_subst_tac
    2.32 +  );
    2.33 +  val blast_tac = Blast.blast_tac;
    2.34  *}
    2.35  
    2.36  setup Blast.setup
     3.1 --- a/src/Provers/blast.ML	Tue Apr 26 21:05:52 2011 +0200
     3.2 +++ b/src/Provers/blast.ML	Tue Apr 26 21:27:01 2011 +0200
     3.3 @@ -40,24 +40,13 @@
     3.4  
     3.5  signature BLAST_DATA =
     3.6  sig
     3.7 +  structure Classical: CLASSICAL
     3.8    val thy: theory
     3.9 -  type claset
    3.10    val equality_name: string
    3.11    val not_name: string
    3.12 -  val notE              : thm           (* [| ~P;  P |] ==> R *)
    3.13 -  val ccontr            : thm
    3.14 -  val contr_tac         : int -> tactic
    3.15 -  val dup_intr          : thm -> thm
    3.16 -  val hyp_subst_tac     : bool -> int -> tactic
    3.17 -  val rep_cs    : (* dependent on classical.ML *)
    3.18 -      claset -> {safeIs: thm list, safeEs: thm list,
    3.19 -                 hazIs: thm list, hazEs: thm list,
    3.20 -                 swrappers: (string * wrapper) list,
    3.21 -                 uwrappers: (string * wrapper) list,
    3.22 -                 safe0_netpair: netpair, safep_netpair: netpair,
    3.23 -                 haz_netpair: netpair, dup_netpair: netpair, xtra_netpair: Context_Rules.netpair}
    3.24 -  val cla_modifiers: Method.modifier parser list
    3.25 -  val cla_meth': (claset -> int -> tactic) -> Proof.context -> Proof.method
    3.26 +  val notE: thm           (* [| ~P;  P |] ==> R *)
    3.27 +  val ccontr: thm
    3.28 +  val hyp_subst_tac: bool -> int -> tactic
    3.29  end;
    3.30  
    3.31  signature BLAST =
    3.32 @@ -72,31 +61,31 @@
    3.33      | Bound of int
    3.34      | Abs   of string*term
    3.35      | $  of term*term;
    3.36 -  type branch
    3.37 -  val depth_tac         : claset -> int -> int -> tactic
    3.38 -  val depth_limit       : int Config.T
    3.39 -  val blast_tac         : claset -> int -> tactic
    3.40 -  val setup             : theory -> theory
    3.41 +  val depth_tac: claset -> int -> int -> tactic
    3.42 +  val depth_limit: int Config.T
    3.43 +  val blast_tac: claset -> int -> tactic
    3.44 +  val setup: theory -> theory
    3.45    (*debugging tools*)
    3.46 -  val stats             : bool Unsynchronized.ref
    3.47 -  val trace             : bool Unsynchronized.ref
    3.48 -  val fullTrace         : branch list list Unsynchronized.ref
    3.49 -  val fromType          : (indexname * term) list Unsynchronized.ref -> Term.typ -> term
    3.50 -  val fromTerm          : theory -> Term.term -> term
    3.51 -  val fromSubgoal       : theory -> Term.term -> term
    3.52 -  val instVars          : term -> (unit -> unit)
    3.53 -  val toTerm            : int -> term -> Term.term
    3.54 -  val readGoal          : theory -> string -> term
    3.55 -  val tryInThy          : theory -> claset -> int -> string ->
    3.56 -                  (int->tactic) list * branch list list * (int*int*exn) list
    3.57 -  val normBr            : branch -> branch
    3.58 +  type branch
    3.59 +  val stats: bool Unsynchronized.ref
    3.60 +  val trace: bool Unsynchronized.ref
    3.61 +  val fullTrace: branch list list Unsynchronized.ref
    3.62 +  val fromType: (indexname * term) list Unsynchronized.ref -> Term.typ -> term
    3.63 +  val fromTerm: theory -> Term.term -> term
    3.64 +  val fromSubgoal: theory -> Term.term -> term
    3.65 +  val instVars: term -> (unit -> unit)
    3.66 +  val toTerm: int -> term -> Term.term
    3.67 +  val readGoal: theory -> string -> term
    3.68 +  val tryInThy: theory -> claset -> int -> string ->
    3.69 +    (int -> tactic) list * branch list list * (int * int * exn) list
    3.70 +  val normBr: branch -> branch
    3.71  end;
    3.72  
    3.73 -
    3.74 -functor Blast(Data: BLAST_DATA) : BLAST =
    3.75 +functor Blast(Data: BLAST_DATA): BLAST =
    3.76  struct
    3.77  
    3.78 -type claset = Data.claset;
    3.79 +structure Classical = Data.Classical;
    3.80 +type claset = Classical.claset;
    3.81  
    3.82  val trace = Unsynchronized.ref false
    3.83  and stats = Unsynchronized.ref false;   (*for runtime and search statistics*)
    3.84 @@ -541,7 +530,7 @@
    3.85  fun fromIntrRule thy vars rl =
    3.86    let val trl = rl |> Thm.prop_of |> fromTerm thy |> convertIntrRule vars
    3.87        fun tac (upd,dup,rot) i =
    3.88 -         rmtac upd (if dup then Data.dup_intr rl else rl) i
    3.89 +         rmtac upd (if dup then Classical.dup_intr rl else rl) i
    3.90           THEN
    3.91           rot_subgoals_tac (rot, #2 trl) i
    3.92    in (trl, tac) end;
    3.93 @@ -928,7 +917,7 @@
    3.94  *)
    3.95  fun prove (state, start, cs, brs, cont) =
    3.96   let val State {thy, ntrail, nclosed, ntried, ...} = state;
    3.97 -     val {safe0_netpair, safep_netpair, haz_netpair, ...} = Data.rep_cs cs
    3.98 +     val {safe0_netpair, safep_netpair, haz_netpair, ...} = Classical.rep_cs cs
    3.99       val safeList = [safe0_netpair, safep_netpair]
   3.100       and hazList  = [haz_netpair]
   3.101       fun prv (tacs, trs, choices, []) =
   3.102 @@ -1314,9 +1303,9 @@
   3.103  val setup =
   3.104    setup_depth_limit #>
   3.105    Method.setup @{binding blast}
   3.106 -    (Scan.lift (Scan.option Parse.nat) --| Method.sections Data.cla_modifiers >>
   3.107 -      (fn NONE => Data.cla_meth' blast_tac
   3.108 -        | SOME lim => Data.cla_meth' (fn cs => depth_tac cs lim)))
   3.109 +    (Scan.lift (Scan.option Parse.nat) --| Method.sections Classical.cla_modifiers >>
   3.110 +      (fn NONE => Classical.cla_meth' blast_tac
   3.111 +        | SOME lim => Classical.cla_meth' (fn cs => depth_tac cs lim)))
   3.112      "classical tableau prover";
   3.113  
   3.114  end;