nipkow@5261: (*  Title:      HOL/Lambda/ListBeta.thy
nipkow@5261:     ID:         $Id$
nipkow@5261:     Author:     Tobias Nipkow
nipkow@5261:     Copyright   1998 TU Muenchen
nipkow@5261: *)
nipkow@5261: 
wenzelm@9811: header {* Lifting beta-reduction to lists *}
wenzelm@9811: 
haftmann@16417: theory ListBeta imports ListApplication ListOrder begin
wenzelm@9762: 
wenzelm@9811: text {*
wenzelm@9811:   Lifting beta-reduction to lists of terms, reducing exactly one element.
wenzelm@9811: *}
wenzelm@9811: 
wenzelm@19363: abbreviation
wenzelm@21404:   list_beta :: "dB list => dB list => bool"  (infixl "=>" 50) where
wenzelm@19363:   "rs => ss == (rs, ss) : step1 beta"
wenzelm@9762: 
wenzelm@18513: lemma head_Var_reduction:
wenzelm@18513:   "Var n \<degree>\<degree> rs -> v \<Longrightarrow> \<exists>ss. rs => ss \<and> v = Var n \<degree>\<degree> ss"
wenzelm@20503:   apply (induct u == "Var n \<degree>\<degree> rs" v arbitrary: rs set: beta)
wenzelm@9762:      apply simp
wenzelm@9762:     apply (rule_tac xs = rs in rev_exhaust)
wenzelm@9762:      apply simp
wenzelm@18513:     apply (atomize, force intro: append_step1I)
wenzelm@9762:    apply (rule_tac xs = rs in rev_exhaust)
wenzelm@9762:     apply simp
wenzelm@9771:     apply (auto 0 3 intro: disjI2 [THEN append_step1I])
wenzelm@9762:   done
wenzelm@9762: 
wenzelm@18513: lemma apps_betasE [elim!]:
wenzelm@18513:   assumes major: "r \<degree>\<degree> rs -> s"
wenzelm@18513:     and cases: "!!r'. [| r -> r'; s = r' \<degree>\<degree> rs |] ==> R"
wenzelm@18513:       "!!rs'. [| rs => rs'; s = r \<degree>\<degree> rs' |] ==> R"
wenzelm@18513:       "!!t u us. [| r = Abs t; rs = u # us; s = t[u/0] \<degree>\<degree> us |] ==> R"
wenzelm@18513:   shows R
wenzelm@18513: proof -
wenzelm@18513:   from major have
wenzelm@18513:    "(\<exists>r'. r -> r' \<and> s = r' \<degree>\<degree> rs) \<or>
wenzelm@18513:     (\<exists>rs'. rs => rs' \<and> s = r \<degree>\<degree> rs') \<or>
wenzelm@18513:     (\<exists>t u us. r = Abs t \<and> rs = u # us \<and> s = t[u/0] \<degree>\<degree> us)"
wenzelm@20503:     apply (induct u == "r \<degree>\<degree> rs" s arbitrary: r rs set: beta)
wenzelm@18513:        apply (case_tac r)
wenzelm@18513:          apply simp
wenzelm@18513:         apply (simp add: App_eq_foldl_conv)
wenzelm@18513:         apply (split split_if_asm)
wenzelm@18513:          apply simp
wenzelm@18513:          apply blast
wenzelm@18513:         apply simp
wenzelm@18513:        apply (simp add: App_eq_foldl_conv)
wenzelm@18513:        apply (split split_if_asm)
wenzelm@18513:         apply simp
wenzelm@9762:        apply simp
wenzelm@18513:       apply (drule App_eq_foldl_conv [THEN iffD1])
nipkow@10653:       apply (split split_if_asm)
wenzelm@9762:        apply simp
wenzelm@9762:        apply blast
wenzelm@18513:       apply (force intro!: disjI1 [THEN append_step1I])
wenzelm@18513:      apply (drule App_eq_foldl_conv [THEN iffD1])
nipkow@10653:      apply (split split_if_asm)
wenzelm@9762:       apply simp
wenzelm@18513:       apply blast
wenzelm@18513:      apply (clarify, auto 0 3 intro!: exI intro: append_step1I)
wenzelm@18513:     done
wenzelm@18513:   with cases show ?thesis by blast
wenzelm@18513: qed
wenzelm@9762: 
wenzelm@9762: lemma apps_preserves_beta [simp]:
wenzelm@12011:     "r -> s ==> r \<degree>\<degree> ss -> s \<degree>\<degree> ss"
wenzelm@18241:   by (induct ss rule: rev_induct) auto
wenzelm@9762: 
wenzelm@9762: lemma apps_preserves_beta2 [simp]:
wenzelm@12011:     "r ->> s ==> r \<degree>\<degree> ss ->> s \<degree>\<degree> ss"
wenzelm@18241:   apply (induct set: rtrancl)
wenzelm@9762:    apply blast
wenzelm@9762:   apply (blast intro: apps_preserves_beta rtrancl_into_rtrancl)
wenzelm@9762:   done
wenzelm@9762: 
wenzelm@18241: lemma apps_preserves_betas [simp]:
wenzelm@18241:     "rs => ss \<Longrightarrow> r \<degree>\<degree> rs -> r \<degree>\<degree> ss"
wenzelm@20503:   apply (induct rs arbitrary: ss rule: rev_induct)
wenzelm@9762:    apply simp
wenzelm@9762:   apply simp
wenzelm@9762:   apply (rule_tac xs = ss in rev_exhaust)
wenzelm@9762:    apply simp
wenzelm@9762:   apply simp
wenzelm@9762:   apply (drule Snoc_step1_SnocD)
wenzelm@9762:   apply blast
wenzelm@9762:   done
nipkow@5261: 
wenzelm@11639: end