(*  Title:      HOL/Proofs/Lambda/ListBeta.thy
    Author:     Tobias Nipkow
    Copyright   1998 TU Muenchen
*)

section ‹Lifting beta-reduction to lists›

theory ListBeta imports ListApplication ListOrder begin

text ‹
 Lifting beta-reduction to lists of terms, reducing exactly one element.
 ›

abbreviation
  list_beta :: "dB list => dB list => bool"  (infixl ‹=>› 50) where
  "rs => ss == step1 beta rs ss"

lemma head_Var_reduction:
  "Var n 🚫🚫 rs →_\<beta> 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 →_\<beta> s"
    and cases: "!!r'. [| r →_\<beta> 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 →_\<beta> r' ∧ s = r' 🚫🚫 rs) ∨
    (∃rs'. rs => rs' ∧ s = r 🚫🚫 rs') ∨
    (∃t u us. r = Abs t ∧ rs = u # us ∧ s = t[u/0] 🚫🚫 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 →_\<beta> s ==> r 🚫🚫 ss →_\<beta> s 🚫🚫 ss"
  by (induct ss rule: rev_induct) auto

lemma apps_preserves_beta2 [simp]:
    "r →_\<beta>^* s ==> r 🚫🚫 ss →_\<beta>^* 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 →_\<beta> 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