src/HOLCF/Fix.ML
author nipkow
Sun, 22 Dec 2002 10:43:43 +0100
changeset 13763 f94b569cd610
parent 13524 604d0f3622d6
child 14981 e73f8140af78
permissions -rw-r--r--
added print translations tha avoid eta contraction for important binders.
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
12030
wenzelm
parents: 11346
diff changeset
     4
    License:    GPL (GNU GENERAL PUBLIC LICENSE)
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
     5
9245
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
     6
fixed point operator and admissibility
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
(* ------------------------------------------------------------------------ *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    10
(* derive inductive properties of iterate from primitive recursion          *)
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
10834
a7897aebbffc *** empty log message ***
nipkow
parents: 10230
diff changeset
    13
Goal "iterate (Suc n) F x = iterate n F (F$x)";
9245
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
    14
by (induct_tac "n" 1);
9248
e1dee89de037 massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents: 9245
diff changeset
    15
by Auto_tac;  
9245
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
    16
qed "iterate_Suc2";
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    17
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    18
(* ------------------------------------------------------------------------ *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    19
(* the sequence of function itertaions is a chain                           *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    20
(* 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
    21
(* ------------------------------------------------------------------------ *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    22
11346
0d28bc664955 corrected ML names of definitions
oheimb
parents: 10834
diff changeset
    23
Goalw [chain_def]  "x << F$x ==> chain (%i. iterate i F x)";
9245
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
    24
by (strip_tac 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
    25
by (induct_tac "i" 1);
9248
e1dee89de037 massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents: 9245
diff changeset
    26
by Auto_tac;  
9245
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
    27
by (etac monofun_cfun_arg 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
    28
qed "chain_iterate2";
243
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
11346
0d28bc664955 corrected ML names of definitions
oheimb
parents: 10834
diff changeset
    31
Goal "chain (%i. iterate i F UU)";
9245
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
    32
by (rtac chain_iterate2 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
    33
by (rtac minimal 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
    34
qed "chain_iterate";
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    35
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    36
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    37
(* ------------------------------------------------------------------------ *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    38
(* 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
    39
(* omega cpo's                                                              *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    40
(* ------------------------------------------------------------------------ *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    41
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    42
10834
a7897aebbffc *** empty log message ***
nipkow
parents: 10230
diff changeset
    43
Goalw [Ifix_def] "Ifix F =F$(Ifix F)";
9245
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
    44
by (stac contlub_cfun_arg 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
    45
by (rtac chain_iterate 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
    46
by (rtac antisym_less 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
    47
by (rtac lub_mono 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
    48
by (rtac chain_iterate 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
    49
by (rtac ch2ch_Rep_CFunR 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
    50
by (rtac chain_iterate 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
    51
by (rtac allI 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
    52
by (rtac (iterate_Suc RS subst) 1);
9248
e1dee89de037 massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents: 9245
diff changeset
    53
by (rtac (chain_iterate RS chainE) 1);
9245
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
    54
by (rtac is_lub_thelub 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
    55
by (rtac ch2ch_Rep_CFunR 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
    56
by (rtac chain_iterate 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
    57
by (rtac ub_rangeI 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
    58
by (rtac (iterate_Suc RS subst) 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
    59
by (rtac is_ub_thelub 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
    60
by (rtac chain_iterate 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
    61
qed "Ifix_eq";
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    62
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    63
10834
a7897aebbffc *** empty log message ***
nipkow
parents: 10230
diff changeset
    64
Goalw [Ifix_def] "F$x=x ==> Ifix(F) << x";
9245
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
    65
by (rtac is_lub_thelub 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
    66
by (rtac chain_iterate 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
    67
by (rtac ub_rangeI 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
    68
by (strip_tac 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
    69
by (induct_tac "i" 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
    70
by (Asm_simp_tac 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
    71
by (Asm_simp_tac 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
    72
by (res_inst_tac [("t","x")] subst 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
    73
by (atac 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
    74
by (etac monofun_cfun_arg 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
    75
qed "Ifix_least";
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    76
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    77
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    78
(* ------------------------------------------------------------------------ *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    79
(* monotonicity and continuity of iterate                                   *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    80
(* ------------------------------------------------------------------------ *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    81
9245
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
    82
Goalw [monofun] "monofun(iterate(i))";
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
    83
by (strip_tac 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
    84
by (induct_tac "i" 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
    85
by (Asm_simp_tac 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
    86
by (asm_full_simp_tac (simpset() addsimps [less_fun, monofun_cfun]) 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
    87
qed "monofun_iterate";
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    88
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    89
(* ------------------------------------------------------------------------ *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    90
(* 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
    91
(* diagonalisation lemma for continuous functions with two arguments.       *)
5291
5706f0ef1d43 eliminated fabs,fapp.
slotosch
parents: 5192
diff changeset
    92
(* 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
    93
(* ------------------------------------------------------------------------ *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    94
9248
e1dee89de037 massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents: 9245
diff changeset
    95
Goalw [contlub] "contlub(iterate(i))";
9245
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
    96
by (strip_tac 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
    97
by (induct_tac "i" 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
    98
by (Asm_simp_tac 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
    99
by (rtac (lub_const RS thelubI RS sym) 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   100
by (asm_simp_tac (simpset() delsimps [range_composition]) 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   101
by (rtac ext 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   102
by (stac thelub_fun 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   103
by (rtac chainI 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   104
by (rtac (less_fun RS iffD2) 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   105
by (rtac allI 1);
9248
e1dee89de037 massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents: 9245
diff changeset
   106
by (rtac (chainE) 1);
9245
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   107
by (rtac (monofun_Rep_CFun1 RS ch2ch_MF2LR) 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   108
by (rtac allI 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   109
by (rtac monofun_Rep_CFun2 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   110
by (atac 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   111
by (rtac ch2ch_fun 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   112
by (rtac (monofun_iterate RS ch2ch_monofun) 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   113
by (atac 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   114
by (stac thelub_fun 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   115
by (rtac (monofun_iterate RS ch2ch_monofun) 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   116
by (atac 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   117
by (rtac contlub_cfun  1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   118
by (atac 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   119
by (etac (monofun_iterate RS ch2ch_monofun RS ch2ch_fun) 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   120
qed "contlub_iterate";
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   121
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   122
9248
e1dee89de037 massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents: 9245
diff changeset
   123
Goal "cont(iterate(i))";
9245
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   124
by (rtac monocontlub2cont 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   125
by (rtac monofun_iterate 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   126
by (rtac contlub_iterate 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   127
qed "cont_iterate";
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   128
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   129
(* ------------------------------------------------------------------------ *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   130
(* 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
   131
(* ------------------------------------------------------------------------ *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   132
9248
e1dee89de037 massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents: 9245
diff changeset
   133
Goal "monofun(iterate n F)";
9245
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   134
by (rtac monofunI 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   135
by (strip_tac 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   136
by (induct_tac "n" 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   137
by (Asm_simp_tac 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   138
by (Asm_simp_tac 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   139
by (etac monofun_cfun_arg 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   140
qed "monofun_iterate2";
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   141
9245
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   142
Goal "contlub(iterate n F)";
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   143
by (rtac contlubI 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   144
by (strip_tac 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   145
by (induct_tac "n" 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   146
by (Simp_tac 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   147
by (Simp_tac 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   148
by (res_inst_tac [("t","iterate n F (lub(range(%u. Y u)))"),
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   149
                  ("s","lub(range(%i. iterate n F (Y i)))")] ssubst 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   150
by (atac 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   151
by (rtac contlub_cfun_arg 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   152
by (etac (monofun_iterate2 RS ch2ch_monofun) 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   153
qed "contlub_iterate2";
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   154
9248
e1dee89de037 massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents: 9245
diff changeset
   155
Goal "cont (iterate n F)";
9245
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   156
by (rtac monocontlub2cont 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   157
by (rtac monofun_iterate2 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   158
by (rtac contlub_iterate2 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   159
qed "cont_iterate2";
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   160
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   161
(* ------------------------------------------------------------------------ *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   162
(* monotonicity and continuity of Ifix                                      *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   163
(* ------------------------------------------------------------------------ *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   164
9245
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   165
Goalw [monofun,Ifix_def] "monofun(Ifix)";
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   166
by (strip_tac 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   167
by (rtac lub_mono 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   168
by (rtac chain_iterate 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   169
by (rtac chain_iterate 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   170
by (rtac allI 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   171
by (rtac (less_fun RS iffD1 RS spec) 1 THEN
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   172
    etac (monofun_iterate RS monofunE RS spec RS spec RS mp) 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   173
qed "monofun_Ifix";
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   174
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   175
(* ------------------------------------------------------------------------ *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   176
(* 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
   177
(* be derived for lubs in this argument                                     *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   178
(* ------------------------------------------------------------------------ *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   179
9248
e1dee89de037 massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents: 9245
diff changeset
   180
Goal   
9245
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   181
"chain(Y) ==> chain(%i. lub(range(%ia. iterate ia (Y i) UU)))";
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   182
by (rtac chainI 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   183
by (strip_tac 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   184
by (rtac lub_mono 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   185
by (rtac chain_iterate 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   186
by (rtac chain_iterate 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   187
by (strip_tac 1);
9248
e1dee89de037 massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents: 9245
diff changeset
   188
by (etac (monofun_iterate RS ch2ch_monofun RS ch2ch_fun RS chainE) 1);
9245
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   189
qed "chain_iterate_lub";
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   190
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   191
(* ------------------------------------------------------------------------ *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   192
(* 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
   193
(* 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
   194
(* 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
   195
(* ------------------------------------------------------------------------ *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   196
9248
e1dee89de037 massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents: 9245
diff changeset
   197
Goal "chain(Y) ==>iterate n (lub(range Y)) y = lub(range(%i. iterate n (Y i) y))";
9245
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   198
by (rtac (thelub_fun RS subst) 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   199
by (etac (monofun_iterate RS ch2ch_monofun) 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   200
by (asm_simp_tac (simpset() addsimps [contlub_iterate RS contlubE]) 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   201
qed "contlub_Ifix_lemma1";
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
9248
e1dee89de037 massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents: 9245
diff changeset
   204
Goal  "chain(Y) ==>\
1168
74be52691d62 The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents: 892
diff changeset
   205
\         lub(range(%i. lub(range(%ia. iterate i (Y ia) UU)))) =\
9245
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   206
\         lub(range(%i. lub(range(%ia. iterate ia (Y i) UU))))";
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   207
by (rtac antisym_less 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   208
by (rtac is_lub_thelub 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   209
by (rtac (contlub_Ifix_lemma1 RS ext RS subst) 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   210
by (atac 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   211
by (rtac chain_iterate 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   212
by (rtac ub_rangeI 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   213
by (strip_tac 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   214
by (rtac lub_mono 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   215
by (etac (monofun_iterate RS ch2ch_monofun RS ch2ch_fun) 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   216
by (etac chain_iterate_lub 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   217
by (strip_tac 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   218
by (rtac is_ub_thelub 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   219
by (rtac chain_iterate 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   220
by (rtac is_lub_thelub 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   221
by (etac chain_iterate_lub 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   222
by (rtac ub_rangeI 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   223
by (strip_tac 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   224
by (rtac lub_mono 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   225
by (rtac chain_iterate 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   226
by (rtac (contlub_Ifix_lemma1 RS ext RS subst) 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   227
by (atac 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   228
by (rtac chain_iterate 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   229
by (strip_tac 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   230
by (rtac is_ub_thelub 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   231
by (etac (monofun_iterate RS ch2ch_monofun RS ch2ch_fun) 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   232
qed "ex_lub_iterate";
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   233
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   234
9248
e1dee89de037 massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents: 9245
diff changeset
   235
Goalw [contlub,Ifix_def] "contlub(Ifix)";
9245
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   236
by (strip_tac 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   237
by (stac (contlub_Ifix_lemma1 RS ext) 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   238
by (atac 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   239
by (etac ex_lub_iterate 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   240
qed "contlub_Ifix";
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   241
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   242
9248
e1dee89de037 massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents: 9245
diff changeset
   243
Goal "cont(Ifix)";
9245
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   244
by (rtac monocontlub2cont 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   245
by (rtac monofun_Ifix 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   246
by (rtac contlub_Ifix 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   247
qed "cont_Ifix";
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   248
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   249
(* ------------------------------------------------------------------------ *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   250
(* propagate properties of Ifix to its continuous counterpart               *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   251
(* ------------------------------------------------------------------------ *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   252
10834
a7897aebbffc *** empty log message ***
nipkow
parents: 10230
diff changeset
   253
Goalw [fix_def] "fix$F = F$(fix$F)";
9245
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   254
by (asm_simp_tac (simpset() addsimps [cont_Ifix]) 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   255
by (rtac Ifix_eq 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   256
qed "fix_eq";
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   257
10834
a7897aebbffc *** empty log message ***
nipkow
parents: 10230
diff changeset
   258
Goalw [fix_def] "F$x = x ==> fix$F << x";
9245
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   259
by (asm_simp_tac (simpset() addsimps [cont_Ifix]) 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   260
by (etac Ifix_least 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   261
qed "fix_least";
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   262
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   263
9248
e1dee89de037 massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents: 9245
diff changeset
   264
Goal
10834
a7897aebbffc *** empty log message ***
nipkow
parents: 10230
diff changeset
   265
"[| F$x = x; !z. F$z = z --> x << z |] ==> x = fix$F";
9245
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   266
by (rtac antisym_less 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   267
by (etac allE 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   268
by (etac mp 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   269
by (rtac (fix_eq RS sym) 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   270
by (etac fix_least 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   271
qed "fix_eqI";
1274
ea0668a1c0ba added 8bit pragmas
regensbu
parents: 1267
diff changeset
   272
ea0668a1c0ba added 8bit pragmas
regensbu
parents: 1267
diff changeset
   273
10834
a7897aebbffc *** empty log message ***
nipkow
parents: 10230
diff changeset
   274
Goal "f == fix$F ==> f = F$f";
9248
e1dee89de037 massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents: 9245
diff changeset
   275
by (asm_simp_tac (simpset() addsimps [fix_eq RS sym]) 1);
9245
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   276
qed "fix_eq2";
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   277
10834
a7897aebbffc *** empty log message ***
nipkow
parents: 10230
diff changeset
   278
Goal "f == fix$F ==> f$x = F$f$x";
9248
e1dee89de037 massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents: 9245
diff changeset
   279
by (etac (fix_eq2 RS cfun_fun_cong) 1);
9245
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   280
qed "fix_eq3";
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   281
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   282
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
   283
10834
a7897aebbffc *** empty log message ***
nipkow
parents: 10230
diff changeset
   284
Goal "f = fix$F ==> f = F$f";
9245
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   285
by (hyp_subst_tac 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   286
by (rtac fix_eq 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   287
qed "fix_eq4";
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   288
10834
a7897aebbffc *** empty log message ***
nipkow
parents: 10230
diff changeset
   289
Goal "f = fix$F ==> f$x = F$f$x";
9245
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   290
by (rtac trans 1);
9248
e1dee89de037 massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents: 9245
diff changeset
   291
by (etac (fix_eq4 RS cfun_fun_cong) 1);
9245
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   292
by (rtac refl 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   293
qed "fix_eq5";
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   294
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   295
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
   296
10834
a7897aebbffc *** empty log message ***
nipkow
parents: 10230
diff changeset
   297
(* proves the unfolding theorem for function equations f = fix$... *)
3652
4c484f03079c added case_prover
oheimb
parents: 3460
diff changeset
   298
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
   299
        (rtac trans 1),
3652
4c484f03079c added case_prover
oheimb
parents: 3460
diff changeset
   300
        (rtac (fixeq RS fix_eq4) 1),
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   301
        (rtac trans 1),
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   302
        (rtac beta_cfun 1),
2566
cbf02fc74332 changed handling of cont_lemmas and adm_lemmas
oheimb
parents: 2354
diff changeset
   303
        (Simp_tac 1)
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   304
        ]);
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   305
10834
a7897aebbffc *** empty log message ***
nipkow
parents: 10230
diff changeset
   306
(* proves the unfolding theorem for function definitions f == fix$... *)
3652
4c484f03079c added case_prover
oheimb
parents: 3460
diff changeset
   307
fun fix_prover2 thy fixdef s = prove_goal thy s (fn prems => [
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   308
        (rtac trans 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   309
        (rtac (fix_eq2) 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   310
        (rtac fixdef 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1410
diff changeset
   311
        (rtac beta_cfun 1),
2566
cbf02fc74332 changed handling of cont_lemmas and adm_lemmas
oheimb
parents: 2354
diff changeset
   312
        (Simp_tac 1)
1168
74be52691d62 The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents: 892
diff changeset
   313
        ]);
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   314
3652
4c484f03079c added case_prover
oheimb
parents: 3460
diff changeset
   315
(* proves an application case for a function from its unfolding thm *)
4c484f03079c added case_prover
oheimb
parents: 3460
diff changeset
   316
fun case_prover thy unfold s = prove_goal thy s (fn prems => [
4c484f03079c added case_prover
oheimb
parents: 3460
diff changeset
   317
	(cut_facts_tac prems 1),
4c484f03079c added case_prover
oheimb
parents: 3460
diff changeset
   318
	(rtac trans 1),
4c484f03079c added case_prover
oheimb
parents: 3460
diff changeset
   319
	(stac unfold 1),
4477
b3e5857d8d99 New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
paulson
parents: 4423
diff changeset
   320
	Auto_tac
3652
4c484f03079c added case_prover
oheimb
parents: 3460
diff changeset
   321
	]);
4c484f03079c added case_prover
oheimb
parents: 3460
diff changeset
   322
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   323
(* ------------------------------------------------------------------------ *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   324
(* better access to definitions                                             *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   325
(* ------------------------------------------------------------------------ *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   326
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   327
9248
e1dee89de037 massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents: 9245
diff changeset
   328
Goal "Ifix=(%x. lub(range(%i. iterate i x UU)))";
9245
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   329
by (rtac ext 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   330
by (rewtac Ifix_def);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   331
by (rtac refl 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   332
qed "Ifix_def2";
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   333
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   334
(* ------------------------------------------------------------------------ *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   335
(* direct connection between fix and iteration without Ifix                 *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   336
(* ------------------------------------------------------------------------ *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   337
10834
a7897aebbffc *** empty log message ***
nipkow
parents: 10230
diff changeset
   338
Goalw [fix_def] "fix$F = lub(range(%i. iterate i F UU))";
9245
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   339
by (fold_goals_tac [Ifix_def]);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   340
by (asm_simp_tac (simpset() addsimps [cont_Ifix]) 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   341
qed "fix_def2";
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   342
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   343
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   344
(* ------------------------------------------------------------------------ *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   345
(* Lemmas about admissibility and fixed point induction                     *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   346
(* ------------------------------------------------------------------------ *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   347
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   348
(* ------------------------------------------------------------------------ *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   349
(* access to definitions                                                    *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   350
(* ------------------------------------------------------------------------ *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   351
9248
e1dee89de037 massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents: 9245
diff changeset
   352
val prems = Goalw [adm_def]
11346
0d28bc664955 corrected ML names of definitions
oheimb
parents: 10834
diff changeset
   353
   "(!!Y. [| chain Y; !i. P (Y i) |] ==> P (lub (range Y))) ==> adm P";
9248
e1dee89de037 massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents: 9245
diff changeset
   354
by (blast_tac (claset() addIs prems) 1);
9245
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   355
qed "admI";
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   356
11346
0d28bc664955 corrected ML names of definitions
oheimb
parents: 10834
diff changeset
   357
Goal "!x. P x ==> adm P";
0d28bc664955 corrected ML names of definitions
oheimb
parents: 10834
diff changeset
   358
by (rtac admI 1);
0d28bc664955 corrected ML names of definitions
oheimb
parents: 10834
diff changeset
   359
by (etac spec 1);
0d28bc664955 corrected ML names of definitions
oheimb
parents: 10834
diff changeset
   360
qed "triv_admI";
0d28bc664955 corrected ML names of definitions
oheimb
parents: 10834
diff changeset
   361
9245
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   362
Goalw [adm_def] "[| adm(P); chain(Y); !i. P(Y(i)) |] ==> P(lub(range(Y)))";
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   363
by (Blast_tac 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   364
qed "admD";
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   365
9248
e1dee89de037 massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents: 9245
diff changeset
   366
Goalw [admw_def] "admw(P) = (!F.(!n. P(iterate n F UU)) -->\
9245
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   367
\                        P (lub(range(%i. iterate i F UU))))";
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   368
by (rtac refl 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   369
qed "admw_def2";
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   370
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   371
(* ------------------------------------------------------------------------ *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   372
(* an admissible formula is also weak admissible                            *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   373
(* ------------------------------------------------------------------------ *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   374
10230
5eb935d6cc69 tidying and renaming of contrapos rules
paulson
parents: 9248
diff changeset
   375
Goalw [admw_def] "adm(P)==>admw(P)";
9245
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   376
by (strip_tac 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   377
by (etac admD 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   378
by (rtac chain_iterate 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   379
by (atac 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   380
qed "adm_impl_admw";
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   381
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   382
(* ------------------------------------------------------------------------ *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   383
(* fixed point induction                                                    *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   384
(* ------------------------------------------------------------------------ *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   385
9248
e1dee89de037 massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents: 9245
diff changeset
   386
val major::prems = Goal
10834
a7897aebbffc *** empty log message ***
nipkow
parents: 10230
diff changeset
   387
     "[| adm(P); P(UU); !!x. P(x) ==> P(F$x)|] ==> P(fix$F)";
9245
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   388
by (stac fix_def2 1);
9248
e1dee89de037 massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents: 9245
diff changeset
   389
by (rtac (major RS admD) 1);
9245
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   390
by (rtac chain_iterate 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   391
by (rtac allI 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   392
by (induct_tac "i" 1);
9248
e1dee89de037 massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents: 9245
diff changeset
   393
by (asm_simp_tac (simpset() addsimps (iterate_0::prems)) 1);
e1dee89de037 massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents: 9245
diff changeset
   394
by (asm_simp_tac (simpset() addsimps (iterate_Suc::prems)) 1);
9245
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   395
qed "fix_ind";
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   396
10834
a7897aebbffc *** empty log message ***
nipkow
parents: 10230
diff changeset
   397
val prems = Goal "[| f == fix$F; adm(P); \
a7897aebbffc *** empty log message ***
nipkow
parents: 10230
diff changeset
   398
\       P(UU); !!x. P(x) ==> P(F$x)|] ==> P f";
9245
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   399
by (cut_facts_tac prems 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   400
by (asm_simp_tac HOL_ss 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   401
by (etac fix_ind 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   402
by (atac 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   403
by (eresolve_tac prems 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   404
qed "def_fix_ind";
2568
f86367e104f5 added def_fix_ind and def_wfix_ind for convenience
oheimb
parents: 2566
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
(* computational induction for weak admissible formulae                     *)
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
10834
a7897aebbffc *** empty log message ***
nipkow
parents: 10230
diff changeset
   410
Goal "[| admw(P); !n. P(iterate n F UU)|] ==> P(fix$F)";
9245
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   411
by (stac fix_def2 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   412
by (rtac (admw_def2 RS iffD1 RS spec RS mp) 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   413
by (atac 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   414
by (rtac allI 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   415
by (etac spec 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   416
qed "wfix_ind";
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   417
10834
a7897aebbffc *** empty log message ***
nipkow
parents: 10230
diff changeset
   418
Goal "[| f == fix$F; admw(P); \
9245
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   419
\       !n. P(iterate n F UU) |] ==> P f";
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   420
by (asm_simp_tac HOL_ss 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   421
by (etac wfix_ind 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   422
by (atac 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   423
qed "def_wfix_ind";
2568
f86367e104f5 added def_fix_ind and def_wfix_ind for convenience
oheimb
parents: 2566
diff changeset
   424
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   425
(* ------------------------------------------------------------------------ *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   426
(* 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
   427
(* ------------------------------------------------------------------------ *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   428
9248
e1dee89de037 massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents: 9245
diff changeset
   429
Goalw [adm_def]
9245
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   430
"!Y. chain(Y::nat=>'a) --> (? n. max_in_chain n Y) ==> adm(P::'a=>bool)";
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   431
by (strip_tac 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   432
by (rtac exE 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   433
by (rtac mp 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   434
by (etac spec 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   435
by (atac 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   436
by (stac (lub_finch1 RS thelubI) 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   437
by (atac 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   438
by (atac 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   439
by (etac spec 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   440
qed "adm_max_in_chain";
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   441
4720
c1b83b42f65a added not1_or and if_eq_cancel to simpset()
oheimb
parents: 4477
diff changeset
   442
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
   443
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   444
(* ------------------------------------------------------------------------ *)
4720
c1b83b42f65a added not1_or and if_eq_cancel to simpset()
oheimb
parents: 4477
diff changeset
   445
(* some lemmata for functions with flat/chfin domain/range types	    *)
2354
b4a1e3306aa0 added theorems
sandnerr
parents: 2275
diff changeset
   446
(* ------------------------------------------------------------------------ *)
b4a1e3306aa0 added theorems
sandnerr
parents: 2275
diff changeset
   447
10834
a7897aebbffc *** empty log message ***
nipkow
parents: 10230
diff changeset
   448
val _ = goalw thy [adm_def] "adm (%(u::'a::cpo->'b::chfin). P(u$s))";
9245
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   449
by (strip_tac 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   450
by (dtac chfin_Rep_CFunR 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   451
by (eres_inst_tac [("x","s")] allE 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   452
by (fast_tac (HOL_cs addss (simpset() addsimps [chfin])) 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   453
qed "adm_chfindom";
2354
b4a1e3306aa0 added theorems
sandnerr
parents: 2275
diff changeset
   454
3324
6b26b886ff69 Eliminated the prediates flat,chfin
slotosch
parents: 3044
diff changeset
   455
(* adm_flat not needed any more, since it is a special case of adm_chfindom *)
2354
b4a1e3306aa0 added theorems
sandnerr
parents: 2275
diff changeset
   456
1992
0256c8b71ff1 added flat_eq,
oheimb
parents: 1872
diff changeset
   457
(* ------------------------------------------------------------------------ *)
3326
930c9bed5a09 Moved the classes flat chfin from Fix to Pcpo.
slotosch
parents: 3324
diff changeset
   458
(* improved admisibility introduction                                       *)
1992
0256c8b71ff1 added flat_eq,
oheimb
parents: 1872
diff changeset
   459
(* ------------------------------------------------------------------------ *)
0256c8b71ff1 added flat_eq,
oheimb
parents: 1872
diff changeset
   460
9248
e1dee89de037 massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents: 9245
diff changeset
   461
val prems = Goalw [adm_def]
4720
c1b83b42f65a added not1_or and if_eq_cancel to simpset()
oheimb
parents: 4477
diff changeset
   462
 "(!!Y. [| chain Y; !i. P (Y i); !i. ? j. i < j & Y i ~= Y j & Y i << Y j |]\
9245
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   463
\ ==> P(lub (range Y))) ==> adm P";
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   464
by (strip_tac 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   465
by (etac increasing_chain_adm_lemma 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   466
by (atac 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   467
by (eresolve_tac prems 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   468
by (atac 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   469
by (atac 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   470
qed "admI2";
1992
0256c8b71ff1 added flat_eq,
oheimb
parents: 1872
diff changeset
   471
0256c8b71ff1 added flat_eq,
oheimb
parents: 1872
diff changeset
   472
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   473
(* ------------------------------------------------------------------------ *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   474
(* admissibility of special formulae and propagation                        *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   475
(* ------------------------------------------------------------------------ *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   476
9248
e1dee89de037 massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents: 9245
diff changeset
   477
Goalw [adm_def] "[|cont u;cont v|]==> adm(%x. u x << v x)";
9245
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   478
by (strip_tac 1);
9248
e1dee89de037 massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents: 9245
diff changeset
   479
by (forw_inst_tac [("f","u")] (cont2mono RS ch2ch_monofun) 1);
e1dee89de037 massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents: 9245
diff changeset
   480
by (assume_tac  1);
e1dee89de037 massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents: 9245
diff changeset
   481
by (forw_inst_tac [("f","v")] (cont2mono RS ch2ch_monofun) 1);
e1dee89de037 massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents: 9245
diff changeset
   482
by (assume_tac  1);
9245
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   483
by (etac (cont2contlub RS contlubE RS spec RS mp RS ssubst) 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   484
by (atac 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   485
by (etac (cont2contlub RS contlubE RS spec RS mp RS ssubst) 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   486
by (atac 1);
9248
e1dee89de037 massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents: 9245
diff changeset
   487
by (blast_tac (claset() addIs [lub_mono]) 1);
9245
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   488
qed "adm_less";
3460
5d71eed16fbe Tuned Franz's proofs.
nipkow
parents: 3326
diff changeset
   489
Addsimps [adm_less];
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   490
10230
5eb935d6cc69 tidying and renaming of contrapos rules
paulson
parents: 9248
diff changeset
   491
Goal   "[| adm P; adm Q |] ==> adm(%x. P x & Q x)";
9245
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   492
by (fast_tac (HOL_cs addEs [admD] addIs [admI]) 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   493
qed "adm_conj";
3460
5d71eed16fbe Tuned Franz's proofs.
nipkow
parents: 3326
diff changeset
   494
Addsimps [adm_conj];
5d71eed16fbe Tuned Franz's proofs.
nipkow
parents: 3326
diff changeset
   495
9248
e1dee89de037 massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents: 9245
diff changeset
   496
Goalw [adm_def] "adm(%x. t)";
9245
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   497
by (fast_tac HOL_cs 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   498
qed "adm_not_free";
3460
5d71eed16fbe Tuned Franz's proofs.
nipkow
parents: 3326
diff changeset
   499
Addsimps [adm_not_free];
5d71eed16fbe Tuned Franz's proofs.
nipkow
parents: 3326
diff changeset
   500
10230
5eb935d6cc69 tidying and renaming of contrapos rules
paulson
parents: 9248
diff changeset
   501
Goalw [adm_def] "cont t ==> adm(%x.~ (t x) << u)";
9245
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   502
by (strip_tac 1);
10230
5eb935d6cc69 tidying and renaming of contrapos rules
paulson
parents: 9248
diff changeset
   503
by (rtac contrapos_nn 1);
9245
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   504
by (etac spec 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   505
by (rtac trans_less 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   506
by (atac 2);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   507
by (etac (cont2mono RS monofun_fun_arg) 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   508
by (rtac is_ub_thelub 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   509
by (atac 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   510
qed "adm_not_less";
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   511
10230
5eb935d6cc69 tidying and renaming of contrapos rules
paulson
parents: 9248
diff changeset
   512
Goal   "!y. adm(P y) ==> adm(%x.!y. P y x)";
9245
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   513
by (fast_tac (HOL_cs addIs [admI] addEs [admD]) 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   514
qed "adm_all";
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   515
1779
1155c06fa956 introduced forgotten bind_thm calls
oheimb
parents: 1681
diff changeset
   516
bind_thm ("adm_all2", allI RS adm_all);
625
119391dd1d59 New version
nipkow
parents: 442
diff changeset
   517
10230
5eb935d6cc69 tidying and renaming of contrapos rules
paulson
parents: 9248
diff changeset
   518
Goal   "[|cont t; adm P|] ==> adm(%x. P (t x))";
9245
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   519
by (rtac admI 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   520
by (stac (cont2contlub RS contlubE RS spec RS mp) 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   521
by (atac 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   522
by (atac 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   523
by (etac admD 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   524
by (etac (cont2mono RS ch2ch_monofun) 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   525
by (atac 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   526
by (atac 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   527
qed "adm_subst";
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   528
9248
e1dee89de037 massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents: 9245
diff changeset
   529
Goal "adm(%x.~ UU << t(x))";
9245
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   530
by (Simp_tac 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   531
qed "adm_UU_not_less";
3460
5d71eed16fbe Tuned Franz's proofs.
nipkow
parents: 3326
diff changeset
   532
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   533
9245
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   534
Goalw [adm_def] "cont(t)==> adm(%x.~ (t x) = UU)";
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   535
by (strip_tac 1);
10230
5eb935d6cc69 tidying and renaming of contrapos rules
paulson
parents: 9248
diff changeset
   536
by (rtac contrapos_nn 1);
9245
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   537
by (etac spec 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   538
by (rtac (chain_UU_I RS spec) 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   539
by (etac (cont2mono RS ch2ch_monofun) 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   540
by (atac 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   541
by (etac (cont2contlub RS contlubE RS spec RS mp RS subst) 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   542
by (atac 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   543
by (atac 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   544
qed "adm_not_UU";
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   545
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   546
Goal "[|cont u ; cont v|]==> adm(%x. u x = v x)";
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   547
by (asm_simp_tac (simpset() addsimps [po_eq_conv]) 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   548
qed "adm_eq";
3460
5d71eed16fbe Tuned Franz's proofs.
nipkow
parents: 3326
diff changeset
   549
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   550
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   551
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   552
(* ------------------------------------------------------------------------ *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   553
(* 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
   554
(* ------------------------------------------------------------------------ *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   555
1992
0256c8b71ff1 added flat_eq,
oheimb
parents: 1872
diff changeset
   556
9248
e1dee89de037 massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents: 9245
diff changeset
   557
Goal  "!n. P(Y n)|Q(Y n) ==> (? i.!j. R i j --> Q(Y(j))) | (!i.? j. R i j & P(Y(j)))";
e1dee89de037 massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents: 9245
diff changeset
   558
by (Fast_tac 1);
9245
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   559
qed "adm_disj_lemma1";
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   560
9248
e1dee89de037 massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents: 9245
diff changeset
   561
Goal "[| adm(Q); ? X. chain(X) & (!n. Q(X(n))) &\
9245
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   562
  \   lub(range(Y))=lub(range(X))|] ==> Q(lub(range(Y)))";
9248
e1dee89de037 massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents: 9245
diff changeset
   563
by (force_tac (claset() addEs [admD], simpset()) 1);
9245
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   564
qed "adm_disj_lemma2";
2619
3fd774ee405a Modified and shortened adm_disj lemmas.
nipkow
parents: 2568
diff changeset
   565
11346
0d28bc664955 corrected ML names of definitions
oheimb
parents: 10834
diff changeset
   566
Goalw [chain_def]"chain Y ==> chain (%m. if m < Suc i then Y (Suc i) else Y m)";
9245
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   567
by (Asm_simp_tac 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   568
by (safe_tac HOL_cs);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   569
by (subgoal_tac "ia = i" 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   570
by (ALLGOALS Asm_simp_tac);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   571
qed "adm_disj_lemma3";
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   572
9248
e1dee89de037 massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents: 9245
diff changeset
   573
Goal "!j. i < j --> Q(Y(j))  ==> !n. Q( if n < Suc i then Y(Suc i) else Y n)";
e1dee89de037 massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents: 9245
diff changeset
   574
by (Asm_simp_tac 1);
9245
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   575
qed "adm_disj_lemma4";
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   576
9248
e1dee89de037 massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents: 9245
diff changeset
   577
Goal
4720
c1b83b42f65a added not1_or and if_eq_cancel to simpset()
oheimb
parents: 4477
diff changeset
   578
  "!!Y::nat=>'a::cpo. [| chain(Y); ! j. i < j --> Q(Y(j)) |] ==>\
9245
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   579
  \       lub(range(Y)) = lub(range(%m. if m< Suc(i) then Y(Suc(i)) else Y m))";
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   580
by (safe_tac (HOL_cs addSIs [lub_equal2,adm_disj_lemma3]));
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   581
by (atac 2);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   582
by (res_inst_tac [("x","i")] exI 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   583
by (Asm_simp_tac 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   584
qed "adm_disj_lemma5";
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   585
9248
e1dee89de037 massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents: 9245
diff changeset
   586
Goal
4720
c1b83b42f65a added not1_or and if_eq_cancel to simpset()
oheimb
parents: 4477
diff changeset
   587
  "[| chain(Y::nat=>'a::cpo); ? i. ! j. i < j --> Q(Y(j)) |] ==>\
9245
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   588
  \         ? X. chain(X) & (! n. Q(X(n))) & lub(range(Y)) = lub(range(X))";
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   589
by (etac exE 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   590
by (res_inst_tac [("x","%m. if m<Suc(i) then Y(Suc(i)) else Y m")] exI 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   591
by (rtac conjI 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   592
by (rtac adm_disj_lemma3 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   593
by (atac 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   594
by (rtac conjI 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   595
by (rtac adm_disj_lemma4 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   596
by (atac 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   597
by (rtac adm_disj_lemma5 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   598
by (atac 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   599
by (atac 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   600
qed "adm_disj_lemma6";
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   601
9248
e1dee89de037 massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents: 9245
diff changeset
   602
Goal 
4720
c1b83b42f65a added not1_or and if_eq_cancel to simpset()
oheimb
parents: 4477
diff changeset
   603
  "[| chain(Y::nat=>'a::cpo); ! i. ? j. i < j & P(Y(j))  |] ==>\
9245
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   604
  \         chain(%m. Y(Least(%j. m<j & P(Y(j)))))";
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   605
by (rtac chainI 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   606
by (rtac chain_mono3 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   607
by (atac 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   608
by (rtac Least_le 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   609
by (rtac conjI 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   610
by (rtac Suc_lessD 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   611
by (etac allE 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   612
by (etac exE 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   613
by (rtac (LeastI RS conjunct1) 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   614
by (atac 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   615
by (etac allE 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   616
by (etac exE 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   617
by (rtac (LeastI RS conjunct2) 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   618
by (atac 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   619
qed "adm_disj_lemma7";
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   620
9248
e1dee89de037 massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents: 9245
diff changeset
   621
Goal 
9245
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   622
  "[| ! i. ? j. i < j & P(Y(j)) |] ==> ! m. P(Y(LEAST j::nat. m<j & P(Y(j))))";
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   623
by (strip_tac 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   624
by (etac allE 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   625
by (etac exE 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   626
by (etac (LeastI RS conjunct2) 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   627
qed "adm_disj_lemma8";
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   628
9248
e1dee89de037 massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents: 9245
diff changeset
   629
Goal
4720
c1b83b42f65a added not1_or and if_eq_cancel to simpset()
oheimb
parents: 4477
diff changeset
   630
  "[| chain(Y::nat=>'a::cpo); ! i. ? j. i < j & P(Y(j)) |] ==>\
9245
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   631
  \         lub(range(Y)) = lub(range(%m. Y(Least(%j. m<j & P(Y(j))))))";
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   632
by (rtac antisym_less 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   633
by (rtac lub_mono 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   634
by (atac 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   635
by (rtac adm_disj_lemma7 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   636
by (atac 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   637
by (atac 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   638
by (strip_tac 1);
9248
e1dee89de037 massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents: 9245
diff changeset
   639
by (rtac (chain_mono) 1);
9245
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   640
by (atac 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   641
by (etac allE 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   642
by (etac exE 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   643
by (rtac (LeastI RS conjunct1) 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   644
by (atac 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   645
by (rtac lub_mono3 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   646
by (rtac adm_disj_lemma7 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   647
by (atac 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   648
by (atac 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   649
by (atac 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   650
by (strip_tac 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   651
by (rtac exI 1);
9248
e1dee89de037 massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents: 9245
diff changeset
   652
by (rtac (chain_mono) 1);
9245
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   653
by (atac 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   654
by (rtac lessI 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   655
qed "adm_disj_lemma9";
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   656
9248
e1dee89de037 massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents: 9245
diff changeset
   657
Goal "[| chain(Y::nat=>'a::cpo); ! i. ? j. i < j & P(Y(j)) |] ==>\
9245
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   658
  \         ? X. chain(X) & (! n. P(X(n))) & lub(range(Y)) = lub(range(X))";
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   659
by (res_inst_tac [("x","%m. Y(Least(%j. m<j & P(Y(j))))")] exI 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   660
by (rtac conjI 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   661
by (rtac adm_disj_lemma7 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   662
by (atac 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   663
by (atac 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   664
by (rtac conjI 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   665
by (rtac adm_disj_lemma8 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   666
by (atac 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   667
by (rtac adm_disj_lemma9 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   668
by (atac 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   669
by (atac 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   670
qed "adm_disj_lemma10";
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   671
9248
e1dee89de037 massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents: 9245
diff changeset
   672
Goal "[| adm(P); chain(Y);? i. ! j. i < j --> P(Y(j))|]==>P(lub(range(Y)))";
9245
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   673
by (etac adm_disj_lemma2 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   674
by (etac adm_disj_lemma6 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   675
by (atac 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   676
qed "adm_disj_lemma12";
430
89e1986125fe Franz Regensburger's changes.
nipkow
parents: 300
diff changeset
   677
1992
0256c8b71ff1 added flat_eq,
oheimb
parents: 1872
diff changeset
   678
9248
e1dee89de037 massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents: 9245
diff changeset
   679
Goal
9245
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   680
"[| adm(P); chain(Y); ! i. ? j. i < j & P(Y(j)) |]==>P(lub(range(Y)))";
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   681
by (etac adm_disj_lemma2 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   682
by (etac adm_disj_lemma10 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   683
by (atac 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   684
qed "adm_lemma11";
430
89e1986125fe Franz Regensburger's changes.
nipkow
parents: 300
diff changeset
   685
10230
5eb935d6cc69 tidying and renaming of contrapos rules
paulson
parents: 9248
diff changeset
   686
Goal "[| adm P; adm Q |] ==> adm(%x. P x | Q x)";
9245
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   687
by (rtac admI 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   688
by (rtac (adm_disj_lemma1 RS disjE) 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   689
by (atac 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   690
by (rtac disjI2 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   691
by (etac adm_disj_lemma12 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   692
by (atac 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   693
by (atac 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   694
by (rtac disjI1 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   695
by (etac adm_lemma11 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   696
by (atac 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   697
by (atac 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   698
qed "adm_disj";
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   699
10230
5eb935d6cc69 tidying and renaming of contrapos rules
paulson
parents: 9248
diff changeset
   700
Goal "[| adm(%x.~(P x)); adm Q |] ==> adm(%x. P x --> Q x)";
9245
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   701
by (subgoal_tac "(%x. P x --> Q x) = (%x. ~P x | Q x)" 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   702
by (etac ssubst 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   703
by (etac adm_disj 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   704
by (atac 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   705
by (Simp_tac 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   706
qed "adm_imp";
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   707
5143
b94cd208f073 Removal of leading "\!\!..." from most Goal commands
paulson
parents: 5068
diff changeset
   708
Goal "[| adm (%x. P x --> Q x); adm (%x. Q x --> P x) |] \
3460
5d71eed16fbe Tuned Franz's proofs.
nipkow
parents: 3326
diff changeset
   709
\           ==> adm (%x. P x = Q x)";
4423
a129b817b58a expandshort;
wenzelm
parents: 4098
diff changeset
   710
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
   711
by (Asm_simp_tac 1);
5d71eed16fbe Tuned Franz's proofs.
nipkow
parents: 3326
diff changeset
   712
by (rtac ext 1);
5d71eed16fbe Tuned Franz's proofs.
nipkow
parents: 3326
diff changeset
   713
by (fast_tac HOL_cs 1);
5d71eed16fbe Tuned Franz's proofs.
nipkow
parents: 3326
diff changeset
   714
qed"adm_iff";
5d71eed16fbe Tuned Franz's proofs.
nipkow
parents: 3326
diff changeset
   715
5d71eed16fbe Tuned Franz's proofs.
nipkow
parents: 3326
diff changeset
   716
9248
e1dee89de037 massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents: 9245
diff changeset
   717
Goal "[| adm (%x. ~ P x); adm (%x. ~ Q x) |] ==> adm (%x. ~ (P x & Q x))";
9245
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   718
by (subgoal_tac "(%x. ~ (P x & Q x)) = (%x. ~ P x | ~ Q x)" 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   719
by (rtac ext 2);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   720
by (fast_tac HOL_cs 2);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   721
by (etac ssubst 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   722
by (etac adm_disj 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   723
by (atac 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 8161
diff changeset
   724
qed "adm_not_conj";
1675
36ba4da350c3 adapted several proofs
oheimb
parents: 1461
diff changeset
   725
11346
0d28bc664955 corrected ML names of definitions
oheimb
parents: 10834
diff changeset
   726
bind_thms ("adm_lemmas", [adm_not_free,adm_imp,adm_disj,adm_eq,adm_not_UU,
0d28bc664955 corrected ML names of definitions
oheimb
parents: 10834
diff changeset
   727
        adm_UU_not_less,adm_all2,adm_not_less,adm_not_conj,adm_iff]);
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   728
2566
cbf02fc74332 changed handling of cont_lemmas and adm_lemmas
oheimb
parents: 2354
diff changeset
   729
Addsimps adm_lemmas;