src/HOLCF/Fix.thy
author huffman
Sat, 04 Jun 2005 00:22:08 +0200
changeset 16221 879400e029bf
parent 16214 e3816a7db016
child 16388 1ff571813848
permissions -rw-r--r--
New theory with lemmas for the fixrec package
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
2640
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch:
slotosch
parents: 2275
diff changeset
     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
21eb5e156d91 expanded tabs
clasohm
parents: 1410
diff changeset
     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
e16da3068ad6 fix headers
huffman
parents: 15576
diff changeset
     8
header {* Fixed point operator and admissibility *}
e16da3068ad6 fix headers
huffman
parents: 15576
diff changeset
     9
e16da3068ad6 fix headers
huffman
parents: 15576
diff changeset
    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
e16da3068ad6 fix headers
huffman
parents: 15576
diff changeset
    12
begin
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    13
16082
ebb53ebfd4e2 added defaultsort declaration
huffman
parents: 16079
diff changeset
    14
defaultsort pcpo
ebb53ebfd4e2 added defaultsort declaration
huffman
parents: 16079
diff changeset
    15
16005
42f3f299ee68 cleaned up and shortened some proofs
huffman
parents: 15857
diff changeset
    16
subsection {* Definitions *}
42f3f299ee68 cleaned up and shortened some proofs
huffman
parents: 15857
diff changeset
    17
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    18
consts
16214
e3816a7db016 cleaned up proof of cont_Ifix
huffman
parents: 16082
diff changeset
    19
  iterate :: "nat \<Rightarrow> ('a \<rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a"
e3816a7db016 cleaned up proof of cont_Ifix
huffman
parents: 16082
diff changeset
    20
  Ifix    :: "('a \<rightarrow> 'a) \<Rightarrow> 'a"
e3816a7db016 cleaned up proof of cont_Ifix
huffman
parents: 16082
diff changeset
    21
  "fix"   :: "('a \<rightarrow> 'a) \<rightarrow> 'a"
e3816a7db016 cleaned up proof of cont_Ifix
huffman
parents: 16082
diff changeset
    22
  admw    :: "('a \<Rightarrow> bool) \<Rightarrow> bool"
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    23
5192
704dd3a6d47d Adapted to new datatype package.
berghofe
parents: 4721
diff changeset
    24
primrec
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents: 14981
diff changeset
    25
  iterate_0:   "iterate 0 F x = x"
16214
e3816a7db016 cleaned up proof of cont_Ifix
huffman
parents: 16082
diff changeset
    26
  iterate_Suc: "iterate (Suc n) F x  = F\<cdot>(iterate n F x)"
5192
704dd3a6d47d Adapted to new datatype package.
berghofe
parents: 4721
diff changeset
    27
1168
74be52691d62 The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents: 1150
diff changeset
    28
defs
16214
e3816a7db016 cleaned up proof of cont_Ifix
huffman
parents: 16082
diff changeset
    29
  Ifix_def:      "Ifix \<equiv> \<lambda>F. \<Squnion>i. iterate i F \<bottom>"
e3816a7db016 cleaned up proof of cont_Ifix
huffman
parents: 16082
diff changeset
    30
  fix_def:       "fix \<equiv> \<Lambda> F. Ifix F"
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    31
16214
e3816a7db016 cleaned up proof of cont_Ifix
huffman
parents: 16082
diff changeset
    32
  admw_def:      "admw P == !F. (!n. P (iterate n F UU)) -->
1479
21eb5e156d91 expanded tabs
clasohm
parents: 1410
diff changeset
    33
                            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
    34
16005
42f3f299ee68 cleaned up and shortened some proofs
huffman
parents: 15857
diff changeset
    35
subsection {* Binder syntax for @{term fix} *}
15857
83cb9dae3817 Added binder syntax for fix
huffman
parents: 15637
diff changeset
    36
83cb9dae3817 Added binder syntax for fix
huffman
parents: 15637
diff changeset
    37
syntax
83cb9dae3817 Added binder syntax for fix
huffman
parents: 15637
diff changeset
    38
  "@FIX" :: "('a => 'a) => 'a"  (binder "FIX " 10)
83cb9dae3817 Added binder syntax for fix
huffman
parents: 15637
diff changeset
    39
  "@FIXP" :: "[patterns, 'a] => 'a"  ("(3FIX <_>./ _)" [0, 10] 10)
83cb9dae3817 Added binder syntax for fix
huffman
parents: 15637
diff changeset
    40
83cb9dae3817 Added binder syntax for fix
huffman
parents: 15637
diff changeset
    41
