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