src/HOL/Proofs/Lambda/ListApplication.thy
author wenzelm
Thu May 24 17:25:53 2012 +0200 (2012-05-24)
changeset 47988 e4b69e10b990
parent 47397 d654c73e4b12
child 57512 cc97b347b301
permissions -rw-r--r--
tuned proofs;
     1 (*  Title:      HOL/Proofs/Lambda/ListApplication.thy
     2     Author:     Tobias Nipkow
     3     Copyright   1998 TU Muenchen
     4 *)
     5 
     6 header {* Application of a term to a list of terms *}
     7 
     8 theory ListApplication imports Lambda begin
     9 
    10 abbreviation
    11   list_application :: "dB => dB list => dB"  (infixl "\<degree>\<degree>" 150) where
    12   "t \<degree>\<degree> ts == foldl (op \<degree>) t ts"
    13 
    14 lemma apps_eq_tail_conv [iff]: "(r \<degree>\<degree> ts = s \<degree>\<degree> ts) = (r = s)"
    15   by (induct ts rule: rev_induct) auto
    16 
    17 lemma Var_eq_apps_conv [iff]: "(Var m = s \<degree>\<degree> ss) = (Var m = s \<and> ss = [])"
    18   by (induct ss arbitrary: s) auto
    19 
    20 lemma Var_apps_eq_Var_apps_conv [iff]:
    21     "(Var m \<degree>\<degree> rs = Var n \<degree>\<degree> ss) = (m = n \<and> rs = ss)"
    22   apply (induct rs arbitrary: ss rule: rev_induct)
    23    apply simp
    24    apply blast
    25   apply (induct_tac ss rule: rev_induct)
    26    apply auto
    27   done
    28 
    29 lemma App_eq_foldl_conv:
    30   "(r \<degree> s = t \<degree>\<degree> ts) =
    31     (if ts = [] then r \<degree> s = t
    32     else (\<exists>ss. ts = ss @ [s] \<and> r = t \<degree>\<degree> ss))"
    33   apply (rule_tac xs = ts in rev_exhaust)
    34    apply auto
    35   done
    36 
    37 lemma Abs_eq_apps_conv [iff]:
    38     "(Abs r = s \<degree>\<degree> ss) = (Abs r = s \<and> ss = [])"
    39   by (induct ss rule: rev_induct) auto
    40 
    41 lemma apps_eq_Abs_conv [iff]: "(s \<degree>\<degree> ss = Abs r) = (s = Abs r \<and> ss = [])"
    42   by (induct ss rule: rev_induct) auto
    43 
    44 lemma Abs_apps_eq_Abs_apps_conv [iff]:
    45     "(Abs r \<degree>\<degree> rs = Abs s \<degree>\<degree> ss) = (r = s \<and> rs = ss)"
    46   apply (induct rs arbitrary: ss rule: rev_induct)
    47    apply simp
    48    apply blast
    49   apply (induct_tac ss rule: rev_induct)
    50    apply auto
    51   done
    52 
    53 lemma Abs_App_neq_Var_apps [iff]:
    54     "Abs s \<degree> t \<noteq> Var n \<degree>\<degree> ss"
    55   by (induct ss arbitrary: s t rule: rev_induct) auto
    56 
    57 lemma Var_apps_neq_Abs_apps [iff]:
    58     "Var n \<degree>\<degree> ts \<noteq> Abs r \<degree>\<degree> ss"
    59   apply (induct ss arbitrary: ts rule: rev_induct)
    60    apply simp
    61   apply (induct_tac ts rule: rev_induct)
    62    apply auto
    63   done
    64 
    65 lemma ex_head_tail:
    66   "\<exists>ts h. t = h \<degree>\<degree> ts \<and> ((\<exists>n. h = Var n) \<or> (\<exists>u. h = Abs u))"
    67   apply (induct t)
    68     apply (rule_tac x = "[]" in exI)
    69     apply simp
    70    apply clarify
    71    apply (rename_tac ts1 ts2 h1 h2)
    72    apply (rule_tac x = "ts1 @ [h2 \<degree>\<degree> ts2]" in exI)
    73    apply simp
    74   apply simp
    75   done
    76 
    77 lemma size_apps [simp]:
    78   "size (r \<degree>\<degree> rs) = size r + foldl (op +) 0 (map size rs) + length rs"
    79   by (induct rs rule: rev_induct) auto
    80 
    81 lemma lem0: "[| (0::nat) < k; m <= n |] ==> m < n + k"
    82   by simp
    83 
    84 lemma lift_map [simp]:
    85     "lift (t \<degree>\<degree> ts) i = lift t i \<degree>\<degree> map (\<lambda>t. lift t i) ts"
    86   by (induct ts arbitrary: t) simp_all
    87 
    88 lemma subst_map [simp]:
    89     "subst (t \<degree>\<degree> ts) u i = subst t u i \<degree>\<degree> map (\<lambda>t. subst t u i) ts"
    90   by (induct ts arbitrary: t) simp_all
    91 
    92 lemma app_last: "(t \<degree>\<degree> ts) \<degree> u = t \<degree>\<degree> (ts @ [u])"
    93   by simp
    94 
    95 
    96 text {* \medskip A customized induction schema for @{text "\<degree>\<degree>"}. *}
    97 
    98 lemma lem:
    99   assumes "!!n ts. \<forall>t \<in> set ts. P t ==> P (Var n \<degree>\<degree> ts)"
   100     and "!!u ts. [| P u; \<forall>t \<in> set ts. P t |] ==> P (Abs u \<degree>\<degree> ts)"
   101   shows "size t = n \<Longrightarrow> P t"
   102   apply (induct n arbitrary: t rule: nat_less_induct)
   103   apply (cut_tac t = t in ex_head_tail)
   104   apply clarify
   105   apply (erule disjE)
   106    apply clarify
   107    apply (rule assms)
   108    apply clarify
   109    apply (erule allE, erule impE)
   110     prefer 2
   111     apply (erule allE, erule mp, rule refl)
   112    apply simp
   113    apply (simp only: foldl_conv_fold add_commute fold_plus_listsum_rev)
   114    apply (fastforce simp add: listsum_map_remove1)
   115   apply clarify
   116   apply (rule assms)
   117    apply (erule allE, erule impE)
   118     prefer 2
   119     apply (erule allE, erule mp, rule refl)
   120    apply simp
   121   apply clarify
   122   apply (erule allE, erule impE)
   123    prefer 2
   124    apply (erule allE, erule mp, rule refl)
   125   apply simp
   126   apply (rule le_imp_less_Suc)
   127   apply (rule trans_le_add1)
   128   apply (rule trans_le_add2)
   129   apply (simp only: foldl_conv_fold add_commute fold_plus_listsum_rev)
   130   apply (simp add: member_le_listsum_nat)
   131   done
   132 
   133 theorem Apps_dB_induct:
   134   assumes "!!n ts. \<forall>t \<in> set ts. P t ==> P (Var n \<degree>\<degree> ts)"
   135     and "!!u ts. [| P u; \<forall>t \<in> set ts. P t |] ==> P (Abs u \<degree>\<degree> ts)"
   136   shows "P t"
   137   apply (rule_tac t = t in lem)
   138     prefer 3
   139     apply (rule refl)
   140     using assms apply iprover+
   141   done
   142 
   143 end
   144