tuned signature;
authorwenzelm
Sun May 15 16:40:24 2011 +0200 (2011-05-15)
changeset 42812dda4aef7cba4
parent 42811 c5146d5fc54c
child 42813 6c841fa92fa2
tuned signature;
src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML
src/Provers/blast.ML
src/Provers/classical.ML
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML	Sat May 14 22:00:24 2011 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML	Sun May 15 16:40:24 2011 +0200
     1.3 @@ -798,7 +798,7 @@
     1.4  
     1.5  fun clasimpset_rules_of ctxt =
     1.6    let
     1.7 -    val {safeIs, safeEs, hazIs, hazEs, ...} = ctxt |> claset_of |> rep_cs
     1.8 +    val {safeIs, safeEs, hazIs, hazEs, ...} = ctxt |> claset_of |> Classical.rep_cs
     1.9      val intros = Item_Net.content safeIs @ Item_Net.content hazIs
    1.10      val elims = map Classical.classical_rule (Item_Net.content safeEs @ Item_Net.content hazEs)
    1.11      val simps = ctxt |> simpset_of |> dest_ss |> #simps
     2.1 --- a/src/Provers/blast.ML	Sat May 14 22:00:24 2011 +0200
     2.2 +++ b/src/Provers/blast.ML	Sun May 15 16:40:24 2011 +0200
     2.3 @@ -35,9 +35,6 @@
     2.4          "no DETERM" flag would prevent proofs failing here.
     2.5  *)
     2.6  
     2.7 -(*Should be a type abbreviation?*)
     2.8 -type netpair = (int*(bool*thm)) Net.net * (int*(bool*thm)) Net.net;
     2.9 -
    2.10  signature BLAST_DATA =
    2.11  sig
    2.12    structure Classical: CLASSICAL
    2.13 @@ -554,7 +551,7 @@
    2.14    | toTerm d (f $ u)       = Term.$ (toTerm d f, toTerm (d-1) u);
    2.15  
    2.16  
    2.17 -fun netMkRules ctxt P vars (nps: netpair list) =
    2.18 +fun netMkRules ctxt P vars (nps: Classical.netpair list) =
    2.19    case P of
    2.20        (Const ("*Goal*", _) $ G) =>
    2.21          let val pG = mk_Trueprop (toTerm 2 G)
     3.1 --- a/src/Provers/classical.ML	Sat May 14 22:00:24 2011 +0200
     3.2 +++ b/src/Provers/classical.ML	Sun May 15 16:40:24 2011 +0200
     3.3 @@ -18,11 +18,6 @@
     3.4    addSbefore addSafter addbefore addafter
     3.5    addD2 addE2 addSD2 addSE2;
     3.6  
     3.7 -
     3.8 -(*should be a type abbreviation in signature CLASSICAL*)
     3.9 -type netpair = (int * (bool * thm)) Net.net * (int * (bool * thm)) Net.net;
    3.10 -type wrapper = (int -> tactic) -> (int -> tactic);
    3.11 -
    3.12  signature CLASSICAL_DATA =
    3.13  sig
    3.14    val imp_elim: thm  (* P --> Q ==> (~ R ==> P) ==> (Q ==> R) ==> R *)
    3.15 @@ -35,21 +30,8 @@
    3.16  
    3.17  signature BASIC_CLASSICAL =
    3.18  sig
    3.19 +  type wrapper = (int -> tactic) -> int -> tactic
    3.20    type claset
    3.21 -  val empty_cs: claset
    3.22 -  val merge_cs: claset * claset -> claset
    3.23 -  val rep_cs: claset ->
    3.24 -   {safeIs: thm Item_Net.T,
    3.25 -    safeEs: thm Item_Net.T,
    3.26 -    hazIs: thm Item_Net.T,
    3.27 -    hazEs: thm Item_Net.T,
    3.28 -    swrappers: (string * (Proof.context -> wrapper)) list,
    3.29 -    uwrappers: (string * (Proof.context -> wrapper)) list,
    3.30 -    safe0_netpair: netpair,
    3.31 -    safep_netpair: netpair,
    3.32 -    haz_netpair: netpair,
    3.33 -    dup_netpair: netpair,
    3.34 -    xtra_netpair: Context_Rules.netpair}
    3.35    val print_claset: Proof.context -> unit
    3.36    val addDs: Proof.context * thm list -> Proof.context
    3.37    val addEs: Proof.context * thm list -> Proof.context
    3.38 @@ -114,6 +96,19 @@
    3.39  sig
    3.40    include BASIC_CLASSICAL
    3.41    val classical_rule: thm -> thm
    3.42 +  type netpair = (int * (bool * thm)) Net.net * (int * (bool * thm)) Net.net
    3.43 +  val rep_cs: claset ->
    3.44 +   {safeIs: thm Item_Net.T,
    3.45 +    safeEs: thm Item_Net.T,
    3.46 +    hazIs: thm Item_Net.T,
    3.47 +    hazEs: thm Item_Net.T,
    3.48 +    swrappers: (string * (Proof.context -> wrapper)) list,
    3.49 +    uwrappers: (string * (Proof.context -> wrapper)) list,
    3.50 +    safe0_netpair: netpair,
    3.51 +    safep_netpair: netpair,
    3.52 +    haz_netpair: netpair,
    3.53 +    dup_netpair: netpair,
    3.54 +    xtra_netpair: Context_Rules.netpair}
    3.55    val get_cs: Context.generic -> claset
    3.56    val map_cs: (claset -> claset) -> Context.generic -> Context.generic
    3.57    val safe_dest: int option -> attribute
    3.58 @@ -213,6 +208,9 @@
    3.59  
    3.60  (**** Classical rule sets ****)
    3.61  
    3.62 +type netpair = (int * (bool * thm)) Net.net * (int * (bool * thm)) Net.net;
    3.63 +type wrapper = (int -> tactic) -> int -> tactic;
    3.64 +
    3.65  datatype claset =
    3.66    CS of
    3.67     {safeIs         : thm Item_Net.T,          (*safe introduction rules*)