src/HOL/HOLCF/Fix.thy
author wenzelm
Sat, 07 Apr 2012 16:41:59 +0200
changeset 47389 e8552cba702d
parent 44066 d74182c93f04
child 58880 0baae4311a9f
permissions -rw-r--r--
explicit checks stable_finished_theory/stable_command allow parallel asynchronous command transactions; tuned;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
42151
4da4fc77664b tuned headers;
wenzelm
parents: 41430
diff changeset
     1
(*  Title:      HOL/HOLCF/Fix.thy
1479
21eb5e156d91 expanded tabs
clasohm
parents: 1410
diff changeset
     2
    Author:     Franz Regensburger
35794
8cd7134275cc use headers consistently
huffman
parents: 35055
diff changeset
     3
    Author:     Brian Huffman
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
     4
*)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
     5
15577
e16da3068ad6 fix headers
huffman
parents: 15576
diff changeset
     6
header {* Fixed point operator and admissibility *}
e16da3068ad6 fix headers
huffman
parents: 15576
diff changeset
     7
e16da3068ad6 fix headers
huffman
parents: 15576
diff changeset
     8
theory Fix
35939
db69a6a1fbb5 minimize dependencies
huffman
parents: 35932
diff changeset
     9
imports Cfun
15577
e16da3068ad6 fix headers
huffman
parents: 15576
diff changeset
    10
begin
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    11
36452
d37c6eed8117 renamed command 'defaultsort' to 'default_sort';
wenzelm
parents: 36075
diff changeset
    12
default_sort pcpo
16082
ebb53ebfd4e2 added defaultsort declaration
huffman
parents: 16079
diff changeset
    13
18093
587692219f69 put iterate and fix in separate sections; added Letrec
huffman
parents: 18092
diff changeset
    14
subsection {* Iteration *}
16005
42f3f299ee68 cleaned up and shortened some proofs
huffman
parents: 15857
diff changeset
    15
34941
156925dd67af dropped some old primrecs and some constdefs
haftmann
parents: 33590
diff changeset
    16
primrec iterate :: "nat \<Rightarrow> ('a::cpo \<rightarrow> 'a) \<rightarrow> ('a \<rightarrow> 'a)" where
156925dd67af dropped some old primrecs and some constdefs
haftmann
parents: 33590
diff changeset
    17
    "iterate 0 = (\<Lambda> F x. x)"
156925dd67af dropped some old primrecs and some constdefs
haftmann
parents: 33590
diff changeset
    18
  | "iterate (Suc n) = (\<Lambda> F x. F\<cdot>(iterate n\<cdot>F\<cdot>x))"
5192
704dd3a6d47d Adapted to new datatype package.
berghofe
parents: 4721
diff changeset
    19
18093
587692219f69 put iterate and fix in separate sections; added Letrec
huffman
parents: 18092
diff changeset
    20
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
    21
18074
a92b7c5133de reorganized; removed intermediate constant Ifix; changed iterate to a continuous type; added theorem fix_least_less
huffman
parents: 17816
diff changeset
    22
lemma iterate_0 [simp]: "iterate 0\<cdot>F\<cdot>x = x"
a92b7c5133de reorganized; removed intermediate constant Ifix; changed iterate to a continuous type; added theorem fix_least_less
huffman
parents: 17816
diff changeset
    23
by simp
a92b7c5133de reorganized; removed intermediate constant Ifix; changed iterate to a continuous type; added theorem fix_least_less
huffman
parents: 17816
diff changeset
    24
a92b7c5133de reorganized; removed intermediate constant Ifix; changed iterate to a continuous type; added theorem fix_least_less
huffman
parents: 17816
diff changeset
    25
lemma iterate_Suc [simp]: "iterate (Suc n)\<cdot>F\<cdot>x = F\<cdot>(iterate n\<cdot>F\<cdot>x)"
a92b7c5133de reorganized; removed intermediate constant Ifix; changed iterate to a continuous type; added theorem fix_least_less
huffman
parents: 17816
diff changeset
    26
by simp
a92b7c5133de reorganized; removed intermediate constant Ifix; changed iterate to a continuous type; added theorem fix_least_less
huffman
parents: 17816
diff changeset
    27
a92b7c5133de reorganized; removed intermediate constant Ifix; changed iterate to a continuous type; added theorem fix_least_less
huffman
parents: 17816
diff changeset
    28
declare iterate.simps [simp del]
a92b7c5133de reorganized; removed intermediate constant Ifix; changed iterate to a continuous type; added theorem fix_least_less
huffman
parents: 17816
diff changeset
    29
a92b7c5133de reorganized; removed intermediate constant Ifix; changed iterate to a continuous type; added theorem fix_least_less
huffman
parents: 17816
diff changeset
    30
lemma iterate_Suc2: "iterate (Suc n)\<cdot>F\<cdot>x = iterate n\<cdot>F\<cdot>(F\<cdot>x)"
27270
6a353260735e add lemma iterate_iterate
huffman
parents: 27185
diff changeset
    31
by (induct n) simp_all
6a353260735e add lemma iterate_iterate
huffman
parents: 27185
diff changeset
    32
