src/HOL/Proofs/Lambda/Lambda.thy
author haftmann
Sat, 05 Jul 2014 11:01:53 +0200
changeset 57514 bdc2c6b40bf2
parent 46512 4f9f61f9b535
child 58273 9f0bfcd15097
permissions -rw-r--r--
prefer ac_simps collections over separate name bindings for add and mult
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
39157
b98909faaea8 more explicit HOL-Proofs sessions, including former ex/Hilbert_Classical.thy which works in parallel mode without the antiquotation option "margin" (which is still critical);
wenzelm
parents: 39126
diff changeset
     1
(*  Title:      HOL/Proofs/Lambda/Lambda.thy
1120
ff7dd80513e6 Lambda calculus in de Bruijn notation.
nipkow
parents:
diff changeset
     2
    Author:     Tobias Nipkow
ff7dd80513e6 Lambda calculus in de Bruijn notation.
nipkow
parents:
diff changeset
     3
    Copyright   1995 TU Muenchen
ff7dd80513e6 Lambda calculus in de Bruijn notation.
nipkow
parents:
diff changeset
     4
*)
ff7dd80513e6 Lambda calculus in de Bruijn notation.
nipkow
parents:
diff changeset
     5
9811
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 6453
diff changeset
     6
header {* Basic definitions of Lambda-calculus *}
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 6453
diff changeset
     7
16417
9bc16273c2d4 migrated theory headers to new format
haftmann
parents: 14065
diff changeset
     8
theory Lambda imports Main begin
9811
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 6453
diff changeset
     9
46512
4f9f61f9b535 simplified configuration options for syntax ambiguity;
wenzelm
parents: 46506
diff changeset
    10
declare [[syntax_ambiguity_warning = false]]
39126
ee117c5b3b75 configuration options Syntax.ambiguity_enabled (inverse of former Syntax.ambiguity_is_error), Syntax.ambiguity_level (with Isar attribute "syntax_ambiguity_level"), Syntax.ambiguity_limit;
wenzelm
parents: 36862
diff changeset
    11
1120
ff7dd80513e6 Lambda calculus in de Bruijn notation.
nipkow
parents:
diff changeset
    12
9811
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 6453
diff changeset
    13
subsection {* Lambda-terms in de Bruijn notation and substitution *}
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 6453
diff changeset
    14
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 6453
diff changeset
    15
datatype dB =
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 6453
diff changeset
    16
    Var nat
12011
1a3a7b3cd9bb tuned notation (degree instead of dollar);
wenzelm
parents: 11943
diff changeset
    17
  | App dB dB (infixl "\<degree>" 200)
9811
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 6453
diff changeset
    18
  | Abs dB
1120
ff7dd80513e6 Lambda calculus in de Bruijn notation.
nipkow
parents:
diff changeset
    19
25974
0cb35fa9c6fa modernized primrec;
wenzelm
parents: 23750
diff changeset
    20
primrec
9811
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 6453
diff changeset
    21
  lift :: "[dB, nat] => dB"
25974
0cb35fa9c6fa modernized primrec;
wenzelm
parents: 23750
diff changeset
    22
where
0cb35fa9c6fa modernized primrec;
wenzelm
parents: 23750
diff changeset
    23
    "lift (Var i) k = (if i < k then Var i else Var (i + 1))"
0cb35fa9c6fa modernized primrec;
wenzelm
parents: 23750
diff changeset
    24
  | "lift (s \<degree> t) k = lift s k \<degree> lift t k"
0cb35fa9c6fa modernized primrec;
wenzelm
parents: 23750
diff changeset
    25
  | "lift (Abs s) k = Abs (lift s (k + 1))"
1153
5c5daf97cf2d Simplified the confluence proofs.
nipkow
parents: 1124
diff changeset
    26
5184
9b8547a9496a Adapted to new datatype package.
berghofe
parents: 5146
diff changeset
    27
primrec
25974
0cb35fa9c6fa modernized primrec;
wenzelm
parents: 23750
diff changeset
    28
  subst :: "[dB, dB, nat] => dB"  ("_[_'/_]" [300, 0, 0] 300)
0cb35fa9c6fa modernized primrec;
wenzelm
parents: 23750
diff changeset
    29
where (* FIXME base names *)
0cb35fa9c6fa modernized primrec;
wenzelm
parents: 23750
diff changeset
    30
    subst_Var: "(Var i)[s/k] =
