equal
deleted
inserted
replaced
1 (* Title: HOLCF/One.ML |
|
2 ID: $Id$ |
|
3 Author: Oscar Slotosch |
|
4 |
1 |
5 The unit domain. |
2 (* legacy ML bindings *) |
6 *) |
|
7 |
3 |
8 (* ------------------------------------------------------------------------ *) |
4 val Exh_one = thm "Exh_one"; |
9 (* Exhaustion and Elimination for type one *) |
5 val oneE = thm "oneE"; |
10 (* ------------------------------------------------------------------------ *) |
6 val dist_less_one = thm "dist_less_one"; |
11 |
7 val dist_eq_one = thms "dist_eq_one"; |
12 Goalw [ONE_def] "t=UU | t = ONE"; |
|
13 by (induct_tac "t" 1); |
|
14 by (Simp_tac 1); |
|
15 by (Simp_tac 1); |
|
16 qed "Exh_one"; |
|
17 |
|
18 val prems = Goal "[| p=UU ==> Q; p = ONE ==>Q|] ==>Q"; |
|
19 by (rtac (Exh_one RS disjE) 1); |
|
20 by (eresolve_tac prems 1); |
|
21 by (eresolve_tac prems 1); |
|
22 qed "oneE"; |
|
23 |
|
24 (* ------------------------------------------------------------------------ *) |
|
25 (* tactic for one-thms *) |
|
26 (* ------------------------------------------------------------------------ *) |
|
27 |
|
28 fun prover t = prove_goalw thy [ONE_def] t |
|
29 (fn prems => |
|
30 [ |
|
31 (asm_simp_tac (simpset() addsimps [inst_lift_po]) 1) |
|
32 ]); |
|
33 |
|
34 (* ------------------------------------------------------------------------ *) |
|
35 (* distinctness for type one : stored in a list *) |
|
36 (* ------------------------------------------------------------------------ *) |
|
37 |
|
38 val dist_less_one = map prover ["~ONE << UU"]; |
|
39 |
|
40 val dist_eq_one = map prover ["ONE~=UU","UU~=ONE"]; |
|
41 |
|
42 Addsimps (dist_less_one@dist_eq_one); |
|