author | wenzelm |
Mon, 03 Nov 1997 21:12:21 +0100 | |
changeset 4104 | 84433b1ab826 |
parent 3370 | 5c5fdce3a4e4 |
child 4613 | 67a726003cf8 |
permissions | -rw-r--r-- |
923 | 1 |
(* Title: HOL/Nat.thy |
2 |
ID: $Id$ |
|
2608 | 3 |
Author: Tobias Nipkow |
4 |
Copyright 1997 TU Muenchen |
|
923 | 5 |
|
2608 | 6 |
Nat is a partial order |
923 | 7 |
*) |
8 |
||
2608 | 9 |
Nat = NatDef + |
923 | 10 |
|
4104 | 11 |
(*install 'automatic' induction tactic, pretending nat is a datatype |
12 |
except for induct_tac and exhaust_tac, everything is dummy*) |
|
13 |
||
14 |
MLtext {| |
|
15 |
|> Dtype.add_datatype_info |
|
16 |
("nat", {case_const = Bound 0, case_rewrites = [], |
|
17 |
constructors = [], induct_tac = nat_ind_tac, |
|
18 |
exhaustion = natE, |
|
19 |
exhaust_tac = fn v => ALLNEWSUBGOALS (res_inst_tac [("n",v)] natE) |
|
20 |
(rotate_tac ~1), |
|
21 |
nchotomy = ProtoPure.flexpair_def, case_cong = ProtoPure.flexpair_def}) |
|
22 |
|} |
|
23 |
||
24 |
||
2608 | 25 |
instance nat :: order (le_refl,le_trans,le_anti_sym,nat_less_le) |
1660 | 26 |
|
3370
5c5fdce3a4e4
Overloading of "^" requires new type class "power", with types "nat" and
paulson
parents:
2608
diff
changeset
|
27 |
consts |
5c5fdce3a4e4
Overloading of "^" requires new type class "power", with types "nat" and
paulson
parents:
2608
diff
changeset
|
28 |
"^" :: ['a::power,nat] => 'a (infixr 80) |
5c5fdce3a4e4
Overloading of "^" requires new type class "power", with types "nat" and
paulson
parents:
2608
diff
changeset
|
29 |
|
923 | 30 |
end |