move some example files into new HOLCF/Tutorial directory
authorhuffman
Wed May 19 17:01:07 2010 -0700 (2010-05-19)
changeset 3700041a22e7c1145
parent 36999 5d9091ba3128
child 37010 8096a4c755eb
move some example files into new HOLCF/Tutorial directory
src/HOLCF/IsaMakefile
src/HOLCF/Tutorial/Domain_ex.thy
src/HOLCF/Tutorial/Fixrec_ex.thy
src/HOLCF/Tutorial/New_Domain.thy
src/HOLCF/Tutorial/ROOT.ML
src/HOLCF/Tutorial/document/root.tex
src/HOLCF/ex/Domain_ex.thy
src/HOLCF/ex/Fixrec_ex.thy
src/HOLCF/ex/New_Domain.thy
src/HOLCF/ex/ROOT.ML
     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"];