src/HOL/Lambda/NormalForm.thy
author wenzelm
Sat Oct 17 14:43:18 2009 +0200 (2009-10-17)
changeset 32960 69916a850301
parent 24537 57c7dfaa0153
child 33704 6aeb8454efc1
permissions -rw-r--r--
eliminated hard tabulators, guessing at each author's individual tab-width;
tuned headers;
berghofe@24537
     1
(*  Title:      HOL/Lambda/NormalForm.thy
berghofe@24537
     2
    Author:     Stefan Berghofer, TU Muenchen, 2003
berghofe@24537
     3
*)
berghofe@24537
     4
berghofe@24537
     5
header {* Inductive characterization of lambda terms in normal form *}
berghofe@24537
     6
berghofe@24537
     7
theory NormalForm
berghofe@24537
     8
imports ListBeta
berghofe@24537
     9
begin
berghofe@24537
    10
berghofe@24537
    11
subsection {* Terms in normal form *}
berghofe@24537
    12
berghofe@24537
    13
definition
berghofe@24537
    14
  listall :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> bool" where
berghofe@24537
    15
  "listall P xs \<equiv> (\<forall>i. i < length xs \<longrightarrow> P (xs ! i))"
berghofe@24537
    16
berghofe@24537
    17
declare listall_def [extraction_expand]
berghofe@24537
    18
berghofe@24537
    19
theorem listall_nil: "listall P []"
berghofe@24537
    20
  by (simp add: listall_def)
berghofe@24537
    21
berghofe@24537
    22
theorem listall_nil_eq [simp]: "listall P [] = True"
berghofe@24537
    23
  by (iprover intro: listall_nil)
berghofe@24537
    24
berghofe@24537
    25
theorem listall_cons: "P x \<Longrightarrow> listall P xs \<Longrightarrow> listall P (x # xs)"
berghofe@24537
    26
  apply (simp add: listall_def)
berghofe@24537
    27
  apply (rule allI impI)+
berghofe@24537
    28
  apply (case_tac i)
berghofe@24537
    29
  apply simp+
berghofe@24537
    30
  done
berghofe@24537
    31
berghofe@24537
    32
theorem listall_cons_eq [simp]: "listall P (x # xs) = (P x \<and> listall P xs)"
berghofe@24537
    33
  apply (rule iffI)
berghofe@24537
    34
  prefer 2
berghofe@24537
    35
  apply (erule conjE)
berghofe@24537
    36
  apply (erule listall_cons)
berghofe@24537
    37
  apply assumption
berghofe@24537
    38
  apply (unfold listall_def)
berghofe@24537
    39
  apply (rule conjI)
berghofe@24537
    40
  apply (erule_tac x=0 in allE)
berghofe@24537
    41
  apply simp
berghofe@24537
    42
  apply simp
berghofe@24537
    43
  apply (rule allI)
berghofe@24537
    44
  apply (erule_tac x="Suc i" in allE)
berghofe@24537
    45
  apply simp
berghofe@24537
    46
  done
berghofe@24537
    47
berghofe@24537
    48
lemma listall_conj1: "listall (\<lambda>x. P x \<and> Q x) xs \<Longrightarrow> listall P xs"
berghofe@24537
    49
  by (induct xs) simp_all
berghofe@24537
    50
berghofe@24537
    51
lemma listall_conj2: "listall (\<lambda>x. P x \<and> Q x) xs \<Longrightarrow> listall Q xs"
berghofe@24537
    52
  by (induct xs) simp_all
berghofe@24537
    53
berghofe@24537
    54
lemma listall_app: "listall P (xs @ ys) = (listall P xs \<and> listall P ys)"
berghofe@24537
    55
  apply (induct xs)
berghofe@24537
    56
   apply (rule iffI, simp, simp)
berghofe@24537
    57
  apply (rule iffI, simp, simp)
berghofe@24537
    58
  done
berghofe@24537
    59
berghofe@24537
    60
lemma listall_snoc [simp]: "listall P (xs @ [x]) = (listall P xs \<and> P x)"
berghofe@24537
    61
  apply (rule iffI)
