5261
|
1 |
(* Title: HOL/Lambda/ListApplication.ML
|
|
2 |
ID: $Id$
|
|
3 |
Author: Tobias Nipkow
|
|
4 |
Copyright 1998 TU Muenchen
|
|
5 |
*)
|
|
6 |
|
|
7 |
Goal "(r$$ts = s$$ts) = (r = s)";
|
5318
|
8 |
by (rev_induct_tac "ts" 1);
|
|
9 |
by (Auto_tac);
|
5261
|
10 |
qed "apps_eq_tail_conv";
|
|
11 |
AddIffs [apps_eq_tail_conv];
|
|
12 |
|
|
13 |
Goal "!s. (Var m = s$$ss) = (Var m = s & ss = [])";
|
5318
|
14 |
by (induct_tac "ss" 1);
|
|
15 |
by (Auto_tac);
|
5261
|
16 |
qed_spec_mp "Var_eq_apps_conv";
|
|
17 |
AddIffs [Var_eq_apps_conv];
|
|
18 |
|
|
19 |
Goal "!ss. ((Var m)$$rs = (Var n)$$ss) = (m=n & rs=ss)";
|
5318
|
20 |
by (rev_induct_tac "rs" 1);
|
|
21 |
by (Simp_tac 1);
|
|
22 |
by (Blast_tac 1);
|
|
23 |
by (rtac allI 1);
|
|
24 |
by (rev_induct_tac "ss" 1);
|
|
25 |
by (Auto_tac);
|
5261
|
26 |
qed_spec_mp "Var_apps_eq_Var_apps_conv";
|
|
27 |
AddIffs [Var_apps_eq_Var_apps_conv];
|
|
28 |
|
|
29 |
Goal "(r$s = t$$ts) = \
|
|
30 |
\ (if ts = [] then r$s = t \
|
|
31 |
\ else (? ss. ts = ss@[s] & r = t$$ss))";
|
5318
|
32 |
by (res_inst_tac [("xs","ts")] rev_exhaust 1);
|
|
33 |
by (Auto_tac);
|
5261
|
34 |
qed "App_eq_foldl_conv";
|
|
35 |
|
|
36 |
Goal "(Abs r = s$$ss) = (Abs r = s & ss=[])";
|
5318
|
37 |
by (rev_induct_tac "ss" 1);
|
|
38 |
by (Auto_tac);
|
5261
|
39 |
qed "Abs_eq_apps_conv";
|
|
40 |
AddIffs [Abs_eq_apps_conv];
|
|
41 |
|
|
42 |
Goal "(s$$ss = Abs r) = (s = Abs r & ss=[])";
|
5318
|
43 |
by (rev_induct_tac "ss" 1);
|
|
44 |
by (Auto_tac);
|
5261
|
45 |
qed "apps_eq_Abs_conv";
|
|
46 |
AddIffs [apps_eq_Abs_conv];
|
|
47 |
|
|
48 |
Goal "!ss. ((Abs r)$$rs = (Abs s)$$ss) = (r=s & rs=ss)";
|
5318
|
49 |
by (rev_induct_tac "rs" 1);
|
|
50 |
by (Simp_tac 1);
|
|
51 |
by (Blast_tac 1);
|
|
52 |
by (rtac allI 1);
|
|
53 |
by (rev_induct_tac "ss" 1);
|
|
54 |
by (Auto_tac);
|
5261
|
55 |
qed_spec_mp "Abs_apps_eq_Abs_apps_conv";
|
|
56 |
AddIffs [Abs_apps_eq_Abs_apps_conv];
|
|
57 |
|
|
58 |
Goal "!s t. Abs s $ t ~= (Var n)$$ss";
|
5318
|
59 |
by (rev_induct_tac "ss" 1);
|
|
60 |
by (Auto_tac);
|
5261
|
61 |
qed_spec_mp "Abs_App_neq_Var_apps";
|
|
62 |
AddIffs [Abs_App_neq_Var_apps];
|
|
63 |
|
|
64 |
Goal "!ts. Var n $$ ts ~= (Abs r)$$ss";
|
5318
|
65 |
by (rev_induct_tac "ss" 1);
|
|
66 |
by (Simp_tac 1);
|
|
67 |
by (rtac allI 1);
|
|
68 |
by (rev_induct_tac "ts" 1);
|
|
69 |
by (Auto_tac);
|
5261
|
70 |
qed_spec_mp "Var_apps_neq_Abs_apps";
|
|
71 |
AddIffs [Var_apps_neq_Abs_apps];
|
|
72 |
|
|
73 |
Goal "? ts h. t = h$$ts & ((? n. h = Var n) | (? u. h = Abs u))";
|
5318
|
74 |
by (induct_tac "t" 1);
|
|
75 |
by (res_inst_tac[("x","[]")] exI 1);
|
|
76 |
by (Simp_tac 1);
|
|
77 |
by (Clarify_tac 1);
|
|
78 |
by (rename_tac "ts1 ts2 h1 h2" 1);
|
|
79 |
by (res_inst_tac[("x","ts1@[h2$$ts2]")] exI 1);
|
|
80 |
by (Simp_tac 1);
|
|
81 |
by (Simp_tac 1);
|
5261
|
82 |
qed "ex_head_tail";
|
|
83 |
|
|
84 |
Goal "size(r$$rs) = size r + foldl (op +) 0 (map size rs) + length rs";
|
5318
|
85 |
by (rev_induct_tac "rs" 1);
|
|
86 |
by (Auto_tac);
|
5261
|
87 |
qed "size_apps";
|
|
88 |
Addsimps [size_apps];
|
|
89 |
|
|
90 |
Goal "[| 0 < k; m <= n |] ==> m < n+k";
|
6301
|
91 |
by (fast_arith_tac 1);
|
5261
|
92 |
val lemma = result();
|
|
93 |
|
|
94 |
(* a customized induction schema for $$ *)
|
|
95 |
|
|
96 |
val prems = Goal
|
|
97 |
"[| !!n ts. !t : set ts. P t ==> P((Var n)$$ts); \
|
|
98 |
\ !!u ts. [| P u; !t : set ts. P t |] ==> P((Abs u)$$ts) \
|
|
99 |
\|] ==> !t. size t = n --> P t";
|
5318
|
100 |
by (res_inst_tac [("n","n")] less_induct 1);
|
|
101 |
by (rtac allI 1);
|
|
102 |
by (cut_inst_tac [("t","t")] ex_head_tail 1);
|
|
103 |
by (Clarify_tac 1);
|
|
104 |
by (etac disjE 1);
|
|
105 |
by (Clarify_tac 1);
|
|
106 |
by (resolve_tac prems 1);
|
|
107 |
by (Clarify_tac 1);
|
|
108 |
by (EVERY[etac allE 1, etac impE 1, etac allE 2, etac mp 2, rtac refl 2]);
|
|
109 |
by (Simp_tac 1);
|
|
110 |
by (rtac lemma 1);
|
|
111 |
by (Force_tac 1);
|
|
112 |
by (rtac elem_le_sum 1);
|
|
113 |
by (Force_tac 1);
|
|
114 |
by (Clarify_tac 1);
|
|
115 |
by (resolve_tac prems 1);
|
|
116 |
by (EVERY[etac allE 1, etac impE 1, etac allE 2, etac mp 2, rtac refl 2]);
|
|
117 |
by (Simp_tac 1);
|
|
118 |
by (Clarify_tac 1);
|
|
119 |
by (EVERY[etac allE 1, etac impE 1, etac allE 2, etac mp 2, rtac refl 2]);
|
|
120 |
by (Simp_tac 1);
|
|
121 |
by (rtac le_imp_less_Suc 1);
|
|
122 |
by (rtac trans_le_add1 1);
|
|
123 |
by (rtac trans_le_add2 1);
|
|
124 |
by (rtac elem_le_sum 1);
|
|
125 |
by (Force_tac 1);
|
5261
|
126 |
val lemma = result() RS spec RS mp;
|
|
127 |
|
|
128 |
val prems = Goal
|
|
129 |
"[| !!n ts. !t : set ts. P t ==> P((Var n)$$ts); \
|
|
130 |
\ !!u ts. [| P u; !t : set ts. P t |] ==> P((Abs u)$$ts) \
|
|
131 |
\|] ==> P t";
|
5318
|
132 |
by (res_inst_tac [("x1","t")] lemma 1);
|
|
133 |
by (rtac refl 3);
|
|
134 |
by (REPEAT(ares_tac prems 1));
|
5261
|
135 |
qed "Apps_dB_induct";
|