src/HOL/Lambda/Lambda.ML
author nipkow
Tue Apr 08 10:48:42 1997 +0200 (1997-04-08)
changeset 2919 953a47dc0519
parent 2891 d8f254ad1ab9
child 2922 580647a879cf
permissions -rw-r--r--
Dep. on Provers/nat_transitive
nipkow@1269
     1
(*  Title:      HOL/Lambda/Lambda.ML
nipkow@1120
     2
    ID:         $Id$
nipkow@1120
     3
    Author:     Tobias Nipkow
nipkow@1120
     4
    Copyright   1995 TU Muenchen
nipkow@1120
     5
nipkow@2116
     6
Substitution-lemmas.
nipkow@1120
     7
*)
nipkow@1120
     8
nipkow@1120
     9
(*** Lambda ***)
nipkow@1120
    10
nipkow@1120
    11
open Lambda;
nipkow@1120
    12
nipkow@1974
    13
Delsimps [subst_Var];
nipkow@1269
    14
Addsimps ([if_not_P, not_less_eq] @ beta.intrs);
nipkow@1120
    15
nipkow@1302
    16
(* don't add r_into_rtrancl! *)
nipkow@1974
    17
AddSIs beta.intrs;
nipkow@1120
    18
nipkow@2159
    19
val dB_case_distinction =
nipkow@2159
    20
  rule_by_tactic(EVERY[etac thin_rl 2,etac thin_rl 2,etac thin_rl 3])dB.induct;
nipkow@1759
    21
nipkow@1120
    22
(*** Congruence rules for ->> ***)
nipkow@1120
    23
nipkow@2159
    24
goal Lambda.thy "!!s. s ->> s' ==> Abs s ->> Abs s'";
clasohm@1465
    25
by (etac rtrancl_induct 1);
paulson@2891
    26
by (ALLGOALS (blast_tac (!claset addIs [rtrancl_into_rtrancl])));
nipkow@2159
    27
qed "rtrancl_beta_Abs";
nipkow@2159
    28
AddSIs [rtrancl_beta_Abs];
nipkow@1120
    29
nipkow@1120
    30
goal Lambda.thy "!!s. s ->> s' ==> s @ t ->> s' @ t";
clasohm@1465
    31
by (etac rtrancl_induct 1);
paulson@2891
    32
by (ALLGOALS (blast_tac (!claset addIs [rtrancl_into_rtrancl])));
nipkow@1120
    33
qed "rtrancl_beta_AppL";
nipkow@1120
    34
nipkow@1120
    35
goal Lambda.thy "!!s. t ->> t' ==> s @ t ->> s @ t'";
clasohm@1465
    36
by (etac rtrancl_induct 1);
paulson@2891
    37
by (ALLGOALS (blast_tac (!claset addIs [rtrancl_into_rtrancl])));
nipkow@1120
    38
qed "rtrancl_beta_AppR";
nipkow@1120
    39
nipkow@1120
    40
goal Lambda.thy "!!s. [| s ->> s'; t ->> t' |] ==> s @ t ->> s' @ t'";
paulson@2891
    41
by (deepen_tac (!claset addSIs [rtrancl_beta_AppL, rtrancl_beta_AppR]
nipkow@1974
    42
                        addIs  [rtrancl_trans]) 3 1);
nipkow@1120
    43
qed "rtrancl_beta_App";
nipkow@1974
    44
AddIs [rtrancl_beta_App];
nipkow@1120
    45
nipkow@1120
    46
(*** subst and lift ***)
nipkow@1120
    47
paulson@2891
    48
fun addsplit ss = ss addsimps [subst_Var] 
paulson@2891
    49
                     setloop  (split_inside_tac [expand_if]);
nipkow@1120
    50
nipkow@1153
    51
goal Lambda.thy "(Var k)[u/k] = u";
nipkow@1269
    52
by (asm_full_simp_tac(addsplit(!simpset)) 1);
nipkow@1120
    53
qed "subst_eq";
nipkow@1120
    54
nipkow@1153
    55
goal Lambda.thy "!!s. i<j ==> (Var j)[u/i] = Var(pred j)";
nipkow@1269
    56
by (asm_full_simp_tac(addsplit(!simpset)) 1);
nipkow@1120
    57
qed "subst_gt";
nipkow@1120
    58
nipkow@1153
    59
goal Lambda.thy "!!s. j<i ==> (Var j)[u/i] = Var(j)";
nipkow@1269
    60
by (asm_full_simp_tac (addsplit(!simpset) addsimps
nipkow@1120
    61
                          [less_not_refl2 RS not_sym,less_SucI]) 1);
nipkow@1120
    62
qed "subst_lt";
nipkow@1120
    63
clasohm@1266
    64
Addsimps [subst_eq,subst_gt,subst_lt];
nipkow@1120
    65
nipkow@1120
    66
goal Lambda.thy
nipkow@1172
    67
  "!i k. i < Suc k --> lift (lift t i) (Suc k) = lift (lift t k) i";
nipkow@2159
    68
by (dB.induct_tac "t" 1);
nipkow@2116
    69
by (ALLGOALS(asm_simp_tac (!simpset setloop (split_tac [expand_if])
oheimb@2637
    70
                                    addSolver cut_trans_tac)));
nipkow@2116
    71
by (safe_tac HOL_cs);
nipkow@2116
    72
by (ALLGOALS trans_tac);
nipkow@1486
    73
qed_spec_mp "lift_lift";
nipkow@1120
    74
nipkow@1153
    75
goal Lambda.thy "!i j s. j < Suc i --> \
nipkow@1153
    76
\         lift (t[s/j]) i = (lift t (Suc i)) [lift s i / j]";
nipkow@2159
    77
by (dB.induct_tac "t" 1);
nipkow@2116
    78
by (ALLGOALS(asm_simp_tac (!simpset addsimps [pred_def,subst_Var,lift_lift]
nipkow@2116
    79
                                setloop (split_tac [expand_if,expand_nat_case])
oheimb@2637
    80
                                addSolver cut_trans_tac)));
nipkow@2116
    81
by (safe_tac HOL_cs);
nipkow@2116
    82
by (ALLGOALS trans_tac);
nipkow@1120
    83
qed "lift_subst";
clasohm@1266
    84
Addsimps [lift_subst];
nipkow@1120
    85
nipkow@1120
    86
goal Lambda.thy
nipkow@1172
    87
  "!i j s. i < Suc j -->\
nipkow@1172
    88
\         lift (t[s/j]) i = (lift t i) [lift s i / Suc j]";
nipkow@2159
    89
by (dB.induct_tac "t" 1);
nipkow@2116
    90
by (ALLGOALS(asm_simp_tac (!simpset addsimps [subst_Var,lift_lift]
nipkow@2116
    91
                                setloop (split_tac [expand_if])
oheimb@2637
    92
                                addSolver cut_trans_tac)));
nipkow@2116
    93
by(safe_tac (HOL_cs addSEs [nat_neqE]));
nipkow@2116
    94
by(ALLGOALS trans_tac);
nipkow@1120
    95
qed "lift_subst_lt";
nipkow@1120
    96
nipkow@1172
    97
goal Lambda.thy "!k s. (lift t k)[s/k] = t";
nipkow@2159
    98
by (dB.induct_tac "t" 1);
nipkow@2116
    99
by (ALLGOALS (asm_full_simp_tac (!simpset setloop (split_tac[expand_if]))));
nipkow@1120
   100
qed "subst_lift";
clasohm@1266
   101
Addsimps [subst_lift];
nipkow@1120
   102
nipkow@1120
   103
nipkow@1172
   104
goal Lambda.thy "!i j u v. i < Suc j --> \
nipkow@1172
   105
\ t[lift v i / Suc j][u[v/j]/i] = t[u/i][v/j]";
nipkow@2159
   106
by (dB.induct_tac "t" 1);
nipkow@2116
   107
by (ALLGOALS(asm_simp_tac
nipkow@2116
   108
      (!simpset addsimps [pred_def,subst_Var,lift_lift RS sym,lift_subst_lt]
nipkow@2116
   109
                setloop (split_tac [expand_if,expand_nat_case])
oheimb@2637
   110
                addSolver cut_trans_tac)));
nipkow@2116
   111
by(safe_tac (HOL_cs addSEs [nat_neqE]));
nipkow@2116
   112
by(ALLGOALS trans_tac);
nipkow@1486
   113
qed_spec_mp "subst_subst";
nipkow@1153
   114
nipkow@1153
   115
nipkow@1153
   116
(*** Equivalence proof for optimized substitution ***)
nipkow@1153
   117
nipkow@1153
   118
goal Lambda.thy "!k. liftn 0 t k = t";
nipkow@2159
   119
by (dB.induct_tac "t" 1);
paulson@2031
   120
by (ALLGOALS(asm_simp_tac(addsplit(!simpset))));
nipkow@1153
   121
qed "liftn_0";
clasohm@1266
   122
Addsimps [liftn_0];
nipkow@1153
   123
nipkow@1153
   124
goal Lambda.thy "!k. liftn (Suc n) t k = lift (liftn n t k) k";
nipkow@2159
   125
by (dB.induct_tac "t" 1);
paulson@2031
   126
by (ALLGOALS(asm_simp_tac(addsplit(!simpset))));
paulson@2891
   127
by (blast_tac (!claset addDs [add_lessD1]) 1);
nipkow@1153
   128
qed "liftn_lift";
clasohm@1266
   129
Addsimps [liftn_lift];
nipkow@1153
   130
nipkow@1153
   131
goal Lambda.thy "!n. substn t s n = t[liftn n s 0 / n]";
nipkow@2159
   132
by (dB.induct_tac "t" 1);
paulson@2031
   133
by (ALLGOALS(asm_simp_tac(addsplit(!simpset))));
nipkow@1153
   134
qed "substn_subst_n";
clasohm@1266
   135
Addsimps [substn_subst_n];
nipkow@1153
   136
nipkow@1153
   137
goal Lambda.thy "substn t s 0 = t[s/0]";
paulson@2031
   138
by (Simp_tac 1);
nipkow@1153
   139
qed "substn_subst_0";