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