src/HOL/Lambda/Eta.thy
author wenzelm
Mon, 04 Sep 2000 11:21:24 +0200
changeset 9827 ce6e22ff89c3
parent 9811 39ffdb8cab03
child 9858 c3ac6128b649
permissions -rw-r--r--
tuned;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
1269
ee011b365770 New version with eta reduction.
nipkow
parents:
diff changeset
     1
(*  Title:      HOL/Lambda/Eta.thy
ee011b365770 New version with eta reduction.
nipkow
parents:
diff changeset
     2
    ID:         $Id$
ee011b365770 New version with eta reduction.
nipkow
parents:
diff changeset
     3
    Author:     Tobias Nipkow
ee011b365770 New version with eta reduction.
nipkow
parents:
diff changeset
     4
    Copyright   1995 TU Muenchen
ee011b365770 New version with eta reduction.
nipkow
parents:
diff changeset
     5
*)
ee011b365770 New version with eta reduction.
nipkow
parents:
diff changeset
     6
9811
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
     7
header {* Eta-reduction *}
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
     8
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
     9
theory Eta = ParRed:
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
    10
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
    11
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
    12
subsection {* Definition of eta-reduction and relatives *}
1269
ee011b365770 New version with eta reduction.
nipkow
parents:
diff changeset
    13
9811
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
    14
consts
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
    15
  free :: "dB => nat => bool"
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
    16
primrec
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
    17
  "free (Var j) i = (j = i)"
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
    18
  "free (s $ t) i = (free s i \<or> free t i)"
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
    19
  "free (Abs s) i = free s (i + 1)"
1269
ee011b365770 New version with eta reduction.
nipkow
parents:
diff changeset
    20
9811
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
    21
consts
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
    22
  eta :: "(dB \<times> dB) set"
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
    23
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
    24
syntax 
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
    25
  "_eta" :: "[dB, dB] => bool"   (infixl "-e>" 50)
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
    26
  "_eta_rtrancl" :: "[dB, dB] => bool"   (infixl "-e>>" 50)
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
    27
  "_eta_reflcl" :: "[dB, dB] => bool"   (infixl "-e>=" 50)
1269
ee011b365770 New version with eta reduction.
nipkow
parents:
diff changeset
    28
translations
9827
wenzelm
parents: 9811
diff changeset
    29
  "s -e> t" == "(s, t) \<in> eta"
wenzelm
parents: 9811
diff changeset
    30
  "s -e>> t" == "(s, t) \<in> eta^*"
wenzelm
parents: 9811
diff changeset
    31
  "s -e>= t" == "(s, t) \<in> eta^="
1269
ee011b365770 New version with eta reduction.
nipkow
parents:
diff changeset
    32
1789
aade046ec6d5 Quotes now optional around inductive set
paulson
parents: 1376
diff changeset
    33
inductive eta
9811
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
    34
  intros [simp, intro]
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
    35
    eta: "\<not> free s 0 ==> Abs (s $ Var 0) -e> s[dummy/0]"
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
    36
    appL: "s -e> t ==> s $ u -e> t $ u"
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
    37
    appR: "s -e> t ==> u $ s -e> u $ t"
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
    38
    abs: "s -e> t ==> Abs s -e> Abs t"
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
    39
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
    40
inductive_cases eta_cases [elim!]:
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
    41
  "Abs s -e> z"
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
    42
  "s $ t -e> u"
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
    43
  "Var i -e> t"
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
    44
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
    45
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
    46
subsection "Properties of eta, subst and free"
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
    47
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
    48
lemma subst_not_free [rulify, simp]:
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
    49
    "\<forall>i t u. \<not> free s i --> s[t/i] = s[u/i]"
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
    50
  apply (induct_tac s)
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
    51
    apply (simp_all add: subst_Var)
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
    52
  done
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
    53
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
    54
lemma free_lift [simp]:
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
    55
    "\<forall>i k. free (lift t k) i =
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
    56
      (i < k \<and> free t i \<or> k < i \<and> free t (i - 1))"
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
    57
  apply (induct_tac t)
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
    58
    apply (auto cong: conj_cong)
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
    59
  apply arith
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
    60
  done
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
    61
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
    62
