--- a/src/HOL/NSA/Examples/NSPrimes.thy Thu May 20 07:34:45 2010 +0200
+++ b/src/HOL/NSA/Examples/NSPrimes.thy Thu May 20 07:36:50 2010 +0200
@@ -13,9 +13,7 @@
text{*These can be used to derive an alternative proof of the infinitude of
primes by considering a property of nonstandard sets.*}
-definition
- hdvd :: "[hypnat, hypnat] => bool" (infixl "hdvd" 50) where
- [transfer_unfold]: "(M::hypnat) hdvd N = ( *p2* (op dvd)) M N"
+declare dvd_def [transfer_refold]
definition
starprime :: "hypnat set" where
@@ -49,14 +47,14 @@
(* Goldblatt: Exercise 5.11(2) - p. 57 *)
-lemma hdvd_by_all: "\<forall>M. \<exists>N. 0 < N & (\<forall>m. 0 < m & (m::hypnat) <= M --> m hdvd N)"
+lemma hdvd_by_all: "\<forall>M. \<exists>N. 0 < N & (\<forall>m. 0 < m & (m::hypnat) <= M --> m dvd N)"
by (transfer, rule dvd_by_all)
lemmas hdvd_by_all2 = hdvd_by_all [THEN spec, standard]
(* Goldblatt: Exercise 5.11(2) - p. 57 *)
lemma hypnat_dvd_all_hypnat_of_nat:
- "\<exists>(N::hypnat). 0 < N & (\<forall>n \<in> -{0::nat}. hypnat_of_nat(n) hdvd N)"
+ "\<exists>(N::hypnat). 0 < N & (\<forall>n \<in> -{0::nat}. hypnat_of_nat(n) dvd N)"
apply (cut_tac hdvd_by_all)
apply (drule_tac x = whn in spec, auto)
apply (rule exI, auto)
@@ -70,7 +68,7 @@
(* Goldblatt: Exercise 5.11(3a) - p 57 *)
lemma starprime:
- "starprime = {p. 1 < p & (\<forall>m. m hdvd p --> m = 1 | m = p)}"
+ "starprime = {p. 1 < p & (\<forall>m. m dvd p --> m = 1 | m = p)}"
by (transfer, auto simp add: prime_def)
lemma prime_two: "prime 2"
@@ -88,13 +86,11 @@
apply (rule_tac x = n in exI, auto)
apply (drule conjI [THEN not_prime_ex_mk], auto)
apply (drule_tac x = m in spec, auto)
-apply (rule_tac x = ka in exI)
-apply (auto intro: dvd_mult2)
done
(* Goldblatt Exercise 5.11(3b) - p 57 *)
lemma hyperprime_factor_exists [rule_format]:
- "!!n. 1 < n ==> (\<exists>k \<in> starprime. k hdvd n)"
+ "!!n. 1 < n ==> (\<exists>k \<in> starprime. k dvd n)"
by (transfer, simp add: prime_factor_exists)
(* Goldblatt Exercise 3.10(1) - p. 29 *)
@@ -257,14 +253,14 @@
subsection{*Existence of Infinitely Many Primes: a Nonstandard Proof*}
-lemma lemma_not_dvd_hypnat_one: "~ (\<forall>n \<in> - {0}. hypnat_of_nat n hdvd 1)"
+lemma lemma_not_dvd_hypnat_one: "~ (\<forall>n \<in> - {0}. hypnat_of_nat n dvd 1)"
apply auto
apply (rule_tac x = 2 in bexI)
apply (transfer, auto)
done
declare lemma_not_dvd_hypnat_one [simp]
-lemma lemma_not_dvd_hypnat_one2: "\<exists>n \<in> - {0}. ~ hypnat_of_nat n hdvd 1"
+lemma lemma_not_dvd_hypnat_one2: "\<exists>n \<in> - {0}. ~ hypnat_of_nat n dvd 1"
apply (cut_tac lemma_not_dvd_hypnat_one)
apply (auto simp del: lemma_not_dvd_hypnat_one)
done
@@ -314,13 +310,13 @@
by (cut_tac hypnat_of_nat_one_not_prime, simp)
declare hypnat_one_not_prime [simp]
-lemma hdvd_diff: "!!k m n. [| k hdvd m; k hdvd n |] ==> k hdvd (m - n)"
-by (transfer, rule dvd_diff)
+lemma hdvd_diff: "!!k m n :: hypnat. [| k dvd m; k dvd n |] ==> k dvd (m - n)"
+by (transfer, rule dvd_diff_nat)
lemma dvd_one_eq_one: "x dvd (1::nat) ==> x = 1"
by (unfold dvd_def, auto)
-lemma hdvd_one_eq_one: "!!x. x hdvd 1 ==> x = 1"
+lemma hdvd_one_eq_one: "!!x. x dvd (1::hypnat) ==> x = 1"
by (transfer, rule dvd_one_eq_one)
theorem not_finite_prime: "~ finite {p. prime p}"
--- a/src/HOLCF/Fixrec.thy Thu May 20 07:34:45 2010 +0200
+++ b/src/HOLCF/Fixrec.thy Thu May 20 07:36:50 2010 +0200
@@ -65,30 +65,6 @@
== "CONST maybe_when\<cdot>t1\<cdot>(\<Lambda> x. t2)\<cdot>m"
-subsubsection {* Monadic bind operator *}
-
-definition
- bind :: "'a maybe \<rightarrow> ('a \<rightarrow> 'b maybe) \<rightarrow> 'b maybe" where
- "bind = (\<Lambda> m f. case m of fail \<Rightarrow> fail | return\<cdot>x \<Rightarrow> f\<cdot>x)"
-
-text {* monad laws *}
-
-lemma bind_strict [simp]: "bind\<cdot>\<bottom>\<cdot>f = \<bottom>"
-by (simp add: bind_def)
-
-lemma bind_fail [simp]: "bind\<cdot>fail\<cdot>f = fail"
-by (simp add: bind_def)
-
-lemma left_unit [simp]: "bind\<cdot>(return\<cdot>a)\<cdot>k = k\<cdot>a"
-by (simp add: bind_def)
-
-lemma right_unit [simp]: "bind\<cdot>m\<cdot>return = m"
-by (rule_tac p=m in maybeE, simp_all)
-
-lemma bind_assoc:
- "bind\<cdot>(bind\<cdot>m\<cdot>k)\<cdot>h = bind\<cdot>m\<cdot>(\<Lambda> a. bind\<cdot>(k\<cdot>a)\<cdot>h)"
-by (rule_tac p=m in maybeE, simp_all)
-
subsubsection {* Run operator *}
definition
@@ -169,7 +145,7 @@
definition
branch :: "('a \<rightarrow> 'b maybe) \<Rightarrow> ('b \<rightarrow> 'c) \<rightarrow> ('a \<rightarrow> 'c maybe)" where
- "branch p \<equiv> \<Lambda> r x. bind\<cdot>(p\<cdot>x)\<cdot>(\<Lambda> y. return\<cdot>(r\<cdot>y))"
+ "branch p \<equiv> \<Lambda> r x. maybe_when\<cdot>fail\<cdot>(\<Lambda> y. return\<cdot>(r\<cdot>y))\<cdot>(p\<cdot>x)"
lemma branch_rews:
"p\<cdot>x = \<bottom> \<Longrightarrow> branch p\<cdot>r\<cdot>x = \<bottom>"
@@ -277,7 +253,7 @@
definition
cpair_pat :: "('a, 'c) pat \<Rightarrow> ('b, 'd) pat \<Rightarrow> ('a \<times> 'b, 'c \<times> 'd) pat" where
"cpair_pat p1 p2 = (\<Lambda>(x, y).
- bind\<cdot>(p1\<cdot>x)\<cdot>(\<Lambda> a. bind\<cdot>(p2\<cdot>y)\<cdot>(\<Lambda> b. return\<cdot>(a, b))))"
+ maybe_when\<cdot>fail\<cdot>(\<Lambda> a. maybe_when\<cdot>fail\<cdot>(\<Lambda> b. return\<cdot>(a, b))\<cdot>(p2\<cdot>y))\<cdot>(p1\<cdot>x))"
definition
spair_pat ::
@@ -425,7 +401,7 @@
definition
as_pat :: "('a \<rightarrow> 'b maybe) \<Rightarrow> 'a \<rightarrow> ('a \<times> 'b) maybe" where
- "as_pat p = (\<Lambda> x. bind\<cdot>(p\<cdot>x)\<cdot>(\<Lambda> a. return\<cdot>(x, a)))"
+ "as_pat p = (\<Lambda> x. maybe_when\<cdot>fail\<cdot>(\<Lambda> a. return\<cdot>(x, a))\<cdot>(p\<cdot>x))"
definition
lazy_pat :: "('a \<rightarrow> 'b::pcpo maybe) \<Rightarrow> ('a \<rightarrow> 'b maybe)" where
@@ -608,7 +584,7 @@
(@{const_name UU}, @{const_name match_UU}) ]
*}
-hide_const (open) return bind fail run cases
+hide_const (open) return fail run cases
lemmas [fixrec_simp] =
run_strict run_fail run_return
--- a/src/HOLCF/IsaMakefile Thu May 20 07:34:45 2010 +0200
+++ b/src/HOLCF/IsaMakefile Thu May 20 07:36:50 2010 +0200
@@ -7,6 +7,7 @@
default: HOLCF
images: HOLCF IOA
test: HOLCF-IMP HOLCF-ex HOLCF-FOCUS \
+ HOLCF-Tutorial \
IOA-ABP IOA-NTP IOA-Modelcheck IOA-Storage IOA-ex
all: images test
@@ -78,6 +79,19 @@
@$(ISABELLE_TOOL) usedir -b -g true -r $(OUT)/HOL HOLCF
+## HOLCF-Tutorial
+
+HOLCF-Tutorial: HOLCF $(LOG)/HOLCF-Tutorial.gz
+
+$(LOG)/HOLCF-Tutorial.gz: $(OUT)/HOLCF \
+ Tutorial/Domain_ex.thy \
+ Tutorial/Fixrec_ex.thy \
+ Tutorial/New_Domain.thy \
+ Tutorial/document/root.tex \
+ Tutorial/ROOT.ML
+ @$(ISABELLE_TOOL) usedir $(OUT)/HOLCF Tutorial
+
+
## HOLCF-IMP
HOLCF-IMP: HOLCF $(LOG)/HOLCF-IMP.gz
@@ -95,15 +109,12 @@
../HOL/Library/Nat_Infinity.thy \
ex/Dagstuhl.thy \
ex/Dnat.thy \
- ex/Domain_ex.thy \
ex/Domain_Proofs.thy \
ex/Fix2.thy \
- ex/Fixrec_ex.thy \
ex/Focus_ex.thy \
ex/Hoare.thy \
ex/Letrec.thy \
ex/Loop.thy \
- ex/New_Domain.thy \
ex/Powerdomain_ex.thy \
ex/Stream.thy \
ex/Strict_Fun.thy \
@@ -201,4 +212,4 @@
$(LOG)/HOLCF-ex.gz $(LOG)/HOLCF-FOCUS.gz $(OUT)/IOA \
$(LOG)/IOA.gz $(LOG)/IOA-ABP.gz $(LOG)/IOA-NTP.gz \
$(LOG)/IOA-Modelcheck.gz $(LOG)/IOA-Storage.gz \
- $(LOG)/IOA-ex.gz
+ $(LOG)/IOA-ex.gz $(LOG)/HOLCF-Tutorial.gz
--- a/src/HOLCF/Tools/Domain/domain_constructors.ML Thu May 20 07:34:45 2010 +0200
+++ b/src/HOLCF/Tools/Domain/domain_constructors.ML Thu May 20 07:36:50 2010 +0200
@@ -952,7 +952,7 @@
val (fun1, fun2, taken) = pat_lhs (pat, args);
val defs = @{thm branch_def} :: pat_defs;
val goal = mk_trp (mk_strict fun1);
- val rules = @{thm Fixrec.bind_strict} :: case_rews;
+ val rules = @{thms maybe_when_rews} @ case_rews;
val tacs = [simp_tac (beta_ss addsimps rules) 1];
in prove thy defs goal (K tacs) end;
fun pat_apps (i, (pat, (con, args))) =
@@ -967,7 +967,7 @@
val concl = mk_trp (mk_eq (fun1 ` con_app, rhs));
val goal = Logic.list_implies (assms, concl);
val defs = @{thm branch_def} :: pat_defs;
- val rules = @{thms bind_fail left_unit} @ case_rews;
+ val rules = @{thms maybe_when_rews} @ case_rews;
val tacs = [asm_simp_tac (beta_ss addsimps rules) 1];
in prove thy defs goal (K tacs) end;
in map_index pat_app spec end;
--- a/src/HOLCF/Tools/fixrec.ML Thu May 20 07:34:45 2010 +0200
+++ b/src/HOLCF/Tools/fixrec.ML Thu May 20 07:36:50 2010 +0200
@@ -125,10 +125,20 @@
val (lhss, rhss) = ListPair.unzip (map (dest_eqs o snd) spec);
val functional = lambda_tuple lhss (mk_tuple rhss);
val fixpoint = mk_fix (mk_cabs functional);
-
+
val cont_thm =
- Goal.prove lthy [] [] (mk_trp (mk_cont functional))
- (K (simp_tac (simpset_of lthy) 1));
+ let
+ val prop = mk_trp (mk_cont functional);
+ fun err () = error (
+ "Continuity proof failed; please check that cont2cont rules\n" ^
+ "are configured for all non-HOLCF constants.\n" ^
+ "The error occurred for the goal statement:\n" ^
+ Syntax.string_of_term lthy prop);
+ fun check th = case Thm.nprems_of th of 0 => all_tac th | n => err ();
+ val tac = simp_tac (simpset_of lthy) 1 THEN check;
+ in
+ Goal.prove lthy [] [] prop (K tac)
+ end;
fun one_def (l as Free(n,_)) r =
let val b = Long_Name.base_name n
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/Tutorial/Domain_ex.thy Thu May 20 07:36:50 2010 +0200
@@ -0,0 +1,211 @@
+(* Title: HOLCF/ex/Domain_ex.thy
+ Author: Brian Huffman
+*)
+
+header {* Domain package examples *}
+
+theory Domain_ex
+imports HOLCF
+begin
+
+text {* Domain constructors are strict by default. *}
+
+domain d1 = d1a | d1b "d1" "d1"
+
+lemma "d1b\<cdot>\<bottom>\<cdot>y = \<bottom>" by simp
+
+text {* Constructors can be made lazy using the @{text "lazy"} keyword. *}
+
+domain d2 = d2a | d2b (lazy "d2")
+
+lemma "d2b\<cdot>x \<noteq> \<bottom>" by simp
+
+text {* Strict and lazy arguments may be mixed arbitrarily. *}
+
+domain d3 = d3a | d3b (lazy "d2") "d2"
+
+lemma "P (d3b\<cdot>x\<cdot>y = \<bottom>) \<longleftrightarrow> P (y = \<bottom>)" by simp
+
+text {* Selectors can be used with strict or lazy constructor arguments. *}
+
+domain d4 = d4a | d4b (lazy d4b_left :: "d2") (d4b_right :: "d2")
+
+lemma "y \<noteq> \<bottom> \<Longrightarrow> d4b_left\<cdot>(d4b\<cdot>x\<cdot>y) = x" by simp
+
+text {* Mixfix declarations can be given for data constructors. *}
+
+domain d5 = d5a | d5b (lazy "d5") "d5" (infixl ":#:" 70)
+
+lemma "d5a \<noteq> x :#: y :#: z" by simp
+
+text {* Mixfix declarations can also be given for type constructors. *}
+
+domain ('a, 'b) lazypair (infixl ":*:" 25) =
+ lpair (lazy lfst :: 'a) (lazy lsnd :: 'b) (infixl ":*:" 75)
+
+lemma "\<forall>p::('a :*: 'b). p \<sqsubseteq> lfst\<cdot>p :*: lsnd\<cdot>p"
+by (rule allI, case_tac p, simp_all)
+
+text {* Non-recursive constructor arguments can have arbitrary types. *}
+
+domain ('a, 'b) d6 = d6 "int lift" "'a \<oplus> 'b u" (lazy "('a :*: 'b) \<times> ('b \<rightarrow> 'a)")
+
+text {*
+ Indirect recusion is allowed for sums, products, lifting, and the
+ continuous function space. However, the domain package does not
+ generate an induction rule in terms of the constructors.
+*}
+
+domain 'a d7 = d7a "'a d7 \<oplus> int lift" | d7b "'a \<otimes> 'a d7" | d7c (lazy "'a d7 \<rightarrow> 'a")
+ -- "Indirect recursion detected, skipping proofs of (co)induction rules"
+
+text {* Note that @{text d7.induct} is absent. *}
+
+text {*
+ Indirect recursion is also allowed using previously-defined datatypes.
+*}
+
+domain 'a slist = SNil | SCons 'a "'a slist"
+
+domain 'a stree = STip | SBranch "'a stree slist"
+
+text {* Mutually-recursive datatypes can be defined using the @{text "and"} keyword. *}
+
+domain d8 = d8a | d8b "d9" and d9 = d9a | d9b (lazy "d8")
+
+text {* Non-regular recursion is not allowed. *}
+(*
+domain ('a, 'b) altlist = ANil | ACons 'a "('b, 'a) altlist"
+ -- "illegal direct recursion with different arguments"
+domain 'a nest = Nest1 'a | Nest2 "'a nest nest"
+ -- "illegal direct recursion with different arguments"
+*)
+
+text {*
+ Mutually-recursive datatypes must have all the same type arguments,
+ not necessarily in the same order.
+*}
+
+domain ('a, 'b) list1 = Nil1 | Cons1 'a "('b, 'a) list2"
+ and ('b, 'a) list2 = Nil2 | Cons2 'b "('a, 'b) list1"
+
+text {* Induction rules for flat datatypes have no admissibility side-condition. *}
+
+domain 'a flattree = Tip | Branch "'a flattree" "'a flattree"
+
+lemma "\<lbrakk>P \<bottom>; P Tip; \<And>x y. \<lbrakk>x \<noteq> \<bottom>; y \<noteq> \<bottom>; P x; P y\<rbrakk> \<Longrightarrow> P (Branch\<cdot>x\<cdot>y)\<rbrakk> \<Longrightarrow> P x"
+by (rule flattree.induct) -- "no admissibility requirement"
+
+text {* Trivial datatypes will produce a warning message. *}
+
+domain triv = Triv triv triv
+ -- "domain @{text Domain_ex.triv} is empty!"
+
+lemma "(x::triv) = \<bottom>" by (induct x, simp_all)
+
+text {* Lazy constructor arguments may have unpointed types. *}
+
+domain natlist = nnil | ncons (lazy "nat discr") natlist
+
+text {* Class constraints may be given for type parameters on the LHS. *}
+
+domain ('a::cpo) box = Box (lazy 'a)
+
+
+subsection {* Generated constants and theorems *}
+
+domain 'a tree = Leaf (lazy 'a) | Node (left :: "'a tree") (right :: "'a tree")
+
+lemmas tree_abs_defined_iff =
+ iso.abs_defined_iff [OF iso.intro [OF tree.abs_iso tree.rep_iso]]
+
+text {* Rules about ismorphism *}
+term tree_rep
+term tree_abs
+thm tree.rep_iso
+thm tree.abs_iso
+thm tree.iso_rews
+
+text {* Rules about constructors *}
+term Leaf
+term Node
+thm Leaf_def Node_def
+thm tree.nchotomy
+thm tree.exhaust
+thm tree.compacts
+thm tree.con_rews
+thm tree.dist_les
+thm tree.dist_eqs
+thm tree.inverts
+thm tree.injects
+
+text {* Rules about case combinator *}
+term tree_when
+thm tree.tree_when_def
+thm tree.when_rews
+
+text {* Rules about selectors *}
+term left
+term right
+thm tree.sel_rews
+
+text {* Rules about discriminators *}
+term is_Leaf
+term is_Node
+thm tree.dis_rews
+
+text {* Rules about pattern match combinators *}
+term Leaf_pat
+term Node_pat
+thm tree.pat_rews
+
+text {* Rules about monadic pattern match combinators *}
+term match_Leaf
+term match_Node
+thm tree.match_rews
+
+text {* Rules about take function *}
+term tree_take
+thm tree.take_def
+thm tree.take_0
+thm tree.take_Suc
+thm tree.take_rews
+thm tree.chain_take
+thm tree.take_take
+thm tree.deflation_take
+thm tree.take_below
+thm tree.take_lemma
+thm tree.lub_take
+thm tree.reach
+thm tree.finite_induct
+
+text {* Rules about finiteness predicate *}
+term tree_finite
+thm tree.finite_def
+thm tree.finite (* only generated for flat datatypes *)
+
+text {* Rules about bisimulation predicate *}
+term tree_bisim
+thm tree.bisim_def
+thm tree.coinduct
+
+text {* Induction rule *}
+thm tree.induct
+
+
+subsection {* Known bugs *}
+
+text {* Declaring a mixfix with spaces causes some strange parse errors. *}
+(*
+domain xx = xx ("x y")
+ -- "Inner syntax error: unexpected end of input"
+*)
+
+text {*
+ Non-cpo type parameters currently do not work.
+*}
+(*
+domain ('a::type) stream = snil | scons (lazy "'a discr") "'a stream"
+*)
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/Tutorial/Fixrec_ex.thy Thu May 20 07:36:50 2010 +0200
@@ -0,0 +1,246 @@
+(* Title: HOLCF/ex/Fixrec_ex.thy
+ Author: Brian Huffman
+*)
+
+header {* Fixrec package examples *}
+
+theory Fixrec_ex
+imports HOLCF
+begin
+
+subsection {* Basic @{text fixrec} examples *}
+
+text {*
+ Fixrec patterns can mention any constructor defined by the domain
+ package, as well as any of the following built-in constructors:
+ Pair, spair, sinl, sinr, up, ONE, TT, FF.
+*}
+
+text {* Typical usage is with lazy constructors. *}
+
+fixrec down :: "'a u \<rightarrow> 'a"
+where "down\<cdot>(up\<cdot>x) = x"
+
+text {* With strict constructors, rewrite rules may require side conditions. *}
+
+fixrec from_sinl :: "'a \<oplus> 'b \<rightarrow> 'a"
+where "x \<noteq> \<bottom> \<Longrightarrow> from_sinl\<cdot>(sinl\<cdot>x) = x"
+
+text {* Lifting can turn a strict constructor into a lazy one. *}
+
+fixrec from_sinl_up :: "'a u \<oplus> 'b \<rightarrow> 'a"
+where "from_sinl_up\<cdot>(sinl\<cdot>(up\<cdot>x)) = x"
+
+text {* Fixrec also works with the HOL pair constructor. *}
+
+fixrec down2 :: "'a u \<times> 'b u \<rightarrow> 'a \<times> 'b"
+where "down2\<cdot>(up\<cdot>x, up\<cdot>y) = (x, y)"
+
+
+subsection {* Examples using @{text fixrec_simp} *}
+
+text {* A type of lazy lists. *}
+
+domain 'a llist = lNil | lCons (lazy 'a) (lazy "'a llist")
+
+text {* A zip function for lazy lists. *}
+
+text {* Notice that the patterns are not exhaustive. *}
+
+fixrec
+ lzip :: "'a llist \<rightarrow> 'b llist \<rightarrow> ('a \<times> 'b) llist"
+where
+ "lzip\<cdot>(lCons\<cdot>x\<cdot>xs)\<cdot>(lCons\<cdot>y\<cdot>ys) = lCons\<cdot>(x, y)\<cdot>(lzip\<cdot>xs\<cdot>ys)"
+| "lzip\<cdot>lNil\<cdot>lNil = lNil"
+
+text {* @{text fixrec_simp} is useful for producing strictness theorems. *}
+text {* Note that pattern matching is done in left-to-right order. *}
+
+lemma lzip_stricts [simp]:
+ "lzip\<cdot>\<bottom>\<cdot>ys = \<bottom>"
+ "lzip\<cdot>lNil\<cdot>\<bottom> = \<bottom>"
+ "lzip\<cdot>(lCons\<cdot>x\<cdot>xs)\<cdot>\<bottom> = \<bottom>"
+by fixrec_simp+
+
+text {* @{text fixrec_simp} can also produce rules for missing cases. *}
+
+lemma lzip_undefs [simp]:
+ "lzip\<cdot>lNil\<cdot>(lCons\<cdot>y\<cdot>ys) = \<bottom>"
+ "lzip\<cdot>(lCons\<cdot>x\<cdot>xs)\<cdot>lNil = \<bottom>"
+by fixrec_simp+
+
+
+subsection {* Pattern matching with bottoms *}
+
+text {*
+ As an alternative to using @{text fixrec_simp}, it is also possible
+ to use bottom as a constructor pattern. When using a bottom
+ pattern, the right-hand-side must also be bottom; otherwise, @{text
+ fixrec} will not be able to prove the equation.
+*}
+
+fixrec
+ from_sinr_up :: "'a \<oplus> 'b\<^sub>\<bottom> \<rightarrow> 'b"
+where
+ "from_sinr_up\<cdot>\<bottom> = \<bottom>"
+| "from_sinr_up\<cdot>(sinr\<cdot>(up\<cdot>x)) = x"
+
+text {*
+ If the function is already strict in that argument, then the bottom
+ pattern does not change the meaning of the function. For example,
+ in the definition of @{term from_sinr_up}, the first equation is
+ actually redundant, and could have been proven separately by
+ @{text fixrec_simp}.
+*}
+
+text {*
+ A bottom pattern can also be used to make a function strict in a
+ certain argument, similar to a bang-pattern in Haskell.
+*}
+
+fixrec
+ seq :: "'a \<rightarrow> 'b \<rightarrow> 'b"
+where
+ "seq\<cdot>\<bottom>\<cdot>y = \<bottom>"
+| "x \<noteq> \<bottom> \<Longrightarrow> seq\<cdot>x\<cdot>y = y"
+
+
+subsection {* Skipping proofs of rewrite rules *}
+
+text {* Another zip function for lazy lists. *}
+
+text {*
+ Notice that this version has overlapping patterns.
+ The second equation cannot be proved as a theorem
+ because it only applies when the first pattern fails.
+*}
+
+fixrec (permissive)
+ lzip2 :: "'a llist \<rightarrow> 'b llist \<rightarrow> ('a \<times> 'b) llist"
+where
+ "lzip2\<cdot>(lCons\<cdot>x\<cdot>xs)\<cdot>(lCons\<cdot>y\<cdot>ys) = lCons\<cdot>(x, y)\<cdot>(lzip\<cdot>xs\<cdot>ys)"
+| "lzip2\<cdot>xs\<cdot>ys = lNil"
+
+text {*
+ Usually fixrec tries to prove all equations as theorems.
+ The "permissive" option overrides this behavior, so fixrec
+ does not produce any simp rules.
+*}
+
+text {* Simp rules can be generated later using @{text fixrec_simp}. *}
+
+lemma lzip2_simps [simp]:
+ "lzip2\<cdot>(lCons\<cdot>x\<cdot>xs)\<cdot>(lCons\<cdot>y\<cdot>ys) = lCons\<cdot>(x, y)\<cdot>(lzip\<cdot>xs\<cdot>ys)"
+ "lzip2\<cdot>(lCons\<cdot>x\<cdot>xs)\<cdot>lNil = lNil"
+ "lzip2\<cdot>lNil\<cdot>(lCons\<cdot>y\<cdot>ys) = lNil"
+ "lzip2\<cdot>lNil\<cdot>lNil = lNil"
+by fixrec_simp+
+
+lemma lzip2_stricts [simp]:
+ "lzip2\<cdot>\<bottom>\<cdot>ys = \<bottom>"
+ "lzip2\<cdot>(lCons\<cdot>x\<cdot>xs)\<cdot>\<bottom> = \<bottom>"
+by fixrec_simp+
+
+
+subsection {* Mutual recursion with @{text fixrec} *}
+
+text {* Tree and forest types. *}
+
+domain 'a tree = Leaf (lazy 'a) | Branch (lazy "'a forest")
+and 'a forest = Empty | Trees (lazy "'a tree") "'a forest"
+
+text {*
+ To define mutually recursive functions, give multiple type signatures
+ separated by the keyword @{text "and"}.
+*}
+
+fixrec
+ map_tree :: "('a \<rightarrow> 'b) \<rightarrow> ('a tree \<rightarrow> 'b tree)"
+and
+ map_forest :: "('a \<rightarrow> 'b) \<rightarrow> ('a forest \<rightarrow> 'b forest)"
+where
+ "map_tree\<cdot>f\<cdot>(Leaf\<cdot>x) = Leaf\<cdot>(f\<cdot>x)"
+| "map_tree\<cdot>f\<cdot>(Branch\<cdot>ts) = Branch\<cdot>(map_forest\<cdot>f\<cdot>ts)"
+| "map_forest\<cdot>f\<cdot>Empty = Empty"
+| "ts \<noteq> \<bottom> \<Longrightarrow>
+ map_forest\<cdot>f\<cdot>(Trees\<cdot>t\<cdot>ts) = Trees\<cdot>(map_tree\<cdot>f\<cdot>t)\<cdot>(map_forest\<cdot>f\<cdot>ts)"
+
+lemma map_tree_strict [simp]: "map_tree\<cdot>f\<cdot>\<bottom> = \<bottom>"
+by fixrec_simp
+
+lemma map_forest_strict [simp]: "map_forest\<cdot>f\<cdot>\<bottom> = \<bottom>"
+by fixrec_simp
+
+(*
+ Theorems generated:
+ @{text map_tree_def} @{thm map_tree_def}
+ @{text map_forest_def} @{thm map_forest_def}
+ @{text map_tree.unfold} @{thm map_tree.unfold}
+ @{text map_forest.unfold} @{thm map_forest.unfold}
+ @{text map_tree.simps} @{thm map_tree.simps}
+ @{text map_forest.simps} @{thm map_forest.simps}
+ @{text map_tree_map_forest.induct} @{thm map_tree_map_forest.induct}
+*)
+
+
+subsection {* Looping simp rules *}
+
+text {*
+ The defining equations of a fixrec definition are declared as simp
+ rules by default. In some cases, especially for constants with no
+ arguments or functions with variable patterns, the defining
+ equations may cause the simplifier to loop. In these cases it will
+ be necessary to use a @{text "[simp del]"} declaration.
+*}
+
+fixrec
+ repeat :: "'a \<rightarrow> 'a llist"
+where
+ [simp del]: "repeat\<cdot>x = lCons\<cdot>x\<cdot>(repeat\<cdot>x)"
+
+text {*
+ We can derive other non-looping simp rules for @{const repeat} by
+ using the @{text subst} method with the @{text repeat.simps} rule.
+*}
+
+lemma repeat_simps [simp]:
+ "repeat\<cdot>x \<noteq> \<bottom>"
+ "repeat\<cdot>x \<noteq> lNil"
+ "repeat\<cdot>x = lCons\<cdot>y\<cdot>ys \<longleftrightarrow> x = y \<and> repeat\<cdot>x = ys"
+by (subst repeat.simps, simp)+
+
+lemma llist_when_repeat [simp]:
+ "llist_when\<cdot>z\<cdot>f\<cdot>(repeat\<cdot>x) = f\<cdot>x\<cdot>(repeat\<cdot>x)"
+by (subst repeat.simps, simp)
+
+text {*
+ For mutually-recursive constants, looping might only occur if all
+ equations are in the simpset at the same time. In such cases it may
+ only be necessary to declare @{text "[simp del]"} on one equation.
+*}
+
+fixrec
+ inf_tree :: "'a tree" and inf_forest :: "'a forest"
+where
+ [simp del]: "inf_tree = Branch\<cdot>inf_forest"
+| "inf_forest = Trees\<cdot>inf_tree\<cdot>(Trees\<cdot>inf_tree\<cdot>Empty)"
+
+
+subsection {* Using @{text fixrec} inside locales *}
+
+locale test =
+ fixes foo :: "'a \<rightarrow> 'a"
+ assumes foo_strict: "foo\<cdot>\<bottom> = \<bottom>"
+begin
+
+fixrec
+ bar :: "'a u \<rightarrow> 'a"
+where
+ "bar\<cdot>(up\<cdot>x) = foo\<cdot>x"
+
+lemma bar_strict: "bar\<cdot>\<bottom> = \<bottom>"
+by fixrec_simp
+
+end
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/Tutorial/New_Domain.thy Thu May 20 07:36:50 2010 +0200
@@ -0,0 +1,92 @@
+(* Title: HOLCF/ex/New_Domain.thy
+ Author: Brian Huffman
+*)
+
+header {* Definitional domain package *}
+
+theory New_Domain
+imports HOLCF
+begin
+
+text {*
+ The definitional domain package only works with representable domains,
+ i.e. types in class @{text rep}.
+*}
+
+default_sort rep
+
+text {*
+ Provided that @{text rep} is the default sort, the @{text new_domain}
+ package should work with any type definition supported by the old
+ domain package.
+*}
+
+new_domain 'a llist = LNil | LCons (lazy 'a) (lazy "'a llist")
+
+text {*
+ The difference is that the new domain package is completely
+ definitional, and does not generate any axioms. The following type
+ and constant definitions are not produced by the old domain package.
+*}
+
+thm type_definition_llist
+thm llist_abs_def llist_rep_def
+
+text {*
+ The new domain package also adds support for indirect recursion with
+ user-defined datatypes. This definition of a tree datatype uses
+ indirect recursion through the lazy list type constructor.
+*}
+
+new_domain 'a ltree = Leaf (lazy 'a) | Branch (lazy "'a ltree llist")
+
+text {*
+ For indirect-recursive definitions, the domain package is not able to
+ generate a high-level induction rule. (It produces a warning
+ message instead.) The low-level reach lemma (now proved as a
+ theorem, no longer generated as an axiom) can be used to derive
+ other induction rules.
+*}
+
+thm ltree.reach
+
+text {*
+ The definition of the take function uses map functions associated with
+ each type constructor involved in the definition. A map function
+ for the lazy list type has been generated by the new domain package.
+*}
+
+thm ltree.take_rews
+thm llist_map_def
+
+lemma ltree_induct:
+ fixes P :: "'a ltree \<Rightarrow> bool"
+ assumes adm: "adm P"
+ assumes bot: "P \<bottom>"
+ assumes Leaf: "\<And>x. P (Leaf\<cdot>x)"
+ assumes Branch: "\<And>f l. \<forall>x. P (f\<cdot>x) \<Longrightarrow> P (Branch\<cdot>(llist_map\<cdot>f\<cdot>l))"
+ shows "P x"
+proof -
+ have "P (\<Squnion>i. ltree_take i\<cdot>x)"
+ using adm
+ proof (rule admD)
+ fix i
+ show "P (ltree_take i\<cdot>x)"
+ proof (induct i arbitrary: x)
+ case (0 x)
+ show "P (ltree_take 0\<cdot>x)" by (simp add: bot)
+ next
+ case (Suc n x)
+ show "P (ltree_take (Suc n)\<cdot>x)"
+ apply (cases x)
+ apply (simp add: bot)
+ apply (simp add: Leaf)
+ apply (simp add: Branch Suc)
+ done
+ qed
+ qed (simp add: ltree.chain_take)
+ thus ?thesis
+ by (simp add: ltree.reach)
+qed
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/Tutorial/ROOT.ML Thu May 20 07:36:50 2010 +0200
@@ -0,0 +1,1 @@
+use_thys ["Domain_ex", "Fixrec_ex", "New_Domain"];
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/Tutorial/document/root.tex Thu May 20 07:36:50 2010 +0200
@@ -0,0 +1,29 @@
+
+% HOLCF/document/root.tex
+
+\documentclass[11pt,a4paper]{article}
+\usepackage{graphicx,isabelle,isabellesym,latexsym}
+\usepackage[only,bigsqcap]{stmaryrd}
+\usepackage[latin1]{inputenc}
+\usepackage{pdfsetup}
+
+\urlstyle{rm}
+%\isabellestyle{it}
+\pagestyle{myheadings}
+
+\begin{document}
+
+\title{Isabelle/HOLCF Tutorial}
+\maketitle
+
+\tableofcontents
+
+%\newpage
+
+%\renewcommand{\isamarkupheader}[1]%
+%{\section{\isabellecontext: #1}\markright{THEORY~``\isabellecontext''}}
+
+\parindent 0pt\parskip 0.5ex
+\input{session}
+
+\end{document}
--- a/src/HOLCF/ex/Domain_ex.thy Thu May 20 07:34:45 2010 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,210 +0,0 @@
-(* Title: HOLCF/ex/Domain_ex.thy
- Author: Brian Huffman
-*)
-
-header {* Domain package examples *}
-
-theory Domain_ex
-imports HOLCF
-begin
-
-text {* Domain constructors are strict by default. *}
-
-domain d1 = d1a | d1b "d1" "d1"
-
-lemma "d1b\<cdot>\<bottom>\<cdot>y = \<bottom>" by simp
-
-text {* Constructors can be made lazy using the @{text "lazy"} keyword. *}
-
-domain d2 = d2a | d2b (lazy "d2")
-
-lemma "d2b\<cdot>x \<noteq> \<bottom>" by simp
-
-text {* Strict and lazy arguments may be mixed arbitrarily. *}
-
-domain d3 = d3a | d3b (lazy "d2") "d2"
-
-lemma "P (d3b\<cdot>x\<cdot>y = \<bottom>) \<longleftrightarrow> P (y = \<bottom>)" by simp
-
-text {* Selectors can be used with strict or lazy constructor arguments. *}
-
-domain d4 = d4a | d4b (lazy d4b_left :: "d2") (d4b_right :: "d2")
-
-lemma "y \<noteq> \<bottom> \<Longrightarrow> d4b_left\<cdot>(d4b\<cdot>x\<cdot>y) = x" by simp
-
-text {* Mixfix declarations can be given for data constructors. *}
-
-domain d5 = d5a | d5b (lazy "d5") "d5" (infixl ":#:" 70)
-
-lemma "d5a \<noteq> x :#: y :#: z" by simp
-
-text {* Mixfix declarations can also be given for type constructors. *}
-
-domain ('a, 'b) lazypair (infixl ":*:" 25) =
- lpair (lazy lfst :: 'a) (lazy lsnd :: 'b) (infixl ":*:" 75)
-
-lemma "\<forall>p::('a :*: 'b). p \<sqsubseteq> lfst\<cdot>p :*: lsnd\<cdot>p"
-by (rule allI, case_tac p, simp_all)
-
-text {* Non-recursive constructor arguments can have arbitrary types. *}
-
-domain ('a, 'b) d6 = d6 "int lift" "'a \<oplus> 'b u" (lazy "('a :*: 'b) \<times> ('b \<rightarrow> 'a)")
-
-text {*
- Indirect recusion is allowed for sums, products, lifting, and the
- continuous function space. However, the domain package does not
- generate an induction rule in terms of the constructors.
-*}
-
-domain 'a d7 = d7a "'a d7 \<oplus> int lift" | d7b "'a \<otimes> 'a d7" | d7c (lazy "'a d7 \<rightarrow> 'a")
- -- "Indirect recursion detected, skipping proofs of (co)induction rules"
-(* d7.induct is absent *)
-
-text {*
- Indirect recursion is also allowed using previously-defined datatypes.
-*}
-
-domain 'a slist = SNil | SCons 'a "'a slist"
-
-domain 'a stree = STip | SBranch "'a stree slist"
-
-text {* Mutually-recursive datatypes can be defined using the @{text "and"} keyword. *}
-
-domain d8 = d8a | d8b "d9" and d9 = d9a | d9b (lazy "d8")
-
-text {* Non-regular recursion is not allowed. *}
-(*
-domain ('a, 'b) altlist = ANil | ACons 'a "('b, 'a) altlist"
- -- "illegal direct recursion with different arguments"
-domain 'a nest = Nest1 'a | Nest2 "'a nest nest"
- -- "illegal direct recursion with different arguments"
-*)
-
-text {*
- Mutually-recursive datatypes must have all the same type arguments,
- not necessarily in the same order.
-*}
-
-domain ('a, 'b) list1 = Nil1 | Cons1 'a "('b, 'a) list2"
- and ('b, 'a) list2 = Nil2 | Cons2 'b "('a, 'b) list1"
-
-text {* Induction rules for flat datatypes have no admissibility side-condition. *}
-
-domain 'a flattree = Tip | Branch "'a flattree" "'a flattree"
-
-lemma "\<lbrakk>P \<bottom>; P Tip; \<And>x y. \<lbrakk>x \<noteq> \<bottom>; y \<noteq> \<bottom>; P x; P y\<rbrakk> \<Longrightarrow> P (Branch\<cdot>x\<cdot>y)\<rbrakk> \<Longrightarrow> P x"
-by (rule flattree.induct) -- "no admissibility requirement"
-
-text {* Trivial datatypes will produce a warning message. *}
-
-domain triv = Triv triv triv
- -- "domain Domain_ex.triv is empty!"
-
-lemma "(x::triv) = \<bottom>" by (induct x, simp_all)
-
-text {* Lazy constructor arguments may have unpointed types. *}
-
-domain natlist = nnil | ncons (lazy "nat discr") natlist
-
-text {* Class constraints may be given for type parameters on the LHS. *}
-
-domain ('a::cpo) box = Box (lazy 'a)
-
-
-subsection {* Generated constants and theorems *}
-
-domain 'a tree = Leaf (lazy 'a) | Node (left :: "'a tree") (right :: "'a tree")
-
-lemmas tree_abs_defined_iff =
- iso.abs_defined_iff [OF iso.intro [OF tree.abs_iso tree.rep_iso]]
-
-text {* Rules about ismorphism *}
-term tree_rep
-term tree_abs
-thm tree.rep_iso
-thm tree.abs_iso
-thm tree.iso_rews
-
-text {* Rules about constructors *}
-term Leaf
-term Node
-thm Leaf_def Node_def
-thm tree.nchotomy
-thm tree.exhaust
-thm tree.compacts
-thm tree.con_rews
-thm tree.dist_les
-thm tree.dist_eqs
-thm tree.inverts
-thm tree.injects
-
-text {* Rules about case combinator *}
-term tree_when
-thm tree.tree_when_def
-thm tree.when_rews
-
-text {* Rules about selectors *}
-term left
-term right
-thm tree.sel_rews
-
-text {* Rules about discriminators *}
-term is_Leaf
-term is_Node
-thm tree.dis_rews
-
-text {* Rules about pattern match combinators *}
-term Leaf_pat
-term Node_pat
-thm tree.pat_rews
-
-text {* Rules about monadic pattern match combinators *}
-term match_Leaf
-term match_Node
-thm tree.match_rews
-
-text {* Rules about take function *}
-term tree_take
-thm tree.take_def
-thm tree.take_0
-thm tree.take_Suc
-thm tree.take_rews
-thm tree.chain_take
-thm tree.take_take
-thm tree.deflation_take
-thm tree.take_below
-thm tree.take_lemma
-thm tree.lub_take
-thm tree.reach
-thm tree.finite_induct
-
-text {* Rules about finiteness predicate *}
-term tree_finite
-thm tree.finite_def
-thm tree.finite (* only generated for flat datatypes *)
-
-text {* Rules about bisimulation predicate *}
-term tree_bisim
-thm tree.bisim_def
-thm tree.coinduct
-
-text {* Induction rule *}
-thm tree.induct
-
-
-subsection {* Known bugs *}
-
-text {* Declaring a mixfix with spaces causes some strange parse errors. *}
-(*
-domain xx = xx ("x y")
- -- "Inner syntax error: unexpected end of input"
-*)
-
-text {*
- Non-cpo type parameters currently do not work.
-*}
-(*
-domain ('a::type) stream = snil | scons (lazy "'a discr") "'a stream"
-*)
-
-end
--- a/src/HOLCF/ex/Fixrec_ex.thy Thu May 20 07:34:45 2010 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,203 +0,0 @@
-(* Title: HOLCF/ex/Fixrec_ex.thy
- Author: Brian Huffman
-*)
-
-header {* Fixrec package examples *}
-
-theory Fixrec_ex
-imports HOLCF
-begin
-
-subsection {* Basic @{text fixrec} examples *}
-
-text {*
- Fixrec patterns can mention any constructor defined by the domain
- package, as well as any of the following built-in constructors:
- Pair, spair, sinl, sinr, up, ONE, TT, FF.
-*}
-
-text {* Typical usage is with lazy constructors. *}
-
-fixrec down :: "'a u \<rightarrow> 'a"
-where "down\<cdot>(up\<cdot>x) = x"
-
-text {* With strict constructors, rewrite rules may require side conditions. *}
-
-fixrec from_sinl :: "'a \<oplus> 'b \<rightarrow> 'a"
-where "x \<noteq> \<bottom> \<Longrightarrow> from_sinl\<cdot>(sinl\<cdot>x) = x"
-
-text {* Lifting can turn a strict constructor into a lazy one. *}
-
-fixrec from_sinl_up :: "'a u \<oplus> 'b \<rightarrow> 'a"
-where "from_sinl_up\<cdot>(sinl\<cdot>(up\<cdot>x)) = x"
-
-text {* Fixrec also works with the HOL pair constructor. *}
-
-fixrec down2 :: "'a u \<times> 'b u \<rightarrow> 'a \<times> 'b"
-where "down2\<cdot>(up\<cdot>x, up\<cdot>y) = (x, y)"
-
-
-subsection {* Examples using @{text fixrec_simp} *}
-
-text {* A type of lazy lists. *}
-
-domain 'a llist = lNil | lCons (lazy 'a) (lazy "'a llist")
-
-text {* A zip function for lazy lists. *}
-
-text {* Notice that the patterns are not exhaustive. *}
-
-fixrec
- lzip :: "'a llist \<rightarrow> 'b llist \<rightarrow> ('a \<times> 'b) llist"
-where
- "lzip\<cdot>(lCons\<cdot>x\<cdot>xs)\<cdot>(lCons\<cdot>y\<cdot>ys) = lCons\<cdot>(x, y)\<cdot>(lzip\<cdot>xs\<cdot>ys)"
-| "lzip\<cdot>lNil\<cdot>lNil = lNil"
-
-text {* @{text fixrec_simp} is useful for producing strictness theorems. *}
-text {* Note that pattern matching is done in left-to-right order. *}
-
-lemma lzip_stricts [simp]:
- "lzip\<cdot>\<bottom>\<cdot>ys = \<bottom>"
- "lzip\<cdot>lNil\<cdot>\<bottom> = \<bottom>"
- "lzip\<cdot>(lCons\<cdot>x\<cdot>xs)\<cdot>\<bottom> = \<bottom>"
-by fixrec_simp+
-
-text {* @{text fixrec_simp} can also produce rules for missing cases. *}
-
-lemma lzip_undefs [simp]:
- "lzip\<cdot>lNil\<cdot>(lCons\<cdot>y\<cdot>ys) = \<bottom>"
- "lzip\<cdot>(lCons\<cdot>x\<cdot>xs)\<cdot>lNil = \<bottom>"
-by fixrec_simp+
-
-
-subsection {* Pattern matching with bottoms *}
-
-text {*
- As an alternative to using @{text fixrec_simp}, it is also possible
- to use bottom as a constructor pattern. When using a bottom
- pattern, the right-hand-side must also be bottom; otherwise, @{text
- fixrec} will not be able to prove the equation.
-*}
-
-fixrec
- from_sinr_up :: "'a \<oplus> 'b\<^sub>\<bottom> \<rightarrow> 'b"
-where
- "from_sinr_up\<cdot>\<bottom> = \<bottom>"
-| "from_sinr_up\<cdot>(sinr\<cdot>(up\<cdot>x)) = x"
-
-text {*
- If the function is already strict in that argument, then the bottom
- pattern does not change the meaning of the function. For example,
- in the definition of @{term from_sinr_up}, the first equation is
- actually redundant, and could have been proven separately by
- @{text fixrec_simp}.
-*}
-
-text {*
- A bottom pattern can also be used to make a function strict in a
- certain argument, similar to a bang-pattern in Haskell.
-*}
-
-fixrec
- seq :: "'a \<rightarrow> 'b \<rightarrow> 'b"
-where
- "seq\<cdot>\<bottom>\<cdot>y = \<bottom>"
-| "x \<noteq> \<bottom> \<Longrightarrow> seq\<cdot>x\<cdot>y = y"
-
-
-subsection {* Skipping proofs of rewrite rules *}
-
-text {* Another zip function for lazy lists. *}
-
-text {*
- Notice that this version has overlapping patterns.
- The second equation cannot be proved as a theorem
- because it only applies when the first pattern fails.
-*}
-
-fixrec (permissive)
- lzip2 :: "'a llist \<rightarrow> 'b llist \<rightarrow> ('a \<times> 'b) llist"
-where
- "lzip2\<cdot>(lCons\<cdot>x\<cdot>xs)\<cdot>(lCons\<cdot>y\<cdot>ys) = lCons\<cdot>(x, y)\<cdot>(lzip\<cdot>xs\<cdot>ys)"
-| "lzip2\<cdot>xs\<cdot>ys = lNil"
-
-text {*
- Usually fixrec tries to prove all equations as theorems.
- The "permissive" option overrides this behavior, so fixrec
- does not produce any simp rules.
-*}
-
-text {* Simp rules can be generated later using @{text fixrec_simp}. *}
-
-lemma lzip2_simps [simp]:
- "lzip2\<cdot>(lCons\<cdot>x\<cdot>xs)\<cdot>(lCons\<cdot>y\<cdot>ys) = lCons\<cdot>(x, y)\<cdot>(lzip\<cdot>xs\<cdot>ys)"
- "lzip2\<cdot>(lCons\<cdot>x\<cdot>xs)\<cdot>lNil = lNil"
- "lzip2\<cdot>lNil\<cdot>(lCons\<cdot>y\<cdot>ys) = lNil"
- "lzip2\<cdot>lNil\<cdot>lNil = lNil"
-by fixrec_simp+
-
-lemma lzip2_stricts [simp]:
- "lzip2\<cdot>\<bottom>\<cdot>ys = \<bottom>"
- "lzip2\<cdot>(lCons\<cdot>x\<cdot>xs)\<cdot>\<bottom> = \<bottom>"
-by fixrec_simp+
-
-
-subsection {* Mutual recursion with @{text fixrec} *}
-
-text {* Tree and forest types. *}
-
-domain 'a tree = Leaf (lazy 'a) | Branch (lazy "'a forest")
-and 'a forest = Empty | Trees (lazy "'a tree") "'a forest"
-
-text {*
- To define mutually recursive functions, give multiple type signatures
- separated by the keyword @{text "and"}.
-*}
-
-fixrec
- map_tree :: "('a \<rightarrow> 'b) \<rightarrow> ('a tree \<rightarrow> 'b tree)"
-and
- map_forest :: "('a \<rightarrow> 'b) \<rightarrow> ('a forest \<rightarrow> 'b forest)"
-where
- "map_tree\<cdot>f\<cdot>(Leaf\<cdot>x) = Leaf\<cdot>(f\<cdot>x)"
-| "map_tree\<cdot>f\<cdot>(Branch\<cdot>ts) = Branch\<cdot>(map_forest\<cdot>f\<cdot>ts)"
-| "map_forest\<cdot>f\<cdot>Empty = Empty"
-| "ts \<noteq> \<bottom> \<Longrightarrow>
- map_forest\<cdot>f\<cdot>(Trees\<cdot>t\<cdot>ts) = Trees\<cdot>(map_tree\<cdot>f\<cdot>t)\<cdot>(map_forest\<cdot>f\<cdot>ts)"
-
-lemma map_tree_strict [simp]: "map_tree\<cdot>f\<cdot>\<bottom> = \<bottom>"
-by fixrec_simp
-
-lemma map_forest_strict [simp]: "map_forest\<cdot>f\<cdot>\<bottom> = \<bottom>"
-by fixrec_simp
-
-text {*
- Theorems generated:
- @{text map_tree_def} @{thm map_tree_def}
- @{text map_forest_def} @{thm map_forest_def}
- @{text map_tree.unfold} @{thm map_tree.unfold}
- @{text map_forest.unfold} @{thm map_forest.unfold}
- @{text map_tree.simps} @{thm map_tree.simps}
- @{text map_forest.simps} @{thm map_forest.simps}
- @{text map_tree_map_forest.induct} @{thm map_tree_map_forest.induct}
-*}
-
-
-subsection {* Using @{text fixrec} inside locales *}
-
-locale test =
- fixes foo :: "'a \<rightarrow> 'a"
- assumes foo_strict: "foo\<cdot>\<bottom> = \<bottom>"
-begin
-
-fixrec
- bar :: "'a u \<rightarrow> 'a"
-where
- "bar\<cdot>(up\<cdot>x) = foo\<cdot>x"
-
-lemma bar_strict: "bar\<cdot>\<bottom> = \<bottom>"
-by fixrec_simp
-
-end
-
-end
--- a/src/HOLCF/ex/New_Domain.thy Thu May 20 07:34:45 2010 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,92 +0,0 @@
-(* Title: HOLCF/ex/New_Domain.thy
- Author: Brian Huffman
-*)
-
-header {* Definitional domain package *}
-
-theory New_Domain
-imports HOLCF
-begin
-
-text {*
- The definitional domain package only works with representable domains,
- i.e. types in class @{text rep}.
-*}
-
-default_sort rep
-
-text {*
- Provided that @{text rep} is the default sort, the @{text new_domain}
- package should work with any type definition supported by the old
- domain package.
-*}
-
-new_domain 'a llist = LNil | LCons (lazy 'a) (lazy "'a llist")
-
-text {*
- The difference is that the new domain package is completely
- definitional, and does not generate any axioms. The following type
- and constant definitions are not produced by the old domain package.
-*}
-
-thm type_definition_llist
-thm llist_abs_def llist_rep_def
-
-text {*
- The new domain package also adds support for indirect recursion with
- user-defined datatypes. This definition of a tree datatype uses
- indirect recursion through the lazy list type constructor.
-*}
-
-new_domain 'a ltree = Leaf (lazy 'a) | Branch (lazy "'a ltree llist")
-
-text {*
- For indirect-recursive definitions, the domain package is not able to
- generate a high-level induction rule. (It produces a warning
- message instead.) The low-level reach lemma (now proved as a
- theorem, no longer generated as an axiom) can be used to derive
- other induction rules.
-*}
-
-thm ltree.reach
-
-text {*
- The definition of the take function uses map functions associated with
- each type constructor involved in the definition. A map function
- for the lazy list type has been generated by the new domain package.
-*}
-
-thm ltree.take_rews
-thm llist_map_def
-
-lemma ltree_induct:
- fixes P :: "'a ltree \<Rightarrow> bool"
- assumes adm: "adm P"
- assumes bot: "P \<bottom>"
- assumes Leaf: "\<And>x. P (Leaf\<cdot>x)"
- assumes Branch: "\<And>f l. \<forall>x. P (f\<cdot>x) \<Longrightarrow> P (Branch\<cdot>(llist_map\<cdot>f\<cdot>l))"
- shows "P x"
-proof -
- have "P (\<Squnion>i. ltree_take i\<cdot>x)"
- using adm
- proof (rule admD)
- fix i
- show "P (ltree_take i\<cdot>x)"
- proof (induct i arbitrary: x)
- case (0 x)
- show "P (ltree_take 0\<cdot>x)" by (simp add: bot)
- next
- case (Suc n x)
- show "P (ltree_take (Suc n)\<cdot>x)"
- apply (cases x)
- apply (simp add: bot)
- apply (simp add: Leaf)
- apply (simp add: Branch Suc)
- done
- qed
- qed (simp add: ltree.chain_take)
- thus ?thesis
- by (simp add: ltree.reach)
-qed
-
-end
--- a/src/HOLCF/ex/ROOT.ML Thu May 20 07:34:45 2010 +0200
+++ b/src/HOLCF/ex/ROOT.ML Thu May 20 07:36:50 2010 +0200
@@ -4,7 +4,6 @@
*)
use_thys ["Dnat", "Stream", "Dagstuhl", "Focus_ex", "Fix2", "Hoare",
- "Loop", "Fixrec_ex", "Powerdomain_ex", "Domain_ex", "Domain_Proofs",
+ "Loop", "Powerdomain_ex", "Domain_Proofs",
"Letrec",
- "Strict_Fun",
- "New_Domain"];
+ "Strict_Fun"];