src/ZF/Resid/Substitution.thy
author wenzelm
Thu Apr 26 14:24:08 2007 +0200 (2007-04-26)
changeset 22808 a7daa74e2980
parent 16417 9bc16273c2d4
child 24892 c663e675e177
permissions -rw-r--r--
eliminated unnamed infixes, tuned syntax;
     1 (*  Title:      ZF/Resid/Substitution.thy
     2     ID:         $Id$
     3     Author:     Ole Rasmussen
     4     Copyright   1995  University of Cambridge
     5     Logic Image: ZF
     6 *)
     7 
     8 theory Substitution imports Redex begin
     9 
    10 consts
    11   lift_aux      :: "i=>i"
    12   lift          :: "i=>i"
    13   subst_aux     :: "i=>i"
    14   subst         :: "[i,i]=>i"  (infixl "'/" 70)
    15 
    16 constdefs
    17   lift_rec      :: "[i,i]=> i"
    18     "lift_rec(r,k) == lift_aux(r)`k"
    19 
    20   subst_rec     :: "[i,i,i]=> i"	(**NOTE THE ARGUMENT ORDER BELOW**)
    21     "subst_rec(u,r,k) == subst_aux(r)`u`k"
    22 
    23 translations
    24   "lift(r)"  == "lift_rec(r,0)"
    25   "u/v"      == "subst_rec(u,v,0)"
    26   
    27 
    28 (** The clumsy _aux functions are required because other arguments vary
    29     in the recursive calls ***)
    30 
    31 primrec
    32   "lift_aux(Var(i)) = (\<lambda>k \<in> nat. if i<k then Var(i) else Var(succ(i)))"
    33 
    34   "lift_aux(Fun(t)) = (\<lambda>k \<in> nat. Fun(lift_aux(t) ` succ(k)))"
    35 
    36   "lift_aux(App(b,f,a)) = (\<lambda>k \<in> nat. App(b, lift_aux(f)`k, lift_aux(a)`k))"
    37 
    38 
    39   
    40 primrec
    41   "subst_aux(Var(i)) =
    42      (\<lambda>r \<in> redexes. \<lambda>k \<in> nat. if k<i then Var(i #- 1) 
    43 				else if k=i then r else Var(i))"
    44   "subst_aux(Fun(t)) =
    45      (\<lambda>r \<in> redexes. \<lambda>k \<in> nat. Fun(subst_aux(t) ` lift(r) ` succ(k)))"
    46 
    47   "subst_aux(App(b,f,a)) = 
    48      (\<lambda>r \<in> redexes. \<lambda>k \<in> nat. App(b, subst_aux(f)`r`k, subst_aux(a)`r`k))"
    49 
    50 
    51 (* ------------------------------------------------------------------------- *)
    52 (*   Arithmetic extensions                                                   *)
    53 (* ------------------------------------------------------------------------- *)
    54 
    55 lemma gt_not_eq: "p < n ==> n\<noteq>p"
    56 by blast
    57 
    58 lemma succ_pred [rule_format, simp]: "j \<in> nat ==> i < j --> succ(j #- 1) = j"
    59 by (induct_tac "j", auto)
    60 
    61 lemma lt_pred: "[|succ(x)<n; n \<in> nat|] ==> x < n #- 1 "
    62 apply (rule succ_leE)
    63 apply (simp add: succ_pred)
    64 done
    65 
    66 lemma gt_pred: "[|n < succ(x); p<n; n \<in> nat|] ==> n #- 1 < x "
    67 apply (rule succ_leE)
    68 apply (simp add: succ_pred)
    69 done
    70 
    71 
    72 declare not_lt_iff_le [simp] if_P [simp] if_not_P [simp]
    73 
    74 
    75 (* ------------------------------------------------------------------------- *)
    76 (*     lift_rec equality rules                                               *)
    77 (* ------------------------------------------------------------------------- *)
    78 lemma lift_rec_Var:
    79      "n \<in> nat ==> lift_rec(Var(i),n) = (if i<n then Var(i) else Var(succ(i)))"
    80 by (simp add: lift_rec_def)
    81 
    82 lemma lift_rec_le [simp]:
    83      "[|i \<in> nat; k\<le>i|] ==> lift_rec(Var(i),k) = Var(succ(i))"
    84 by (simp add: lift_rec_def le_in_nat)
    85 
    86 lemma lift_rec_gt [simp]: "[| k \<in> nat; i<k |] ==> lift_rec(Var(i),k) = Var(i)"
    87 by (simp add: lift_rec_def)
    88 
    89 lemma lift_rec_Fun [simp]:
    90      "k \<in> nat ==> lift_rec(Fun(t),k) = Fun(lift_rec(t,succ(k)))"
    91 by (simp add: lift_rec_def)
    92 
    93 lemma lift_rec_App [simp]:
    94      "k \<in> nat ==> lift_rec(App(b,f,a),k) = App(b,lift_rec(f,k),lift_rec(a,k))"
    95 by (simp add: lift_rec_def)
    96 
    97 
    98 (* ------------------------------------------------------------------------- *)
    99 (*    substitution quality rules                                             *)
   100 (* ------------------------------------------------------------------------- *)
   101 
   102 lemma subst_Var:
   103      "[|k \<in> nat; u \<in> redexes|]   
   104       ==> subst_rec(u,Var(i),k) =   
   105           (if k<i then Var(i #- 1) else if k=i then u else Var(i))"
   106 by (simp add: subst_rec_def gt_not_eq leI)
   107 
   108 
   109 lemma subst_eq [simp]:
   110      "[|n \<in> nat; u \<in> redexes|] ==> subst_rec(u,Var(n),n) = u"
   111 by (simp add: subst_rec_def)
   112 
   113 lemma subst_gt [simp]:
   114      "[|u \<in> redexes; p \<in> nat; p<n|] ==> subst_rec(u,Var(n),p) = Var(n #- 1)"
   115 by (simp add: subst_rec_def)
   116 
   117 lemma subst_lt [simp]:
   118      "[|u \<in> redexes; p \<in> nat; n<p|] ==> subst_rec(u,Var(n),p) = Var(n)"
   119 by (simp add: subst_rec_def gt_not_eq leI lt_nat_in_nat)
   120 
   121 lemma subst_Fun [simp]:
   122      "[|p \<in> nat; u \<in> redexes|]
   123       ==> subst_rec(u,Fun(t),p) = Fun(subst_rec(lift(u),t,succ(p))) "
   124 by (simp add: subst_rec_def)
   125 
   126 lemma subst_App [simp]:
   127      "[|p \<in> nat; u \<in> redexes|]
   128       ==> subst_rec(u,App(b,f,a),p) = App(b,subst_rec(u,f,p),subst_rec(u,a,p))"
   129 by (simp add: subst_rec_def)
   130 
   131 
   132 lemma lift_rec_type [rule_format, simp]:
   133      "u \<in> redexes ==> \<forall>k \<in> nat. lift_rec(u,k) \<in> redexes"
   134 apply (erule redexes.induct)
   135 apply (simp_all add: lift_rec_Var lift_rec_Fun lift_rec_App)
   136 done
   137 
   138 lemma subst_type [rule_format, simp]:
   139      "v \<in> redexes ==>  \<forall>n \<in> nat. \<forall>u \<in> redexes. subst_rec(u,v,n) \<in> redexes"
   140 apply (erule redexes.induct)
   141 apply (simp_all add: subst_Var lift_rec_type)
   142 done
   143 
   144 
   145 (* ------------------------------------------------------------------------- *)
   146 (*    lift and  substitution proofs                                          *)
   147 (* ------------------------------------------------------------------------- *)
   148 
   149 (*The i\<in>nat is redundant*)
   150 lemma lift_lift_rec [rule_format]:
   151      "u \<in> redexes 
   152       ==> \<forall>n \<in> nat. \<forall>i \<in> nat. i\<le>n -->    
   153            (lift_rec(lift_rec(u,i),succ(n)) = lift_rec(lift_rec(u,n),i))"
   154 apply (erule redexes.induct, auto)
   155 apply (case_tac "n < i")
   156 apply (frule lt_trans2, assumption)
   157 apply (simp_all add: lift_rec_Var leI)
   158 done
   159 
   160 lemma lift_lift:
   161      "[|u \<in> redexes; n \<in> nat|] 
   162       ==> lift_rec(lift(u),succ(n)) = lift(lift_rec(u,n))"
   163 by (simp add: lift_lift_rec)
   164 
   165 lemma lt_not_m1_lt: "\<lbrakk>m < n; n \<in> nat; m \<in> nat\<rbrakk>\<Longrightarrow> ~ n #- 1 < m"
   166 by (erule natE, auto)
   167 
   168 lemma lift_rec_subst_rec [rule_format]:
   169      "v \<in> redexes ==>   
   170        \<forall>n \<in> nat. \<forall>m \<in> nat. \<forall>u \<in> redexes. n\<le>m--> 
   171           lift_rec(subst_rec(u,v,n),m) =  
   172                subst_rec(lift_rec(u,m),lift_rec(v,succ(m)),n)"
   173 apply (erule redexes.induct, simp_all (no_asm_simp) add: lift_lift)
   174 apply safe
   175 apply (rename_tac n n' m u) 
   176 apply (case_tac "n < n'")
   177  apply (frule_tac j = n' in lt_trans2, assumption)
   178  apply (simp add: leI, simp)
   179 apply (erule_tac j=n in leE)
   180 apply (auto simp add: lift_rec_Var subst_Var leI lt_not_m1_lt)
   181 done
   182 
   183 
   184 lemma lift_subst:
   185      "[|v \<in> redexes; u \<in> redexes; n \<in> nat|] 
   186       ==> lift_rec(u/v,n) = lift_rec(u,n)/lift_rec(v,succ(n))"
   187 by (simp add: lift_rec_subst_rec)
   188 
   189 
   190 lemma lift_rec_subst_rec_lt [rule_format]:
   191      "v \<in> redexes ==>   
   192        \<forall>n \<in> nat. \<forall>m \<in> nat. \<forall>u \<in> redexes. m\<le>n--> 
   193           lift_rec(subst_rec(u,v,n),m) =  
   194                subst_rec(lift_rec(u,m),lift_rec(v,m),succ(n))"
   195 apply (erule redexes.induct, simp_all (no_asm_simp) add: lift_lift)
   196 apply safe
   197 apply (rename_tac n n' m u) 
   198 apply (case_tac "n < n'")
   199 apply (case_tac "n < m")
   200 apply (simp_all add: leI)
   201 apply (erule_tac i=n' in leE)
   202 apply (frule lt_trans1, assumption)
   203 apply (simp_all add: succ_pred leI gt_pred)
   204 done
   205 
   206 
   207 lemma subst_rec_lift_rec [rule_format]:
   208      "u \<in> redexes ==>   
   209         \<forall>n \<in> nat. \<forall>v \<in> redexes. subst_rec(v,lift_rec(u,n),n) = u"
   210 apply (erule redexes.induct, auto)
   211 apply (case_tac "n < na", auto)
   212 done
   213 
   214 lemma subst_rec_subst_rec [rule_format]:
   215      "v \<in> redexes ==>   
   216         \<forall>m \<in> nat. \<forall>n \<in> nat. \<forall>u \<in> redexes. \<forall>w \<in> redexes. m\<le>n -->  
   217 	  subst_rec(subst_rec(w,u,n),subst_rec(lift_rec(w,m),v,succ(n)),m) = 
   218 	  subst_rec(w,subst_rec(u,v,m),n)"
   219 apply (erule redexes.induct)
   220 apply (simp_all add: lift_lift [symmetric] lift_rec_subst_rec_lt, safe)
   221 apply (rename_tac n' u w) 
   222 apply (case_tac "n \<le> succ(n') ")
   223  apply (erule_tac i = n in leE)
   224  apply (simp_all add: succ_pred subst_rec_lift_rec leI)
   225  apply (case_tac "n < m")
   226   apply (frule lt_trans2, assumption, simp add: gt_pred)
   227  apply simp
   228  apply (erule_tac j = n in leE, simp add: gt_pred)
   229  apply (simp add: subst_rec_lift_rec)
   230 (*final case*)
   231 apply (frule nat_into_Ord [THEN le_refl, THEN lt_trans], assumption)
   232 apply (erule leE)
   233  apply (frule succ_leI [THEN lt_trans], assumption)
   234  apply (frule_tac i = m in nat_into_Ord [THEN le_refl, THEN lt_trans], 
   235         assumption)
   236  apply (simp_all add: succ_pred lt_pred)
   237 done
   238 
   239 
   240 lemma substitution:
   241      "[|v \<in> redexes; u \<in> redexes; w \<in> redexes; n \<in> nat|]
   242       ==> subst_rec(w,u,n)/subst_rec(lift(w),v,succ(n)) = subst_rec(w,u/v,n)"
   243 by (simp add: subst_rec_subst_rec)
   244 
   245 
   246 (* ------------------------------------------------------------------------- *)
   247 (*          Preservation lemmas                                              *)
   248 (*          Substitution preserves comp and regular                          *)
   249 (* ------------------------------------------------------------------------- *)
   250 
   251 
   252 lemma lift_rec_preserve_comp [rule_format, simp]:
   253      "u ~ v ==> \<forall>m \<in> nat. lift_rec(u,m) ~ lift_rec(v,m)"
   254 by (erule Scomp.induct, simp_all add: comp_refl)
   255 
   256 lemma subst_rec_preserve_comp [rule_format, simp]:
   257      "u2 ~ v2 ==> \<forall>m \<in> nat. \<forall>u1 \<in> redexes. \<forall>v1 \<in> redexes. 
   258                   u1 ~ v1--> subst_rec(u1,u2,m) ~ subst_rec(v1,v2,m)"
   259 by (erule Scomp.induct, 
   260     simp_all add: subst_Var lift_rec_preserve_comp comp_refl)
   261 
   262 lemma lift_rec_preserve_reg [simp]:
   263      "regular(u) ==> \<forall>m \<in> nat. regular(lift_rec(u,m))"
   264 by (erule Sreg.induct, simp_all add: lift_rec_Var)
   265 
   266 lemma subst_rec_preserve_reg [simp]:
   267      "regular(v) ==>   
   268         \<forall>m \<in> nat. \<forall>u \<in> redexes. regular(u)-->regular(subst_rec(u,v,m))"
   269 by (erule Sreg.induct, simp_all add: subst_Var lift_rec_preserve_reg)
   270 
   271 end