berghofe@24537
    62
  apply (simp add: listall_app)+
berghofe@24537
    63
  done
berghofe@24537
    64
berghofe@24537
    65
lemma listall_cong [cong, extraction_expand]:
berghofe@24537
    66
  "xs = ys \<Longrightarrow> listall P xs = listall P ys"
berghofe@24537
    67
  -- {* Currently needed for strange technical reasons *}
berghofe@24537
    68
  by (unfold listall_def) simp
berghofe@24537
    69
berghofe@24537
    70
text {*
berghofe@24537
    71
@{term "listsp"} is equivalent to @{term "listall"}, but cannot be
berghofe@24537
    72
used for program extraction.
berghofe@24537
    73
*}
berghofe@24537
    74
berghofe@24537
    75
lemma listall_listsp_eq: "listall P xs = listsp P xs"
berghofe@24537
    76
  by (induct xs) (auto intro: listsp.intros)
berghofe@24537
    77
berghofe@24537
    78
inductive NF :: "dB \<Rightarrow> bool"
berghofe@24537
    79
where
berghofe@24537
    80
  App: "listall NF ts \<Longrightarrow> NF (Var x \<degree>\<degree> ts)"
berghofe@24537
    81
| Abs: "NF t \<Longrightarrow> NF (Abs t)"
berghofe@24537
    82
monos listall_def
berghofe@24537
    83
berghofe@24537
    84
lemma nat_eq_dec: "\<And>n::nat. m = n \<or> m \<noteq> n"
berghofe@24537
    85
  apply (induct m)
berghofe@24537
    86
  apply (case_tac n)
berghofe@24537
    87
  apply (case_tac [3] n)
berghofe@24537
    88
  apply (simp only: nat.simps, iprover?)+
berghofe@24537
    89
  done
berghofe@24537
    90
berghofe@24537
    91
lemma nat_le_dec: "\<And>n::nat. m < n \<or> \<not> (m < n)"
berghofe@24537
    92
  apply (induct m)
berghofe@24537
    93
  apply (case_tac n)
berghofe@24537
    94
  apply (case_tac [3] n)
berghofe@24537
    95
  apply (simp del: simp_thms, iprover?)+
berghofe@24537
    96
  done
berghofe@24537
    97
berghofe@24537
    98
lemma App_NF_D: assumes NF: "NF (Var n \<degree>\<degree> ts)"
berghofe@24537
    99
  shows "listall NF ts" using NF
berghofe@24537
   100
  by cases simp_all
berghofe@24537
   101
berghofe@24537
   102
berghofe@24537
   103
subsection {* Properties of @{text NF} *}
berghofe@24537
   104
berghofe@24537
   105
lemma Var_NF: "NF (Var n)"
berghofe@24537
   106
  apply (subgoal_tac "NF (Var n \<degree>\<degree> [])")
berghofe@24537
   107
   apply simp
berghofe@24537
   108
  apply (rule NF.App)
berghofe@24537
   109
  apply simp
berghofe@24537
   110
  done
berghofe@24537
   111
berghofe@24537
   112
lemma Abs_NF:
berghofe@24537
   113
  assumes NF: "NF (Abs t \<degree>\<degree> ts)"
berghofe@24537
   114
  shows "ts = []" using NF
berghofe@24537
   115
proof cases
berghofe@24537
   116
  case (App us i)
berghofe@24537
   117
  thus ?thesis by (simp add: Var_apps_neq_Abs_apps [THEN not_sym])
berghofe@24537
   118
next
berghofe@24537
   119
  case (Abs u)
berghofe@24537
   120
  thus ?thesis by simp
berghofe@24537
   121
qed
berghofe@24537
   122
berghofe@24537
   123
lemma subst_terms_NF: "listall NF ts \<Longrightarrow>
berghofe@24537
   124
    listall (\<lambda>t. \<forall>i j. NF (t[Var i/j])) ts \<Longrightarrow>
berghofe@24537
   125
    listall NF (map (\<lambda>t. t[Var i/j]) ts)"
berghofe@24537
   126
  by (induct ts) simp_all