syntax (xsymbols)
83cb9dae3817 Added binder syntax for fix
huffman
parents: 15637
diff changeset
    42
  "FIX " :: "[idt, 'a] => 'a"  ("(3\<mu>_./ _)" [0, 10] 10)
83cb9dae3817 Added binder syntax for fix
huffman
parents: 15637
diff changeset
    43
  "@FIXP" :: "[patterns, 'a] => 'a"  ("(3\<mu>()<_>./ _)" [0, 10] 10)
83cb9dae3817 Added binder syntax for fix
huffman
parents: 15637
diff changeset
    44
83cb9dae3817 Added binder syntax for fix
huffman
parents: 15637
diff changeset
    45
translations
83cb9dae3817 Added binder syntax for fix
huffman
parents: 15637
diff changeset
    46
  "FIX x. LAM y. t" == "fix\<cdot>(LAM x y. t)"
83cb9dae3817 Added binder syntax for fix
huffman
parents: 15637
diff changeset
    47
  "FIX x. t" == "fix\<cdot>(LAM x. t)"
83cb9dae3817 Added binder syntax for fix
huffman
parents: 15637
diff changeset
    48
  "FIX <xs>. t" == "fix\<cdot>(LAM <xs>. t)"
83cb9dae3817 Added binder syntax for fix
huffman
parents: 15637
diff changeset
    49
16005
42f3f299ee68 cleaned up and shortened some proofs
huffman
parents: 15857
diff changeset
    50
subsection {* Properties of @{term iterate} and @{term fix} *}
42f3f299ee68 cleaned up and shortened some proofs
huffman
parents: 15857
diff changeset
    51
15637
d2a06007ebfa changed comments to text blocks, cleaned up a few proofs
huffman
parents: 15577
diff changeset
    52
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
    53
16214
e3816a7db016 cleaned up proof of cont_Ifix
huffman
parents: 16082
diff changeset
    54
lemma iterate_Suc2: "iterate (Suc n) F x = iterate n F (F\<cdot>x)"
e3816a7db016 cleaned up proof of cont_Ifix
huffman
parents: 16082
diff changeset
    55
by (induct_tac n, auto)
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents: 14981
diff changeset
    56
15637
d2a06007ebfa changed comments to text blocks, cleaned up a few proofs
huffman
parents: 15577
diff changeset
    57
text {*
d2a06007ebfa changed comments to text blocks, cleaned up a few proofs
huffman
parents: 15577
diff changeset
    58
  The sequence of function iterations is a chain.
d2a06007ebfa changed comments to text blocks, cleaned up a few proofs
huffman
parents: 15577
diff changeset
    59
  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
    60
*}
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents: 14981
diff changeset
    61
16214
e3816a7db016 cleaned up proof of cont_Ifix
huffman
parents: 16082
diff changeset
    62
lemma chain_iterate2: "x \<sqsubseteq> F\<cdot>x \<Longrightarrow> chain (\<lambda>i. iterate i F x)"
e3816a7db016 cleaned up proof of cont_Ifix
huffman
parents: 16082
diff changeset
    63
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
    64
16214
e3816a7db016 cleaned up proof of cont_Ifix
huffman
parents: 16082
diff changeset
    65
lemma chain_iterate: "chain (\<lambda>i. iterate i F \<bottom>)"
16005
42f3f299ee68 cleaned up and shortened some proofs
huffman
parents: 15857
diff changeset
    66
by (rule chain_iterate2 [OF minimal])
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents: 14981
diff changeset
    67
15637
d2a06007ebfa changed comments to text blocks, cleaned up a few proofs
huffman
parents: 15577
diff changeset
    68
text {*
d2a06007ebfa changed comments to text blocks, cleaned up a few proofs
huffman
parents: 15577
diff changeset
    69
  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
    70
  omega cpo's
d2a06007ebfa changed comments to text blocks, cleaned up a few proofs
huffman
parents: 15577
diff changeset
    71
*}
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents: 14981
diff changeset
    72
16214
e3816a7db016 cleaned up proof of cont_Ifix
huffman
parents: 16082
diff changeset
    73
lemma Ifix_eq: "Ifix F = F\<cdot>(Ifix F)"
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents: 14981
diff changeset
    74
apply (unfold Ifix_def)
16005
42f3f299ee68 cleaned up and shortened some proofs
huffman
parents: 15857
diff changeset
    75
apply (subst lub_range_shift [of _ 1, symmetric])
42f3f299ee68 cleaned up and shortened some proofs
huffman
parents: 15857
diff changeset
    76
apply (rule chain_iterate)
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents: 14981
diff changeset
    77
