--- a/src/HOL/BNF/Examples/Derivation_Trees/Prelim.thy Wed Oct 02 11:57:52 2013 +0200
+++ b/src/HOL/BNF/Examples/Derivation_Trees/Prelim.thy Wed Oct 02 13:29:04 2013 +0200
@@ -28,9 +28,6 @@
abbreviation sum_case_abbrev ("[[_,_]]" 800)
where "[[f,g]] \<equiv> Sum_Type.sum_case f g"
-lemma inj_Inl[simp]: "inj Inl" unfolding inj_on_def by auto
-lemma inj_Inr[simp]: "inj Inr" unfolding inj_on_def by auto
-
lemma Inl_oplus_elim:
assumes "Inl tr \<in> (id \<oplus> f) ` tns"
shows "Inl tr \<in> tns"
--- a/src/HOL/BNF/Examples/Koenig.thy Wed Oct 02 11:57:52 2013 +0200
+++ b/src/HOL/BNF/Examples/Koenig.thy Wed Oct 02 13:29:04 2013 +0200
@@ -23,13 +23,6 @@
apply (auto simp add: stl_def)
by (simp add: Stream_def stream.dtor_ctor)
-lemma unfold_pair_fun_shd[simp]: "shd (stream_dtor_unfold (f \<odot> g) t) = f t"
-unfolding shd_def' pair_fun_def stream.dtor_unfold by simp
-
-lemma unfold_pair_fun_stl[simp]: "stl (stream_dtor_unfold (f \<odot> g) t) =
- stream_dtor_unfold (f \<odot> g) (g t)"
-unfolding stl_def' pair_fun_def stream.dtor_unfold by simp
-
(* infinite trees: *)
coinductive infiniteTr where
"\<lbrakk>tr' \<in> listF_set (sub tr); infiniteTr tr'\<rbrakk> \<Longrightarrow> infiniteTr tr"
@@ -50,13 +43,9 @@
"infiniteTr tr \<Longrightarrow> (\<exists> tr' \<in> listF_set (sub tr). infiniteTr tr')"
by (erule infiniteTr.cases) blast
-definition "konigPath \<equiv> stream_dtor_unfold
- (lab \<odot> (\<lambda>tr. SOME tr'. tr' \<in> listF_set (sub tr) \<and> infiniteTr tr'))"
-
-lemma konigPath_simps[simp]:
-"shd (konigPath t) = lab t"
-"stl (konigPath t) = konigPath (SOME tr. tr \<in> listF_set (sub t) \<and> infiniteTr tr)"
-unfolding konigPath_def by simp+
+primcorec konigPath where
+ "shd (konigPath t) = lab t"
+| "stl (konigPath t) = konigPath (SOME tr. tr \<in> listF_set (sub t) \<and> infiniteTr tr)"
(* proper paths in trees: *)
coinductive properPath where
@@ -97,16 +86,14 @@
proof-
{fix as
assume "infiniteTr tr \<and> as = konigPath tr" hence "properPath as tr"
- proof (induct rule: properPath_coind, safe)
- fix t
- let ?t = "SOME t'. t' \<in> listF_set (sub t) \<and> infiniteTr t'"
- assume "infiniteTr t"
- hence "\<exists>t' \<in> listF_set (sub t). infiniteTr t'" by simp
- hence "\<exists>t'. t' \<in> listF_set (sub t) \<and> infiniteTr t'" by blast
- hence "?t \<in> listF_set (sub t) \<and> infiniteTr ?t" by (elim someI_ex)
- moreover have "stl (konigPath t) = konigPath ?t" by simp
- ultimately show "\<exists>t' \<in> listF_set (sub t).
- infiniteTr t' \<and> stl (konigPath t) = konigPath t'" by blast
+ proof (coinduction arbitrary: tr as rule: properPath_coind)
+ case (sub tr as)
+ let ?t = "SOME t'. t' \<in> listF_set (sub tr) \<and> infiniteTr t'"
+ from sub have "\<exists>t' \<in> listF_set (sub tr). infiniteTr t'" by simp
+ then have "\<exists>t'. t' \<in> listF_set (sub tr) \<and> infiniteTr t'" by blast
+ then have "?t \<in> listF_set (sub tr) \<and> infiniteTr ?t" by (rule someI_ex)
+ moreover have "stl (konigPath tr) = konigPath ?t" by simp
+ ultimately show ?case using sub by blast
qed simp
}
thus ?thesis using assms by blast
@@ -114,38 +101,33 @@
(* some more stream theorems *)
-lemma stream_map[simp]: "smap f = stream_dtor_unfold (f o shd \<odot> stl)"
-unfolding smap_def pair_fun_def shd_def'[abs_def] stl_def'[abs_def]
- map_pair_def o_def prod_case_beta by simp
-
-definition plus :: "nat stream \<Rightarrow> nat stream \<Rightarrow> nat stream" (infixr "\<oplus>" 66) where
- [simp]: "plus xs ys =
- stream_dtor_unfold ((%(xs, ys). shd xs + shd ys) \<odot> (%(xs, ys). (stl xs, stl ys))) (xs, ys)"
+primcorec plus :: "nat stream \<Rightarrow> nat stream \<Rightarrow> nat stream" (infixr "\<oplus>" 66) where
+ "shd (plus xs ys) = shd xs + shd ys"
+| "stl (plus xs ys) = plus (stl xs) (stl ys)"
definition scalar :: "nat \<Rightarrow> nat stream \<Rightarrow> nat stream" (infixr "\<cdot>" 68) where
[simp]: "scalar n = smap (\<lambda>x. n * x)"
-definition ones :: "nat stream" where [simp]: "ones = stream_dtor_unfold ((%x. 1) \<odot> id) ()"
-definition twos :: "nat stream" where [simp]: "twos = stream_dtor_unfold ((%x. 2) \<odot> id) ()"
+primcorec ones :: "nat stream" where "ones = 1 ## ones"
+primcorec twos :: "nat stream" where "twos = 2 ## twos"
definition ns :: "nat \<Rightarrow> nat stream" where [simp]: "ns n = scalar n ones"
lemma "ones \<oplus> ones = twos"
-by (rule stream.coinduct[of "%x1 x2. \<exists>x. x1 = ones \<oplus> ones \<and> x2 = twos"]) auto
+ by coinduction simp
lemma "n \<cdot> twos = ns (2 * n)"
-by (rule stream.coinduct[of "%x1 x2. \<exists>n. x1 = n \<cdot> twos \<and> x2 = ns (2 * n)"]) force+
+ by coinduction simp
lemma prod_scalar: "(n * m) \<cdot> xs = n \<cdot> m \<cdot> xs"
-by (rule stream.coinduct[of "%x1 x2. \<exists>n m xs. x1 = (n * m) \<cdot> xs \<and> x2 = n \<cdot> m \<cdot> xs"]) force+
+ by (coinduction arbitrary: xs) auto
lemma scalar_plus: "n \<cdot> (xs \<oplus> ys) = n \<cdot> xs \<oplus> n \<cdot> ys"
-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"])
- (force simp: add_mult_distrib2)+
+ by (coinduction arbitrary: xs ys) (auto simp: add_mult_distrib2)
lemma plus_comm: "xs \<oplus> ys = ys \<oplus> xs"
-by (rule stream.coinduct[of "%x1 x2. \<exists>xs ys. x1 = xs \<oplus> ys \<and> x2 = ys \<oplus> xs"]) force+
+ by (coinduction arbitrary: xs ys) auto
lemma plus_assoc: "(xs \<oplus> ys) \<oplus> zs = xs \<oplus> ys \<oplus> zs"
-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+
+ by (coinduction arbitrary: xs ys zs) auto
end
--- a/src/HOL/BNF/Examples/Process.thy Wed Oct 02 11:57:52 2013 +0200
+++ b/src/HOL/BNF/Examples/Process.thy Wed Oct 02 13:29:04 2013 +0200
@@ -71,19 +71,10 @@
subsection{* Single-guard fixpoint definition *}
-definition
-"BX \<equiv>
- process_unfold
- (\<lambda> P. True)
- (\<lambda> P. ''a'')
- (\<lambda> P. P)
- undefined
- undefined
- ()"
-
-lemma BX: "BX = Action ''a'' BX"
-unfolding BX_def
-using process.unfold(1)[of "\<lambda> P. True" "()" "\<lambda> P. ''a''" "\<lambda> P. P"] by simp
+primcorec BX where
+ "isAction BX"
+| "prefOf BX = ''a''"
+| "contOf BX = BX"
subsection{* Multi-guard fixpoint definitions, simulated with auxiliary arguments *}
@@ -172,28 +163,9 @@
definition "guarded sys \<equiv> \<forall> X Y. sys X \<noteq> VAR Y"
-definition
-"solution sys \<equiv>
- process_unfold
- (isACT sys)
- (PREF sys)
- (CONT sys)
- (CH1 sys)
- (CH2 sys)"
-
-lemma solution_Action:
-assumes "isACT sys T"
-shows "solution sys T = Action (PREF sys T) (solution sys (CONT sys T))"
-unfolding solution_def
-using process.unfold(1)[of "isACT sys" T "PREF sys" "CONT sys" "CH1 sys" "CH2 sys"]
- assms by simp
-
-lemma solution_Choice:
-assumes "\<not> isACT sys T"
-shows "solution sys T = Choice (solution sys (CH1 sys T)) (solution sys (CH2 sys T))"
-unfolding solution_def
-using process.unfold(2)[of "isACT sys" T "PREF sys" "CONT sys" "CH1 sys" "CH2 sys"]
- assms by simp
+primcorec solution where
+ "isACT sys T \<Longrightarrow> solution sys T = Action (PREF sys T) (solution sys (CONT sys T))"
+| "_ \<Longrightarrow> solution sys T = Choice (solution sys (CH1 sys T)) (solution sys (CH2 sys T))"
lemma isACT_VAR:
assumes g: "guarded sys"
@@ -207,13 +179,13 @@
case True
hence T: "isACT sys (sys X)" unfolding isACT_VAR[OF g] .
show ?thesis
- unfolding solution_Action[OF T] using solution_Action[of sys "VAR X"] True g
+ unfolding solution.ctr(1)[OF T] using solution.ctr(1)[of sys "VAR X"] True g
unfolding guarded_def by (cases "sys X", auto)
next
case False note FFalse = False
hence TT: "\<not> isACT sys (sys X)" unfolding isACT_VAR[OF g] .
show ?thesis
- unfolding solution_Choice[OF TT] using solution_Choice[of sys "VAR X"] FFalse g
+ unfolding solution.ctr(2)[OF TT] using solution.ctr(2)[of sys "VAR X"] FFalse g
unfolding guarded_def by (cases "sys X", auto)
qed
@@ -222,29 +194,27 @@
proof-
{fix q assume "q = solution sys (PROC p)"
hence "p = q"
- proof(induct rule: process_coind)
+ proof (coinduct rule: process_coind)
case (iss p p')
from isAction_isChoice[of p] show ?case
proof
assume p: "isAction p"
hence 0: "isACT sys (PROC p)" by simp
- thus ?thesis using iss not_isAction_isChoice
- unfolding solution_Action[OF 0] by auto
+ thus ?thesis using iss not_isAction_isChoice by auto
next
assume "isChoice p"
hence 0: "\<not> isACT sys (PROC p)"
using not_isAction_isChoice by auto
- thus ?thesis using iss isAction_isChoice
- unfolding solution_Choice[OF 0] by auto
+ thus ?thesis using iss isAction_isChoice by auto
qed
next
case (Action a a' p p')
hence 0: "isACT sys (PROC (Action a p))" by simp
- show ?case using Action unfolding solution_Action[OF 0] by simp
+ show ?case using Action unfolding solution.ctr(1)[OF 0] by simp
next
case (Choice p q p' q')
hence 0: "\<not> isACT sys (PROC (Choice p q))" using not_isAction_isChoice by auto
- show ?case using Choice unfolding solution_Choice[OF 0] by simp
+ show ?case using Choice unfolding solution.ctr(2)[OF 0] by simp
qed
}
thus ?thesis by metis
@@ -252,11 +222,11 @@
lemma solution_ACT[simp]:
"solution sys (ACT a T) = Action a (solution sys T)"
-by (metis CONT.simps(3) PREF.simps(3) isACT.simps(3) solution_Action)
+by (metis CONT.simps(3) PREF.simps(3) isACT.simps(3) solution.ctr(1))
lemma solution_CH[simp]:
"solution sys (CH T1 T2) = Choice (solution sys T1) (solution sys T2)"
-by (metis CH1.simps(3) CH2.simps(3) isACT.simps(4) solution_Choice)
+by (metis CH1.simps(3) CH2.simps(3) isACT.simps(4) solution.ctr(2))
(* Example: *)
--- a/src/HOL/BNF/Examples/Stream.thy Wed Oct 02 11:57:52 2013 +0200
+++ b/src/HOL/BNF/Examples/Stream.thy Wed Oct 02 13:29:04 2013 +0200
@@ -101,14 +101,8 @@
lemma sset_streams:
assumes "sset s \<subseteq> A"
shows "s \<in> streams A"
-proof (coinduct rule: streams.coinduct[of "\<lambda>s'. \<exists>a s. s' = a ## s \<and> a \<in> A \<and> sset s \<subseteq> A"])
- case streams from assms show ?case by (cases s) auto
-next
- fix s' assume "\<exists>a s. s' = a ## s \<and> a \<in> A \<and> sset s \<subseteq> A"
- then guess a s by (elim exE)
- with assms show "\<exists>a l. s' = a ## l \<and>
- a \<in> A \<and> ((\<exists>a s. l = a ## s \<and> a \<in> A \<and> sset s \<subseteq> A) \<or> l \<in> streams A)"
- by (cases s) auto
+using assms proof (coinduction arbitrary: s)
+ case streams then show ?case by (cases s) simp
qed
@@ -175,9 +169,9 @@
lemma smap_alt: "smap f s = s' \<longleftrightarrow> (\<forall>n. f (s !! n) = s' !! n)" (is "?L = ?R")
proof
assume ?R
- thus ?L
- by (coinduct rule: stream.coinduct[of "\<lambda>s1 s2. \<exists>n. s1 = smap f (sdrop n s) \<and> s2 = sdrop n s'", consumes 0])
- (auto intro: exI[of _ 0] simp del: sdrop.simps(2))
+ then have "\<And>n. smap f (sdrop n s) = sdrop n s'"
+ by coinduction (auto intro: exI[of _ 0] simp del: sdrop.simps(2))
+ then show ?L using sdrop.simps(1) by metis
qed auto
lemma stake_invert_Nil[iff]: "stake n s = [] \<longleftrightarrow> n = 0"
@@ -218,15 +212,15 @@
qed (metis comp_apply sdrop.simps(1) sdrop_while.simps snth.simps(1))
qed
-definition "sfilter P = stream_unfold (shd o sdrop_while (Not o P)) (stl o sdrop_while (Not o P))"
+primcorec sfilter where
+ "shd (sfilter P s) = shd (sdrop_while (Not o P) s)"
+| "stl (sfilter P s) = sfilter P (stl (sdrop_while (Not o P) s))"
lemma sfilter_Stream: "sfilter P (x ## s) = (if P x then x ## sfilter P s else sfilter P s)"
proof (cases "P x")
- case True thus ?thesis unfolding sfilter_def
- by (subst stream.unfold) (simp add: sdrop_while_Stream)
+ case True thus ?thesis by (subst sfilter.ctr) (simp add: sdrop_while_Stream)
next
- case False thus ?thesis unfolding sfilter_def
- by (subst (1 2) stream.unfold) (simp add: sdrop_while_Stream)
+ case False thus ?thesis by (subst (1 2) sfilter.ctr) (simp add: sdrop_while_Stream)
qed
@@ -243,28 +237,17 @@
subsection {* recurring stream out of a list *}
-definition cycle :: "'a list \<Rightarrow> 'a stream" where
- "cycle = stream_unfold hd (\<lambda>xs. tl xs @ [hd xs])"
-
-lemma cycle_simps[simp]:
- "shd (cycle u) = hd u"
- "stl (cycle u) = cycle (tl u @ [hd u])"
- by (auto simp: cycle_def)
-
+primcorec cycle :: "'a list \<Rightarrow> 'a stream" where
+ "shd (cycle xs) = hd xs"
+| "stl (cycle xs) = cycle (tl xs @ [hd xs])"
lemma cycle_decomp: "u \<noteq> [] \<Longrightarrow> cycle u = u @- cycle u"
-proof (coinduct rule: stream.coinduct[of "\<lambda>s1 s2. \<exists>u. s1 = cycle u \<and> s2 = u @- cycle u \<and> u \<noteq> []", consumes 0, case_names _ Eq_stream])
- case (Eq_stream s1 s2)
- then obtain u where "s1 = cycle u \<and> s2 = u @- cycle u \<and> u \<noteq> []" by blast
- thus ?case using stream.unfold[of hd "\<lambda>xs. tl xs @ [hd xs]" u] by (auto simp: cycle_def)
-qed auto
+proof (coinduction arbitrary: u)
+ case Eq_stream then show ?case using stream.collapse[of "cycle u"]
+ by (auto intro!: exI[of _ "tl u @ [hd u]"])
+qed
lemma cycle_Cons[code]: "cycle (x # xs) = x ## cycle (xs @ [x])"
-proof (coinduct rule: stream.coinduct[of "\<lambda>s1 s2. \<exists>x xs. s1 = cycle (x # xs) \<and> s2 = x ## cycle (xs @ [x])", consumes 0, case_names _ Eq_stream])
- case (Eq_stream s1 s2)
- then obtain x xs where "s1 = cycle (x # xs) \<and> s2 = x ## cycle (xs @ [x])" by blast
- thus ?case
- by (auto simp: cycle_def intro!: exI[of _ "hd (xs @ [x])"] exI[of _ "tl (xs @ [x])"] stream.unfold)
-qed auto
+ by (subst cycle.ctr) simp
lemma cycle_rotated: "\<lbrakk>v \<noteq> []; cycle u = v @- s\<rbrakk> \<Longrightarrow> cycle (tl u @ [hd u]) = tl v @- s"
by (auto dest: arg_cong[of _ _ stl])
@@ -304,13 +287,9 @@
subsection {* stream repeating a single element *}
-definition "same x = stream_unfold (\<lambda>_. x) id ()"
-
-lemma same_simps[simp]: "shd (same x) = x" "stl (same x) = same x"
- unfolding same_def by auto
-
-lemma same_unfold[code]: "same x = x ## same x"
- by (metis same_simps stream.collapse)
+primcorec same where
+ "shd (same x) = x"
+| "stl (same x) = same x"
lemma snth_same[simp]: "same x !! n = x"
unfolding same_def by (induct n) auto
@@ -328,18 +307,13 @@
unfolding stream_all_def by auto
lemma same_cycle: "same x = cycle [x]"
- by (coinduct rule: stream.coinduct[of "\<lambda>s1 s2. s1 = same x \<and> s2 = cycle [x]"]) auto
+ by coinduction auto
subsection {* stream of natural numbers *}
-definition "fromN n = stream_unfold id Suc n"
-
-lemma fromN_simps[simp]: "shd (fromN n) = n" "stl (fromN n) = fromN (Suc n)"
- unfolding fromN_def by auto
-
-lemma fromN_unfold[code]: "fromN n = n ## fromN (Suc n)"
- unfolding fromN_def by (metis id_def stream.unfold)
+primcorec fromN :: "nat \<Rightarrow> nat stream" where
+ "fromN n = n ## fromN (n + 1)"
lemma snth_fromN[simp]: "fromN n !! m = n + m"
unfolding fromN_def by (induct m arbitrary: n) auto
@@ -352,12 +326,12 @@
lemma sset_fromN[simp]: "sset (fromN n) = {n ..}" (is "?L = ?R")
proof safe
- fix m assume "m : ?L"
+ fix m assume "m \<in> ?L"
moreover
{ fix s assume "m \<in> sset s" "\<exists>n'\<ge>n. s = fromN n'"
- hence "n \<le> m" by (induct arbitrary: n rule: sset_induct1) fastforce+
+ hence "n \<le> m" by (induct arbitrary: n rule: sset_induct1) fastforce+
}
- ultimately show "n \<le> m" by blast
+ ultimately show "n \<le> m" by auto
next
fix m assume "n \<le> m" thus "m \<in> ?L" by (metis le_iff_add snth_fromN snth_sset)
qed
@@ -367,16 +341,12 @@
subsection {* flatten a stream of lists *}
-definition flat where
- "flat \<equiv> stream_unfold (hd o shd) (\<lambda>s. if tl (shd s) = [] then stl s else tl (shd s) ## stl s)"
-
-lemma flat_simps[simp]:
+primcorec flat where
"shd (flat ws) = hd (shd ws)"
- "stl (flat ws) = flat (if tl (shd ws) = [] then stl ws else tl (shd ws) ## stl ws)"
- unfolding flat_def by auto
+| "stl (flat ws) = flat (if tl (shd ws) = [] then stl ws else tl (shd ws) ## stl ws)"
lemma flat_Cons[simp, code]: "flat ((x # xs) ## ws) = x ## flat (if xs = [] then ws else xs ## ws)"
- unfolding flat_def using stream.unfold[of "hd o shd" _ "(x # xs) ## ws"] by auto
+ by (subst flat.ctr) simp
lemma flat_Stream[simp]: "xs \<noteq> [] \<Longrightarrow> flat (xs ## ws) = xs @- flat ws"
by (induct xs) auto
@@ -465,17 +435,13 @@
subsection {* interleave two streams *}
-definition sinterleave :: "'a stream \<Rightarrow> 'a stream \<Rightarrow> 'a stream" where
- [code del]: "sinterleave s1 s2 =
- stream_unfold (\<lambda>(s1, s2). shd s1) (\<lambda>(s1, s2). (s2, stl s1)) (s1, s2)"
-
-lemma sinterleave_simps[simp]:
- "shd (sinterleave s1 s2) = shd s1" "stl (sinterleave s1 s2) = sinterleave s2 (stl s1)"
- unfolding sinterleave_def by auto
+primcorec sinterleave where
+ "shd (sinterleave s1 s2) = shd s1"
+| "stl (sinterleave s1 s2) = sinterleave s2 (stl s1)"
lemma sinterleave_code[code]:
"sinterleave (x ## s1) s2 = x ## sinterleave s2 s1"
- by (metis sinterleave_simps stream.exhaust stream.sel)
+ by (subst sinterleave.ctr) simp
lemma sinterleave_snth[simp]:
"even n \<Longrightarrow> sinterleave s1 s2 !! n = s1 !! (n div 2)"
@@ -507,15 +473,12 @@
subsection {* zip *}
-definition "szip s1 s2 =
- stream_unfold (map_pair shd shd) (map_pair stl stl) (s1, s2)"
-
-lemma szip_simps[simp]:
- "shd (szip s1 s2) = (shd s1, shd s2)" "stl (szip s1 s2) = szip (stl s1) (stl s2)"
- unfolding szip_def by auto
+primcorec szip where
+ "shd (szip s1 s2) = (shd s1, shd s2)"
+| "stl (szip s1 s2) = szip (stl s1) (stl s2)"
lemma szip_unfold[code]: "szip (Stream a s1) (Stream b s2) = Stream (a, b) (szip s1 s2)"
- unfolding szip_def by (subst stream.unfold) simp
+ by (subst szip.ctr) simp
lemma snth_szip[simp]: "szip s1 s2 !! n = (s1 !! n, s2 !! n)"
by (induct n arbitrary: s1 s2) auto
@@ -523,35 +486,24 @@
subsection {* zip via function *}
-definition "smap2 f s1 s2 =
- stream_unfold (\<lambda>(s1,s2). f (shd s1) (shd s2)) (map_pair stl stl) (s1, s2)"
-
-lemma smap2_simps[simp]:
+primcorec smap2 where
"shd (smap2 f s1 s2) = f (shd s1) (shd s2)"
- "stl (smap2 f s1 s2) = smap2 f (stl s1) (stl s2)"
- unfolding smap2_def by auto
+| "stl (smap2 f s1 s2) = smap2 f (stl s1) (stl s2)"
lemma smap2_unfold[code]:
"smap2 f (Stream a s1) (Stream b s2) = Stream (f a b) (smap2 f s1 s2)"
- unfolding smap2_def by (subst stream.unfold) simp
+ by (subst smap2.ctr) simp
lemma smap2_szip:
"smap2 f s1 s2 = smap (split f) (szip s1 s2)"
- by (coinduct rule: stream.coinduct[of
- "\<lambda>s1 s2. \<exists>s1' s2'. s1 = smap2 f s1' s2' \<and> s2 = smap (split f) (szip s1' s2')"])
- fastforce+
+ by (coinduction arbitrary: s1 s2) auto
subsection {* iterated application of a function *}
-definition siterate :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a stream" where
- "siterate f x = x ## stream_unfold f f x"
-
-lemma siterate_simps[simp]: "shd (siterate f x) = x" "stl (siterate f x) = siterate f (f x)"
- unfolding siterate_def by (auto intro: stream.unfold)
-
-lemma siterate_code[code]: "siterate f x = x ## siterate f (f x)"
- by (metis siterate_def stream.unfold)
+primcorec siterate where
+ "shd (siterate f x) = x"
+| "stl (siterate f x) = siterate f (f x)"
lemma stake_Suc: "stake (Suc n) s = stake n s @ [s !! n]"
by (induct n arbitrary: s) auto
--- a/src/HOL/BNF/Examples/TreeFI.thy Wed Oct 02 11:57:52 2013 +0200
+++ b/src/HOL/BNF/Examples/TreeFI.thy Wed Oct 02 13:29:04 2013 +0200
@@ -14,17 +14,10 @@
codatatype 'a treeFI = Tree (lab: 'a) (sub: "'a treeFI listF")
-definition pair_fun (infixr "\<odot>" 50) where
- "f \<odot> g \<equiv> \<lambda>x. (f x, g x)"
-
(* Tree reverse:*)
-definition "trev \<equiv> treeFI_unfold lab (lrev o sub)"
-
-lemma trev_simps1[simp]: "lab (trev t) = lab t"
- unfolding trev_def by simp
-
-lemma trev_simps2[simp]: "sub (trev t) = mapF trev (lrev (sub t))"
- unfolding trev_def by simp
+primcorec trev where
+ "lab (trev t) = lab t"
+| "sub (trev t) = mapF trev (lrev (sub t))"
lemma treeFI_coinduct:
assumes *: "phi x y"
@@ -33,9 +26,10 @@
lengthh (sub a) = lengthh (sub b) \<and>
(\<forall>i < lengthh (sub a). phi (nthh (sub a) i) (nthh (sub b) i))"
shows "x = y"
-using * proof (coinduct rule: treeFI.coinduct)
- fix t1 t2 assume "phi t1 t2" note * = step[OF this] and ** = conjunct2[OF *]
- from conjunct1[OF **] conjunct2[OF **] have "relF phi (sub t1) (sub t2)"
+using * proof (coinduction arbitrary: x y)
+ case (Eq_treeFI t1 t2)
+ from conjunct1[OF conjunct2[OF step[OF Eq_treeFI]]] conjunct2[OF conjunct2[OF step[OF Eq_treeFI]]]
+ have "relF phi (sub t1) (sub t2)"
proof (induction "sub t1" "sub t2" arbitrary: t1 t2 rule: listF_induct2)
case (Conss x xs y ys)
note sub = Conss(2,3)[symmetric] and phi = mp[OF spec[OF Conss(4)], unfolded sub]
@@ -43,10 +37,10 @@
unfolded sub, simplified]
from phi[of 0] show ?case unfolding sub by (auto intro!: IH dest: phi[simplified, OF Suc_mono])
qed simp
- with conjunct1[OF *] show "lab t1 = lab t2 \<and> relF phi (sub t1) (sub t2)" ..
+ with conjunct1[OF step[OF Eq_treeFI]] show ?case by simp
qed
lemma trev_trev: "trev (trev tr) = tr"
- by (rule treeFI_coinduct[of "%a b. trev (trev b) = a"]) auto
+ by (coinduction arbitrary: tr rule: treeFI_coinduct) auto
end
--- a/src/HOL/BNF/Examples/TreeFsetI.thy Wed Oct 02 11:57:52 2013 +0200
+++ b/src/HOL/BNF/Examples/TreeFsetI.thy Wed Oct 02 13:29:04 2013 +0200
@@ -16,22 +16,12 @@
codatatype 'a treeFsetI = Tree (lab: 'a) (sub: "'a treeFsetI fset")
-definition pair_fun (infixr "\<odot>" 50) where
- "f \<odot> g \<equiv> \<lambda>x. (f x, g x)"
-
(* tree map (contrived example): *)
-definition tmap where
-"tmap f = treeFsetI_unfold (f o lab) sub"
-
-lemma tmap_simps[simp]:
-"lab (tmap f t) = f (lab t)"
+primcorec tmap where
+"lab (tmap f t) = f (lab t)" |
"sub (tmap f t) = fimage (tmap f) (sub t)"
-unfolding tmap_def treeFsetI.sel_unfold by simp+
lemma "tmap (f o g) x = tmap f (tmap g x)"
-apply (rule treeFsetI.coinduct[of "%x1 x2. \<exists>x. x1 = tmap (f o g) x \<and> x2 = tmap f (tmap g x)"])
-apply auto
-apply (unfold fset_rel_alt)
-by auto
+ by (coinduction arbitrary: x) (auto simp: fset_rel_alt)
end