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