src/HOLCF/Fix.ML
author nipkow
Fri, 27 Nov 1998 17:01:21 +0100
changeset 5984 4c2fc177f4d3
parent 5656 f8389824189b
child 6073 fba734ba6894
permissions -rw-r--r--
*** empty log message ***
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
2640
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch:
slotosch
parents: 2619
diff changeset
     1
(*  Title:      HOLCF/Fix.ML
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
     2
    ID:         $Id$
1461
6bcb44e4d6e5 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
    Copyright   1993  Technische Universitaet Muenchen
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
     5
2640
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch:
slotosch
parents: 2619
diff changeset
     6
Lemmas for Fix.thy 
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
     7
*)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
     8
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
     9
open Fix;
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    10
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    11
(* ------------------------------------------------------------------------ *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    12
(* derive inductive properties of iterate from primitive recursion          *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    13
(* ------------------------------------------------------------------------ *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    14
2640
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch:
slotosch
parents: 2619
diff changeset
    15
qed_goal "iterate_Suc2" thy "iterate (Suc n) F x = iterate n F (F`x)"
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    16
 (fn prems =>
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
    17
        [
5192
704dd3a6d47d Adapted to new datatype package.
berghofe
parents: 5143
diff changeset
    18
        (induct_tac "n" 1),
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
    19
        (Simp_tac 1),
2033
639de962ded4 Ran expandshort; used stac instead of ssubst
paulson
parents: 1992
diff changeset
    20
        (stac iterate_Suc 1),
639de962ded4 Ran expandshort; used stac instead of ssubst
paulson
parents: 1992
diff changeset
    21
        (stac iterate_Suc 1),
639de962ded4 Ran expandshort; used stac instead of ssubst
paulson
parents: 1992
diff changeset
    22
        (etac ssubst 1),
639de962ded4 Ran expandshort; used stac instead of ssubst
paulson
parents: 1992
diff changeset
    23
        (rtac refl 1)
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
    24
        ]);
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    25
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    26
(* ------------------------------------------------------------------------ *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    27
(* the sequence of function itertaions is a chain                           *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    28
(* This property is essential since monotonicity of iterate makes no sense  *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    29
(* ------------------------------------------------------------------------ *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    30
4720
c1b83b42f65a added not1_or and if_eq_cancel to simpset()
oheimb
parents: 4477
diff changeset
    31
qed_goalw "chain_iterate2" thy [chain] 
c1b83b42f65a added not1_or and if_eq_cancel to simpset()
oheimb
parents: 4477
diff changeset
    32
        " x << F`x ==> chain (%i. iterate i F x)"
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    33
 (fn prems =>
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
    34
        [
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
    35
        (cut_facts_tac prems 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
    36
        (strip_tac 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
    37
        (Simp_tac 1),
5192
704dd3a6d47d Adapted to new datatype package.
berghofe
parents: 5143
diff changeset
    38
        (induct_tac "i" 1),
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
    39
        (Asm_simp_tac 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
    40
        (Asm_simp_tac 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
    41
        (etac monofun_cfun_arg 1)
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
    42
        ]);
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    43
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    44
4720
c1b83b42f65a added not1_or and if_eq_cancel to simpset()
oheimb
parents: 4477
diff changeset
    45
qed_goal "chain_iterate" thy  
c1b83b42f65a added not1_or and if_eq_cancel to simpset()
oheimb
parents: 4477
diff changeset
    46
        "chain (%i. iterate i F UU)"
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    47
 (fn prems =>
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
    48
        [
4720
c1b83b42f65a added not1_or and if_eq_cancel to simpset()
oheimb
parents: 4477
diff changeset
    49
        (rtac chain_iterate2 1),
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
    50
        (rtac minimal 1)
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
    51
        ]);
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    52
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    53
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    54
(* ------------------------------------------------------------------------ *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    55
(* Kleene's fixed point theorems for continuous functions in pointed        *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    56
(* omega cpo's                                                              *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    57
(* ------------------------------------------------------------------------ *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    58
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    59
2640
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch:
slotosch
parents: 2619
diff changeset
    60
qed_goalw "Ifix_eq" thy  [Ifix_def] "Ifix F =F`(Ifix F)"
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    61
 (fn prems =>
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
    62
        [
2033
639de962ded4 Ran expandshort; used stac instead of ssubst
paulson
parents: 1992
diff changeset
    63
        (stac contlub_cfun_arg 1),
4720
c1b83b42f65a added not1_or and if_eq_cancel to simpset()
oheimb
parents: 4477
diff changeset
    64
        (rtac chain_iterate 1),
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
    65
        (rtac antisym_less 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
    66
        (rtac lub_mono 1),
4720
c1b83b42f65a added not1_or and if_eq_cancel to simpset()
oheimb
parents: 4477
diff changeset
    67
        (rtac chain_iterate 1),
5291
5706f0ef1d43 eliminated fabs,fapp.
slotosch
parents: 5192
diff changeset
    68
        (rtac ch2ch_Rep_CFunR 1),
4720
c1b83b42f65a added not1_or and if_eq_cancel to simpset()
oheimb
parents: 4477
diff changeset
    69
        (rtac chain_iterate 1),
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
    70
        (rtac allI 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
    71
        (rtac (iterate_Suc RS subst) 1),
4720
c1b83b42f65a added not1_or and if_eq_cancel to simpset()
oheimb
parents: 4477
diff changeset
    72
        (rtac (chain_iterate RS chainE RS spec) 1),
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
    73
        (rtac is_lub_thelub 1),
5291
5706f0ef1d43 eliminated fabs,fapp.
slotosch
parents: 5192
diff changeset
    74
        (rtac ch2ch_Rep_CFunR 1),
4720
c1b83b42f65a added not1_or and if_eq_cancel to simpset()
oheimb
parents: 4477
diff changeset
    75
        (rtac chain_iterate 1),
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
    76
        (rtac ub_rangeI 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
    77
        (rtac allI 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
    78
        (rtac (iterate_Suc RS subst) 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
    79
        (rtac is_ub_thelub 1),
4720
c1b83b42f65a added not1_or and if_eq_cancel to simpset()
oheimb
parents: 4477
diff changeset
    80
        (rtac chain_iterate 1)
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
    81
        ]);
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    82
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    83
2640
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch:
slotosch
parents: 2619
diff changeset
    84
qed_goalw "Ifix_least" thy [Ifix_def] "F`x=x ==> Ifix(F) << x"
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    85
 (fn prems =>
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
    86
        [
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
    87
        (cut_facts_tac prems 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
    88
        (rtac is_lub_thelub 1),
4720
c1b83b42f65a added not1_or and if_eq_cancel to simpset()
oheimb
parents: 4477
diff changeset
    89
        (rtac chain_iterate 1),
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
    90
        (rtac ub_rangeI 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
    91
        (strip_tac 1),
5192
704dd3a6d47d Adapted to new datatype package.
berghofe
parents: 5143
diff changeset
    92
        (induct_tac "i" 1),
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
    93
        (Asm_simp_tac 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
    94
        (Asm_simp_tac 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
    95
        (res_inst_tac [("t","x")] subst 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
    96
        (atac 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
    97
        (etac monofun_cfun_arg 1)
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
    98
        ]);
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    99
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   100
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   101
(* ------------------------------------------------------------------------ *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   102
(* monotonicity and continuity of iterate                                   *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   103
(* ------------------------------------------------------------------------ *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   104
2640
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch:
slotosch
parents: 2619
diff changeset
   105
qed_goalw "monofun_iterate" thy  [monofun] "monofun(iterate(i))"
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   106
 (fn prems =>
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   107
        [
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   108
        (strip_tac 1),
5192
704dd3a6d47d Adapted to new datatype package.
berghofe
parents: 5143
diff changeset
   109
        (induct_tac "i" 1),
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   110
        (Asm_simp_tac 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   111
        (Asm_simp_tac 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   112
        (rtac (less_fun RS iffD2) 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   113
        (rtac allI 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   114
        (rtac monofun_cfun 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   115
        (atac 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   116
        (rtac (less_fun RS iffD1 RS spec) 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   117
        (atac 1)
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   118
        ]);
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   119
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   120
(* ------------------------------------------------------------------------ *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   121
(* the following lemma uses contlub_cfun which itself is based on a         *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   122
(* diagonalisation lemma for continuous functions with two arguments.       *)
5291
5706f0ef1d43 eliminated fabs,fapp.
slotosch
parents: 5192
diff changeset
   123
(* In this special case it is the application function Rep_CFun                 *)
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   124
(* ------------------------------------------------------------------------ *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   125
2640
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch:
slotosch
parents: 2619
diff changeset
   126
qed_goalw "contlub_iterate" thy  [contlub] "contlub(iterate(i))"
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   127
 (fn prems =>
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   128
        [
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   129
        (strip_tac 1),
5192
704dd3a6d47d Adapted to new datatype package.
berghofe
parents: 5143
diff changeset
   130
        (induct_tac "i" 1),
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   131
        (Asm_simp_tac 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   132
        (rtac (lub_const RS thelubI RS sym) 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   133
        (Asm_simp_tac 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   134
        (rtac ext 1),
2033
639de962ded4 Ran expandshort; used stac instead of ssubst
paulson
parents: 1992
diff changeset
   135
        (stac thelub_fun 1),
4720
c1b83b42f65a added not1_or and if_eq_cancel to simpset()
oheimb
parents: 4477
diff changeset
   136
        (rtac chainI 1),
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   137
        (rtac allI 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   138
        (rtac (less_fun RS iffD2) 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   139
        (rtac allI 1),
4720
c1b83b42f65a added not1_or and if_eq_cancel to simpset()
oheimb
parents: 4477
diff changeset
   140
        (rtac (chainE RS spec) 1),
5291
5706f0ef1d43 eliminated fabs,fapp.
slotosch
parents: 5192
diff changeset
   141
        (rtac (monofun_Rep_CFun1 RS ch2ch_MF2LR) 1),
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   142
        (rtac allI 1),
5291
5706f0ef1d43 eliminated fabs,fapp.
slotosch
parents: 5192
diff changeset
   143
        (rtac monofun_Rep_CFun2 1),
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   144
        (atac 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   145
        (rtac ch2ch_fun 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   146
        (rtac (monofun_iterate RS ch2ch_monofun) 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   147
        (atac 1),
2033
639de962ded4 Ran expandshort; used stac instead of ssubst
paulson
parents: 1992
diff changeset
   148
        (stac thelub_fun 1),
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   149
        (rtac (monofun_iterate RS ch2ch_monofun) 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   150
        (atac 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   151
        (rtac contlub_cfun  1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   152
        (atac 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   153
        (etac (monofun_iterate RS ch2ch_monofun RS ch2ch_fun) 1)
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   154
        ]);
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   155
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   156
2640
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch:
slotosch
parents: 2619
diff changeset
   157
qed_goal "cont_iterate" thy "cont(iterate(i))"
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   158
 (fn prems =>
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   159
        [
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   160
        (rtac monocontlub2cont 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   161
        (rtac monofun_iterate 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   162
        (rtac contlub_iterate 1)
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   163
        ]);
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   164
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   165
(* ------------------------------------------------------------------------ *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   166
(* a lemma about continuity of iterate in its third argument                *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   167
(* ------------------------------------------------------------------------ *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   168
2640
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch:
slotosch
parents: 2619
diff changeset
   169
qed_goal "monofun_iterate2" thy "monofun(iterate n F)"
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   170
 (fn prems =>
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   171
        [
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   172
        (rtac monofunI 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   173
        (strip_tac 1),
5192
704dd3a6d47d Adapted to new datatype package.
berghofe
parents: 5143
diff changeset
   174
        (induct_tac "n" 1),
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   175
        (Asm_simp_tac 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   176
        (Asm_simp_tac 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   177
        (etac monofun_cfun_arg 1)
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   178
        ]);
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   179
2640
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch:
slotosch
parents: 2619
diff changeset
   180
qed_goal "contlub_iterate2" thy "contlub(iterate n F)"
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   181
 (fn prems =>
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   182
        [
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   183
        (rtac contlubI 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   184
        (strip_tac 1),
5192
704dd3a6d47d Adapted to new datatype package.
berghofe
parents: 5143
diff changeset
   185
        (induct_tac "n" 1),
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   186
        (Simp_tac 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   187
        (Simp_tac 1),
3044
3e3087aa69e7 Updates because nat_ind_tac no longer appends "1" to the ind.var.
nipkow
parents: 2841
diff changeset
   188
        (res_inst_tac [("t","iterate n F (lub(range(%u. Y u)))"),
3e3087aa69e7 Updates because nat_ind_tac no longer appends "1" to the ind.var.
nipkow
parents: 2841
diff changeset
   189
        ("s","lub(range(%i. iterate n F (Y i)))")] ssubst 1),
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   190
        (atac 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   191
        (rtac contlub_cfun_arg 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   192
        (etac (monofun_iterate2 RS ch2ch_monofun) 1)
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   193
        ]);
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   194
2640
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch:
slotosch
parents: 2619
diff changeset
   195
qed_goal "cont_iterate2" thy "cont (iterate n F)"
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   196
 (fn prems =>
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   197
        [
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   198
        (rtac monocontlub2cont 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   199
        (rtac monofun_iterate2 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   200
        (rtac contlub_iterate2 1)
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   201
        ]);
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   202
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   203
(* ------------------------------------------------------------------------ *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   204
(* monotonicity and continuity of Ifix                                      *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   205
(* ------------------------------------------------------------------------ *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   206
2640
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch:
slotosch
parents: 2619
diff changeset
   207
qed_goalw "monofun_Ifix" thy  [monofun,Ifix_def] "monofun(Ifix)"
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   208
 (fn prems =>
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   209
        [
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   210
        (strip_tac 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   211
        (rtac lub_mono 1),
4720
c1b83b42f65a added not1_or and if_eq_cancel to simpset()
oheimb
parents: 4477
diff changeset
   212
        (rtac chain_iterate 1),
c1b83b42f65a added not1_or and if_eq_cancel to simpset()
oheimb
parents: 4477
diff changeset
   213
        (rtac chain_iterate 1),
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   214
        (rtac allI 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   215
        (rtac (less_fun RS iffD1 RS spec) 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   216
        (etac (monofun_iterate RS monofunE RS spec RS spec RS mp) 1)
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   217
        ]);
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   218
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   219
(* ------------------------------------------------------------------------ *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   220
(* since iterate is not monotone in its first argument, special lemmas must *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   221
(* be derived for lubs in this argument                                     *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   222
(* ------------------------------------------------------------------------ *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   223
4720
c1b83b42f65a added not1_or and if_eq_cancel to simpset()
oheimb
parents: 4477
diff changeset
   224
qed_goal "chain_iterate_lub" thy   
c1b83b42f65a added not1_or and if_eq_cancel to simpset()
oheimb
parents: 4477
diff changeset
   225
"chain(Y) ==> chain(%i. lub(range(%ia. iterate ia (Y i) UU)))"
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   226
 (fn prems =>
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   227
        [
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   228
        (cut_facts_tac prems 1),
4720
c1b83b42f65a added not1_or and if_eq_cancel to simpset()
oheimb
parents: 4477
diff changeset
   229
        (rtac chainI 1),
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   230
        (strip_tac 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   231
        (rtac lub_mono 1),
4720
c1b83b42f65a added not1_or and if_eq_cancel to simpset()
oheimb
parents: 4477
diff changeset
   232
        (rtac chain_iterate 1),
c1b83b42f65a added not1_or and if_eq_cancel to simpset()
oheimb
parents: 4477
diff changeset
   233
        (rtac chain_iterate 1),
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   234
        (strip_tac 1),
4720
c1b83b42f65a added not1_or and if_eq_cancel to simpset()
oheimb
parents: 4477
diff changeset
   235
        (etac (monofun_iterate RS ch2ch_monofun RS ch2ch_fun RS chainE 
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   236
         RS spec) 1)
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   237
        ]);
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   238
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   239
(* ------------------------------------------------------------------------ *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   240
(* this exchange lemma is analog to the one for monotone functions          *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   241
(* observe that monotonicity is not really needed. The propagation of       *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   242
(* chains is the essential argument which is usually derived from monot.    *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   243
(* ------------------------------------------------------------------------ *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   244
2640
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch:
slotosch
parents: 2619
diff changeset
   245
qed_goal "contlub_Ifix_lemma1" thy 
4720
c1b83b42f65a added not1_or and if_eq_cancel to simpset()
oheimb
parents: 4477
diff changeset
   246
"chain(Y) ==>iterate n (lub(range Y)) y = lub(range(%i. iterate n (Y i) y))"
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   247
 (fn prems =>
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   248
        [
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   249
        (cut_facts_tac prems 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   250
        (rtac (thelub_fun RS subst) 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   251
        (rtac (monofun_iterate RS ch2ch_monofun) 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   252
        (atac 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   253
        (rtac fun_cong 1),
2033
639de962ded4 Ran expandshort; used stac instead of ssubst
paulson
parents: 1992
diff changeset
   254
        (stac (contlub_iterate RS contlubE RS spec RS mp) 1),
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   255
        (atac 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   256
        (rtac refl 1)
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   257
        ]);
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   258
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   259
4720
c1b83b42f65a added not1_or and if_eq_cancel to simpset()
oheimb
parents: 4477
diff changeset
   260
qed_goal "ex_lub_iterate" thy  "chain(Y) ==>\
1168
74be52691d62 The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents: 892
diff changeset
   261
\         lub(range(%i. lub(range(%ia. iterate i (Y ia) UU)))) =\
74be52691d62 The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents: 892
diff changeset
   262
\         lub(range(%i. lub(range(%ia. iterate ia (Y i) UU))))"
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   263
 (fn prems =>
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   264
        [
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   265
        (cut_facts_tac prems 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   266
        (rtac antisym_less 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   267
        (rtac is_lub_thelub 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   268
        (rtac (contlub_Ifix_lemma1 RS ext RS subst) 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   269
        (atac 1),
4720
c1b83b42f65a added not1_or and if_eq_cancel to simpset()
oheimb
parents: 4477
diff changeset
   270
        (rtac chain_iterate 1),
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   271
        (rtac ub_rangeI 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   272
        (strip_tac 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   273
        (rtac lub_mono 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   274
        (etac (monofun_iterate RS ch2ch_monofun RS ch2ch_fun) 1),
4720
c1b83b42f65a added not1_or and if_eq_cancel to simpset()
oheimb
parents: 4477
diff changeset
   275
        (etac chain_iterate_lub 1),
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   276
        (strip_tac 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   277
        (rtac is_ub_thelub 1),
4720
c1b83b42f65a added not1_or and if_eq_cancel to simpset()
oheimb
parents: 4477
diff changeset
   278
        (rtac chain_iterate 1),
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   279
        (rtac is_lub_thelub 1),
4720
c1b83b42f65a added not1_or and if_eq_cancel to simpset()
oheimb
parents: 4477
diff changeset
   280
        (etac chain_iterate_lub 1),
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   281
        (rtac ub_rangeI 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   282
        (strip_tac 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   283
        (rtac lub_mono 1),
4720
c1b83b42f65a added not1_or and if_eq_cancel to simpset()
oheimb
parents: 4477
diff changeset
   284
        (rtac chain_iterate 1),
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   285
        (rtac (contlub_Ifix_lemma1 RS ext RS subst) 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   286
        (atac 1),
4720
c1b83b42f65a added not1_or and if_eq_cancel to simpset()
oheimb
parents: 4477
diff changeset
   287
        (rtac chain_iterate 1),
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   288
        (strip_tac 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   289
        (rtac is_ub_thelub 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   290
        (etac (monofun_iterate RS ch2ch_monofun RS ch2ch_fun) 1)
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   291
        ]);
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   292
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   293
2640
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch:
slotosch
parents: 2619
diff changeset
   294
qed_goalw "contlub_Ifix" thy  [contlub,Ifix_def] "contlub(Ifix)"
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   295
 (fn prems =>
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   296
        [
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   297
        (strip_tac 1),
2033
639de962ded4 Ran expandshort; used stac instead of ssubst
paulson
parents: 1992
diff changeset
   298
        (stac (contlub_Ifix_lemma1 RS ext) 1),
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   299
        (atac 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   300
        (etac ex_lub_iterate 1)
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   301
        ]);
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   302
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   303
2640
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch:
slotosch
parents: 2619
diff changeset
   304
qed_goal "cont_Ifix" thy "cont(Ifix)"
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   305
 (fn prems =>
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   306
        [
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   307
        (rtac monocontlub2cont 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   308
        (rtac monofun_Ifix 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   309
        (rtac contlub_Ifix 1)
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   310
        ]);
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   311
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   312
(* ------------------------------------------------------------------------ *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   313
(* propagate properties of Ifix to its continuous counterpart               *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   314
(* ------------------------------------------------------------------------ *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   315
2640
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch:
slotosch
parents: 2619
diff changeset
   316
qed_goalw "fix_eq" thy  [fix_def] "fix`F = F`(fix`F)"
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   317
 (fn prems =>
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   318
        [
4098
71e05eb27fb6 isatool fixclasimp;
wenzelm
parents: 3842
diff changeset
   319
        (asm_simp_tac (simpset() addsimps [cont_Ifix]) 1),
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   320
        (rtac Ifix_eq 1)
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   321
        ]);
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   322
2640
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch:
slotosch
parents: 2619
diff changeset
   323
qed_goalw "fix_least" thy [fix_def] "F`x = x ==> fix`F << x"
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   324
 (fn prems =>
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   325
        [
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   326
        (cut_facts_tac prems 1),
4098
71e05eb27fb6 isatool fixclasimp;
wenzelm
parents: 3842
diff changeset
   327
        (asm_simp_tac (simpset() addsimps [cont_Ifix]) 1),
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   328
        (etac Ifix_least 1)
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   329
        ]);
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   330
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   331
2640
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch:
slotosch
parents: 2619
diff changeset
   332
qed_goal "fix_eqI" thy
1274
ea0668a1c0ba added 8bit pragmas
regensbu
parents: 1267
diff changeset
   333
"[| F`x = x; !z. F`z = z --> x << z |] ==> x = fix`F"
ea0668a1c0ba added 8bit pragmas
regensbu
parents: 1267
diff changeset
   334
 (fn prems =>
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   335
        [
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   336
        (cut_facts_tac prems 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   337
        (rtac antisym_less 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   338
        (etac allE 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   339
        (etac mp 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   340
        (rtac (fix_eq RS sym) 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   341
        (etac fix_least 1)
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   342
        ]);
1274
ea0668a1c0ba added 8bit pragmas
regensbu
parents: 1267
diff changeset
   343
ea0668a1c0ba added 8bit pragmas
regensbu
parents: 1267
diff changeset
   344
2640
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch:
slotosch
parents: 2619
diff changeset
   345
qed_goal "fix_eq2" thy "f == fix`F ==> f = F`f"
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   346
 (fn prems =>
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   347
        [
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   348
        (rewrite_goals_tac prems),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   349
        (rtac fix_eq 1)
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   350
        ]);
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   351
2640
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch:
slotosch
parents: 2619
diff changeset
   352
qed_goal "fix_eq3" thy "f == fix`F ==> f`x = F`f`x"
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   353
 (fn prems =>
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   354
        [
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   355
        (rtac trans 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   356
        (rtac ((hd prems) RS fix_eq2 RS cfun_fun_cong) 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   357
        (rtac refl 1)
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   358
        ]);
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   359
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   360
fun fix_tac3 thm i  = ((rtac trans i) THEN (rtac (thm RS fix_eq3) i)); 
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   361
2640
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch:
slotosch
parents: 2619
diff changeset
   362
qed_goal "fix_eq4" thy "f = fix`F ==> f = F`f"
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   363
 (fn prems =>
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   364
        [
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   365
        (cut_facts_tac prems 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   366
        (hyp_subst_tac 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   367
        (rtac fix_eq 1)
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   368
        ]);
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   369
2640
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch:
slotosch
parents: 2619
diff changeset
   370
qed_goal "fix_eq5" thy "f = fix`F ==> f`x = F`f`x"
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   371
 (fn prems =>
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   372
        [
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   373
        (rtac trans 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   374
        (rtac ((hd prems) RS fix_eq4 RS cfun_fun_cong) 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   375
        (rtac refl 1)
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   376
        ]);
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   377
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   378
fun fix_tac5 thm i  = ((rtac trans i) THEN (rtac (thm RS fix_eq5) i)); 
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   379
3652
4c484f03079c added case_prover
oheimb
parents: 3460
diff changeset
   380
(* proves the unfolding theorem for function equations f = fix`... *)
4c484f03079c added case_prover
oheimb
parents: 3460
diff changeset
   381
fun fix_prover thy fixeq s = prove_goal thy s (fn prems => [
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   382
        (rtac trans 1),
3652
4c484f03079c added case_prover
oheimb
parents: 3460
diff changeset
   383
        (rtac (fixeq RS fix_eq4) 1),
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   384
        (rtac trans 1),
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   385
        (rtac beta_cfun 1),
2566
cbf02fc74332 changed handling of cont_lemmas and adm_lemmas
oheimb
parents: 2354
diff changeset
   386
        (Simp_tac 1)
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   387
        ]);
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   388
3652
4c484f03079c added case_prover
oheimb
parents: 3460
diff changeset
   389
(* proves the unfolding theorem for function definitions f == fix`... *)
4c484f03079c added case_prover
oheimb
parents: 3460
diff changeset
   390
fun fix_prover2 thy fixdef s = prove_goal thy s (fn prems => [
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   391
        (rtac trans 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   392
        (rtac (fix_eq2) 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   393
        (rtac fixdef 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   394
        (rtac beta_cfun 1),
2566
cbf02fc74332 changed handling of cont_lemmas and adm_lemmas
oheimb
parents: 2354
diff changeset
   395
        (Simp_tac 1)
1168
74be52691d62 The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents: 892
diff changeset
   396
        ]);
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   397
3652
4c484f03079c added case_prover
oheimb
parents: 3460
diff changeset
   398
(* proves an application case for a function from its unfolding thm *)
4c484f03079c added case_prover
oheimb
parents: 3460
diff changeset
   399
fun case_prover thy unfold s = prove_goal thy s (fn prems => [
4c484f03079c added case_prover
oheimb
parents: 3460
diff changeset
   400
	(cut_facts_tac prems 1),
4c484f03079c added case_prover
oheimb
parents: 3460
diff changeset
   401
	(rtac trans 1),
4c484f03079c added case_prover
oheimb
parents: 3460
diff changeset
   402
	(stac unfold 1),
4477
b3e5857d8d99 New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
paulson
parents: 4423
diff changeset
   403
	Auto_tac
3652
4c484f03079c added case_prover
oheimb
parents: 3460
diff changeset
   404
	]);
4c484f03079c added case_prover
oheimb
parents: 3460
diff changeset
   405
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   406
(* ------------------------------------------------------------------------ *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   407
(* better access to definitions                                             *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   408
(* ------------------------------------------------------------------------ *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   409
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   410
2640
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch:
slotosch
parents: 2619
diff changeset
   411
qed_goal "Ifix_def2" thy "Ifix=(%x. lub(range(%i. iterate i x UU)))"
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   412
 (fn prems =>
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   413
        [
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   414
        (rtac ext 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   415
        (rewtac Ifix_def),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   416
        (rtac refl 1)
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   417
        ]);
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   418
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   419
(* ------------------------------------------------------------------------ *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   420
(* direct connection between fix and iteration without Ifix                 *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   421
(* ------------------------------------------------------------------------ *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   422
2640
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch:
slotosch
parents: 2619
diff changeset
   423
qed_goalw "fix_def2" thy [fix_def]
1168
74be52691d62 The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents: 892
diff changeset
   424
 "fix`F = lub(range(%i. iterate i F UU))"
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   425
 (fn prems =>
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   426
        [
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   427
        (fold_goals_tac [Ifix_def]),
4098
71e05eb27fb6 isatool fixclasimp;
wenzelm
parents: 3842
diff changeset
   428
        (asm_simp_tac (simpset() addsimps [cont_Ifix]) 1)
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   429
        ]);
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   430
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   431
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   432
(* ------------------------------------------------------------------------ *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   433
(* Lemmas about admissibility and fixed point induction                     *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   434
(* ------------------------------------------------------------------------ *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   435
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   436
(* ------------------------------------------------------------------------ *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   437
(* access to definitions                                                    *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   438
(* ------------------------------------------------------------------------ *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   439
3460
5d71eed16fbe Tuned Franz's proofs.
nipkow
parents: 3326
diff changeset
   440
qed_goalw "admI" thy [adm_def]
4720
c1b83b42f65a added not1_or and if_eq_cancel to simpset()
oheimb
parents: 4477
diff changeset
   441
        "(!!Y. [| chain(Y); !i. P(Y(i)) |] ==> P(lub(range(Y)))) ==> adm(P)"
3460
5d71eed16fbe Tuned Franz's proofs.
nipkow
parents: 3326
diff changeset
   442
 (fn prems => [fast_tac (HOL_cs addIs prems) 1]);
5d71eed16fbe Tuned Franz's proofs.
nipkow
parents: 3326
diff changeset
   443
5d71eed16fbe Tuned Franz's proofs.
nipkow
parents: 3326
diff changeset
   444
qed_goalw "admD" thy [adm_def]
4720
c1b83b42f65a added not1_or and if_eq_cancel to simpset()
oheimb
parents: 4477
diff changeset
   445
        "!!P. [| adm(P); chain(Y); !i. P(Y(i)) |] ==> P(lub(range(Y)))"
3460
5d71eed16fbe Tuned Franz's proofs.
nipkow
parents: 3326
diff changeset
   446
 (fn prems => [fast_tac HOL_cs 1]);
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   447
2640
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch:
slotosch
parents: 2619
diff changeset
   448
qed_goalw "admw_def2" thy [admw_def]
3842
b55686a7b22c fixed dots;
wenzelm
parents: 3661
diff changeset
   449
        "admw(P) = (!F.(!n. P(iterate n F UU)) -->\
b55686a7b22c fixed dots;
wenzelm
parents: 3661
diff changeset
   450
\                        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
   451
 (fn prems =>
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   452
        [
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   453
        (rtac refl 1)
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   454
        ]);
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   455
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   456
(* ------------------------------------------------------------------------ *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   457
(* an admissible formula is also weak admissible                            *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   458
(* ------------------------------------------------------------------------ *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   459
3460
5d71eed16fbe Tuned Franz's proofs.
nipkow
parents: 3326
diff changeset
   460
qed_goalw "adm_impl_admw"  thy [admw_def] "!!P. adm(P)==>admw(P)"
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   461
 (fn prems =>
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   462
        [
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   463
        (strip_tac 1),
3460
5d71eed16fbe Tuned Franz's proofs.
nipkow
parents: 3326
diff changeset
   464
        (etac admD 1),
4720
c1b83b42f65a added not1_or and if_eq_cancel to simpset()
oheimb
parents: 4477
diff changeset
   465
        (rtac chain_iterate 1),
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   466
        (atac 1)
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   467
        ]);
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   468
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   469
(* ------------------------------------------------------------------------ *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   470
(* fixed point induction                                                    *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   471
(* ------------------------------------------------------------------------ *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   472
2640
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch:
slotosch
parents: 2619
diff changeset
   473
qed_goal "fix_ind"  thy  
1168
74be52691d62 The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents: 892
diff changeset
   474
"[| adm(P);P(UU);!!x. P(x) ==> P(F`x)|] ==> P(fix`F)"
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   475
 (fn prems =>
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   476
        [
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   477
        (cut_facts_tac prems 1),
2033
639de962ded4 Ran expandshort; used stac instead of ssubst
paulson
parents: 1992
diff changeset
   478
        (stac fix_def2 1),
3460
5d71eed16fbe Tuned Franz's proofs.
nipkow
parents: 3326
diff changeset
   479
        (etac admD 1),
4720
c1b83b42f65a added not1_or and if_eq_cancel to simpset()
oheimb
parents: 4477
diff changeset
   480
        (rtac chain_iterate 1),
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   481
        (rtac allI 1),
5192
704dd3a6d47d Adapted to new datatype package.
berghofe
parents: 5143
diff changeset
   482
        (induct_tac "i" 1),
2033
639de962ded4 Ran expandshort; used stac instead of ssubst
paulson
parents: 1992
diff changeset
   483
        (stac iterate_0 1),
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   484
        (atac 1),
2033
639de962ded4 Ran expandshort; used stac instead of ssubst
paulson
parents: 1992
diff changeset
   485
        (stac iterate_Suc 1),
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   486
        (resolve_tac prems 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   487
        (atac 1)
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   488
        ]);
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   489
2640
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch:
slotosch
parents: 2619
diff changeset
   490
qed_goal "def_fix_ind" thy "[| f == fix`F; adm(P); \
2568
f86367e104f5 added def_fix_ind and def_wfix_ind for convenience
oheimb
parents: 2566
diff changeset
   491
\       P(UU);!!x. P(x) ==> P(F`x)|] ==> P f" (fn prems => [
f86367e104f5 added def_fix_ind and def_wfix_ind for convenience
oheimb
parents: 2566
diff changeset
   492
        (cut_facts_tac prems 1),
f86367e104f5 added def_fix_ind and def_wfix_ind for convenience
oheimb
parents: 2566
diff changeset
   493
	(asm_simp_tac HOL_ss 1),
f86367e104f5 added def_fix_ind and def_wfix_ind for convenience
oheimb
parents: 2566
diff changeset
   494
	(etac fix_ind 1),
f86367e104f5 added def_fix_ind and def_wfix_ind for convenience
oheimb
parents: 2566
diff changeset
   495
	(atac 1),
f86367e104f5 added def_fix_ind and def_wfix_ind for convenience
oheimb
parents: 2566
diff changeset
   496
	(eresolve_tac prems 1)]);
f86367e104f5 added def_fix_ind and def_wfix_ind for convenience
oheimb
parents: 2566
diff changeset
   497
	
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   498
(* ------------------------------------------------------------------------ *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   499
(* computational induction for weak admissible formulae                     *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   500
(* ------------------------------------------------------------------------ *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   501
2640
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch:
slotosch
parents: 2619
diff changeset
   502
qed_goal "wfix_ind"  thy  
1168
74be52691d62 The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents: 892
diff changeset
   503
"[| admw(P); !n. P(iterate n F UU)|] ==> P(fix`F)"
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   504
 (fn prems =>
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   505
        [
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   506
        (cut_facts_tac prems 1),
2033
639de962ded4 Ran expandshort; used stac instead of ssubst
paulson
parents: 1992
diff changeset
   507
        (stac fix_def2 1),
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   508
        (rtac (admw_def2 RS iffD1 RS spec RS mp) 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   509
        (atac 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   510
        (rtac allI 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   511
        (etac spec 1)
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   512
        ]);
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   513
2640
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch:
slotosch
parents: 2619
diff changeset
   514
qed_goal "def_wfix_ind" thy "[| f == fix`F; admw(P); \
2568
f86367e104f5 added def_fix_ind and def_wfix_ind for convenience
oheimb
parents: 2566
diff changeset
   515
\       !n. P(iterate n F UU) |] ==> P f" (fn prems => [
f86367e104f5 added def_fix_ind and def_wfix_ind for convenience
oheimb
parents: 2566
diff changeset
   516
        (cut_facts_tac prems 1),
f86367e104f5 added def_fix_ind and def_wfix_ind for convenience
oheimb
parents: 2566
diff changeset
   517
	(asm_simp_tac HOL_ss 1),
f86367e104f5 added def_fix_ind and def_wfix_ind for convenience
oheimb
parents: 2566
diff changeset
   518
	(etac wfix_ind 1),
f86367e104f5 added def_fix_ind and def_wfix_ind for convenience
oheimb
parents: 2566
diff changeset
   519
	(atac 1)]);
f86367e104f5 added def_fix_ind and def_wfix_ind for convenience
oheimb
parents: 2566
diff changeset
   520
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   521
(* ------------------------------------------------------------------------ *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   522
(* for chain-finite (easy) types every formula is admissible                *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   523
(* ------------------------------------------------------------------------ *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   524
2640
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch:
slotosch
parents: 2619
diff changeset
   525
qed_goalw "adm_max_in_chain"  thy  [adm_def]
4720
c1b83b42f65a added not1_or and if_eq_cancel to simpset()
oheimb
parents: 4477
diff changeset
   526
"!Y. chain(Y::nat=>'a) --> (? n. max_in_chain n Y) ==> adm(P::'a=>bool)"
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   527
 (fn prems =>
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   528
        [
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   529
        (cut_facts_tac prems 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   530
        (strip_tac 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   531
        (rtac exE 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   532
        (rtac mp 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   533
        (etac spec 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   534
        (atac 1),
2033
639de962ded4 Ran expandshort; used stac instead of ssubst
paulson
parents: 1992
diff changeset
   535
        (stac (lub_finch1 RS thelubI) 1),
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   536
        (atac 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   537
        (atac 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   538
        (etac spec 1)
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   539
        ]);
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   540
4720
c1b83b42f65a added not1_or and if_eq_cancel to simpset()
oheimb
parents: 4477
diff changeset
   541
bind_thm ("adm_chfin" ,chfin RS adm_max_in_chain);
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   542
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   543
(* ------------------------------------------------------------------------ *)
4720
c1b83b42f65a added not1_or and if_eq_cancel to simpset()
oheimb
parents: 4477
diff changeset
   544
(* some lemmata for functions with flat/chfin domain/range types	    *)
2354
b4a1e3306aa0 added theorems
sandnerr
parents: 2275
diff changeset
   545
(* ------------------------------------------------------------------------ *)
b4a1e3306aa0 added theorems
sandnerr
parents: 2275
diff changeset
   546
3324
6b26b886ff69 Eliminated the prediates flat,chfin
slotosch
parents: 3044
diff changeset
   547
qed_goalw "adm_chfindom" thy [adm_def] "adm (%(u::'a::cpo->'b::chfin). P(u`s))"
6b26b886ff69 Eliminated the prediates flat,chfin
slotosch
parents: 3044
diff changeset
   548
    (fn _ => [
2354
b4a1e3306aa0 added theorems
sandnerr
parents: 2275
diff changeset
   549
	strip_tac 1,
5291
5706f0ef1d43 eliminated fabs,fapp.
slotosch
parents: 5192
diff changeset
   550
	dtac chfin_Rep_CFunR 1,
2354
b4a1e3306aa0 added theorems
sandnerr
parents: 2275
diff changeset
   551
	eres_inst_tac [("x","s")] allE 1,
4098
71e05eb27fb6 isatool fixclasimp;
wenzelm
parents: 3842
diff changeset
   552
	fast_tac (HOL_cs addss (simpset() addsimps [chfin])) 1]);
2354
b4a1e3306aa0 added theorems
sandnerr
parents: 2275
diff changeset
   553
3324
6b26b886ff69 Eliminated the prediates flat,chfin
slotosch
parents: 3044
diff changeset
   554
(* adm_flat not needed any more, since it is a special case of adm_chfindom *)
2354
b4a1e3306aa0 added theorems
sandnerr
parents: 2275
diff changeset
   555
1992
0256c8b71ff1 added flat_eq,
oheimb
parents: 1872
diff changeset
   556
(* ------------------------------------------------------------------------ *)
3326
930c9bed5a09 Moved the classes flat chfin from Fix to Pcpo.
slotosch
parents: 3324
diff changeset
   557
(* improved admisibility introduction                                       *)
1992
0256c8b71ff1 added flat_eq,
oheimb
parents: 1872
diff changeset
   558
(* ------------------------------------------------------------------------ *)
0256c8b71ff1 added flat_eq,
oheimb
parents: 1872
diff changeset
   559
3460
5d71eed16fbe Tuned Franz's proofs.
nipkow
parents: 3326
diff changeset
   560
qed_goalw "admI2" thy [adm_def]
4720
c1b83b42f65a added not1_or and if_eq_cancel to simpset()
oheimb
parents: 4477
diff changeset
   561
 "(!!Y. [| chain Y; !i. P (Y i); !i. ? j. i < j & Y i ~= Y j & Y i << Y j |]\
1992
0256c8b71ff1 added flat_eq,
oheimb
parents: 1872
diff changeset
   562
\ ==> P(lub (range Y))) ==> adm P" 
0256c8b71ff1 added flat_eq,
oheimb
parents: 1872
diff changeset
   563
 (fn prems => [
2033
639de962ded4 Ran expandshort; used stac instead of ssubst
paulson
parents: 1992
diff changeset
   564
        strip_tac 1,
639de962ded4 Ran expandshort; used stac instead of ssubst
paulson
parents: 1992
diff changeset
   565
        etac increasing_chain_adm_lemma 1, atac 1,
639de962ded4 Ran expandshort; used stac instead of ssubst
paulson
parents: 1992
diff changeset
   566
        eresolve_tac prems 1, atac 1, atac 1]);
1992
0256c8b71ff1 added flat_eq,
oheimb
parents: 1872
diff changeset
   567
0256c8b71ff1 added flat_eq,
oheimb
parents: 1872
diff changeset
   568
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   569
(* ------------------------------------------------------------------------ *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   570
(* admissibility of special formulae and propagation                        *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   571
(* ------------------------------------------------------------------------ *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   572
2640
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch:
slotosch
parents: 2619
diff changeset
   573
qed_goalw "adm_less"  thy [adm_def]
3842
b55686a7b22c fixed dots;
wenzelm
parents: 3661
diff changeset
   574
        "[|cont u;cont v|]==> adm(%x. u x << v x)"
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   575
 (fn prems =>
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   576
        [
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   577
        (cut_facts_tac prems 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   578
        (strip_tac 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   579
        (etac (cont2contlub RS contlubE RS spec RS mp RS ssubst) 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   580
        (atac 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   581
        (etac (cont2contlub RS contlubE RS spec RS mp RS ssubst) 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   582
        (atac 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   583
        (rtac lub_mono 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   584
        (cut_facts_tac prems 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   585
        (etac (cont2mono RS ch2ch_monofun) 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   586
        (atac 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   587
        (cut_facts_tac prems 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   588
        (etac (cont2mono RS ch2ch_monofun) 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   589
        (atac 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   590
        (atac 1)
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   591
        ]);
3460
5d71eed16fbe Tuned Franz's proofs.
nipkow
parents: 3326
diff changeset
   592
Addsimps [adm_less];
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   593
2640
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch:
slotosch
parents: 2619
diff changeset
   594
qed_goal "adm_conj"  thy  
3460
5d71eed16fbe Tuned Franz's proofs.
nipkow
parents: 3326
diff changeset
   595
        "!!P. [| adm P; adm Q |] ==> adm(%x. P x & Q x)"
5d71eed16fbe Tuned Franz's proofs.
nipkow
parents: 3326
diff changeset
   596
 (fn prems => [fast_tac (HOL_cs addEs [admD] addIs [admI]) 1]);
5d71eed16fbe Tuned Franz's proofs.
nipkow
parents: 3326
diff changeset
   597
Addsimps [adm_conj];
5d71eed16fbe Tuned Franz's proofs.
nipkow
parents: 3326
diff changeset
   598
3842
b55686a7b22c fixed dots;
wenzelm
parents: 3661
diff changeset
   599
qed_goalw "adm_not_free"  thy [adm_def] "adm(%x. t)"
3460
5d71eed16fbe Tuned Franz's proofs.
nipkow
parents: 3326
diff changeset
   600
 (fn prems => [fast_tac HOL_cs 1]);
5d71eed16fbe Tuned Franz's proofs.
nipkow
parents: 3326
diff changeset
   601
Addsimps [adm_not_free];
5d71eed16fbe Tuned Franz's proofs.
nipkow
parents: 3326
diff changeset
   602
5d71eed16fbe Tuned Franz's proofs.
nipkow
parents: 3326
diff changeset
   603
qed_goalw "adm_not_less"  thy [adm_def]
5d71eed16fbe Tuned Franz's proofs.
nipkow
parents: 3326
diff changeset
   604
        "!!t. cont t ==> adm(%x.~ (t x) << u)"
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   605
 (fn prems =>
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   606
        [
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   607
        (strip_tac 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   608
        (rtac contrapos 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   609
        (etac spec 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   610
        (rtac trans_less 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   611
        (atac 2),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   612
        (etac (cont2mono RS monofun_fun_arg) 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   613
        (rtac is_ub_thelub 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   614
        (atac 1)
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   615
        ]);
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   616
3460
5d71eed16fbe Tuned Franz's proofs.
nipkow
parents: 3326
diff changeset
   617
qed_goal "adm_all" thy  
3842
b55686a7b22c fixed dots;
wenzelm
parents: 3661
diff changeset
   618
        "!!P. !y. adm(P y) ==> adm(%x.!y. P y x)"
3460
5d71eed16fbe Tuned Franz's proofs.
nipkow
parents: 3326
diff changeset
   619
 (fn prems => [fast_tac (HOL_cs addIs [admI] addEs [admD]) 1]);
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   620
1779
1155c06fa956 introduced forgotten bind_thm calls
oheimb
parents: 1681
diff changeset
   621
bind_thm ("adm_all2", allI RS adm_all);
625
119391dd1d59 New version
nipkow
parents: 442
diff changeset
   622
2640
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch:
slotosch
parents: 2619
diff changeset
   623
qed_goal "adm_subst"  thy  
3460
5d71eed16fbe Tuned Franz's proofs.
nipkow
parents: 3326
diff changeset
   624
        "!!P. [|cont t; adm P|] ==> adm(%x. P (t x))"
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   625
 (fn prems =>
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   626
        [
3460
5d71eed16fbe Tuned Franz's proofs.
nipkow
parents: 3326
diff changeset
   627
        (rtac admI 1),
2033
639de962ded4 Ran expandshort; used stac instead of ssubst
paulson
parents: 1992
diff changeset
   628
        (stac (cont2contlub RS contlubE RS spec RS mp) 1),
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   629
        (atac 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   630
        (atac 1),
3460
5d71eed16fbe Tuned Franz's proofs.
nipkow
parents: 3326
diff changeset
   631
        (etac admD 1),
5d71eed16fbe Tuned Franz's proofs.
nipkow
parents: 3326
diff changeset
   632
        (etac (cont2mono RS ch2ch_monofun) 1),
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   633
        (atac 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   634
        (atac 1)
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   635
        ]);
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   636
2640
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch:
slotosch
parents: 2619
diff changeset
   637
qed_goal "adm_UU_not_less"  thy "adm(%x.~ UU << t(x))"
3460
5d71eed16fbe Tuned Franz's proofs.
nipkow
parents: 3326
diff changeset
   638
 (fn prems => [Simp_tac 1]);
5d71eed16fbe Tuned Franz's proofs.
nipkow
parents: 3326
diff changeset
   639
5d71eed16fbe Tuned Franz's proofs.
nipkow
parents: 3326
diff changeset
   640
qed_goalw "adm_not_UU"  thy [adm_def] 
5d71eed16fbe Tuned Franz's proofs.
nipkow
parents: 3326
diff changeset
   641
        "!!t. cont(t)==> adm(%x.~ (t x) = UU)"
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   642
 (fn prems =>
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   643
        [
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   644
        (strip_tac 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   645
        (rtac contrapos 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   646
        (etac spec 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   647
        (rtac (chain_UU_I RS spec) 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   648
        (rtac (cont2mono RS ch2ch_monofun) 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   649
        (atac 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   650
        (atac 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   651
        (rtac (cont2contlub RS contlubE RS spec RS mp RS subst) 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   652
        (atac 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   653
        (atac 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   654
        (atac 1)
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   655
        ]);
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   656
2640
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch:
slotosch
parents: 2619
diff changeset
   657
qed_goal "adm_eq"  thy 
3460
5d71eed16fbe Tuned Franz's proofs.
nipkow
parents: 3326
diff changeset
   658
        "!!u. [|cont u ; cont v|]==> adm(%x. u x = v x)"
4098
71e05eb27fb6 isatool fixclasimp;
wenzelm
parents: 3842
diff changeset
   659
 (fn prems => [asm_simp_tac (simpset() addsimps [po_eq_conv]) 1]);
3460
5d71eed16fbe Tuned Franz's proofs.
nipkow
parents: 3326
diff changeset
   660
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   661
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   662
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   663
(* ------------------------------------------------------------------------ *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   664
(* admissibility for disjunction is hard to prove. It takes 10 Lemmas       *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   665
(* ------------------------------------------------------------------------ *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   666
1992
0256c8b71ff1 added flat_eq,
oheimb
parents: 1872
diff changeset
   667
local
0256c8b71ff1 added flat_eq,
oheimb
parents: 1872
diff changeset
   668
2619
3fd774ee405a Modified and shortened adm_disj lemmas.
nipkow
parents: 2568
diff changeset
   669
  val adm_disj_lemma1 = prove_goal HOL.thy 
3842
b55686a7b22c fixed dots;
wenzelm
parents: 3661
diff changeset
   670
  "!n. P(Y n)|Q(Y n) ==> (? i.!j. R i j --> Q(Y(j))) | (!i.? j. R i j & P(Y(j)))"
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   671
 (fn prems =>
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   672
        [
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   673
        (cut_facts_tac prems 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   674
        (fast_tac HOL_cs 1)
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   675
        ]);
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   676
2640
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch:
slotosch
parents: 2619
diff changeset
   677
  val adm_disj_lemma2 = prove_goal thy  
4720
c1b83b42f65a added not1_or and if_eq_cancel to simpset()
oheimb
parents: 4477
diff changeset
   678
  "!!Q. [| adm(Q); ? X. chain(X) & (!n. Q(X(n))) &\
1992
0256c8b71ff1 added flat_eq,
oheimb
parents: 1872
diff changeset
   679
  \   lub(range(Y))=lub(range(X))|] ==> Q(lub(range(Y)))"
4098
71e05eb27fb6 isatool fixclasimp;
wenzelm
parents: 3842
diff changeset
   680
 (fn _ => [fast_tac (claset() addEs [admD] addss simpset()) 1]);
2619
3fd774ee405a Modified and shortened adm_disj lemmas.
nipkow
parents: 2568
diff changeset
   681
4720
c1b83b42f65a added not1_or and if_eq_cancel to simpset()
oheimb
parents: 4477
diff changeset
   682
  val adm_disj_lemma3 = prove_goalw thy [chain]
c1b83b42f65a added not1_or and if_eq_cancel to simpset()
oheimb
parents: 4477
diff changeset
   683
  "!!Q. chain(Y) ==> chain(%m. if m < Suc i then Y(Suc i) else Y m)"
2619
3fd774ee405a Modified and shortened adm_disj lemmas.
nipkow
parents: 2568
diff changeset
   684
 (fn _ =>
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   685
        [
4833
2e53109d4bc8 Renamed expand_const -> split_const
nipkow
parents: 4720
diff changeset
   686
        Asm_simp_tac 1,
2619
3fd774ee405a Modified and shortened adm_disj lemmas.
nipkow
parents: 2568
diff changeset
   687
        safe_tac HOL_cs,
3fd774ee405a Modified and shortened adm_disj lemmas.
nipkow
parents: 2568
diff changeset
   688
        subgoal_tac "ia = i" 1,
5984
4c2fc177f4d3 *** empty log message ***
nipkow
parents: 5656
diff changeset
   689
        ALLGOALS Asm_simp_tac
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   690
        ]);
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   691
2619
3fd774ee405a Modified and shortened adm_disj lemmas.
nipkow
parents: 2568
diff changeset
   692
  val adm_disj_lemma4 = prove_goal Nat.thy
3fd774ee405a Modified and shortened adm_disj lemmas.
nipkow
parents: 2568
diff changeset
   693
  "!!Q. !j. i < j --> Q(Y(j))  ==> !n. Q( if n < Suc i then Y(Suc i) else Y n)"
3fd774ee405a Modified and shortened adm_disj lemmas.
nipkow
parents: 2568
diff changeset
   694
 (fn _ =>
5656
f8389824189b Mods because trans_tac is now part of thge simplifier.
nipkow
parents: 5291
diff changeset
   695
        [Asm_simp_tac 1]);
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   696
2640
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch:
slotosch
parents: 2619
diff changeset
   697
  val adm_disj_lemma5 = prove_goal thy
4720
c1b83b42f65a added not1_or and if_eq_cancel to simpset()
oheimb
parents: 4477
diff changeset
   698
  "!!Y::nat=>'a::cpo. [| chain(Y); ! j. i < j --> Q(Y(j)) |] ==>\
1992
0256c8b71ff1 added flat_eq,
oheimb
parents: 1872
diff changeset
   699
  \       lub(range(Y)) = lub(range(%m. if m< Suc(i) then Y(Suc(i)) else Y m))"
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   700
 (fn prems =>
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   701
        [
2619
3fd774ee405a Modified and shortened adm_disj lemmas.
nipkow
parents: 2568
diff changeset
   702
        safe_tac (HOL_cs addSIs [lub_equal2,adm_disj_lemma3]),
2764
d56b5df57d73 added atac 2 (again);
wenzelm
parents: 2749
diff changeset
   703
        atac 2,
4833
2e53109d4bc8 Renamed expand_const -> split_const
nipkow
parents: 4720
diff changeset
   704
        Asm_simp_tac 1,
2619
3fd774ee405a Modified and shortened adm_disj lemmas.
nipkow
parents: 2568
diff changeset
   705
        res_inst_tac [("x","i")] exI 1,
3fd774ee405a Modified and shortened adm_disj lemmas.
nipkow
parents: 2568
diff changeset
   706
        strip_tac 1,
5984
4c2fc177f4d3 *** empty log message ***
nipkow
parents: 5656
diff changeset
   707
        Simp_tac 1
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   708
        ]);
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   709
2640
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch:
slotosch
parents: 2619
diff changeset
   710
  val adm_disj_lemma6 = prove_goal thy
4720
c1b83b42f65a added not1_or and if_eq_cancel to simpset()
oheimb
parents: 4477
diff changeset
   711
  "[| chain(Y::nat=>'a::cpo); ? i. ! j. i < j --> Q(Y(j)) |] ==>\
c1b83b42f65a added not1_or and if_eq_cancel to simpset()
oheimb
parents: 4477
diff changeset
   712
  \         ? X. chain(X) & (! n. Q(X(n))) & lub(range(Y)) = lub(range(X))"
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   713
 (fn prems =>
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   714
        [
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   715
        (cut_facts_tac prems 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   716
        (etac exE 1),
3842
b55686a7b22c fixed dots;
wenzelm
parents: 3661
diff changeset
   717
        (res_inst_tac [("x","%m. if m<Suc(i) then Y(Suc(i)) else Y m")] exI 1),
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   718
        (rtac conjI 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   719
        (rtac adm_disj_lemma3 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   720
        (atac 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   721
        (rtac conjI 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   722
        (rtac adm_disj_lemma4 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   723
        (atac 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   724
        (rtac adm_disj_lemma5 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   725
        (atac 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   726
        (atac 1)
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   727
        ]);
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   728
2640
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch:
slotosch
parents: 2619
diff changeset
   729
  val adm_disj_lemma7 = prove_goal thy 
4720
c1b83b42f65a added not1_or and if_eq_cancel to simpset()
oheimb
parents: 4477
diff changeset
   730
  "[| chain(Y::nat=>'a::cpo); ! i. ? j. i < j & P(Y(j))  |] ==>\
c1b83b42f65a added not1_or and if_eq_cancel to simpset()
oheimb
parents: 4477
diff changeset
   731
  \         chain(%m. Y(Least(%j. m<j & P(Y(j)))))"
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   732
 (fn prems =>
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   733
        [
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   734
        (cut_facts_tac prems 1),
4720
c1b83b42f65a added not1_or and if_eq_cancel to simpset()
oheimb
parents: 4477
diff changeset
   735
        (rtac chainI 1),
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   736
        (rtac allI 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   737
        (rtac chain_mono3 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   738
        (atac 1),
1675
36ba4da350c3 adapted several proofs
oheimb
parents: 1461
diff changeset
   739
        (rtac Least_le 1),
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   740
        (rtac conjI 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   741
        (rtac Suc_lessD 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   742
        (etac allE 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   743
        (etac exE 1),
1675
36ba4da350c3 adapted several proofs
oheimb
parents: 1461
diff changeset
   744
        (rtac (LeastI RS conjunct1) 1),
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   745
        (atac 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   746
        (etac allE 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   747
        (etac exE 1),
1675
36ba4da350c3 adapted several proofs
oheimb
parents: 1461
diff changeset
   748
        (rtac (LeastI RS conjunct2) 1),
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   749
        (atac 1)
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   750
        ]);
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   751
2640
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch:
slotosch
parents: 2619
diff changeset
   752
  val adm_disj_lemma8 = prove_goal thy 
2619
3fd774ee405a Modified and shortened adm_disj lemmas.
nipkow
parents: 2568
diff changeset
   753
  "[| ! i. ? j. i < j & P(Y(j)) |] ==> ! m. P(Y(LEAST j::nat. m<j & P(Y(j))))"
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   754
 (fn prems =>
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   755
        [
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   756
        (cut_facts_tac prems 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   757
        (strip_tac 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   758
        (etac allE 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   759
        (etac exE 1),
1675
36ba4da350c3 adapted several proofs
oheimb
parents: 1461
diff changeset
   760
        (etac (LeastI RS conjunct2) 1)
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   761
        ]);
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   762
2640
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch:
slotosch
parents: 2619
diff changeset
   763
  val adm_disj_lemma9 = prove_goal thy
4720
c1b83b42f65a added not1_or and if_eq_cancel to simpset()
oheimb
parents: 4477
diff changeset
   764
  "[| chain(Y::nat=>'a::cpo); ! i. ? j. i < j & P(Y(j)) |] ==>\
1992
0256c8b71ff1 added flat_eq,
oheimb
parents: 1872
diff changeset
   765
  \         lub(range(Y)) = lub(range(%m. Y(Least(%j. m<j & P(Y(j))))))"
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   766
 (fn prems =>
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   767
        [
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   768
        (cut_facts_tac prems 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   769
        (rtac antisym_less 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   770
        (rtac lub_mono 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   771
        (atac 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   772
        (rtac adm_disj_lemma7 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   773
        (atac 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   774
        (atac 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   775
        (strip_tac 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   776
        (rtac (chain_mono RS mp) 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   777
        (atac 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   778
        (etac allE 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   779
        (etac exE 1),
1675
36ba4da350c3 adapted several proofs
oheimb
parents: 1461
diff changeset
   780
        (rtac (LeastI RS conjunct1) 1),
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   781
        (atac 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   782
        (rtac lub_mono3 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   783
        (rtac adm_disj_lemma7 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   784
        (atac 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   785
        (atac 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   786
        (atac 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   787
        (strip_tac 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   788
        (rtac exI 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   789
        (rtac (chain_mono RS mp) 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   790
        (atac 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   791
        (rtac lessI 1)
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   792
        ]);
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   793
2640
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch:
slotosch
parents: 2619
diff changeset
   794
  val adm_disj_lemma10 = prove_goal thy
4720
c1b83b42f65a added not1_or and if_eq_cancel to simpset()
oheimb
parents: 4477
diff changeset
   795
  "[| chain(Y::nat=>'a::cpo); ! i. ? j. i < j & P(Y(j)) |] ==>\
c1b83b42f65a added not1_or and if_eq_cancel to simpset()
oheimb
parents: 4477
diff changeset
   796
  \         ? X. chain(X) & (! n. P(X(n))) & lub(range(Y)) = lub(range(X))"
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   797
 (fn prems =>
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   798
        [
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   799
        (cut_facts_tac prems 1),
1675
36ba4da350c3 adapted several proofs
oheimb
parents: 1461
diff changeset
   800
        (res_inst_tac [("x","%m. Y(Least(%j. m<j & P(Y(j))))")] exI 1),
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   801
        (rtac conjI 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   802
        (rtac adm_disj_lemma7 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   803
        (atac 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   804
        (atac 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   805
        (rtac conjI 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   806
        (rtac adm_disj_lemma8 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   807
        (atac 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   808
        (rtac adm_disj_lemma9 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   809
        (atac 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   810
        (atac 1)
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   811
        ]);
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   812
2640
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch:
slotosch
parents: 2619
diff changeset
   813
  val adm_disj_lemma12 = prove_goal thy
4720
c1b83b42f65a added not1_or and if_eq_cancel to simpset()
oheimb
parents: 4477
diff changeset
   814
  "[| adm(P); chain(Y);? i. ! j. i < j --> P(Y(j))|]==>P(lub(range(Y)))"
1992
0256c8b71ff1 added flat_eq,
oheimb
parents: 1872
diff changeset
   815
 (fn prems =>
0256c8b71ff1 added flat_eq,
oheimb
parents: 1872
diff changeset
   816
        [
0256c8b71ff1 added flat_eq,
oheimb
parents: 1872
diff changeset
   817
        (cut_facts_tac prems 1),
0256c8b71ff1 added flat_eq,
oheimb
parents: 1872
diff changeset
   818
        (etac adm_disj_lemma2 1),
0256c8b71ff1 added flat_eq,
oheimb
parents: 1872
diff changeset
   819
        (etac adm_disj_lemma6 1),
0256c8b71ff1 added flat_eq,
oheimb
parents: 1872
diff changeset
   820
        (atac 1)
0256c8b71ff1 added flat_eq,
oheimb
parents: 1872
diff changeset
   821
        ]);
430
89e1986125fe Franz Regensburger's changes.
nipkow
parents: 300
diff changeset
   822
1992
0256c8b71ff1 added flat_eq,
oheimb
parents: 1872
diff changeset
   823
in
0256c8b71ff1 added flat_eq,
oheimb
parents: 1872
diff changeset
   824
2640
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch:
slotosch
parents: 2619
diff changeset
   825
val adm_lemma11 = prove_goal thy
4720
c1b83b42f65a added not1_or and if_eq_cancel to simpset()
oheimb
parents: 4477
diff changeset
   826
"[| adm(P); chain(Y); ! i. ? j. i < j & P(Y(j)) |]==>P(lub(range(Y)))"
430
89e1986125fe Franz Regensburger's changes.
nipkow
parents: 300
diff changeset
   827
 (fn prems =>
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   828
        [
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   829
        (cut_facts_tac prems 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   830
        (etac adm_disj_lemma2 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   831
        (etac adm_disj_lemma10 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   832
        (atac 1)
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   833
        ]);
430
89e1986125fe Franz Regensburger's changes.
nipkow
parents: 300
diff changeset
   834
2640
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch:
slotosch
parents: 2619
diff changeset
   835
val adm_disj = prove_goal thy  
3842
b55686a7b22c fixed dots;
wenzelm
parents: 3661
diff changeset
   836
        "!!P. [| adm P; adm Q |] ==> adm(%x. P x | Q x)"
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   837
 (fn prems =>
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   838
        [
3460
5d71eed16fbe Tuned Franz's proofs.
nipkow
parents: 3326
diff changeset
   839
        (rtac admI 1),
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   840
        (rtac (adm_disj_lemma1 RS disjE) 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   841
        (atac 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   842
        (rtac disjI2 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   843
        (etac adm_disj_lemma12 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   844
        (atac 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   845
        (atac 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   846
        (rtac disjI1 1),
1992
0256c8b71ff1 added flat_eq,
oheimb
parents: 1872
diff changeset
   847
        (etac adm_lemma11 1),
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   848
        (atac 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   849
        (atac 1)
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   850
        ]);
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   851
1992
0256c8b71ff1 added flat_eq,
oheimb
parents: 1872
diff changeset
   852
end;
0256c8b71ff1 added flat_eq,
oheimb
parents: 1872
diff changeset
   853
0256c8b71ff1 added flat_eq,
oheimb
parents: 1872
diff changeset
   854
bind_thm("adm_lemma11",adm_lemma11);
0256c8b71ff1 added flat_eq,
oheimb
parents: 1872
diff changeset
   855
bind_thm("adm_disj",adm_disj);
430
89e1986125fe Franz Regensburger's changes.
nipkow
parents: 300
diff changeset
   856
2640
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch:
slotosch
parents: 2619
diff changeset
   857
qed_goal "adm_imp"  thy  
4720
c1b83b42f65a added not1_or and if_eq_cancel to simpset()
oheimb
parents: 4477
diff changeset
   858
        "!!P. [| adm(%x.~(P x)); adm Q |] ==> adm(%x. P x --> Q x)" (K [
3842
b55686a7b22c fixed dots;
wenzelm
parents: 3661
diff changeset
   859
        (subgoal_tac "(%x. P x --> Q x) = (%x. ~P x | Q x)" 1),
4720
c1b83b42f65a added not1_or and if_eq_cancel to simpset()
oheimb
parents: 4477
diff changeset
   860
         (etac ssubst 1),
3652
4c484f03079c added case_prover
oheimb
parents: 3460
diff changeset
   861
         (etac adm_disj 1),
4c484f03079c added case_prover
oheimb
parents: 3460
diff changeset
   862
         (atac 1),
4720
c1b83b42f65a added not1_or and if_eq_cancel to simpset()
oheimb
parents: 4477
diff changeset
   863
        (Simp_tac 1)
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   864
        ]);
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   865
5143
b94cd208f073 Removal of leading "\!\!..." from most Goal commands
paulson
parents: 5068
diff changeset
   866
Goal "[| adm (%x. P x --> Q x); adm (%x. Q x --> P x) |] \
3460
5d71eed16fbe Tuned Franz's proofs.
nipkow
parents: 3326
diff changeset
   867
\           ==> adm (%x. P x = Q x)";
4423
a129b817b58a expandshort;
wenzelm
parents: 4098
diff changeset
   868
by (subgoal_tac "(%x. P x = Q x) = (%x. (P x --> Q x) & (Q x --> P x))" 1);
3460
5d71eed16fbe Tuned Franz's proofs.
nipkow
parents: 3326
diff changeset
   869
by (Asm_simp_tac 1);
5d71eed16fbe Tuned Franz's proofs.
nipkow
parents: 3326
diff changeset
   870
by (rtac ext 1);
5d71eed16fbe Tuned Franz's proofs.
nipkow
parents: 3326
diff changeset
   871
by (fast_tac HOL_cs 1);
5d71eed16fbe Tuned Franz's proofs.
nipkow
parents: 3326
diff changeset
   872
qed"adm_iff";
5d71eed16fbe Tuned Franz's proofs.
nipkow
parents: 3326
diff changeset
   873
5d71eed16fbe Tuned Franz's proofs.
nipkow
parents: 3326
diff changeset
   874
2640
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch:
slotosch
parents: 2619
diff changeset
   875
qed_goal "adm_not_conj"  thy  
1681
d9aaae4ff6c3 changed two goals formulated with 8bit font
oheimb
parents: 1675
diff changeset
   876
"[| adm (%x. ~ P x); adm (%x. ~ Q x) |] ==> adm (%x. ~ (P x & Q x))"(fn prems=>[
2033
639de962ded4 Ran expandshort; used stac instead of ssubst
paulson
parents: 1992
diff changeset
   877
        cut_facts_tac prems 1,
639de962ded4 Ran expandshort; used stac instead of ssubst
paulson
parents: 1992
diff changeset
   878
        subgoal_tac 
639de962ded4 Ran expandshort; used stac instead of ssubst
paulson
parents: 1992
diff changeset
   879
        "(%x. ~ (P x & Q x)) = (%x. ~ P x | ~ Q x)" 1,
639de962ded4 Ran expandshort; used stac instead of ssubst
paulson
parents: 1992
diff changeset
   880
        rtac ext 2,
639de962ded4 Ran expandshort; used stac instead of ssubst
paulson
parents: 1992
diff changeset
   881
        fast_tac HOL_cs 2,
639de962ded4 Ran expandshort; used stac instead of ssubst
paulson
parents: 1992
diff changeset
   882
        etac ssubst 1,
639de962ded4 Ran expandshort; used stac instead of ssubst
paulson
parents: 1992
diff changeset
   883
        etac adm_disj 1,
639de962ded4 Ran expandshort; used stac instead of ssubst
paulson
parents: 1992
diff changeset
   884
        atac 1]);
1675
36ba4da350c3 adapted several proofs
oheimb
parents: 1461
diff changeset
   885
2566
cbf02fc74332 changed handling of cont_lemmas and adm_lemmas
oheimb
parents: 2354
diff changeset
   886
val adm_lemmas = [adm_imp,adm_disj,adm_eq,adm_not_UU,adm_UU_not_less,
3460
5d71eed16fbe Tuned Franz's proofs.
nipkow
parents: 3326
diff changeset
   887
        adm_all2,adm_not_less,adm_not_free,adm_not_conj,adm_conj,adm_less,
5d71eed16fbe Tuned Franz's proofs.
nipkow
parents: 3326
diff changeset
   888
        adm_iff];
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   889
2566
cbf02fc74332 changed handling of cont_lemmas and adm_lemmas
oheimb
parents: 2354
diff changeset
   890
Addsimps adm_lemmas;