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