author | huffman |
Thu, 26 May 2005 02:24:08 +0200 | |
changeset 16082 | ebb53ebfd4e2 |
parent 16079 | 757e1c4a8081 |
child 16214 | e3816a7db016 |
permissions | -rw-r--r-- |
2640 | 1 |
(* Title: HOLCF/Fix.thy |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
2 |
ID: $Id$ |
1479 | 3 |
Author: Franz Regensburger |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
4 |
|
16070
4a83dd540b88
removed LICENCE note -- everything is subject to Isabelle licence as
wenzelm
parents:
16056
diff
changeset
|
5 |
Definitions for fixed point operator and admissibility. |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
6 |
*) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
7 |
|
15577 | 8 |
header {* Fixed point operator and admissibility *} |
9 |
||
10 |
theory Fix |
|
16056
32c3b7188c28
Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
16006
diff
changeset
|
11 |
imports Cfun Cprod Adm |
15577 | 12 |
begin |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
13 |
|
16082 | 14 |
defaultsort pcpo |
15 |
||
16005 | 16 |
subsection {* Definitions *} |
17 |
||
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
18 |
consts |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
19 |
|
1990 | 20 |
iterate :: "nat=>('a->'a)=>'a=>'a" |
21 |
Ifix :: "('a->'a)=>'a" |
|
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
22 |
"fix" :: "('a->'a)->'a" |
1990 | 23 |
admw :: "('a=>bool)=>bool" |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
24 |
|
5192 | 25 |
primrec |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
26 |
iterate_0: "iterate 0 F x = x" |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
27 |
iterate_Suc: "iterate (Suc n) F x = F$(iterate n F x)" |
5192 | 28 |
|
1168
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
1150
diff
changeset
|
29 |
defs |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
30 |
|
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
31 |
Ifix_def: "Ifix F == lub(range(%i. iterate i F UU))" |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
32 |
fix_def: "fix == (LAM f. Ifix f)" |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
33 |
|
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
34 |
admw_def: "admw P == !F. (!n. P (iterate n F UU)) --> |
1479 | 35 |
P (lub(range (%i. iterate i F UU)))" |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
36 |
|
16005 | 37 |
subsection {* Binder syntax for @{term fix} *} |
15857 | 38 |
|
39 |
syntax |
|
40 |
"@FIX" :: "('a => 'a) => 'a" (binder "FIX " 10) |
|
41 |
"@FIXP" :: "[patterns, 'a] => 'a" ("(3FIX <_>./ _)" [0, 10] 10) |
|
42 |
||
43 |
syntax (xsymbols) |
|
44 |
"FIX " :: "[idt, 'a] => 'a" ("(3\<mu>_./ _)" [0, 10] 10) |
|
45 |
"@FIXP" :: "[patterns, 'a] => 'a" ("(3\<mu>()<_>./ _)" [0, 10] 10) |
|
46 |
||
47 |
translations |
|
48 |
"FIX x. LAM y. t" == "fix\<cdot>(LAM x y. t)" |
|
49 |
"FIX x. t" == "fix\<cdot>(LAM x. t)" |
|
50 |
"FIX <xs>. t" == "fix\<cdot>(LAM <xs>. t)" |
|
51 |
||
16005 | 52 |
subsection {* Properties of @{term iterate} and @{term fix} *} |
53 |
||
15637
d2a06007ebfa
changed comments to text blocks, cleaned up a few proofs
huffman
parents:
15577
diff
changeset
|
54 |
text {* derive inductive properties of iterate from primitive recursion *} |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
55 |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
56 |
lemma iterate_Suc2: "iterate (Suc n) F x = iterate n F (F$x)" |
16005 | 57 |
by (induct_tac "n", auto) |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
58 |
|
15637
d2a06007ebfa
changed comments to text blocks, cleaned up a few proofs
huffman
parents:
15577
diff
changeset
|
59 |
text {* |
d2a06007ebfa
changed comments to text blocks, cleaned up a few proofs
huffman
parents:
15577
diff
changeset
|
60 |
The sequence of function iterations is a chain. |
d2a06007ebfa
changed comments to text blocks, cleaned up a few proofs
huffman
parents:
15577
diff
changeset
|
61 |
This property is essential since monotonicity of iterate makes no sense. |
d2a06007ebfa
changed comments to text blocks, cleaned up a few proofs
huffman
parents:
15577
diff
changeset
|
62 |
*} |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
63 |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
64 |
lemma chain_iterate2: "x << F$x ==> chain (%i. iterate i F x)" |
16005 | 65 |
by (rule chainI, induct_tac "i", auto elim: monofun_cfun_arg) |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
66 |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
67 |
lemma chain_iterate: "chain (%i. iterate i F UU)" |
16005 | 68 |
by (rule chain_iterate2 [OF minimal]) |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
69 |
|
15637
d2a06007ebfa
changed comments to text blocks, cleaned up a few proofs
huffman
parents:
15577
diff
changeset
|
70 |
text {* |
d2a06007ebfa
changed comments to text blocks, cleaned up a few proofs
huffman
parents:
15577
diff
changeset
|
71 |
Kleene's fixed point theorems for continuous functions in pointed |
d2a06007ebfa
changed comments to text blocks, cleaned up a few proofs
huffman
parents:
15577
diff
changeset
|
72 |
omega cpo's |
d2a06007ebfa
changed comments to text blocks, cleaned up a few proofs
huffman
parents:
15577
diff
changeset
|
73 |
*} |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
74 |
|
16005 | 75 |
lemma Ifix_eq: "Ifix F = F$(Ifix F)" |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
76 |
apply (unfold Ifix_def) |
16005 | 77 |
apply (subst lub_range_shift [of _ 1, symmetric]) |
78 |
apply (rule chain_iterate) |
|
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
79 |
apply (subst contlub_cfun_arg) |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
80 |
apply (rule chain_iterate) |
16005 | 81 |
apply simp |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
82 |
done |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
83 |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
84 |
lemma Ifix_least: "F$x=x ==> Ifix(F) << x" |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
85 |
apply (unfold Ifix_def) |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
86 |
apply (rule is_lub_thelub) |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
87 |
apply (rule chain_iterate) |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
88 |
apply (rule ub_rangeI) |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
89 |
apply (induct_tac "i") |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
90 |
apply (simp (no_asm_simp)) |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
91 |
apply (simp (no_asm_simp)) |
16005 | 92 |
apply (erule_tac t = "x" in subst) |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
93 |
apply (erule monofun_cfun_arg) |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
94 |
done |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
95 |
|
15637
d2a06007ebfa
changed comments to text blocks, cleaned up a few proofs
huffman
parents:
15577
diff
changeset
|
96 |
text {* monotonicity and continuity of @{term iterate} *} |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
97 |
|
16005 | 98 |
lemma cont_iterate: "cont(iterate(i))" |
99 |
apply (induct_tac i) |
|
100 |
apply simp |
|
101 |
apply simp |
|
102 |
apply (rule cont2cont_CF1L_rev) |
|
103 |
apply (rule allI) |
|
104 |
apply (rule cont2cont_Rep_CFun) |
|
105 |
apply (rule cont_id) |
|
106 |
apply (erule cont2cont_CF1L) |
|
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
107 |
done |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
108 |
|
16005 | 109 |
lemma monofun_iterate: "monofun(iterate(i))" |
110 |
by (rule cont_iterate [THEN cont2mono]) |
|
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
111 |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
112 |
lemma contlub_iterate: "contlub(iterate(i))" |
16005 | 113 |
by (rule cont_iterate [THEN cont2contlub]) |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
114 |
|
15637
d2a06007ebfa
changed comments to text blocks, cleaned up a few proofs
huffman
parents:
15577
diff
changeset
|
115 |
text {* a lemma about continuity of @{term iterate} in its third argument *} |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
116 |
|
16005 | 117 |
lemma cont_iterate2: "cont (iterate n F)" |
118 |
by (induct_tac "n", simp_all) |
|
119 |
||
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
120 |
lemma monofun_iterate2: "monofun(iterate n F)" |
16005 | 121 |
by (rule cont_iterate2 [THEN cont2mono]) |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
122 |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
123 |
lemma contlub_iterate2: "contlub(iterate n F)" |
16005 | 124 |
by (rule cont_iterate2 [THEN cont2contlub]) |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
125 |
|
15637
d2a06007ebfa
changed comments to text blocks, cleaned up a few proofs
huffman
parents:
15577
diff
changeset
|
126 |
text {* monotonicity and continuity of @{term Ifix} *} |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
127 |
|
16005 | 128 |
text {* better access to definitions *} |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
129 |
|
16005 | 130 |
lemma Ifix_def2: "Ifix=(%x. lub(range(%i. iterate i x UU)))" |
131 |
apply (rule ext) |
|
15637
d2a06007ebfa
changed comments to text blocks, cleaned up a few proofs
huffman
parents:
15577
diff
changeset
|
132 |
apply (unfold Ifix_def) |
16005 | 133 |
apply (rule refl) |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
134 |
done |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
135 |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
136 |
lemma cont_Ifix: "cont(Ifix)" |
16005 | 137 |
apply (subst Ifix_def2) |
138 |
apply (subst cont_iterate [THEN cont2cont_CF1L, THEN beta_cfun, symmetric]) |
|
139 |
apply (rule cont_lubcfun) |
|
140 |
apply (rule chainI) |
|
141 |
apply (rule less_cfun2) |
|
142 |
apply (simp add: cont_iterate [THEN cont2cont_CF1L] del: iterate_Suc) |
|
143 |
apply (rule chainE) |
|
144 |
apply (rule chain_iterate) |
|
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
145 |
done |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
146 |
|
16005 | 147 |
lemma monofun_Ifix: "monofun(Ifix)" |
148 |
by (rule cont_Ifix [THEN cont2mono]) |
|
149 |
||
150 |
lemma contlub_Ifix: "contlub(Ifix)" |
|
151 |
by (rule cont_Ifix [THEN cont2contlub]) |
|
152 |
||
15637
d2a06007ebfa
changed comments to text blocks, cleaned up a few proofs
huffman
parents:
15577
diff
changeset
|
153 |
text {* propagate properties of @{term Ifix} to its continuous counterpart *} |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
154 |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
155 |
lemma fix_eq: "fix$F = F$(fix$F)" |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
156 |
apply (unfold fix_def) |
15637
d2a06007ebfa
changed comments to text blocks, cleaned up a few proofs
huffman
parents:
15577
diff
changeset
|
157 |
apply (simp add: cont_Ifix) |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
158 |
apply (rule Ifix_eq) |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
159 |
done |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
160 |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
161 |
lemma fix_least: "F$x = x ==> fix$F << x" |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
162 |
apply (unfold fix_def) |
15637
d2a06007ebfa
changed comments to text blocks, cleaned up a few proofs
huffman
parents:
15577
diff
changeset
|
163 |
apply (simp add: cont_Ifix) |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
164 |
apply (erule Ifix_least) |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
165 |
done |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
166 |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
167 |
lemma fix_eqI: |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
168 |
"[| F$x = x; !z. F$z = z --> x << z |] ==> x = fix$F" |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
169 |
apply (rule antisym_less) |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
170 |
apply (erule allE) |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
171 |
apply (erule mp) |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
172 |
apply (rule fix_eq [symmetric]) |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
173 |
apply (erule fix_least) |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
174 |
done |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
175 |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
176 |
lemma fix_eq2: "f == fix$F ==> f = F$f" |
15637
d2a06007ebfa
changed comments to text blocks, cleaned up a few proofs
huffman
parents:
15577
diff
changeset
|
177 |
by (simp add: fix_eq [symmetric]) |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
178 |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
179 |
lemma fix_eq3: "f == fix$F ==> f$x = F$f$x" |
15637
d2a06007ebfa
changed comments to text blocks, cleaned up a few proofs
huffman
parents:
15577
diff
changeset
|
180 |
by (erule fix_eq2 [THEN cfun_fun_cong]) |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
181 |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
182 |
(* fun fix_tac3 thm i = ((rtac trans i) THEN (rtac (thm RS fix_eq3) i)) *) |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
183 |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
184 |
lemma fix_eq4: "f = fix$F ==> f = F$f" |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
185 |
apply (erule ssubst) |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
186 |
apply (rule fix_eq) |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
187 |
done |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
188 |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
189 |
lemma fix_eq5: "f = fix$F ==> f$x = F$f$x" |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
190 |
apply (rule trans) |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
191 |
apply (erule fix_eq4 [THEN cfun_fun_cong]) |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
192 |
apply (rule refl) |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
193 |
done |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
194 |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
195 |
(* fun fix_tac5 thm i = ((rtac trans i) THEN (rtac (thm RS fix_eq5) i)) *) |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
196 |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
197 |
(* proves the unfolding theorem for function equations f = fix$... *) |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
198 |
(* |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
199 |
fun fix_prover thy fixeq s = prove_goal thy s (fn prems => [ |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
200 |
(rtac trans 1), |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
201 |
(rtac (fixeq RS fix_eq4) 1), |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
202 |
(rtac trans 1), |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
203 |
(rtac beta_cfun 1), |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
204 |
(Simp_tac 1) |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
205 |
]) |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
206 |
*) |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
207 |
(* proves the unfolding theorem for function definitions f == fix$... *) |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
208 |
(* |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
209 |
fun fix_prover2 thy fixdef s = prove_goal thy s (fn prems => [ |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
210 |
(rtac trans 1), |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
211 |
(rtac (fix_eq2) 1), |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
212 |
(rtac fixdef 1), |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
213 |
(rtac beta_cfun 1), |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
214 |
(Simp_tac 1) |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
215 |
]) |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
216 |
*) |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
217 |
(* proves an application case for a function from its unfolding thm *) |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
218 |
(* |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
219 |
fun case_prover thy unfold s = prove_goal thy s (fn prems => [ |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
220 |
(cut_facts_tac prems 1), |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
221 |
(rtac trans 1), |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
222 |
(stac unfold 1), |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
223 |
Auto_tac |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
224 |
]) |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
225 |
*) |
15637
d2a06007ebfa
changed comments to text blocks, cleaned up a few proofs
huffman
parents:
15577
diff
changeset
|
226 |
text {* direct connection between @{term fix} and iteration without @{term Ifix} *} |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
227 |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
228 |
lemma fix_def2: "fix$F = lub(range(%i. iterate i F UU))" |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
229 |
apply (unfold fix_def) |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
230 |
apply (fold Ifix_def) |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
231 |
apply (simp (no_asm_simp) add: cont_Ifix) |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
232 |
done |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
233 |
|
16005 | 234 |
subsection {* Admissibility and fixed point induction *} |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
235 |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
236 |
lemma admw_def2: "admw(P) = (!F.(!n. P(iterate n F UU)) --> |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
237 |
P (lub(range(%i. iterate i F UU))))" |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
238 |
apply (unfold admw_def) |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
239 |
apply (rule refl) |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
240 |
done |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
241 |
|
15637
d2a06007ebfa
changed comments to text blocks, cleaned up a few proofs
huffman
parents:
15577
diff
changeset
|
242 |
text {* an admissible formula is also weak admissible *} |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
243 |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
244 |
lemma adm_impl_admw: "adm(P)==>admw(P)" |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
245 |
apply (unfold admw_def) |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
246 |
apply (intro strip) |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
247 |
apply (erule admD) |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
248 |
apply (rule chain_iterate) |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
249 |
apply assumption |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
250 |
done |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
251 |
|
16079
757e1c4a8081
moved adm_chfindom from Adm.thy to Fix.thy, to remove dependence on Cfun
huffman
parents:
16070
diff
changeset
|
252 |
text {* some lemmata for functions with flat/chfin domain/range types *} |
757e1c4a8081
moved adm_chfindom from Adm.thy to Fix.thy, to remove dependence on Cfun
huffman
parents:
16070
diff
changeset
|
253 |
|
757e1c4a8081
moved adm_chfindom from Adm.thy to Fix.thy, to remove dependence on Cfun
huffman
parents:
16070
diff
changeset
|
254 |
lemma adm_chfindom: "adm (%(u::'a::cpo->'b::chfin). P(u$s))" |
757e1c4a8081
moved adm_chfindom from Adm.thy to Fix.thy, to remove dependence on Cfun
huffman
parents:
16070
diff
changeset
|
255 |
apply (unfold adm_def) |
757e1c4a8081
moved adm_chfindom from Adm.thy to Fix.thy, to remove dependence on Cfun
huffman
parents:
16070
diff
changeset
|
256 |
apply (intro strip) |
757e1c4a8081
moved adm_chfindom from Adm.thy to Fix.thy, to remove dependence on Cfun
huffman
parents:
16070
diff
changeset
|
257 |
apply (drule chfin_Rep_CFunR) |
757e1c4a8081
moved adm_chfindom from Adm.thy to Fix.thy, to remove dependence on Cfun
huffman
parents:
16070
diff
changeset
|
258 |
apply (erule_tac x = "s" in allE) |
757e1c4a8081
moved adm_chfindom from Adm.thy to Fix.thy, to remove dependence on Cfun
huffman
parents:
16070
diff
changeset
|
259 |
apply clarsimp |
757e1c4a8081
moved adm_chfindom from Adm.thy to Fix.thy, to remove dependence on Cfun
huffman
parents:
16070
diff
changeset
|
260 |
done |
757e1c4a8081
moved adm_chfindom from Adm.thy to Fix.thy, to remove dependence on Cfun
huffman
parents:
16070
diff
changeset
|
261 |
|
757e1c4a8081
moved adm_chfindom from Adm.thy to Fix.thy, to remove dependence on Cfun
huffman
parents:
16070
diff
changeset
|
262 |
(* adm_flat not needed any more, since it is a special case of adm_chfindom *) |
757e1c4a8081
moved adm_chfindom from Adm.thy to Fix.thy, to remove dependence on Cfun
huffman
parents:
16070
diff
changeset
|
263 |
|
15637
d2a06007ebfa
changed comments to text blocks, cleaned up a few proofs
huffman
parents:
15577
diff
changeset
|
264 |
text {* fixed point induction *} |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
265 |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
266 |
lemma fix_ind: |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
267 |
"[| adm(P); P(UU); !!x. P(x) ==> P(F$x)|] ==> P(fix$F)" |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
268 |
apply (subst fix_def2) |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
269 |
apply (erule admD) |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
270 |
apply (rule chain_iterate) |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
271 |
apply (rule allI) |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
272 |
apply (induct_tac "i") |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
273 |
apply simp |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
274 |
apply simp |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
275 |
done |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
276 |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
277 |
lemma def_fix_ind: "[| f == fix$F; adm(P); |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
278 |
P(UU); !!x. P(x) ==> P(F$x)|] ==> P f" |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
279 |
apply simp |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
280 |
apply (erule fix_ind) |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
281 |
apply assumption |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
282 |
apply fast |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
283 |
done |
15637
d2a06007ebfa
changed comments to text blocks, cleaned up a few proofs
huffman
parents:
15577
diff
changeset
|
284 |
|
d2a06007ebfa
changed comments to text blocks, cleaned up a few proofs
huffman
parents:
15577
diff
changeset
|
285 |
text {* computational induction for weak admissible formulae *} |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
286 |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
287 |
lemma wfix_ind: "[| admw(P); !n. P(iterate n F UU)|] ==> P(fix$F)" |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
288 |
apply (subst fix_def2) |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
289 |
apply (rule admw_def2 [THEN iffD1, THEN spec, THEN mp]) |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
290 |
apply assumption |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
291 |
apply (rule allI) |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
292 |
apply (erule spec) |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
293 |
done |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
294 |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
295 |
lemma def_wfix_ind: "[| f == fix$F; admw(P); |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
296 |
!n. P(iterate n F UU) |] ==> P f" |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
297 |
apply simp |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
298 |
apply (erule wfix_ind) |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
299 |
apply assumption |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
300 |
done |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
301 |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
302 |
end |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
303 |