0cb35fa9c6fa modernized primrec;
wenzelm
parents: 23750
diff changeset
    31
      (if k < i then Var (i - 1) else if i = k then s else Var i)"
0cb35fa9c6fa modernized primrec;
wenzelm
parents: 23750
diff changeset
    32
  | subst_App: "(t \<degree> u)[s/k] = t[s/k] \<degree> u[s/k]"
0cb35fa9c6fa modernized primrec;
wenzelm
parents: 23750
diff changeset
    33
  | subst_Abs: "(Abs t)[s/k] = Abs (t[lift s 0 / k+1])"
9811
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 6453
diff changeset
    34
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 6453
diff changeset
    35
declare subst_Var [simp del]
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 6453
diff changeset
    36
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 6453
diff changeset
    37
text {* Optimized versions of @{term subst} and @{term lift}. *}
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 6453
diff changeset
    38
25974
0cb35fa9c6fa modernized primrec;
wenzelm
parents: 23750
diff changeset
    39
primrec
9811
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 6453
diff changeset
    40
  liftn :: "[nat, dB, nat] => dB"
25974
0cb35fa9c6fa modernized primrec;
wenzelm
parents: 23750
diff changeset
    41
where
0cb35fa9c6fa modernized primrec;
wenzelm
parents: 23750
diff changeset
    42
    "liftn n (Var i) k = (if i < k then Var i else Var (i + n))"
0cb35fa9c6fa modernized primrec;
wenzelm
parents: 23750
diff changeset
    43
  | "liftn n (s \<degree> t) k = liftn n s k \<degree> liftn n t k"
0cb35fa9c6fa modernized primrec;
wenzelm
parents: 23750
diff changeset
    44
  | "liftn n (Abs s) k = Abs (liftn n s (k + 1))"
9811
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 6453
diff changeset
    45
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 6453
diff changeset
    46
primrec
25974
0cb35fa9c6fa modernized primrec;
wenzelm
parents: 23750
diff changeset
    47
  substn :: "[dB, dB, nat] => dB"
0cb35fa9c6fa modernized primrec;
wenzelm
parents: 23750
diff changeset
    48
where
0cb35fa9c6fa modernized primrec;
wenzelm
parents: 23750
diff changeset
    49
    "substn (Var i) s k =
0cb35fa9c6fa modernized primrec;
wenzelm
parents: 23750
diff changeset
    50
      (if k < i then Var (i - 1) else if i = k then liftn k s 0 else Var i)"
0cb35fa9c6fa modernized primrec;
wenzelm
parents: 23750
diff changeset
    51
  | "substn (t \<degree> u) s k = substn t s k \<degree> substn u s k"
0cb35fa9c6fa modernized primrec;
wenzelm
parents: 23750
diff changeset
    52
  | "substn (Abs t) s k = Abs (substn t s (k + 1))"
1120
ff7dd80513e6 Lambda calculus in de Bruijn notation.
nipkow
parents:
diff changeset
    53
9811
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 6453
diff changeset
    54
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 6453
diff changeset
    55
subsection {* Beta-reduction *}
1153
5c5daf97cf2d Simplified the confluence proofs.
nipkow
parents: 1124
diff changeset
    56
23750
a1db5f819d00 - Renamed inductive2 to inductive
berghofe
parents: 22271
diff changeset
    57
inductive beta :: "[dB, dB] => bool"  (infixl "\<rightarrow>\<^sub>\<beta>" 50)
22271
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21404
diff changeset
    58
  where
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21404
diff changeset
    59
    beta [simp, intro!]: "Abs s \<degree> t \<rightarrow>\<^sub>\<beta> s[t/0]"
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21404
diff changeset
    60
  | appL [simp, intro!]: "s \<rightarrow>\<^sub>\<beta> t ==> s \<degree> u \<rightarrow>\<^sub>\<beta> t \<degree> u"
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21404
diff changeset
    61
  | appR [simp, intro!]: "s \<rightarrow>\<^sub>\<beta> t ==> u \<degree> s \<rightarrow>\<^sub>\<beta> u \<degree> t"
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21404
diff changeset
    62
  | abs [simp, intro!]: "s \<rightarrow>\<^sub>\<beta> t ==> Abs s \<rightarrow>\<^sub>\<beta> Abs t"
21404
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 21210
diff changeset
    63
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 21210
diff changeset
    64
