src/HOL/HOL.thy
changeset 1672 2c109cd2fdd0
parent 1370 7361ac9b024d
child 1674 33aff4d854e4
     1.1 --- a/src/HOL/HOL.thy	Tue Apr 23 16:44:22 1996 +0200
     1.2 +++ b/src/HOL/HOL.thy	Tue Apr 23 16:58:21 1996 +0200
     1.3 @@ -143,6 +143,40 @@
     1.4    if_def        "If P x y == @z::'a. (P=True --> z=x) & (P=False --> z=y)"
     1.5  
     1.6  (* start 8bit 1 *)
     1.7 +types
     1.8 +('a, 'b) ""          (infixr 5)
     1.9 +
    1.10 +syntax
    1.11 +  ""		:: "['a::{}, 'a] => prop"       ("(_ / _)"         [3, 2] 2)
    1.12 +  ""		:: "[prop, prop] => prop"	("(_ / _)"        [2, 1] 1)
    1.13 +  "Gbigimpl"	:: "[asms, prop] => prop"	("((3 _ ) / _)" [0, 1] 1)
    1.14 +  "Gall"	:: "('a => prop) => prop"	(binder ""                0)
    1.15 +
    1.16 +  "Glam"         :: "[idts, 'a::logic] => 'b::logic"  ("(3_./ _)" 10)
    1.17 +  ""           :: "['a, 'a] => bool"                 (infixl 50)
    1.18 +  "Gnot"        :: "bool => bool"                     (" _" [40] 40)
    1.19 +  "GEps"        :: "[pttrn, bool] => 'a"               ("(3_./ _)" 10)
    1.20 +  "GAll"        :: "[idts, bool] => bool"             ("(3_./ _)" 10)
    1.21 +  "GEx"         :: "[idts, bool] => bool"             ("(3_./ _)" 10)
    1.22 +  "GEx1"        :: "[idts, bool] => bool"             ("(3!_./ _)" 10)
    1.23 +  ""           :: "[bool, bool] => bool"             (infixr 35)
    1.24 +  ""           :: "[bool, bool] => bool"             (infixr 30)
    1.25 +  ""          :: "[bool, bool] => bool"             (infixr 25)
    1.26 +
    1.27 +translations
    1.28 +(type)  "x  y"	== (type) "x => y" 
    1.29 +
    1.30 +(*  "x.t"	=> "%x.t" *)
    1.31 +
    1.32 +  "x  y"	== "x ~= y"
    1.33 +  " y"		== "~y"
    1.34 +  "x.P"	== "@x.P"
    1.35 +  "x.P"	== "! x. P"
    1.36 +  "x.P"	== "? x. P"
    1.37 +  "!x.P"	== "?! x. P"
    1.38 +  "x  y"	== "x & y"
    1.39 +  "x  y"	== "x | y"
    1.40 +  "x  y"	== "x --> y"
    1.41  (* end 8bit 1 *)
    1.42  
    1.43  end
    1.44 @@ -167,6 +201,36 @@
    1.45    map alt_ast_tr' [("! ", "*All"), ("? ", "*Ex"), ("?! ", "*Ex1")];
    1.46  
    1.47  (* start 8bit 2 *)
    1.48 +local open Ast;
    1.49 +fun bigimpl_ast_tr (*"Gbigimpl"*) [asms, concl] =
    1.50 +      fold_ast_p "" (unfold_ast "_asms" asms, concl)
    1.51 +  | bigimpl_ast_tr (*"Gbigimpl"*) asts = raise_ast "bigimpl_ast_tr" asts;
    1.52 +fun impl_ast_tr' (*""*) asts =
    1.53 +  (case unfold_ast_p "" (Appl (Constant "" :: asts)) of
    1.54 +    (asms as _ :: _ :: _, concl)
    1.55 +      => Appl [Constant "Gbigimpl", fold_ast "_asms" asms, concl]
    1.56 +  | _ => raise Match);
    1.57 +
    1.58 +in
    1.59 +val parse_ast_translation = ("Gbigimpl", bigimpl_ast_tr)::
    1.60 +				("Glam",    fn asts => Appl (Constant "_abs" :: asts))::
    1.61 +				parse_ast_translation;
    1.62 +
    1.63 +val print_ast_translation = ("", impl_ast_tr')::
    1.64 +				("_lambda", fn asts => Appl (Constant "Glam" :: asts)) ::	
    1.65 +				print_ast_translation;
    1.66 +
    1.67 +end;
    1.68 +
    1.69 +local open Syntax in
    1.70 +val thy = thy 
    1.71 +|> add_trrules_i 
    1.72 +[mk_appl (Constant "" ) [Variable "P", Variable "Q"] <-> 
    1.73 + mk_appl (Constant "==") [Variable "P", Variable "Q"],
    1.74 + mk_appl (Constant "" ) [Variable "P", Variable "Q"] <-> 
    1.75 + mk_appl (Constant "==>") [Variable "P", Variable "Q"],
    1.76 + (Constant "" ) <->  (Constant "!!")]
    1.77 +end;
    1.78  (* end 8bit 2 *)
    1.79  
    1.80