diff -r 000000000000 -r 7949f97df77a hol.thy --- /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")]; +