10007

1 
header {* Nested datatypes *}

8676

2 

31758

3 
theory Nested_Datatype


4 
imports Main


5 
begin

8676

6 

10007

7 
subsection {* Terms and substitution *}

8676

8 


9 
datatype ('a, 'b) "term" =


10 
Var 'a

10007

11 
 App 'b "('a, 'b) term list"

8676

12 

37671

13 
primrec


14 
subst_term :: "('a => ('a, 'b) term) => ('a, 'b) term => ('a, 'b) term" and


15 
subst_term_list :: "('a => ('a, 'b) term) => ('a, 'b) term list => ('a, 'b) term list"


16 
where

37597

17 
"subst_term f (Var a) = f a"


18 
 "subst_term f (App b ts) = App b (subst_term_list f ts)"


19 
 "subst_term_list f [] = []"


20 
 "subst_term_list f (t # ts) = subst_term f t # subst_term_list f ts"

8676

21 

37597

22 
lemmas subst_simps = subst_term_subst_term_list.simps

8676

23 

37671

24 
text {* \medskip A simple lemma about composition of substitutions. *}

8676

25 

37671

26 
lemma


27 
"subst_term (subst_term f1 o f2) t =


28 
subst_term f1 (subst_term f2 t)"


29 
and


30 
"subst_term_list (subst_term f1 o f2) ts =


31 
subst_term_list f1 (subst_term_list f2 ts)"

11809

32 
by (induct t and ts) simp_all

8676

33 

9659

34 
lemma "subst_term (subst_term f1 o f2) t =

37671

35 
subst_term f1 (subst_term f2 t)"

10007

36 
proof 


37 
let "?P t" = ?thesis


38 
let ?Q = "\<lambda>ts. subst_term_list (subst_term f1 o f2) ts =


39 
subst_term_list f1 (subst_term_list f2 ts)"


40 
show ?thesis


41 
proof (induct t)


42 
fix a show "?P (Var a)" by simp


43 
next


44 
fix b ts assume "?Q ts"

23373

45 
then show "?P (App b ts)"

37597

46 
by (simp only: subst_simps)

10007

47 
next


48 
show "?Q []" by simp


49 
next


50 
fix t ts

23373

51 
assume "?P t" "?Q ts" then show "?Q (t # ts)"

37597

52 
by (simp only: subst_simps)

10007

53 
qed


54 
qed

8676

55 


56 

10007

57 
subsection {* Alternative induction *}

8676

58 


59 
theorem term_induct' [case_names Var App]:

18153

60 
assumes var: "!!a. P (Var a)"

37597

61 
and app: "!!b ts. (\<forall>t \<in> set ts. P t) ==> P (App b ts)"

18153

62 
shows "P t"


63 
proof (induct t)


64 
fix a show "P (Var a)" by (rule var)


65 
next

37597

66 
fix b t ts assume "\<forall>t \<in> set ts. P t"

23373

67 
then show "P (App b ts)" by (rule app)

18153

68 
next

37597

69 
show "\<forall>t \<in> set []. P t" by simp

18153

70 
next

37597

71 
fix t ts assume "P t" "\<forall>t' \<in> set ts. P t'"


72 
then show "\<forall>t' \<in> set (t # ts). P t'" by simp

10007

73 
qed

8676

74 

8717

75 
lemma


76 
"subst_term (subst_term f1 o f2) t = subst_term f1 (subst_term f2 t)"

11809

77 
proof (induct t rule: term_induct')


78 
case (Var a)

18153

79 
show ?case by (simp add: o_def)

10007

80 
next

11809

81 
case (App b ts)

23373

82 
then show ?case by (induct ts) simp_all

10007

83 
qed

8676

84 

10007

85 
end
