(* Title: HOL/Proofs/Lambda/NormalForm.thy
Author: Stefan Berghofer, TU Muenchen, 2003
*)
section \<open>Inductive characterization of lambda terms in normal form\<close>
theory NormalForm
imports ListBeta
begin
subsection \<open>Terms in normal form\<close>
definition
listall :: "('a \ bool) \ 'a list \ bool" where
"listall P xs \ (\i. i < length xs \ P (xs ! i))"
declare listall_def [extraction_expand_def]
theorem listall_nil: "listall P []"
by (simp add: listall_def)
theorem listall_nil_eq [simp]: "listall P [] = True"
by (iprover intro: listall_nil)
theorem listall_cons: "P x \ listall P xs \ listall P (x # xs)"
apply (simp add: listall_def)
apply (rule allI impI)+
apply (case_tac i)
apply simp+
done
theorem listall_cons_eq [simp]: "listall P (x # xs) = (P x \ listall P xs)"
apply (rule iffI)
prefer 2
apply (erule conjE)
apply (erule listall_cons)
apply assumption
apply (unfold listall_def)
apply (rule conjI)
apply (erule_tac x=0 in allE)
apply simp
apply simp
apply (rule allI)
apply (erule_tac x="Suc i" in allE)
apply simp
done
lemma listall_conj1: "listall (\x. P x \ Q x) xs \ listall P xs"
by (induct xs) simp_all
lemma listall_conj2: "listall (\x. P x \ Q x) xs \ listall Q xs"
by (induct xs) simp_all
lemma listall_app: "listall P (xs @ ys) = (listall P xs \ listall P ys)"
apply (induct xs)
apply (rule iffI, simp, simp)
apply (rule iffI, simp, simp)
done
lemma listall_snoc [simp]: "listall P (xs @ [x]) = (listall P xs \ P x)"
apply (rule iffI)
apply (simp add: listall_app)+
done
lemma listall_cong [cong, extraction_expand]:
"xs = ys \ listall P xs = listall P ys"
\<comment> \<open>Currently needed for strange technical reasons\<close>
by (unfold listall_def) simp
text \<open>
\<^term>\<open>listsp\<close> is equivalent to \<^term>\<open>listall\<close>, but cannot be
used for program extraction.
\<close>
lemma listall_listsp_eq: "listall P xs = listsp P xs"
by (induct xs) (auto intro: listsp.intros)
inductive NF :: "dB \ bool"
where
App: "listall NF ts \ NF (Var x \\ ts)"
| Abs: "NF t \ NF (Abs t)"
monos listall_def
lemma nat_eq_dec: "\n::nat. m = n \ m \ n"
apply (induct m)
apply (case_tac n)
apply (case_tac [3] n)
apply (simp only: nat.simps, iprover?)+
done
lemma nat_le_dec: "\n::nat. m < n \ \ (m < n)"
apply (induct m)
apply (case_tac n)
apply (case_tac [3] n)
apply (simp del: simp_thms subst_all, iprover?)+
done
lemma App_NF_D: assumes NF: "NF (Var n \\ ts)"
shows "listall NF ts" using NF
by cases simp_all
subsection \<open>Properties of \<open>NF\<close>\<close>
lemma Var_NF: "NF (Var n)"
apply (subgoal_tac "NF (Var n \\ [])")
apply simp
apply (rule NF.App)
apply simp
done
lemma Abs_NF:
assumes NF: "NF (Abs t \\ ts)"
shows "ts = []" using NF
proof cases
case (App us i)
thus ?thesis by (simp add: Var_apps_neq_Abs_apps [THEN not_sym])
next
case (Abs u)
thus ?thesis by simp
qed
lemma subst_terms_NF: "listall NF ts \
listall (\<lambda>t. \<forall>i j. NF (t[Var i/j])) ts \<Longrightarrow>
listall NF (map (\<lambda>t. t[Var i/j]) ts)"
by (induct ts) simp_all
lemma subst_Var_NF: "NF t \ NF (t[Var i/j])"
apply (induct arbitrary: i j set: NF)
apply simp
apply (frule listall_conj1)
apply (drule listall_conj2)
apply (drule_tac i=i and j=j in subst_terms_NF)
apply assumption
apply (rule_tac m1=x and n1=j in nat_eq_dec [THEN disjE])
apply simp
apply (erule NF.App)
apply (rule_tac m1=j and n1=x in nat_le_dec [THEN disjE])
apply simp
apply (iprover intro: NF.App)
apply simp
apply (iprover intro: NF.App)
apply simp
apply (iprover intro: NF.Abs)
done
lemma app_Var_NF: "NF t \ \t'. t \ Var i \\<^sub>\\<^sup>* t' \ NF t'"
apply (induct set: NF)
apply (simplesubst app_last) \<comment> \<open>Using \<open>subst\<close> makes extraction fail\<close>
apply (rule exI)
apply (rule conjI)
apply (rule rtranclp.rtrancl_refl)
apply (rule NF.App)
apply (drule listall_conj1)
apply (simp add: listall_app)
apply (rule Var_NF)
apply (rule exI)
apply (rule conjI)
apply (rule rtranclp.rtrancl_into_rtrancl)
apply (rule rtranclp.rtrancl_refl)
apply (rule beta)
apply (erule subst_Var_NF)
done
lemma lift_terms_NF: "listall NF ts \
listall (\<lambda>t. \<forall>i. NF (lift t i)) ts \<Longrightarrow>
listall NF (map (\<lambda>t. lift t i) ts)"
by (induct ts) simp_all
lemma lift_NF: "NF t \ NF (lift t i)"
apply (induct arbitrary: i set: NF)
apply (frule listall_conj1)
apply (drule listall_conj2)
apply (drule_tac i=i in lift_terms_NF)
apply assumption
apply (rule_tac m1=x and n1=i in nat_le_dec [THEN disjE])
apply simp
apply (rule NF.App)
apply assumption
apply simp
apply (rule NF.App)
apply assumption
apply simp
apply (rule NF.Abs)
apply simp
done
text \<open>
\<^term>\<open>NF\<close> characterizes exactly the terms that are in normal form.
\<close>
lemma NF_eq: "NF t = (\t'. \ t \\<^sub>\ t')"
proof
assume "NF t"
then have "\t'. \ t \\<^sub>\ t'"
proof induct
case (App ts t)
show ?case
proof
assume "Var t \\ ts \\<^sub>\ t'"
then obtain rs where "ts => rs"
by (iprover dest: head_Var_reduction)
with App show False
by (induct rs arbitrary: ts) auto
qed
next
case (Abs t)
show ?case
proof
assume "Abs t \\<^sub>\ t'"
then show False using Abs by cases simp_all
qed
qed
then show "\t'. \ t \\<^sub>\ t'" ..
next
assume H: "\t'. \ t \\<^sub>\ t'"
then show "NF t"
proof (induct t rule: Apps_dB_induct)
case (1 n ts)
then have "\ts'. \ ts => ts'"
by (iprover intro: apps_preserves_betas)
with 1(1) have "listall NF ts"
by (induct ts) auto
then show ?case by (rule NF.App)
next
case (2 u ts)
show ?case
proof (cases ts)
case Nil
from 2 have "\u'. \ u \\<^sub>\ u'"
by (auto intro: apps_preserves_beta)
then have "NF u" by (rule 2)
then have "NF (Abs u)" by (rule NF.Abs)
with Nil show ?thesis by simp
next
case (Cons r rs)
have "Abs u \ r \\<^sub>\ u[r/0]" ..
then have "Abs u \ r \\ rs \\<^sub>\ u[r/0] \\ rs"
by (rule apps_preserves_beta)
with Cons have "Abs u \\ ts \\<^sub>\ u[r/0] \\ rs"
by simp
with 2 show ?thesis by iprover
qed
qed
qed
end
¤ Dauer der Verarbeitung: 0.1 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
