src/HOL/ROOT.ML
author clasohm
Fri, 03 Mar 1995 12:02:25 +0100
changeset 923 ff1574a81019
child 1024 b86042000035
permissions -rw-r--r--
new version of HOL with curried function application
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
     1
(*  Title:      CHOL/ROOT.ML
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
     2
    ID:         $Id$
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
     3
    Author:     Tobias Nipkow
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
     4
    Copyright   1993  University of Cambridge
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
     5
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
     6
Adds Classical Higher-order Logic to a database containing Pure Isabelle.
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
     7
Should be executed in the subdirectory HOL.
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
     8
*)
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
     9
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    10
val banner = "Higher-Order Logic with curried functions";
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    11
writeln banner;
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    12
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    13
print_depth 1;
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    14
set eta_contract;
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    15
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    16
(* Add user sections *)
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    17
use "../Pure/section_utils.ML";
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    18
use "thy_syntax.ML";
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    19
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    20
use_thy "HOL";
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    21
use "../Provers/hypsubst.ML";
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    22
use "../Provers/classical.ML";
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    23
use "../Provers/simplifier.ML";
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    24
use "../Provers/splitter.ML";
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    25
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    26
(** Applying HypsubstFun to generate hyp_subst_tac **)
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    27
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    28
structure Hypsubst_Data =
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    29
  struct
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    30
  (*Take apart an equality judgement; otherwise raise Match!*)
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    31
  fun dest_eq (Const("Trueprop",_) $ (Const("op =",_)  $ t $ u)) = (t,u);
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    32
  val imp_intr = impI
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    33
  val rev_mp = rev_mp
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    34
  val subst = subst
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    35
  val sym = sym
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    36
  end;
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    37
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    38
structure Hypsubst = HypsubstFun(Hypsubst_Data);
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    39
open Hypsubst;
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    40
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    41
(*** Applying ClassicalFun to create a classical prover ***)
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    42
structure Classical_Data = 
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    43
  struct
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    44
  val sizef	= size_of_thm
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    45
  val mp	= mp
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    46
  val not_elim	= notE
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    47
  val classical	= classical
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    48
  val hyp_subst_tacs=[hyp_subst_tac]
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    49
  end;
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    50
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    51
structure Classical = ClassicalFun(Classical_Data);
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    52
open Classical;
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    53
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    54
(*Propositional rules*)
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    55
val prop_cs = empty_cs addSIs [refl,TrueI,conjI,disjCI,impI,notI,iffI]
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    56
                       addSEs [conjE,disjE,impCE,FalseE,iffE];
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    57
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    58
(*Quantifier rules*)
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    59
val HOL_cs = prop_cs addSIs [allI] addIs [exI,ex1I]
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    60
                     addSEs [exE,ex1E] addEs [allE];
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    61
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    62
use     "simpdata.ML";
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    63
use_thy "Ord";
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    64
use_thy "subset";
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    65
use_thy "equalities";
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    66
use     "hologic.ML";
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    67
use     "subtype.ML";
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    68
use_thy "Prod";
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    69
use_thy "Sum";
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    70
use_thy "Gfp";
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    71
use_thy "Nat";
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    72
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    73
use "datatype.ML";
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    74
use "ind_syntax.ML";
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    75
use "add_ind_def.ML";
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    76
use "intr_elim.ML";
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    77
use "indrule.ML";
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    78
use_thy "Inductive";
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    79
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    80
use_thy "Finite";
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    81
use_thy "Sexp";
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    82
use_thy "List";
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    83
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    84
init_pps ();
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    85
print_depth 8;
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    86
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    87
val CHOL_build_completed = ();   (*indicate successful build*)