(* Title: HOL/Proofs/Lambda/InductTermi.thy
Author: Tobias Nipkow
Copyright 1998 TU Muenchen
Inductive characterization of terminating lambda terms. Goes back to
Raamsdonk & Severi. On normalization. CWI TR CS-R9545, 1995. Also
rediscovered by Matthes and Joachimski.
*)
section \<open>Inductive characterization of terminating lambda terms\<close>
theory InductTermi imports ListBeta begin
subsection \<open>Terminating lambda terms\<close>
inductive IT :: "dB => bool"
where
Var [intro]: "listsp IT rs ==> IT (Var n \\ rs)"
| Lambda [intro]: "IT r ==> IT (Abs r)"
| Beta [intro]: "IT ((r[s/0]) \\ ss) ==> IT s ==> IT ((Abs r \ s) \\ ss)"
subsection \<open>Every term in \<open>IT\<close> terminates\<close>
lemma double_induction_lemma [rule_format]:
"termip beta s ==> \t. termip beta t -->
(\<forall>r ss. t = r[s/0] \<degree>\<degree> ss --> termip beta (Abs r \<degree> s \<degree>\<degree> ss))"
apply (erule accp_induct)
apply (rule allI)
apply (rule impI)
apply (erule thin_rl)
apply (erule accp_induct)
apply clarify
apply (rule accp.accI)
apply (safe elim!: apps_betasE)
apply (blast intro: subst_preserves_beta apps_preserves_beta)
apply (blast intro: apps_preserves_beta2 subst_preserves_beta2 rtranclp_converseI
dest: accp_downwards) (* FIXME: acc_downwards can be replaced by acc(R ^* ) = acc(r) *)
apply (blast dest: apps_preserves_betas)
done
lemma IT_implies_termi: "IT t ==> termip beta t"
apply (induct set: IT)
apply (drule rev_predicate1D [OF _ listsp_mono [where B="termip beta"]])
apply (fast intro!: predicate1I)
apply (drule lists_accD)
apply (erule accp_induct)
apply (rule accp.accI)
apply (blast dest: head_Var_reduction)
apply (erule accp_induct)
apply (rule accp.accI)
apply blast
apply (blast intro: double_induction_lemma)
done
subsection \<open>Every terminating term is in \<open>IT\<close>\<close>
declare Var_apps_neq_Abs_apps [symmetric, simp]
lemma [simp, THEN not_sym, simp]: "Var n \\ ss \ Abs r \ s \\ ts"
by (simp add: foldl_Cons [symmetric] del: foldl_Cons)
lemma [simp]:
"(Abs r \ s \\ ss = Abs r' \ s' \\ ss') = (r = r' \ s = s' \ ss = ss')"
by (simp add: foldl_Cons [symmetric] del: foldl_Cons)
inductive_cases [elim!]:
"IT (Var n \\ ss)"
"IT (Abs t)"
"IT (Abs r \ s \\ ts)"
theorem termi_implies_IT: "termip beta r ==> IT r"
apply (erule accp_induct)
apply (rename_tac r)
apply (erule thin_rl)
apply (erule rev_mp)
apply simp
apply (rule_tac t = r in Apps_dB_induct)
apply clarify
apply (rule IT.intros)
apply clarify
apply (drule bspec, assumption)
apply (erule mp)
apply clarify
apply (drule_tac r=beta in conversepI)
apply (drule_tac r="beta\\" in ex_step1I, assumption)
apply clarify
apply (rename_tac us)
apply (erule_tac x = "Var n \\ us" in allE)
apply force
apply (rename_tac u ts)
apply (case_tac ts)
apply simp
apply blast
apply (rename_tac s ss)
apply simp
apply clarify
apply (rule IT.intros)
apply (blast intro: apps_preserves_beta)
apply (erule mp)
apply clarify
apply (rename_tac t)
apply (erule_tac x = "Abs u \ t \\ ss" in allE)
apply force
done
end
¤ Dauer der Verarbeitung: 0.20 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.
|
