--- a/NEWS Mon Jul 16 23:33:28 2018 +0100
+++ b/NEWS Mon Jul 16 23:33:38 2018 +0100
@@ -379,8 +379,9 @@
* Theory HOL-Library.Code_Lazy provides a new preprocessor for the code
generator to generate code for algebraic types with lazy evaluation
-semantics even in call-by-value target languages. See theory
-HOL-Codegenerator_Test.Code_Lazy_Test for some examples.
+semantics even in call-by-value target languages. See the theories
+HOL-ex.Code_Lazy_Demo and HOL-Codegenerator_Test.Code_Lazy_Test for
+some examples.
* Theory HOL-Library.Landau_Symbols has been moved here from AFP.
--- a/src/HOL/Analysis/FPS_Convergence.thy Mon Jul 16 23:33:28 2018 +0100
+++ b/src/HOL/Analysis/FPS_Convergence.thy Mon Jul 16 23:33:38 2018 +0100
@@ -13,7 +13,7 @@
"HOL-Computational_Algebra.Formal_Power_Series"
begin
-subsection \<open>Balls with extended real radius\<close>
+subsection%unimportant \<open>Balls with extended real radius\<close>
text \<open>
The following is a variant of @{const ball} that also allows an infinite radius.
@@ -54,13 +54,13 @@
subsection \<open>Basic properties of convergent power series\<close>
-definition fps_conv_radius :: "'a :: {banach, real_normed_div_algebra} fps \<Rightarrow> ereal" where
+definition%important fps_conv_radius :: "'a :: {banach, real_normed_div_algebra} fps \<Rightarrow> ereal" where
"fps_conv_radius f = conv_radius (fps_nth f)"
-definition eval_fps :: "'a :: {banach, real_normed_div_algebra} fps \<Rightarrow> 'a \<Rightarrow> 'a" where
+definition%important eval_fps :: "'a :: {banach, real_normed_div_algebra} fps \<Rightarrow> 'a \<Rightarrow> 'a" where
"eval_fps f z = (\<Sum>n. fps_nth f n * z ^ n)"
-definition fps_expansion :: "(complex \<Rightarrow> complex) \<Rightarrow> complex \<Rightarrow> complex fps" where
+definition%important fps_expansion :: "(complex \<Rightarrow> complex) \<Rightarrow> complex \<Rightarrow> complex fps" where
"fps_expansion f z0 = Abs_fps (\<lambda>n. (deriv ^^ n) f z0 / fact n)"
lemma norm_summable_fps:
@@ -73,7 +73,7 @@
shows "norm z < fps_conv_radius f \<Longrightarrow> summable (\<lambda>n. fps_nth f n * z ^ n)"
by (rule summable_in_conv_radius) (simp_all add: fps_conv_radius_def)
-lemma sums_eval_fps:
+theorem sums_eval_fps:
fixes f :: "'a :: {banach, real_normed_div_algebra} fps"
assumes "norm z < fps_conv_radius f"
shows "(\<lambda>n. fps_nth f n * z ^ n) sums eval_fps f z"
@@ -194,7 +194,7 @@
qed
-subsection \<open>Lower bounds on radius of convergence\<close>
+subsection%unimportant \<open>Lower bounds on radius of convergence\<close>
lemma fps_conv_radius_deriv:
fixes f :: "'a :: {banach, real_normed_field} fps"
@@ -447,12 +447,12 @@
subsection \<open>Evaluating power series\<close>
-lemma eval_fps_deriv:
+theorem eval_fps_deriv:
assumes "norm z < fps_conv_radius f"
shows "eval_fps (fps_deriv f) z = deriv (eval_fps f) z"
by (intro DERIV_imp_deriv [symmetric] has_field_derivative_eval_fps assms)
-lemma fps_nth_conv_deriv:
+theorem fps_nth_conv_deriv:
fixes f :: "complex fps"
assumes "fps_conv_radius f > 0"
shows "fps_nth f n = (deriv ^^ n) (eval_fps f) 0 / fact n"
@@ -478,7 +478,7 @@
finally show ?case by (simp add: divide_simps)
qed
-lemma eval_fps_eqD:
+theorem eval_fps_eqD:
fixes f g :: "complex fps"
assumes "fps_conv_radius f > 0" "fps_conv_radius g > 0"
assumes "eventually (\<lambda>z. eval_fps f z = eval_fps g z) (nhds 0)"
@@ -792,7 +792,8 @@
the coefficients of the series with the singularities of the function, this predicate
is enough.
\<close>
-definition has_fps_expansion :: "('a :: {banach,real_normed_div_algebra} \<Rightarrow> 'a) \<Rightarrow> 'a fps \<Rightarrow> bool"
+definition%important
+ has_fps_expansion :: "('a :: {banach,real_normed_div_algebra} \<Rightarrow> 'a) \<Rightarrow> 'a fps \<Rightarrow> bool"
(infixl "has'_fps'_expansion" 60)
where "(f has_fps_expansion F) \<longleftrightarrow>
fps_conv_radius F > 0 \<and> eventually (\<lambda>z. eval_fps F z = f z) (nhds 0)"
@@ -1261,7 +1262,7 @@
by (intro that[of ?s']) (auto simp: has_fps_expansion_def zero_ereal_def)
qed
-lemma residue_fps_expansion_over_power_at_0:
+theorem residue_fps_expansion_over_power_at_0:
assumes "f has_fps_expansion F"
shows "residue (\<lambda>z. f z / z ^ Suc n) 0 = fps_nth F n"
proof -
--- a/src/HOL/Analysis/Generalised_Binomial_Theorem.thy Mon Jul 16 23:33:28 2018 +0100
+++ b/src/HOL/Analysis/Generalised_Binomial_Theorem.thy Mon Jul 16 23:33:38 2018 +0100
@@ -70,7 +70,7 @@
with a show ?thesis by simp
qed
-lemma gen_binomial_complex:
+theorem gen_binomial_complex:
fixes z :: complex
assumes "norm z < 1"
shows "(\<lambda>n. (a gchoose n) * z^n) sums (1 + z) powr a"
--- a/src/HOL/Analysis/Harmonic_Numbers.thy Mon Jul 16 23:33:28 2018 +0100
+++ b/src/HOL/Analysis/Harmonic_Numbers.thy Mon Jul 16 23:33:38 2018 +0100
@@ -19,7 +19,7 @@
subsection \<open>The Harmonic numbers\<close>
-definition harm :: "nat \<Rightarrow> 'a :: real_normed_field" where
+definition%important harm :: "nat \<Rightarrow> 'a :: real_normed_field" where
"harm n = (\<Sum>k=1..n. inverse (of_nat k))"
lemma harm_altdef: "harm n = (\<Sum>k<n. inverse (of_nat (Suc k)))"
@@ -54,7 +54,7 @@
finally show "harm (numeral n) = harm (pred_numeral n) + inverse (numeral n)" .
qed (simp_all add: harm_def)
-lemma not_convergent_harm: "\<not>convergent (harm :: nat \<Rightarrow> 'a :: real_normed_field)"
+theorem not_convergent_harm: "\<not>convergent (harm :: nat \<Rightarrow> 'a :: real_normed_field)"
proof -
have "convergent (\<lambda>n. norm (harm n :: 'a)) \<longleftrightarrow>
convergent (harm :: nat \<Rightarrow> real)" by (simp add: norm_harm)
@@ -156,7 +156,7 @@
thus ?thesis by (subst (asm) convergent_Suc_iff)
qed
-lemma euler_mascheroni_LIMSEQ:
+lemma%important euler_mascheroni_LIMSEQ:
"(\<lambda>n. harm n - ln (of_nat n) :: real) \<longlonglongrightarrow> euler_mascheroni"
unfolding euler_mascheroni_def
by (simp add: convergent_LIMSEQ_iff [symmetric] euler_mascheroni_convergent)
@@ -187,7 +187,7 @@
thus ?thesis by simp
qed
-lemma alternating_harmonic_series_sums: "(\<lambda>k. (-1)^k / real_of_nat (Suc k)) sums ln 2"
+theorem alternating_harmonic_series_sums: "(\<lambda>k. (-1)^k / real_of_nat (Suc k)) sums ln 2"
proof -
let ?f = "\<lambda>n. harm n - ln (real_of_nat n)"
let ?g = "\<lambda>n. if even n then 0 else (2::real)"
@@ -250,7 +250,7 @@
qed
-subsection \<open>Bounds on the Euler-Mascheroni constant\<close>
+subsection%unimportant \<open>Bounds on the Euler-Mascheroni constant\<close>
(* TODO: Move? *)
lemma ln_inverse_approx_le:
@@ -340,9 +340,9 @@
lemma euler_mascheroni_lower:
- "euler_mascheroni \<ge> harm (Suc n) - ln (real_of_nat (n + 2)) + 1/real_of_nat (2 * (n + 2))"
- and euler_mascheroni_upper:
- "euler_mascheroni \<le> harm (Suc n) - ln (real_of_nat (n + 2)) + 1/real_of_nat (2 * (n + 1))"
+ "euler_mascheroni \<ge> harm (Suc n) - ln (real_of_nat (n + 2)) + 1/real_of_nat (2 * (n + 2))"
+ and euler_mascheroni_upper:
+ "euler_mascheroni \<le> harm (Suc n) - ln (real_of_nat (n + 2)) + 1/real_of_nat (2 * (n + 1))"
proof -
define D :: "_ \<Rightarrow> real"
where "D n = inverse (of_nat (n+1)) + ln (of_nat (n+1)) - ln (of_nat (n+2))" for n
--- a/src/HOL/Analysis/Integral_Test.thy Mon Jul 16 23:33:28 2018 +0100
+++ b/src/HOL/Analysis/Integral_Test.thy Mon Jul 16 23:33:38 2018 +0100
@@ -19,7 +19,7 @@
\<close>
(* TODO: continuous_in \<rightarrow> integrable_on *)
-locale antimono_fun_sum_integral_diff =
+locale%important antimono_fun_sum_integral_diff =
fixes f :: "real \<Rightarrow> real"
assumes dec: "\<And>x y. x \<ge> 0 \<Longrightarrow> x \<le> y \<Longrightarrow> f x \<ge> f y"
assumes nonneg: "\<And>x. x \<ge> 0 \<Longrightarrow> f x \<ge> 0"
@@ -89,7 +89,7 @@
using sum_integral_diff_series_Bseq sum_integral_diff_series_monoseq
by (blast intro!: Bseq_monoseq_convergent)
-lemma integral_test:
+theorem integral_test:
"summable (\<lambda>n. f (of_nat n)) \<longleftrightarrow> convergent (\<lambda>n. integral {0..of_nat n} f)"
proof -
have "summable (\<lambda>n. f (of_nat n)) \<longleftrightarrow> convergent (\<lambda>n. \<Sum>k\<le>n. f (of_nat k))"
--- a/src/HOL/Analysis/Summation_Tests.thy Mon Jul 16 23:33:28 2018 +0100
+++ b/src/HOL/Analysis/Summation_Tests.thy Mon Jul 16 23:33:38 2018 +0100
@@ -50,7 +50,7 @@
shows "limsup (\<lambda>n. ereal (root n (norm (f n)))) = ereal l"
by (intro limsup_root_limit tendsto_ereal assms)
-lemma root_test_convergence':
+theorem root_test_convergence':
fixes f :: "nat \<Rightarrow> 'a :: banach"
defines "l \<equiv> limsup (\<lambda>n. ereal (root n (norm (f n))))"
assumes l: "l < 1"
@@ -82,7 +82,7 @@
by (rule summable_comparison_test_ev[OF _ summable_geometric]) (simp add: c)
qed
-lemma root_test_divergence:
+theorem root_test_divergence:
fixes f :: "nat \<Rightarrow> 'a :: banach"
defines "l \<equiv> limsup (\<lambda>n. ereal (root n (norm (f n))))"
assumes l: "l > 1"
@@ -167,7 +167,7 @@
finally show ?case by simp
qed simp
-lemma condensation_test:
+theorem condensation_test:
assumes mono: "\<And>m. 0 < m \<Longrightarrow> f (Suc m) \<le> f m"
assumes nonneg: "\<And>n. f n \<ge> 0"
shows "summable f \<longleftrightarrow> summable (\<lambda>n. 2^n * f (2^n))"
@@ -273,7 +273,7 @@
finally show ?thesis .
qed
-lemma summable_complex_powr_iff:
+theorem summable_complex_powr_iff:
assumes "Re s < -1"
shows "summable (\<lambda>n. exp (of_real (ln (of_nat n)) * s))"
by (rule summable_norm_cancel, subst abs_summable_complex_powr_iff) fact
@@ -312,7 +312,7 @@
subsubsection \<open>Kummer's test\<close>
-lemma kummers_test_convergence:
+theorem kummers_test_convergence:
fixes f p :: "nat \<Rightarrow> real"
assumes pos_f: "eventually (\<lambda>n. f n > 0) sequentially"
assumes nonneg_p: "eventually (\<lambda>n. p n \<ge> 0) sequentially"
@@ -372,7 +372,7 @@
qed
-lemma kummers_test_divergence:
+theorem kummers_test_divergence:
fixes f p :: "nat \<Rightarrow> real"
assumes pos_f: "eventually (\<lambda>n. f n > 0) sequentially"
assumes pos_p: "eventually (\<lambda>n. p n > 0) sequentially"
@@ -403,7 +403,7 @@
subsubsection \<open>Ratio test\<close>
-lemma ratio_test_convergence:
+theorem ratio_test_convergence:
fixes f :: "nat \<Rightarrow> real"
assumes pos_f: "eventually (\<lambda>n. f n > 0) sequentially"
defines "l \<equiv> liminf (\<lambda>n. ereal (f n / f (Suc n)))"
@@ -417,7 +417,7 @@
by (cases "liminf (\<lambda>n. ereal (1 * f n / f (Suc n) - 1))") simp_all
qed simp
-lemma ratio_test_divergence:
+theorem ratio_test_divergence:
fixes f :: "nat \<Rightarrow> real"
assumes pos_f: "eventually (\<lambda>n. f n > 0) sequentially"
defines "l \<equiv> limsup (\<lambda>n. ereal (f n / f (Suc n)))"
@@ -434,7 +434,7 @@
subsubsection \<open>Raabe's test\<close>
-lemma raabes_test_convergence:
+theorem raabes_test_convergence:
fixes f :: "nat \<Rightarrow> real"
assumes pos: "eventually (\<lambda>n. f n > 0) sequentially"
defines "l \<equiv> liminf (\<lambda>n. ereal (of_nat n * (f n / f (Suc n) - 1)))"
@@ -449,7 +449,7 @@
finally show "?l' > 0" by (cases ?l') (simp_all add: algebra_simps)
qed (simp_all add: pos)
-lemma raabes_test_divergence:
+theorem raabes_test_divergence:
fixes f :: "nat \<Rightarrow> real"
assumes pos: "eventually (\<lambda>n. f n > 0) sequentially"
defines "l \<equiv> limsup (\<lambda>n. ereal (of_nat n * (f n / f (Suc n) - 1)))"
@@ -473,7 +473,7 @@
all inputs with a norm that is smaller than that radius and to diverge for all inputs with a
norm that is greater.
\<close>
-definition conv_radius :: "(nat \<Rightarrow> 'a :: banach) \<Rightarrow> ereal" where
+definition%important conv_radius :: "(nat \<Rightarrow> 'a :: banach) \<Rightarrow> ereal" where
"conv_radius f = inverse (limsup (\<lambda>n. ereal (root n (norm (f n)))))"
lemma conv_radius_cong_weak [cong]: "(\<And>n. f n = g n) \<Longrightarrow> conv_radius f = conv_radius g"
@@ -505,7 +505,7 @@
shows "conv_radius f = conv_radius g"
unfolding conv_radius_altdef by (intro Liminf_eq eventually_mono [OF assms]) auto
-lemma abs_summable_in_conv_radius:
+theorem abs_summable_in_conv_radius:
fixes f :: "nat \<Rightarrow> 'a :: {banach, real_normed_div_algebra}"
assumes "ereal (norm z) < conv_radius f"
shows "summable (\<lambda>n. norm (f n * z ^ n))"
@@ -543,7 +543,7 @@
shows "summable (\<lambda>n. f n * z ^ n)"
by (rule summable_norm_cancel, rule abs_summable_in_conv_radius) fact+
-lemma not_summable_outside_conv_radius:
+theorem not_summable_outside_conv_radius:
fixes f :: "nat \<Rightarrow> 'a :: {banach, real_normed_div_algebra}"
assumes "ereal (norm z) > conv_radius f"
shows "\<not>summable (\<lambda>n. f n * z ^ n)"
--- a/src/HOL/ROOT Mon Jul 16 23:33:28 2018 +0100
+++ b/src/HOL/ROOT Mon Jul 16 23:33:38 2018 +0100
@@ -542,6 +542,7 @@
Chinese
Classical
Code_Binary_Nat_examples
+ Code_Lazy_Demo
Code_Timing
Coercion_Examples
Coherent
--- a/src/HOL/Transcendental.thy Mon Jul 16 23:33:28 2018 +0100
+++ b/src/HOL/Transcendental.thy Mon Jul 16 23:33:38 2018 +0100
@@ -7199,6 +7199,7 @@
SOME (Thm.instantiate' [] (map (SOME o Thm.cterm_of ctxt o HOLogic.mk_numeral) [m, n])
@{thm sqrt_numeral_simproc_aux})
end
+ handle TERM _ => NONE
fun root_simproc (threshold1, threshold2) ctxt ct =
let
@@ -7212,6 +7213,8 @@
SOME (Thm.instantiate' [] (map (SOME o Thm.cterm_of ctxt o HOLogic.mk_numeral) [m, n, x])
@{thm root_numeral_simproc_aux})
end
+ handle TERM _ => NONE
+ | Match => NONE
fun powr_simproc (threshold1, threshold2) ctxt ct =
let
@@ -7233,6 +7236,8 @@
SOME (@{thm transitive} OF [eq_thm, thm])
end
end
+ handle TERM _ => NONE
+ | Match => NONE
end
\<close>
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/ex/Code_Lazy_Demo.thy Mon Jul 16 23:33:38 2018 +0100
@@ -0,0 +1,178 @@
+(* Author: Andreas Lochbihler, Digital Asset *)
+
+theory Code_Lazy_Demo imports
+ "HOL-Library.Code_Lazy"
+ "HOL-Library.Debug"
+ "HOL-Library.RBT_Impl"
+begin
+
+text \<open>This theory demonstrates the use of the @{theory "HOL-Library.Code_Lazy"} theory.\<close>
+
+section \<open>Streams\<close>
+
+text \<open>Lazy evaluation for streams\<close>
+
+codatatype 'a stream =
+ SCons (shd: 'a) (stl: "'a stream") (infixr "##" 65)
+
+primcorec up :: "nat \<Rightarrow> nat stream" where
+ "up n = n ## up (n + 1)"
+
+primrec stake :: "nat \<Rightarrow> 'a stream \<Rightarrow> 'a list" where
+ "stake 0 xs = []"
+| "stake (Suc n) xs = shd xs # stake n (stl xs)"
+
+code_thms up stake \<comment> \<open>The original code equations\<close>
+
+code_lazy_type stream
+
+code_thms up stake \<comment> \<open>The lazified code equations\<close>
+
+value "stake 5 (up 3)"
+
+
+section \<open>Finite lazy lists\<close>
+
+text \<open>Lazy types need not be infinite. We can also have lazy types that are finite.\<close>
+
+datatype 'a llist
+ = LNil ("\<^bold>\<lbrakk>\<^bold>\<rbrakk>")
+ | LCons (lhd: 'a) (ltl: "'a llist") (infixr "###" 65)
+
+syntax "_llist" :: "args => 'a list" ("\<^bold>\<lbrakk>(_)\<^bold>\<rbrakk>")
+translations
+ "\<^bold>\<lbrakk>x, xs\<^bold>\<rbrakk>" == "x###\<^bold>\<lbrakk>xs\<^bold>\<rbrakk>"
+ "\<^bold>\<lbrakk>x\<^bold>\<rbrakk>" == "x###\<^bold>\<lbrakk>\<^bold>\<rbrakk>"
+
+fun lnth :: "nat \<Rightarrow> 'a llist \<Rightarrow> 'a" where
+ "lnth 0 (x ### xs) = x"
+| "lnth (Suc n) (x ### xs) = lnth n xs"
+
+definition llist :: "nat llist" where
+ "llist = \<^bold>\<lbrakk>1, 2, 3, hd [], 4\<^bold>\<rbrakk>"
+
+code_lazy_type llist
+
+value [code] "llist"
+value [code] "lnth 2 llist"
+value [code] "let x = lnth 2 llist in (x, llist)"
+
+fun lfilter :: "('a \<Rightarrow> bool) \<Rightarrow> 'a llist \<Rightarrow> 'a llist" where
+ "lfilter P \<^bold>\<lbrakk>\<^bold>\<rbrakk> = \<^bold>\<lbrakk>\<^bold>\<rbrakk>"
+| "lfilter P (x ### xs) =
+ (if P x then x ### lfilter P xs else lfilter P xs)"
+
+export_code lfilter in SML
+
+value [code] "lfilter odd llist"
+
+value [code] "lhd (lfilter odd llist)"
+
+
+section \<open>Iterator for red-black trees\<close>
+
+text \<open>Thanks to laziness, we do not need to program a complicated iterator for a tree.
+ A conversion function to lazy lists is enough.\<close>
+
+primrec lappend :: "'a llist \<Rightarrow> 'a llist \<Rightarrow> 'a llist"
+ (infixr "@@" 65) where
+ "\<^bold>\<lbrakk>\<^bold>\<rbrakk> @@ ys = ys"
+| "(x ### xs) @@ ys = x ### (xs @@ ys)"
+
+primrec rbt_iterator :: "('a, 'b) rbt \<Rightarrow> ('a \<times> 'b) llist" where
+ "rbt_iterator rbt.Empty = \<^bold>\<lbrakk>\<^bold>\<rbrakk>"
+| "rbt_iterator (Branch _ l k v r) =
+ (let _ = Debug.flush (STR ''tick'') in
+ rbt_iterator l @@ (k, v) ### rbt_iterator r)"
+
+definition tree :: "(nat, unit) rbt"
+ where "tree = fold (\<lambda>k. rbt_insert k ()) [0..<100] rbt.Empty"
+
+definition find_min :: "('a :: linorder, 'b) rbt \<Rightarrow> ('a \<times> 'b) option" where
+ "find_min rbt =
+ (case rbt_iterator rbt of \<^bold>\<lbrakk>\<^bold>\<rbrakk> \<Rightarrow> None
+ | kv ### _ \<Rightarrow> Some kv)"
+
+value "find_min tree" \<comment> \<open>Observe that @{const rbt_iterator} is evaluated only for going down
+ to the first leaf, not for the whole tree (as seen by the ticks).\<close>
+
+text \<open>With strict lists, the whole tree is converted into a list.\<close>
+
+deactivate_lazy_type llist
+value "find_min tree"
+activate_lazy_type llist
+
+
+
+section \<open>Branching datatypes\<close>
+
+datatype tree
+ = L ("\<spadesuit>")
+ | Node tree tree (infix "\<triangle>" 900)
+
+notation (output) Node ("\<triangle>(//\<^bold>l: _//\<^bold>r: _)")
+
+code_lazy_type tree
+
+fun mk_tree :: "nat \<Rightarrow> tree" where mk_tree_0:
+ "mk_tree 0 = \<spadesuit>"
+| "mk_tree (Suc n) = (let t = mk_tree n in t \<triangle> t)"
+
+declare mk_tree.simps [code]
+
+code_thms mk_tree
+
+function subtree :: "bool list \<Rightarrow> tree \<Rightarrow> tree" where
+ "subtree [] t = t"
+| "subtree (True # p) (l \<triangle> r) = subtree p l"
+| "subtree (False # p) (l \<triangle> r) = subtree p r"
+| "subtree _ \<spadesuit> = \<spadesuit>"
+ by pat_completeness auto
+termination by lexicographic_order
+
+value [code] "mk_tree 10"
+value [code] "let t = mk_tree 10; _ = subtree [True, True, False, False] t in t"
+ \<comment> \<open>Since @{const mk_tree} shares the two subtrees of a node thanks to the let binding,
+ digging into one subtree spreads to the whole tree.\<close>
+value [code] "let t = mk_tree 3; _ = subtree [True, True, False, False] t in t"
+
+lemma mk_tree_Suc_debug [code]: \<comment> \<open>Make the evaluation visible with tracing.\<close>
+ "mk_tree (Suc n) =
+ (let _ = Debug.flush (STR ''tick''); t = mk_tree n in t \<triangle> t)"
+ by simp
+
+value [code] "mk_tree 10"
+ \<comment> \<open>The recursive call to @{const mk_tree} is not guarded by a lazy constructor,
+ so all the suspensions are built up immediately.\<close>
+
+lemma mk_tree_Suc [code]: "mk_tree (Suc n) = mk_tree n \<triangle> mk_tree n"
+ \<comment> \<open>In this code equation, there is no sharing and the recursive calls are guarded by a constructor.\<close>
+ by(simp add: Let_def)
+
+value [code] "mk_tree 10"
+value [code] "let t = mk_tree 10; _ = subtree [True, True, False, False] t in t"
+
+lemma mk_tree_Suc_debug' [code]:
+ "mk_tree (Suc n) = (let _ = Debug.flush (STR ''tick'') in mk_tree n \<triangle> mk_tree n)"
+ by(simp add: Let_def)
+
+value [code] "mk_tree 10" \<comment> \<open>Only one tick thanks to the guarding constructor\<close>
+value [code] "let t = mk_tree 10; _ = subtree [True, True, False, False] t in t"
+value [code] "let t = mk_tree 3; _ = subtree [True, True, False, False] t in t"
+
+
+section \<open>Pattern matching elimination\<close>
+
+text \<open>The pattern matching elimination handles deep pattern matches and overlapping equations
+ and only eliminates necessary pattern matches.\<close>
+
+function crazy :: "nat llist llist \<Rightarrow> tree \<Rightarrow> bool \<Rightarrow> unit" where
+ "crazy (\<^bold>\<lbrakk>0\<^bold>\<rbrakk> ### xs) _ _ = Debug.flush (1 :: integer)"
+| "crazy xs \<spadesuit> True = Debug.flush (2 :: integer)"
+| "crazy xs t b = Debug.flush (3 :: integer)"
+ by pat_completeness auto
+termination by lexicographic_order
+
+code_thms crazy
+
+end
\ No newline at end of file