1(* Title: HOL/HOLCF/Tutorial/Domain_ex.thy 2 Author: Brian Huffman 3*) 4 5section \<open>Domain package examples\<close> 6 7theory Domain_ex 8imports HOLCF 9begin 10 11text \<open>Domain constructors are strict by default.\<close> 12 13domain d1 = d1a | d1b "d1" "d1" 14 15lemma "d1b\<cdot>\<bottom>\<cdot>y = \<bottom>" by simp 16 17text \<open>Constructors can be made lazy using the \<open>lazy\<close> keyword.\<close> 18 19domain d2 = d2a | d2b (lazy "d2") 20 21lemma "d2b\<cdot>x \<noteq> \<bottom>" by simp 22 23text \<open>Strict and lazy arguments may be mixed arbitrarily.\<close> 24 25domain d3 = d3a | d3b (lazy "d2") "d2" 26 27lemma "P (d3b\<cdot>x\<cdot>y = \<bottom>) \<longleftrightarrow> P (y = \<bottom>)" by simp 28 29text \<open>Selectors can be used with strict or lazy constructor arguments.\<close> 30 31domain d4 = d4a | d4b (lazy d4b_left :: "d2") (d4b_right :: "d2") 32 33lemma "y \<noteq> \<bottom> \<Longrightarrow> d4b_left\<cdot>(d4b\<cdot>x\<cdot>y) = x" by simp 34 35text \<open>Mixfix declarations can be given for data constructors.\<close> 36 37domain d5 = d5a | d5b (lazy "d5") "d5" (infixl ":#:" 70) 38 39lemma "d5a \<noteq> x :#: y :#: z" by simp 40 41text \<open>Mixfix declarations can also be given for type constructors.\<close> 42 43domain ('a, 'b) lazypair (infixl ":*:" 25) = 44 lpair (lazy lfst :: 'a) (lazy lsnd :: 'b) (infixl ":*:" 75) 45 46lemma "\<forall>p::('a :*: 'b). p \<sqsubseteq> lfst\<cdot>p :*: lsnd\<cdot>p" 47by (rule allI, case_tac p, simp_all) 48 49text \<open>Non-recursive constructor arguments can have arbitrary types.\<close> 50 51domain ('a, 'b) d6 = d6 "int lift" "'a \<oplus> 'b u" (lazy "('a :*: 'b) \<times> ('b \<rightarrow> 'a)") 52 53text \<open> 54 Indirect recusion is allowed for sums, products, lifting, and the 55 continuous function space. However, the domain package does not 56 generate an induction rule in terms of the constructors. 57\<close> 58 59domain 'a d7 = d7a "'a d7 \<oplus> int lift" | d7b "'a \<otimes> 'a d7" | d7c (lazy "'a d7 \<rightarrow> 'a") 60 \<comment> \<open>Indirect recursion detected, skipping proofs of (co)induction rules\<close> 61 62text \<open>Note that \<open>d7.induct\<close> is absent.\<close> 63 64text \<open> 65 Indirect recursion is also allowed using previously-defined datatypes. 66\<close> 67 68domain 'a slist = SNil | SCons 'a "'a slist" 69 70domain 'a stree = STip | SBranch "'a stree slist" 71 72text \<open>Mutually-recursive datatypes can be defined using the \<open>and\<close> keyword.\<close> 73 74domain d8 = d8a | d8b "d9" and d9 = d9a | d9b (lazy "d8") 75 76text \<open>Non-regular recursion is not allowed.\<close> 77(* 78domain ('a, 'b) altlist = ANil | ACons 'a "('b, 'a) altlist" 79 -- "illegal direct recursion with different arguments" 80domain 'a nest = Nest1 'a | Nest2 "'a nest nest" 81 -- "illegal direct recursion with different arguments" 82*) 83 84text \<open> 85 Mutually-recursive datatypes must have all the same type arguments, 86 not necessarily in the same order. 87\<close> 88 89domain ('a, 'b) list1 = Nil1 | Cons1 'a "('b, 'a) list2" 90 and ('b, 'a) list2 = Nil2 | Cons2 'b "('a, 'b) list1" 91 92text \<open>Induction rules for flat datatypes have no admissibility side-condition.\<close> 93 94domain 'a flattree = Tip | Branch "'a flattree" "'a flattree" 95 96lemma "\<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" 97by (rule flattree.induct) \<comment> \<open>no admissibility requirement\<close> 98 99text \<open>Trivial datatypes will produce a warning message.\<close> 100 101domain triv = Triv triv triv 102 \<comment> \<open>domain \<open>Domain_ex.triv\<close> is empty!\<close> 103 104lemma "(x::triv) = \<bottom>" by (induct x, simp_all) 105 106text \<open>Lazy constructor arguments may have unpointed types.\<close> 107 108domain natlist = nnil | ncons (lazy "nat discr") natlist 109 110text \<open>Class constraints may be given for type parameters on the LHS.\<close> 111 112domain ('a::predomain) box = Box (lazy 'a) 113 114domain ('a::countable) stream = snil | scons (lazy "'a discr") "'a stream" 115 116 117subsection \<open>Generated constants and theorems\<close> 118 119domain 'a tree = Leaf (lazy 'a) | Node (left :: "'a tree") (right :: "'a tree") 120 121lemmas tree_abs_bottom_iff = 122 iso.abs_bottom_iff [OF iso.intro [OF tree.abs_iso tree.rep_iso]] 123 124text \<open>Rules about ismorphism\<close> 125term tree_rep 126term tree_abs 127thm tree.rep_iso 128thm tree.abs_iso 129thm tree.iso_rews 130 131text \<open>Rules about constructors\<close> 132term Leaf 133term Node 134thm Leaf_def Node_def 135thm tree.nchotomy 136thm tree.exhaust 137thm tree.compacts 138thm tree.con_rews 139thm tree.dist_les 140thm tree.dist_eqs 141thm tree.inverts 142thm tree.injects 143 144text \<open>Rules about case combinator\<close> 145term tree_case 146thm tree.tree_case_def 147thm tree.case_rews 148 149text \<open>Rules about selectors\<close> 150term left 151term right 152thm tree.sel_rews 153 154text \<open>Rules about discriminators\<close> 155term is_Leaf 156term is_Node 157thm tree.dis_rews 158 159text \<open>Rules about monadic pattern match combinators\<close> 160term match_Leaf 161term match_Node 162thm tree.match_rews 163 164text \<open>Rules about take function\<close> 165term tree_take 166thm tree.take_def 167thm tree.take_0 168thm tree.take_Suc 169thm tree.take_rews 170thm tree.chain_take 171thm tree.take_take 172thm tree.deflation_take 173thm tree.take_below 174thm tree.take_lemma 175thm tree.lub_take 176thm tree.reach 177thm tree.finite_induct 178 179text \<open>Rules about finiteness predicate\<close> 180term tree_finite 181thm tree.finite_def 182thm tree.finite (* only generated for flat datatypes *) 183 184text \<open>Rules about bisimulation predicate\<close> 185term tree_bisim 186thm tree.bisim_def 187thm tree.coinduct 188 189text \<open>Induction rule\<close> 190thm tree.induct 191 192 193subsection \<open>Known bugs\<close> 194 195text \<open>Declaring a mixfix with spaces causes some strange parse errors.\<close> 196(* 197domain xx = xx ("x y") 198 -- "Inner syntax error: unexpected end of input" 199*) 200 201end 202