src/HOL/cladata.ML
changeset 1985 84cf16192e03
child 2860 6dde30a9e905
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/cladata.ML	Thu Sep 12 10:40:05 1996 +0200
     1.3 @@ -0,0 +1,63 @@
     1.4 +(*  Title:      HOL/cladata.ML
     1.5 +    ID:         $Id$
     1.6 +    Author:     Tobias Nipkow
     1.7 +    Copyright   1996  University of Cambridge
     1.8 +
     1.9 +Setting up the classical reasoner 
    1.10 +*)
    1.11 +
    1.12 +
    1.13 +(** Applying HypsubstFun to generate hyp_subst_tac **)
    1.14 +section "Classical Reasoner";
    1.15 +
    1.16 +structure Hypsubst_Data =
    1.17 +  struct
    1.18 +  structure Simplifier = Simplifier
    1.19 +  (*Take apart an equality judgement; otherwise raise Match!*)
    1.20 +  fun dest_eq (Const("Trueprop",_) $ (Const("op =",_)  $ t $ u)) = (t,u);
    1.21 +  val eq_reflection = eq_reflection
    1.22 +  val imp_intr = impI
    1.23 +  val rev_mp = rev_mp
    1.24 +  val subst = subst
    1.25 +  val sym = sym
    1.26 +  end;
    1.27 +
    1.28 +structure Hypsubst = HypsubstFun(Hypsubst_Data);
    1.29 +open Hypsubst;
    1.30 +
    1.31 +(*** Applying ClassicalFun to create a classical prover ***)
    1.32 +structure Classical_Data = 
    1.33 +  struct
    1.34 +  val sizef     = size_of_thm
    1.35 +  val mp        = mp
    1.36 +  val not_elim  = notE
    1.37 +  val classical = classical
    1.38 +  val hyp_subst_tacs=[hyp_subst_tac]
    1.39 +  end;
    1.40 +
    1.41 +structure Classical = ClassicalFun(Classical_Data);
    1.42 +open Classical;
    1.43 +
    1.44 +(*Propositional rules*)
    1.45 +val prop_cs = empty_cs addSIs [refl,TrueI,conjI,disjCI,impI,notI,iffI]
    1.46 +                       addSEs [conjE,disjE,impCE,FalseE,iffE];
    1.47 +
    1.48 +(*Quantifier rules*)
    1.49 +val HOL_cs = prop_cs addSIs [allI] addIs [exI,ex1I]
    1.50 +                     addSEs [exE,ex1E] addEs [allE];
    1.51 +
    1.52 +exception CS_DATA of claset;
    1.53 +
    1.54 +let fun merge [] = CS_DATA empty_cs
    1.55 +      | merge cs = let val cs = map (fn CS_DATA x => x) cs;
    1.56 +                   in CS_DATA (foldl merge_cs (hd cs, tl cs)) end;
    1.57 +
    1.58 +    fun put (CS_DATA cs) = claset := cs;
    1.59 +
    1.60 +    fun get () = CS_DATA (!claset);
    1.61 +in add_thydata "HOL"
    1.62 +     ("claset", ThyMethods {merge = merge, put = put, get = get})
    1.63 +end;
    1.64 +
    1.65 +claset := HOL_cs;
    1.66 +