12 "_list_application" :: "dB => dB list => dB" (infixl "\<degree>\<degree>" 150) |
12 "_list_application" :: "dB => dB list => dB" (infixl "\<degree>\<degree>" 150) |
13 translations |
13 translations |
14 "t \<degree>\<degree> ts" == "foldl (op \<degree>) t ts" |
14 "t \<degree>\<degree> ts" == "foldl (op \<degree>) t ts" |
15 |
15 |
16 lemma apps_eq_tail_conv [iff]: "(r \<degree>\<degree> ts = s \<degree>\<degree> ts) = (r = s)" |
16 lemma apps_eq_tail_conv [iff]: "(r \<degree>\<degree> ts = s \<degree>\<degree> ts) = (r = s)" |
17 apply (induct_tac ts rule: rev_induct) |
17 by (induct ts rule: rev_induct) auto |
18 apply auto |
|
19 done |
|
20 |
18 |
21 lemma Var_eq_apps_conv [iff]: |
19 lemma Var_eq_apps_conv [iff]: "(Var m = s \<degree>\<degree> ss) = (Var m = s \<and> ss = [])" |
22 "\<And>s. (Var m = s \<degree>\<degree> ss) = (Var m = s \<and> ss = [])" |
20 by (induct ss fixing: s) auto |
23 apply (induct ss) |
|
24 apply auto |
|
25 done |
|
26 |
21 |
27 lemma Var_apps_eq_Var_apps_conv [iff]: |
22 lemma Var_apps_eq_Var_apps_conv [iff]: |
28 "\<And>ss. (Var m \<degree>\<degree> rs = Var n \<degree>\<degree> ss) = (m = n \<and> rs = ss)" |
23 "(Var m \<degree>\<degree> rs = Var n \<degree>\<degree> ss) = (m = n \<and> rs = ss)" |
29 apply (induct rs rule: rev_induct) |
24 apply (induct rs fixing: ss rule: rev_induct) |
30 apply simp |
25 apply simp |
31 apply blast |
26 apply blast |
32 apply (induct_tac ss rule: rev_induct) |
27 apply (induct_tac ss rule: rev_induct) |
33 apply auto |
28 apply auto |
34 done |
29 done |
41 apply auto |
36 apply auto |
42 done |
37 done |
43 |
38 |
44 lemma Abs_eq_apps_conv [iff]: |
39 lemma Abs_eq_apps_conv [iff]: |
45 "(Abs r = s \<degree>\<degree> ss) = (Abs r = s \<and> ss = [])" |
40 "(Abs r = s \<degree>\<degree> ss) = (Abs r = s \<and> ss = [])" |
46 apply (induct_tac ss rule: rev_induct) |
41 by (induct ss rule: rev_induct) auto |
47 apply auto |
|
48 done |
|
49 |
42 |
50 lemma apps_eq_Abs_conv [iff]: "(s \<degree>\<degree> ss = Abs r) = (s = Abs r \<and> ss = [])" |
43 lemma apps_eq_Abs_conv [iff]: "(s \<degree>\<degree> ss = Abs r) = (s = Abs r \<and> ss = [])" |
51 apply (induct_tac ss rule: rev_induct) |
44 by (induct ss rule: rev_induct) auto |
52 apply auto |
|
53 done |
|
54 |
45 |
55 lemma Abs_apps_eq_Abs_apps_conv [iff]: |
46 lemma Abs_apps_eq_Abs_apps_conv [iff]: |
56 "\<And>ss. (Abs r \<degree>\<degree> rs = Abs s \<degree>\<degree> ss) = (r = s \<and> rs = ss)" |
47 "(Abs r \<degree>\<degree> rs = Abs s \<degree>\<degree> ss) = (r = s \<and> rs = ss)" |
57 apply (induct rs rule: rev_induct) |
48 apply (induct rs fixing: ss rule: rev_induct) |
58 apply simp |
49 apply simp |
59 apply blast |
50 apply blast |
60 apply (induct_tac ss rule: rev_induct) |
51 apply (induct_tac ss rule: rev_induct) |
61 apply auto |
52 apply auto |
62 done |
53 done |
63 |
54 |
64 lemma Abs_App_neq_Var_apps [iff]: |
55 lemma Abs_App_neq_Var_apps [iff]: |
65 "\<forall>s t. Abs s \<degree> t ~= Var n \<degree>\<degree> ss" |
56 "Abs s \<degree> t ~= Var n \<degree>\<degree> ss" |
66 apply (induct_tac ss rule: rev_induct) |
57 by (induct ss fixing: s t rule: rev_induct) auto |
67 apply auto |
|
68 done |
|
69 |
58 |
70 lemma Var_apps_neq_Abs_apps [iff]: |
59 lemma Var_apps_neq_Abs_apps [iff]: |
71 "\<And>ts. Var n \<degree>\<degree> ts ~= Abs r \<degree>\<degree> ss" |
60 "Var n \<degree>\<degree> ts ~= Abs r \<degree>\<degree> ss" |
72 apply (induct ss rule: rev_induct) |
61 apply (induct ss fixing: ts rule: rev_induct) |
73 apply simp |
62 apply simp |
74 apply (induct_tac ts rule: rev_induct) |
63 apply (induct_tac ts rule: rev_induct) |
75 apply auto |
64 apply auto |
76 done |
65 done |
77 |
66 |
78 lemma ex_head_tail: |
67 lemma ex_head_tail: |
79 "\<exists>ts h. t = h \<degree>\<degree> ts \<and> ((\<exists>n. h = Var n) \<or> (\<exists>u. h = Abs u))" |
68 "\<exists>ts h. t = h \<degree>\<degree> ts \<and> ((\<exists>n. h = Var n) \<or> (\<exists>u. h = Abs u))" |
80 apply (induct_tac t) |
69 apply (induct t) |
81 apply (rule_tac x = "[]" in exI) |
70 apply (rule_tac x = "[]" in exI) |
82 apply simp |
71 apply simp |
83 apply clarify |
72 apply clarify |
84 apply (rename_tac ts1 ts2 h1 h2) |
73 apply (rename_tac ts1 ts2 h1 h2) |
85 apply (rule_tac x = "ts1 @ [h2 \<degree>\<degree> ts2]" in exI) |
74 apply (rule_tac x = "ts1 @ [h2 \<degree>\<degree> ts2]" in exI) |
87 apply simp |
76 apply simp |
88 done |
77 done |
89 |
78 |
90 lemma size_apps [simp]: |
79 lemma size_apps [simp]: |
91 "size (r \<degree>\<degree> rs) = size r + foldl (op +) 0 (map size rs) + length rs" |
80 "size (r \<degree>\<degree> rs) = size r + foldl (op +) 0 (map size rs) + length rs" |
92 apply (induct_tac rs rule: rev_induct) |
81 by (induct rs rule: rev_induct) auto |
93 apply auto |
|
94 done |
|
95 |
82 |
96 lemma lem0: "[| (0::nat) < k; m <= n |] ==> m < n + k" |
83 lemma lem0: "[| (0::nat) < k; m <= n |] ==> m < n + k" |
97 apply simp |
84 by simp |
98 done |
|
99 |
85 |
100 lemma lift_map [simp]: |
86 lemma lift_map [simp]: |
101 "\<And>t. lift (t \<degree>\<degree> ts) i = lift t i \<degree>\<degree> map (\<lambda>t. lift t i) ts" |
87 "lift (t \<degree>\<degree> ts) i = lift t i \<degree>\<degree> map (\<lambda>t. lift t i) ts" |
102 by (induct ts) simp_all |
88 by (induct ts fixing: t) simp_all |
103 |
89 |
104 lemma subst_map [simp]: |
90 lemma subst_map [simp]: |
105 "\<And>t. subst (t \<degree>\<degree> ts) u i = subst t u i \<degree>\<degree> map (\<lambda>t. subst t u i) ts" |
91 "subst (t \<degree>\<degree> ts) u i = subst t u i \<degree>\<degree> map (\<lambda>t. subst t u i) ts" |
106 by (induct ts) simp_all |
92 by (induct ts fixing: t) simp_all |
107 |
93 |
108 lemma app_last: "(t \<degree>\<degree> ts) \<degree> u = t \<degree>\<degree> (ts @ [u])" |
94 lemma app_last: "(t \<degree>\<degree> ts) \<degree> u = t \<degree>\<degree> (ts @ [u])" |
109 by simp |
95 by simp |
110 |
96 |
111 |
97 |
112 text {* \medskip A customized induction schema for @{text "\<degree>\<degree>"}. *} |
98 text {* \medskip A customized induction schema for @{text "\<degree>\<degree>"}. *} |
113 |
99 |
114 lemma lem [rule_format (no_asm)]: |
100 lemma lem: |
115 "[| !!n ts. \<forall>t \<in> set ts. P t ==> P (Var n \<degree>\<degree> ts); |
101 assumes "!!n ts. \<forall>t \<in> set ts. P t ==> P (Var n \<degree>\<degree> ts)" |
116 !!u ts. [| P u; \<forall>t \<in> set ts. P t |] ==> P (Abs u \<degree>\<degree> ts) |
102 and "!!u ts. [| P u; \<forall>t \<in> set ts. P t |] ==> P (Abs u \<degree>\<degree> ts)" |
117 |] ==> \<forall>t. size t = n --> P t" |
103 shows "size t = n \<Longrightarrow> P t" |
118 proof - |
104 apply (induct n fixing: t rule: nat_less_induct) |
119 case rule_context |
105 apply (cut_tac t = t in ex_head_tail) |
120 show ?thesis |
106 apply clarify |
121 apply (induct_tac n rule: nat_less_induct) |
107 apply (erule disjE) |
122 apply (rule allI) |
|
123 apply (cut_tac t = t in ex_head_tail) |
|
124 apply clarify |
108 apply clarify |
125 apply (erule disjE) |
109 apply (rule prems) |
126 apply clarify |
110 apply clarify |
127 apply (rule prems) |
111 apply (erule allE, erule impE) |
128 apply clarify |
112 prefer 2 |
129 apply (erule allE, erule impE) |
113 apply (erule allE, erule mp, rule refl) |
130 prefer 2 |
114 apply simp |
131 apply (erule allE, erule mp, rule refl) |
115 apply (rule lem0) |
132 apply simp |
|
133 apply (rule lem0) |
|
134 apply force |
|
135 apply (rule elem_le_sum) |
|
136 apply force |
|
137 apply clarify |
|
138 apply (rule prems) |
|
139 apply (erule allE, erule impE) |
|
140 prefer 2 |
|
141 apply (erule allE, erule mp, rule refl) |
|
142 apply simp |
|
143 apply clarify |
|
144 apply (erule allE, erule impE) |
|
145 prefer 2 |
|
146 apply (erule allE, erule mp, rule refl) |
|
147 apply simp |
|
148 apply (rule le_imp_less_Suc) |
|
149 apply (rule trans_le_add1) |
|
150 apply (rule trans_le_add2) |
|
151 apply (rule elem_le_sum) |
|
152 apply force |
116 apply force |
153 done |
117 apply (rule elem_le_sum) |
154 qed |
118 apply force |
|
119 apply clarify |
|
120 apply (rule prems) |
|
121 apply (erule allE, erule impE) |
|
122 prefer 2 |
|
123 apply (erule allE, erule mp, rule refl) |
|
124 apply simp |
|
125 apply clarify |
|
126 apply (erule allE, erule impE) |
|
127 prefer 2 |
|
128 apply (erule allE, erule mp, rule refl) |
|
129 apply simp |
|
130 apply (rule le_imp_less_Suc) |
|
131 apply (rule trans_le_add1) |
|
132 apply (rule trans_le_add2) |
|
133 apply (rule elem_le_sum) |
|
134 apply force |
|
135 done |
155 |
136 |
156 theorem Apps_dB_induct: |
137 theorem Apps_dB_induct: |
157 "[| !!n ts. \<forall>t \<in> set ts. P t ==> P (Var n \<degree>\<degree> ts); |
138 assumes "!!n ts. \<forall>t \<in> set ts. P t ==> P (Var n \<degree>\<degree> ts)" |
158 !!u ts. [| P u; \<forall>t \<in> set ts. P t |] ==> P (Abs u \<degree>\<degree> ts) |
139 and "!!u ts. [| P u; \<forall>t \<in> set ts. P t |] ==> P (Abs u \<degree>\<degree> ts)" |
159 |] ==> P t" |
140 shows "P t" |
160 proof - |
141 apply (rule_tac t = t in lem) |
161 case rule_context |
142 prefer 3 |
162 show ?thesis |
143 apply (rule refl) |
163 apply (rule_tac t = t in lem) |
144 apply (assumption | rule prems)+ |
164 prefer 3 |
145 done |
165 apply (rule refl) |
|
166 apply (assumption | rule prems)+ |
|
167 done |
|
168 qed |
|
169 |
146 |
170 end |
147 end |