6a353260735e add lemma iterate_iterate
huffman
parents: 27185
diff changeset
    33
lemma iterate_iterate:
6a353260735e add lemma iterate_iterate
huffman
parents: 27185
diff changeset
    34
  "iterate m\<cdot>F\<cdot>(iterate n\<cdot>F\<cdot>x) = iterate (m + n)\<cdot>F\<cdot>x"
6a353260735e add lemma iterate_iterate
huffman
parents: 27185
diff changeset
    35
by (induct m) simp_all
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents: 14981
diff changeset
    36
36075
2e0370c03066 tuned proof (no induction needed); removed unused lemma and fuzzy comment
krauss
parents: 35939
diff changeset
    37
text {* The sequence of function iterations is a chain. *}
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents: 14981
diff changeset
    38
18074
a92b7c5133de reorganized; removed intermediate constant Ifix; changed iterate to a continuous type; added theorem fix_least_less
huffman
parents: 17816
diff changeset
    39
lemma chain_iterate [simp]: "chain (\<lambda>i. iterate i\<cdot>F\<cdot>\<bottom>)"
36075
2e0370c03066 tuned proof (no induction needed); removed unused lemma and fuzzy comment
krauss
parents: 35939
diff changeset
    40
by (rule chainI, unfold iterate_Suc2, rule monofun_cfun_arg, rule minimal)
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents: 14981
diff changeset
    41
18093
587692219f69 put iterate and fix in separate sections; added Letrec
huffman
parents: 18092
diff changeset
    42
587692219f69 put iterate and fix in separate sections; added Letrec
huffman
parents: 18092
diff changeset
    43
subsection {* Least fixed point operator *}
587692219f69 put iterate and fix in separate sections; added Letrec
huffman
parents: 18092
diff changeset
    44
25131
2c8caac48ade modernized specifications ('definition', 'abbreviation', 'notation');
wenzelm
parents: 18095
diff changeset
    45
definition
2c8caac48ade modernized specifications ('definition', 'abbreviation', 'notation');
wenzelm
parents: 18095
diff changeset
    46
  "fix" :: "('a \<rightarrow> 'a) \<rightarrow> 'a" where
2c8caac48ade modernized specifications ('definition', 'abbreviation', 'notation');
wenzelm
parents: 18095
diff changeset
    47
  "fix = (\<Lambda> F. \<Squnion>i. iterate i\<cdot>F\<cdot>\<bottom>)"
18093
587692219f69 put iterate and fix in separate sections; added Letrec
huffman
parents: 18092
diff changeset
    48
587692219f69 put iterate and fix in separate sections; added Letrec
huffman
parents: 18092
diff changeset
    49
text {* Binder syntax for @{term fix} *}
587692219f69 put iterate and fix in separate sections; added Letrec
huffman
parents: 18092
diff changeset
    50
27316
9e74019041d4 use new-style abbreviation/notation for fix syntax
huffman
parents: 27270
diff changeset
    51
abbreviation
9e74019041d4 use new-style abbreviation/notation for fix syntax
huffman
parents: 27270
diff changeset
    52
  fix_syn :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a"  (binder "FIX " 10) where
9e74019041d4 use new-style abbreviation/notation for fix syntax
huffman
parents: 27270
diff changeset
    53
  "fix_syn (\<lambda>x. f x) \<equiv> fix\<cdot>(\<Lambda> x. f x)"
18093
587692219f69 put iterate and fix in separate sections; added Letrec
huffman
parents: 18092
diff changeset
    54
27316
9e74019041d4 use new-style abbreviation/notation for fix syntax
huffman
parents: 27270
diff changeset
    55
notation (xsymbols)
9e74019041d4 use new-style abbreviation/notation for fix syntax
huffman
parents: 27270
diff changeset
    56
  fix_syn  (binder "\<mu> " 10)
18093
587692219f69 put iterate and fix in separate sections; added Letrec
huffman
parents: 18092
diff changeset
    57
587692219f69 put iterate and fix in separate sections; added Letrec
huffman
parents: 18092
diff changeset
    58
text {* Properties of @{term fix} *}
18074
a92b7c5133de reorganized; removed intermediate constant Ifix; changed iterate to a continuous type; added theorem fix_least_less
huffman
parents: 17816
diff changeset
    59
18090
9d5cfd71f510 moved adm_chfindom from Fix.thy to Cfun.thy; moved admw-related stuff to its own section
huffman
parents: 18078
diff changeset
    60
text {* direct connection between @{term fix} and iteration *}
18074
a92b7c5133de reorganized; removed intermediate constant Ifix; changed iterate to a continuous type; added theorem fix_least_less
huffman
parents: 17816
diff changeset
    61
a92b7c5133de reorganized; removed intermediate constant Ifix; changed iterate to a continuous type; added theorem fix_least_less
huffman
parents: 17816
diff changeset
    62
lemma fix_def2: "fix\<cdot>F = (\<Squnion>i. iterate i\<cdot>F\<cdot>\<bottom>)"
40004
9f6ed6840e8d reformulate lemma cont2cont_lub and move to Cont.thy
huffman
parents: 36452
diff changeset
    63
