author | wenzelm |
Wed, 30 Dec 2015 18:25:39 +0100 | |
changeset 61986 | 2461779da2b8 |
parent 58889 | 5b7a9633cfa8 |
child 63882 | 018998c00003 |
permissions | -rw-r--r-- |
39157
b98909faaea8
more explicit HOL-Proofs sessions, including former ex/Hilbert_Classical.thy which works in parallel mode without the antiquotation option "margin" (which is still critical);
wenzelm
parents:
36862
diff
changeset
|
1 |
(* Title: HOL/Proofs/Lambda/ListApplication.thy |
5261 | 2 |
Author: Tobias Nipkow |
3 |
Copyright 1998 TU Muenchen |
|
9811
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9771
diff
changeset
|
4 |
*) |
5261 | 5 |
|
61986 | 6 |
section \<open>Application of a term to a list of terms\<close> |
5261 | 7 |
|
16417 | 8 |
theory ListApplication imports Lambda begin |
9771 | 9 |
|
19363 | 10 |
abbreviation |
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
20503
diff
changeset
|
11 |
list_application :: "dB => dB list => dB" (infixl "\<degree>\<degree>" 150) where |
19363 | 12 |
"t \<degree>\<degree> ts == foldl (op \<degree>) t ts" |
11943 | 13 |
|
12011 | 14 |
lemma apps_eq_tail_conv [iff]: "(r \<degree>\<degree> ts = s \<degree>\<degree> ts) = (r = s)" |
18241 | 15 |
by (induct ts rule: rev_induct) auto |
9771 | 16 |
|
18241 | 17 |
lemma Var_eq_apps_conv [iff]: "(Var m = s \<degree>\<degree> ss) = (Var m = s \<and> ss = [])" |
20503 | 18 |
by (induct ss arbitrary: s) auto |
9771 | 19 |
|
13915
28ccb51bd2f3
Eliminated most occurrences of rule_format attribute.
berghofe
parents:
12011
diff
changeset
|
20 |
lemma Var_apps_eq_Var_apps_conv [iff]: |
18241 | 21 |
"(Var m \<degree>\<degree> rs = Var n \<degree>\<degree> ss) = (m = n \<and> rs = ss)" |
20503 | 22 |
apply (induct rs arbitrary: ss rule: rev_induct) |
9771 | 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: |
|
12011 | 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))" |
|
9771 | 33 |
apply (rule_tac xs = ts in rev_exhaust) |
34 |
apply auto |
|
35 |
done |
|
36 |
||
37 |
lemma Abs_eq_apps_conv [iff]: |
|
12011 | 38 |
"(Abs r = s \<degree>\<degree> ss) = (Abs r = s \<and> ss = [])" |
18241 | 39 |
by (induct ss rule: rev_induct) auto |
9771 | 40 |
|
12011 | 41 |
lemma apps_eq_Abs_conv [iff]: "(s \<degree>\<degree> ss = Abs r) = (s = Abs r \<and> ss = [])" |
18241 | 42 |
by (induct ss rule: rev_induct) auto |
9771 | 43 |
|
44 |
lemma Abs_apps_eq_Abs_apps_conv [iff]: |
|
18241 | 45 |
"(Abs r \<degree>\<degree> rs = Abs s \<degree>\<degree> ss) = (r = s \<and> rs = ss)" |
20503 | 46 |
apply (induct rs arbitrary: ss rule: rev_induct) |
9771 | 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]: |
|
18257 | 54 |
"Abs s \<degree> t \<noteq> Var n \<degree>\<degree> ss" |
20503 | 55 |
by (induct ss arbitrary: s t rule: rev_induct) auto |
9771 | 56 |
|
13915
28ccb51bd2f3
Eliminated most occurrences of rule_format attribute.
berghofe
parents:
12011
diff
changeset
|
57 |
lemma Var_apps_neq_Abs_apps [iff]: |
18257 | 58 |
"Var n \<degree>\<degree> ts \<noteq> Abs r \<degree>\<degree> ss" |
20503 | 59 |
apply (induct ss arbitrary: ts rule: rev_induct) |
9771 | 60 |
apply simp |
61 |
apply (induct_tac ts rule: rev_induct) |
|
62 |
apply auto |
|
63 |
done |
|
5261 | 64 |
|
9771 | 65 |
lemma ex_head_tail: |
12011 | 66 |
"\<exists>ts h. t = h \<degree>\<degree> ts \<and> ((\<exists>n. h = Var n) \<or> (\<exists>u. h = Abs u))" |
18241 | 67 |
apply (induct t) |
9771 | 68 |
apply (rule_tac x = "[]" in exI) |
69 |
apply simp |
|
70 |
apply clarify |
|
71 |
apply (rename_tac ts1 ts2 h1 h2) |
|
12011 | 72 |
apply (rule_tac x = "ts1 @ [h2 \<degree>\<degree> ts2]" in exI) |
9771 | 73 |
apply simp |
74 |
apply simp |
|
75 |
done |
|
76 |
||
77 |
lemma size_apps [simp]: |
|
12011 | 78 |
"size (r \<degree>\<degree> rs) = size r + foldl (op +) 0 (map size rs) + length rs" |
18241 | 79 |
by (induct rs rule: rev_induct) auto |
9771 | 80 |
|
81 |
lemma lem0: "[| (0::nat) < k; m <= n |] ==> m < n + k" |
|
18241 | 82 |
by simp |
9771 | 83 |
|
14066 | 84 |
lemma lift_map [simp]: |
18241 | 85 |
"lift (t \<degree>\<degree> ts) i = lift t i \<degree>\<degree> map (\<lambda>t. lift t i) ts" |
20503 | 86 |
by (induct ts arbitrary: t) simp_all |
14066 | 87 |
|
88 |
lemma subst_map [simp]: |
|
18241 | 89 |
"subst (t \<degree>\<degree> ts) u i = subst t u i \<degree>\<degree> map (\<lambda>t. subst t u i) ts" |
20503 | 90 |
by (induct ts arbitrary: t) simp_all |
14066 | 91 |
|
92 |
lemma app_last: "(t \<degree>\<degree> ts) \<degree> u = t \<degree>\<degree> (ts @ [u])" |
|
93 |
by simp |
|
94 |
||
9811
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9771
diff
changeset
|
95 |
|
61986 | 96 |
text \<open>\medskip A customized induction schema for \<open>\<degree>\<degree>\<close>.\<close> |
9771 | 97 |
|
18241 | 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" |
|
20503 | 102 |
apply (induct n arbitrary: t rule: nat_less_induct) |
18241 | 103 |
apply (cut_tac t = t in ex_head_tail) |
104 |
apply clarify |
|
105 |
apply (erule disjE) |
|
106 |
apply clarify |
|
23464 | 107 |
apply (rule assms) |
9771 | 108 |
apply clarify |
18241 | 109 |
apply (erule allE, erule impE) |
110 |
prefer 2 |
|
111 |
apply (erule allE, erule mp, rule refl) |
|
112 |
apply simp |
|
57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
47397
diff
changeset
|
113 |
apply (simp only: foldl_conv_fold add.commute fold_plus_listsum_rev) |
47397
d654c73e4b12
no preference wrt. fold(l/r); prefer fold rather than foldr for iterating over lists in generated code
haftmann
parents:
39157
diff
changeset
|
114 |
apply (fastforce simp add: listsum_map_remove1) |
18241 | 115 |
apply clarify |
23464 | 116 |
apply (rule assms) |
18241 | 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) |
|
57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
47397
diff
changeset
|
129 |
apply (simp only: foldl_conv_fold add.commute fold_plus_listsum_rev) |
47397
d654c73e4b12
no preference wrt. fold(l/r); prefer fold rather than foldr for iterating over lists in generated code
haftmann
parents:
39157
diff
changeset
|
130 |
apply (simp add: member_le_listsum_nat) |
18241 | 131 |
done |
9771 | 132 |
|
9811
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
9771
diff
changeset
|
133 |
theorem Apps_dB_induct: |
18241 | 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) |
|
23464 | 140 |
using assms apply iprover+ |
18241 | 141 |
done |
5261 | 142 |
|
9870 | 143 |
end |
47397
d654c73e4b12
no preference wrt. fold(l/r); prefer fold rather than foldr for iterating over lists in generated code
haftmann
parents:
39157
diff
changeset
|
144 |