1(* Title: HOL/Proofs/Lambda/ListApplication.thy 2 Author: Tobias Nipkow 3 Copyright 1998 TU Muenchen 4*) 5 6section \<open>Application of a term to a list of terms\<close> 7 8theory ListApplication imports Lambda begin 9 10abbreviation 11 list_application :: "dB => dB list => dB" (infixl "\<degree>\<degree>" 150) where 12 "t \<degree>\<degree> ts == foldl (\<degree>) t ts" 13 14lemma apps_eq_tail_conv [iff]: "(r \<degree>\<degree> ts = s \<degree>\<degree> ts) = (r = s)" 15 by (induct ts rule: rev_induct) auto 16 17lemma Var_eq_apps_conv [iff]: "(Var m = s \<degree>\<degree> ss) = (Var m = s \<and> ss = [])" 18 by (induct ss arbitrary: s) auto 19 20lemma 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 29lemma 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 37lemma 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 41lemma 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 44lemma 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 53lemma 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 57lemma 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 65lemma 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 77lemma size_apps [simp]: 78 "size (r \<degree>\<degree> rs) = size r + foldl (+) 0 (map size rs) + length rs" 79 by (induct rs rule: rev_induct) auto 80 81lemma lem0: "[| (0::nat) < k; m <= n |] ==> m < n + k" 82 by simp 83 84lemma 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 88lemma 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 92lemma app_last: "(t \<degree>\<degree> ts) \<degree> u = t \<degree>\<degree> (ts @ [u])" 93 by simp 94 95 96text \<open>\medskip A customized induction schema for \<open>\<degree>\<degree>\<close>.\<close> 97 98lemma 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_sum_list_rev) 114 apply (fastforce simp add: sum_list_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_sum_list_rev) 130 apply (simp add: member_le_sum_list) 131 done 132 133theorem 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 143end 144 145