unfolding fix_def by simp
18074
a92b7c5133de reorganized; removed intermediate constant Ifix; changed iterate to a continuous type; added theorem fix_least_less
huffman
parents: 17816
diff changeset
    64
35055
f0ecf952b864 add lemma iterate_below_fix
huffman
parents: 34941
diff changeset
    65
lemma iterate_below_fix: "iterate n\<cdot>f\<cdot>\<bottom> \<sqsubseteq> fix\<cdot>f"
f0ecf952b864 add lemma iterate_below_fix
huffman
parents: 34941
diff changeset
    66
  unfolding fix_def2
f0ecf952b864 add lemma iterate_below_fix
huffman
parents: 34941
diff changeset
    67
  using chain_iterate by (rule is_ub_thelub)
f0ecf952b864 add lemma iterate_below_fix
huffman
parents: 34941
diff changeset
    68
15637
d2a06007ebfa changed comments to text blocks, cleaned up a few proofs
huffman
parents: 15577
diff changeset
    69
text {*
d2a06007ebfa changed comments to text blocks, cleaned up a few proofs
huffman
parents: 15577
diff changeset
    70
  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
    71
  omega cpo's
d2a06007ebfa changed comments to text blocks, cleaned up a few proofs
huffman
parents: 15577
diff changeset
    72
*}
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents: 14981
diff changeset
    73
18074
a92b7c5133de reorganized; removed intermediate constant Ifix; changed iterate to a continuous type; added theorem fix_least_less
huffman
parents: 17816
diff changeset
    74
lemma fix_eq: "fix\<cdot>F = F\<cdot>(fix\<cdot>F)"
a92b7c5133de reorganized; removed intermediate constant Ifix; changed iterate to a continuous type; added theorem fix_least_less
huffman
parents: 17816
diff changeset
    75
apply (simp add: fix_def2)
16005
42f3f299ee68 cleaned up and shortened some proofs
huffman
parents: 15857
diff changeset
    76
apply (subst lub_range_shift [of _ 1, symmetric])
42f3f299ee68 cleaned up and shortened some proofs
huffman
parents: 15857
diff changeset
    77
apply (rule chain_iterate)
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents: 14981
diff changeset
    78
apply (subst contlub_cfun_arg)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents: 14981
diff changeset
    79
apply (rule chain_iterate)
16005
42f3f299ee68 cleaned up and shortened some proofs
huffman
parents: 15857
diff changeset
    80
apply simp
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents: 14981
diff changeset
    81
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents: 14981
diff changeset
    82
31076
99fe356cbbc2 rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names
huffman
parents: 29138
diff changeset
    83
lemma fix_least_below: "F\<cdot>x \<sqsubseteq> x \<Longrightarrow> fix\<cdot>F \<sqsubseteq> x"
18074
a92b7c5133de reorganized; removed intermediate constant Ifix; changed iterate to a continuous type; added theorem fix_least_less
huffman
parents: 17816
diff changeset
    84
apply (simp add: fix_def2)
40500
ee9c8d36318e add lemmas lub_below, below_lub; simplify some proofs; remove some unused lemmas
huffman
parents: 40321
diff changeset
    85
apply (rule lub_below)
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents: 14981
diff changeset
    86
apply (rule chain_iterate)
16005
42f3f299ee68 cleaned up and shortened some proofs
huffman
parents: 15857
diff changeset
    87
apply (induct_tac i)
42f3f299ee68 cleaned up and shortened some proofs
huffman
parents: 15857
diff changeset
    88
apply simp
42f3f299ee68 cleaned up and shortened some proofs
huffman
parents: 15857
diff changeset
    89
apply simp
31076
99fe356cbbc2 rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names
huffman
parents: 29138
diff changeset
    90
apply (erule rev_below_trans)
16214
e3816a7db016 cleaned up proof of cont_Ifix
huffman
parents: 16082
diff changeset
    91
apply (erule monofun_cfun_arg)
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents: 14981
diff changeset
    92
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents: 14981
diff changeset
    93
16214
e3816a7db016 cleaned up proof of cont_Ifix
huffman
parents: 16082
diff changeset
    94
lemma fix_least: "F\<cdot>x = x \<Longrightarrow> fix\<cdot>F \<sqsubseteq> x"
31076
99fe356cbbc2 rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names
huffman
parents: 29138
diff changeset
    95
by (rule fix_least_below, simp)
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents: 14981
diff changeset
    96
27185
0407630909ef change orientation of fix_eqI and convert to rule_format;
huffman
parents: 25927
diff changeset
    97
lemma fix_eqI:
0407630909ef change orientation of fix_eqI and convert to rule_format;
huffman
parents: 25927
diff changeset
    98
  assumes fixed: "F\<cdot>x = x" and least: "\<And>z. F\<cdot>z = z \<Longrightarrow> x \<sqsubseteq> z"
0407630909ef change orientation of fix_eqI and convert to rule_format;
huffman
parents: 25927
diff changeset
    99
  shows "fix\<cdot>F = x"
31076
99fe356cbbc2 rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names
huffman
parents: 29138
diff changeset
   100
apply (rule below_antisym)
27185
0407630909ef change orientation of fix_eqI and convert to rule_format;
huffman
parents: 25927
diff changeset
   101
