src/HOL/Isar_examples/NestedDatatype.thy
changeset 10007 64bf7da1994a
parent 9659 b9cf6801f3da
child 10458 df4e182c0fcd
     1.1 --- a/src/HOL/Isar_examples/NestedDatatype.thy	Sun Sep 17 22:15:08 2000 +0200
     1.2 +++ b/src/HOL/Isar_examples/NestedDatatype.thy	Sun Sep 17 22:19:02 2000 +0200
     1.3 @@ -1,91 +1,91 @@
     1.4  
     1.5 -header {* Nested datatypes *};
     1.6 +header {* Nested datatypes *}
     1.7  
     1.8 -theory NestedDatatype = Main:;
     1.9 +theory NestedDatatype = Main:
    1.10  
    1.11 -subsection {* Terms and substitution *};
    1.12 +subsection {* Terms and substitution *}
    1.13  
    1.14  datatype ('a, 'b) "term" =
    1.15      Var 'a
    1.16 -  | App 'b "('a, 'b) term list";
    1.17 +  | App 'b "('a, 'b) term list"
    1.18  
    1.19  consts
    1.20    subst_term :: "('a => ('a, 'b) term) => ('a, 'b) term => ('a, 'b) term"
    1.21    subst_term_list ::
    1.22 -    "('a => ('a, 'b) term) => ('a, 'b) term list => ('a, 'b) term list";
    1.23 +    "('a => ('a, 'b) term) => ('a, 'b) term list => ('a, 'b) term list"
    1.24  
    1.25  primrec (subst)
    1.26    "subst_term f (Var a) = f a"
    1.27    "subst_term f (App b ts) = App b (subst_term_list f ts)"
    1.28    "subst_term_list f [] = []"
    1.29 -  "subst_term_list f (t # ts) = subst_term f t # subst_term_list f ts";
    1.30 +  "subst_term_list f (t # ts) = subst_term f t # subst_term_list f ts"
    1.31  
    1.32  
    1.33  text {*
    1.34   \medskip A simple lemma about composition of substitutions.
    1.35 -*};
    1.36 +*}
    1.37  
    1.38  lemma
    1.39     "subst_term (subst_term f1 o f2) t =
    1.40        subst_term f1 (subst_term f2 t) &
    1.41      subst_term_list (subst_term f1 o f2) ts =
    1.42 -      subst_term_list f1 (subst_term_list f2 ts)";
    1.43 -  by (induct t and ts rule: term.induct) simp_all;
    1.44 +      subst_term_list f1 (subst_term_list f2 ts)"
    1.45 +  by (induct t and ts rule: term.induct) simp_all
    1.46  
    1.47  lemma "subst_term (subst_term f1 o f2) t =
    1.48 -  subst_term f1 (subst_term f2 t)";
    1.49 -proof -;
    1.50 -  let "?P t" = ?thesis;
    1.51 -  let ?Q = "\\<lambda>ts. subst_term_list (subst_term f1 o f2) ts =
    1.52 -    subst_term_list f1 (subst_term_list f2 ts)";
    1.53 -  show ?thesis;
    1.54 -  proof (induct t);
    1.55 -    fix a; show "?P (Var a)"; by simp;
    1.56 -  next;
    1.57 -    fix b ts; assume "?Q ts";
    1.58 -    thus "?P (App b ts)"; by (simp add: o_def);
    1.59 -  next;
    1.60 -    show "?Q []"; by simp;
    1.61 -  next;
    1.62 -    fix t ts;
    1.63 -    assume "?P t" "?Q ts"; thus "?Q (t # ts)"; by simp;
    1.64 -  qed;
    1.65 -qed;
    1.66 +  subst_term f1 (subst_term f2 t)"
    1.67 +proof -
    1.68 +  let "?P t" = ?thesis
    1.69 +  let ?Q = "\<lambda>ts. subst_term_list (subst_term f1 o f2) ts =
    1.70 +    subst_term_list f1 (subst_term_list f2 ts)"
    1.71 +  show ?thesis
    1.72 +  proof (induct t)
    1.73 +    fix a show "?P (Var a)" by simp
    1.74 +  next
    1.75 +    fix b ts assume "?Q ts"
    1.76 +    thus "?P (App b ts)" by (simp add: o_def)
    1.77 +  next
    1.78 +    show "?Q []" by simp
    1.79 +  next
    1.80 +    fix t ts
    1.81 +    assume "?P t" "?Q ts" thus "?Q (t # ts)" by simp
    1.82 +  qed
    1.83 +qed
    1.84  
    1.85  
    1.86 -subsection {* Alternative induction *};
    1.87 +subsection {* Alternative induction *}
    1.88  
    1.89  theorem term_induct' [case_names Var App]:
    1.90    "(!!a. P (Var a)) ==>
    1.91 -   (!!b ts. list_all P ts ==> P (App b ts)) ==> P t";
    1.92 -proof -;
    1.93 -  assume var: "!!a. P (Var a)";
    1.94 -  assume app: "!!b ts. list_all P ts ==> P (App b ts)";
    1.95 -  show ?thesis;
    1.96 -  proof (induct P t);
    1.97 -    fix a; show "P (Var a)"; by (rule var);
    1.98 -  next;
    1.99 -    fix b t ts; assume "list_all P ts";
   1.100 -    thus "P (App b ts)"; by (rule app);
   1.101 -  next;
   1.102 -    show "list_all P []"; by simp;
   1.103 -  next;
   1.104 -    fix t ts; assume "P t" "list_all P ts";
   1.105 -    thus "list_all P (t # ts)"; by simp;
   1.106 -  qed;
   1.107 -qed;
   1.108 +   (!!b ts. list_all P ts ==> P (App b ts)) ==> P t"
   1.109 +proof -
   1.110 +  assume var: "!!a. P (Var a)"
   1.111 +  assume app: "!!b ts. list_all P ts ==> P (App b ts)"
   1.112 +  show ?thesis
   1.113 +  proof (induct P t)
   1.114 +    fix a show "P (Var a)" by (rule var)
   1.115 +  next
   1.116 +    fix b t ts assume "list_all P ts"
   1.117 +    thus "P (App b ts)" by (rule app)
   1.118 +  next
   1.119 +    show "list_all P []" by simp
   1.120 +  next
   1.121 +    fix t ts assume "P t" "list_all P ts"
   1.122 +    thus "list_all P (t # ts)" by simp
   1.123 +  qed
   1.124 +qed
   1.125  
   1.126  lemma
   1.127    "subst_term (subst_term f1 o f2) t = subst_term f1 (subst_term f2 t)"
   1.128 -  (is "?P t");
   1.129 -proof (induct (open) ?P t rule: term_induct');
   1.130 -  case Var;
   1.131 -  show "?P (Var a)"; by (simp add: o_def);
   1.132 -next;
   1.133 -  case App;
   1.134 -  have "?this --> ?P (App b ts)";
   1.135 -    by (induct ts) simp_all;
   1.136 -  thus "..."; ..;
   1.137 -qed;
   1.138 +  (is "?P t")
   1.139 +proof (induct (open) ?P t rule: term_induct')
   1.140 +  case Var
   1.141 +  show "?P (Var a)" by (simp add: o_def)
   1.142 +next
   1.143 +  case App
   1.144 +  have "?this --> ?P (App b ts)"
   1.145 +    by (induct ts) simp_all
   1.146 +  thus "..." ..
   1.147 +qed
   1.148  
   1.149 -end;
   1.150 +end