apply (subst contlub_cfun_arg)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents: 14981
diff changeset
    78
apply (rule chain_iterate)
16005
42f3f299ee68 cleaned up and shortened some proofs
huffman
parents: 15857
diff changeset
    79
apply simp
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents: 14981
diff changeset
    80
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents: 14981
diff changeset
    81
16214
e3816a7db016 cleaned up proof of cont_Ifix
huffman
parents: 16082
diff changeset
    82
lemma Ifix_least: "F\<cdot>x = x \<Longrightarrow> Ifix F \<sqsubseteq> x"
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents: 14981
diff changeset
    83
apply (unfold Ifix_def)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents: 14981
diff changeset
    84
apply (rule is_lub_thelub)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents: 14981
diff changeset
    85
apply (rule chain_iterate)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents: 14981
diff changeset
    86
apply (rule ub_rangeI)
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
16214
e3816a7db016 cleaned up proof of cont_Ifix
huffman
parents: 16082
diff changeset
    90
apply (erule subst)
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
text {* continuity of @{term iterate} *}
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents: 14981
diff changeset
    95
16214
e3816a7db016 cleaned up proof of cont_Ifix
huffman
parents: 16082
diff changeset
    96
lemma cont_iterate1: "cont (\<lambda>F. iterate n F x)"
e3816a7db016 cleaned up proof of cont_Ifix
huffman
parents: 16082
diff changeset
    97
by (induct_tac n, simp_all)
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents: 14981
diff changeset
    98
16214
e3816a7db016 cleaned up proof of cont_Ifix
huffman
parents: 16082
diff changeset
    99
lemma cont_iterate2: "cont (\<lambda>x. iterate n F x)"
e3816a7db016 cleaned up proof of cont_Ifix
huffman
parents: 16082
diff changeset
   100
by (induct_tac n, simp_all)
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents: 14981
diff changeset
   101
16214
e3816a7db016 cleaned up proof of cont_Ifix
huffman
parents: 16082
diff changeset
   102
lemma cont_iterate: "cont (iterate n)"
e3816a7db016 cleaned up proof of cont_Ifix
huffman
parents: 16082
diff changeset
   103
by (rule cont_iterate1 [THEN cont2cont_CF1L_rev2])
15576
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
lemmas monofun_iterate2 = cont_iterate2 [THEN cont2mono, standard]
e3816a7db016 cleaned up proof of cont_Ifix
huffman
parents: 16082
diff changeset
   106
lemmas contlub_iterate2 = cont_iterate2 [THEN cont2contlub, standard]
e3816a7db016 cleaned up proof of cont_Ifix
huffman
parents: 16082
diff changeset
   107
e3816a7db016 cleaned up proof of cont_Ifix
huffman
parents: 16082
diff changeset
   108
text {* continuity of @{term Ifix} *}
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents: 14981
diff changeset
   109
16214
e3816a7db016 cleaned up proof of cont_Ifix
huffman
parents: 16082
diff changeset
   110
lemma cont_Ifix: "cont Ifix"
e3816a7db016 cleaned up proof of cont_Ifix
huffman
parents: 16082
diff changeset
   111
apply (unfold Ifix_def)
e3816a7db016 cleaned up proof of cont_Ifix
huffman
parents: 16082
diff changeset
   112
apply (rule cont2cont_lub)
e3816a7db016 cleaned up proof of cont_Ifix
huffman
parents: 16082
diff changeset
   113
apply (rule ch2ch_fun_rev)
16005
42f3f299ee68 cleaned up and shortened some proofs
huffman
parents: 15857
diff changeset
   114
apply (rule chain_iterate)
16214
e3816a7db016 cleaned up proof of cont_Ifix
huffman
parents: 16082
diff changeset
   115
apply (rule cont_iterate1)
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents: 14981
diff changeset
   116
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents: 14981
diff changeset
   117
15637
d2a06007ebfa changed comments to text blocks, cleaned up a few proofs
huffman
parents: 15577
diff changeset
   118
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
   119
16214
e3816a7db016 cleaned up proof of cont_Ifix
huffman
parents: 16082
diff changeset
   120
lemma fix_eq: "fix\<cdot>F = F\<cdot>(fix\<cdot>F)"
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents: 14981
diff changeset
   121
apply (unfold fix_def)
15637
d2a06007ebfa changed comments to text blocks, cleaned up a few proofs
huffman
parents: 15577
diff changeset
   122
apply (simp add: cont_Ifix)
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents: 14981
diff changeset
   123
apply (rule Ifix_eq)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents: 14981
diff changeset
   124
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents: 14981
diff changeset
   125
