src/HOL/Lambda/Eta.ML
author paulson
Wed Mar 03 11:15:18 1999 +0100 (1999-03-03)
changeset 6301 08245f5a436d
parent 6141 a6922171b396
child 6307 fdf236c98914
permissions -rw-r--r--
expandshort
nipkow@1269
     1
(*  Title:      HOL/Lambda/Eta.ML
nipkow@1269
     2
    ID:         $Id$
nipkow@1269
     3
    Author:     Tobias Nipkow
nipkow@1269
     4
    Copyright   1995 TU Muenchen
nipkow@1269
     5
nipkow@1269
     6
Eta reduction,
nipkow@1302
     7
confluence of eta,
nipkow@1269
     8
commutation of beta/eta,
nipkow@1269
     9
confluence of beta+eta
nipkow@1269
    10
*)
nipkow@1269
    11
nipkow@1302
    12
Addsimps eta.intrs;
nipkow@5261
    13
AddIs eta.intrs;
nipkow@1269
    14
paulson@6141
    15
val eta_cases = map eta.mk_cases ["Abs s -e> z", "s $ t -e> u", "Var i -e> t"];
nipkow@5261
    16
AddSEs eta_cases;
nipkow@1269
    17
nipkow@2159
    18
section "eta, subst and free";
nipkow@2159
    19
wenzelm@5069
    20
Goal "!i t u. ~free s i --> s[t/i] = s[u/i]";
berghofe@5184
    21
by (induct_tac "s" 1);
wenzelm@4089
    22
by (ALLGOALS(simp_tac (addsplit (simpset()))));
paulson@2891
    23
by (Blast_tac 1);
paulson@2891
    24
by (Blast_tac 1);
nipkow@2159
    25
qed_spec_mp "subst_not_free";
nipkow@2159
    26
Addsimps [subst_not_free RS eqTrueI];
nipkow@1269
    27
nipkow@5117
    28
Goal "!i k. free (lift t k) i = (i < k & free t i | k < i & free t (i-1))";
berghofe@5184
    29
by (induct_tac "t" 1);
nipkow@6079
    30
  by (ALLGOALS(asm_full_simp_tac (addsplit (simpset()) addcongs [conj_cong])));
paulson@6301
    31
 by (arith_tac 1);
paulson@6301
    32
by (Auto_tac);
nipkow@1269
    33
qed "free_lift";
nipkow@1269
    34
Addsimps [free_lift];
nipkow@1269
    35
wenzelm@5069
    36
Goal "!i k t. free (s[t/k]) i = \
nipkow@1269
    37
\              (free s k & free t i | free s (if i<k then i else Suc i))";
berghofe@5184
    38
by (induct_tac "s" 1);
nipkow@2116
    39
by (Asm_simp_tac 2);
paulson@2891
    40
by (Blast_tac 2);
wenzelm@4089
    41
by (asm_full_simp_tac (addsplit (simpset())) 2);
nipkow@4360
    42
by (simp_tac (simpset() addsimps [diff_Suc,subst_Var]
berghofe@5184
    43
                      addsplits [nat.split]) 1);
paulson@5625
    44
by (safe_tac (HOL_cs addSEs [linorder_neqE]));
nipkow@5983
    45
by (ALLGOALS Simp_tac);
nipkow@1269
    46
qed "free_subst";
nipkow@1269
    47
Addsimps [free_subst];
nipkow@1269
    48
nipkow@5117
    49
Goal "s -e> t ==> !i. free t i = free s i";
paulson@1730
    50
by (etac eta.induct 1);
wenzelm@4089
    51
by (ALLGOALS(asm_simp_tac (simpset() addcongs [conj_cong])));
nipkow@1486
    52
qed_spec_mp "free_eta";
nipkow@1269
    53
nipkow@5117
    54
Goal "[| s -e> t; ~free s i |] ==> ~free t i";
wenzelm@4089
    55
by (asm_simp_tac (simpset() addsimps [free_eta]) 1);
nipkow@1269
    56
qed "not_free_eta";
nipkow@1269
    57
nipkow@5117
    58
Goal "s -e> t ==> !u i. s[u/i] -e> t[u/i]";
paulson@1730
    59
by (etac eta.induct 1);
wenzelm@4089
    60
by (ALLGOALS(asm_simp_tac (simpset() addsimps [subst_subst RS sym])));
nipkow@1486
    61
qed_spec_mp "eta_subst";
nipkow@1269
    62
Addsimps [eta_subst];
nipkow@1269
    63
nipkow@1759
    64
section "Confluence of -e>";
nipkow@1269
    65
wenzelm@5069
    66
Goalw [square_def,id_def]  "square eta eta (eta^=) (eta^=)";
paulson@1730
    67
by (rtac (impI RS allI RS allI) 1);
paulson@2057
    68
by (Simp_tac 1);
paulson@1730
    69
by (etac eta.induct 1);
wenzelm@4089
    70
by (slow_tac (claset() addIs [subst_not_free,eta_subst]
wenzelm@4089
    71
                      addIs [free_eta RS iffD1] addss simpset()) 1);
