26 |
26 |
27 consts |
27 consts |
28 |
28 |
29 (* Constants *) |
29 (* Constants *) |
30 |
30 |
31 Trueprop :: "bool => prop" ("(_)" [0] 5) |
31 Trueprop :: "bool => prop" ("(_)" 5) |
32 not :: "bool => bool" ("~ _" [40] 40) |
32 not :: "bool => bool" ("~ _" [40] 40) |
33 True, False :: "bool" |
33 True, False :: "bool" |
34 if :: "[bool, 'a, 'a] => 'a" |
34 if :: "[bool, 'a, 'a] => 'a" |
35 Inv :: "('a => 'b) => ('b => 'a)" |
35 Inv :: "('a => 'b) => ('b => 'a)" |
36 |
36 |
37 (* Binders *) |
37 (* Binders *) |
38 |
38 |
39 Eps :: "('a => bool) => 'a" (binder "@" 10) |
39 Eps :: "('a => bool) => 'a" (binder "@" 10) |
40 All :: "('a => bool) => bool" (binder "! " 10) |
40 All :: "('a => bool) => bool" (binder "! " 10) |
41 Ex :: "('a => bool) => bool" (binder "? " 10) |
41 Ex :: "('a => bool) => bool" (binder "? " 10) |
42 Ex1 :: "('a => bool) => bool" (binder "?! " 10) |
42 Ex1 :: "('a => bool) => bool" (binder "?! " 10) |
43 |
43 |
44 Let :: "['a, 'a=>'b] => 'b" |
44 Let :: "['a, 'a => 'b] => 'b" |
45 "@let" :: "[idt,'a,'b] => 'b" ("(let _ = (2_)/ in (2_))" 10) |
45 "@Let" :: "[idt, 'a, 'b] => 'b" ("(let _ = (2_)/ in (2_))" 10) |
46 |
46 |
47 (* Alternative Quantifiers *) |
47 (* Alternative Quantifiers *) |
48 |
48 |
49 "*All" :: "[idts, bool] => bool" ("(3ALL _./ _)" [0,0] 10) |
49 "*The" :: "[idts, bool] => 'a" ("(3THE _./ _)" 10) |
50 "*Ex" :: "[idts, bool] => bool" ("(3EX _./ _)" [0,0] 10) |
50 "*All" :: "[idts, bool] => bool" ("(3ALL _./ _)" 10) |
51 "*Ex1" :: "[idts, bool] => bool" ("(3EX! _./ _)" [0,0] 10) |
51 "*Ex" :: "[idts, bool] => bool" ("(3EX _./ _)" 10) |
|
52 "*Ex1" :: "[idts, bool] => bool" ("(3EX! _./ _)" 10) |
52 |
53 |
53 (* Infixes *) |
54 (* Infixes *) |
54 |
55 |
55 o :: "['b => 'c, 'a => 'b, 'a] => 'c" (infixr 50) |
56 o :: "['b => 'c, 'a => 'b, 'a] => 'c" (infixr 50) |
56 "=" :: "['a, 'a] => bool" (infixl 50) |
57 "=" :: "['a, 'a] => bool" (infixl 50) |
57 "&" :: "[bool, bool] => bool" (infixr 35) |
58 "&" :: "[bool, bool] => bool" (infixr 35) |
58 "|" :: "[bool, bool] => bool" (infixr 30) |
59 "|" :: "[bool, bool] => bool" (infixr 30) |
59 "-->" :: "[bool, bool] => bool" (infixr 25) |
60 "-->" :: "[bool, bool] => bool" (infixr 25) |
60 |
61 |
61 (* Overloaded Constants *) |
62 (* Overloaded Constants *) |
62 |
63 |
63 "+" :: "['a::plus, 'a] => 'a" (infixl 65) |
64 "+" :: "['a::plus, 'a] => 'a" (infixl 65) |
64 "-" :: "['a::minus, 'a] => 'a" (infixl 65) |
65 "-" :: "['a::minus, 'a] => 'a" (infixl 65) |
65 "*" :: "['a::times, 'a] => 'a" (infixl 70) |
66 "*" :: "['a::times, 'a] => 'a" (infixl 70) |
66 |
67 |
67 (* Rewriting Gadget *) |
68 (* Rewriting Gadget *) |
68 |
69 |
69 NORM :: "'a => 'a" |
70 NORM :: "'a => 'a" |
70 |
71 |
71 |
72 |
72 translations |
73 translations |
|
74 "THE xs. P" => "@ xs. P" |
73 "ALL xs. P" => "! xs. P" |
75 "ALL xs. P" => "! xs. P" |
74 "EX xs. P" => "? xs. P" |
76 "EX xs. P" => "? xs. P" |
75 "EX! xs. P" => "?! xs. P" |
77 "EX! xs. P" => "?! xs. P" |
76 |
78 |
77 "let x = s in t" == "Let(s,%x.t)" |
79 "let x = s in t" == "Let(s, %x. t)" |
78 |
80 |
79 rules |
81 rules |
80 |
82 |
81 eq_reflection "(x=y) ==> (x==y)" |
83 eq_reflection "(x=y) ==> (x==y)" |
82 |
84 |
98 False_def "False = (!P.P)" |
100 False_def "False = (!P.P)" |
99 not_def "not = (%P. P-->False)" |
101 not_def "not = (%P. P-->False)" |
100 and_def "op & = (%P Q. !R. (P-->Q-->R) --> R)" |
102 and_def "op & = (%P Q. !R. (P-->Q-->R) --> R)" |
101 or_def "op | = (%P Q. !R. (P-->R) --> (Q-->R) --> R)" |
103 or_def "op | = (%P Q. !R. (P-->R) --> (Q-->R) --> R)" |
102 Ex1_def "Ex1 = (%P. ? x. P(x) & (! y. P(y) --> y=x))" |
104 Ex1_def "Ex1 = (%P. ? x. P(x) & (! y. P(y) --> y=x))" |
103 Let_def "Let(s,f) = f(s)" |
105 Let_def "Let(s, f) = f(s)" |
104 |
106 |
105 (* Axioms *) |
107 (* Axioms *) |
106 |
108 |
107 iff "(P-->Q) --> (Q-->P) --> (P=Q)" |
109 iff "(P-->Q) --> (Q-->P) --> (P=Q)" |
108 True_or_False "(P=True) | (P=False)" |
110 True_or_False "(P=True) | (P=False)" |
125 |
127 |
126 (** Choice between the HOL and Isabelle style of quantifiers **) |
128 (** Choice between the HOL and Isabelle style of quantifiers **) |
127 |
129 |
128 val HOL_quantifiers = ref true; |
130 val HOL_quantifiers = ref true; |
129 |
131 |
130 fun mk_alt_ast_tr' (name, alt_name) = |
132 fun alt_ast_tr' (name, alt_name) = |
131 let |
133 let |
132 fun ast_tr' (*name*) args = |
134 fun ast_tr' (*name*) args = |
133 if ! HOL_quantifiers then raise Match |
135 if ! HOL_quantifiers then raise Match |
134 else Ast.mk_appl (Ast.Constant alt_name) args; |
136 else Syntax.mk_appl (Syntax.Constant alt_name) args; |
135 in |
137 in |
136 (name, ast_tr') |
138 (name, ast_tr') |
137 end; |
139 end; |
138 |
140 |
139 |
141 |
140 val print_ast_translation = |
142 val print_ast_translation = |
141 map mk_alt_ast_tr' [("! ", "*All"), ("? ", "*Ex"), ("?! ", "*Ex1")]; |
143 map alt_ast_tr' [("@", "*The"), ("! ", "*All"), ("? ", "*Ex"), ("?! ", "*Ex1")]; |
142 |
144 |