--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/hol.thy Thu Sep 16 12:21:07 1993 +0200
@@ -0,0 +1,142 @@
+(* Title: HOL/hol.thy
+ ID: $Id$
+ Author: Tobias Nipkow
+ Copyright 1993 University of Cambridge
+
+Higher-Order Logic
+*)
+
+HOL = Pure +
+
+classes
+ term < logic
+ plus < term
+ minus < term
+ times < term
+
+default term
+
+types
+ bool 0
+
+arities
+ fun :: (term, term) term
+ bool :: term
+
+
+consts
+
+ (* Constants *)
+
+ Trueprop :: "bool => prop" ("(_)" [0] 5)
+ not :: "bool => bool" ("~ _" [40] 40)
+ True, False :: "bool"
+ if :: "[bool, 'a, 'a] => 'a"
+ Inv :: "('a => 'b) => ('b => 'a)"
+
+ (* Binders *)
+
+ Eps :: "('a => bool) => 'a" (binder "@" 10)
+ All :: "('a => bool) => bool" (binder "! " 10)
+ Ex :: "('a => bool) => bool" (binder "? " 10)
+ Ex1 :: "('a => bool) => bool" (binder "?! " 10)
+
+ Let :: "['a, 'a=>'b] => 'b"
+ "@let" :: "[idt,'a,'b] => 'b" ("(let _ = (2_)/ in (2_))" 10)
+
+ (* Alternative Quantifiers *)
+
+ "*All" :: "[idts, bool] => bool" ("(3ALL _./ _)" [0,0] 10)
+ "*Ex" :: "[idts, bool] => bool" ("(3EX _./ _)" [0,0] 10)
+ "*Ex1" :: "[idts, bool] => bool" ("(3EX! _./ _)" [0,0] 10)
+
+ (* Infixes *)
+
+ o :: "['b => 'c, 'a => 'b, 'a] => 'c" (infixr 50)
+ "=" :: "['a, 'a] => bool" (infixl 50)
+ "&" :: "[bool, bool] => bool" (infixr 35)
+ "|" :: "[bool, bool] => bool" (infixr 30)
+ "-->" :: "[bool, bool] => bool" (infixr 25)
+
+ (* Overloaded Constants *)
+
+ "+" :: "['a::plus, 'a] => 'a" (infixl 65)
+ "-" :: "['a::minus, 'a] => 'a" (infixl 65)
+ "*" :: "['a::times, 'a] => 'a" (infixl 70)
+
+ (* Rewriting Gadget *)
+
+ NORM :: "'a => 'a"
+
+
+translations
+ "ALL xs. P" => "! xs. P"
+ "EX xs. P" => "? xs. P"
+ "EX! xs. P" => "?! xs. P"
+
+ "let x = s in t" == "Let(s,%x.t)"
+
+rules
+
+ eq_reflection "(x=y) ==> (x==y)"
+
+ (* Basic Rules *)
+
+ refl "t = t::'a"
+ subst "[| s = t; P(s) |] ==> P(t::'a)"
+ ext "(!!x::'a. f(x)::'b = g(x)) ==> (%x.f(x)) = (%x.g(x))"
+ selectI "P(x::'a) ==> P(@x.P(x))"
+
+ impI "(P ==> Q) ==> P-->Q"
+ mp "[| P-->Q; P |] ==> Q"
+
+ (* Definitions *)
+
+ True_def "True = ((%x.x)=(%x.x))"
+ All_def "All = (%P. P = (%x.True))"
+ Ex_def "Ex = (%P. P(@x.P(x)))"
+ False_def "False = (!P.P)"
+ not_def "not = (%P. P-->False)"
+ and_def "op & = (%P Q. !R. (P-->Q-->R) --> R)"
+ or_def "op | = (%P Q. !R. (P-->R) --> (Q-->R) --> R)"
+ Ex1_def "Ex1 = (%P. ? x. P(x) & (! y. P(y) --> y=x))"
+ Let_def "Let(s,f) = f(s)"
+
+ (* Axioms *)
+
+ iff "(P-->Q) --> (Q-->P) --> (P=Q)"
+ True_or_False "(P=True) | (P=False)"
+
+ (* Misc Definitions *)
+
+ Inv_def "Inv = (%(f::'a=>'b) y. @x. f(x)=y)"
+ o_def "op o = (%(f::'b=>'c) g (x::'a). f(g(x)))"
+
+ if_def "if = (%P x y.@z::'a. (P=True --> z=x) & (P=False --> z=y))"
+
+ (* Rewriting -- special constant to flag normalized terms *)
+
+ NORM_def "NORM(x) = x"
+
+end
+
+
+ML
+
+(** Choice between the HOL and Isabelle style of quantifiers **)
+
+val HOL_quantifiers = ref true;
+
+fun mk_alt_ast_tr' (name, alt_name) =
+ let
+ fun ast_tr' (*name*) args =
+ if ! HOL_quantifiers then raise Match
+ else Ast.mk_appl (Ast.Constant alt_name) args;
+ in
+ (name, ast_tr')
+ end;
+
+
+val print_ast_translation =
+ map mk_alt_ast_tr' [("! ", "*All"), ("? ", "*Ex"), ("?! ", "*Ex1")];
+