apply (rule fix_least [OF fixed])
0407630909ef change orientation of fix_eqI and convert to rule_format;
huffman
parents: 25927
diff changeset
   102
apply (rule least [OF fix_eq [symmetric]])
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents: 14981
diff changeset
   103
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents: 14981
diff changeset
   104
16214
e3816a7db016 cleaned up proof of cont_Ifix
huffman
parents: 16082
diff changeset
   105
lemma fix_eq2: "f \<equiv> fix\<cdot>F \<Longrightarrow> f = F\<cdot>f"
15637
d2a06007ebfa changed comments to text blocks, cleaned up a few proofs
huffman
parents: 15577
diff changeset
   106
by (simp add: fix_eq [symmetric])
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents: 14981
diff changeset
   107
16214
e3816a7db016 cleaned up proof of cont_Ifix
huffman
parents: 16082
diff changeset
   108
lemma fix_eq3: "f \<equiv> fix\<cdot>F \<Longrightarrow> f\<cdot>x = F\<cdot>f\<cdot>x"
15637
d2a06007ebfa changed comments to text blocks, cleaned up a few proofs
huffman
parents: 15577
diff changeset
   109
by (erule fix_eq2 [THEN cfun_fun_cong])
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents: 14981
diff changeset
   110
16214
e3816a7db016 cleaned up proof of cont_Ifix
huffman
parents: 16082
diff changeset
   111
lemma fix_eq4: "f = fix\<cdot>F \<Longrightarrow> f = F\<cdot>f"
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents: 14981
diff changeset
   112
apply (erule ssubst)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents: 14981
diff changeset
   113
apply (rule fix_eq)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents: 14981
diff changeset
   114
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents: 14981
diff changeset
   115
16214
e3816a7db016 cleaned up proof of cont_Ifix
huffman
parents: 16082
diff changeset
   116
lemma fix_eq5: "f = fix\<cdot>F \<Longrightarrow> f\<cdot>x = F\<cdot>f\<cdot>x"
e3816a7db016 cleaned up proof of cont_Ifix
huffman
parents: 16082
diff changeset
   117
by (erule fix_eq4 [THEN cfun_fun_cong])
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents: 14981
diff changeset
   118
16556
a0c8d0499b5f added theorems fix_strict, fix_defined, fix_id, fix_const
huffman
parents: 16388
diff changeset
   119
text {* strictness of @{term fix} *}
a0c8d0499b5f added theorems fix_strict, fix_defined, fix_id, fix_const
huffman
parents: 16388
diff changeset
   120
40321
d065b195ec89 rename lemmas *_defined_iff and *_strict_iff to *_bottom_iff
huffman
parents: 40004
diff changeset
   121
lemma fix_bottom_iff: "(fix\<cdot>F = \<bottom>) = (F\<cdot>\<bottom> = \<bottom>)"
16917
1fe50b19daba add theorem fix_defined_iff; cleaned up
huffman
parents: 16556
diff changeset
   122
apply (rule iffI)
1fe50b19daba add theorem fix_defined_iff; cleaned up
huffman
parents: 16556
diff changeset
   123
apply (erule subst)
1fe50b19daba add theorem fix_defined_iff; cleaned up
huffman
parents: 16556
diff changeset
   124
apply (rule fix_eq [symmetric])
41430
1aa23e9f2c87 change some lemma names containing 'UU' to 'bottom'
huffman
parents: 41324
diff changeset
   125
apply (erule fix_least [THEN bottomI])
16917
1fe50b19daba add theorem fix_defined_iff; cleaned up
huffman
parents: 16556
diff changeset
   126
done
1fe50b19daba add theorem fix_defined_iff; cleaned up
huffman
parents: 16556
diff changeset
   127
16556
a0c8d0499b5f added theorems fix_strict, fix_defined, fix_id, fix_const
huffman
parents: 16388
diff changeset
   128
lemma fix_strict: "F\<cdot>\<bottom> = \<bottom> \<Longrightarrow> fix\<cdot>F = \<bottom>"
40321
d065b195ec89 rename lemmas *_defined_iff and *_strict_iff to *_bottom_iff
huffman
parents: 40004
diff changeset
   129
by (simp add: fix_bottom_iff)
16556
a0c8d0499b5f added theorems fix_strict, fix_defined, fix_id, fix_const
huffman
parents: 16388
diff changeset
   130
a0c8d0499b5f added theorems fix_strict, fix_defined, fix_id, fix_const
huffman
parents: 16388
diff changeset
   131
lemma fix_defined: "F\<cdot>\<bottom> \<noteq> \<bottom> \<Longrightarrow> fix\<cdot>F \<noteq> \<bottom>"
40321
d065b195ec89 rename lemmas *_defined_iff and *_strict_iff to *_bottom_iff
huffman
parents: 40004
diff changeset
   132
by (simp add: fix_bottom_iff)
16556
a0c8d0499b5f added theorems fix_strict, fix_defined, fix_id, fix_const
huffman
parents: 16388
diff changeset
   133
