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