1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOLCF/Tutorial/Domain_ex.thy	Wed May 19 17:01:07 2010 -0700
     1.3 @@ -0,0 +1,211 @@
     1.4 +(*  Title:      HOLCF/ex/Domain_ex.thy
     1.5 +    Author:     Brian Huffman
     1.6 +*)
     1.7 +
     1.8 +header {* Domain package examples *}
     1.9 +
    1.10 +theory Domain_ex
    1.11 +imports HOLCF
    1.12 +begin
    1.13 +
    1.14 +text {* Domain constructors are strict by default. *}
    1.15 +
    1.16 +domain d1 = d1a | d1b "d1" "d1"
    1.17 +
    1.18 +lemma "d1b\<cdot>\<bottom>\<cdot>y = \<bottom>" by simp
    1.19 +
    1.20 +text {* Constructors can be made lazy using the @{text "lazy"} keyword. *}
    1.21 +
    1.22 +domain d2 = d2a | d2b (lazy "d2")
    1.23 +
    1.24 +lemma "d2b\<cdot>x \<noteq> \<bottom>" by simp
    1.25 +
    1.26 +text {* Strict and lazy arguments may be mixed arbitrarily. *}
    1.27 +
    1.28 +domain d3 = d3a | d3b (lazy "d2") "d2"
    1.29 +
    1.30 +lemma "P (d3b\<cdot>x\<cdot>y = \<bottom>) \<longleftrightarrow> P (y = \<bottom>)" by simp
    1.31 +
    1.32 +text {* Selectors can be used with strict or lazy constructor arguments. *}
    1.33 +
    1.34 +domain d4 = d4a | d4b (lazy d4b_left :: "d2") (d4b_right :: "d2")
    1.35 +
    1.36 +lemma "y \<noteq> \<bottom> \<Longrightarrow> d4b_left\<cdot>(d4b\<cdot>x\<cdot>y) = x" by simp
    1.37 +
    1.38 +text {* Mixfix declarations can be given for data constructors. *}
    1.39 +
    1.40 +domain d5 = d5a | d5b (lazy "d5") "d5" (infixl ":#:" 70)
    1.41 +
    1.42 +lemma "d5a \<noteq> x :#: y :#: z" by simp
    1.43 +
    1.44 +text {* Mixfix declarations can also be given for type constructors. *}
    1.45 +
    1.46 +domain ('a, 'b) lazypair (infixl ":*:" 25) =
    1.47 +  lpair (lazy lfst :: 'a) (lazy lsnd :: 'b) (infixl ":*:" 75)
    1.48 +
    1.49 +lemma "\<forall>p::('a :*: 'b). p \<sqsubseteq> lfst\<cdot>p :*: lsnd\<cdot>p"
    1.50 +by (rule allI, case_tac p, simp_all)
    1.51 +
    1.52 +text {* Non-recursive constructor arguments can have arbitrary types. *}
    1.53 +
    1.54 +domain ('a, 'b) d6 = d6 "int lift" "'a \<oplus> 'b u" (lazy "('a :*: 'b) \<times> ('b \<rightarrow> 'a)")
    1.55 +
    1.56 +text {*
    1.57 +  Indirect recusion is allowed for sums, products, lifting, and the
    1.58 +  continuous function space.  However, the domain package does not
    1.59 +  generate an induction rule in terms of the constructors.
    1.60 +*}
    1.61 +
    1.62 +domain 'a d7 = d7a "'a d7 \<oplus> int lift" | d7b "'a \<otimes> 'a d7" | d7c (lazy "'a d7 \<rightarrow> 'a")
    1.63 +  -- "Indirect recursion detected, skipping proofs of (co)induction rules"
    1.64 +
    1.65 +text {* Note that @{text d7.induct} is absent. *}
    1.66 +
    1.67 +text {*
    1.68 +  Indirect recursion is also allowed using previously-defined datatypes.
    1.69 +*}
    1.70 +
    1.71 +domain 'a slist = SNil | SCons 'a "'a slist"
    1.72 +
    1.73 +domain 'a stree = STip | SBranch "'a stree slist"
    1.74 +
    1.75 +text {* Mutually-recursive datatypes can be defined using the @{text "and"} keyword. *}
    1.76 +
    1.77 +domain d8 = d8a | d8b "d9" and d9 = d9a | d9b (lazy "d8")
    1.78 +
    1.79 +text {* Non-regular recursion is not allowed. *}
    1.80 +(*
    1.81 +domain ('a, 'b) altlist = ANil | ACons 'a "('b, 'a) altlist"
    1.82 +  -- "illegal direct recursion with different arguments"
    1.83 +domain 'a nest = Nest1 'a | Nest2 "'a nest nest"
    1.84 +  -- "illegal direct recursion with different arguments"
    1.85 +*)
    1.86 +
    1.87 +text {*
    1.88 +  Mutually-recursive datatypes must have all the same type arguments,
    1.89 +  not necessarily in the same order.
    1.90 +*}
    1.91 +
    1.92 +domain ('a, 'b) list1 = Nil1 | Cons1 'a "('b, 'a) list2"
    1.93 +   and ('b, 'a) list2 = Nil2 | Cons2 'b "('a, 'b) list1"
    1.94 +
    1.95 +text {* Induction rules for flat datatypes have no admissibility side-condition. *}
    1.96 +
    1.97 +domain 'a flattree = Tip | Branch "'a flattree" "'a flattree"
    1.98 +
    1.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"
   1.100 +by (rule flattree.induct) -- "no admissibility requirement"
   1.101 +
   1.102 +text {* Trivial datatypes will produce a warning message. *}
   1.103 +
   1.104 +domain triv = Triv triv triv
   1.105 +  -- "domain @{text Domain_ex.triv} is empty!"
   1.106 +
   1.107 +lemma "(x::triv) = \<bottom>" by (induct x, simp_all)
   1.108 +
   1.109 +text {* Lazy constructor arguments may have unpointed types. *}
   1.110 +
   1.111 +domain natlist = nnil | ncons (lazy "nat discr") natlist
   1.112 +
   1.113 +text {* Class constraints may be given for type parameters on the LHS. *}
   1.114 +
   1.115 +domain ('a::cpo) box = Box (lazy 'a)
   1.116 +
   1.117 +
   1.118 +subsection {* Generated constants and theorems *}
   1.119 +
   1.120 +domain 'a tree = Leaf (lazy 'a) | Node (left :: "'a tree") (right :: "'a tree")
   1.121 +
   1.122 +lemmas tree_abs_defined_iff =
   1.123 +  iso.abs_defined_iff [OF iso.intro [OF tree.abs_iso tree.rep_iso]]
   1.124 +
   1.125 +text {* Rules about ismorphism *}
   1.126 +term tree_rep
   1.127 +term tree_abs
   1.128 +thm tree.rep_iso
   1.129 +thm tree.abs_iso
   1.130 +thm tree.iso_rews
   1.131 +
   1.132 +text {* Rules about constructors *}
   1.133 +term Leaf
   1.134 +term Node
   1.135 +thm Leaf_def Node_def
   1.136 +thm tree.nchotomy
   1.137 +thm tree.exhaust
   1.138 +thm tree.compacts
   1.139 +thm tree.con_rews
   1.140 +thm tree.dist_les
   1.141 +thm tree.dist_eqs
   1.142 +thm tree.inverts
   1.143 +thm tree.injects
   1.144 +
   1.145 +text {* Rules about case combinator *}
   1.146 +term tree_when
   1.147 +thm tree.tree_when_def
   1.148 +thm tree.when_rews
   1.149 +
   1.150 +text {* Rules about selectors *}
   1.151 +term left
   1.152 +term right
   1.153 +thm tree.sel_rews
   1.154 +
   1.155 +text {* Rules about discriminators *}
   1.156 +term is_Leaf
   1.157 +term is_Node
   1.158 +thm tree.dis_rews
   1.159 +
   1.160 +text {* Rules about pattern match combinators *}
   1.161 +term Leaf_pat
   1.162 +term Node_pat
   1.163 +thm tree.pat_rews
   1.164 +
   1.165 +text {* Rules about monadic pattern match combinators *}
   1.166 +term match_Leaf
   1.167 +term match_Node
   1.168 +thm tree.match_rews
   1.169 +
   1.170 +text {* Rules about take function *}
   1.171 +term tree_take
   1.172 +thm tree.take_def
   1.173 +thm tree.take_0
   1.174 +thm tree.take_Suc
   1.175 +thm tree.take_rews
   1.176 +thm tree.chain_take
   1.177 +thm tree.take_take
   1.178 +thm tree.deflation_take
   1.179 +thm tree.take_below
   1.180 +thm tree.take_lemma
   1.181 +thm tree.lub_take
   1.182 +thm tree.reach
   1.183 +thm tree.finite_induct
   1.184 +
   1.185 +text {* Rules about finiteness predicate *}
   1.186 +term tree_finite
   1.187 +thm tree.finite_def
   1.188 +thm tree.finite (* only generated for flat datatypes *)
   1.189 +
   1.190 +text {* Rules about bisimulation predicate *}
   1.191 +term tree_bisim
   1.192 +thm tree.bisim_def
   1.193 +thm tree.coinduct
   1.194 +
   1.195 +text {* Induction rule *}
   1.196 +thm tree.induct
   1.197 +
   1.198 +
   1.199 +subsection {* Known bugs *}
   1.200 +
   1.201 +text {* Declaring a mixfix with spaces causes some strange parse errors. *}
   1.202 +(*
   1.203 +domain xx = xx ("x y")
   1.204 +  -- "Inner syntax error: unexpected end of input"
   1.205 +*)
   1.206 +
   1.207 +text {*
   1.208 +  Non-cpo type parameters currently do not work.
   1.209 +*}
   1.210 +(*
   1.211 +domain ('a::type) stream = snil | scons (lazy "'a discr") "'a stream"
   1.212 +*)
   1.213 +
   1.214 +end