author | paulson |
Tue, 04 Jul 2000 15:58:11 +0200 | |
changeset 9245 | 428385c4bc50 |
parent 5291 | 5706f0ef1d43 |
child 9248 | e1dee89de037 |
permissions | -rw-r--r-- |
2640 | 1 |
(* Title: HOLCF/Cfun1.ML |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
2 |
ID: $Id$ |
1461 | 3 |
Author: Franz Regensburger |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
4 |
Copyright 1993 Technische Universitaet Muenchen |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
5 |
|
9245 | 6 |
The type -> of continuous functions. |
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 |
(* ------------------------------------------------------------------------ *) |
5291 | 10 |
(* derive old type definition rules for Abs_CFun & Rep_CFun *) |
11 |
(* Rep_CFun and Abs_CFun should be replaced by Rep_Cfun anf Abs_Cfun in future *) |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
12 |
(* ------------------------------------------------------------------------ *) |
9245 | 13 |
val prems = goal thy "Rep_CFun fo : CFun"; |
14 |
by (rtac Rep_CFun 1); |
|
15 |
qed "Rep_Cfun"; |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
16 |
|
9245 | 17 |
val prems = goal thy "Abs_CFun (Rep_CFun fo) = fo"; |
18 |
by (rtac Rep_CFun_inverse 1); |
|
19 |
qed "Rep_Cfun_inverse"; |
|
2640 | 20 |
|
9245 | 21 |
val prems = goal thy "f:CFun==>Rep_CFun(Abs_CFun f)=f"; |
22 |
by (cut_facts_tac prems 1); |
|
23 |
by (etac Abs_CFun_inverse 1); |
|
24 |
qed "Abs_Cfun_inverse"; |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
25 |
|
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
26 |
(* ------------------------------------------------------------------------ *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
27 |
(* less_cfun is a partial order on type 'a -> 'b *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
28 |
(* ------------------------------------------------------------------------ *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
29 |
|
9245 | 30 |
val prems = goalw thy [less_cfun_def] "(f::'a->'b) << f"; |
31 |
by (rtac refl_less 1); |
|
32 |
qed "refl_less_cfun"; |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
33 |
|
9245 | 34 |
val prems = goalw thy [less_cfun_def] |
35 |
"[|(f1::'a->'b) << f2; f2 << f1|] ==> f1 = f2"; |
|
36 |
by (cut_facts_tac prems 1); |
|
37 |
by (rtac injD 1); |
|
38 |
by (rtac antisym_less 2); |
|
39 |
by (atac 3); |
|
40 |
by (atac 2); |
|
41 |
by (rtac inj_inverseI 1); |
|
42 |
by (rtac Rep_Cfun_inverse 1); |
|
43 |
qed "antisym_less_cfun"; |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
44 |
|
9245 | 45 |
val prems = goalw thy [less_cfun_def] |
46 |
"[|(f1::'a->'b) << f2; f2 << f3|] ==> f1 << f3"; |
|
47 |
by (cut_facts_tac prems 1); |
|
48 |
by (etac trans_less 1); |
|
49 |
by (atac 1); |
|
50 |
qed "trans_less_cfun"; |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
51 |
|
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
52 |
(* ------------------------------------------------------------------------ *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
53 |
(* lemmas about application of continuous functions *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
54 |
(* ------------------------------------------------------------------------ *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
55 |
|
9245 | 56 |
val prems = goal thy |
57 |
"[| f=g; x=y |] ==> f`x = g`y"; |
|
58 |
by (cut_facts_tac prems 1); |
|
59 |
by (fast_tac HOL_cs 1); |
|
60 |
qed "cfun_cong"; |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
61 |
|
9245 | 62 |
val prems = goal thy "f=g ==> f`x = g`x"; |
63 |
by (cut_facts_tac prems 1); |
|
64 |
by (etac cfun_cong 1); |
|
65 |
by (rtac refl 1); |
|
66 |
qed "cfun_fun_cong"; |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
67 |
|
9245 | 68 |
val prems = goal thy "x=y ==> f`x = f`y"; |
69 |
by (cut_facts_tac prems 1); |
|
70 |
by (rtac cfun_cong 1); |
|
71 |
by (rtac refl 1); |
|
72 |
by (atac 1); |
|
73 |
qed "cfun_arg_cong"; |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
74 |
|
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
75 |
|
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
76 |
(* ------------------------------------------------------------------------ *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
77 |
(* additional lemma about the isomorphism between -> and Cfun *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
78 |
(* ------------------------------------------------------------------------ *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
79 |
|
9245 | 80 |
val prems = goal thy "cont f ==> Rep_CFun (Abs_CFun f) = f"; |
81 |
by (cut_facts_tac prems 1); |
|
82 |
by (rtac Abs_Cfun_inverse 1); |
|
83 |
by (rewtac CFun_def); |
|
84 |
by (etac (mem_Collect_eq RS ssubst) 1); |
|
85 |
qed "Abs_Cfun_inverse2"; |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
86 |
|
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
87 |
(* ------------------------------------------------------------------------ *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
88 |
(* simplification of application *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
89 |
(* ------------------------------------------------------------------------ *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
90 |
|
9245 | 91 |
val prems = goal thy "cont f ==> (Abs_CFun f)`x = f x"; |
92 |
by (cut_facts_tac prems 1); |
|
93 |
by (etac (Abs_Cfun_inverse2 RS fun_cong) 1); |
|
94 |
qed "Cfunapp2"; |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
95 |
|
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
96 |
(* ------------------------------------------------------------------------ *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
97 |
(* beta - equality for continuous functions *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
98 |
(* ------------------------------------------------------------------------ *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
99 |
|
9245 | 100 |
val prems = goal thy |
101 |
"cont(c1) ==> (LAM x .c1 x)`u = c1 u"; |
|
102 |
by (cut_facts_tac prems 1); |
|
103 |
by (rtac Cfunapp2 1); |
|
104 |
by (atac 1); |
|
105 |
qed "beta_cfun"; |