src/HOL/Isar_examples/NestedDatatype.thy
author paulson
Tue Jun 28 15:27:45 2005 +0200 (2005-06-28)
changeset 16587 b34c8aa657a5
parent 16417 9bc16273c2d4
child 18153 a084aa91f701
permissions -rw-r--r--
Constant "If" is now local
     1 
     2 header {* Nested datatypes *}
     3 
     4 theory NestedDatatype imports Main begin
     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) 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 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 t rule: term_induct')
    82   case (Var a)
    83   show "?P (Var a)" by (simp add: o_def)
    84 next
    85   case (App b ts)
    86   thus "?P (App b ts)" by (induct ts) simp_all
    87 qed
    88 
    89 end