8 |
8 |
9 datatype ('a, 'b) "term" = |
9 datatype ('a, 'b) "term" = |
10 Var 'a |
10 Var 'a |
11 | App 'b "('a, 'b) term list" |
11 | App 'b "('a, 'b) term list" |
12 |
12 |
13 consts |
13 primrec subst_term :: "('a => ('a, 'b) term) => ('a, 'b) term => ('a, 'b) term" and |
14 subst_term :: "('a => ('a, 'b) term) => ('a, 'b) term => ('a, 'b) term" |
14 subst_term_list :: "('a => ('a, 'b) term) => ('a, 'b) term list => ('a, 'b) term list" where |
15 subst_term_list :: |
15 "subst_term f (Var a) = f a" |
16 "('a => ('a, 'b) term) => ('a, 'b) term list => ('a, 'b) term list" |
16 | "subst_term f (App b ts) = App b (subst_term_list f ts)" |
|
17 | "subst_term_list f [] = []" |
|
18 | "subst_term_list f (t # ts) = subst_term f t # subst_term_list f ts" |
17 |
19 |
18 primrec (subst) |
20 lemmas subst_simps = subst_term_subst_term_list.simps |
19 "subst_term f (Var a) = f a" |
|
20 "subst_term f (App b ts) = App b (subst_term_list f ts)" |
|
21 "subst_term_list f [] = []" |
|
22 "subst_term_list f (t # ts) = subst_term f t # subst_term_list f ts" |
|
23 |
|
24 |
21 |
25 text {* |
22 text {* |
26 \medskip A simple lemma about composition of substitutions. |
23 \medskip A simple lemma about composition of substitutions. |
27 *} |
24 *} |
28 |
25 |
42 proof (induct t) |
39 proof (induct t) |
43 fix a show "?P (Var a)" by simp |
40 fix a show "?P (Var a)" by simp |
44 next |
41 next |
45 fix b ts assume "?Q ts" |
42 fix b ts assume "?Q ts" |
46 then show "?P (App b ts)" |
43 then show "?P (App b ts)" |
47 by (simp only: subst.simps) |
44 by (simp only: subst_simps) |
48 next |
45 next |
49 show "?Q []" by simp |
46 show "?Q []" by simp |
50 next |
47 next |
51 fix t ts |
48 fix t ts |
52 assume "?P t" "?Q ts" then show "?Q (t # ts)" |
49 assume "?P t" "?Q ts" then show "?Q (t # ts)" |
53 by (simp only: subst.simps) |
50 by (simp only: subst_simps) |
54 qed |
51 qed |
55 qed |
52 qed |
56 |
53 |
57 |
54 |
58 subsection {* Alternative induction *} |
55 subsection {* Alternative induction *} |
59 |
56 |
60 theorem term_induct' [case_names Var App]: |
57 theorem term_induct' [case_names Var App]: |
61 assumes var: "!!a. P (Var a)" |
58 assumes var: "!!a. P (Var a)" |
62 and app: "!!b ts. list_all P ts ==> P (App b ts)" |
59 and app: "!!b ts. (\<forall>t \<in> set ts. P t) ==> P (App b ts)" |
63 shows "P t" |
60 shows "P t" |
64 proof (induct t) |
61 proof (induct t) |
65 fix a show "P (Var a)" by (rule var) |
62 fix a show "P (Var a)" by (rule var) |
66 next |
63 next |
67 fix b t ts assume "list_all P ts" |
64 fix b t ts assume "\<forall>t \<in> set ts. P t" |
68 then show "P (App b ts)" by (rule app) |
65 then show "P (App b ts)" by (rule app) |
69 next |
66 next |
70 show "list_all P []" by simp |
67 show "\<forall>t \<in> set []. P t" by simp |
71 next |
68 next |
72 fix t ts assume "P t" "list_all P ts" |
69 fix t ts assume "P t" "\<forall>t' \<in> set ts. P t'" |
73 then show "list_all P (t # ts)" by simp |
70 then show "\<forall>t' \<in> set (t # ts). P t'" by simp |
74 qed |
71 qed |
75 |
72 |
76 lemma |
73 lemma |
77 "subst_term (subst_term f1 o f2) t = subst_term f1 (subst_term f2 t)" |
74 "subst_term (subst_term f1 o f2) t = subst_term f1 (subst_term f2 t)" |
78 proof (induct t rule: term_induct') |
75 proof (induct t rule: term_induct') |