src/HOL/ROOT.ML
author clasohm
Thu, 29 Jun 1995 12:48:48 +0200
changeset 1165 97b2bb5d43c3
parent 1024 b86042000035
child 1264 3eb91524b938
permissions -rw-r--r--
renamed CHOL to HOL
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";
1024
b86042000035 ROOT.ML: installed new hyp_subst_tac
nipkow
parents: 923
diff changeset
    21
use "../Provers/simplifier.ML";
b86042000035 ROOT.ML: installed new hyp_subst_tac
nipkow
parents: 923
diff changeset
    22
use "../Provers/splitter.ML";
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    23
use "../Provers/hypsubst.ML";
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    24
use "../Provers/classical.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
1024
b86042000035 ROOT.ML: installed new hyp_subst_tac
nipkow
parents: 923
diff changeset
    30
  structure Simplifier = Simplifier
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    31
  (*Take apart an equality judgement; otherwise raise Match!*)
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    32
  fun dest_eq (Const("Trueprop",_) $ (Const("op =",_)  $ t $ u)) = (t,u);
1024
b86042000035 ROOT.ML: installed new hyp_subst_tac
nipkow
parents: 923
diff changeset
    33
  val eq_reflection = eq_reflection
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    34
  val imp_intr = impI
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    35
  val rev_mp = rev_mp
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    36
  val subst = subst
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    37
  val sym = sym
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    38
  end;
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    39
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    40
structure Hypsubst = HypsubstFun(Hypsubst_Data);
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    41
open Hypsubst;
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    42
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    43
(*** Applying ClassicalFun to create a classical prover ***)
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    44
structure Classical_Data = 
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    45
  struct
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    46
  val sizef	= size_of_thm
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    47
  val mp	= mp
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    48
  val not_elim	= notE
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    49
  val classical	= classical
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    50
  val hyp_subst_tacs=[hyp_subst_tac]
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    51
  end;
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    52
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    53
structure Classical = ClassicalFun(Classical_Data);
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    54
open Classical;
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    55
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    56
(*Propositional rules*)
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    57
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
    58
                       addSEs [conjE,disjE,impCE,FalseE,iffE];
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    59
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    60
(*Quantifier rules*)
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    61
val HOL_cs = prop_cs addSIs [allI] addIs [exI,ex1I]
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    62
                     addSEs [exE,ex1E] addEs [allE];
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    63
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    64
use     "simpdata.ML";
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    65
use_thy "Ord";
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    66
use_thy "subset";
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    67
use_thy "equalities";
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    68
use     "hologic.ML";
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    69
use     "subtype.ML";
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    70
use_thy "Prod";
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    71
use_thy "Sum";
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    72
use_thy "Gfp";
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    73
use_thy "Nat";
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    74
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    75
use "datatype.ML";
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    76
use "ind_syntax.ML";
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    77
use "add_ind_def.ML";
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    78
use "intr_elim.ML";
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    79
use "indrule.ML";
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    80
use_thy "Inductive";
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    81
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    82
use_thy "Finite";
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    83
use_thy "Sexp";
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    84
use_thy "List";
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    85
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    86
init_pps ();
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    87
print_depth 8;
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    88
1165
97b2bb5d43c3 renamed CHOL to HOL
clasohm
parents: 1024
diff changeset
    89
val HOL_build_completed = ();   (*indicate successful build*)