a0c8d0499b5f added theorems fix_strict, fix_defined, fix_id, fix_const
huffman
parents: 16388
diff changeset
   134
text {* @{term fix} applied to identity and constant functions *}
a0c8d0499b5f added theorems fix_strict, fix_defined, fix_id, fix_const
huffman
parents: 16388
diff changeset
   135
a0c8d0499b5f added theorems fix_strict, fix_defined, fix_id, fix_const
huffman
parents: 16388
diff changeset
   136
lemma fix_id: "(\<mu> x. x) = \<bottom>"
a0c8d0499b5f added theorems fix_strict, fix_defined, fix_id, fix_const
huffman
parents: 16388
diff changeset
   137
by (simp add: fix_strict)
a0c8d0499b5f added theorems fix_strict, fix_defined, fix_id, fix_const
huffman
parents: 16388
diff changeset
   138
a0c8d0499b5f added theorems fix_strict, fix_defined, fix_id, fix_const
huffman
parents: 16388
diff changeset
   139
lemma fix_const: "(\<mu> x. c) = c"
18074
a92b7c5133de reorganized; removed intermediate constant Ifix; changed iterate to a continuous type; added theorem fix_least_less
huffman
parents: 17816
diff changeset
   140
by (subst fix_eq, simp)
16556
a0c8d0499b5f added theorems fix_strict, fix_defined, fix_id, fix_const
huffman
parents: 16388
diff changeset
   141
18090
9d5cfd71f510 moved adm_chfindom from Fix.thy to Cfun.thy; moved admw-related stuff to its own section
huffman
parents: 18078
diff changeset
   142
subsection {* Fixed point induction *}
9d5cfd71f510 moved adm_chfindom from Fix.thy to Cfun.thy; moved admw-related stuff to its own section
huffman
parents: 18078
diff changeset
   143
9d5cfd71f510 moved adm_chfindom from Fix.thy to Cfun.thy; moved admw-related stuff to its own section
huffman
parents: 18078
diff changeset
   144
lemma fix_ind: "\<lbrakk>adm P; P \<bottom>; \<And>x. P x \<Longrightarrow> P (F\<cdot>x)\<rbrakk> \<Longrightarrow> P (fix\<cdot>F)"
27185
0407630909ef change orientation of fix_eqI and convert to rule_format;
huffman
parents: 25927
diff changeset
   145
unfolding fix_def2
25925
3dc4acca4388 change lemma admD to rule_format
huffman
parents: 25131
diff changeset
   146
apply (erule admD)
18090
9d5cfd71f510 moved adm_chfindom from Fix.thy to Cfun.thy; moved admw-related stuff to its own section
huffman
parents: 18078
diff changeset
   147
apply (rule chain_iterate)
27185
0407630909ef change orientation of fix_eqI and convert to rule_format;
huffman
parents: 25927
diff changeset
   148
apply (rule nat_induct, simp_all)
18090
9d5cfd71f510 moved adm_chfindom from Fix.thy to Cfun.thy; moved admw-related stuff to its own section
huffman
parents: 18078
diff changeset
   149
done
9d5cfd71f510 moved adm_chfindom from Fix.thy to Cfun.thy; moved admw-related stuff to its own section
huffman
parents: 18078
diff changeset
   150
41324
1383653efec3 make internal proofs for deflation and isodefl theorems more robust, by avoiding calls to the simplifier for beta-reduction
huffman
parents: 40774
diff changeset
   151
lemma cont_fix_ind:
1383653efec3 make internal proofs for deflation and isodefl theorems more robust, by avoiding calls to the simplifier for beta-reduction
huffman
parents: 40774
diff changeset
   152
  "\<lbrakk>cont F; adm P; P \<bottom>; \<And>x. P x \<Longrightarrow> P (F x)\<rbrakk> \<Longrightarrow> P (fix\<cdot>(Abs_cfun F))"
1383653efec3 make internal proofs for deflation and isodefl theorems more robust, by avoiding calls to the simplifier for beta-reduction
huffman
parents: 40774
diff changeset
   153
by (simp add: fix_ind)
1383653efec3 make internal proofs for deflation and isodefl theorems more robust, by avoiding calls to the simplifier for beta-reduction
huffman
parents: 40774
diff changeset
   154
18090
9d5cfd71f510 moved adm_chfindom from Fix.thy to Cfun.thy; moved admw-related stuff to its own section
huffman
parents: 18078
diff changeset
   155
lemma def_fix_ind:
9d5cfd71f510 moved adm_chfindom from Fix.thy to Cfun.thy; moved admw-related stuff to its own section
huffman
parents: 18078
diff changeset
   156
  "\<lbrakk>f \<equiv> fix\<cdot>F; adm P; P \<bottom>; \<And>x. P x \<Longrightarrow> P (F\<cdot>x)\<rbrakk> \<Longrightarrow> P f"
9d5cfd71f510 moved adm_chfindom from Fix.thy to Cfun.thy; moved admw-related stuff to its own section
huffman
parents: 18078
diff changeset
   157
by (simp add: fix_ind)
9d5cfd71f510 moved adm_chfindom from Fix.thy to Cfun.thy; moved admw-related stuff to its own section
huffman
parents: 18078
diff changeset
   158