paulson@4162
    72
by Safe_tac;
wenzelm@4089
    73
by (blast_tac (claset() addSIs [eta_subst] addIs [free_eta RS iffD1]) 5);
paulson@2922
    74
by (ALLGOALS Blast_tac);
nipkow@2159
    75
qed "square_eta";
nipkow@1269
    76
wenzelm@5069
    77
Goal "confluent(eta)";
nipkow@2159
    78
by (rtac (square_eta RS square_reflcl_confluent) 1);
nipkow@1269
    79
qed "eta_confluent";
nipkow@1269
    80
nipkow@1759
    81
section "Congruence rules for -e>>";
nipkow@1269
    82
nipkow@5117
    83
Goal "s -e>> s' ==> Abs s -e>> Abs s'";
clasohm@1465
    84
by (etac rtrancl_induct 1);
wenzelm@4089
    85
by (ALLGOALS(blast_tac (claset() addIs [rtrancl_refl,rtrancl_into_rtrancl])));
nipkow@2159
    86
qed "rtrancl_eta_Abs";
nipkow@1269
    87
nipkow@5146
    88
Goal "s -e>> s' ==> s $ t -e>> s' $ t";
clasohm@1465
    89
by (etac rtrancl_induct 1);
wenzelm@4089
    90
by (ALLGOALS(blast_tac (claset() addIs [rtrancl_refl,rtrancl_into_rtrancl])));
nipkow@1269
    91
qed "rtrancl_eta_AppL";
nipkow@1269
    92
nipkow@5146
    93
Goal "t -e>> t' ==> s $ t -e>> s $ t'";
clasohm@1465
    94
by (etac rtrancl_induct 1);
wenzelm@4089
    95
by (ALLGOALS(blast_tac (claset() addIs [rtrancl_refl,rtrancl_into_rtrancl])));
nipkow@1269
    96
qed "rtrancl_eta_AppR";
nipkow@1269
    97
nipkow@5146
    98
Goal "[| s -e>> s'; t -e>> t' |] ==> s $ t -e>> s' $ t'";
wenzelm@4089
    99
by (blast_tac (claset() addSIs [rtrancl_eta_AppL, rtrancl_eta_AppR]
paulson@2922
   100
                       addIs [rtrancl_trans]) 1);
nipkow@1269
   101
qed "rtrancl_eta_App";
nipkow@1269
   102
nipkow@1759
   103
section "Commutation of -> and -e>";
nipkow@1269
   104
nipkow@5117
   105
Goal "s -> t ==> (!i. free t i --> free s i)";
paulson@1730
   106
by (etac beta.induct 1);
paulson@2031
   107
by (ALLGOALS(Asm_full_simp_tac));
nipkow@1486
   108
qed_spec_mp "free_beta";
nipkow@1269
   109
nipkow@5117
   110
Goal "s -> t ==> !u i. s[u/i] -> t[u/i]";
paulson@1730
   111
by (etac beta.induct 1);
wenzelm@4089
   112
by (ALLGOALS(asm_full_simp_tac (simpset() addsimps [subst_subst RS sym])));
nipkow@2159
   113
qed_spec_mp "beta_subst";
nipkow@2159
   114
AddIs [beta_subst];
nipkow@1269
   115
wenzelm@5069
   116
Goal "!i. t[Var i/i] = t[Var(i)/Suc i]";
berghofe@5184
   117
by (induct_tac "t" 1);
paulson@6301
   118
by (auto_tac (claset() addSEs [linorder_neqE], addsplit (simpset())));
nipkow@2159
   119
qed_spec_mp "subst_Var_Suc";
nipkow@2159
   120
Addsimps [subst_Var_Suc];
nipkow@1269
   121
nipkow@5117
   122
Goal "s -e> t ==> (!i. lift s i -e> lift t i)";
paulson@1730
   123
by (etac eta.induct 1);
wenzelm@4089
   124
by (ALLGOALS(asm_simp_tac (addsplit (simpset()))));
nipkow@1486
   125
qed_spec_mp "eta_lift";
nipkow@1269
   126
Addsimps [eta_lift];
nipkow@1269
   127
wenzelm@5069
   128
Goal "!s t i. s -e> t --> u[s/i] -e>> u[t/i]";
berghofe@5184
   129
by (induct_tac "u" 1);
wenzelm@4089
   130
by (ALLGOALS(asm_simp_tac (addsplit (simpset()))));
wenzelm@4089
   131
by (blast_tac (claset() addIs [r_into_rtrancl]) 1);
wenzelm@4089
   132
by (blast_tac (claset() addSIs [rtrancl_eta_App]) 1);
wenzelm@4089
   133
by (blast_tac (claset() addSIs [rtrancl_eta_Abs,eta_lift]) 1);
nipkow@1486
   134
qed_spec_mp "rtrancl_eta_subst";
nipkow@1269
   135
wenzelm@5069
   136
Goalw [square_def] "square beta eta (eta^*) (beta^=)";
paulson@1730
   137
by (rtac (impI RS allI RS allI) 1);
paulson@1730
   138
by (etac beta.induct 1);
wenzelm@4089
   139
