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 "listsp"} is equivalent to @{term "listall"}, 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 NF} 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