berghofe@24537
   127
berghofe@24537
   128
lemma subst_Var_NF: "NF t \<Longrightarrow> NF (t[Var i/j])"
berghofe@24537
   129
  apply (induct arbitrary: i j set: NF)
berghofe@24537
   130
  apply simp
berghofe@24537
   131
  apply (frule listall_conj1)
berghofe@24537
   132
  apply (drule listall_conj2)
berghofe@24537
   133
  apply (drule_tac i=i and j=j in subst_terms_NF)
berghofe@24537
   134
  apply assumption
berghofe@24537
   135
  apply (rule_tac m=x and n=j in nat_eq_dec [THEN disjE, standard])
berghofe@24537
   136
  apply simp
berghofe@24537
   137
  apply (erule NF.App)
berghofe@24537
   138
  apply (rule_tac m=j and n=x in nat_le_dec [THEN disjE, standard])
berghofe@24537
   139
  apply simp
berghofe@24537
   140
  apply (iprover intro: NF.App)
berghofe@24537
   141
  apply simp
berghofe@24537
   142
  apply (iprover intro: NF.App)
berghofe@24537
   143
  apply simp
berghofe@24537
   144
  apply (iprover intro: NF.Abs)
berghofe@24537
   145
  done
berghofe@24537
   146
berghofe@24537
   147
lemma app_Var_NF: "NF t \<Longrightarrow> \<exists>t'. t \<degree> Var i \<rightarrow>\<^sub>\<beta>\<^sup>* t' \<and> NF t'"
berghofe@24537
   148
  apply (induct set: NF)
berghofe@24537
   149
  apply (simplesubst app_last)  --{*Using @{text subst} makes extraction fail*}
berghofe@24537
   150
  apply (rule exI)
berghofe@24537
   151
  apply (rule conjI)
berghofe@24537
   152
  apply (rule rtranclp.rtrancl_refl)
berghofe@24537
   153
  apply (rule NF.App)
berghofe@24537
   154
  apply (drule listall_conj1)
berghofe@24537
   155
  apply (simp add: listall_app)
berghofe@24537
   156
  apply (rule Var_NF)
berghofe@24537
   157
  apply (rule exI)
berghofe@24537
   158
  apply (rule conjI)
berghofe@24537
   159
  apply (rule rtranclp.rtrancl_into_rtrancl)
berghofe@24537
   160
  apply (rule rtranclp.rtrancl_refl)
berghofe@24537
   161
  apply (rule beta)
berghofe@24537
   162
  apply (erule subst_Var_NF)
berghofe@24537
   163
  done
berghofe@24537
   164
berghofe@24537
   165
lemma lift_terms_NF: "listall NF ts \<Longrightarrow>
berghofe@24537
   166
    listall (\<lambda>t. \<forall>i. NF (lift t i)) ts \<Longrightarrow>
berghofe@24537
   167
    listall NF (map (\<lambda>t. lift t i) ts)"
berghofe@24537
   168
  by (induct ts) simp_all
berghofe@24537
   169
berghofe@24537
   170
lemma lift_NF: "NF t \<Longrightarrow> NF (lift t i)"
berghofe@24537
   171
  apply (induct arbitrary: i set: NF)
berghofe@24537
   172
  apply (frule listall_conj1)
berghofe@24537
   173
  apply (drule listall_conj2)
berghofe@24537
   174
  apply (drule_tac i=i in lift_terms_NF)
berghofe@24537
   175
  apply assumption
berghofe@24537
   176
  apply (rule_tac m=x and n=i in nat_le_dec [THEN disjE, standard])
berghofe@24537
   177
  apply simp
berghofe@24537
   178
  apply (rule NF.App)
berghofe@24537
   179
  apply assumption
berghofe@24537
   180
  apply simp
berghofe@24537
   181
  apply (rule NF.App)
berghofe@24537
   182
  apply assumption
berghofe@24537
   183
  apply simp
berghofe@24537
   184
  apply (rule NF.Abs)
berghofe@24537
   185
  apply simp
berghofe@24537
   186
  done