by (slow_tac (claset() addIs [r_into_rtrancl,rtrancl_eta_subst,eta_subst]
wenzelm@4089
   140
                      addss simpset()) 1);
wenzelm@4089
   141
by (blast_tac (claset() addIs [r_into_rtrancl,rtrancl_eta_AppL]) 1);
wenzelm@4089
   142
by (blast_tac (claset() addIs [r_into_rtrancl,rtrancl_eta_AppR]) 1);
paulson@2922
   143
(*23 seconds?*)
nipkow@2931
   144
DelIffs dB.distinct;
nipkow@2931
   145
Addsimps dB.distinct;
wenzelm@4089
   146
by (slow_tac (claset() addIs [r_into_rtrancl,rtrancl_eta_Abs,free_beta]
wenzelm@4089
   147
                      addss simpset()) 1);
nipkow@1269
   148
qed "square_beta_eta";
nipkow@1269
   149
wenzelm@5069
   150
Goal "confluent(beta Un eta)";
paulson@2031
   151
by (REPEAT(ares_tac [square_rtrancl_reflcl_commute,confluent_Un,
nipkow@1269
   152
                    beta_confluent,eta_confluent,square_beta_eta] 1));
nipkow@1269
   153
qed "confluent_beta_eta";
nipkow@1759
   154
nipkow@5146
   155
section "Implicit definition of -e>: Abs(lift s 0 $ Var 0) -e> s";
nipkow@1759
   156
wenzelm@5069
   157
Goal "!i. (~free s i) = (? t. s = lift t i)";
berghofe@5184
   158
by (induct_tac "s" 1);
nipkow@4686
   159
  by (Simp_tac 1);
paulson@2057
   160
  by (SELECT_GOAL(safe_tac HOL_cs)1);
paulson@5625
   161
   by (etac linorder_neqE 1);
nipkow@2159
   162
    by (res_inst_tac [("x","Var nat")] exI 1);
nipkow@2159
   163
    by (Asm_simp_tac 1);
nipkow@4360
   164
   by (res_inst_tac [("x","Var(nat-1)")] exI 1);
paulson@2057
   165
   by (Asm_simp_tac 1);
paulson@2057
   166
  by (rtac notE 1);
paulson@2057
   167
   by (assume_tac 2);
paulson@2057
   168
  by (etac thin_rl 1);
nipkow@5261
   169
  by (exhaust_tac "t" 1);
nipkow@5261
   170
    by (Asm_simp_tac 1);
nipkow@5261
   171
   by (Asm_simp_tac 1);
nipkow@5261
   172
  by (Asm_simp_tac 1);
nipkow@2116
   173
 by (Asm_simp_tac 1);
paulson@2057
   174
 by (etac thin_rl 1);
paulson@2057
   175
 by (etac thin_rl 1);
paulson@2057
   176
 by (rtac allI 1);
paulson@2057
   177
 by (rtac iffI 1);
paulson@2057
   178
  by (REPEAT(eresolve_tac [conjE,exE] 1));
paulson@2057
   179
  by (rename_tac "u1 u2" 1);
nipkow@5146
   180
  by (res_inst_tac [("x","u1$u2")] exI 1);
paulson@2057
   181
  by (Asm_simp_tac 1);
paulson@2057
   182
 by (etac exE 1);
paulson@2057
   183
 by (etac rev_mp 1);
nipkow@5261
   184
 by (exhaust_tac "t" 1);
nipkow@5261
   185
   by (Asm_simp_tac 1);
nipkow@5261
   186
  by (Asm_simp_tac 1);
paulson@2891
   187
  by (Blast_tac 1);
nipkow@5261
   188
 by (Asm_simp_tac 1);
paulson@2031
   189
by (Asm_simp_tac 1);
paulson@2031
   190
by (etac thin_rl 1);
paulson@2031
   191
by (rtac allI 1);
paulson@2031
   192
by (rtac iffI 1);
paulson@2057
   193
 by (etac exE 1);
nipkow@2159
   194
 by (res_inst_tac [("x","Abs t")] exI 1);
paulson@2057
   195
 by (Asm_simp_tac 1);
paulson@2031
   196
by (etac exE 1);
paulson@2031
   197
by (etac rev_mp 1);
nipkow@5261
   198
by (exhaust_tac "t" 1);
nipkow@5261
   199
  by (Asm_simp_tac 1);
nipkow@5261
   200
 by (Asm_simp_tac 1);
nipkow@5261
   201
by (Asm_simp_tac 1);
paulson@2891
   202
by (Blast_tac 1);
nipkow@1759
   203
qed_spec_mp "not_free_iff_lifted";
nipkow@1759
   204
nipkow@5146
   205
Goal "(!s u. (~free s 0) --> R(Abs(s $ Var 0))(s[u/0])) = \
nipkow@5146
   206
\     (!s. R(Abs(lift s 0 $ Var 0))(s))";
wenzelm@4089
   207
by (fast_tac (HOL_cs addss (simpset() addsimps [not_free_iff_lifted])) 1);
nipkow@1759
   208
qed "explicit_is_implicit";