Theory ListApplication

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

section ‹Application of a term to a list of terms›

theory ListApplication imports Lambda begin

abbreviation
  list_application :: "dB => dB list => dB"  (infixl "°°" 150) where
  "t °° ts == foldl (°) t ts"

lemma apps_eq_tail_conv [iff]: "(r °° ts = s °° ts) = (r = s)"
  by (induct ts rule: rev_induct) auto

lemma Var_eq_apps_conv [iff]: "(Var m = s °° ss) = (Var m = s ∧ ss = [])"
  by (induct ss arbitrary: s) auto

lemma Var_apps_eq_Var_apps_conv [iff]:
    "(Var m °° rs = Var n °° ss) = (m = n ∧ rs = ss)"
  apply (induct rs arbitrary: ss rule: rev_induct)
   apply simp
   apply blast
  apply (induct_tac ss rule: rev_induct)
   apply auto
  done

lemma App_eq_foldl_conv:
  "(r ° s = t °° ts) =
    (if ts = [] then r ° s = t
    else (∃ss. ts = ss @ [s] ∧ r = t °° ss))"
  apply (rule_tac xs = ts in rev_exhaust)
   apply auto
  done

lemma Abs_eq_apps_conv [iff]:
    "(Abs r = s °° ss) = (Abs r = s ∧ ss = [])"
  by (induct ss rule: rev_induct) auto

lemma apps_eq_Abs_conv [iff]: "(s °° ss = Abs r) = (s = Abs r ∧ ss = [])"
  by (induct ss rule: rev_induct) auto

lemma Abs_apps_eq_Abs_apps_conv [iff]:
    "(Abs r °° rs = Abs s °° ss) = (r = s ∧ rs = ss)"
  apply (induct rs arbitrary: ss rule: rev_induct)
   apply simp
   apply blast
  apply (induct_tac ss rule: rev_induct)
   apply auto
  done

lemma Abs_App_neq_Var_apps [iff]:
    "Abs s ° t ≠ Var n °° ss"
  by (induct ss arbitrary: s t rule: rev_induct) auto

lemma Var_apps_neq_Abs_apps [iff]:
    "Var n °° ts ≠ Abs r °° ss"
  apply (induct ss arbitrary: ts rule: rev_induct)
   apply simp
  apply (induct_tac ts rule: rev_induct)
   apply auto
  done

lemma ex_head_tail:
  "∃ts h. t = h °° ts ∧ ((∃n. h = Var n) ∨ (∃u. h = Abs u))"
  apply (induct t)
    apply (rule_tac x = "[]" in exI)
    apply simp
   apply clarify
   apply (rename_tac ts1 ts2 h1 h2)
   apply (rule_tac x = "ts1 @ [h2 °° ts2]" in exI)
   apply simp
  apply simp
  done

lemma size_apps [simp]:
  "size (r °° rs) = size r + foldl (+) 0 (map size rs) + length rs"
  by (induct rs rule: rev_induct) auto

lemma lem0: "[| (0::nat) < k; m <= n |] ==> m < n + k"
  by simp

lemma lift_map [simp]:
    "lift (t °° ts) i = lift t i °° map (λt. lift t i) ts"
  by (induct ts arbitrary: t) simp_all

lemma subst_map [simp]:
    "subst (t °° ts) u i = subst t u i °° map (λt. subst t u i) ts"
  by (induct ts arbitrary: t) simp_all

lemma app_last: "(t °° ts) ° u = t °° (ts @ [u])"
  by simp


text ‹\medskip A customized induction schema for ‹°°›.›

lemma lem:
  assumes "!!n ts. ∀t ∈ set ts. P t ==> P (Var n °° ts)"
    and "!!u ts. [| P u; ∀t ∈ set ts. P t |] ==> P (Abs u °° ts)"
  shows "size t = n ⟹ P t"
  apply (induct n arbitrary: t rule: nat_less_induct)
  apply (cut_tac t = t in ex_head_tail)
  apply clarify
  apply (erule disjE)
   apply clarify
   apply (rule assms)
   apply clarify
   apply (erule allE, erule impE)
    prefer 2
    apply (erule allE, erule mp, rule refl)
   apply simp
   apply (simp only: foldl_conv_fold add.commute fold_plus_sum_list_rev)
   apply (fastforce simp add: sum_list_map_remove1)
  apply clarify
  apply (rule assms)
   apply (erule allE, erule impE)
    prefer 2
    apply (erule allE, erule mp, rule refl)
   apply simp
  apply clarify
  apply (erule allE, erule impE)
   prefer 2
   apply (erule allE, erule mp, rule refl)
  apply simp
  apply (rule le_imp_less_Suc)
  apply (rule trans_le_add1)
  apply (rule trans_le_add2)
  apply (simp only: foldl_conv_fold add.commute fold_plus_sum_list_rev)
  apply (simp add: member_le_sum_list)
  done

theorem Apps_dB_induct:
  assumes "!!n ts. ∀t ∈ set ts. P t ==> P (Var n °° ts)"
    and "!!u ts. [| P u; ∀t ∈ set ts. P t |] ==> P (Abs u °° ts)"
  shows "P t"
  apply (rule_tac t = t in lem)
    prefer 3
    apply (rule refl)
    using assms apply iprover+
  done

end