src/HOL/Isar_examples/NestedDatatype.thy
author wenzelm
Sat Apr 15 15:00:57 2000 +0200 (2000-04-15)
changeset 8717 20c42415c07d
parent 8676 4bf18b611a75
child 9659 b9cf6801f3da
permissions -rw-r--r--
plain ASCII;
     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 = 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     thus "?P (App b ts)"; by (simp add: o_def);
    46   next;
    47     show "?Q []"; by simp;
    48   next;
    49     fix t ts;
    50     assume "?P t" "?Q ts"; thus "?Q (t # ts)"; by simp;
    51   qed;
    52 qed;
    53 
    54 
    55 subsection {* Alternative induction *};
    56 
    57 theorem term_induct' [case_names Var App]:
    58  "(!!a. P (Var a)) ==> (!!b ts. list_all P ts ==> P (App b ts)) ==> P t";
    59 proof -;
    60   assume var: "!!a. P (Var a)";
    61   assume app: "!!b ts. list_all P ts ==> P (App b ts)";
    62   show ?thesis;
    63   proof (induct P t);
    64     fix a; show "P (Var a)"; by (rule var);
    65   next;
    66     fix b t ts; assume "list_all P ts";
    67     thus "P (App b ts)"; by (rule app);
    68   next;
    69     show "list_all P []"; by simp;
    70   next;
    71     fix t ts; assume "P t" "list_all P ts";
    72     thus "list_all P (t # ts)"; by simp;
    73   qed;
    74 qed;
    75 
    76 lemma
    77   "subst_term (subst_term f1 o f2) t = subst_term f1 (subst_term f2 t)"
    78   (is "?P t");
    79 proof (induct ?P t rule: term_induct');
    80   case Var;
    81   show "?P (Var a)"; by (simp add: o_def);
    82 next;
    83   case App;
    84   have "?this --> ?P (App b ts)";
    85     by (induct ts) simp_all;
    86   thus "..."; ..;
    87 qed;
    88 
    89 end;