berghofe@24537
   187
berghofe@24537
   188
text {*
berghofe@24537
   189
@{term NF} characterizes exactly the terms that are in normal form.
berghofe@24537
   190
*}
berghofe@24537
   191
  
berghofe@24537
   192
lemma NF_eq: "NF t = (\<forall>t'. \<not> t \<rightarrow>\<^sub>\<beta> t')"
berghofe@24537
   193
proof
berghofe@24537
   194
  assume "NF t"
berghofe@24537
   195
  then have "\<And>t'. \<not> t \<rightarrow>\<^sub>\<beta> t'"
berghofe@24537
   196
  proof induct
berghofe@24537
   197
    case (App ts t)
berghofe@24537
   198
    show ?case
berghofe@24537
   199
    proof
berghofe@24537
   200
      assume "Var t \<degree>\<degree> ts \<rightarrow>\<^sub>\<beta> t'"
berghofe@24537
   201
      then obtain rs where "ts => rs"
wenzelm@32960
   202
        by (iprover dest: head_Var_reduction)
berghofe@24537
   203
      with App show False
wenzelm@32960
   204
        by (induct rs arbitrary: ts) auto
berghofe@24537
   205
    qed
berghofe@24537
   206
  next
berghofe@24537
   207
    case (Abs t)
berghofe@24537
   208
    show ?case
berghofe@24537
   209
    proof
berghofe@24537
   210
      assume "Abs t \<rightarrow>\<^sub>\<beta> t'"
berghofe@24537
   211
      then show False using Abs by cases simp_all
berghofe@24537
   212
    qed
berghofe@24537
   213
  qed
berghofe@24537
   214
  then show "\<forall>t'. \<not> t \<rightarrow>\<^sub>\<beta> t'" ..
berghofe@24537
   215
next
berghofe@24537
   216
  assume H: "\<forall>t'. \<not> t \<rightarrow>\<^sub>\<beta> t'"
berghofe@24537
   217
  then show "NF t"
berghofe@24537
   218
  proof (induct t rule: Apps_dB_induct)
berghofe@24537
   219
    case (1 n ts)
berghofe@24537
   220
    then have "\<forall>ts'. \<not> ts => ts'"
berghofe@24537
   221
      by (iprover intro: apps_preserves_betas)
berghofe@24537
   222
    with 1(1) have "listall NF ts"
berghofe@24537
   223
      by (induct ts) auto
berghofe@24537
   224
    then show ?case by (rule NF.App)
berghofe@24537
   225
  next
berghofe@24537
   226
    case (2 u ts)
berghofe@24537
   227
    show ?case
berghofe@24537
   228
    proof (cases ts)
berghofe@24537
   229
      case Nil
berghofe@24537
   230
      from 2 have "\<forall>u'. \<not> u \<rightarrow>\<^sub>\<beta> u'"
wenzelm@32960
   231
        by (auto intro: apps_preserves_beta)
berghofe@24537
   232
      then have "NF u" by (rule 2)
berghofe@24537
   233
      then have "NF (Abs u)" by (rule NF.Abs)
berghofe@24537
   234
      with Nil show ?thesis by simp
berghofe@24537
   235
    next
berghofe@24537
   236
      case (Cons r rs)
berghofe@24537
   237
      have "Abs u \<degree> r \<rightarrow>\<^sub>\<beta> u[r/0]" ..
berghofe@24537
   238
      then have "Abs u \<degree> r \<degree>\<degree> rs \<rightarrow>\<^sub>\<beta> u[r/0] \<degree>\<degree> rs"
wenzelm@32960
   239
        by (rule apps_preserves_beta)
berghofe@24537
   240
      with Cons have "Abs u \<degree>\<degree> ts \<rightarrow>\<^sub>\<beta> u[r/0] \<degree>\<degree> rs"
wenzelm@32960
   241
        by simp
berghofe@24537
   242
      with 2 show ?thesis by iprover
berghofe@24537
   243
    qed
berghofe@24537
   244
  qed
berghofe@24537
   245
qed
berghofe@24537
   246
berghofe@24537
   247
end