Induct: converted some theories to new-style format;
authorwenzelm
Sat Feb 03 17:40:16 2001 +0100 (2001-02-03)
changeset 11046b5f5942781a0
parent 11045 971a50fda146
child 11047 10c51288b00d
Induct: converted some theories to new-style format;
src/HOL/Induct/ABexp.ML
src/HOL/Induct/ABexp.thy
src/HOL/Induct/Mutil.ML
src/HOL/Induct/Mutil.thy
src/HOL/Induct/ROOT.ML
src/HOL/Induct/Sigma_Algebra.thy
src/HOL/Induct/Term.ML
src/HOL/Induct/Term.thy
src/HOL/Induct/Tree.ML
src/HOL/Induct/Tree.thy
src/HOL/Induct/document/root.tex
src/HOL/IsaMakefile
     1.1 --- a/src/HOL/Induct/ABexp.ML	Sat Feb 03 15:22:57 2001 +0100
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,25 +0,0 @@
     1.4 -(*  Title:      HOL/Induct/ABexp.ML
     1.5 -    ID:         $Id$
     1.6 -    Author:     Stefan Berghofer, TU Muenchen
     1.7 -    Copyright   1998  TU Muenchen
     1.8 -
     1.9 -Arithmetic and boolean expressions
    1.10 -*)
    1.11 -
    1.12 -(** substitution theorems for arithmetic and boolean expressions **)
    1.13 -
    1.14 -(* One variable *)
    1.15 -Goal
    1.16 -  "evala env (substa (Var(v := a')) a) = evala (env(v := evala env a')) a &  \
    1.17 - \ evalb env (substb (Var(v := a')) b) = evalb (env(v := evala env a')) b";
    1.18 -by (induct_tac "a b" 1);
    1.19 -by (ALLGOALS Asm_full_simp_tac);
    1.20 -qed "subst1_aexp_bexp";
    1.21 -
    1.22 -(* All variables *)
    1.23 -Goal
    1.24 -  "evala env (substa s a) = evala (%x. evala env (s x)) a &  \
    1.25 - \ evalb env (substb s b) = evalb (%x. evala env (s x)) b";
    1.26 -by (induct_tac "a b" 1);
    1.27 -by (Auto_tac);
    1.28 -qed "subst_all_aexp_bexp";
     2.1 --- a/src/HOL/Induct/ABexp.thy	Sat Feb 03 15:22:57 2001 +0100
     2.2 +++ b/src/HOL/Induct/ABexp.thy	Sat Feb 03 17:40:16 2001 +0100
     2.3 @@ -2,52 +2,50 @@
     2.4      ID:         $Id$
     2.5      Author:     Stefan Berghofer, TU Muenchen
     2.6      Copyright   1998  TU Muenchen
     2.7 -
     2.8 -Arithmetic and boolean expressions
     2.9  *)
    2.10  
    2.11 -ABexp = Main +
    2.12 +header {* Arithmetic and boolean expressions *}
    2.13 +
    2.14 +theory ABexp = Main:
    2.15  
    2.16 -datatype
    2.17 -  'a aexp = IF ('a bexp) ('a aexp) ('a aexp)
    2.18 -          | Sum ('a aexp) ('a aexp)
    2.19 -          | Diff ('a aexp) ('a aexp)
    2.20 -          | Var 'a
    2.21 -          | Num nat
    2.22 -and
    2.23 -  'a bexp = Less ('a aexp) ('a aexp)
    2.24 -          | And ('a bexp) ('a bexp)
    2.25 -          | Neg ('a bexp)
    2.26 +datatype 'a aexp =
    2.27 +    IF "'a bexp"  "'a aexp"  "'a aexp"
    2.28 +  | Sum "'a aexp"  "'a aexp"
    2.29 +  | Diff "'a aexp"  "'a aexp"
    2.30 +  | Var 'a
    2.31 +  | Num nat
    2.32 +and 'a bexp =
    2.33 +    Less "'a aexp"  "'a aexp"
    2.34 +  | And "'a bexp"  "'a bexp"
    2.35 +  | Neg "'a bexp"
    2.36  
    2.37  
    2.38 -(** evaluation of arithmetic and boolean expressions **)
    2.39 +text {* \medskip Evaluation of arithmetic and boolean expressions *}
    2.40  
    2.41  consts
    2.42 -  evala :: ('a => nat) => 'a aexp => nat
    2.43 -  evalb :: ('a => nat) => 'a bexp => bool
    2.44 +  evala :: "('a => nat) => 'a aexp => nat"
    2.45 +  evalb :: "('a => nat) => 'a bexp => bool"
    2.46  
    2.47  primrec
    2.48 -  "evala env (IF b a1 a2) =
    2.49 -     (if evalb env b then evala env a1 else evala env a2)"
    2.50 +  "evala env (IF b a1 a2) = (if evalb env b then evala env a1 else evala env a2)"
    2.51    "evala env (Sum a1 a2) = evala env a1 + evala env a2"
    2.52    "evala env (Diff a1 a2) = evala env a1 - evala env a2"
    2.53    "evala env (Var v) = env v"
    2.54    "evala env (Num n) = n"
    2.55  
    2.56    "evalb env (Less a1 a2) = (evala env a1 < evala env a2)"
    2.57 -  "evalb env (And b1 b2) = (evalb env b1 & evalb env b2)"
    2.58 -  "evalb env (Neg b) = (~ evalb env b)"
    2.59 +  "evalb env (And b1 b2) = (evalb env b1 \<and> evalb env b2)"
    2.60 +  "evalb env (Neg b) = (\<not> evalb env b)"
    2.61  
    2.62  
    2.63 -(** substitution on arithmetic and boolean expressions **)
    2.64 +text {* \medskip Substitution on arithmetic and boolean expressions *}
    2.65  
    2.66  consts
    2.67 -  substa :: ('a => 'b aexp) => 'a aexp => 'b aexp
    2.68 -  substb :: ('a => 'b aexp) => 'a bexp => 'b bexp
    2.69 +  substa :: "('a => 'b aexp) => 'a aexp => 'b aexp"
    2.70 +  substb :: "('a => 'b aexp) => 'a bexp => 'b bexp"
    2.71  
    2.72  primrec
    2.73 -  "substa f (IF b a1 a2) =
    2.74 -     IF (substb f b) (substa f a1) (substa f a2)"
    2.75 +  "substa f (IF b a1 a2) = IF (substb f b) (substa f a1) (substa f a2)"
    2.76    "substa f (Sum a1 a2) = Sum (substa f a1) (substa f a2)"
    2.77    "substa f (Diff a1 a2) = Diff (substa f a1) (substa f a2)"
    2.78    "substa f (Var v) = f v"
    2.79 @@ -57,4 +55,20 @@
    2.80    "substb f (And b1 b2) = And (substb f b1) (substb f b2)"
    2.81    "substb f (Neg b) = Neg (substb f b)"
    2.82  
    2.83 +lemma subst1_aexp_bexp:
    2.84 +  "evala env (substa (Var (v := a')) a) = evala (env (v := evala env a')) a \<and>
    2.85 +  evalb env (substb (Var (v := a')) b) = evalb (env (v := evala env a')) b"
    2.86 +    --  {* one variable *}
    2.87 +  apply (induct a and b)
    2.88 +         apply simp_all
    2.89 +  done
    2.90 +
    2.91 +lemma subst_all_aexp_bexp:
    2.92 +  "evala env (substa s a) = evala (\<lambda>x. evala env (s x)) a \<and>
    2.93 +  evalb env (substb s b) = evalb (\<lambda>x. evala env (s x)) b"
    2.94 +    -- {* all variables *}
    2.95 +  apply (induct a and b)
    2.96 +         apply auto
    2.97 +  done
    2.98 +
    2.99  end
     3.1 --- a/src/HOL/Induct/Mutil.ML	Sat Feb 03 15:22:57 2001 +0100
     3.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.3 @@ -1,117 +0,0 @@
     3.4 -(*  Title:      HOL/Induct/Mutil
     3.5 -    ID:         $Id$
     3.6 -    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     3.7 -    Copyright   1996  University of Cambridge
     3.8 -
     3.9 -The Mutilated Chess Board Problem, formalized inductively
    3.10 -*)
    3.11 -
    3.12 -Addsimps (tiling.intrs @ domino.intrs);
    3.13 -AddIs    tiling.intrs;
    3.14 -
    3.15 -(** The union of two disjoint tilings is a tiling **)
    3.16 -
    3.17 -Goal "t: tiling A ==> u: tiling A --> t Int u = {} --> t Un u : tiling A";
    3.18 -by (etac tiling.induct 1);
    3.19 -by (simp_tac (simpset() addsimps [Un_assoc]) 2);
    3.20 -by Auto_tac;
    3.21 -qed_spec_mp "tiling_UnI";
    3.22 -
    3.23 -AddIs [tiling_UnI];
    3.24 -
    3.25 -(*** Chess boards ***)
    3.26 -
    3.27 -Goalw [lessThan_def]
    3.28 -    "lessThan(Suc n) <*> B = ({n} <*> B) Un ((lessThan n) <*> B)";
    3.29 -by Auto_tac;
    3.30 -qed "Sigma_Suc1";
    3.31 -
    3.32 -Goalw [lessThan_def]
    3.33 -    "A <*> lessThan(Suc n) = (A <*> {n}) Un (A <*> (lessThan n))";
    3.34 -by Auto_tac;
    3.35 -qed "Sigma_Suc2";
    3.36 -
    3.37 -Addsimps [Sigma_Suc1, Sigma_Suc2];
    3.38 -
    3.39 -Goal "({i} <*> {n}) Un ({i} <*> {m}) = {(i,m), (i,n)}";
    3.40 -by Auto_tac;
    3.41 -qed "sing_Times_lemma";
    3.42 -
    3.43 -Goal "{i} <*> lessThan(#2*n) : tiling domino";
    3.44 -by (induct_tac "n" 1);
    3.45 -by (ALLGOALS (asm_simp_tac (simpset() addsimps [Un_assoc RS sym])));
    3.46 -by (rtac tiling.Un 1);
    3.47 -by (auto_tac (claset(), simpset() addsimps [sing_Times_lemma]));  
    3.48 -qed "dominoes_tile_row";
    3.49 -
    3.50 -AddSIs [dominoes_tile_row]; 
    3.51 -
    3.52 -Goal "(lessThan m) <*> lessThan(#2*n) : tiling domino";
    3.53 -by (induct_tac "m" 1);
    3.54 -by Auto_tac;
    3.55 -qed "dominoes_tile_matrix";
    3.56 -
    3.57 -
    3.58 -(*** "coloured" and Dominoes ***)
    3.59 -
    3.60 -Goalw [coloured_def]
    3.61 -    "coloured b Int (insert (i,j) t) = \
    3.62 -\      (if (i+j) mod #2 = b then insert (i,j) (coloured b Int t) \
    3.63 -\                           else coloured b Int t)";
    3.64 -by Auto_tac;
    3.65 -qed "coloured_insert";
    3.66 -Addsimps [coloured_insert];
    3.67 -
    3.68 -Goal "d:domino ==> (EX i j. coloured 0 Int d = {(i,j)}) & \
    3.69 -\                  (EX m n. coloured 1 Int d = {(m,n)})";
    3.70 -by (etac domino.elim 1);
    3.71 -by (auto_tac (claset(), simpset() addsimps [mod_Suc]));
    3.72 -qed "domino_singletons";
    3.73 -
    3.74 -Goal "d:domino ==> finite d";
    3.75 -by (etac domino.elim 1);
    3.76 -by Auto_tac;
    3.77 -qed "domino_finite";
    3.78 -Addsimps [domino_finite];
    3.79 -
    3.80 -
    3.81 -(*** Tilings of dominoes ***)
    3.82 -
    3.83 -Goal "t:tiling domino ==> finite t";
    3.84 -by (etac tiling.induct 1);
    3.85 -by Auto_tac;
    3.86 -qed "tiling_domino_finite";
    3.87 -
    3.88 -Addsimps [tiling_domino_finite, Int_Un_distrib, Diff_Int_distrib];
    3.89 -
    3.90 -Goal "t: tiling domino ==> card(coloured 0 Int t) = card(coloured 1 Int t)";
    3.91 -by (etac tiling.induct 1);
    3.92 -by (dtac domino_singletons 2);
    3.93 -by Auto_tac;
    3.94 -(*this lemma tells us that both "inserts" are non-trivial*)
    3.95 -by (subgoal_tac "ALL p C. C Int a = {p} --> p ~: t" 1);
    3.96 -by (Asm_simp_tac 1);
    3.97 -by (Blast_tac 1);
    3.98 -qed "tiling_domino_0_1";
    3.99 -
   3.100 -(*Final argument is surprisingly complex*)
   3.101 -Goal "[| t : tiling domino;       \
   3.102 -\        (i+j) mod #2 = 0;  (m+n) mod #2 = 0;  \
   3.103 -\        {(i,j),(m,n)} <= t |]    \
   3.104 -\     ==> (t - {(i,j)} - {(m,n)}) ~: tiling domino";
   3.105 -by (rtac notI 1);
   3.106 -by (subgoal_tac "card (coloured 0 Int (t - {(i,j)} - {(m,n)})) < \
   3.107 -\                card (coloured 1 Int (t - {(i,j)} - {(m,n)}))" 1);
   3.108 -by (force_tac (claset(), HOL_ss addsimps [tiling_domino_0_1]) 1);
   3.109 -by (asm_simp_tac (simpset() addsimps [tiling_domino_0_1 RS sym]) 1);
   3.110 -by (asm_full_simp_tac (simpset() addsimps [coloured_def, card_Diff2_less]) 1); 
   3.111 -qed "gen_mutil_not_tiling";
   3.112 -
   3.113 -(*Apply the general theorem to the well-known case*)
   3.114 -Goal "t = lessThan(#2 * Suc m) <*> lessThan(#2 * Suc n) \
   3.115 -\     ==> t - {(0,0)} - {(Suc(#2*m), Suc(#2*n))} ~: tiling domino";
   3.116 -by (rtac gen_mutil_not_tiling 1);
   3.117 -by (blast_tac (claset() addSIs [dominoes_tile_matrix]) 1);
   3.118 -by Auto_tac;
   3.119 -qed "mutil_not_tiling";
   3.120 -
     4.1 --- a/src/HOL/Induct/Mutil.thy	Sat Feb 03 15:22:57 2001 +0100
     4.2 +++ b/src/HOL/Induct/Mutil.thy	Sat Feb 03 17:40:16 2001 +0100
     4.3 @@ -1,29 +1,150 @@
     4.4 -(*  Title:      HOL/Induct/Mutil
     4.5 +(*  Title:      HOL/Induct/Mutil.thy
     4.6      ID:         $Id$
     4.7      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4.8      Copyright   1996  University of Cambridge
     4.9 -
    4.10 -The Mutilated Chess Board Problem, formalized inductively
    4.11 -  Originator is Max Black, according to J A Robinson.
    4.12 -  Popularized as the Mutilated Checkerboard Problem by J McCarthy
    4.13  *)
    4.14  
    4.15 -Mutil = Main +
    4.16 +header {* The Mutilated Chess Board Problem *}
    4.17 +
    4.18 +theory Mutil = Main:
    4.19  
    4.20 -consts     tiling :: "'a set set => 'a set set"
    4.21 +text {*
    4.22 +  The Mutilated Chess Board Problem, formalized inductively.
    4.23 +
    4.24 +  Originator is Max Black, according to J A Robinson.  Popularized as
    4.25 +  the Mutilated Checkerboard Problem by J McCarthy.
    4.26 +*}
    4.27 +
    4.28 +consts tiling :: "'a set set => 'a set set"
    4.29  inductive "tiling A"
    4.30 -  intrs
    4.31 -    empty  "{} : tiling A"
    4.32 -    Un     "[| a: A;  t: tiling A;  a Int t = {} |] ==> a Un t : tiling A"
    4.33 +  intros [simp, intro]
    4.34 +    empty: "{} \<in> tiling A"
    4.35 +    Un: "a \<in> A ==> t \<in> tiling A ==> a \<inter> t = {} ==> a \<union> t \<in> tiling A"
    4.36  
    4.37 -consts    domino :: "(nat*nat)set set"
    4.38 +consts domino :: "(nat \<times> nat) set set"
    4.39  inductive domino
    4.40 -  intrs
    4.41 -    horiz  "{(i, j), (i, Suc j)} : domino"
    4.42 -    vertl  "{(i, j), (Suc i, j)} : domino"
    4.43 +  intros [simp]
    4.44 +    horiz: "{(i, j), (i, Suc j)} \<in> domino"
    4.45 +    vertl: "{(i, j), (Suc i, j)} \<in> domino"
    4.46  
    4.47  constdefs
    4.48 -  coloured  :: "nat => (nat*nat)set"
    4.49 -   "coloured b == {(i,j). (i+j) mod #2 = b}"
    4.50 +  coloured :: "nat => (nat \<times> nat) set"
    4.51 +   "coloured b == {(i, j). (i + j) mod #2 = b}"
    4.52 +
    4.53 +
    4.54 +text {* \medskip The union of two disjoint tilings is a tiling *}
    4.55 +
    4.56 +lemma tiling_UnI [rule_format, intro]:
    4.57 +  "t \<in> tiling A ==> u \<in> tiling A --> t \<inter> u = {} --> t \<union> u \<in> tiling A"
    4.58 +  apply (erule tiling.induct)
    4.59 +   prefer 2
    4.60 +   apply (simp add: Un_assoc)
    4.61 +  apply auto
    4.62 +  done
    4.63 +
    4.64 +
    4.65 +text {* \medskip Chess boards *}
    4.66 +
    4.67 +lemma Sigma_Suc1 [simp]:
    4.68 +  "lessThan (Suc n) \<times> B = ({n} \<times> B) \<union> ((lessThan n) \<times> B)"
    4.69 +  apply (unfold lessThan_def)
    4.70 +  apply auto
    4.71 +  done
    4.72 +
    4.73 +lemma Sigma_Suc2 [simp]:
    4.74 +  "A \<times> lessThan (Suc n) = (A \<times> {n}) \<union> (A \<times> (lessThan n))"
    4.75 +  apply (unfold lessThan_def)
    4.76 +  apply auto
    4.77 +  done
    4.78 +
    4.79 +lemma sing_Times_lemma: "({i} \<times> {n}) \<union> ({i} \<times> {m}) = {(i, m), (i, n)}"
    4.80 +  apply auto
    4.81 +  done
    4.82 +
    4.83 +lemma dominoes_tile_row [intro!]: "{i} \<times> lessThan (#2 * n) \<in> tiling domino"
    4.84 +  apply (induct n)
    4.85 +   apply (simp_all add: Un_assoc [symmetric])
    4.86 +  apply (rule tiling.Un)
    4.87 +    apply (auto simp add: sing_Times_lemma)
    4.88 +  done
    4.89 +
    4.90 +lemma dominoes_tile_matrix: "(lessThan m) \<times> lessThan (#2 * n) \<in> tiling domino"
    4.91 +  apply (induct m)
    4.92 +   apply auto
    4.93 +  done
    4.94 +
    4.95 +
    4.96 +text {* \medskip @{term coloured} and Dominoes *}
    4.97 +
    4.98 +lemma coloured_insert [simp]:
    4.99 +  "coloured b \<inter> (insert (i, j) t) =
   4.100 +   (if (i + j) mod #2 = b then insert (i, j) (coloured b \<inter> t)
   4.101 +    else coloured b \<inter> t)"
   4.102 +  apply (unfold coloured_def)
   4.103 +  apply auto
   4.104 +  done
   4.105 +
   4.106 +lemma domino_singletons:
   4.107 +  "d \<in> domino ==>
   4.108 +    (\<exists>i j. coloured 0 \<inter> d = {(i, j)}) \<and>
   4.109 +    (\<exists>m n. coloured 1 \<inter> d = {(m, n)})"
   4.110 +  apply (erule domino.cases)
   4.111 +   apply (auto simp add: mod_Suc)
   4.112 +  done
   4.113 +
   4.114 +lemma domino_finite [simp]: "d \<in> domino ==> finite d"
   4.115 +  apply (erule domino.cases)
   4.116 +   apply auto
   4.117 +  done
   4.118 +
   4.119 +
   4.120 +text {* \medskip Tilings of dominoes *}
   4.121 +
   4.122 +lemma tiling_domino_finite [simp]: "t \<in> tiling domino ==> finite t"
   4.123 +  apply (erule tiling.induct)
   4.124 +   apply auto
   4.125 +  done
   4.126 +
   4.127 +declare
   4.128 +  Int_Un_distrib [simp]
   4.129 +  Diff_Int_distrib [simp]
   4.130 +
   4.131 +lemma tiling_domino_0_1:
   4.132 +  "t \<in> tiling domino ==> card (coloured 0 \<inter> t) = card (coloured 1 \<inter> t)"
   4.133 +  apply (erule tiling.induct)
   4.134 +   apply (drule_tac [2] domino_singletons)
   4.135 +   apply auto
   4.136 +  apply (subgoal_tac "\<forall>p C. C \<inter> a = {p} --> p \<notin> t")
   4.137 +    -- {* this lemma tells us that both ``inserts'' are non-trivial *}
   4.138 +   apply (simp (no_asm_simp))
   4.139 +  apply blast
   4.140 +  done
   4.141 +
   4.142 +
   4.143 +text {* \medskip Final argument is surprisingly complex *}
   4.144 +
   4.145 +theorem gen_mutil_not_tiling:
   4.146 +  "t \<in> tiling domino ==>
   4.147 +    (i + j) mod #2 = 0 ==> (m + n) mod #2 = 0 ==>
   4.148 +    {(i, j), (m, n)} \<subseteq> t
   4.149 +  ==> (t - {(i, j)} - {(m, n)}) \<notin> tiling domino"
   4.150 +  apply (rule notI)
   4.151 +  apply (subgoal_tac
   4.152 +    "card (coloured 0 \<inter> (t - {(i, j)} - {(m, n)})) <
   4.153 +      card (coloured 1 \<inter> (t - {(i, j)} - {(m, n)}))")
   4.154 +   apply (force simp only: tiling_domino_0_1)
   4.155 +  apply (simp add: tiling_domino_0_1 [symmetric])
   4.156 +  apply (simp add: coloured_def card_Diff2_less)
   4.157 +  done
   4.158 +
   4.159 +text {* Apply the general theorem to the well-known case *}
   4.160 +
   4.161 +theorem mutil_not_tiling:
   4.162 +  "t = lessThan (#2 * Suc m) \<times> lessThan (#2 * Suc n)
   4.163 +    ==> t - {(0, 0)} - {(Suc (#2 * m), Suc (#2 * n))} \<notin> tiling domino"
   4.164 +  apply (rule gen_mutil_not_tiling)
   4.165 +     apply (blast intro!: dominoes_tile_matrix)
   4.166 +    apply auto
   4.167 +  done
   4.168  
   4.169  end
     5.1 --- a/src/HOL/Induct/ROOT.ML	Sat Feb 03 15:22:57 2001 +0100
     5.2 +++ b/src/HOL/Induct/ROOT.ML	Sat Feb 03 17:40:16 2001 +0100
     5.3 @@ -1,16 +1,12 @@
     5.4 -(*  Title:      HOL/Induct/ROOT.ML
     5.5  
     5.6 -Examples of Inductive and Coinductive Definitions.
     5.7 -*)
     5.8 -
     5.9 +time_use_thy "Mutil";
    5.10 +time_use_thy "Term";
    5.11 +time_use_thy "ABexp";
    5.12 +time_use_thy "Tree";
    5.13  time_use_thy "Sigma_Algebra";
    5.14  time_use_thy "Perm";
    5.15  time_use_thy "Comb";
    5.16 -time_use_thy "Mutil";
    5.17  time_use_thy "PropLog";
    5.18  time_use_thy "SList";
    5.19  time_use_thy "LFilter";
    5.20 -time_use_thy "Term";
    5.21 -time_use_thy "ABexp";
    5.22  time_use_thy "Exp";
    5.23 -time_use_thy "Tree";
     6.1 --- a/src/HOL/Induct/Sigma_Algebra.thy	Sat Feb 03 15:22:57 2001 +0100
     6.2 +++ b/src/HOL/Induct/Sigma_Algebra.thy	Sat Feb 03 17:40:16 2001 +0100
     6.3 @@ -4,6 +4,8 @@
     6.4      License:    GPL (GNU GENERAL PUBLIC LICENSE)
     6.5  *)
     6.6  
     6.7 +header {* Sigma algebras *}
     6.8 +
     6.9  theory Sigma_Algebra = Main:
    6.10  
    6.11  text {*
     7.1 --- a/src/HOL/Induct/Term.ML	Sat Feb 03 15:22:57 2001 +0100
     7.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     7.3 @@ -1,30 +0,0 @@
     7.4 -(*  Title:      HOL/Induct/Term.ML
     7.5 -    ID:         $Id$
     7.6 -    Author:     Stefan Berghofer, TU Muenchen
     7.7 -    Copyright   1998  TU Muenchen
     7.8 -
     7.9 -Terms over a given alphabet -- function applications
    7.10 -*)
    7.11 -
    7.12 -(** a simple theorem about composition of substitutions **)
    7.13 -
    7.14 -Goal "(subst_term ((subst_term f1) o f2) t) =  \
    7.15 -  \  (subst_term f1 (subst_term f2 t)) &  \
    7.16 -  \  (subst_term_list ((subst_term f1) o f2) ts) =  \
    7.17 -  \  (subst_term_list f1 (subst_term_list f2 ts))";
    7.18 -by (induct_tac "t ts" 1);
    7.19 -by (ALLGOALS Asm_full_simp_tac);
    7.20 -qed "subst_comp";
    7.21 -
    7.22 -(**** alternative induction rule ****)
    7.23 -
    7.24 -bind_thm ("term_induct2", prove_goal thy
    7.25 -  "[| !!v. P (Var v);  \
    7.26 -   \  !!f ts. list_all P ts ==> P (App f ts) |] ==>  \
    7.27 -   \    P t & list_all P ts"
    7.28 -  (fn prems =>
    7.29 -    [induct_tac "t ts" 1,
    7.30 -     resolve_tac prems 1,
    7.31 -     resolve_tac prems 1,
    7.32 -     atac 1,
    7.33 -     ALLGOALS Asm_simp_tac]) RS conjunct1);
     8.1 --- a/src/HOL/Induct/Term.thy	Sat Feb 03 15:22:57 2001 +0100
     8.2 +++ b/src/HOL/Induct/Term.thy	Sat Feb 03 17:40:16 2001 +0100
     8.3 @@ -2,23 +2,23 @@
     8.4      ID:         $Id$
     8.5      Author:     Stefan Berghofer,  TU Muenchen
     8.6      Copyright   1998  TU Muenchen
     8.7 -
     8.8 -Terms over a given alphabet -- function applications
     8.9  *)
    8.10  
    8.11 -Term = Main +
    8.12 +header {* Terms over a given alphabet *}
    8.13 +
    8.14 +theory Term = Main:
    8.15  
    8.16 -datatype
    8.17 -  ('a, 'b) term = Var 'a
    8.18 -                | App 'b ((('a, 'b) term) list)
    8.19 +datatype ('a, 'b) "term" =
    8.20 +    Var 'a
    8.21 +  | App 'b "('a, 'b) term list"
    8.22  
    8.23  
    8.24 -(** substitution function on terms **)
    8.25 +text {* \medskip Substitution function on terms *}
    8.26  
    8.27  consts
    8.28 -  subst_term :: "['a => ('a, 'b) term, ('a, 'b) term] => ('a, 'b) term"
    8.29 +  subst_term :: "('a => ('a, 'b) term) => ('a, 'b) term => ('a, 'b) term"
    8.30    subst_term_list ::
    8.31 -    "['a => ('a, 'b) term, ('a, 'b) term list] => ('a, 'b) term list"
    8.32 +    "('a => ('a, 'b) term) => ('a, 'b) term list => ('a, 'b) term list"
    8.33  
    8.34  primrec
    8.35    "subst_term f (Var a) = f a"
    8.36 @@ -28,4 +28,35 @@
    8.37    "subst_term_list f (t # ts) =
    8.38       subst_term f t # subst_term_list f ts"
    8.39  
    8.40 +
    8.41 +text {* \medskip A simple theorem about composition of substitutions *}
    8.42 +
    8.43 +lemma subst_comp:
    8.44 +  "(subst_term ((subst_term f1) \<circ> f2) t) =
    8.45 +    (subst_term f1 (subst_term f2 t)) \<and>
    8.46 +  (subst_term_list ((subst_term f1) \<circ> f2) ts) =
    8.47 +    (subst_term_list f1 (subst_term_list f2 ts))"
    8.48 +  apply (induct t and ts rule: term.induct)
    8.49 +     apply simp_all
    8.50 +  done
    8.51 +
    8.52 +
    8.53 +text {* \medskip Alternative induction rule *}
    8.54 +
    8.55 +lemma term_induct2:
    8.56 +  "(!!v. P (Var v)) ==>
    8.57 +    (!!f ts. list_all P ts ==> P (App f ts))
    8.58 +  ==> P t"
    8.59 +proof -
    8.60 +  case antecedent
    8.61 +  have "P t \<and> list_all P ts"
    8.62 +    apply (induct t and ts rule: term.induct)
    8.63 +       apply (rule antecedent)
    8.64 +      apply (rule antecedent)
    8.65 +      apply assumption
    8.66 +     apply simp_all
    8.67 +    done
    8.68 +  thus ?thesis ..
    8.69 +qed
    8.70 +
    8.71  end
     9.1 --- a/src/HOL/Induct/Tree.ML	Sat Feb 03 15:22:57 2001 +0100
     9.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     9.3 @@ -1,20 +0,0 @@
     9.4 -(*  Title:      HOL/Induct/Tree.ML
     9.5 -    ID:         $Id$
     9.6 -    Author:     Stefan Berghofer,  TU Muenchen
     9.7 -    Copyright   1999  TU Muenchen
     9.8 -
     9.9 -Infinitely branching trees
    9.10 -*)
    9.11 -
    9.12 -Goal "map_tree g (map_tree f t) = map_tree (g o f) t";
    9.13 -by (induct_tac "t" 1);
    9.14 -by (ALLGOALS Asm_simp_tac);
    9.15 -qed "tree_map_compose";
    9.16 -
    9.17 -val prems = Goal "(!!x. P x ==> Q (f x)) ==>  \
    9.18 -   \    exists_tree P ts --> exists_tree Q (map_tree f ts)";
    9.19 -by (induct_tac "ts" 1);
    9.20 -by (ALLGOALS (asm_simp_tac (simpset() addsimps prems)));
    9.21 -by (Fast_tac 1);
    9.22 -qed "exists_map";
    9.23 -
    10.1 --- a/src/HOL/Induct/Tree.thy	Sat Feb 03 15:22:57 2001 +0100
    10.2 +++ b/src/HOL/Induct/Tree.thy	Sat Feb 03 17:40:16 2001 +0100
    10.3 @@ -2,26 +2,39 @@
    10.4      ID:         $Id$
    10.5      Author:     Stefan Berghofer,  TU Muenchen
    10.6      Copyright   1999  TU Muenchen
    10.7 -
    10.8 -Infinitely branching trees
    10.9  *)
   10.10  
   10.11 -Tree = Main +
   10.12 +header {* Infinitely branching trees *}
   10.13 +
   10.14 +theory Tree = Main:
   10.15  
   10.16 -datatype 'a tree = Atom 'a | Branch "nat => 'a tree"
   10.17 +datatype 'a tree =
   10.18 +    Atom 'a
   10.19 +  | Branch "nat => 'a tree"
   10.20  
   10.21  consts
   10.22    map_tree :: "('a => 'b) => 'a tree => 'b tree"
   10.23 -
   10.24  primrec
   10.25    "map_tree f (Atom a) = Atom (f a)"
   10.26 -  "map_tree f (Branch ts) = Branch (%x. map_tree f (ts x))"
   10.27 +  "map_tree f (Branch ts) = Branch (\<lambda>x. map_tree f (ts x))"
   10.28 +
   10.29 +lemma tree_map_compose: "map_tree g (map_tree f t) = map_tree (g \<circ> f) t"
   10.30 +  apply (induct t)
   10.31 +   apply simp_all
   10.32 +  done
   10.33  
   10.34  consts
   10.35    exists_tree :: "('a => bool) => 'a tree => bool"
   10.36 -
   10.37  primrec
   10.38    "exists_tree P (Atom a) = P a"
   10.39 -  "exists_tree P (Branch ts) = (? x. exists_tree P (ts x))"
   10.40 +  "exists_tree P (Branch ts) = (\<exists>x. exists_tree P (ts x))"
   10.41 +
   10.42 +lemma exists_map:
   10.43 +  "(!!x. P x ==> Q (f x)) ==>
   10.44 +    exists_tree P ts ==> exists_tree Q (map_tree f ts)"
   10.45 +  apply (induct ts)
   10.46 +   apply simp_all
   10.47 +  apply blast
   10.48 +  done
   10.49  
   10.50  end
    11.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    11.2 +++ b/src/HOL/Induct/document/root.tex	Sat Feb 03 17:40:16 2001 +0100
    11.3 @@ -0,0 +1,27 @@
    11.4 +
    11.5 +\documentclass[11pt,a4paper]{article}
    11.6 +\usepackage{isabelle,isabellesym,pdfsetup}
    11.7 +
    11.8 +%for best-style documents ...
    11.9 +\urlstyle{rm}
   11.10 +\isabellestyle{it}
   11.11 +
   11.12 +\begin{document}
   11.13 +
   11.14 +\title{Examples of Inductive and Coinductive Definitions}
   11.15 +\author{Stefan Berghofer \\ Tobias Nipkow \\ Lawrence C Paulson \\ Markus Wenzel}
   11.16 +\maketitle
   11.17 +
   11.18 +\begin{abstract}
   11.19 +  This is a collection of small examples to demonstrate Isabelle/HOL's
   11.20 +  (co)inductive definitions package.  Large examples appear on many other
   11.21 +  sessions, such as Lambda, IMP, and Auth.
   11.22 +\end{abstract}
   11.23 +
   11.24 +\tableofcontents
   11.25 +\newpage
   11.26 +
   11.27 +\parindent 0pt\parskip 0.5ex
   11.28 +\input{session}
   11.29 +
   11.30 +\end{document}
    12.1 --- a/src/HOL/IsaMakefile	Sat Feb 03 15:22:57 2001 +0100
    12.2 +++ b/src/HOL/IsaMakefile	Sat Feb 03 17:40:16 2001 +0100
    12.3 @@ -205,11 +205,11 @@
    12.4  $(LOG)/HOL-Induct.gz: $(OUT)/HOL \
    12.5    Induct/Com.ML Induct/Com.thy Induct/Comb.ML Induct/Comb.thy \
    12.6    Induct/Exp.ML Induct/Exp.thy Induct/LFilter.ML Induct/LFilter.thy \
    12.7 -  Induct/LList.ML Induct/LList.thy Induct/Mutil.ML Induct/Mutil.thy \
    12.8 -  Induct/Perm.ML Induct/Perm.thy Induct/PropLog.ML \
    12.9 -  Induct/PropLog.thy Induct/ROOT.ML Induct/Sexp.ML Induct/Sexp.thy \
   12.10 -  Induct/Sigma_Algebra.thy Induct/SList.ML Induct/SList.thy \
   12.11 -  Induct/ABexp.ML Induct/ABexp.thy Induct/Term.ML Induct/Term.thy
   12.12 +  Induct/LList.ML Induct/LList.thy Induct/Mutil.thy Induct/Perm.ML \
   12.13 +  Induct/Perm.thy Induct/PropLog.ML Induct/PropLog.thy Induct/ROOT.ML \
   12.14 +  Induct/Sexp.ML Induct/Sexp.thy Induct/Sigma_Algebra.thy \
   12.15 +  Induct/SList.ML Induct/SList.thy Induct/ABexp.thy Induct/Term.thy \
   12.16 +  Induct/Tree.thy Induct/document/root.tex
   12.17  	@$(ISATOOL) usedir $(OUT)/HOL Induct
   12.18  
   12.19