16214
e3816a7db016 cleaned up proof of cont_Ifix
huffman
parents: 16082
diff changeset
   126
lemma fix_least: "F\<cdot>x = x \<Longrightarrow> fix\<cdot>F \<sqsubseteq> x"
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents: 14981
diff changeset
   127
apply (unfold fix_def)
15637
d2a06007ebfa changed comments to text blocks, cleaned up a few proofs
huffman
parents: 15577
diff changeset
   128
apply (simp add: cont_Ifix)
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents: 14981
diff changeset
   129
apply (erule Ifix_least)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents: 14981
diff changeset
   130
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents: 14981
diff changeset
   131
16214
e3816a7db016 cleaned up proof of cont_Ifix
huffman
parents: 16082
diff changeset
   132
lemma fix_eqI: "\<lbrakk>F\<cdot>x = x; \<forall>z. F\<cdot>z = z \<longrightarrow> x \<sqsubseteq> z\<rbrakk> \<Longrightarrow> x = fix\<cdot>F"
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents: 14981
diff changeset
   133
apply (rule antisym_less)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents: 14981
diff changeset
   134
apply (erule allE)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents: 14981
diff changeset
   135
apply (erule mp)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents: 14981
diff changeset
   136
apply (rule fix_eq [symmetric])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents: 14981
diff changeset
   137
apply (erule fix_least)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents: 14981
diff changeset
   138
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents: 14981
diff changeset
   139
16214
e3816a7db016 cleaned up proof of cont_Ifix
huffman
parents: 16082
diff changeset
   140
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
   141
by (simp add: fix_eq [symmetric])
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents: 14981
diff changeset
   142
16214
e3816a7db016 cleaned up proof of cont_Ifix
huffman
parents: 16082
diff changeset
   143
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
   144
by (erule fix_eq2 [THEN cfun_fun_cong])
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents: 14981
diff changeset
   145
16214
e3816a7db016 cleaned up proof of cont_Ifix
huffman
parents: 16082
diff changeset
   146
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
   147
apply (erule ssubst)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents: 14981
diff changeset
   148
apply (rule fix_eq)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents: 14981
diff changeset
   149
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents: 14981
diff changeset
   150
16214
e3816a7db016 cleaned up proof of cont_Ifix
huffman
parents: 16082
diff changeset
   151
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
   152
by (erule fix_eq4 [THEN cfun_fun_cong])
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents: 14981
diff changeset
   153
15637
d2a06007ebfa changed comments to text blocks, cleaned up a few proofs
huffman
parents: 15577
diff changeset
   154
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
   155
16214
e3816a7db016 cleaned up proof of cont_Ifix
huffman
parents: 16082
diff changeset
   156
lemma fix_def2: "fix\<cdot>F = (\<Squnion>i. iterate i F \<bottom>)"
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents: 14981
diff changeset
   157
apply (unfold fix_def)
16214
e3816a7db016 cleaned up proof of cont_Ifix
huffman
parents: 16082
diff changeset
   158
apply (simp add: cont_Ifix)
e3816a7db016 cleaned up proof of cont_Ifix
huffman
parents: 16082
diff changeset
   159
apply (simp add: Ifix_def)
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents: 14981
diff changeset
   160
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents: 14981
diff changeset
   161
16005
42f3f299ee68 cleaned up and shortened some proofs
huffman
parents: 15857
diff changeset
   162
subsection {* Admissibility and fixed point induction *}
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents: 14981
diff changeset
   163
15637
d2a06007ebfa changed comments to text blocks, cleaned up a few proofs
huffman
parents: 15577
diff changeset
   164
text {* an admissible formula is also weak admissible *}
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents: 14981
diff changeset
   165
16214
e3816a7db016 cleaned up proof of cont_Ifix
huffman
parents: 16082
diff changeset
   166
lemma adm_impl_admw: "adm P \<Longrightarrow> admw P"
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents: 14981
diff changeset
   167
apply (unfold admw_def)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents: 14981
diff changeset
   168
apply (intro strip)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents: 14981
diff changeset
   169
apply (erule admD)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents: 14981
diff changeset
   170
apply (rule chain_iterate)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents: 14981
diff changeset
   171
apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents: 14981
diff changeset
   172
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents: 14981
diff changeset
   173
16079
757e1c4a8081 moved adm_chfindom from Adm.thy to Fix.thy, to remove dependence on Cfun
huffman
parents: 16070
diff changeset
   174
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
   175
16214
e3816a7db016 cleaned up proof of cont_Ifix
huffman
parents: 16082
diff changeset
   176
