author | huffman |
Wed, 14 Jan 2009 17:11:29 -0800 | |
changeset 29530 | 9905b660612b |
parent 29138 | 661a8db7e647 |
child 29532 | 59bee7985149 |
permissions | -rw-r--r-- |
15600 | 1 |
(* Title: HOLCF/Cont.thy |
1479 | 2 |
Author: Franz Regensburger |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
3 |
*) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
4 |
|
15577 | 5 |
header {* Continuity and monotonicity *} |
6 |
||
7 |
theory Cont |
|
25786 | 8 |
imports Pcpo |
15577 | 9 |
begin |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
10 |
|
15588
14e3228f18cc
arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
11 |
text {* |
14e3228f18cc
arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
12 |
Now we change the default class! Form now on all untyped type variables are |
3323
194ae2e0c193
eliminated the constant less by the introduction of the axclass sq_ord
slotosch
parents:
2838
diff
changeset
|
13 |
of default class po |
15588
14e3228f18cc
arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
14 |
*} |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
15 |
|
15565 | 16 |
defaultsort po |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
17 |
|
16624
645b9560f3fd
cleaned up; reorganized and added section headings
huffman
parents:
16564
diff
changeset
|
18 |
subsection {* Definitions *} |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
19 |
|
25131
2c8caac48ade
modernized specifications ('definition', 'abbreviation', 'notation');
wenzelm
parents:
18092
diff
changeset
|
20 |
definition |
2c8caac48ade
modernized specifications ('definition', 'abbreviation', 'notation');
wenzelm
parents:
18092
diff
changeset
|
21 |
monofun :: "('a \<Rightarrow> 'b) \<Rightarrow> bool" -- "monotonicity" where |
2c8caac48ade
modernized specifications ('definition', 'abbreviation', 'notation');
wenzelm
parents:
18092
diff
changeset
|
22 |
"monofun f = (\<forall>x y. x \<sqsubseteq> y \<longrightarrow> f x \<sqsubseteq> f y)" |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
23 |
|
25131
2c8caac48ade
modernized specifications ('definition', 'abbreviation', 'notation');
wenzelm
parents:
18092
diff
changeset
|
24 |
definition |
2c8caac48ade
modernized specifications ('definition', 'abbreviation', 'notation');
wenzelm
parents:
18092
diff
changeset
|
25 |
contlub :: "('a::cpo \<Rightarrow> 'b::cpo) \<Rightarrow> bool" -- "first cont. def" where |
2c8caac48ade
modernized specifications ('definition', 'abbreviation', 'notation');
wenzelm
parents:
18092
diff
changeset
|
26 |
"contlub f = (\<forall>Y. chain Y \<longrightarrow> f (\<Squnion>i. Y i) = (\<Squnion>i. f (Y i)))" |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
27 |
|
25131
2c8caac48ade
modernized specifications ('definition', 'abbreviation', 'notation');
wenzelm
parents:
18092
diff
changeset
|
28 |
definition |
2c8caac48ade
modernized specifications ('definition', 'abbreviation', 'notation');
wenzelm
parents:
18092
diff
changeset
|
29 |
cont :: "('a::cpo \<Rightarrow> 'b::cpo) \<Rightarrow> bool" -- "secnd cont. def" where |
2c8caac48ade
modernized specifications ('definition', 'abbreviation', 'notation');
wenzelm
parents:
18092
diff
changeset
|
30 |
"cont f = (\<forall>Y. chain Y \<longrightarrow> range (\<lambda>i. f (Y i)) <<| f (\<Squnion>i. Y i))" |
15565 | 31 |
|
32 |
lemma contlubI: |
|
16204
5dd79d3f0105
renamed theorems monofun, contlub, cont to monofun_def, etc.; changed intro/elim rules for these predicates into more useful rule_format; removed all MF2 lemmas (Pcpo.thy has more general versions now); cleaned up many proofs.
huffman
parents:
16096
diff
changeset
|
33 |
"\<lbrakk>\<And>Y. chain Y \<Longrightarrow> f (\<Squnion>i. Y i) = (\<Squnion>i. f (Y i))\<rbrakk> \<Longrightarrow> contlub f" |
5dd79d3f0105
renamed theorems monofun, contlub, cont to monofun_def, etc.; changed intro/elim rules for these predicates into more useful rule_format; removed all MF2 lemmas (Pcpo.thy has more general versions now); cleaned up many proofs.
huffman
parents:
16096
diff
changeset
|
34 |
by (simp add: contlub_def) |
15565 | 35 |
|
36 |
lemma contlubE: |
|
16204
5dd79d3f0105
renamed theorems monofun, contlub, cont to monofun_def, etc.; changed intro/elim rules for these predicates into more useful rule_format; removed all MF2 lemmas (Pcpo.thy has more general versions now); cleaned up many proofs.
huffman
parents:
16096
diff
changeset
|
37 |
"\<lbrakk>contlub f; chain Y\<rbrakk> \<Longrightarrow> f (\<Squnion>i. Y i) = (\<Squnion>i. f (Y i))" |
5dd79d3f0105
renamed theorems monofun, contlub, cont to monofun_def, etc.; changed intro/elim rules for these predicates into more useful rule_format; removed all MF2 lemmas (Pcpo.thy has more general versions now); cleaned up many proofs.
huffman
parents:
16096
diff
changeset
|
38 |
by (simp add: contlub_def) |
15565 | 39 |
|
16204
5dd79d3f0105
renamed theorems monofun, contlub, cont to monofun_def, etc.; changed intro/elim rules for these predicates into more useful rule_format; removed all MF2 lemmas (Pcpo.thy has more general versions now); cleaned up many proofs.
huffman
parents:
16096
diff
changeset
|
40 |
lemma contI: |
5dd79d3f0105
renamed theorems monofun, contlub, cont to monofun_def, etc.; changed intro/elim rules for these predicates into more useful rule_format; removed all MF2 lemmas (Pcpo.thy has more general versions now); cleaned up many proofs.
huffman
parents:
16096
diff
changeset
|
41 |
"\<lbrakk>\<And>Y. chain Y \<Longrightarrow> range (\<lambda>i. f (Y i)) <<| f (\<Squnion>i. Y i)\<rbrakk> \<Longrightarrow> cont f" |
5dd79d3f0105
renamed theorems monofun, contlub, cont to monofun_def, etc.; changed intro/elim rules for these predicates into more useful rule_format; removed all MF2 lemmas (Pcpo.thy has more general versions now); cleaned up many proofs.
huffman
parents:
16096
diff
changeset
|
42 |
by (simp add: cont_def) |
15565 | 43 |
|
16204
5dd79d3f0105
renamed theorems monofun, contlub, cont to monofun_def, etc.; changed intro/elim rules for these predicates into more useful rule_format; removed all MF2 lemmas (Pcpo.thy has more general versions now); cleaned up many proofs.
huffman
parents:
16096
diff
changeset
|
44 |
lemma contE: |
5dd79d3f0105
renamed theorems monofun, contlub, cont to monofun_def, etc.; changed intro/elim rules for these predicates into more useful rule_format; removed all MF2 lemmas (Pcpo.thy has more general versions now); cleaned up many proofs.
huffman
parents:
16096
diff
changeset
|
45 |
"\<lbrakk>cont f; chain Y\<rbrakk> \<Longrightarrow> range (\<lambda>i. f (Y i)) <<| f (\<Squnion>i. Y i)" |
5dd79d3f0105
renamed theorems monofun, contlub, cont to monofun_def, etc.; changed intro/elim rules for these predicates into more useful rule_format; removed all MF2 lemmas (Pcpo.thy has more general versions now); cleaned up many proofs.
huffman
parents:
16096
diff
changeset
|
46 |
by (simp add: cont_def) |
15565 | 47 |
|
48 |
lemma monofunI: |
|
16204
5dd79d3f0105
renamed theorems monofun, contlub, cont to monofun_def, etc.; changed intro/elim rules for these predicates into more useful rule_format; removed all MF2 lemmas (Pcpo.thy has more general versions now); cleaned up many proofs.
huffman
parents:
16096
diff
changeset
|
49 |
"\<lbrakk>\<And>x y. x \<sqsubseteq> y \<Longrightarrow> f x \<sqsubseteq> f y\<rbrakk> \<Longrightarrow> monofun f" |
5dd79d3f0105
renamed theorems monofun, contlub, cont to monofun_def, etc.; changed intro/elim rules for these predicates into more useful rule_format; removed all MF2 lemmas (Pcpo.thy has more general versions now); cleaned up many proofs.
huffman
parents:
16096
diff
changeset
|
50 |
by (simp add: monofun_def) |
15565 | 51 |
|
52 |
lemma monofunE: |
|
16204
5dd79d3f0105
renamed theorems monofun, contlub, cont to monofun_def, etc.; changed intro/elim rules for these predicates into more useful rule_format; removed all MF2 lemmas (Pcpo.thy has more general versions now); cleaned up many proofs.
huffman
parents:
16096
diff
changeset
|
53 |
"\<lbrakk>monofun f; x \<sqsubseteq> y\<rbrakk> \<Longrightarrow> f x \<sqsubseteq> f y" |
5dd79d3f0105
renamed theorems monofun, contlub, cont to monofun_def, etc.; changed intro/elim rules for these predicates into more useful rule_format; removed all MF2 lemmas (Pcpo.thy has more general versions now); cleaned up many proofs.
huffman
parents:
16096
diff
changeset
|
54 |
by (simp add: monofun_def) |
15565 | 55 |
|
16624
645b9560f3fd
cleaned up; reorganized and added section headings
huffman
parents:
16564
diff
changeset
|
56 |
|
645b9560f3fd
cleaned up; reorganized and added section headings
huffman
parents:
16564
diff
changeset
|
57 |
subsection {* @{prop "monofun f \<and> contlub f \<equiv> cont f"} *} |
645b9560f3fd
cleaned up; reorganized and added section headings
huffman
parents:
16564
diff
changeset
|
58 |
|
15588
14e3228f18cc
arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
59 |
text {* monotone functions map chains to chains *} |
15565 | 60 |
|
16204
5dd79d3f0105
renamed theorems monofun, contlub, cont to monofun_def, etc.; changed intro/elim rules for these predicates into more useful rule_format; removed all MF2 lemmas (Pcpo.thy has more general versions now); cleaned up many proofs.
huffman
parents:
16096
diff
changeset
|
61 |
lemma ch2ch_monofun: "\<lbrakk>monofun f; chain Y\<rbrakk> \<Longrightarrow> chain (\<lambda>i. f (Y i))" |
15565 | 62 |
apply (rule chainI) |
16204
5dd79d3f0105
renamed theorems monofun, contlub, cont to monofun_def, etc.; changed intro/elim rules for these predicates into more useful rule_format; removed all MF2 lemmas (Pcpo.thy has more general versions now); cleaned up many proofs.
huffman
parents:
16096
diff
changeset
|
63 |
apply (erule monofunE) |
15565 | 64 |
apply (erule chainE) |
65 |
done |
|
66 |
||
15588
14e3228f18cc
arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
67 |
text {* monotone functions map upper bound to upper bounds *} |
15565 | 68 |
|
69 |
lemma ub2ub_monofun: |
|
16204
5dd79d3f0105
renamed theorems monofun, contlub, cont to monofun_def, etc.; changed intro/elim rules for these predicates into more useful rule_format; removed all MF2 lemmas (Pcpo.thy has more general versions now); cleaned up many proofs.
huffman
parents:
16096
diff
changeset
|
70 |
"\<lbrakk>monofun f; range Y <| u\<rbrakk> \<Longrightarrow> range (\<lambda>i. f (Y i)) <| f u" |
15565 | 71 |
apply (rule ub_rangeI) |
16204
5dd79d3f0105
renamed theorems monofun, contlub, cont to monofun_def, etc.; changed intro/elim rules for these predicates into more useful rule_format; removed all MF2 lemmas (Pcpo.thy has more general versions now); cleaned up many proofs.
huffman
parents:
16096
diff
changeset
|
72 |
apply (erule monofunE) |
15565 | 73 |
apply (erule ub_rangeD) |
74 |
done |
|
75 |
||
16624
645b9560f3fd
cleaned up; reorganized and added section headings
huffman
parents:
16564
diff
changeset
|
76 |
text {* left to right: @{prop "monofun f \<and> contlub f \<Longrightarrow> cont f"} *} |
15565 | 77 |
|
16204
5dd79d3f0105
renamed theorems monofun, contlub, cont to monofun_def, etc.; changed intro/elim rules for these predicates into more useful rule_format; removed all MF2 lemmas (Pcpo.thy has more general versions now); cleaned up many proofs.
huffman
parents:
16096
diff
changeset
|
78 |
lemma monocontlub2cont: "\<lbrakk>monofun f; contlub f\<rbrakk> \<Longrightarrow> cont f" |
5dd79d3f0105
renamed theorems monofun, contlub, cont to monofun_def, etc.; changed intro/elim rules for these predicates into more useful rule_format; removed all MF2 lemmas (Pcpo.thy has more general versions now); cleaned up many proofs.
huffman
parents:
16096
diff
changeset
|
79 |
apply (rule contI) |
15565 | 80 |
apply (rule thelubE) |
18088 | 81 |
apply (erule (1) ch2ch_monofun) |
82 |
apply (erule (1) contlubE [symmetric]) |
|
15565 | 83 |
done |
84 |
||
15588
14e3228f18cc
arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
85 |
text {* first a lemma about binary chains *} |
15565 | 86 |
|
16204
5dd79d3f0105
renamed theorems monofun, contlub, cont to monofun_def, etc.; changed intro/elim rules for these predicates into more useful rule_format; removed all MF2 lemmas (Pcpo.thy has more general versions now); cleaned up many proofs.
huffman
parents:
16096
diff
changeset
|
87 |
lemma binchain_cont: |
5dd79d3f0105
renamed theorems monofun, contlub, cont to monofun_def, etc.; changed intro/elim rules for these predicates into more useful rule_format; removed all MF2 lemmas (Pcpo.thy has more general versions now); cleaned up many proofs.
huffman
parents:
16096
diff
changeset
|
88 |
"\<lbrakk>cont f; x \<sqsubseteq> y\<rbrakk> \<Longrightarrow> range (\<lambda>i::nat. f (if i = 0 then x else y)) <<| f y" |
5dd79d3f0105
renamed theorems monofun, contlub, cont to monofun_def, etc.; changed intro/elim rules for these predicates into more useful rule_format; removed all MF2 lemmas (Pcpo.thy has more general versions now); cleaned up many proofs.
huffman
parents:
16096
diff
changeset
|
89 |
apply (subgoal_tac "f (\<Squnion>i::nat. if i = 0 then x else y) = f y") |
5dd79d3f0105
renamed theorems monofun, contlub, cont to monofun_def, etc.; changed intro/elim rules for these predicates into more useful rule_format; removed all MF2 lemmas (Pcpo.thy has more general versions now); cleaned up many proofs.
huffman
parents:
16096
diff
changeset
|
90 |
apply (erule subst) |
5dd79d3f0105
renamed theorems monofun, contlub, cont to monofun_def, etc.; changed intro/elim rules for these predicates into more useful rule_format; removed all MF2 lemmas (Pcpo.thy has more general versions now); cleaned up many proofs.
huffman
parents:
16096
diff
changeset
|
91 |
apply (erule contE) |
15565 | 92 |
apply (erule bin_chain) |
16204
5dd79d3f0105
renamed theorems monofun, contlub, cont to monofun_def, etc.; changed intro/elim rules for these predicates into more useful rule_format; removed all MF2 lemmas (Pcpo.thy has more general versions now); cleaned up many proofs.
huffman
parents:
16096
diff
changeset
|
93 |
apply (rule_tac f=f in arg_cong) |
15565 | 94 |
apply (erule lub_bin_chain [THEN thelubI]) |
95 |
done |
|
96 |
||
16204
5dd79d3f0105
renamed theorems monofun, contlub, cont to monofun_def, etc.; changed intro/elim rules for these predicates into more useful rule_format; removed all MF2 lemmas (Pcpo.thy has more general versions now); cleaned up many proofs.
huffman
parents:
16096
diff
changeset
|
97 |
text {* right to left: @{prop "cont f \<Longrightarrow> monofun f \<and> contlub f"} *} |
5dd79d3f0105
renamed theorems monofun, contlub, cont to monofun_def, etc.; changed intro/elim rules for these predicates into more useful rule_format; removed all MF2 lemmas (Pcpo.thy has more general versions now); cleaned up many proofs.
huffman
parents:
16096
diff
changeset
|
98 |
text {* part1: @{prop "cont f \<Longrightarrow> monofun f"} *} |
15565 | 99 |
|
16204
5dd79d3f0105
renamed theorems monofun, contlub, cont to monofun_def, etc.; changed intro/elim rules for these predicates into more useful rule_format; removed all MF2 lemmas (Pcpo.thy has more general versions now); cleaned up many proofs.
huffman
parents:
16096
diff
changeset
|
100 |
lemma cont2mono: "cont f \<Longrightarrow> monofun f" |
5dd79d3f0105
renamed theorems monofun, contlub, cont to monofun_def, etc.; changed intro/elim rules for these predicates into more useful rule_format; removed all MF2 lemmas (Pcpo.thy has more general versions now); cleaned up many proofs.
huffman
parents:
16096
diff
changeset
|
101 |
apply (rule monofunI) |
18088 | 102 |
apply (drule (1) binchain_cont) |
16204
5dd79d3f0105
renamed theorems monofun, contlub, cont to monofun_def, etc.; changed intro/elim rules for these predicates into more useful rule_format; removed all MF2 lemmas (Pcpo.thy has more general versions now); cleaned up many proofs.
huffman
parents:
16096
diff
changeset
|
103 |
apply (drule_tac i=0 in is_ub_lub) |
5dd79d3f0105
renamed theorems monofun, contlub, cont to monofun_def, etc.; changed intro/elim rules for these predicates into more useful rule_format; removed all MF2 lemmas (Pcpo.thy has more general versions now); cleaned up many proofs.
huffman
parents:
16096
diff
changeset
|
104 |
apply simp |
15565 | 105 |
done |
106 |
||
16737 | 107 |
lemmas ch2ch_cont = cont2mono [THEN ch2ch_monofun] |
108 |
||
16204
5dd79d3f0105
renamed theorems monofun, contlub, cont to monofun_def, etc.; changed intro/elim rules for these predicates into more useful rule_format; removed all MF2 lemmas (Pcpo.thy has more general versions now); cleaned up many proofs.
huffman
parents:
16096
diff
changeset
|
109 |
text {* right to left: @{prop "cont f \<Longrightarrow> monofun f \<and> contlub f"} *} |
5dd79d3f0105
renamed theorems monofun, contlub, cont to monofun_def, etc.; changed intro/elim rules for these predicates into more useful rule_format; removed all MF2 lemmas (Pcpo.thy has more general versions now); cleaned up many proofs.
huffman
parents:
16096
diff
changeset
|
110 |
text {* part2: @{prop "cont f \<Longrightarrow> contlub f"} *} |
15565 | 111 |
|
16624
645b9560f3fd
cleaned up; reorganized and added section headings
huffman
parents:
16564
diff
changeset
|
112 |
lemma cont2contlub: "cont f \<Longrightarrow> contlub f" |
16204
5dd79d3f0105
renamed theorems monofun, contlub, cont to monofun_def, etc.; changed intro/elim rules for these predicates into more useful rule_format; removed all MF2 lemmas (Pcpo.thy has more general versions now); cleaned up many proofs.
huffman
parents:
16096
diff
changeset
|
113 |
apply (rule contlubI) |
15565 | 114 |
apply (rule thelubI [symmetric]) |
18088 | 115 |
apply (erule (1) contE) |
15565 | 116 |
done |
117 |
||
16737 | 118 |
lemmas cont2contlubE = cont2contlub [THEN contlubE] |
119 |
||
25896 | 120 |
lemma contI2: |
121 |
assumes mono: "monofun f" |
|
122 |
assumes less: "\<And>Y. \<lbrakk>chain Y; chain (\<lambda>i. f (Y i))\<rbrakk> |
|
27413 | 123 |
\<Longrightarrow> f (\<Squnion>i. Y i) \<sqsubseteq> (\<Squnion>i. f (Y i))" |
25896 | 124 |
shows "cont f" |
125 |
apply (rule monocontlub2cont) |
|
126 |
apply (rule mono) |
|
127 |
apply (rule contlubI) |
|
128 |
apply (rule antisym_less) |
|
129 |
apply (rule less, assumption) |
|
130 |
apply (erule ch2ch_monofun [OF mono]) |
|
131 |
apply (rule is_lub_thelub) |
|
132 |
apply (erule ch2ch_monofun [OF mono]) |
|
133 |
apply (rule ub2ub_monofun [OF mono]) |
|
134 |
apply (rule is_lubD1) |
|
26027 | 135 |
apply (erule cpo_lubI) |
25896 | 136 |
done |
137 |
||
29530
9905b660612b
change to simpler, more extensible continuity simproc
huffman
parents:
29138
diff
changeset
|
138 |
subsection {* Continuity simproc *} |
9905b660612b
change to simpler, more extensible continuity simproc
huffman
parents:
29138
diff
changeset
|
139 |
|
9905b660612b
change to simpler, more extensible continuity simproc
huffman
parents:
29138
diff
changeset
|
140 |
ML {* |
9905b660612b
change to simpler, more extensible continuity simproc
huffman
parents:
29138
diff
changeset
|
141 |
structure Cont2ContData = NamedThmsFun |
9905b660612b
change to simpler, more extensible continuity simproc
huffman
parents:
29138
diff
changeset
|
142 |
( val name = "cont2cont" val description = "continuity intro rule" ) |
9905b660612b
change to simpler, more extensible continuity simproc
huffman
parents:
29138
diff
changeset
|
143 |
*} |
9905b660612b
change to simpler, more extensible continuity simproc
huffman
parents:
29138
diff
changeset
|
144 |
|
9905b660612b
change to simpler, more extensible continuity simproc
huffman
parents:
29138
diff
changeset
|
145 |
setup {* Cont2ContData.setup *} |
9905b660612b
change to simpler, more extensible continuity simproc
huffman
parents:
29138
diff
changeset
|
146 |
|
9905b660612b
change to simpler, more extensible continuity simproc
huffman
parents:
29138
diff
changeset
|
147 |
text {* |
9905b660612b
change to simpler, more extensible continuity simproc
huffman
parents:
29138
diff
changeset
|
148 |
Given the term @{term "cont f"}, the procedure tries to construct the |
9905b660612b
change to simpler, more extensible continuity simproc
huffman
parents:
29138
diff
changeset
|
149 |
theorem @{term "cont f == True"}. If this theorem cannot be completely |
9905b660612b
change to simpler, more extensible continuity simproc
huffman
parents:
29138
diff
changeset
|
150 |
solved by the introduction rules, then the procedure returns a |
9905b660612b
change to simpler, more extensible continuity simproc
huffman
parents:
29138
diff
changeset
|
151 |
conditional rewrite rule with the unsolved subgoals as premises. |
9905b660612b
change to simpler, more extensible continuity simproc
huffman
parents:
29138
diff
changeset
|
152 |
*} |
9905b660612b
change to simpler, more extensible continuity simproc
huffman
parents:
29138
diff
changeset
|
153 |
|
9905b660612b
change to simpler, more extensible continuity simproc
huffman
parents:
29138
diff
changeset
|
154 |
setup {* |
9905b660612b
change to simpler, more extensible continuity simproc
huffman
parents:
29138
diff
changeset
|
155 |
let |
9905b660612b
change to simpler, more extensible continuity simproc
huffman
parents:
29138
diff
changeset
|
156 |
fun solve_cont thy ss t = |
9905b660612b
change to simpler, more extensible continuity simproc
huffman
parents:
29138
diff
changeset
|
157 |
let |
9905b660612b
change to simpler, more extensible continuity simproc
huffman
parents:
29138
diff
changeset
|
158 |
val tr = instantiate' [] [SOME (cterm_of thy t)] Eq_TrueI; |
9905b660612b
change to simpler, more extensible continuity simproc
huffman
parents:
29138
diff
changeset
|
159 |
val rules = Cont2ContData.get (Simplifier.the_context ss); |
9905b660612b
change to simpler, more extensible continuity simproc
huffman
parents:
29138
diff
changeset
|
160 |
val tac = REPEAT_ALL_NEW (resolve_tac rules); |
9905b660612b
change to simpler, more extensible continuity simproc
huffman
parents:
29138
diff
changeset
|
161 |
in Option.map fst (Seq.pull (tac 1 tr)) end |
9905b660612b
change to simpler, more extensible continuity simproc
huffman
parents:
29138
diff
changeset
|
162 |
|
9905b660612b
change to simpler, more extensible continuity simproc
huffman
parents:
29138
diff
changeset
|
163 |
val proc = |
9905b660612b
change to simpler, more extensible continuity simproc
huffman
parents:
29138
diff
changeset
|
164 |
Simplifier.simproc @{theory} "cont_proc" ["cont f"] solve_cont; |
9905b660612b
change to simpler, more extensible continuity simproc
huffman
parents:
29138
diff
changeset
|
165 |
in |
9905b660612b
change to simpler, more extensible continuity simproc
huffman
parents:
29138
diff
changeset
|
166 |
Simplifier.map_simpset (fn ss => ss addsimprocs [proc]) |
9905b660612b
change to simpler, more extensible continuity simproc
huffman
parents:
29138
diff
changeset
|
167 |
end |
9905b660612b
change to simpler, more extensible continuity simproc
huffman
parents:
29138
diff
changeset
|
168 |
*} |
9905b660612b
change to simpler, more extensible continuity simproc
huffman
parents:
29138
diff
changeset
|
169 |
|
16624
645b9560f3fd
cleaned up; reorganized and added section headings
huffman
parents:
16564
diff
changeset
|
170 |
subsection {* Continuity of basic functions *} |
645b9560f3fd
cleaned up; reorganized and added section headings
huffman
parents:
16564
diff
changeset
|
171 |
|
645b9560f3fd
cleaned up; reorganized and added section headings
huffman
parents:
16564
diff
changeset
|
172 |
text {* The identity function is continuous *} |
15565 | 173 |
|
29530
9905b660612b
change to simpler, more extensible continuity simproc
huffman
parents:
29138
diff
changeset
|
174 |
lemma cont_id [cont2cont]: "cont (\<lambda>x. x)" |
16624
645b9560f3fd
cleaned up; reorganized and added section headings
huffman
parents:
16564
diff
changeset
|
175 |
apply (rule contI) |
26027 | 176 |
apply (erule cpo_lubI) |
15565 | 177 |
done |
178 |
||
16624
645b9560f3fd
cleaned up; reorganized and added section headings
huffman
parents:
16564
diff
changeset
|
179 |
text {* constant functions are continuous *} |
645b9560f3fd
cleaned up; reorganized and added section headings
huffman
parents:
16564
diff
changeset
|
180 |
|
29530
9905b660612b
change to simpler, more extensible continuity simproc
huffman
parents:
29138
diff
changeset
|
181 |
lemma cont_const [cont2cont]: "cont (\<lambda>x. c)" |
16624
645b9560f3fd
cleaned up; reorganized and added section headings
huffman
parents:
16564
diff
changeset
|
182 |
apply (rule contI) |
645b9560f3fd
cleaned up; reorganized and added section headings
huffman
parents:
16564
diff
changeset
|
183 |
apply (rule lub_const) |
645b9560f3fd
cleaned up; reorganized and added section headings
huffman
parents:
16564
diff
changeset
|
184 |
done |
15565 | 185 |
|
16624
645b9560f3fd
cleaned up; reorganized and added section headings
huffman
parents:
16564
diff
changeset
|
186 |
text {* if-then-else is continuous *} |
645b9560f3fd
cleaned up; reorganized and added section headings
huffman
parents:
16564
diff
changeset
|
187 |
|
26452
ed657432b8b9
declare cont_lemmas_ext as simp rules individually
huffman
parents:
26027
diff
changeset
|
188 |
lemma cont_if [simp]: |
ed657432b8b9
declare cont_lemmas_ext as simp rules individually
huffman
parents:
26027
diff
changeset
|
189 |
"\<lbrakk>cont f; cont g\<rbrakk> \<Longrightarrow> cont (\<lambda>x. if b then f x else g x)" |
16624
645b9560f3fd
cleaned up; reorganized and added section headings
huffman
parents:
16564
diff
changeset
|
190 |
by (induct b) simp_all |
645b9560f3fd
cleaned up; reorganized and added section headings
huffman
parents:
16564
diff
changeset
|
191 |
|
645b9560f3fd
cleaned up; reorganized and added section headings
huffman
parents:
16564
diff
changeset
|
192 |
subsection {* Finite chains and flat pcpos *} |
15565 | 193 |
|
16624
645b9560f3fd
cleaned up; reorganized and added section headings
huffman
parents:
16564
diff
changeset
|
194 |
text {* monotone functions map finite chains to finite chains *} |
15565 | 195 |
|
16624
645b9560f3fd
cleaned up; reorganized and added section headings
huffman
parents:
16564
diff
changeset
|
196 |
lemma monofun_finch2finch: |
645b9560f3fd
cleaned up; reorganized and added section headings
huffman
parents:
16564
diff
changeset
|
197 |
"\<lbrakk>monofun f; finite_chain Y\<rbrakk> \<Longrightarrow> finite_chain (\<lambda>n. f (Y n))" |
645b9560f3fd
cleaned up; reorganized and added section headings
huffman
parents:
16564
diff
changeset
|
198 |
apply (unfold finite_chain_def) |
645b9560f3fd
cleaned up; reorganized and added section headings
huffman
parents:
16564
diff
changeset
|
199 |
apply (simp add: ch2ch_monofun) |
645b9560f3fd
cleaned up; reorganized and added section headings
huffman
parents:
16564
diff
changeset
|
200 |
apply (force simp add: max_in_chain_def) |
15565 | 201 |
done |
202 |
||
16624
645b9560f3fd
cleaned up; reorganized and added section headings
huffman
parents:
16564
diff
changeset
|
203 |
text {* The same holds for continuous functions *} |
15565 | 204 |
|
16624
645b9560f3fd
cleaned up; reorganized and added section headings
huffman
parents:
16564
diff
changeset
|
205 |
lemma cont_finch2finch: |
645b9560f3fd
cleaned up; reorganized and added section headings
huffman
parents:
16564
diff
changeset
|
206 |
"\<lbrakk>cont f; finite_chain Y\<rbrakk> \<Longrightarrow> finite_chain (\<lambda>n. f (Y n))" |
645b9560f3fd
cleaned up; reorganized and added section headings
huffman
parents:
16564
diff
changeset
|
207 |
by (rule cont2mono [THEN monofun_finch2finch]) |
15565 | 208 |
|
25825 | 209 |
lemma chfindom_monofun2cont: "monofun f \<Longrightarrow> cont (f::'a::chfin \<Rightarrow> 'b::cpo)" |
15565 | 210 |
apply (rule monocontlub2cont) |
211 |
apply assumption |
|
16204
5dd79d3f0105
renamed theorems monofun, contlub, cont to monofun_def, etc.; changed intro/elim rules for these predicates into more useful rule_format; removed all MF2 lemmas (Pcpo.thy has more general versions now); cleaned up many proofs.
huffman
parents:
16096
diff
changeset
|
212 |
apply (rule contlubI) |
15565 | 213 |
apply (frule chfin2finch) |
16204
5dd79d3f0105
renamed theorems monofun, contlub, cont to monofun_def, etc.; changed intro/elim rules for these predicates into more useful rule_format; removed all MF2 lemmas (Pcpo.thy has more general versions now); cleaned up many proofs.
huffman
parents:
16096
diff
changeset
|
214 |
apply (clarsimp simp add: finite_chain_def) |
5dd79d3f0105
renamed theorems monofun, contlub, cont to monofun_def, etc.; changed intro/elim rules for these predicates into more useful rule_format; removed all MF2 lemmas (Pcpo.thy has more general versions now); cleaned up many proofs.
huffman
parents:
16096
diff
changeset
|
215 |
apply (subgoal_tac "max_in_chain i (\<lambda>i. f (Y i))") |
5dd79d3f0105
renamed theorems monofun, contlub, cont to monofun_def, etc.; changed intro/elim rules for these predicates into more useful rule_format; removed all MF2 lemmas (Pcpo.thy has more general versions now); cleaned up many proofs.
huffman
parents:
16096
diff
changeset
|
216 |
apply (simp add: maxinch_is_thelub ch2ch_monofun) |
5dd79d3f0105
renamed theorems monofun, contlub, cont to monofun_def, etc.; changed intro/elim rules for these predicates into more useful rule_format; removed all MF2 lemmas (Pcpo.thy has more general versions now); cleaned up many proofs.
huffman
parents:
16096
diff
changeset
|
217 |
apply (force simp add: max_in_chain_def) |
15565 | 218 |
done |
219 |
||
16624
645b9560f3fd
cleaned up; reorganized and added section headings
huffman
parents:
16564
diff
changeset
|
220 |
text {* some properties of flat *} |
645b9560f3fd
cleaned up; reorganized and added section headings
huffman
parents:
16564
diff
changeset
|
221 |
|
645b9560f3fd
cleaned up; reorganized and added section headings
huffman
parents:
16564
diff
changeset
|
222 |
lemma flatdom_strict2mono: "f \<bottom> = \<bottom> \<Longrightarrow> monofun (f::'a::flat \<Rightarrow> 'b::pcpo)" |
645b9560f3fd
cleaned up; reorganized and added section headings
huffman
parents:
16564
diff
changeset
|
223 |
apply (rule monofunI) |
25920 | 224 |
apply (drule ax_flat) |
16624
645b9560f3fd
cleaned up; reorganized and added section headings
huffman
parents:
16564
diff
changeset
|
225 |
apply auto |
645b9560f3fd
cleaned up; reorganized and added section headings
huffman
parents:
16564
diff
changeset
|
226 |
done |
645b9560f3fd
cleaned up; reorganized and added section headings
huffman
parents:
16564
diff
changeset
|
227 |
|
645b9560f3fd
cleaned up; reorganized and added section headings
huffman
parents:
16564
diff
changeset
|
228 |
lemma flatdom_strict2cont: "f \<bottom> = \<bottom> \<Longrightarrow> cont (f::'a::flat \<Rightarrow> 'b::pcpo)" |
645b9560f3fd
cleaned up; reorganized and added section headings
huffman
parents:
16564
diff
changeset
|
229 |
by (rule flatdom_strict2mono [THEN chfindom_monofun2cont]) |
15565 | 230 |
|
26024 | 231 |
text {* functions with discrete domain *} |
232 |
||
233 |
lemma cont_discrete_cpo [simp]: "cont (f::'a::discrete_cpo \<Rightarrow> 'b::cpo)" |
|
234 |
apply (rule contI) |
|
235 |
apply (drule discrete_chain_const, clarify) |
|
236 |
apply (simp add: lub_const) |
|
237 |
done |
|
238 |
||
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
239 |
end |