1.1 --- a/src/HOLCF/IsaMakefile Wed May 19 16:28:24 2010 -0700
1.2 +++ b/src/HOLCF/IsaMakefile Wed May 19 17:01:07 2010 -0700
1.3 @@ -7,6 +7,7 @@
1.4 default: HOLCF
1.5 images: HOLCF IOA
1.6 test: HOLCF-IMP HOLCF-ex HOLCF-FOCUS \
1.7 + HOLCF-Tutorial \
1.8 IOA-ABP IOA-NTP IOA-Modelcheck IOA-Storage IOA-ex
1.9 all: images test
1.10
1.11 @@ -78,6 +79,19 @@
1.12 @$(ISABELLE_TOOL) usedir -b -g true -r $(OUT)/HOL HOLCF
1.13
1.14
1.15 +## HOLCF-Tutorial
1.16 +
1.17 +HOLCF-Tutorial: HOLCF $(LOG)/HOLCF-Tutorial.gz
1.18 +
1.19 +$(LOG)/HOLCF-Tutorial.gz: $(OUT)/HOLCF \
1.20 + Tutorial/Domain_ex.thy \
1.21 + Tutorial/Fixrec_ex.thy \
1.22 + Tutorial/New_Domain.thy \
1.23 + Tutorial/document/root.tex \
1.24 + Tutorial/ROOT.ML
1.25 + @$(ISABELLE_TOOL) usedir $(OUT)/HOLCF Tutorial
1.26 +
1.27 +
1.28 ## HOLCF-IMP
1.29
1.30 HOLCF-IMP: HOLCF $(LOG)/HOLCF-IMP.gz
1.31 @@ -95,15 +109,12 @@
1.32 ../HOL/Library/Nat_Infinity.thy \
1.33 ex/Dagstuhl.thy \
1.34 ex/Dnat.thy \
1.35 - ex/Domain_ex.thy \
1.36 ex/Domain_Proofs.thy \
1.37 ex/Fix2.thy \
1.38 - ex/Fixrec_ex.thy \
1.39 ex/Focus_ex.thy \
1.40 ex/Hoare.thy \
1.41 ex/Letrec.thy \
1.42 ex/Loop.thy \
1.43 - ex/New_Domain.thy \
1.44 ex/Powerdomain_ex.thy \
1.45 ex/Stream.thy \
1.46 ex/Strict_Fun.thy \
1.47 @@ -201,4 +212,4 @@
1.48 $(LOG)/HOLCF-ex.gz $(LOG)/HOLCF-FOCUS.gz $(OUT)/IOA \
1.49 $(LOG)/IOA.gz $(LOG)/IOA-ABP.gz $(LOG)/IOA-NTP.gz \
1.50 $(LOG)/IOA-Modelcheck.gz $(LOG)/IOA-Storage.gz \
1.51 - $(LOG)/IOA-ex.gz
1.52 + $(LOG)/IOA-ex.gz $(LOG)/HOLCF-Tutorial.gz
2.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
2.2 +++ b/src/HOLCF/Tutorial/Domain_ex.thy Wed May 19 17:01:07 2010 -0700
2.3 @@ -0,0 +1,211 @@
2.4 +(* Title: HOLCF/ex/Domain_ex.thy
2.5 + Author: Brian Huffman
2.6 +*)
2.7 +
2.8 +header {* Domain package examples *}
2.9 +
2.10 +theory Domain_ex
2.11 +imports HOLCF
2.12 +begin
2.13 +
2.14 +text {* Domain constructors are strict by default. *}
2.15 +
2.16 +domain d1 = d1a | d1b "d1" "d1"
2.17 +
2.18 +lemma "d1b\<cdot>\<bottom>\<cdot>y = \<bottom>" by simp
2.19 +
2.20 +text {* Constructors can be made lazy using the @{text "lazy"} keyword. *}
2.21 +
2.22 +domain d2 = d2a | d2b (lazy "d2")
2.23 +
2.24 +lemma "d2b\<cdot>x \<noteq> \<bottom>" by simp
2.25 +
2.26 +text {* Strict and lazy arguments may be mixed arbitrarily. *}
2.27 +
2.28 +domain d3 = d3a | d3b (lazy "d2") "d2"
2.29 +
2.30 +lemma "P (d3b\<cdot>x\<cdot>y = \<bottom>) \<longleftrightarrow> P (y = \<bottom>)" by simp
2.31 +
2.32 +text {* Selectors can be used with strict or lazy constructor arguments. *}
2.33 +
2.34 +domain d4 = d4a | d4b (lazy d4b_left :: "d2") (d4b_right :: "d2")
2.35 +
2.36 +lemma "y \<noteq> \<bottom> \<Longrightarrow> d4b_left\<cdot>(d4b\<cdot>x\<cdot>y) = x" by simp
2.37 +
2.38 +text {* Mixfix declarations can be given for data constructors. *}
2.39 +
2.40 +domain d5 = d5a | d5b (lazy "d5") "d5" (infixl ":#:" 70)
2.41 +
2.42 +lemma "d5a \<noteq> x :#: y :#: z" by simp
2.43 +
2.44 +text {* Mixfix declarations can also be given for type constructors. *}
2.45 +
2.46 +domain ('a, 'b) lazypair (infixl ":*:" 25) =
2.47 + lpair (lazy lfst :: 'a) (lazy lsnd :: 'b) (infixl ":*:" 75)
2.48 +
2.49 +lemma "\<forall>p::('a :*: 'b). p \<sqsubseteq> lfst\<cdot>p :*: lsnd\<cdot>p"
2.50 +by (rule allI, case_tac p, simp_all)
2.51 +
2.52 +text {* Non-recursive constructor arguments can have arbitrary types. *}
2.53 +
2.54 +domain ('a, 'b) d6 = d6 "int lift" "'a \<oplus> 'b u" (lazy "('a :*: 'b) \<times> ('b \<rightarrow> 'a)")
2.55 +
2.56 +text {*
2.57 + Indirect recusion is allowed for sums, products, lifting, and the
2.58 + continuous function space. However, the domain package does not
2.59 + generate an induction rule in terms of the constructors.
2.60 +*}
2.61 +
2.62 +domain 'a d7 = d7a "'a d7 \<oplus> int lift" | d7b "'a \<otimes> 'a d7" | d7c (lazy "'a d7 \<rightarrow> 'a")
2.63 + -- "Indirect recursion detected, skipping proofs of (co)induction rules"
2.64 +
2.65 +text {* Note that @{text d7.induct} is absent. *}
2.66 +
2.67 +text {*
2.68 + Indirect recursion is also allowed using previously-defined datatypes.
2.69 +*}
2.70 +
2.71 +domain 'a slist = SNil | SCons 'a "'a slist"
2.72 +
2.73 +domain 'a stree = STip | SBranch "'a stree slist"
2.74 +
2.75 +text {* Mutually-recursive datatypes can be defined using the @{text "and"} keyword. *}
2.76 +
2.77 +domain d8 = d8a | d8b "d9" and d9 = d9a | d9b (lazy "d8")
2.78 +
2.79 +text {* Non-regular recursion is not allowed. *}
2.80 +(*
2.81 +domain ('a, 'b) altlist = ANil | ACons 'a "('b, 'a) altlist"
2.82 + -- "illegal direct recursion with different arguments"
2.83 +domain 'a nest = Nest1 'a | Nest2 "'a nest nest"
2.84 + -- "illegal direct recursion with different arguments"
2.85 +*)
2.86 +
2.87 +text {*
2.88 + Mutually-recursive datatypes must have all the same type arguments,
2.89 + not necessarily in the same order.
2.90 +*}
2.91 +
2.92 +domain ('a, 'b) list1 = Nil1 | Cons1 'a "('b, 'a) list2"
2.93 + and ('b, 'a) list2 = Nil2 | Cons2 'b "('a, 'b) list1"
2.94 +
2.95 +text {* Induction rules for flat datatypes have no admissibility side-condition. *}
2.96 +
2.97 +domain 'a flattree = Tip | Branch "'a flattree" "'a flattree"
2.98 +
2.99 +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"
2.100 +by (rule flattree.induct) -- "no admissibility requirement"
2.101 +
2.102 +text {* Trivial datatypes will produce a warning message. *}
2.103 +
2.104 +domain triv = Triv triv triv
2.105 + -- "domain @{text Domain_ex.triv} is empty!"
2.106 +
2.107 +lemma "(x::triv) = \<bottom>" by (induct x, simp_all)
2.108 +
2.109 +text {* Lazy constructor arguments may have unpointed types. *}
2.110 +
2.111 +domain natlist = nnil | ncons (lazy "nat discr") natlist
2.112 +
2.113 +text {* Class constraints may be given for type parameters on the LHS. *}
2.114 +
2.115 +domain ('a::cpo) box = Box (lazy 'a)
2.116 +
2.117 +
2.118 +subsection {* Generated constants and theorems *}
2.119 +
2.120 +domain 'a tree = Leaf (lazy 'a) | Node (left :: "'a tree") (right :: "'a tree")
2.121 +
2.122 +lemmas tree_abs_defined_iff =
2.123 + iso.abs_defined_iff [OF iso.intro [OF tree.abs_iso tree.rep_iso]]
2.124 +
2.125 +text {* Rules about ismorphism *}
2.126 +term tree_rep
2.127 +term tree_abs
2.128 +thm tree.rep_iso
2.129 +thm tree.abs_iso
2.130 +thm tree.iso_rews
2.131 +
2.132 +text {* Rules about constructors *}
2.133 +term Leaf
2.134 +term Node
2.135 +thm Leaf_def Node_def
2.136 +thm tree.nchotomy
2.137 +thm tree.exhaust
2.138 +thm tree.compacts
2.139 +thm tree.con_rews
2.140 +thm tree.dist_les
2.141 +thm tree.dist_eqs
2.142 +thm tree.inverts
2.143 +thm tree.injects
2.144 +
2.145 +text {* Rules about case combinator *}
2.146 +term tree_when
2.147 +thm tree.tree_when_def
2.148 +thm tree.when_rews
2.149 +
2.150 +text {* Rules about selectors *}
2.151 +term left
2.152 +term right
2.153 +thm tree.sel_rews
2.154 +
2.155 +text {* Rules about discriminators *}
2.156 +term is_Leaf
2.157 +term is_Node
2.158 +thm tree.dis_rews
2.159 +
2.160 +text {* Rules about pattern match combinators *}
2.161 +term Leaf_pat
2.162 +term Node_pat
2.163 +thm tree.pat_rews
2.164 +
2.165 +text {* Rules about monadic pattern match combinators *}
2.166 +term match_Leaf
2.167 +term match_Node
2.168 +thm tree.match_rews
2.169 +
2.170 +text {* Rules about take function *}
2.171 +term tree_take
2.172 +thm tree.take_def
2.173 +thm tree.take_0
2.174 +thm tree.take_Suc
2.175 +thm tree.take_rews
2.176 +thm tree.chain_take
2.177 +thm tree.take_take
2.178 +thm tree.deflation_take
2.179 +thm tree.take_below
2.180 +thm tree.take_lemma
2.181 +thm tree.lub_take
2.182 +thm tree.reach
2.183 +thm tree.finite_induct
2.184 +
2.185 +text {* Rules about finiteness predicate *}
2.186 +term tree_finite
2.187 +thm tree.finite_def
2.188 +thm tree.finite (* only generated for flat datatypes *)
2.189 +
2.190 +text {* Rules about bisimulation predicate *}
2.191 +term tree_bisim
2.192 +thm tree.bisim_def
2.193 +thm tree.coinduct
2.194 +
2.195 +text {* Induction rule *}
2.196 +thm tree.induct
2.197 +
2.198 +
2.199 +subsection {* Known bugs *}
2.200 +
2.201 +text {* Declaring a mixfix with spaces causes some strange parse errors. *}
2.202 +(*
2.203 +domain xx = xx ("x y")
2.204 + -- "Inner syntax error: unexpected end of input"
2.205 +*)
2.206 +
2.207 +text {*
2.208 + Non-cpo type parameters currently do not work.
2.209 +*}
2.210 +(*
2.211 +domain ('a::type) stream = snil | scons (lazy "'a discr") "'a stream"
2.212 +*)
2.213 +
2.214 +end
3.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
3.2 +++ b/src/HOLCF/Tutorial/Fixrec_ex.thy Wed May 19 17:01:07 2010 -0700
3.3 @@ -0,0 +1,246 @@
3.4 +(* Title: HOLCF/ex/Fixrec_ex.thy
3.5 + Author: Brian Huffman
3.6 +*)
3.7 +
3.8 +header {* Fixrec package examples *}
3.9 +
3.10 +theory Fixrec_ex
3.11 +imports HOLCF
3.12 +begin
3.13 +
3.14 +subsection {* Basic @{text fixrec} examples *}
3.15 +
3.16 +text {*
3.17 + Fixrec patterns can mention any constructor defined by the domain
3.18 + package, as well as any of the following built-in constructors:
3.19 + Pair, spair, sinl, sinr, up, ONE, TT, FF.
3.20 +*}
3.21 +
3.22 +text {* Typical usage is with lazy constructors. *}
3.23 +
3.24 +fixrec down :: "'a u \<rightarrow> 'a"
3.25 +where "down\<cdot>(up\<cdot>x) = x"
3.26 +
3.27 +text {* With strict constructors, rewrite rules may require side conditions. *}
3.28 +
3.29 +fixrec from_sinl :: "'a \<oplus> 'b \<rightarrow> 'a"
3.30 +where "x \<noteq> \<bottom> \<Longrightarrow> from_sinl\<cdot>(sinl\<cdot>x) = x"
3.31 +
3.32 +text {* Lifting can turn a strict constructor into a lazy one. *}
3.33 +
3.34 +fixrec from_sinl_up :: "'a u \<oplus> 'b \<rightarrow> 'a"
3.35 +where "from_sinl_up\<cdot>(sinl\<cdot>(up\<cdot>x)) = x"
3.36 +
3.37 +text {* Fixrec also works with the HOL pair constructor. *}
3.38 +
3.39 +fixrec down2 :: "'a u \<times> 'b u \<rightarrow> 'a \<times> 'b"
3.40 +where "down2\<cdot>(up\<cdot>x, up\<cdot>y) = (x, y)"
3.41 +
3.42 +
3.43 +subsection {* Examples using @{text fixrec_simp} *}
3.44 +
3.45 +text {* A type of lazy lists. *}
3.46 +
3.47 +domain 'a llist = lNil | lCons (lazy 'a) (lazy "'a llist")
3.48 +
3.49 +text {* A zip function for lazy lists. *}
3.50 +
3.51 +text {* Notice that the patterns are not exhaustive. *}
3.52 +
3.53 +fixrec
3.54 + lzip :: "'a llist \<rightarrow> 'b llist \<rightarrow> ('a \<times> 'b) llist"
3.55 +where
3.56 + "lzip\<cdot>(lCons\<cdot>x\<cdot>xs)\<cdot>(lCons\<cdot>y\<cdot>ys) = lCons\<cdot>(x, y)\<cdot>(lzip\<cdot>xs\<cdot>ys)"
3.57 +| "lzip\<cdot>lNil\<cdot>lNil = lNil"
3.58 +
3.59 +text {* @{text fixrec_simp} is useful for producing strictness theorems. *}
3.60 +text {* Note that pattern matching is done in left-to-right order. *}
3.61 +
3.62 +lemma lzip_stricts [simp]:
3.63 + "lzip\<cdot>\<bottom>\<cdot>ys = \<bottom>"
3.64 + "lzip\<cdot>lNil\<cdot>\<bottom> = \<bottom>"
3.65 + "lzip\<cdot>(lCons\<cdot>x\<cdot>xs)\<cdot>\<bottom> = \<bottom>"
3.66 +by fixrec_simp+
3.67 +
3.68 +text {* @{text fixrec_simp} can also produce rules for missing cases. *}
3.69 +
3.70 +lemma lzip_undefs [simp]:
3.71 + "lzip\<cdot>lNil\<cdot>(lCons\<cdot>y\<cdot>ys) = \<bottom>"
3.72 + "lzip\<cdot>(lCons\<cdot>x\<cdot>xs)\<cdot>lNil = \<bottom>"
3.73 +by fixrec_simp+
3.74 +
3.75 +
3.76 +subsection {* Pattern matching with bottoms *}
3.77 +
3.78 +text {*
3.79 + As an alternative to using @{text fixrec_simp}, it is also possible
3.80 + to use bottom as a constructor pattern. When using a bottom
3.81 + pattern, the right-hand-side must also be bottom; otherwise, @{text
3.82 + fixrec} will not be able to prove the equation.
3.83 +*}
3.84 +
3.85 +fixrec
3.86 + from_sinr_up :: "'a \<oplus> 'b\<^sub>\<bottom> \<rightarrow> 'b"
3.87 +where
3.88 + "from_sinr_up\<cdot>\<bottom> = \<bottom>"
3.89 +| "from_sinr_up\<cdot>(sinr\<cdot>(up\<cdot>x)) = x"
3.90 +
3.91 +text {*
3.92 + If the function is already strict in that argument, then the bottom
3.93 + pattern does not change the meaning of the function. For example,
3.94 + in the definition of @{term from_sinr_up}, the first equation is
3.95 + actually redundant, and could have been proven separately by
3.96 + @{text fixrec_simp}.
3.97 +*}
3.98 +
3.99 +text {*
3.100 + A bottom pattern can also be used to make a function strict in a
3.101 + certain argument, similar to a bang-pattern in Haskell.
3.102 +*}
3.103 +
3.104 +fixrec
3.105 + seq :: "'a \<rightarrow> 'b \<rightarrow> 'b"
3.106 +where
3.107 + "seq\<cdot>\<bottom>\<cdot>y = \<bottom>"
3.108 +| "x \<noteq> \<bottom> \<Longrightarrow> seq\<cdot>x\<cdot>y = y"
3.109 +
3.110 +
3.111 +subsection {* Skipping proofs of rewrite rules *}
3.112 +
3.113 +text {* Another zip function for lazy lists. *}
3.114 +
3.115 +text {*
3.116 + Notice that this version has overlapping patterns.
3.117 + The second equation cannot be proved as a theorem
3.118 + because it only applies when the first pattern fails.
3.119 +*}
3.120 +
3.121 +fixrec (permissive)
3.122 + lzip2 :: "'a llist \<rightarrow> 'b llist \<rightarrow> ('a \<times> 'b) llist"
3.123 +where
3.124 + "lzip2\<cdot>(lCons\<cdot>x\<cdot>xs)\<cdot>(lCons\<cdot>y\<cdot>ys) = lCons\<cdot>(x, y)\<cdot>(lzip\<cdot>xs\<cdot>ys)"
3.125 +| "lzip2\<cdot>xs\<cdot>ys = lNil"
3.126 +
3.127 +text {*
3.128 + Usually fixrec tries to prove all equations as theorems.
3.129 + The "permissive" option overrides this behavior, so fixrec
3.130 + does not produce any simp rules.
3.131 +*}
3.132 +
3.133 +text {* Simp rules can be generated later using @{text fixrec_simp}. *}
3.134 +
3.135 +lemma lzip2_simps [simp]:
3.136 + "lzip2\<cdot>(lCons\<cdot>x\<cdot>xs)\<cdot>(lCons\<cdot>y\<cdot>ys) = lCons\<cdot>(x, y)\<cdot>(lzip\<cdot>xs\<cdot>ys)"
3.137 + "lzip2\<cdot>(lCons\<cdot>x\<cdot>xs)\<cdot>lNil = lNil"
3.138 + "lzip2\<cdot>lNil\<cdot>(lCons\<cdot>y\<cdot>ys) = lNil"
3.139 + "lzip2\<cdot>lNil\<cdot>lNil = lNil"
3.140 +by fixrec_simp+
3.141 +
3.142 +lemma lzip2_stricts [simp]:
3.143 + "lzip2\<cdot>\<bottom>\<cdot>ys = \<bottom>"
3.144 + "lzip2\<cdot>(lCons\<cdot>x\<cdot>xs)\<cdot>\<bottom> = \<bottom>"
3.145 +by fixrec_simp+
3.146 +
3.147 +
3.148 +subsection {* Mutual recursion with @{text fixrec} *}
3.149 +
3.150 +text {* Tree and forest types. *}
3.151 +
3.152 +domain 'a tree = Leaf (lazy 'a) | Branch (lazy "'a forest")
3.153 +and 'a forest = Empty | Trees (lazy "'a tree") "'a forest"
3.154 +
3.155 +text {*
3.156 + To define mutually recursive functions, give multiple type signatures
3.157 + separated by the keyword @{text "and"}.
3.158 +*}
3.159 +
3.160 +fixrec
3.161 + map_tree :: "('a \<rightarrow> 'b) \<rightarrow> ('a tree \<rightarrow> 'b tree)"
3.162 +and
3.163 + map_forest :: "('a \<rightarrow> 'b) \<rightarrow> ('a forest \<rightarrow> 'b forest)"
3.164 +where
3.165 + "map_tree\<cdot>f\<cdot>(Leaf\<cdot>x) = Leaf\<cdot>(f\<cdot>x)"
3.166 +| "map_tree\<cdot>f\<cdot>(Branch\<cdot>ts) = Branch\<cdot>(map_forest\<cdot>f\<cdot>ts)"
3.167 +| "map_forest\<cdot>f\<cdot>Empty = Empty"
3.168 +| "ts \<noteq> \<bottom> \<Longrightarrow>
3.169 + 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)"
3.170 +
3.171 +lemma map_tree_strict [simp]: "map_tree\<cdot>f\<cdot>\<bottom> = \<bottom>"
3.172 +by fixrec_simp
3.173 +
3.174 +lemma map_forest_strict [simp]: "map_forest\<cdot>f\<cdot>\<bottom> = \<bottom>"
3.175 +by fixrec_simp
3.176 +
3.177 +(*
3.178 + Theorems generated:
3.179 + @{text map_tree_def} @{thm map_tree_def}
3.180 + @{text map_forest_def} @{thm map_forest_def}
3.181 + @{text map_tree.unfold} @{thm map_tree.unfold}
3.182 + @{text map_forest.unfold} @{thm map_forest.unfold}
3.183 + @{text map_tree.simps} @{thm map_tree.simps}
3.184 + @{text map_forest.simps} @{thm map_forest.simps}
3.185 + @{text map_tree_map_forest.induct} @{thm map_tree_map_forest.induct}
3.186 +*)
3.187 +
3.188 +
3.189 +subsection {* Looping simp rules *}
3.190 +
3.191 +text {*
3.192 + The defining equations of a fixrec definition are declared as simp
3.193 + rules by default. In some cases, especially for constants with no
3.194 + arguments or functions with variable patterns, the defining
3.195 + equations may cause the simplifier to loop. In these cases it will
3.196 + be necessary to use a @{text "[simp del]"} declaration.
3.197 +*}
3.198 +
3.199 +fixrec
3.200 + repeat :: "'a \<rightarrow> 'a llist"
3.201 +where
3.202 + [simp del]: "repeat\<cdot>x = lCons\<cdot>x\<cdot>(repeat\<cdot>x)"
3.203 +
3.204 +text {*
3.205 + We can derive other non-looping simp rules for @{const repeat} by
3.206 + using the @{text subst} method with the @{text repeat.simps} rule.
3.207 +*}
3.208 +
3.209 +lemma repeat_simps [simp]:
3.210 + "repeat\<cdot>x \<noteq> \<bottom>"
3.211 + "repeat\<cdot>x \<noteq> lNil"
3.212 + "repeat\<cdot>x = lCons\<cdot>y\<cdot>ys \<longleftrightarrow> x = y \<and> repeat\<cdot>x = ys"
3.213 +by (subst repeat.simps, simp)+
3.214 +
3.215 +lemma llist_when_repeat [simp]:
3.216 + "llist_when\<cdot>z\<cdot>f\<cdot>(repeat\<cdot>x) = f\<cdot>x\<cdot>(repeat\<cdot>x)"
3.217 +by (subst repeat.simps, simp)
3.218 +
3.219 +text {*
3.220 + For mutually-recursive constants, looping might only occur if all
3.221 + equations are in the simpset at the same time. In such cases it may
3.222 + only be necessary to declare @{text "[simp del]"} on one equation.
3.223 +*}
3.224 +
3.225 +fixrec
3.226 + inf_tree :: "'a tree" and inf_forest :: "'a forest"
3.227 +where
3.228 + [simp del]: "inf_tree = Branch\<cdot>inf_forest"
3.229 +| "inf_forest = Trees\<cdot>inf_tree\<cdot>(Trees\<cdot>inf_tree\<cdot>Empty)"
3.230 +
3.231 +
3.232 +subsection {* Using @{text fixrec} inside locales *}
3.233 +
3.234 +locale test =
3.235 + fixes foo :: "'a \<rightarrow> 'a"
3.236 + assumes foo_strict: "foo\<cdot>\<bottom> = \<bottom>"
3.237 +begin
3.238 +
3.239 +fixrec
3.240 + bar :: "'a u \<rightarrow> 'a"
3.241 +where
3.242 + "bar\<cdot>(up\<cdot>x) = foo\<cdot>x"
3.243 +
3.244 +lemma bar_strict: "bar\<cdot>\<bottom> = \<bottom>"
3.245 +by fixrec_simp
3.246 +
3.247 +end
3.248 +
3.249 +end
4.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
4.2 +++ b/src/HOLCF/Tutorial/New_Domain.thy Wed May 19 17:01:07 2010 -0700
4.3 @@ -0,0 +1,92 @@
4.4 +(* Title: HOLCF/ex/New_Domain.thy
4.5 + Author: Brian Huffman
4.6 +*)
4.7 +
4.8 +header {* Definitional domain package *}
4.9 +
4.10 +theory New_Domain
4.11 +imports HOLCF
4.12 +begin
4.13 +
4.14 +text {*
4.15 + The definitional domain package only works with representable domains,
4.16 + i.e. types in class @{text rep}.
4.17 +*}
4.18 +
4.19 +default_sort rep
4.20 +
4.21 +text {*
4.22 + Provided that @{text rep} is the default sort, the @{text new_domain}
4.23 + package should work with any type definition supported by the old
4.24 + domain package.
4.25 +*}
4.26 +
4.27 +new_domain 'a llist = LNil | LCons (lazy 'a) (lazy "'a llist")
4.28 +
4.29 +text {*
4.30 + The difference is that the new domain package is completely
4.31 + definitional, and does not generate any axioms. The following type
4.32 + and constant definitions are not produced by the old domain package.
4.33 +*}
4.34 +
4.35 +thm type_definition_llist
4.36 +thm llist_abs_def llist_rep_def
4.37 +
4.38 +text {*
4.39 + The new domain package also adds support for indirect recursion with
4.40 + user-defined datatypes. This definition of a tree datatype uses
4.41 + indirect recursion through the lazy list type constructor.
4.42 +*}
4.43 +
4.44 +new_domain 'a ltree = Leaf (lazy 'a) | Branch (lazy "'a ltree llist")
4.45 +
4.46 +text {*
4.47 + For indirect-recursive definitions, the domain package is not able to
4.48 + generate a high-level induction rule. (It produces a warning
4.49 + message instead.) The low-level reach lemma (now proved as a
4.50 + theorem, no longer generated as an axiom) can be used to derive
4.51 + other induction rules.
4.52 +*}
4.53 +
4.54 +thm ltree.reach
4.55 +
4.56 +text {*
4.57 + The definition of the take function uses map functions associated with
4.58 + each type constructor involved in the definition. A map function
4.59 + for the lazy list type has been generated by the new domain package.
4.60 +*}
4.61 +
4.62 +thm ltree.take_rews
4.63 +thm llist_map_def
4.64 +
4.65 +lemma ltree_induct:
4.66 + fixes P :: "'a ltree \<Rightarrow> bool"
4.67 + assumes adm: "adm P"
4.68 + assumes bot: "P \<bottom>"
4.69 + assumes Leaf: "\<And>x. P (Leaf\<cdot>x)"
4.70 + assumes Branch: "\<And>f l. \<forall>x. P (f\<cdot>x) \<Longrightarrow> P (Branch\<cdot>(llist_map\<cdot>f\<cdot>l))"
4.71 + shows "P x"
4.72 +proof -
4.73 + have "P (\<Squnion>i. ltree_take i\<cdot>x)"
4.74 + using adm
4.75 + proof (rule admD)
4.76 + fix i
4.77 + show "P (ltree_take i\<cdot>x)"
4.78 + proof (induct i arbitrary: x)
4.79 + case (0 x)
4.80 + show "P (ltree_take 0\<cdot>x)" by (simp add: bot)
4.81 + next
4.82 + case (Suc n x)
4.83 + show "P (ltree_take (Suc n)\<cdot>x)"
4.84 + apply (cases x)
4.85 + apply (simp add: bot)
4.86 + apply (simp add: Leaf)
4.87 + apply (simp add: Branch Suc)
4.88 + done
4.89 + qed
4.90 + qed (simp add: ltree.chain_take)
4.91 + thus ?thesis
4.92 + by (simp add: ltree.reach)
4.93 +qed
4.94 +
4.95 +end
5.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
5.2 +++ b/src/HOLCF/Tutorial/ROOT.ML Wed May 19 17:01:07 2010 -0700
5.3 @@ -0,0 +1,1 @@
5.4 +use_thys ["Domain_ex", "Fixrec_ex", "New_Domain"];
6.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
6.2 +++ b/src/HOLCF/Tutorial/document/root.tex Wed May 19 17:01:07 2010 -0700
6.3 @@ -0,0 +1,29 @@
6.4 +
6.5 +% HOLCF/document/root.tex
6.6 +
6.7 +\documentclass[11pt,a4paper]{article}
6.8 +\usepackage{graphicx,isabelle,isabellesym,latexsym}
6.9 +\usepackage[only,bigsqcap]{stmaryrd}
6.10 +\usepackage[latin1]{inputenc}
6.11 +\usepackage{pdfsetup}
6.12 +
6.13 +\urlstyle{rm}
6.14 +%\isabellestyle{it}
6.15 +\pagestyle{myheadings}
6.16 +
6.17 +\begin{document}
6.18 +
6.19 +\title{Isabelle/HOLCF Tutorial}
6.20 +\maketitle
6.21 +
6.22 +\tableofcontents
6.23 +
6.24 +%\newpage
6.25 +
6.26 +%\renewcommand{\isamarkupheader}[1]%
6.27 +%{\section{\isabellecontext: #1}\markright{THEORY~``\isabellecontext''}}
6.28 +
6.29 +\parindent 0pt\parskip 0.5ex
6.30 +\input{session}
6.31 +
6.32 +\end{document}
7.1 --- a/src/HOLCF/ex/Domain_ex.thy Wed May 19 16:28:24 2010 -0700
7.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
7.3 @@ -1,210 +0,0 @@
7.4 -(* Title: HOLCF/ex/Domain_ex.thy
7.5 - Author: Brian Huffman
7.6 -*)
7.7 -
7.8 -header {* Domain package examples *}
7.9 -
7.10 -theory Domain_ex
7.11 -imports HOLCF
7.12 -begin
7.13 -
7.14 -text {* Domain constructors are strict by default. *}
7.15 -
7.16 -domain d1 = d1a | d1b "d1" "d1"
7.17 -
7.18 -lemma "d1b\<cdot>\<bottom>\<cdot>y = \<bottom>" by simp
7.19 -
7.20 -text {* Constructors can be made lazy using the @{text "lazy"} keyword. *}
7.21 -
7.22 -domain d2 = d2a | d2b (lazy "d2")
7.23 -
7.24 -lemma "d2b\<cdot>x \<noteq> \<bottom>" by simp
7.25 -
7.26 -text {* Strict and lazy arguments may be mixed arbitrarily. *}
7.27 -
7.28 -domain d3 = d3a | d3b (lazy "d2") "d2"
7.29 -
7.30 -lemma "P (d3b\<cdot>x\<cdot>y = \<bottom>) \<longleftrightarrow> P (y = \<bottom>)" by simp
7.31 -
7.32 -text {* Selectors can be used with strict or lazy constructor arguments. *}
7.33 -
7.34 -domain d4 = d4a | d4b (lazy d4b_left :: "d2") (d4b_right :: "d2")
7.35 -
7.36 -lemma "y \<noteq> \<bottom> \<Longrightarrow> d4b_left\<cdot>(d4b\<cdot>x\<cdot>y) = x" by simp
7.37 -
7.38 -text {* Mixfix declarations can be given for data constructors. *}
7.39 -
7.40 -domain d5 = d5a | d5b (lazy "d5") "d5" (infixl ":#:" 70)
7.41 -
7.42 -lemma "d5a \<noteq> x :#: y :#: z" by simp
7.43 -
7.44 -text {* Mixfix declarations can also be given for type constructors. *}
7.45 -
7.46 -domain ('a, 'b) lazypair (infixl ":*:" 25) =
7.47 - lpair (lazy lfst :: 'a) (lazy lsnd :: 'b) (infixl ":*:" 75)
7.48 -
7.49 -lemma "\<forall>p::('a :*: 'b). p \<sqsubseteq> lfst\<cdot>p :*: lsnd\<cdot>p"
7.50 -by (rule allI, case_tac p, simp_all)
7.51 -
7.52 -text {* Non-recursive constructor arguments can have arbitrary types. *}
7.53 -
7.54 -domain ('a, 'b) d6 = d6 "int lift" "'a \<oplus> 'b u" (lazy "('a :*: 'b) \<times> ('b \<rightarrow> 'a)")
7.55 -
7.56 -text {*
7.57 - Indirect recusion is allowed for sums, products, lifting, and the
7.58 - continuous function space. However, the domain package does not
7.59 - generate an induction rule in terms of the constructors.
7.60 -*}
7.61 -
7.62 -domain 'a d7 = d7a "'a d7 \<oplus> int lift" | d7b "'a \<otimes> 'a d7" | d7c (lazy "'a d7 \<rightarrow> 'a")
7.63 - -- "Indirect recursion detected, skipping proofs of (co)induction rules"
7.64 -(* d7.induct is absent *)
7.65 -
7.66 -text {*
7.67 - Indirect recursion is also allowed using previously-defined datatypes.
7.68 -*}
7.69 -
7.70 -domain 'a slist = SNil | SCons 'a "'a slist"
7.71 -
7.72 -domain 'a stree = STip | SBranch "'a stree slist"
7.73 -
7.74 -text {* Mutually-recursive datatypes can be defined using the @{text "and"} keyword. *}
7.75 -
7.76 -domain d8 = d8a | d8b "d9" and d9 = d9a | d9b (lazy "d8")
7.77 -
7.78 -text {* Non-regular recursion is not allowed. *}
7.79 -(*
7.80 -domain ('a, 'b) altlist = ANil | ACons 'a "('b, 'a) altlist"
7.81 - -- "illegal direct recursion with different arguments"
7.82 -domain 'a nest = Nest1 'a | Nest2 "'a nest nest"
7.83 - -- "illegal direct recursion with different arguments"
7.84 -*)
7.85 -
7.86 -text {*
7.87 - Mutually-recursive datatypes must have all the same type arguments,
7.88 - not necessarily in the same order.
7.89 -*}
7.90 -
7.91 -domain ('a, 'b) list1 = Nil1 | Cons1 'a "('b, 'a) list2"
7.92 - and ('b, 'a) list2 = Nil2 | Cons2 'b "('a, 'b) list1"
7.93 -
7.94 -text {* Induction rules for flat datatypes have no admissibility side-condition. *}
7.95 -
7.96 -domain 'a flattree = Tip | Branch "'a flattree" "'a flattree"
7.97 -
7.98 -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"
7.99 -by (rule flattree.induct) -- "no admissibility requirement"
7.100 -
7.101 -text {* Trivial datatypes will produce a warning message. *}
7.102 -
7.103 -domain triv = Triv triv triv
7.104 - -- "domain Domain_ex.triv is empty!"
7.105 -
7.106 -lemma "(x::triv) = \<bottom>" by (induct x, simp_all)
7.107 -
7.108 -text {* Lazy constructor arguments may have unpointed types. *}
7.109 -
7.110 -domain natlist = nnil | ncons (lazy "nat discr") natlist
7.111 -
7.112 -text {* Class constraints may be given for type parameters on the LHS. *}
7.113 -
7.114 -domain ('a::cpo) box = Box (lazy 'a)
7.115 -
7.116 -
7.117 -subsection {* Generated constants and theorems *}
7.118 -
7.119 -domain 'a tree = Leaf (lazy 'a) | Node (left :: "'a tree") (right :: "'a tree")
7.120 -
7.121 -lemmas tree_abs_defined_iff =
7.122 - iso.abs_defined_iff [OF iso.intro [OF tree.abs_iso tree.rep_iso]]
7.123 -
7.124 -text {* Rules about ismorphism *}
7.125 -term tree_rep
7.126 -term tree_abs
7.127 -thm tree.rep_iso
7.128 -thm tree.abs_iso
7.129 -thm tree.iso_rews
7.130 -
7.131 -text {* Rules about constructors *}
7.132 -term Leaf
7.133 -term Node
7.134 -thm Leaf_def Node_def
7.135 -thm tree.nchotomy
7.136 -thm tree.exhaust
7.137 -thm tree.compacts
7.138 -thm tree.con_rews
7.139 -thm tree.dist_les
7.140 -thm tree.dist_eqs
7.141 -thm tree.inverts
7.142 -thm tree.injects
7.143 -
7.144 -text {* Rules about case combinator *}
7.145 -term tree_when
7.146 -thm tree.tree_when_def
7.147 -thm tree.when_rews
7.148 -
7.149 -text {* Rules about selectors *}
7.150 -term left
7.151 -term right
7.152 -thm tree.sel_rews
7.153 -
7.154 -text {* Rules about discriminators *}
7.155 -term is_Leaf
7.156 -term is_Node
7.157 -thm tree.dis_rews
7.158 -
7.159 -text {* Rules about pattern match combinators *}
7.160 -term Leaf_pat
7.161 -term Node_pat
7.162 -thm tree.pat_rews
7.163 -
7.164 -text {* Rules about monadic pattern match combinators *}
7.165 -term match_Leaf
7.166 -term match_Node
7.167 -thm tree.match_rews
7.168 -
7.169 -text {* Rules about take function *}
7.170 -term tree_take
7.171 -thm tree.take_def
7.172 -thm tree.take_0
7.173 -thm tree.take_Suc
7.174 -thm tree.take_rews
7.175 -thm tree.chain_take
7.176 -thm tree.take_take
7.177 -thm tree.deflation_take
7.178 -thm tree.take_below
7.179 -thm tree.take_lemma
7.180 -thm tree.lub_take
7.181 -thm tree.reach
7.182 -thm tree.finite_induct
7.183 -
7.184 -text {* Rules about finiteness predicate *}
7.185 -term tree_finite
7.186 -thm tree.finite_def
7.187 -thm tree.finite (* only generated for flat datatypes *)
7.188 -
7.189 -text {* Rules about bisimulation predicate *}
7.190 -term tree_bisim
7.191 -thm tree.bisim_def
7.192 -thm tree.coinduct
7.193 -
7.194 -text {* Induction rule *}
7.195 -thm tree.induct
7.196 -
7.197 -
7.198 -subsection {* Known bugs *}
7.199 -
7.200 -text {* Declaring a mixfix with spaces causes some strange parse errors. *}
7.201 -(*
7.202 -domain xx = xx ("x y")
7.203 - -- "Inner syntax error: unexpected end of input"
7.204 -*)
7.205 -
7.206 -text {*
7.207 - Non-cpo type parameters currently do not work.
7.208 -*}
7.209 -(*
7.210 -domain ('a::type) stream = snil | scons (lazy "'a discr") "'a stream"
7.211 -*)
7.212 -
7.213 -end
8.1 --- a/src/HOLCF/ex/Fixrec_ex.thy Wed May 19 16:28:24 2010 -0700
8.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
8.3 @@ -1,246 +0,0 @@
8.4 -(* Title: HOLCF/ex/Fixrec_ex.thy
8.5 - Author: Brian Huffman
8.6 -*)
8.7 -
8.8 -header {* Fixrec package examples *}
8.9 -
8.10 -theory Fixrec_ex
8.11 -imports HOLCF
8.12 -begin
8.13 -
8.14 -subsection {* Basic @{text fixrec} examples *}
8.15 -
8.16 -text {*
8.17 - Fixrec patterns can mention any constructor defined by the domain
8.18 - package, as well as any of the following built-in constructors:
8.19 - Pair, spair, sinl, sinr, up, ONE, TT, FF.
8.20 -*}
8.21 -
8.22 -text {* Typical usage is with lazy constructors. *}
8.23 -
8.24 -fixrec down :: "'a u \<rightarrow> 'a"
8.25 -where "down\<cdot>(up\<cdot>x) = x"
8.26 -
8.27 -text {* With strict constructors, rewrite rules may require side conditions. *}
8.28 -
8.29 -fixrec from_sinl :: "'a \<oplus> 'b \<rightarrow> 'a"
8.30 -where "x \<noteq> \<bottom> \<Longrightarrow> from_sinl\<cdot>(sinl\<cdot>x) = x"
8.31 -
8.32 -text {* Lifting can turn a strict constructor into a lazy one. *}
8.33 -
8.34 -fixrec from_sinl_up :: "'a u \<oplus> 'b \<rightarrow> 'a"
8.35 -where "from_sinl_up\<cdot>(sinl\<cdot>(up\<cdot>x)) = x"
8.36 -
8.37 -text {* Fixrec also works with the HOL pair constructor. *}
8.38 -
8.39 -fixrec down2 :: "'a u \<times> 'b u \<rightarrow> 'a \<times> 'b"
8.40 -where "down2\<cdot>(up\<cdot>x, up\<cdot>y) = (x, y)"
8.41 -
8.42 -
8.43 -subsection {* Examples using @{text fixrec_simp} *}
8.44 -
8.45 -text {* A type of lazy lists. *}
8.46 -
8.47 -domain 'a llist = lNil | lCons (lazy 'a) (lazy "'a llist")
8.48 -
8.49 -text {* A zip function for lazy lists. *}
8.50 -
8.51 -text {* Notice that the patterns are not exhaustive. *}
8.52 -
8.53 -fixrec
8.54 - lzip :: "'a llist \<rightarrow> 'b llist \<rightarrow> ('a \<times> 'b) llist"
8.55 -where
8.56 - "lzip\<cdot>(lCons\<cdot>x\<cdot>xs)\<cdot>(lCons\<cdot>y\<cdot>ys) = lCons\<cdot>(x, y)\<cdot>(lzip\<cdot>xs\<cdot>ys)"
8.57 -| "lzip\<cdot>lNil\<cdot>lNil = lNil"
8.58 -
8.59 -text {* @{text fixrec_simp} is useful for producing strictness theorems. *}
8.60 -text {* Note that pattern matching is done in left-to-right order. *}
8.61 -
8.62 -lemma lzip_stricts [simp]:
8.63 - "lzip\<cdot>\<bottom>\<cdot>ys = \<bottom>"
8.64 - "lzip\<cdot>lNil\<cdot>\<bottom> = \<bottom>"
8.65 - "lzip\<cdot>(lCons\<cdot>x\<cdot>xs)\<cdot>\<bottom> = \<bottom>"
8.66 -by fixrec_simp+
8.67 -
8.68 -text {* @{text fixrec_simp} can also produce rules for missing cases. *}
8.69 -
8.70 -lemma lzip_undefs [simp]:
8.71 - "lzip\<cdot>lNil\<cdot>(lCons\<cdot>y\<cdot>ys) = \<bottom>"
8.72 - "lzip\<cdot>(lCons\<cdot>x\<cdot>xs)\<cdot>lNil = \<bottom>"
8.73 -by fixrec_simp+
8.74 -
8.75 -
8.76 -subsection {* Pattern matching with bottoms *}
8.77 -
8.78 -text {*
8.79 - As an alternative to using @{text fixrec_simp}, it is also possible
8.80 - to use bottom as a constructor pattern. When using a bottom
8.81 - pattern, the right-hand-side must also be bottom; otherwise, @{text
8.82 - fixrec} will not be able to prove the equation.
8.83 -*}
8.84 -
8.85 -fixrec
8.86 - from_sinr_up :: "'a \<oplus> 'b\<^sub>\<bottom> \<rightarrow> 'b"
8.87 -where
8.88 - "from_sinr_up\<cdot>\<bottom> = \<bottom>"
8.89 -| "from_sinr_up\<cdot>(sinr\<cdot>(up\<cdot>x)) = x"
8.90 -
8.91 -text {*
8.92 - If the function is already strict in that argument, then the bottom
8.93 - pattern does not change the meaning of the function. For example,
8.94 - in the definition of @{term from_sinr_up}, the first equation is
8.95 - actually redundant, and could have been proven separately by
8.96 - @{text fixrec_simp}.
8.97 -*}
8.98 -
8.99 -text {*
8.100 - A bottom pattern can also be used to make a function strict in a
8.101 - certain argument, similar to a bang-pattern in Haskell.
8.102 -*}
8.103 -
8.104 -fixrec
8.105 - seq :: "'a \<rightarrow> 'b \<rightarrow> 'b"
8.106 -where
8.107 - "seq\<cdot>\<bottom>\<cdot>y = \<bottom>"
8.108 -| "x \<noteq> \<bottom> \<Longrightarrow> seq\<cdot>x\<cdot>y = y"
8.109 -
8.110 -
8.111 -subsection {* Skipping proofs of rewrite rules *}
8.112 -
8.113 -text {* Another zip function for lazy lists. *}
8.114 -
8.115 -text {*
8.116 - Notice that this version has overlapping patterns.
8.117 - The second equation cannot be proved as a theorem
8.118 - because it only applies when the first pattern fails.
8.119 -*}
8.120 -
8.121 -fixrec (permissive)
8.122 - lzip2 :: "'a llist \<rightarrow> 'b llist \<rightarrow> ('a \<times> 'b) llist"
8.123 -where
8.124 - "lzip2\<cdot>(lCons\<cdot>x\<cdot>xs)\<cdot>(lCons\<cdot>y\<cdot>ys) = lCons\<cdot>(x, y)\<cdot>(lzip\<cdot>xs\<cdot>ys)"
8.125 -| "lzip2\<cdot>xs\<cdot>ys = lNil"
8.126 -
8.127 -text {*
8.128 - Usually fixrec tries to prove all equations as theorems.
8.129 - The "permissive" option overrides this behavior, so fixrec
8.130 - does not produce any simp rules.
8.131 -*}
8.132 -
8.133 -text {* Simp rules can be generated later using @{text fixrec_simp}. *}
8.134 -
8.135 -lemma lzip2_simps [simp]:
8.136 - "lzip2\<cdot>(lCons\<cdot>x\<cdot>xs)\<cdot>(lCons\<cdot>y\<cdot>ys) = lCons\<cdot>(x, y)\<cdot>(lzip\<cdot>xs\<cdot>ys)"
8.137 - "lzip2\<cdot>(lCons\<cdot>x\<cdot>xs)\<cdot>lNil = lNil"
8.138 - "lzip2\<cdot>lNil\<cdot>(lCons\<cdot>y\<cdot>ys) = lNil"
8.139 - "lzip2\<cdot>lNil\<cdot>lNil = lNil"
8.140 -by fixrec_simp+
8.141 -
8.142 -lemma lzip2_stricts [simp]:
8.143 - "lzip2\<cdot>\<bottom>\<cdot>ys = \<bottom>"
8.144 - "lzip2\<cdot>(lCons\<cdot>x\<cdot>xs)\<cdot>\<bottom> = \<bottom>"
8.145 -by fixrec_simp+
8.146 -
8.147 -
8.148 -subsection {* Mutual recursion with @{text fixrec} *}
8.149 -
8.150 -text {* Tree and forest types. *}
8.151 -
8.152 -domain 'a tree = Leaf (lazy 'a) | Branch (lazy "'a forest")
8.153 -and 'a forest = Empty | Trees (lazy "'a tree") "'a forest"
8.154 -
8.155 -text {*
8.156 - To define mutually recursive functions, give multiple type signatures
8.157 - separated by the keyword @{text "and"}.
8.158 -*}
8.159 -
8.160 -fixrec
8.161 - map_tree :: "('a \<rightarrow> 'b) \<rightarrow> ('a tree \<rightarrow> 'b tree)"
8.162 -and
8.163 - map_forest :: "('a \<rightarrow> 'b) \<rightarrow> ('a forest \<rightarrow> 'b forest)"
8.164 -where
8.165 - "map_tree\<cdot>f\<cdot>(Leaf\<cdot>x) = Leaf\<cdot>(f\<cdot>x)"
8.166 -| "map_tree\<cdot>f\<cdot>(Branch\<cdot>ts) = Branch\<cdot>(map_forest\<cdot>f\<cdot>ts)"
8.167 -| "map_forest\<cdot>f\<cdot>Empty = Empty"
8.168 -| "ts \<noteq> \<bottom> \<Longrightarrow>
8.169 - 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)"
8.170 -
8.171 -lemma map_tree_strict [simp]: "map_tree\<cdot>f\<cdot>\<bottom> = \<bottom>"
8.172 -by fixrec_simp
8.173 -
8.174 -lemma map_forest_strict [simp]: "map_forest\<cdot>f\<cdot>\<bottom> = \<bottom>"
8.175 -by fixrec_simp
8.176 -
8.177 -text {*
8.178 - Theorems generated:
8.179 - @{text map_tree_def} @{thm map_tree_def}
8.180 - @{text map_forest_def} @{thm map_forest_def}
8.181 - @{text map_tree.unfold} @{thm map_tree.unfold}
8.182 - @{text map_forest.unfold} @{thm map_forest.unfold}
8.183 - @{text map_tree.simps} @{thm map_tree.simps}
8.184 - @{text map_forest.simps} @{thm map_forest.simps}
8.185 - @{text map_tree_map_forest.induct} @{thm map_tree_map_forest.induct}
8.186 -*}
8.187 -
8.188 -
8.189 -subsection {* Looping simp rules *}
8.190 -
8.191 -text {*
8.192 - The defining equations of a fixrec definition are declared as simp
8.193 - rules by default. In some cases, especially for constants with no
8.194 - arguments or functions with variable patterns, the defining
8.195 - equations may cause the simplifier to loop. In these cases it will
8.196 - be necessary to use a @{text "[simp del]"} declaration.
8.197 -*}
8.198 -
8.199 -fixrec
8.200 - repeat :: "'a \<rightarrow> 'a llist"
8.201 -where
8.202 - [simp del]: "repeat\<cdot>x = lCons\<cdot>x\<cdot>(repeat\<cdot>x)"
8.203 -
8.204 -text {*
8.205 - We can derive other non-looping simp rules for @{const repeat} by
8.206 - using the @{text subst} method with the @{text repeat.simps} rule.
8.207 -*}
8.208 -
8.209 -lemma repeat_simps [simp]:
8.210 - "repeat\<cdot>x \<noteq> \<bottom>"
8.211 - "repeat\<cdot>x \<noteq> lNil"
8.212 - "repeat\<cdot>x = lCons\<cdot>y\<cdot>ys \<longleftrightarrow> x = y \<and> repeat\<cdot>x = ys"
8.213 -by (subst repeat.simps, simp)+
8.214 -
8.215 -lemma llist_when_repeat [simp]:
8.216 - "llist_when\<cdot>z\<cdot>f\<cdot>(repeat\<cdot>x) = f\<cdot>x\<cdot>(repeat\<cdot>x)"
8.217 -by (subst repeat.simps, simp)
8.218 -
8.219 -text {*
8.220 - For mutually-recursive constants, looping might only occur if all
8.221 - equations are in the simpset at the same time. In such cases it may
8.222 - only be necessary to declare @{text "[simp del]"} on one equation.
8.223 -*}
8.224 -
8.225 -fixrec
8.226 - inf_tree :: "'a tree" and inf_forest :: "'a forest"
8.227 -where
8.228 - [simp del]: "inf_tree = Branch\<cdot>inf_forest"
8.229 -| "inf_forest = Trees\<cdot>inf_tree\<cdot>(Trees\<cdot>inf_tree\<cdot>Empty)"
8.230 -
8.231 -
8.232 -subsection {* Using @{text fixrec} inside locales *}
8.233 -
8.234 -locale test =
8.235 - fixes foo :: "'a \<rightarrow> 'a"
8.236 - assumes foo_strict: "foo\<cdot>\<bottom> = \<bottom>"
8.237 -begin
8.238 -
8.239 -fixrec
8.240 - bar :: "'a u \<rightarrow> 'a"
8.241 -where
8.242 - "bar\<cdot>(up\<cdot>x) = foo\<cdot>x"
8.243 -
8.244 -lemma bar_strict: "bar\<cdot>\<bottom> = \<bottom>"
8.245 -by fixrec_simp
8.246 -
8.247 -end
8.248 -
8.249 -end
9.1 --- a/src/HOLCF/ex/New_Domain.thy Wed May 19 16:28:24 2010 -0700
9.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
9.3 @@ -1,92 +0,0 @@
9.4 -(* Title: HOLCF/ex/New_Domain.thy
9.5 - Author: Brian Huffman
9.6 -*)
9.7 -
9.8 -header {* Definitional domain package *}
9.9 -
9.10 -theory New_Domain
9.11 -imports HOLCF
9.12 -begin
9.13 -
9.14 -text {*
9.15 - The definitional domain package only works with representable domains,
9.16 - i.e. types in class @{text rep}.
9.17 -*}
9.18 -
9.19 -default_sort rep
9.20 -
9.21 -text {*
9.22 - Provided that @{text rep} is the default sort, the @{text new_domain}
9.23 - package should work with any type definition supported by the old
9.24 - domain package.
9.25 -*}
9.26 -
9.27 -new_domain 'a llist = LNil | LCons (lazy 'a) (lazy "'a llist")
9.28 -
9.29 -text {*
9.30 - The difference is that the new domain package is completely
9.31 - definitional, and does not generate any axioms. The following type
9.32 - and constant definitions are not produced by the old domain package.
9.33 -*}
9.34 -
9.35 -thm type_definition_llist
9.36 -thm llist_abs_def llist_rep_def
9.37 -
9.38 -text {*
9.39 - The new domain package also adds support for indirect recursion with
9.40 - user-defined datatypes. This definition of a tree datatype uses
9.41 - indirect recursion through the lazy list type constructor.
9.42 -*}
9.43 -
9.44 -new_domain 'a ltree = Leaf (lazy 'a) | Branch (lazy "'a ltree llist")
9.45 -
9.46 -text {*
9.47 - For indirect-recursive definitions, the domain package is not able to
9.48 - generate a high-level induction rule. (It produces a warning
9.49 - message instead.) The low-level reach lemma (now proved as a
9.50 - theorem, no longer generated as an axiom) can be used to derive
9.51 - other induction rules.
9.52 -*}
9.53 -
9.54 -thm ltree.reach
9.55 -
9.56 -text {*
9.57 - The definition of the take function uses map functions associated with
9.58 - each type constructor involved in the definition. A map function
9.59 - for the lazy list type has been generated by the new domain package.
9.60 -*}
9.61 -
9.62 -thm ltree.take_rews
9.63 -thm llist_map_def
9.64 -
9.65 -lemma ltree_induct:
9.66 - fixes P :: "'a ltree \<Rightarrow> bool"
9.67 - assumes adm: "adm P"
9.68 - assumes bot: "P \<bottom>"
9.69 - assumes Leaf: "\<And>x. P (Leaf\<cdot>x)"
9.70 - assumes Branch: "\<And>f l. \<forall>x. P (f\<cdot>x) \<Longrightarrow> P (Branch\<cdot>(llist_map\<cdot>f\<cdot>l))"
9.71 - shows "P x"
9.72 -proof -
9.73 - have "P (\<Squnion>i. ltree_take i\<cdot>x)"
9.74 - using adm
9.75 - proof (rule admD)
9.76 - fix i
9.77 - show "P (ltree_take i\<cdot>x)"
9.78 - proof (induct i arbitrary: x)
9.79 - case (0 x)
9.80 - show "P (ltree_take 0\<cdot>x)" by (simp add: bot)
9.81 - next
9.82 - case (Suc n x)
9.83 - show "P (ltree_take (Suc n)\<cdot>x)"
9.84 - apply (cases x)
9.85 - apply (simp add: bot)
9.86 - apply (simp add: Leaf)
9.87 - apply (simp add: Branch Suc)
9.88 - done
9.89 - qed
9.90 - qed (simp add: ltree.chain_take)
9.91 - thus ?thesis
9.92 - by (simp add: ltree.reach)
9.93 -qed
9.94 -
9.95 -end
10.1 --- a/src/HOLCF/ex/ROOT.ML Wed May 19 16:28:24 2010 -0700
10.2 +++ b/src/HOLCF/ex/ROOT.ML Wed May 19 17:01:07 2010 -0700
10.3 @@ -4,7 +4,6 @@
10.4 *)
10.5
10.6 use_thys ["Dnat", "Stream", "Dagstuhl", "Focus_ex", "Fix2", "Hoare",
10.7 - "Loop", "Fixrec_ex", "Powerdomain_ex", "Domain_ex", "Domain_Proofs",
10.8 + "Loop", "Powerdomain_ex", "Domain_Proofs",
10.9 "Letrec",
10.10 - "Strict_Fun",
10.11 - "New_Domain"];
10.12 + "Strict_Fun"];