abbreviation
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 21210
diff changeset
    65
  beta_reds :: "[dB, dB] => bool"  (infixl "->>" 50) where
22271
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21404
diff changeset
    66
  "s ->> t == beta^** s t"
19086
1b3780be6cc2 new-style definitions/abbreviations;
wenzelm
parents: 18257
diff changeset
    67
21210
c17fd2df4e9e renamed 'const_syntax' to 'notation';
wenzelm
parents: 20503
diff changeset
    68
notation (latex)
19656
09be06943252 tuned concrete syntax -- abbreviation/const_syntax;
wenzelm
parents: 19380
diff changeset
    69
  beta_reds  (infixl "\<rightarrow>\<^sub>\<beta>\<^sup>*" 50)
1120
ff7dd80513e6 Lambda calculus in de Bruijn notation.
nipkow
parents:
diff changeset
    70
23750
a1db5f819d00 - Renamed inductive2 to inductive
berghofe
parents: 22271
diff changeset
    71
inductive_cases beta_cases [elim!]:
14065
8abaf978c9c2 Nicer syntax for beta reduction.
berghofe
parents: 13915
diff changeset
    72
  "Var i \<rightarrow>\<^sub>\<beta> t"
8abaf978c9c2 Nicer syntax for beta reduction.
berghofe
parents: 13915
diff changeset
    73
  "Abs r \<rightarrow>\<^sub>\<beta> s"
8abaf978c9c2 Nicer syntax for beta reduction.
berghofe
parents: 13915
diff changeset
    74
  "s \<degree> t \<rightarrow>\<^sub>\<beta> u"
9811
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 6453
diff changeset
    75
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 6453
diff changeset
    76