27185
0407630909ef change orientation of fix_eqI and convert to rule_format;
huffman
parents: 25927
diff changeset
   159
lemma fix_ind2:
0407630909ef change orientation of fix_eqI and convert to rule_format;
huffman
parents: 25927
diff changeset
   160
  assumes adm: "adm P"
0407630909ef change orientation of fix_eqI and convert to rule_format;
huffman
parents: 25927
diff changeset
   161
  assumes 0: "P \<bottom>" and 1: "P (F\<cdot>\<bottom>)"
0407630909ef change orientation of fix_eqI and convert to rule_format;
huffman
parents: 25927
diff changeset
   162
  assumes step: "\<And>x. \<lbrakk>P x; P (F\<cdot>x)\<rbrakk> \<Longrightarrow> P (F\<cdot>(F\<cdot>x))"
0407630909ef change orientation of fix_eqI and convert to rule_format;
huffman
parents: 25927
diff changeset
   163
  shows "P (fix\<cdot>F)"
0407630909ef change orientation of fix_eqI and convert to rule_format;
huffman
parents: 25927
diff changeset
   164
unfolding fix_def2
0407630909ef change orientation of fix_eqI and convert to rule_format;
huffman
parents: 25927
diff changeset
   165
apply (rule admD [OF adm chain_iterate])
0407630909ef change orientation of fix_eqI and convert to rule_format;
huffman
parents: 25927
diff changeset
   166
apply (rule nat_less_induct)
0407630909ef change orientation of fix_eqI and convert to rule_format;
huffman
parents: 25927
diff changeset
   167
apply (case_tac n)
0407630909ef change orientation of fix_eqI and convert to rule_format;
huffman
parents: 25927
diff changeset
   168
apply (simp add: 0)
0407630909ef change orientation of fix_eqI and convert to rule_format;
huffman
parents: 25927
diff changeset
   169
apply (case_tac nat)
0407630909ef change orientation of fix_eqI and convert to rule_format;
huffman
parents: 25927
diff changeset
   170
apply (simp add: 1)
0407630909ef change orientation of fix_eqI and convert to rule_format;
huffman
parents: 25927
diff changeset
   171
apply (frule_tac x=nat in spec)
0407630909ef change orientation of fix_eqI and convert to rule_format;
huffman
parents: 25927
diff changeset
   172
apply (simp add: step)
0407630909ef change orientation of fix_eqI and convert to rule_format;
huffman
parents: 25927
diff changeset
   173
done
0407630909ef change orientation of fix_eqI and convert to rule_format;
huffman
parents: 25927
diff changeset
   174
33590
1806f58a3651 add lemma parallel_fix_ind
huffman
parents: 31076
diff changeset
   175
lemma parallel_fix_ind:
1806f58a3651 add lemma parallel_fix_ind
huffman
parents: 31076
diff changeset
   176
  assumes adm: "adm (\<lambda>x. P (fst x) (snd x))"
1806f58a3651 add lemma parallel_fix_ind
huffman
parents: 31076
diff changeset
   177
  assumes base: "P \<bottom> \<bottom>"
1806f58a3651 add lemma parallel_fix_ind
huffman
parents: 31076
diff changeset
   178
  assumes step: "\<And>x y. P x y \<Longrightarrow> P (F\<cdot>x) (G\<cdot>y)"
1806f58a3651 add lemma parallel_fix_ind
huffman
parents: 31076
diff changeset
   179
  shows "P (fix\<cdot>F) (fix\<cdot>G)"
1806f58a3651 add lemma parallel_fix_ind
huffman
parents: 31076
diff changeset
   180
proof -
1806f58a3651 add lemma parallel_fix_ind
huffman
parents: 31076
diff changeset
   181
  from adm have adm': "adm (split P)"
1806f58a3651 add lemma parallel_fix_ind
huffman
parents: 31076
diff changeset
   182
    unfolding split_def .
1806f58a3651 add lemma parallel_fix_ind
huffman
parents: 31076
diff changeset
   183
  have "\<And>i. P (iterate i\<cdot>F\<cdot>\<bottom>) (iterate i\<cdot>G\<cdot>\<bottom>)"
1806f58a3651 add lemma parallel_fix_ind
huffman
parents: 31076
diff changeset
   184
    by (induct_tac i, simp add: base, simp add: step)
1806f58a3651 add lemma parallel_fix_ind
huffman
parents: 31076
diff changeset
   185
  hence "\<And>i. split P (iterate i\<cdot>F\<cdot>\<bottom>, iterate i\<cdot>G\<cdot>\<bottom>)"
1806f58a3651 add lemma parallel_fix_ind
huffman
parents: 31076
diff changeset
   186
    by simp
1806f58a3651 add lemma parallel_fix_ind
huffman
parents: 31076
diff changeset
   187
  hence "split P (\<Squnion>i. (iterate i\<cdot>F\<cdot>\<bottom>, iterate i\<cdot>G\<cdot>\<bottom>))"
