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