src/HOL/Isar_Examples/Nested_Datatype.thy
 author nipkow Mon Jan 30 21:49:41 2012 +0100 (2012-01-30) changeset 46372 6fa9cdb8b850 parent 37671 fa53d267dab3 child 55656 eb07b0acbebc permissions -rw-r--r--
```     1 header {* Nested datatypes *}
```
```     2
```
```     3 theory Nested_Datatype
```
```     4 imports Main
```
```     5 begin
```
```     6
```
```     7 subsection {* Terms and substitution *}
```
```     8
```
```     9 datatype ('a, 'b) "term" =
```
```    10     Var 'a
```
```    11   | App 'b "('a, 'b) term list"
```
```    12
```
```    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
```
```    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"
```
```    21
```
```    22 lemmas subst_simps = subst_term_subst_term_list.simps
```
```    23
```
```    24 text {* \medskip A simple lemma about composition of substitutions. *}
```
```    25
```
```    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)"
```
```    32   by (induct t and ts) simp_all
```
```    33
```
```    34 lemma "subst_term (subst_term f1 o f2) t =
```
```    35     subst_term f1 (subst_term f2 t)"
```
```    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"
```
```    45     then show "?P (App b ts)"
```
```    46       by (simp only: subst_simps)
```
```    47   next
```
```    48     show "?Q []" by simp
```
```    49   next
```
```    50     fix t ts
```
```    51     assume "?P t" "?Q ts" then show "?Q (t # ts)"
```
```    52       by (simp only: subst_simps)
```
```    53   qed
```
```    54 qed
```
```    55
```
```    56
```
```    57 subsection {* Alternative induction *}
```
```    58
```
```    59 theorem term_induct' [case_names Var App]:
```
```    60   assumes var: "!!a. P (Var a)"
```
```    61     and app: "!!b ts. (\<forall>t \<in> set ts. P t) ==> P (App b ts)"
```
```    62   shows "P t"
```
```    63 proof (induct t)
```
```    64   fix a show "P (Var a)" by (rule var)
```
```    65 next
```
```    66   fix b t ts assume "\<forall>t \<in> set ts. P t"
```
```    67   then show "P (App b ts)" by (rule app)
```
```    68 next
```
```    69   show "\<forall>t \<in> set []. P t" by simp
```
```    70 next
```
```    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
```
```    73 qed
```
```    74
```
```    75 lemma
```
```    76   "subst_term (subst_term f1 o f2) t = subst_term f1 (subst_term f2 t)"
```
```    77 proof (induct t rule: term_induct')
```
```    78   case (Var a)
```
```    79   show ?case by (simp add: o_def)
```
```    80 next
```
```    81   case (App b ts)
```
```    82   then show ?case by (induct ts) simp_all
```
```    83 qed
```
```    84
```
```    85 end
```