lemma adm_chfindom: "adm (\<lambda>(u::'a::cpo \<rightarrow> 'b::chfin). P(u\<cdot>s))"
16079
757e1c4a8081 moved adm_chfindom from Adm.thy to Fix.thy, to remove dependence on Cfun
huffman
parents: 16070
diff changeset
   177
apply (unfold adm_def)
757e1c4a8081 moved adm_chfindom from Adm.thy to Fix.thy, to remove dependence on Cfun
huffman
parents: 16070
diff changeset
   178
apply (intro strip)
757e1c4a8081 moved adm_chfindom from Adm.thy to Fix.thy, to remove dependence on Cfun
huffman
parents: 16070
diff changeset
   179
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
   180
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
   181
apply clarsimp
757e1c4a8081 moved adm_chfindom from Adm.thy to Fix.thy, to remove dependence on Cfun
huffman
parents: 16070
diff changeset
   182
done
757e1c4a8081 moved adm_chfindom from Adm.thy to Fix.thy, to remove dependence on Cfun
huffman
parents: 16070
diff changeset
   183
757e1c4a8081 moved adm_chfindom from Adm.thy to Fix.thy, to remove dependence on Cfun
huffman
parents: 16070
diff changeset
   184
(* 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
   185
15637
d2a06007ebfa changed comments to text blocks, cleaned up a few proofs
huffman
parents: 15577
diff changeset
   186
text {* fixed point induction *}
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents: 14981
diff changeset
   187
16214
e3816a7db016 cleaned up proof of cont_Ifix
huffman
parents: 16082
diff changeset
   188
lemma fix_ind: "\<lbrakk>adm P; P \<bottom>; \<And>x. P x \<Longrightarrow> P (F\<cdot>x)\<rbrakk> \<Longrightarrow> P (fix\<cdot>F)"
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents: 14981
diff changeset
   189
apply (subst fix_def2)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents: 14981
diff changeset
   190
apply (erule admD)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents: 14981
diff changeset
   191
apply (rule chain_iterate)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents: 14981
diff changeset
   192
apply (rule allI)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents: 14981
diff changeset
   193
apply (induct_tac "i")
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents: 14981
diff changeset
   194
apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents: 14981
diff changeset
   195
apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents: 14981
diff changeset
   196
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents: 14981
diff changeset
   197
16214
e3816a7db016 cleaned up proof of cont_Ifix
huffman
parents: 16082
diff changeset
   198
lemma def_fix_ind:
e3816a7db016 cleaned up proof of cont_Ifix
huffman
parents: 16082
diff changeset
   199
  "\<lbrakk>f \<equiv> fix\<cdot>F; adm P; P \<bottom>; \<And>x. P x \<Longrightarrow> P (F\<cdot>x)\<rbrakk> \<Longrightarrow> P f"
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents: 14981
diff changeset
   200
apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents: 14981
diff changeset
   201
apply (erule fix_ind)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents: 14981
diff changeset
   202
apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents: 14981
diff changeset
   203
apply fast
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents: 14981
diff changeset
   204
done
15637
d2a06007ebfa changed comments to text blocks, cleaned up a few proofs
huffman
parents: 15577
diff changeset
   205
d2a06007ebfa changed comments to text blocks, cleaned up a few proofs
huffman
parents: 15577
diff changeset
   206
text {* computational induction for weak admissible formulae *}
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents: 14981
diff changeset
   207
16214
e3816a7db016 cleaned up proof of cont_Ifix
huffman
parents: 16082
diff changeset
   208
lemma wfix_ind: "\<lbrakk>admw P; \<forall>n. P (iterate n F UU)\<rbrakk> \<Longrightarrow> P (fix\<cdot>F)"
e3816a7db016 cleaned up proof of cont_Ifix
huffman
parents: 16082
diff changeset
   209
by (simp add: fix_def2 admw_def)
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents: 14981
diff changeset
   210
16214
e3816a7db016 cleaned up proof of cont_Ifix
huffman
parents: 16082
diff changeset
   211
lemma def_wfix_ind:
e3816a7db016 cleaned up proof of cont_Ifix
huffman
parents: 16082
diff changeset
   212
  "\<lbrakk>f \<equiv> fix\<cdot>F; admw P; \<forall>n. P (iterate n F \<bottom>)\<rbrakk> \<Longrightarrow> P f"
e3816a7db016 cleaned up proof of cont_Ifix
huffman
parents: 16082
diff changeset
   213
by (simp, rule wfix_ind)
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents: 14981
diff changeset
   214
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   215
end