1 |
1 |
2 header {* Nested datatypes *}; |
2 header {* Nested datatypes *} |
3 |
3 |
4 theory NestedDatatype = Main:; |
4 theory NestedDatatype = Main: |
5 |
5 |
6 subsection {* Terms and substitution *}; |
6 subsection {* Terms and substitution *} |
7 |
7 |
8 datatype ('a, 'b) "term" = |
8 datatype ('a, 'b) "term" = |
9 Var 'a |
9 Var 'a |
10 | App 'b "('a, 'b) term list"; |
10 | App 'b "('a, 'b) term list" |
11 |
11 |
12 consts |
12 consts |
13 subst_term :: "('a => ('a, 'b) term) => ('a, 'b) term => ('a, 'b) term" |
13 subst_term :: "('a => ('a, 'b) term) => ('a, 'b) term => ('a, 'b) term" |
14 subst_term_list :: |
14 subst_term_list :: |
15 "('a => ('a, 'b) term) => ('a, 'b) term list => ('a, 'b) term list"; |
15 "('a => ('a, 'b) term) => ('a, 'b) term list => ('a, 'b) term list" |
16 |
16 |
17 primrec (subst) |
17 primrec (subst) |
18 "subst_term f (Var a) = f a" |
18 "subst_term f (Var a) = f a" |
19 "subst_term f (App b ts) = App b (subst_term_list f ts)" |
19 "subst_term f (App b ts) = App b (subst_term_list f ts)" |
20 "subst_term_list f [] = []" |
20 "subst_term_list f [] = []" |
21 "subst_term_list f (t # ts) = subst_term f t # subst_term_list f ts"; |
21 "subst_term_list f (t # ts) = subst_term f t # subst_term_list f ts" |
22 |
22 |
23 |
23 |
24 text {* |
24 text {* |
25 \medskip A simple lemma about composition of substitutions. |
25 \medskip A simple lemma about composition of substitutions. |
26 *}; |
26 *} |
27 |
27 |
28 lemma |
28 lemma |
29 "subst_term (subst_term f1 o f2) t = |
29 "subst_term (subst_term f1 o f2) t = |
30 subst_term f1 (subst_term f2 t) & |
30 subst_term f1 (subst_term f2 t) & |
31 subst_term_list (subst_term f1 o f2) ts = |
31 subst_term_list (subst_term f1 o f2) ts = |
32 subst_term_list f1 (subst_term_list f2 ts)"; |
32 subst_term_list f1 (subst_term_list f2 ts)" |
33 by (induct t and ts rule: term.induct) simp_all; |
33 by (induct t and ts rule: term.induct) simp_all |
34 |
34 |
35 lemma "subst_term (subst_term f1 o f2) t = |
35 lemma "subst_term (subst_term f1 o f2) t = |
36 subst_term f1 (subst_term f2 t)"; |
36 subst_term f1 (subst_term f2 t)" |
37 proof -; |
37 proof - |
38 let "?P t" = ?thesis; |
38 let "?P t" = ?thesis |
39 let ?Q = "\\<lambda>ts. subst_term_list (subst_term f1 o f2) ts = |
39 let ?Q = "\<lambda>ts. subst_term_list (subst_term f1 o f2) ts = |
40 subst_term_list f1 (subst_term_list f2 ts)"; |
40 subst_term_list f1 (subst_term_list f2 ts)" |
41 show ?thesis; |
41 show ?thesis |
42 proof (induct t); |
42 proof (induct t) |
43 fix a; show "?P (Var a)"; by simp; |
43 fix a show "?P (Var a)" by simp |
44 next; |
44 next |
45 fix b ts; assume "?Q ts"; |
45 fix b ts assume "?Q ts" |
46 thus "?P (App b ts)"; by (simp add: o_def); |
46 thus "?P (App b ts)" by (simp add: o_def) |
47 next; |
47 next |
48 show "?Q []"; by simp; |
48 show "?Q []" by simp |
49 next; |
49 next |
50 fix t ts; |
50 fix t ts |
51 assume "?P t" "?Q ts"; thus "?Q (t # ts)"; by simp; |
51 assume "?P t" "?Q ts" thus "?Q (t # ts)" by simp |
52 qed; |
52 qed |
53 qed; |
53 qed |
54 |
54 |
55 |
55 |
56 subsection {* Alternative induction *}; |
56 subsection {* Alternative induction *} |
57 |
57 |
58 theorem term_induct' [case_names Var App]: |
58 theorem term_induct' [case_names Var App]: |
59 "(!!a. P (Var a)) ==> |
59 "(!!a. P (Var a)) ==> |
60 (!!b ts. list_all P ts ==> P (App b ts)) ==> P t"; |
60 (!!b ts. list_all P ts ==> P (App b ts)) ==> P t" |
61 proof -; |
61 proof - |
62 assume var: "!!a. P (Var a)"; |
62 assume var: "!!a. P (Var a)" |
63 assume app: "!!b ts. list_all P ts ==> P (App b ts)"; |
63 assume app: "!!b ts. list_all P ts ==> P (App b ts)" |
64 show ?thesis; |
64 show ?thesis |
65 proof (induct P t); |
65 proof (induct P t) |
66 fix a; show "P (Var a)"; by (rule var); |
66 fix a show "P (Var a)" by (rule var) |
67 next; |
67 next |
68 fix b t ts; assume "list_all P ts"; |
68 fix b t ts assume "list_all P ts" |
69 thus "P (App b ts)"; by (rule app); |
69 thus "P (App b ts)" by (rule app) |
70 next; |
70 next |
71 show "list_all P []"; by simp; |
71 show "list_all P []" by simp |
72 next; |
72 next |
73 fix t ts; assume "P t" "list_all P ts"; |
73 fix t ts assume "P t" "list_all P ts" |
74 thus "list_all P (t # ts)"; by simp; |
74 thus "list_all P (t # ts)" by simp |
75 qed; |
75 qed |
76 qed; |
76 qed |
77 |
77 |
78 lemma |
78 lemma |
79 "subst_term (subst_term f1 o f2) t = subst_term f1 (subst_term f2 t)" |
79 "subst_term (subst_term f1 o f2) t = subst_term f1 (subst_term f2 t)" |
80 (is "?P t"); |
80 (is "?P t") |
81 proof (induct (open) ?P t rule: term_induct'); |
81 proof (induct (open) ?P t rule: term_induct') |
82 case Var; |
82 case Var |
83 show "?P (Var a)"; by (simp add: o_def); |
83 show "?P (Var a)" by (simp add: o_def) |
84 next; |
84 next |
85 case App; |
85 case App |
86 have "?this --> ?P (App b ts)"; |
86 have "?this --> ?P (App b ts)" |
87 by (induct ts) simp_all; |
87 by (induct ts) simp_all |
88 thus "..."; ..; |
88 thus "..." .. |
89 qed; |
89 qed |
90 |
90 |
91 end; |
91 end |