declare if_not_P [simp] not_less_eq [simp]
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 6453
diff changeset
    77
  -- {* don't add @{text "r_into_rtrancl[intro!]"} *}
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 6453
diff changeset
    78
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 6453
diff changeset
    79
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 6453
diff changeset
    80
subsection {* Congruence rules *}
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 6453
diff changeset
    81
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 6453
diff changeset
    82
lemma rtrancl_beta_Abs [intro!]:
14065
8abaf978c9c2 Nicer syntax for beta reduction.
berghofe
parents: 13915
diff changeset
    83
    "s \<rightarrow>\<^sub>\<beta>\<^sup>* s' ==> Abs s \<rightarrow>\<^sub>\<beta>\<^sup>* Abs s'"
23750
a1db5f819d00 - Renamed inductive2 to inductive
berghofe
parents: 22271
diff changeset
    84
  by (induct set: rtranclp) (blast intro: rtranclp.rtrancl_into_rtrancl)+
9811
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 6453
diff changeset
    85
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 6453
diff changeset
    86
lemma rtrancl_beta_AppL:
14065
8abaf978c9c2 Nicer syntax for beta reduction.
berghofe
parents: 13915
diff changeset
    87
    "s \<rightarrow>\<^sub>\<beta>\<^sup>* s' ==> s \<degree> t \<rightarrow>\<^sub>\<beta>\<^sup>* s' \<degree> t"
23750
a1db5f819d00 - Renamed inductive2 to inductive
berghofe
parents: 22271
diff changeset
    88
  by (induct set: rtranclp) (blast intro: rtranclp.rtrancl_into_rtrancl)+
9811
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 6453
diff changeset
    89
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 6453
diff changeset
    90
lemma rtrancl_beta_AppR:
14065
8abaf978c9c2 Nicer syntax for beta reduction.
berghofe
parents: 13915
diff changeset
    91
    "t \<rightarrow>\<^sub>\<beta>\<^sup>* t' ==> s \<degree> t \<rightarrow>\<^sub>\<beta>\<^sup>* s \<degree> t'"
23750
a1db5f819d00 - Renamed inductive2 to inductive
berghofe
parents: 22271
diff changeset
    92
  by (induct set: rtranclp) (blast intro: rtranclp.rtrancl_into_rtrancl)+
9811
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 6453
diff changeset
    93
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 6453
diff changeset
    94
lemma rtrancl_beta_App [intro]:
14065
8abaf978c9c2 Nicer syntax for beta reduction.
berghofe
parents: 13915
diff changeset
    95
    "[| s \<rightarrow>\<^sub>\<beta>\<^sup>* s'; t \<rightarrow>\<^sub>\<beta>\<^sup>* t' |] ==> s \<degree> t \<rightarrow>\<^sub>\<beta>\<^sup>* s' \<degree> t'"
23750
a1db5f819d00 - Renamed inductive2 to inductive
berghofe
parents: 22271
diff changeset
    96
  by (blast intro!: rtrancl_beta_AppL rtrancl_beta_AppR intro: rtranclp_trans)
9811
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 6453
diff changeset
    97
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 6453
diff changeset
    98
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 6453
diff changeset
    99
subsection {* Substitution-lemmas *}
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 6453
diff changeset
   100
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 6453
diff changeset
   101
lemma subst_eq [simp]: "(Var k)[u/k] = u"
18241
afdba6b3e383 tuned induction proofs;
wenzelm
parents: 16417
diff changeset
   102
  by (simp add: subst_Var)
9811
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 6453
diff changeset
   103
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 6453
diff changeset
   104
lemma subst_gt [simp]: "i < j ==> (Var j)[u/i] = Var (j - 1)"
18241
afdba6b3e383 tuned induction proofs;
wenzelm
parents: 16417
diff changeset
   105
  by (simp add: subst_Var)
9811
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 6453
diff changeset
   106
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 6453
diff changeset
   107
lemma subst_lt [simp]: "j < i ==> (Var j)[u/i] = Var j"
18241
afdba6b3e383 tuned induction proofs;
wenzelm
parents: 16417
diff changeset
   108
  by (simp add: subst_Var)
9811
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 6453
diff changeset
   109
18241
afdba6b3e383 tuned induction proofs;
wenzelm
parents: 16417
diff changeset
   110
lemma lift_lift:
afdba6b3e383 tuned induction proofs;
wenzelm
parents: 16417
diff changeset
   111
    "i < k + 1 \<Longrightarrow> lift (lift t i) (Suc k) = lift (lift t k) i"
20503
503ac4c5ef91 induct method: renamed 'fixing' to 'arbitrary';
wenzelm
parents: 19656
diff changeset
   112
  by (induct t arbitrary: i k) auto
9811
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 6453
diff changeset
   113
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 6453
diff changeset
   114
lemma lift_subst [simp]:
18241
afdba6b3e383 tuned induction proofs;
wenzelm
parents: 16417
diff changeset
   115
    "j < i + 1 \<Longrightarrow> lift (t[s/j]) i = (lift t (i + 1)) [lift s i / j]"
20503
503ac4c5ef91 induct method: renamed 'fixing' to 'arbitrary';
wenzelm
parents: 19656
diff changeset
   116
  by (induct t arbitrary: i j s)
18241
afdba6b3e383 tuned induction proofs;
wenzelm
parents: 16417
diff changeset
   117
    (simp_all add: diff_Suc subst_Var lift_lift split: nat.split)
9811
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 6453
diff changeset
   118
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 6453
diff changeset
   119
lemma lift_subst_lt:
18241
afdba6b3e383 tuned induction proofs;
wenzelm
parents: 16417
diff changeset
   120
    "i < j + 1 \<Longrightarrow> lift (t[s/j]) i = (lift t i) [lift s i / j + 1]"
20503
503ac4c5ef91 induct method: renamed 'fixing' to 'arbitrary';
wenzelm
parents: 19656
diff changeset
   121
  by (induct t arbitrary: i j s) (simp_all add: subst_Var lift_lift)
9811
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 6453
diff changeset
   122
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 6453
diff changeset
   123
lemma subst_lift [simp]:
18241
afdba6b3e383 tuned induction proofs;
wenzelm
parents: 16417
diff changeset
   124
    "(lift t k)[s/k] = t"
20503
503ac4c5ef91 induct method: renamed 'fixing' to 'arbitrary';
wenzelm
parents: 19656
diff changeset
   125
  by (induct t arbitrary: k s) simp_all
9811
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 6453
diff changeset
   126
18241
afdba6b3e383 tuned induction proofs;
wenzelm
parents: 16417
diff changeset
   127
lemma subst_subst:
afdba6b3e383 tuned induction proofs;
wenzelm
parents: 16417
diff changeset
   128
    "i < j + 1 \<Longrightarrow> t[lift v i / Suc j][u[v/j]/i] = t[u/i][v/j]"
20503
503ac4c5ef91 induct method: renamed 'fixing' to 'arbitrary';
wenzelm
parents: 19656
diff changeset
   129
  by (induct t arbitrary: i j u v)
18241
afdba6b3e383 tuned induction proofs;
wenzelm
parents: 16417
diff changeset
   130
    (simp_all add: diff_Suc subst_Var lift_lift [symmetric] lift_subst_lt
9811
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 6453
diff changeset
   131
      split: nat.split)
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 6453
diff changeset
   132
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 6453
diff changeset
   133
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 6453
diff changeset
   134
subsection {* Equivalence proof for optimized substitution *}
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 6453
diff changeset
   135
18241
afdba6b3e383 tuned induction proofs;
wenzelm
parents: 16417
diff changeset
   136
lemma liftn_0 [simp]: "liftn 0 t k = t"
20503
503ac4c5ef91 induct method: renamed 'fixing' to 'arbitrary';
wenzelm
parents: 19656
diff changeset
   137
  by (induct t arbitrary: k) (simp_all add: subst_Var)
9811
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 6453
diff changeset
   138
18241
afdba6b3e383 tuned induction proofs;
wenzelm
parents: 16417
diff changeset
   139
lemma liftn_lift [simp]: "liftn (Suc n) t k = lift (liftn n t k) k"
20503
503ac4c5ef91 induct method: renamed 'fixing' to 'arbitrary';
wenzelm
parents: 19656
diff changeset
   140
  by (induct t arbitrary: k) (simp_all add: subst_Var)
9811
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 6453
diff changeset
   141
18241
afdba6b3e383 tuned induction proofs;
wenzelm
parents: 16417
diff changeset
   142
lemma substn_subst_n [simp]: "substn t s n = t[liftn n s 0 / n]"
20503
503ac4c5ef91 induct method: renamed 'fixing' to 'arbitrary';
wenzelm
parents: 19656
diff changeset
   143
  by (induct t arbitrary: n) (simp_all add: subst_Var)
9811
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 6453
diff changeset
   144
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 6453
diff changeset
   145
theorem substn_subst_0: "substn t s 0 = t[s/0]"
18241
afdba6b3e383 tuned induction proofs;
wenzelm
parents: 16417
diff changeset
   146
  by simp
9811
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 6453
diff changeset
   147
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 6453
diff changeset
   148
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 6453
diff changeset
   149
subsection {* Preservation theorems *}
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 6453
diff changeset
   150
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 6453
diff changeset
   151
text {* Not used in Church-Rosser proof, but in Strong
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 6453
diff changeset
   152
  Normalization. \medskip *}
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 6453
diff changeset
   153
13915
28ccb51bd2f3 Eliminated most occurrences of rule_format attribute.
berghofe
parents: 13187
diff changeset
   154
theorem subst_preserves_beta [simp]:
18257
2124b24454dd tuned induct proofs;
wenzelm
parents: 18241
diff changeset
   155
    "r \<rightarrow>\<^sub>\<beta> s ==> r[t/i] \<rightarrow>\<^sub>\<beta> s[t/i]"
20503
503ac4c5ef91 induct method: renamed 'fixing' to 'arbitrary';
wenzelm
parents: 19656
diff changeset
   156
  by (induct arbitrary: t i set: beta) (simp_all add: subst_subst [symmetric])
9811
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 6453
diff changeset
   157
14065
8abaf978c9c2 Nicer syntax for beta reduction.
berghofe
parents: 13915
diff changeset
   158
theorem subst_preserves_beta': "r \<rightarrow>\<^sub>\<beta>\<^sup>* s ==> r[t/i] \<rightarrow>\<^sub>\<beta>\<^sup>* s[t/i]"
23750
a1db5f819d00 - Renamed inductive2 to inductive
berghofe
parents: 22271
diff changeset
   159
  apply (induct set: rtranclp)
a1db5f819d00 - Renamed inductive2 to inductive
berghofe
parents: 22271
diff changeset
   160
   apply (rule rtranclp.rtrancl_refl)
a1db5f819d00 - Renamed inductive2 to inductive
berghofe
parents: 22271
diff changeset
   161
  apply (erule rtranclp.rtrancl_into_rtrancl)
14065
8abaf978c9c2 Nicer syntax for beta reduction.
berghofe
parents: 13915
diff changeset
   162
  apply (erule subst_preserves_beta)
8abaf978c9c2 Nicer syntax for beta reduction.
berghofe
parents: 13915
diff changeset
   163
  done
8abaf978c9c2 Nicer syntax for beta reduction.
berghofe
parents: 13915
diff changeset
   164
13915
28ccb51bd2f3 Eliminated most occurrences of rule_format attribute.
berghofe
parents: 13187
diff changeset
   165
theorem lift_preserves_beta [simp]:
18257
2124b24454dd tuned induct proofs;
wenzelm
parents: 18241
diff changeset
   166
    "r \<rightarrow>\<^sub>\<beta> s ==> lift r i \<rightarrow>\<^sub>\<beta> lift s i"
20503
503ac4c5ef91 induct method: renamed 'fixing' to 'arbitrary';
wenzelm
parents: 19656
diff changeset
   167
  by (induct arbitrary: i set: beta) auto
9811
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 6453
diff changeset
   168
14065
8abaf978c9c2 Nicer syntax for beta reduction.
berghofe
parents: 13915
diff changeset
   169
theorem lift_preserves_beta': "r \<rightarrow>\<^sub>\<beta>\<^sup>* s ==> lift r i \<rightarrow>\<^sub>\<beta>\<^sup>* lift s i"
23750
a1db5f819d00 - Renamed inductive2 to inductive
berghofe
parents: 22271
diff changeset
   170
  apply (induct set: rtranclp)
a1db5f819d00 - Renamed inductive2 to inductive
berghofe
parents: 22271
diff changeset
   171
   apply (rule rtranclp.rtrancl_refl)
a1db5f819d00 - Renamed inductive2 to inductive
berghofe
parents: 22271
diff changeset
   172
  apply (erule rtranclp.rtrancl_into_rtrancl)
14065
8abaf978c9c2 Nicer syntax for beta reduction.
berghofe
parents: 13915
diff changeset
   173
  apply (erule lift_preserves_beta)
8abaf978c9c2 Nicer syntax for beta reduction.
berghofe
parents: 13915
diff changeset
   174
  done
8abaf978c9c2 Nicer syntax for beta reduction.
berghofe
parents: 13915
diff changeset
   175
18241
afdba6b3e383 tuned induction proofs;
wenzelm
parents: 16417
diff changeset
   176
theorem subst_preserves_beta2 [simp]: "r \<rightarrow>\<^sub>\<beta> s ==> t[r/i] \<rightarrow>\<^sub>\<beta>\<^sup>* t[s/i]"
20503
503ac4c5ef91 induct method: renamed 'fixing' to 'arbitrary';
wenzelm
parents: 19656
diff changeset
   177
  apply (induct t arbitrary: r s i)
23750
a1db5f819d00 - Renamed inductive2 to inductive
berghofe
parents: 22271
diff changeset
   178
    apply (simp add: subst_Var r_into_rtranclp)
9811
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 6453
diff changeset
   179
   apply (simp add: rtrancl_beta_App)
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 6453
diff changeset
   180
  apply (simp add: rtrancl_beta_Abs)
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 6453
diff changeset
   181
  done
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 6453
diff changeset
   182
14065
8abaf978c9c2 Nicer syntax for beta reduction.
berghofe
parents: 13915
diff changeset
   183
theorem subst_preserves_beta2': "r \<rightarrow>\<^sub>\<beta>\<^sup>* s ==> t[r/i] \<rightarrow>\<^sub>\<beta>\<^sup>* t[s/i]"
23750
a1db5f819d00 - Renamed inductive2 to inductive
berghofe
parents: 22271
diff changeset
   184
  apply (induct set: rtranclp)
a1db5f819d00 - Renamed inductive2 to inductive
berghofe
parents: 22271
diff changeset
   185
   apply (rule rtranclp.rtrancl_refl)
a1db5f819d00 - Renamed inductive2 to inductive
berghofe
parents: 22271
diff changeset
   186
  apply (erule rtranclp_trans)
14065
8abaf978c9c2 Nicer syntax for beta reduction.
berghofe
parents: 13915
diff changeset
   187
  apply (erule subst_preserves_beta2)
8abaf978c9c2 Nicer syntax for beta reduction.
berghofe
parents: 13915
diff changeset
   188
  done
8abaf978c9c2 Nicer syntax for beta reduction.
berghofe
parents: 13915
diff changeset
   189
11638
2c3dee321b4b inductive: no collective atts;
wenzelm
parents: 10851
diff changeset
   190
end