(* Title: HOL/Proofs/Lambda/ListBeta.thy
Author: Tobias Nipkow
Copyright 1998 TU Muenchen
*)
section \<open>Lifting beta-reduction to lists\<close>
theory ListBeta imports ListApplication ListOrder begin
text \<open>
Lifting beta-reduction to lists of terms, reducing exactly one element.
\<close>
abbreviation
list_beta :: "dB list => dB list => bool" (infixl "=>" 50) where
"rs => ss == step1 beta rs ss"
lemma head_Var_reduction:
"Var n \\ rs \\<^sub>\ v \ \ss. rs => ss \ v = Var n \\ ss"
apply (induct u == "Var n \\ rs" v arbitrary: rs set: beta)
apply simp
apply (rule_tac xs = rs in rev_exhaust)
apply simp
apply (atomize, force intro: append_step1I)
apply (rule_tac xs = rs in rev_exhaust)
apply simp
apply (auto 0 3 intro: disjI2 [THEN append_step1I])
done
lemma apps_betasE [elim!]:
assumes major: "r \\ rs \\<^sub>\ s"
and cases: "!!r'. [| r \\<^sub>\ r'; s = r' \\ rs |] ==> R"
"!!rs'. [| rs => rs'; s = r \\ rs' |] ==> R"
"!!t u us. [| r = Abs t; rs = u # us; s = t[u/0] \\ us |] ==> R"
shows R
proof -
from major have
"(\r'. r \\<^sub>\ r' \ s = r' \\ rs) \
(\<exists>rs'. rs => rs' \<and> s = r \<degree>\<degree> rs') \<or>
(\<exists>t u us. r = Abs t \<and> rs = u # us \<and> s = t[u/0] \<degree>\<degree> us)"
apply (induct u == "r \\ rs" s arbitrary: r rs set: beta)
apply (case_tac r)
apply simp
apply (simp add: App_eq_foldl_conv)
apply (split if_split_asm)
apply simp
apply blast
apply simp
apply (simp add: App_eq_foldl_conv)
apply (split if_split_asm)
apply simp
apply simp
apply (drule App_eq_foldl_conv [THEN iffD1])
apply (split if_split_asm)
apply simp
apply blast
apply (force intro!: disjI1 [THEN append_step1I])
apply (drule App_eq_foldl_conv [THEN iffD1])
apply (split if_split_asm)
apply simp
apply blast
apply (clarify, auto 0 3 intro!: exI intro: append_step1I)
done
with cases show ?thesis by blast
qed
lemma apps_preserves_beta [simp]:
"r \\<^sub>\ s ==> r \\ ss \\<^sub>\ s \\ ss"
by (induct ss rule: rev_induct) auto
lemma apps_preserves_beta2 [simp]:
"r \\<^sub>\\<^sup>* s ==> r \\ ss \\<^sub>\\<^sup>* s \\ ss"
apply (induct set: rtranclp)
apply blast
apply (blast intro: apps_preserves_beta rtranclp.rtrancl_into_rtrancl)
done
lemma apps_preserves_betas [simp]:
"rs => ss \ r \\ rs \\<^sub>\ r \\ ss"
apply (induct rs arbitrary: ss rule: rev_induct)
apply simp
apply simp
apply (rule_tac xs = ss in rev_exhaust)
apply simp
apply simp
apply (drule Snoc_step1_SnocD)
apply blast
done
end
¤ Dauer der Verarbeitung: 0.18 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.
|
