# Theory ListApplication

Up to index of Isabelle/HOL/Lambda

theory ListApplication
imports Lambda
begin

    (*  Title:      HOL/Lambda/ListApplication.thy
        ID:         $Id: ListApplication.thy,v 1.14 2005/06/17 14:13:08 haftmann Exp $
        Author:     Tobias Nipkow
        Copyright   1998 TU Muenchen
    *)

    header {* Application of a term to a list of terms *}

    theory ListApplication imports Lambda begin

    syntax
      "_list_application" :: "dB => dB list => dB"    (infixl "°°" 150)
    translations
      "t °° ts" == "foldl (op °) t ts"

    lemma apps_eq_tail_conv [iff]: "(r °° ts = s °° ts) = (r = s)"
      apply (induct_tac ts rule: rev_induct)
       apply auto
      done

    lemma Var_eq_apps_conv [iff]:
        "!!s. (Var m = s °° ss) = (Var m = s ∧ ss = [])"
      apply (induct ss)
       apply auto
      done

    lemma Var_apps_eq_Var_apps_conv [iff]:
        "!!ss. (Var m °° rs = Var n °° ss) = (m = n ∧ rs = ss)"
      apply (induct rs 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 = [])"
      apply (induct_tac ss rule: rev_induct)
       apply auto
      done

    lemma apps_eq_Abs_conv [iff]: "(s °° ss = Abs r) = (s = Abs r ∧ ss = [])"
      apply (induct_tac ss rule: rev_induct)
       apply auto
      done

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

    lemma Abs_App_neq_Var_apps [iff]:
        "∀s t. Abs s ° t ~= Var n °° ss"
      apply (induct_tac ss rule: rev_induct)
       apply auto
      done

    lemma Var_apps_neq_Abs_apps [iff]:
        "!!ts. Var n °° ts ~= Abs r °° ss"
      apply (induct ss 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_tac 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 (op +) 0 (map size rs) + length rs"
      apply (induct_tac rs rule: rev_induct)
       apply auto
      done

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

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

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

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

    text {* \medskip A customized induction schema for @{text "°°"}. *}

    lemma lem [rule_format (no_asm)]:
      "[| !!n ts. ∀t ∈ set ts. P t ==> P (Var n °° ts);
        !!u ts. [| P u; ∀t ∈ set ts. P t |] ==> P (Abs u °° ts)
      |] ==> ∀t. size t = n --> P t"
    proof -
      case rule_context
      show ?thesis
       apply (induct_tac n rule: nat_less_induct)
       apply (rule allI)
       apply (cut_tac t = t in ex_head_tail)
       apply clarify
       apply (erule disjE)
        apply clarify
        apply (rule prems)
        apply clarify
        apply (erule allE, erule impE)
          prefer 2
          apply (erule allE, erule mp, rule refl)
         apply simp
         apply (rule lem0)
          apply force
         apply (rule elem_le_sum)
         apply force
        apply clarify
        apply (rule prems)
         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 (rule elem_le_sum)
        apply force
        done
    qed

    theorem Apps_dB_induct:
      "[| !!n ts. ∀t ∈ set ts. P t ==> P (Var n °° ts);
        !!u ts. [| P u; ∀t ∈ set ts. P t |] ==> P (Abs u °° ts)
      |] ==> P t"
    proof -
      case rule_context
      show ?thesis
        apply (rule_tac t = t in lem)
          prefer 3
          apply (rule refl)
         apply (assumption | rule prems)+
        done
    qed

    end

lemma apps_eq_tail_conv:

      (r °° ts = s °° ts) = (r = s)

lemma Var_eq_apps_conv:

      (Var m = s °° ss) = (Var m = s ∧ ss = [])

lemma Var_apps_eq_Var_apps_conv:

      (Var m °° rs = Var n °° ss) = (m = n ∧ rs = ss)

lemma App_eq_foldl_conv:

      (r ° s = t °° ts) =
      (if ts = [] then r ° s = t else ∃ss. ts = ss @ [s] ∧ r = t °° ss)

lemma Abs_eq_apps_conv:

      (Abs r = s °° ss) = (Abs r = s ∧ ss = [])

lemma apps_eq_Abs_conv:

      (s °° ss = Abs r) = (s = Abs r ∧ ss = [])

lemma Abs_apps_eq_Abs_apps_conv:

      (Abs r °° rs = Abs s °° ss) = (r = s ∧ rs = ss)

lemma Abs_App_neq_Var_apps:

      ∀s t. Abs s ° t ≠ Var n °° ss

lemma Var_apps_neq_Abs_apps:

      Var n °° ts ≠ Abs r °° ss

lemma ex_head_tail:

      ∃ts h. t = h °° ts ∧ ((∃n. h = Var n) ∨ (∃u. h = Abs u))

lemma size_apps:

      size (r °° rs) = size r + foldl op + 0 (map size rs) + length rs

lemma lem0:

      [| 0 < k; m ≤ n |] ==> m < n + k

lemma lift_map:

      lift (t °° ts) i = lift t i °° map (%t. lift t i) ts

lemma subst_map:

      (t °° ts)[u/i] = t[u/i] °° map (%t. t[u/i]) ts

lemma app_last:

      (t °° ts) ° u = t °° (ts @ [u])

lemma lem:

      [| !!n ts. Ball (set ts) P ==> P (Var n °° ts);
         !!u ts. [| P u; Ball (set ts) P |] ==> P (Abs u °° ts); size t = n |]
      ==> P t

theorem Apps_dB_induct:

      [| !!n ts. ∀t∈set ts. P t ==> P (Var n °° ts);
         !!u ts. [| P u; ∀t∈set ts. P t |] ==> P (Abs u °° ts) |]
      ==> P t