1806f58a3651 add lemma parallel_fix_ind
huffman
parents: 31076
diff changeset
   188
    by - (rule admD [OF adm'], simp, assumption)
1806f58a3651 add lemma parallel_fix_ind
huffman
parents: 31076
diff changeset
   189
  hence "split P (\<Squnion>i. iterate i\<cdot>F\<cdot>\<bottom>, \<Squnion>i. iterate i\<cdot>G\<cdot>\<bottom>)"
40771
1c6f7d4b110e renamed several HOLCF theorems (listed in NEWS)
huffman
parents: 40500
diff changeset
   190
    by (simp add: lub_Pair)
33590
1806f58a3651 add lemma parallel_fix_ind
huffman
parents: 31076
diff changeset
   191
  hence "P (\<Squnion>i. iterate i\<cdot>F\<cdot>\<bottom>) (\<Squnion>i. iterate i\<cdot>G\<cdot>\<bottom>)"
1806f58a3651 add lemma parallel_fix_ind
huffman
parents: 31076
diff changeset
   192
    by simp
1806f58a3651 add lemma parallel_fix_ind
huffman
parents: 31076
diff changeset
   193
  thus "P (fix\<cdot>F) (fix\<cdot>G)"
1806f58a3651 add lemma parallel_fix_ind
huffman
parents: 31076
diff changeset
   194
    by (simp add: fix_def2)
1806f58a3651 add lemma parallel_fix_ind
huffman
parents: 31076
diff changeset
   195
qed
1806f58a3651 add lemma parallel_fix_ind
huffman
parents: 31076
diff changeset
   196
41324
1383653efec3 make internal proofs for deflation and isodefl theorems more robust, by avoiding calls to the simplifier for beta-reduction
huffman
parents: 40774
diff changeset
   197
lemma cont_parallel_fix_ind:
1383653efec3 make internal proofs for deflation and isodefl theorems more robust, by avoiding calls to the simplifier for beta-reduction
huffman
parents: 40774
diff changeset
   198
  assumes "cont F" and "cont G"
1383653efec3 make internal proofs for deflation and isodefl theorems more robust, by avoiding calls to the simplifier for beta-reduction
huffman
parents: 40774
diff changeset
   199
  assumes "adm (\<lambda>x. P (fst x) (snd x))"
1383653efec3 make internal proofs for deflation and isodefl theorems more robust, by avoiding calls to the simplifier for beta-reduction
huffman
parents: 40774
diff changeset
   200
  assumes "P \<bottom> \<bottom>"
1383653efec3 make internal proofs for deflation and isodefl theorems more robust, by avoiding calls to the simplifier for beta-reduction
huffman
parents: 40774
diff changeset
   201
  assumes "\<And>x y. P x y \<Longrightarrow> P (F x) (G y)"
1383653efec3 make internal proofs for deflation and isodefl theorems more robust, by avoiding calls to the simplifier for beta-reduction
huffman
parents: 40774
diff changeset
   202
  shows "P (fix\<cdot>(Abs_cfun F)) (fix\<cdot>(Abs_cfun G))"
1383653efec3 make internal proofs for deflation and isodefl theorems more robust, by avoiding calls to the simplifier for beta-reduction
huffman
parents: 40774
diff changeset
   203
by (rule parallel_fix_ind, simp_all add: assms)
1383653efec3 make internal proofs for deflation and isodefl theorems more robust, by avoiding calls to the simplifier for beta-reduction
huffman
parents: 40774
diff changeset
   204
35932
86559356502d move letrec stuff to new file HOLCF/ex/Letrec.thy
huffman
parents: 35923
diff changeset
   205
subsection {* Fixed-points on product types *}
18093
587692219f69 put iterate and fix in separate sections; added Letrec
huffman
parents: 18092
diff changeset
   206
18095
4328356ab7e6 add proof of Bekic's theorem: fix_cprod
huffman
parents: 18093
diff changeset
   207
text {*
4328356ab7e6 add proof of Bekic's theorem: fix_cprod
huffman
parents: 18093
diff changeset
   208
  Bekic's Theorem: Simultaneous fixed points over pairs
4328356ab7e6 add proof of Bekic's theorem: fix_cprod
huffman
parents: 18093
diff changeset
   209
  can be written in terms of separate fixed points.
4328356ab7e6 add proof of Bekic's theorem: fix_cprod
huffman
parents: 18093
diff changeset
   210
*}
4328356ab7e6 add proof of Bekic's theorem: fix_cprod
huffman
parents: 18093
diff changeset
   211
4328356ab7e6 add proof of Bekic's theorem: fix_cprod
huffman
parents: 18093
diff changeset
   212
lemma fix_cprod:
4328356ab7e6 add proof of Bekic's theorem: fix_cprod
huffman
parents: 18093
diff changeset
   213
  "fix\<cdot>(F::'a \<times> 'b \<rightarrow> 'a \<times> 'b) =
35921
cd1b01664810 convert lemma fix_cprod to use Pair, fst, snd
huffman
parents: 35915
diff changeset
   214
   (\<mu> x. fst (F\<cdot>(x, \<mu> y. snd (F\<cdot>(x, y)))),
cd1b01664810 convert lemma fix_cprod to use Pair, fst, snd
huffman
parents: 35915
diff changeset
   215
    \<mu> y. snd (F\<cdot>(\<mu> x. fst (F\<cdot>(x, \<mu> y. snd (F\<cdot>(x, y)))), y)))"
cd1b01664810 convert lemma fix_cprod to use Pair, fst, snd
huffman
parents: 35915
diff changeset
   216
  (is "fix\<cdot>F = (?x, ?y)")
27185
0407630909ef change orientation of fix_eqI and convert to rule_format;
huffman
parents: 25927
diff changeset
   217
proof (rule fix_eqI)
35921
cd1b01664810 convert lemma fix_cprod to use Pair, fst, snd
huffman
parents: 35915
diff changeset
   218
  have 1: "fst (F\<cdot>(?x, ?y)) = ?x"
18095
4328356ab7e6 add proof of Bekic's theorem: fix_cprod
huffman
parents: 18093
diff changeset
   219
    by (rule trans [symmetric, OF fix_eq], simp)
35921
cd1b01664810 convert lemma fix_cprod to use Pair, fst, snd
huffman
parents: 35915
diff changeset
   220
  have 2: "snd (F\<cdot>(?x, ?y)) = ?y"
18095
4328356ab7e6 add proof of Bekic's theorem: fix_cprod
huffman
parents: 18093
diff changeset
   221
    by (rule trans [symmetric, OF fix_eq], simp)
44066
d74182c93f04 rename Pair_fst_snd_eq to prod_eq_iff (keeping old name too)
huffman
parents: 42151
diff changeset
   222
  from 1 2 show "F\<cdot>(?x, ?y) = (?x, ?y)" by (simp add: prod_eq_iff)
18095
4328356ab7e6 add proof of Bekic's theorem: fix_cprod
huffman
parents: 18093
diff changeset
   223
next
4328356ab7e6 add proof of Bekic's theorem: fix_cprod
huffman
parents: 18093
diff changeset
   224
  fix z assume F_z: "F\<cdot>z = z"
35921
cd1b01664810 convert lemma fix_cprod to use Pair, fst, snd
huffman
parents: 35915
diff changeset
   225
  obtain x y where z: "z = (x,y)" by (rule prod.exhaust)
cd1b01664810 convert lemma fix_cprod to use Pair, fst, snd
huffman
parents: 35915
diff changeset
   226
  from F_z z have F_x: "fst (F\<cdot>(x, y)) = x" by simp
cd1b01664810 convert lemma fix_cprod to use Pair, fst, snd
huffman
parents: 35915
diff changeset
   227
  from F_z z have F_y: "snd (F\<cdot>(x, y)) = y" by simp
cd1b01664810 convert lemma fix_cprod to use Pair, fst, snd
huffman
parents: 35915
diff changeset
   228
  let ?y1 = "\<mu> y. snd (F\<cdot>(x, y))"
18095
4328356ab7e6 add proof of Bekic's theorem: fix_cprod
huffman
parents: 18093
diff changeset
   229
  have "?y1 \<sqsubseteq> y" by (rule fix_least, simp add: F_y)
35921
cd1b01664810 convert lemma fix_cprod to use Pair, fst, snd
huffman
parents: 35915
diff changeset
   230
  hence "fst (F\<cdot>(x, ?y1)) \<sqsubseteq> fst (F\<cdot>(x, y))"
cd1b01664810 convert lemma fix_cprod to use Pair, fst, snd
huffman
parents: 35915
diff changeset
   231
    by (simp add: fst_monofun monofun_cfun)
cd1b01664810 convert lemma fix_cprod to use Pair, fst, snd
huffman
parents: 35915
diff changeset
   232
  hence "fst (F\<cdot>(x, ?y1)) \<sqsubseteq> x" using F_x by simp
31076
99fe356cbbc2 rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names
huffman
parents: 29138
diff changeset
   233
  hence 1: "?x \<sqsubseteq> x" by (simp add: fix_least_below)
35921
cd1b01664810 convert lemma fix_cprod to use Pair, fst, snd
huffman
parents: 35915
diff changeset
   234
  hence "snd (F\<cdot>(?x, y)) \<sqsubseteq> snd (F\<cdot>(x, y))"
cd1b01664810 convert lemma fix_cprod to use Pair, fst, snd
huffman
parents: 35915
diff changeset
   235
    by (simp add: snd_monofun monofun_cfun)
cd1b01664810 convert lemma fix_cprod to use Pair, fst, snd
huffman
parents: 35915
diff changeset
   236
  hence "snd (F\<cdot>(?x, y)) \<sqsubseteq> y" using F_y by simp
31076
99fe356cbbc2 rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names
huffman
parents: 29138
diff changeset
   237
  hence 2: "?y \<sqsubseteq> y" by (simp add: fix_least_below)
35921
cd1b01664810 convert lemma fix_cprod to use Pair, fst, snd
huffman
parents: 35915
diff changeset
   238
  show "(?x, ?y) \<sqsubseteq> z" using z 1 2 by simp
18095
4328356ab7e6 add proof of Bekic's theorem: fix_cprod
huffman
parents: 18093
diff changeset
   239
qed
4328356ab7e6 add proof of Bekic's theorem: fix_cprod
huffman
parents: 18093
diff changeset
   240
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   241
end