lemma free_subst [simp]:
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
    63
    "\<forall>i k t. free (s[t/k]) i =
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
    64
      (free s k \<and> free t i \<or> free s (if i < k then i else i + 1))"
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
    65
  apply (induct_tac s)
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
    66
    prefer 2
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
    67
    apply simp
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
    68
    apply blast
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
    69
   prefer 2
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
    70
   apply simp
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
    71
  apply (simp add: diff_Suc subst_Var split: nat.split)
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
    72
  apply clarify
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
    73
  apply (erule linorder_neqE)
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
    74
  apply simp_all
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
    75
  done
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
    76
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
    77
lemma free_eta [rulify]:
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
    78
    "s -e> t ==> \<forall>i. free t i = free s i"
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
    79
  apply (erule eta.induct)
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
    80
     apply (simp_all cong: conj_cong)
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
    81
  done
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
    82
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
    83
lemma not_free_eta:
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
    84
    "[| s -e> t; \<not> free s i |] ==> \<not> free t i"
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
    85
  apply (simp add: free_eta)
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
    86
  done
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
    87
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
    88
lemma eta_subst [rulify, simp]:
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
    89
    "s -e> t ==> \<forall>u i. s[u/i] -e> t[u/i]"
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
    90
  apply (erule eta.induct)
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
    91
  apply (simp_all add: subst_subst [symmetric])
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
    92
  done
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
    93
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
    94
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
    95
subsection "Confluence of eta"
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
    96
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
    97
lemma square_eta: "square eta eta (eta^=) (eta^=)"
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
    98
  apply (unfold square_def id_def)
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
    99
  apply (rule impI [THEN allI [THEN allI]])
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
   100
  apply simp
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
   101
  apply (erule eta.induct)
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
   102
     apply (slowsimp intro: subst_not_free eta_subst free_eta [THEN iffD1])
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
   103
    apply safe
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
   104
       prefer 5
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
   105
       apply (blast intro!: eta_subst intro: free_eta [THEN iffD1])
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
   106
      apply blast+
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
   107
  done
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
   108
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
   109
theorem eta_confluent: "confluent eta"
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
   110
  apply (rule square_eta [THEN square_reflcl_confluent])
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
   111
  done
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
   112
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
   113
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
   114
subsection "Congruence rules for eta*"
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
   115
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
   116
lemma rtrancl_eta_Abs: "s -e>> s' ==> Abs s -e>> Abs s'"
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
   117
  apply (erule rtrancl_induct)
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
   118
   apply (blast intro: rtrancl_refl rtrancl_into_rtrancl)+
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
   119
  done
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
   120
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
   121
lemma rtrancl_eta_AppL: "s -e>> s' ==> s $ t -e>> s' $ t"
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
   122
  apply (erule rtrancl_induct)
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
   123
   apply (blast intro: rtrancl_refl rtrancl_into_rtrancl)+
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
   124
  done
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
   125
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
   126
lemma rtrancl_eta_AppR: "t -e>> t' ==> s $ t -e>> s $ t'"
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
   127
  apply (erule rtrancl_induct)
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
   128
   apply (blast intro: rtrancl_refl rtrancl_into_rtrancl)+
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
   129
  done
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
   130
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
   131
lemma rtrancl_eta_App:
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
   132
    "[| s -e>> s'; t -e>> t' |] ==> s $ t -e>> s' $ t'"
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
   133
  apply (blast intro!: rtrancl_eta_AppL rtrancl_eta_AppR intro: rtrancl_trans)
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
   134
  done
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
   135
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
   136
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
   137
subsection "Commutation of beta and eta"
1900
c7a869229091 Simplified primrec definitions.
berghofe
parents: 1789
diff changeset
   138
9811
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
   139
lemma free_beta [rulify]:
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
   140
    "s -> t ==> \<forall>i. free t i --> free s i"
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
   141
  apply (erule beta.induct)
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
   142
     apply simp_all
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
   143
  done
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
   144
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
   145
lemma beta_subst [rulify, intro]:
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
   146
    "s -> t ==> \<forall>u i. s[u/i] -> t[u/i]"
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
   147
  apply (erule beta.induct)
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
   148
     apply (simp_all add: subst_subst [symmetric])
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
   149
  done
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
   150
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
   151
lemma subst_Var_Suc [simp]: "\<forall>i. t[Var i/i] = t[Var(i)/i + 1]"
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
   152
  apply (induct_tac t)
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
   153
  apply (auto elim!: linorder_neqE simp: subst_Var)
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
   154
  done
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
   155
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
   156
