src/HOL/Proofs/Lambda/Lambda.thy
 author wenzelm Fri Feb 17 15:42:26 2012 +0100 (2012-02-17) changeset 46512 4f9f61f9b535 parent 46506 c7faa011bfa7 child 58273 9f0bfcd15097 permissions -rw-r--r--
simplified configuration options for syntax ambiguity;
```     1 (*  Title:      HOL/Proofs/Lambda/Lambda.thy
```
```     2     Author:     Tobias Nipkow
```
```     3     Copyright   1995 TU Muenchen
```
```     4 *)
```
```     5
```
```     6 header {* Basic definitions of Lambda-calculus *}
```
```     7
```
```     8 theory Lambda imports Main begin
```
```     9
```
```    10 declare [[syntax_ambiguity_warning = false]]
```
```    11
```
```    12
```
```    13 subsection {* Lambda-terms in de Bruijn notation and substitution *}
```
```    14
```
```    15 datatype dB =
```
```    16     Var nat
```
```    17   | App dB dB (infixl "\<degree>" 200)
```
```    18   | Abs dB
```
```    19
```
```    20 primrec
```
```    21   lift :: "[dB, nat] => dB"
```
```    22 where
```
```    23     "lift (Var i) k = (if i < k then Var i else Var (i + 1))"
```
```    24   | "lift (s \<degree> t) k = lift s k \<degree> lift t k"
```
```    25   | "lift (Abs s) k = Abs (lift s (k + 1))"
```
```    26
```
```    27 primrec
```
```    28   subst :: "[dB, dB, nat] => dB"  ("_[_'/_]" [300, 0, 0] 300)
```
```    29 where (* FIXME base names *)
```
```    30     subst_Var: "(Var i)[s/k] =
```
```    31       (if k < i then Var (i - 1) else if i = k then s else Var i)"
```
```    32   | subst_App: "(t \<degree> u)[s/k] = t[s/k] \<degree> u[s/k]"
```
```    33   | subst_Abs: "(Abs t)[s/k] = Abs (t[lift s 0 / k+1])"
```
```    34
```
```    35 declare subst_Var [simp del]
```
```    36
```
```    37 text {* Optimized versions of @{term subst} and @{term lift}. *}
```
```    38
```
```    39 primrec
```
```    40   liftn :: "[nat, dB, nat] => dB"
```
```    41 where
```
```    42     "liftn n (Var i) k = (if i < k then Var i else Var (i + n))"
```
```    43   | "liftn n (s \<degree> t) k = liftn n s k \<degree> liftn n t k"
```
```    44   | "liftn n (Abs s) k = Abs (liftn n s (k + 1))"
```
```    45
```
```    46 primrec
```
```    47   substn :: "[dB, dB, nat] => dB"
```
```    48 where
```
```    49     "substn (Var i) s k =
```
```    50       (if k < i then Var (i - 1) else if i = k then liftn k s 0 else Var i)"
```
```    51   | "substn (t \<degree> u) s k = substn t s k \<degree> substn u s k"
```
```    52   | "substn (Abs t) s k = Abs (substn t s (k + 1))"
```
```    53
```
```    54
```
```    55 subsection {* Beta-reduction *}
```
```    56
```
```    57 inductive beta :: "[dB, dB] => bool"  (infixl "\<rightarrow>\<^sub>\<beta>" 50)
```
```    58   where
```
```    59     beta [simp, intro!]: "Abs s \<degree> t \<rightarrow>\<^sub>\<beta> s[t/0]"
```
```    60   | appL [simp, intro!]: "s \<rightarrow>\<^sub>\<beta> t ==> s \<degree> u \<rightarrow>\<^sub>\<beta> t \<degree> u"
```
```    61   | appR [simp, intro!]: "s \<rightarrow>\<^sub>\<beta> t ==> u \<degree> s \<rightarrow>\<^sub>\<beta> u \<degree> t"
```
```    62   | abs [simp, intro!]: "s \<rightarrow>\<^sub>\<beta> t ==> Abs s \<rightarrow>\<^sub>\<beta> Abs t"
```
```    63
```
```    64 abbreviation
```
```    65   beta_reds :: "[dB, dB] => bool"  (infixl "->>" 50) where
```
```    66   "s ->> t == beta^** s t"
```
```    67
```
```    68 notation (latex)
```
```    69   beta_reds  (infixl "\<rightarrow>\<^sub>\<beta>\<^sup>*" 50)
```
```    70
```
```    71 inductive_cases beta_cases [elim!]:
```
```    72   "Var i \<rightarrow>\<^sub>\<beta> t"
```
```    73   "Abs r \<rightarrow>\<^sub>\<beta> s"
```
```    74   "s \<degree> t \<rightarrow>\<^sub>\<beta> u"
```
```    75
```
```    76 declare if_not_P [simp] not_less_eq [simp]
```
```    77   -- {* don't add @{text "r_into_rtrancl[intro!]"} *}
```
```    78
```
```    79
```
```    80 subsection {* Congruence rules *}
```
```    81
```
```    82 lemma rtrancl_beta_Abs [intro!]:
```
```    83     "s \<rightarrow>\<^sub>\<beta>\<^sup>* s' ==> Abs s \<rightarrow>\<^sub>\<beta>\<^sup>* Abs s'"
```
```    84   by (induct set: rtranclp) (blast intro: rtranclp.rtrancl_into_rtrancl)+
```
```    85
```
```    86 lemma rtrancl_beta_AppL:
```
```    87     "s \<rightarrow>\<^sub>\<beta>\<^sup>* s' ==> s \<degree> t \<rightarrow>\<^sub>\<beta>\<^sup>* s' \<degree> t"
```
```    88   by (induct set: rtranclp) (blast intro: rtranclp.rtrancl_into_rtrancl)+
```
```    89
```
```    90 lemma rtrancl_beta_AppR:
```
```    91     "t \<rightarrow>\<^sub>\<beta>\<^sup>* t' ==> s \<degree> t \<rightarrow>\<^sub>\<beta>\<^sup>* s \<degree> t'"
```
```    92   by (induct set: rtranclp) (blast intro: rtranclp.rtrancl_into_rtrancl)+
```
```    93
```
```    94 lemma rtrancl_beta_App [intro]:
```
```    95     "[| s \<rightarrow>\<^sub>\<beta>\<^sup>* s'; t \<rightarrow>\<^sub>\<beta>\<^sup>* t' |] ==> s \<degree> t \<rightarrow>\<^sub>\<beta>\<^sup>* s' \<degree> t'"
```
```    96   by (blast intro!: rtrancl_beta_AppL rtrancl_beta_AppR intro: rtranclp_trans)
```
```    97
```
```    98
```
```    99 subsection {* Substitution-lemmas *}
```
```   100
```
```   101 lemma subst_eq [simp]: "(Var k)[u/k] = u"
```
```   102   by (simp add: subst_Var)
```
```   103
```
```   104 lemma subst_gt [simp]: "i < j ==> (Var j)[u/i] = Var (j - 1)"
```
```   105   by (simp add: subst_Var)
```
```   106
```
```   107 lemma subst_lt [simp]: "j < i ==> (Var j)[u/i] = Var j"
```
```   108   by (simp add: subst_Var)
```
```   109
```
```   110 lemma lift_lift:
```
```   111     "i < k + 1 \<Longrightarrow> lift (lift t i) (Suc k) = lift (lift t k) i"
```
```   112   by (induct t arbitrary: i k) auto
```
```   113
```
```   114 lemma lift_subst [simp]:
```
```   115     "j < i + 1 \<Longrightarrow> lift (t[s/j]) i = (lift t (i + 1)) [lift s i / j]"
```
```   116   by (induct t arbitrary: i j s)
```
```   117     (simp_all add: diff_Suc subst_Var lift_lift split: nat.split)
```
```   118
```
```   119 lemma lift_subst_lt:
```
```   120     "i < j + 1 \<Longrightarrow> lift (t[s/j]) i = (lift t i) [lift s i / j + 1]"
```
```   121   by (induct t arbitrary: i j s) (simp_all add: subst_Var lift_lift)
```
```   122
```
```   123 lemma subst_lift [simp]:
```
```   124     "(lift t k)[s/k] = t"
```
```   125   by (induct t arbitrary: k s) simp_all
```
```   126
```
```   127 lemma subst_subst:
```
```   128     "i < j + 1 \<Longrightarrow> t[lift v i / Suc j][u[v/j]/i] = t[u/i][v/j]"
```
```   129   by (induct t arbitrary: i j u v)
```
```   130     (simp_all add: diff_Suc subst_Var lift_lift [symmetric] lift_subst_lt
```
```   131       split: nat.split)
```
```   132
```
```   133
```
```   134 subsection {* Equivalence proof for optimized substitution *}
```
```   135
```
```   136 lemma liftn_0 [simp]: "liftn 0 t k = t"
```
```   137   by (induct t arbitrary: k) (simp_all add: subst_Var)
```
```   138
```
```   139 lemma liftn_lift [simp]: "liftn (Suc n) t k = lift (liftn n t k) k"
```
```   140   by (induct t arbitrary: k) (simp_all add: subst_Var)
```
```   141
```
```   142 lemma substn_subst_n [simp]: "substn t s n = t[liftn n s 0 / n]"
```
```   143   by (induct t arbitrary: n) (simp_all add: subst_Var)
```
```   144
```
```   145 theorem substn_subst_0: "substn t s 0 = t[s/0]"
```
```   146   by simp
```
```   147
```
```   148
```
```   149 subsection {* Preservation theorems *}
```
```   150
```
```   151 text {* Not used in Church-Rosser proof, but in Strong
```
```   152   Normalization. \medskip *}
```
```   153
```
```   154 theorem subst_preserves_beta [simp]:
```
```   155     "r \<rightarrow>\<^sub>\<beta> s ==> r[t/i] \<rightarrow>\<^sub>\<beta> s[t/i]"
```
```   156   by (induct arbitrary: t i set: beta) (simp_all add: subst_subst [symmetric])
```
```   157
```
```   158 theorem subst_preserves_beta': "r \<rightarrow>\<^sub>\<beta>\<^sup>* s ==> r[t/i] \<rightarrow>\<^sub>\<beta>\<^sup>* s[t/i]"
```
```   159   apply (induct set: rtranclp)
```
```   160    apply (rule rtranclp.rtrancl_refl)
```
```   161   apply (erule rtranclp.rtrancl_into_rtrancl)
```
```   162   apply (erule subst_preserves_beta)
```
```   163   done
```
```   164
```
```   165 theorem lift_preserves_beta [simp]:
```
```   166     "r \<rightarrow>\<^sub>\<beta> s ==> lift r i \<rightarrow>\<^sub>\<beta> lift s i"
```
```   167   by (induct arbitrary: i set: beta) auto
```
```   168
```
```   169 theorem lift_preserves_beta': "r \<rightarrow>\<^sub>\<beta>\<^sup>* s ==> lift r i \<rightarrow>\<^sub>\<beta>\<^sup>* lift s i"
```
```   170   apply (induct set: rtranclp)
```
```   171    apply (rule rtranclp.rtrancl_refl)
```
```   172   apply (erule rtranclp.rtrancl_into_rtrancl)
```
```   173   apply (erule lift_preserves_beta)
```
```   174   done
```
```   175
```
```   176 theorem subst_preserves_beta2 [simp]: "r \<rightarrow>\<^sub>\<beta> s ==> t[r/i] \<rightarrow>\<^sub>\<beta>\<^sup>* t[s/i]"
```
```   177   apply (induct t arbitrary: r s i)
```
```   178     apply (simp add: subst_Var r_into_rtranclp)
```
```   179    apply (simp add: rtrancl_beta_App)
```
```   180   apply (simp add: rtrancl_beta_Abs)
```
```   181   done
```
```   182
```
```   183 theorem subst_preserves_beta2': "r \<rightarrow>\<^sub>\<beta>\<^sup>* s ==> t[r/i] \<rightarrow>\<^sub>\<beta>\<^sup>* t[s/i]"
```
```   184   apply (induct set: rtranclp)
```
```   185    apply (rule rtranclp.rtrancl_refl)
```
```   186   apply (erule rtranclp_trans)
```
```   187   apply (erule subst_preserves_beta2)
```
```   188   done
```
```   189
```
```   190 end
```