src/HOL/Isar_Examples/Nested_Datatype.thy
author hoelzl
Tue Mar 26 12:20:58 2013 +0100 (2013-03-26)
changeset 51526 155263089e7b
parent 37671 fa53d267dab3
child 55656 eb07b0acbebc
permissions -rw-r--r--
move SEQ.thy and Lim.thy to Limits.thy
     1 header {* Nested datatypes *}
     2 
     3 theory Nested_Datatype
     4 imports Main
     5 begin
     6 
     7 subsection {* Terms and substitution *}
     8 
     9 datatype ('a, 'b) "term" =
    10     Var 'a
    11   | App 'b "('a, 'b) term list"
    12 
    13 primrec
    14   subst_term :: "('a => ('a, 'b) term) => ('a, 'b) term => ('a, 'b) term" and
    15   subst_term_list :: "('a => ('a, 'b) term) => ('a, 'b) term list => ('a, 'b) term list"
    16 where
    17   "subst_term f (Var a) = f a"
    18 | "subst_term f (App b ts) = App b (subst_term_list f ts)"
    19 | "subst_term_list f [] = []"
    20 | "subst_term_list f (t # ts) = subst_term f t # subst_term_list f ts"
    21 
    22 lemmas subst_simps = subst_term_subst_term_list.simps
    23 
    24 text {* \medskip A simple lemma about composition of substitutions. *}
    25 
    26 lemma
    27   "subst_term (subst_term f1 o f2) t =
    28     subst_term f1 (subst_term f2 t)"
    29   and
    30   "subst_term_list (subst_term f1 o f2) ts =
    31     subst_term_list f1 (subst_term_list f2 ts)"
    32   by (induct t and ts) simp_all
    33 
    34 lemma "subst_term (subst_term f1 o f2) t =
    35     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     then show "?P (App b ts)"
    46       by (simp only: subst_simps)
    47   next
    48     show "?Q []" by simp
    49   next
    50     fix t ts
    51     assume "?P t" "?Q ts" then show "?Q (t # ts)"
    52       by (simp only: subst_simps)
    53   qed
    54 qed
    55 
    56 
    57 subsection {* Alternative induction *}
    58 
    59 theorem term_induct' [case_names Var App]:
    60   assumes var: "!!a. P (Var a)"
    61     and app: "!!b ts. (\<forall>t \<in> set ts. P t) ==> P (App b ts)"
    62   shows "P t"
    63 proof (induct t)
    64   fix a show "P (Var a)" by (rule var)
    65 next
    66   fix b t ts assume "\<forall>t \<in> set ts. P t"
    67   then show "P (App b ts)" by (rule app)
    68 next
    69   show "\<forall>t \<in> set []. P t" by simp
    70 next
    71   fix t ts assume "P t" "\<forall>t' \<in> set ts. P t'"
    72   then show "\<forall>t' \<in> set (t # ts). P t'" by simp
    73 qed
    74 
    75 lemma
    76   "subst_term (subst_term f1 o f2) t = subst_term f1 (subst_term f2 t)"
    77 proof (induct t rule: term_induct')
    78   case (Var a)
    79   show ?case by (simp add: o_def)
    80 next
    81   case (App b ts)
    82   then show ?case by (induct ts) simp_all
    83 qed
    84 
    85 end