author | paulson |
Wed, 27 Oct 1999 12:50:48 +0200 (1999-10-27) | |
changeset 7945 | 3aca6352f063 |
parent 5087 | ee8a754f1981 |
child 9245 | 428385c4bc50 |
permissions | -rw-r--r-- |
2275 | 1 |
(* Title: HOLCF/One.ML |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
2 |
ID: $Id$ |
2640 | 3 |
Author: Oscar Slotosch |
4 |
Copyright 1997 Technische Universitaet Muenchen |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
5 |
|
2640 | 6 |
Lemmas for One.thy |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
7 |
*) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
8 |
|
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
9 |
open One; |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
10 |
|
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
11 |
(* ------------------------------------------------------------------------ *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
12 |
(* Exhaustion and Elimination for type one *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
13 |
(* ------------------------------------------------------------------------ *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
14 |
|
2640 | 15 |
qed_goalw "Exh_one" thy [ONE_def] "t=UU | t = ONE" |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
16 |
(fn prems => |
1461 | 17 |
[ |
2640 | 18 |
(lift.induct_tac "t" 1), |
19 |
(Simp_tac 1), |
|
5087 | 20 |
(Simp_tac 1) |
2640 | 21 |
]); |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
22 |
|
2640 | 23 |
qed_goal "oneE" thy |
24 |
"[| p=UU ==> Q; p = ONE ==>Q|] ==>Q" |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
25 |
(fn prems => |
1461 | 26 |
[ |
27 |
(rtac (Exh_one RS disjE) 1), |
|
28 |
(eresolve_tac prems 1), |
|
29 |
(eresolve_tac prems 1) |
|
30 |
]); |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
31 |
|
2640 | 32 |
(* ------------------------------------------------------------------------ *) |
33 |
(* tactic for one-thms *) |
|
34 |
(* ------------------------------------------------------------------------ *) |
|
35 |
||
36 |
fun prover t = prove_goalw thy [ONE_def] t |
|
37 |
(fn prems => |
|
38 |
[ |
|
4098 | 39 |
(asm_simp_tac (simpset() addsimps [inst_lift_po]) 1) |
2640 | 40 |
]); |
41 |
||
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
42 |
(* ------------------------------------------------------------------------ *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
43 |
(* distinctness for type one : stored in a list *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
44 |
(* ------------------------------------------------------------------------ *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
45 |
|
2640 | 46 |
val dist_less_one = map prover ["~ONE << UU"]; |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
47 |
|
2640 | 48 |
val dist_eq_one = map prover ["ONE~=UU","UU~=ONE"]; |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
49 |
|
2640 | 50 |
Addsimps (dist_less_one@dist_eq_one); |