1 section \<open>Nested datatypes\<close> |
|
2 |
|
3 theory Nested_Datatype |
|
4 imports Main |
|
5 begin |
|
6 |
|
7 subsection \<open>Terms and substitution\<close> |
|
8 |
|
9 datatype ('a, 'b) "term" = |
|
10 Var 'a |
|
11 | App 'b "('a, 'b) term list" |
|
12 |
|
13 primrec subst_term :: "('a \<Rightarrow> ('a, 'b) term) \<Rightarrow> ('a, 'b) term \<Rightarrow> ('a, 'b) term" |
|
14 and subst_term_list :: "('a \<Rightarrow> ('a, 'b) term) \<Rightarrow> ('a, 'b) term list \<Rightarrow> ('a, 'b) term list" |
|
15 where |
|
16 "subst_term f (Var a) = f a" |
|
17 | "subst_term f (App b ts) = App b (subst_term_list f ts)" |
|
18 | "subst_term_list f [] = []" |
|
19 | "subst_term_list f (t # ts) = subst_term f t # subst_term_list f ts" |
|
20 |
|
21 lemmas subst_simps = subst_term.simps subst_term_list.simps |
|
22 |
|
23 text \<open>\<^medskip> A simple lemma about composition of substitutions.\<close> |
|
24 |
|
25 lemma |
|
26 "subst_term (subst_term f1 \<circ> f2) t = |
|
27 subst_term f1 (subst_term f2 t)" |
|
28 and |
|
29 "subst_term_list (subst_term f1 \<circ> f2) ts = |
|
30 subst_term_list f1 (subst_term_list f2 ts)" |
|
31 by (induct t and ts rule: subst_term.induct subst_term_list.induct) simp_all |
|
32 |
|
33 lemma "subst_term (subst_term f1 \<circ> f2) t = subst_term f1 (subst_term f2 t)" |
|
34 proof - |
|
35 let "?P t" = ?thesis |
|
36 let ?Q = "\<lambda>ts. subst_term_list (subst_term f1 \<circ> f2) ts = |
|
37 subst_term_list f1 (subst_term_list f2 ts)" |
|
38 show ?thesis |
|
39 proof (induct t rule: subst_term.induct) |
|
40 show "?P (Var a)" for a by simp |
|
41 show "?P (App b ts)" if "?Q ts" for b ts |
|
42 using that by (simp only: subst_simps) |
|
43 show "?Q []" by simp |
|
44 show "?Q (t # ts)" if "?P t" "?Q ts" for t ts |
|
45 using that by (simp only: subst_simps) |
|
46 qed |
|
47 qed |
|
48 |
|
49 |
|
50 subsection \<open>Alternative induction\<close> |
|
51 |
|
52 lemma "subst_term (subst_term f1 \<circ> f2) t = subst_term f1 (subst_term f2 t)" |
|
53 proof (induct t rule: term.induct) |
|
54 case (Var a) |
|
55 show ?case by (simp add: o_def) |
|
56 next |
|
57 case (App b ts) |
|
58 then show ?case by (induct ts) simp_all |
|
59 qed |
|
60 |
|
61 end |
|