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