equal
deleted
inserted
replaced
1 (* Title: HOL/Proofs/Lambda/NormalForm.thy |
1 (* Title: HOL/Proofs/Lambda/NormalForm.thy |
2 Author: Stefan Berghofer, TU Muenchen, 2003 |
2 Author: Stefan Berghofer, TU Muenchen, 2003 |
3 *) |
3 *) |
4 |
4 |
5 section {* Inductive characterization of lambda terms in normal form *} |
5 section \<open>Inductive characterization of lambda terms in normal form\<close> |
6 |
6 |
7 theory NormalForm |
7 theory NormalForm |
8 imports ListBeta |
8 imports ListBeta |
9 begin |
9 begin |
10 |
10 |
11 subsection {* Terms in normal form *} |
11 subsection \<open>Terms in normal form\<close> |
12 |
12 |
13 definition |
13 definition |
14 listall :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> bool" where |
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))" |
15 "listall P xs \<equiv> (\<forall>i. i < length xs \<longrightarrow> P (xs ! i))" |
16 |
16 |
62 apply (simp add: listall_app)+ |
62 apply (simp add: listall_app)+ |
63 done |
63 done |
64 |
64 |
65 lemma listall_cong [cong, extraction_expand]: |
65 lemma listall_cong [cong, extraction_expand]: |
66 "xs = ys \<Longrightarrow> listall P xs = listall P ys" |
66 "xs = ys \<Longrightarrow> listall P xs = listall P ys" |
67 -- {* Currently needed for strange technical reasons *} |
67 \<comment> \<open>Currently needed for strange technical reasons\<close> |
68 by (unfold listall_def) simp |
68 by (unfold listall_def) simp |
69 |
69 |
70 text {* |
70 text \<open> |
71 @{term "listsp"} is equivalent to @{term "listall"}, but cannot be |
71 @{term "listsp"} is equivalent to @{term "listall"}, but cannot be |
72 used for program extraction. |
72 used for program extraction. |
73 *} |
73 \<close> |
74 |
74 |
75 lemma listall_listsp_eq: "listall P xs = listsp P xs" |
75 lemma listall_listsp_eq: "listall P xs = listsp P xs" |
76 by (induct xs) (auto intro: listsp.intros) |
76 by (induct xs) (auto intro: listsp.intros) |
77 |
77 |
78 inductive NF :: "dB \<Rightarrow> bool" |
78 inductive NF :: "dB \<Rightarrow> bool" |
98 lemma App_NF_D: assumes NF: "NF (Var n \<degree>\<degree> ts)" |
98 lemma App_NF_D: assumes NF: "NF (Var n \<degree>\<degree> ts)" |
99 shows "listall NF ts" using NF |
99 shows "listall NF ts" using NF |
100 by cases simp_all |
100 by cases simp_all |
101 |
101 |
102 |
102 |
103 subsection {* Properties of @{text NF} *} |
103 subsection \<open>Properties of \<open>NF\<close>\<close> |
104 |
104 |
105 lemma Var_NF: "NF (Var n)" |
105 lemma Var_NF: "NF (Var n)" |
106 apply (subgoal_tac "NF (Var n \<degree>\<degree> [])") |
106 apply (subgoal_tac "NF (Var n \<degree>\<degree> [])") |
107 apply simp |
107 apply simp |
108 apply (rule NF.App) |
108 apply (rule NF.App) |
144 apply (iprover intro: NF.Abs) |
144 apply (iprover intro: NF.Abs) |
145 done |
145 done |
146 |
146 |
147 lemma app_Var_NF: "NF t \<Longrightarrow> \<exists>t'. t \<degree> Var i \<rightarrow>\<^sub>\<beta>\<^sup>* t' \<and> NF t'" |
147 lemma 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) |
148 apply (induct set: NF) |
149 apply (simplesubst app_last) --{*Using @{text subst} makes extraction fail*} |
149 apply (simplesubst app_last) \<comment>\<open>Using \<open>subst\<close> makes extraction fail\<close> |
150 apply (rule exI) |
150 apply (rule exI) |
151 apply (rule conjI) |
151 apply (rule conjI) |
152 apply (rule rtranclp.rtrancl_refl) |
152 apply (rule rtranclp.rtrancl_refl) |
153 apply (rule NF.App) |
153 apply (rule NF.App) |
154 apply (drule listall_conj1) |
154 apply (drule listall_conj1) |
183 apply simp |
183 apply simp |
184 apply (rule NF.Abs) |
184 apply (rule NF.Abs) |
185 apply simp |
185 apply simp |
186 done |
186 done |
187 |
187 |
188 text {* |
188 text \<open> |
189 @{term NF} characterizes exactly the terms that are in normal form. |
189 @{term NF} characterizes exactly the terms that are in normal form. |
190 *} |
190 \<close> |
191 |
191 |
192 lemma NF_eq: "NF t = (\<forall>t'. \<not> t \<rightarrow>\<^sub>\<beta> t')" |
192 lemma NF_eq: "NF t = (\<forall>t'. \<not> t \<rightarrow>\<^sub>\<beta> t')" |
193 proof |
193 proof |
194 assume "NF t" |
194 assume "NF t" |
195 then have "\<And>t'. \<not> t \<rightarrow>\<^sub>\<beta> t'" |
195 then have "\<And>t'. \<not> t \<rightarrow>\<^sub>\<beta> t'" |