ROOT.ML

HOL/ROOT/HOL_dup_cs: removed as obsolete
HOL/ROOT: now passes "classical" to Classical_Fun
HOL/ROOT: no longer proves rev_cut_eq for hyp_subst_tac

(*  Title:      HOL/ROOT.ML
    ID:         $Id$
    Author:     Tobias Nipkow
    Copyright   1993  University of Cambridge

Adds Classical Higher-order Logic to a database containing Pure Isabelle.
Should be executed in the subdirectory HOL.
*)

val banner = "Higher-Order Logic";
writeln banner;

print_depth 1;
set eta_contract;

(* Add user sections *)
use "../Pure/section_utils.ML";
use "thy_syntax.ML";

use_thy "HOL";
use "../Provers/hypsubst.ML";
use "../Provers/classical.ML";
use "../Provers/simplifier.ML";
use "../Provers/splitter.ML";
use "../Provers/ind.ML";

(** Applying HypsubstFun to generate hyp_subst_tac **)

structure Hypsubst_Data =
  struct
  (*Take apart an equality judgement; otherwise raise Match!*)
  fun dest_eq (Const("Trueprop",_) $ (Const("op =",_)  $ t $ u)) = (t,u);
  val imp_intr = impI
  val rev_mp = rev_mp
  val subst = subst
  val sym = sym
  end;

structure Hypsubst = HypsubstFun(Hypsubst_Data);
open Hypsubst;

(*** Applying ClassicalFun to create a classical prover ***)
structure Classical_Data = 
  struct
  val sizef	= size_of_thm
  val mp	= mp
  val not_elim	= notE
  val classical	= classical
  val hyp_subst_tacs=[hyp_subst_tac]
  end;

structure Classical = ClassicalFun(Classical_Data);
open Classical;

(*Propositional rules*)
val prop_cs = empty_cs addSIs [refl,TrueI,conjI,disjCI,impI,notI,iffI]
                       addSEs [conjE,disjE,impCE,FalseE,iffE];

(*Quantifier rules*)
val HOL_cs = prop_cs addSIs [allI] addIs [exI,ex1I]
                     addSEs [exE,ex1E] addEs [allE];

structure HOL_Induction = InductionFun(struct val spec=spec end);
open HOL_Induction;

use     "simpdata.ML";
use_thy "Ord";
use_thy "subset";
use_thy "equalities";
use     "hologic.ML";
use     "subtype.ML";
use_thy "Prod";
use_thy "Sum";
use_thy "Gfp";
use_thy "Nat";

use "datatype.ML";
use "ind_syntax.ML";
use "add_ind_def.ML";
use "intr_elim.ML";
use "indrule.ML";
use "Inductive.ML";

(* FIXME -> thy_syntax.ML *)
structure ThySynData =
struct
  val user_keywords = ThySynData.user_keywords;

  val user_sections = ThySynData.user_sections @
   [("datatype", datatype_decls),
    ("primrec", primrec_decl)];
end;
structure ThySyn = ThySynFun(ThySynData);
init_thy_reader ();


use_thy "Finite";
use_thy "List";

init_pps ();
print_depth 8;

val HOL_build_completed = ();   (*indicate successful build*)