src/HOL/Isar_examples/NestedDatatype.thy
author wenzelm
Sat Aug 19 12:44:39 2000 +0200 (2000-08-19)
changeset 9659 b9cf6801f3da
parent 8717 20c42415c07d
child 10007 64bf7da1994a
permissions -rw-r--r--
tuned;
     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;