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