lemma eta_lift [rulify, simp]:
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
   157
    "s -e> t ==> \<forall>i. lift s i -e> lift t i"
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
   158
  apply (erule eta.induct)
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
   159
     apply simp_all
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
   160
  done
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
   161
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
   162
lemma rtrancl_eta_subst [rulify]:
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
   163
    "\<forall>s t i. s -e> t --> u[s/i] -e>> u[t/i]"
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
   164
  apply (induct_tac u)
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
   165
    apply (simp_all add: subst_Var)
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
   166
    apply (blast intro: r_into_rtrancl)
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
   167
   apply (blast intro: rtrancl_eta_App)
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
   168
  apply (blast intro!: rtrancl_eta_Abs eta_lift)
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
   169
  done
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
   170
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
   171
lemma square_beta_eta: "square beta eta (eta^*) (beta^=)"
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
   172
  apply (unfold square_def)
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
   173
  apply (rule impI [THEN allI [THEN allI]])
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
   174
  apply (erule beta.induct)
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
   175
     apply (slowsimp intro: r_into_rtrancl rtrancl_eta_subst eta_subst)
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
   176
    apply (blast intro: r_into_rtrancl rtrancl_eta_AppL)
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
   177
   apply (blast intro: r_into_rtrancl rtrancl_eta_AppR)
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
   178
  apply (slowsimp intro: r_into_rtrancl rtrancl_eta_Abs free_beta
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
   179
    other: dB.distinct [iff del, simp])    (*23 seconds?*)
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
   180
  done
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
   181
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
   182
lemma confluent_beta_eta: "confluent (beta \<union> eta)"
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
   183
  apply (assumption |
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
   184
    rule square_rtrancl_reflcl_commute confluent_Un
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
   185
      beta_confluent eta_confluent square_beta_eta)+
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
   186
  done
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
   187
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
   188
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
   189
subsection "Implicit definition of eta"
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
   190
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
   191
text {* @{term "Abs (lift s 0 $ Var 0) -e> s"} *}
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
   192
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
   193
lemma not_free_iff_lifted [rulify]:
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
   194
    "\<forall>i. (\<not> free s i) = (\<exists>t. s = lift t i)"
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
   195
  apply (induct_tac s)
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
   196
    apply simp
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
   197
    apply clarify
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
   198
    apply (rule iffI)
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
   199
     apply (erule linorder_neqE)
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
   200
      apply (rule_tac x = "Var nat" in exI)
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
   201
      apply simp
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
   202
     apply (rule_tac x = "Var (nat - 1)" in exI)
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
   203
     apply simp
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
   204
    apply clarify
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
   205
    apply (rule notE)
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
   206
     prefer 2
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
   207
     apply assumption
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
   208
    apply (erule thin_rl)
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
   209
    apply (case_tac t)
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
   210
      apply simp
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
   211
     apply simp
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
   212
    apply simp
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
   213
   apply simp
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
   214
   apply (erule thin_rl)
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
   215
   apply (erule thin_rl)
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
   216
   apply (rule allI)
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
   217
   apply (rule iffI)
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
   218
    apply (elim conjE exE)
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
   219
    apply (rename_tac u1 u2)
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
   220
    apply (rule_tac x = "u1 $ u2" in exI)
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
   221
    apply simp
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
   222
   apply (erule exE)
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
   223
   apply (erule rev_mp)
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
   224
   apply (case_tac t)
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
   225
     apply simp
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
   226
    apply simp
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
   227
    apply blast
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
   228
   apply simp
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
   229
  apply simp
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
   230
  apply (erule thin_rl)
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
   231
  apply (rule allI)
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
   232
  apply (rule iffI)
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
   233
   apply (erule exE)
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
   234
   apply (rule_tac x = "Abs t" in exI)
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
   235
   apply simp
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
   236
  apply (erule exE)
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
   237
  apply (erule rev_mp)
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
   238
  apply (case_tac t)
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
   239
    apply simp
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
   240
   apply simp
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
   241
  apply simp
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
   242
  apply blast
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
   243
  done
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
   244
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
   245
theorem explicit_is_implicit:
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
   246
  "(\<forall>s u. (\<not> free s 0) --> R (Abs (s $ Var 0)) (s[u/0])) =
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
   247
    (\<forall>s. R (Abs (lift s 0 $ Var 0)) s)"
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
   248
  apply (auto simp add: not_free_iff_lifted)
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
   249
  done
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
   250
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
   251
end