modernized examples;
authorblanchet
Thu Sep 27 00:40:51 2012 +0200 (2012-09-27)
changeset 49601ba31032887db
parent 49599 e716209814b3
child 49602 289de72578bb
modernized examples;
removed now trivial "HFset"
src/HOL/BNF/Examples/HFset.thy
src/HOL/BNF/Examples/Lambda_Term.thy
src/HOL/BNF/Examples/Misc_Data.thy
src/HOL/BNF/Examples/Stream.thy
src/HOL/ROOT
     1.1 --- a/src/HOL/BNF/Examples/HFset.thy	Wed Sep 26 19:50:10 2012 +0200
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,60 +0,0 @@
     1.4 -(*  Title:      HOL/BNF/Examples/HFset.thy
     1.5 -    Author:     Andrei Popescu, TU Muenchen
     1.6 -    Copyright   2012
     1.7 -
     1.8 -Hereditary sets.
     1.9 -*)
    1.10 -
    1.11 -header {* Hereditary Sets *}
    1.12 -
    1.13 -theory HFset
    1.14 -imports "../BNF"
    1.15 -begin
    1.16 -
    1.17 -
    1.18 -section {* Datatype definition *}
    1.19 -
    1.20 -data_raw hfset: 'hfset = "'hfset fset"
    1.21 -
    1.22 -
    1.23 -section {* Customization of terms *}
    1.24 -
    1.25 -subsection{* Constructors *}
    1.26 -
    1.27 -definition "Fold hs \<equiv> hfset_ctor hs"
    1.28 -
    1.29 -lemma hfset_simps[simp]:
    1.30 -"\<And>hs1 hs2. Fold hs1 = Fold hs2 \<longrightarrow> hs1 = hs2"
    1.31 -unfolding Fold_def hfset.ctor_inject by auto
    1.32 -
    1.33 -theorem hfset_cases[elim, case_names Fold]:
    1.34 -assumes Fold: "\<And> hs. h = Fold hs \<Longrightarrow> phi"
    1.35 -shows phi
    1.36 -using Fold unfolding Fold_def
    1.37 -by (cases rule: hfset.ctor_exhaust[of h]) simp
    1.38 -
    1.39 -lemma hfset_induct[case_names Fold, induct type: hfset]:
    1.40 -assumes Fold: "\<And> hs. (\<And> h. h |\<in>| hs \<Longrightarrow> phi h) \<Longrightarrow> phi (Fold hs)"
    1.41 -shows "phi t"
    1.42 -apply (induct rule: hfset.ctor_induct)
    1.43 -using Fold unfolding Fold_def fset_fset_member mem_Collect_eq ..
    1.44 -
    1.45 -(* alternative induction principle, using fset: *)
    1.46 -lemma hfset_induct_fset[case_names Fold, induct type: hfset]:
    1.47 -assumes Fold: "\<And> hs. (\<And> h. h \<in> fset hs \<Longrightarrow> phi h) \<Longrightarrow> phi (Fold hs)"
    1.48 -shows "phi t"
    1.49 -apply (induct rule: hfset_induct)
    1.50 -using Fold by (metis notin_fset)
    1.51 -
    1.52 -subsection{* Recursion and iteration (fold) *}
    1.53 -
    1.54 -lemma hfset_ctor_rec:
    1.55 -"hfset_ctor_rec R (Fold hs) = R (map_fset <id, hfset_ctor_rec R> hs)"
    1.56 -using hfset.ctor_rec unfolding Fold_def .
    1.57 -
    1.58 -(* The iterator has a simpler form: *)
    1.59 -lemma hfset_ctor_fold:
    1.60 -"hfset_ctor_fold R (Fold hs) = R (map_fset (hfset_ctor_fold R) hs)"
    1.61 -using hfset.ctor_fold unfolding Fold_def .
    1.62 -
    1.63 -end
     2.1 --- a/src/HOL/BNF/Examples/Lambda_Term.thy	Wed Sep 26 19:50:10 2012 +0200
     2.2 +++ b/src/HOL/BNF/Examples/Lambda_Term.thy	Thu Sep 27 00:40:51 2012 +0200
     2.3 @@ -15,203 +15,57 @@
     2.4  
     2.5  section {* Datatype definition *}
     2.6  
     2.7 -data_raw trm: 'trm = "'a + 'trm \<times> 'trm + 'a \<times> 'trm + ('a \<times> 'trm) fset \<times> 'trm"
     2.8 -
     2.9 -
    2.10 -section {* Customization of terms *}
    2.11 -
    2.12 -subsection{* Set and map *}
    2.13 -
    2.14 -lemma pre_trm_set2_Lt: "pre_trm_set2 (Inr (Inr (Inr (xts, t)))) = snd ` (fset xts) \<union> {t}"
    2.15 -unfolding pre_trm_set2_def sum_set_defs prod_set_defs collect_def[abs_def]
    2.16 -by auto
    2.17 -
    2.18 -lemma pre_trm_set2_Var: "\<And>x. pre_trm_set2 (Inl x) = {}"
    2.19 -and pre_trm_set2_App:
    2.20 -"\<And>t1 t2. pre_trm_set2 (Inr (Inl t1t2)) = {fst t1t2, snd t1t2}"
    2.21 -and pre_trm_set2_Lam:
    2.22 -"\<And>x t. pre_trm_set2 (Inr (Inr (Inl (x, t)))) = {t}"
    2.23 -unfolding pre_trm_set2_def sum_set_defs prod_set_defs collect_def[abs_def]
    2.24 -by auto
    2.25 -
    2.26 -lemma pre_trm_map:
    2.27 -"\<And> a1. pre_trm_map f1 f2 (Inl a1) = Inl (f1 a1)"
    2.28 -"\<And> a2 b2. pre_trm_map f1 f2 (Inr (Inl (a2,b2))) = Inr (Inl (f2 a2, f2 b2))"
    2.29 -"\<And> a1 a2. pre_trm_map f1 f2 (Inr (Inr (Inl (a1,a2)))) = Inr (Inr (Inl (f1 a1, f2 a2)))"
    2.30 -"\<And> a1a2s a2.
    2.31 -   pre_trm_map f1 f2 (Inr (Inr (Inr (a1a2s, a2)))) =
    2.32 -   Inr (Inr (Inr (map_fset (\<lambda> (a1', a2'). (f1 a1', f2 a2')) a1a2s, f2 a2)))"
    2.33 -unfolding pre_trm_map_def collect_def[abs_def] map_pair_def by auto
    2.34 +data 'a trm =
    2.35 +  Var 'a |
    2.36 +  App "'a trm" "'a trm" |
    2.37 +  Lam 'a "'a trm" |
    2.38 +  Lt "('a \<times> 'a trm) fset" "'a trm"
    2.39  
    2.40  
    2.41 -subsection{* Constructors *}
    2.42 -
    2.43 -definition "Var x \<equiv> trm_ctor (Inl x)"
    2.44 -definition "App t1 t2 \<equiv> trm_ctor (Inr (Inl (t1,t2)))"
    2.45 -definition "Lam x t \<equiv> trm_ctor (Inr (Inr (Inl (x,t))))"
    2.46 -definition "Lt xts t \<equiv> trm_ctor (Inr (Inr (Inr (xts,t))))"
    2.47 -
    2.48 -lemmas ctor_defs = Var_def App_def Lam_def Lt_def
    2.49 -
    2.50 -theorem trm_simps[simp]:
    2.51 -"\<And>x y. Var x = Var y \<longleftrightarrow> x = y"
    2.52 -"\<And>t1 t2 t1' t2'. App t1 t2 = App t1' t2' \<longleftrightarrow> t1 = t1' \<and> t2 = t2'"
    2.53 -"\<And>x x' t t'. Lam x t = Lam x' t' \<longleftrightarrow> x = x' \<and> t = t'"
    2.54 -"\<And> xts xts' t t'. Lt xts t = Lt xts' t' \<longleftrightarrow> xts = xts' \<and> t = t'"
    2.55 -(*  *)
    2.56 -"\<And> x t1 t2. Var x \<noteq> App t1 t2"  "\<And>x y t. Var x \<noteq> Lam y t"  "\<And> x xts t. Var x \<noteq> Lt xts t"
    2.57 -"\<And> t1 t2 x t. App t1 t2 \<noteq> Lam x t"  "\<And> t1 t2 xts t. App t1 t2 \<noteq> Lt xts t"
    2.58 -"\<And>x t xts t1. Lam x t \<noteq> Lt xts t1"
    2.59 -unfolding ctor_defs trm.ctor_inject by auto
    2.60 -
    2.61 -theorem trm_cases[elim, case_names Var App Lam Lt]:
    2.62 -assumes Var: "\<And> x. t = Var x \<Longrightarrow> phi"
    2.63 -and App: "\<And> t1 t2. t = App t1 t2 \<Longrightarrow> phi"
    2.64 -and Lam: "\<And> x t1. t = Lam x t1 \<Longrightarrow> phi"
    2.65 -and Lt: "\<And> xts t1. t = Lt xts t1 \<Longrightarrow> phi"
    2.66 -shows phi
    2.67 -proof(cases rule: trm.ctor_exhaust[of t])
    2.68 -  fix x assume "t = trm_ctor x"
    2.69 -  thus ?thesis
    2.70 -  apply(cases x) using Var unfolding ctor_defs apply blast
    2.71 -  apply(case_tac b) using App unfolding ctor_defs apply(case_tac a, blast)
    2.72 -  apply(case_tac ba) using Lam unfolding ctor_defs apply(case_tac a, blast)
    2.73 -  apply(case_tac bb) using Lt unfolding ctor_defs by blast
    2.74 -qed
    2.75 +section {* Customi induction rule *}
    2.76  
    2.77  lemma trm_induct[case_names Var App Lam Lt, induct type: trm]:
    2.78 -assumes Var: "\<And> (x::'a). phi (Var x)"
    2.79 +assumes Var: "\<And> x. phi (Var x)"
    2.80  and App: "\<And> t1 t2. \<lbrakk>phi t1; phi t2\<rbrakk> \<Longrightarrow> phi (App t1 t2)"
    2.81  and Lam: "\<And> x t. phi t \<Longrightarrow> phi (Lam x t)"
    2.82  and Lt: "\<And> xts t. \<lbrakk>\<And> x1 t1. (x1,t1) |\<in>| xts \<Longrightarrow> phi t1; phi t\<rbrakk> \<Longrightarrow> phi (Lt xts t)"
    2.83  shows "phi t"
    2.84 -proof(induct rule: trm.ctor_induct)
    2.85 -  fix u :: "'a + 'a trm \<times> 'a trm + 'a \<times> 'a trm + ('a \<times> 'a trm) fset \<times> 'a trm"
    2.86 -  assume IH: "\<And>t. t \<in> pre_trm_set2 u \<Longrightarrow> phi t"
    2.87 -  show "phi (trm_ctor u)"
    2.88 -  proof(cases u)
    2.89 -    case (Inl x)
    2.90 -    show ?thesis using Var unfolding Var_def Inl .
    2.91 -  next
    2.92 -    case (Inr uu) note Inr1 = Inr
    2.93 -    show ?thesis
    2.94 -    proof(cases uu)
    2.95 -      case (Inl t1t2)
    2.96 -      obtain t1 t2 where t1t2: "t1t2 = (t1,t2)" by (cases t1t2, blast)
    2.97 -      show ?thesis unfolding Inr1 Inl t1t2 App_def[symmetric] apply(rule App)
    2.98 -      using IH unfolding Inr1 Inl pre_trm_set2_App t1t2 fst_conv snd_conv by blast+
    2.99 -    next
   2.100 -      case (Inr uuu) note Inr2 = Inr
   2.101 -      show ?thesis
   2.102 -      proof(cases uuu)
   2.103 -        case (Inl xt)
   2.104 -        obtain x t where xt: "xt = (x,t)" by (cases xt, blast)
   2.105 -        show ?thesis unfolding Inr1 Inr2 Inl xt Lam_def[symmetric] apply(rule Lam)
   2.106 -        using IH unfolding Inr1 Inr2 Inl pre_trm_set2_Lam xt by blast
   2.107 -      next
   2.108 -        case (Inr xts_t)
   2.109 -        obtain xts t where xts_t: "xts_t = (xts,t)" by (cases xts_t, blast)
   2.110 -        show ?thesis unfolding Inr1 Inr2 Inr xts_t Lt_def[symmetric] apply(rule Lt) using IH
   2.111 -        unfolding Inr1 Inr2 Inr pre_trm_set2_Lt xts_t fset_fset_member image_def by auto
   2.112 -      qed
   2.113 -    qed
   2.114 -  qed
   2.115 -qed
   2.116 -
   2.117 -
   2.118 -subsection{* Recursion and iteration (fold) *}
   2.119 -
   2.120 -definition
   2.121 -"sumJoin4 f1 f2 f3 f4 \<equiv>
   2.122 -\<lambda> k. (case k of
   2.123 - Inl x1 \<Rightarrow> f1 x1
   2.124 -|Inr k1 \<Rightarrow> (case k1 of
   2.125 - Inl ((s2,a2),(t2,b2)) \<Rightarrow> f2 s2 a2 t2 b2
   2.126 -|Inr k2 \<Rightarrow> (case k2 of Inl (x3,(t3,b3)) \<Rightarrow> f3 x3 t3 b3
   2.127 -|Inr (xts,(t4,b4)) \<Rightarrow> f4 xts t4 b4)))"
   2.128 -
   2.129 -lemma sumJoin4_simps[simp]:
   2.130 -"\<And>x. sumJoin4 var app lam lt (Inl x) = var x"
   2.131 -"\<And> t1 a1 t2 a2. sumJoin4 var app lam lt (Inr (Inl ((t1,a1),(t2,a2)))) = app t1 a1 t2 a2"
   2.132 -"\<And> x t a. sumJoin4 var app lam lt (Inr (Inr (Inl (x,(t,a))))) = lam x t a"
   2.133 -"\<And> xtas t a. sumJoin4 var app lam lt (Inr (Inr (Inr (xtas,(t,a))))) = lt xtas t a"
   2.134 -unfolding sumJoin4_def by auto
   2.135 -
   2.136 -definition "trmrec var app lam lt \<equiv> trm_ctor_rec (sumJoin4 var app lam lt)"
   2.137 -
   2.138 -lemma trmrec_Var[simp]:
   2.139 -"trmrec var app lam lt (Var x) = var x"
   2.140 -unfolding trmrec_def Var_def trm.ctor_rec pre_trm_map(1) by simp
   2.141 -
   2.142 -lemma trmrec_App[simp]:
   2.143 -"trmrec var app lam lt (App t1 t2) =
   2.144 - app t1 (trmrec var app lam lt t1) t2 (trmrec var app lam lt t2)"
   2.145 -unfolding trmrec_def App_def trm.ctor_rec pre_trm_map(2) convol_def by simp
   2.146 -
   2.147 -lemma trmrec_Lam[simp]:
   2.148 -"trmrec var app lam lt (Lam x t) = lam x t (trmrec var app lam lt t)"
   2.149 -unfolding trmrec_def Lam_def trm.ctor_rec pre_trm_map(3) convol_def by simp
   2.150 -
   2.151 -lemma trmrec_Lt[simp]:
   2.152 -"trmrec var app lam lt (Lt xts t) =
   2.153 - lt (map_fset (\<lambda> (x,t). (x,t,trmrec var app lam lt t)) xts) t (trmrec var app lam lt t)"
   2.154 -unfolding trmrec_def Lt_def trm.ctor_rec pre_trm_map(4) convol_def by simp
   2.155 -
   2.156 -definition
   2.157 -"sumJoinI4 f1 f2 f3 f4 \<equiv>
   2.158 -\<lambda> k. (case k of
   2.159 - Inl x1 \<Rightarrow> f1 x1
   2.160 -|Inr k1 \<Rightarrow> (case k1 of
   2.161 - Inl (a2,b2) \<Rightarrow> f2 a2 b2
   2.162 -|Inr k2 \<Rightarrow> (case k2 of Inl (x3,b3) \<Rightarrow> f3 x3 b3
   2.163 -|Inr (xts,b4) \<Rightarrow> f4 xts b4)))"
   2.164 -
   2.165 -lemma sumJoinI4_simps[simp]:
   2.166 -"\<And>x. sumJoinI4 var app lam lt (Inl x) = var x"
   2.167 -"\<And> a1 a2. sumJoinI4 var app lam lt (Inr (Inl (a1,a2))) = app a1 a2"
   2.168 -"\<And> x a. sumJoinI4 var app lam lt (Inr (Inr (Inl (x,a)))) = lam x a"
   2.169 -"\<And> xtas a. sumJoinI4 var app lam lt (Inr (Inr (Inr (xtas,a)))) = lt xtas a"
   2.170 -unfolding sumJoinI4_def by auto
   2.171 -
   2.172 -(* The iterator has a simpler, hence more manageable type. *)
   2.173 -definition "trmfold var app lam lt \<equiv> trm_ctor_fold (sumJoinI4 var app lam lt)"
   2.174 -
   2.175 -lemma trmfold_Var[simp]:
   2.176 -"trmfold var app lam lt (Var x) = var x"
   2.177 -unfolding trmfold_def Var_def trm.ctor_fold pre_trm_map(1) by simp
   2.178 -
   2.179 -lemma trmfold_App[simp]:
   2.180 -"trmfold var app lam lt (App t1 t2) =
   2.181 - app (trmfold var app lam lt t1) (trmfold var app lam lt t2)"
   2.182 -unfolding trmfold_def App_def trm.ctor_fold pre_trm_map(2) by simp
   2.183 -
   2.184 -lemma trmfold_Lam[simp]:
   2.185 -"trmfold var app lam lt (Lam x t) = lam x (trmfold var app lam lt t)"
   2.186 -unfolding trmfold_def Lam_def trm.ctor_fold pre_trm_map(3) by simp
   2.187 -
   2.188 -lemma trmfold_Lt[simp]:
   2.189 -"trmfold var app lam lt (Lt xts t) =
   2.190 - lt (map_fset (\<lambda> (x,t). (x,trmfold var app lam lt t)) xts) (trmfold var app lam lt t)"
   2.191 -unfolding trmfold_def Lt_def trm.ctor_fold pre_trm_map(4) by simp
   2.192 +apply induct
   2.193 +apply (rule Var)
   2.194 +apply (erule App, assumption)
   2.195 +apply (erule Lam)
   2.196 +using Lt unfolding fset_fset_member mem_Collect_eq
   2.197 +apply (rule meta_mp)
   2.198 +defer
   2.199 +apply assumption
   2.200 +apply (erule thin_rl)
   2.201 +apply assumption
   2.202 +apply (drule meta_spec)
   2.203 +apply (drule meta_spec)
   2.204 +apply (drule meta_mp)
   2.205 +apply assumption
   2.206 +apply (auto simp: snds_def)
   2.207 +done
   2.208  
   2.209  
   2.210  subsection{* Example: The set of all variables varsOf and free variables fvarsOf of a term: *}
   2.211  
   2.212 -definition "varsOf = trmfold
   2.213 +definition "varsOf = trm_fold
   2.214  (\<lambda> x. {x})
   2.215  (\<lambda> X1 X2. X1 \<union> X2)
   2.216  (\<lambda> x X. X \<union> {x})
   2.217  (\<lambda> xXs Y. Y \<union> (\<Union> { {x} \<union> X | x X. (x,X) |\<in>| xXs}))"
   2.218  
   2.219 +thm trm.fold
   2.220  lemma varsOf_simps[simp]:
   2.221  "varsOf (Var x) = {x}"
   2.222  "varsOf (App t1 t2) = varsOf t1 \<union> varsOf t2"
   2.223  "varsOf (Lam x t) = varsOf t \<union> {x}"
   2.224  "varsOf (Lt xts t) =
   2.225   varsOf t \<union> (\<Union> { {x} \<union> X | x X. (x,X) |\<in>| map_fset (\<lambda> (x,t1). (x,varsOf t1)) xts})"
   2.226 -unfolding varsOf_def by simp_all
   2.227 +unfolding varsOf_def by (simp add: map_pair_def)+
   2.228  
   2.229 -definition "fvarsOf = trmfold
   2.230 +definition "fvarsOf = trm_fold
   2.231  (\<lambda> x. {x})
   2.232  (\<lambda> X1 X2. X1 \<union> X2)
   2.233  (\<lambda> x X. X - {x})
   2.234 @@ -225,7 +79,7 @@
   2.235   fvarsOf t
   2.236   - {x | x X. (x,X) |\<in>| map_fset (\<lambda> (x,t1). (x,fvarsOf t1)) xts}
   2.237   \<union> (\<Union> {X | x X. (x,X) |\<in>| map_fset (\<lambda> (x,t1). (x,fvarsOf t1)) xts})"
   2.238 -unfolding fvarsOf_def by simp_all
   2.239 +unfolding fvarsOf_def by (simp add: map_pair_def)+
   2.240  
   2.241  lemma diff_Un_incl_triv: "\<lbrakk>A \<subseteq> D; C \<subseteq> E\<rbrakk> \<Longrightarrow> A - B \<union> C \<subseteq> D \<union> E" by blast
   2.242  
     3.1 --- a/src/HOL/BNF/Examples/Misc_Data.thy	Wed Sep 26 19:50:10 2012 +0200
     3.2 +++ b/src/HOL/BNF/Examples/Misc_Data.thy	Thu Sep 27 00:40:51 2012 +0200
     3.3 @@ -21,6 +21,8 @@
     3.4  data ('b, 'c, 'd, 'e) some_passive =
     3.5    SP1 "('b, 'c, 'd, 'e) some_passive" | SP2 'b | SP3 'c | SP4 'd | SP5 'e
     3.6  
     3.7 +data hfset = HFset "hfset fset"
     3.8 +
     3.9  data lambda =
    3.10    Var string |
    3.11    App lambda lambda |
     4.1 --- a/src/HOL/BNF/Examples/Stream.thy	Wed Sep 26 19:50:10 2012 +0200
     4.2 +++ b/src/HOL/BNF/Examples/Stream.thy	Thu Sep 27 00:40:51 2012 +0200
     4.3 @@ -12,21 +12,21 @@
     4.4  imports TreeFI
     4.5  begin
     4.6  
     4.7 -hide_const (open) Quotient_Product.prod_rel
     4.8 -hide_fact (open) Quotient_Product.prod_rel_def
     4.9 -
    4.10 -codata_raw stream: 's = "'a \<times> 's"
    4.11 +codata 'a stream = Stream (hdd: 'a) (tll: "'a stream")
    4.12  
    4.13  (* selectors for streams *)
    4.14 -definition "hdd as \<equiv> fst (stream_dtor as)"
    4.15 -definition "tll as \<equiv> snd (stream_dtor as)"
    4.16 +lemma hdd_def': "hdd as = fst (stream_dtor as)"
    4.17 +unfolding hdd_def stream_case_def fst_def by (rule refl)
    4.18 +
    4.19 +lemma tll_def': "tll as = snd (stream_dtor as)"
    4.20 +unfolding tll_def stream_case_def snd_def by (rule refl)
    4.21  
    4.22  lemma unfold_pair_fun_hdd[simp]: "hdd (stream_dtor_unfold (f \<odot> g) t) = f t"
    4.23 -unfolding hdd_def pair_fun_def stream.dtor_unfold by simp
    4.24 +unfolding hdd_def' pair_fun_def stream.dtor_unfold by simp
    4.25  
    4.26  lemma unfold_pair_fun_tll[simp]: "tll (stream_dtor_unfold (f \<odot> g) t) =
    4.27   stream_dtor_unfold (f \<odot> g) (g t)"
    4.28 -unfolding tll_def pair_fun_def stream.dtor_unfold by simp
    4.29 +unfolding tll_def' pair_fun_def stream.dtor_unfold by simp
    4.30  
    4.31  (* infinite trees: *)
    4.32  coinductive infiniteTr where
    4.33 @@ -51,12 +51,10 @@
    4.34  definition "konigPath \<equiv> stream_dtor_unfold
    4.35    (lab \<odot> (\<lambda>tr. SOME tr'. tr' \<in> listF_set (sub tr) \<and> infiniteTr tr'))"
    4.36  
    4.37 -lemma hdd_simps1[simp]: "hdd (konigPath t) = lab t"
    4.38 -unfolding konigPath_def by simp
    4.39 -
    4.40 -lemma tll_simps2[simp]: "tll (konigPath t) =
    4.41 -  konigPath (SOME tr. tr \<in> listF_set (sub t) \<and> infiniteTr tr)"
    4.42 -unfolding konigPath_def by simp
    4.43 +lemma konigPath_simps[simp]:
    4.44 +"hdd (konigPath t) = lab t"
    4.45 +"tll (konigPath t) = konigPath (SOME tr. tr \<in> listF_set (sub t) \<and> infiniteTr tr)"
    4.46 +unfolding konigPath_def by simp+
    4.47  
    4.48  (* proper paths in trees: *)
    4.49  coinductive properPath where
    4.50 @@ -115,15 +113,9 @@
    4.51  (* some more stream theorems *)
    4.52  
    4.53  lemma stream_map[simp]: "stream_map f = stream_dtor_unfold (f o hdd \<odot> tll)"
    4.54 -unfolding stream_map_def pair_fun_def hdd_def[abs_def] tll_def[abs_def]
    4.55 +unfolding stream_map_def pair_fun_def hdd_def'[abs_def] tll_def'[abs_def]
    4.56    map_pair_def o_def prod_case_beta by simp
    4.57  
    4.58 -lemma prod_rel[simp]: "prod_rel \<phi>1 \<phi>2 a b = (\<phi>1 (fst a) (fst b) \<and> \<phi>2 (snd a) (snd b))"
    4.59 -unfolding prod_rel_def by auto
    4.60 -
    4.61 -lemmas stream_coind =
    4.62 -  mp[OF stream.dtor_coinduct, unfolded prod_rel[abs_def], folded hdd_def tll_def]
    4.63 -
    4.64  definition plus :: "nat stream \<Rightarrow> nat stream \<Rightarrow> nat stream" (infixr "\<oplus>" 66) where
    4.65    [simp]: "plus xs ys =
    4.66      stream_dtor_unfold ((%(xs, ys). hdd xs + hdd ys) \<odot> (%(xs, ys). (tll xs, tll ys))) (xs, ys)"
    4.67 @@ -136,22 +128,22 @@
    4.68  definition ns :: "nat \<Rightarrow> nat stream" where [simp]: "ns n = scalar n ones"
    4.69  
    4.70  lemma "ones \<oplus> ones = twos"
    4.71 -by (intro stream_coind[where P="%x1 x2. \<exists>x. x1 = ones \<oplus> ones \<and> x2 = twos"]) auto
    4.72 +by (rule stream.coinduct[of "%x1 x2. \<exists>x. x1 = ones \<oplus> ones \<and> x2 = twos"]) auto
    4.73  
    4.74  lemma "n \<cdot> twos = ns (2 * n)"
    4.75 -by (intro stream_coind[where P="%x1 x2. \<exists>n. x1 = n \<cdot> twos \<and> x2 = ns (2 * n)"]) force+
    4.76 +by (rule stream.coinduct[of "%x1 x2. \<exists>n. x1 = n \<cdot> twos \<and> x2 = ns (2 * n)"]) force+
    4.77  
    4.78  lemma prod_scalar: "(n * m) \<cdot> xs = n \<cdot> m \<cdot> xs"
    4.79 -by (intro stream_coind[where P="%x1 x2. \<exists>n m xs. x1 = (n * m) \<cdot> xs \<and> x2 = n \<cdot> m \<cdot> xs"]) force+
    4.80 +by (rule stream.coinduct[of "%x1 x2. \<exists>n m xs. x1 = (n * m) \<cdot> xs \<and> x2 = n \<cdot> m \<cdot> xs"]) force+
    4.81  
    4.82  lemma scalar_plus: "n \<cdot> (xs \<oplus> ys) = n \<cdot> xs \<oplus> n \<cdot> ys"
    4.83 -by (intro stream_coind[where P="%x1 x2. \<exists>n xs ys. x1 = n \<cdot> (xs \<oplus> ys) \<and> x2 = n \<cdot> xs \<oplus> n \<cdot> ys"])
    4.84 +by (rule stream.coinduct[of "%x1 x2. \<exists>n xs ys. x1 = n \<cdot> (xs \<oplus> ys) \<and> x2 = n \<cdot> xs \<oplus> n \<cdot> ys"])
    4.85     (force simp: add_mult_distrib2)+
    4.86  
    4.87  lemma plus_comm: "xs \<oplus> ys = ys \<oplus> xs"
    4.88 -by (intro stream_coind[where P="%x1 x2. \<exists>xs ys. x1 = xs \<oplus> ys \<and> x2 = ys \<oplus> xs"]) force+
    4.89 +by (rule stream.coinduct[of "%x1 x2. \<exists>xs ys. x1 = xs \<oplus> ys \<and> x2 = ys \<oplus> xs"]) force+
    4.90  
    4.91  lemma plus_assoc: "(xs \<oplus> ys) \<oplus> zs = xs \<oplus> ys \<oplus> zs"
    4.92 -by (intro stream_coind[where P="%x1 x2. \<exists>xs ys zs. x1 = (xs \<oplus> ys) \<oplus> zs \<and> x2 = xs \<oplus> ys \<oplus> zs"]) force+
    4.93 +by (rule stream.coinduct[of "%x1 x2. \<exists>xs ys zs. x1 = (xs \<oplus> ys) \<oplus> zs \<and> x2 = xs \<oplus> ys \<oplus> zs"]) force+
    4.94  
    4.95  end
     5.1 --- a/src/HOL/ROOT	Wed Sep 26 19:50:10 2012 +0200
     5.2 +++ b/src/HOL/ROOT	Thu Sep 27 00:40:51 2012 +0200
     5.3 @@ -625,7 +625,6 @@
     5.4    description {* Examples for Bounded Natural Functors *}
     5.5    options [document = false]
     5.6    theories
     5.7 -    HFset
     5.8      Lambda_Term
     5.9      Process
    5.10      TreeFsetI