src/HOLCF/ex/Domain_ex.thy
author huffman
Sun Mar 07 16:39:31 2010 -0800 (2010-03-07)
changeset 35642 f478d5a9d238
parent 35585 555f26f00e47
child 35661 ede27eb8e94b
permissions -rw-r--r--
generate separate qualified theorem name for each type's reach and take_lemma
     1 (*  Title:      HOLCF/ex/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 
    61 (* d7.ind is absent *)
    62 
    63 text {*
    64   Indirect recursion using previously-defined datatypes is currently
    65   not allowed.  This restriction does not apply to the new definitional
    66   domain package.
    67 *}
    68 (*
    69 domain 'a slist = SNil | SCons 'a "'a slist"
    70 domain 'a stree = STip | SBranch "'a stree slist" -- "illegal indirect recursion"
    71 *)
    72 
    73 text {* Mutually-recursive datatypes can be defined using the @{text "and"} keyword. *}
    74 
    75 domain d8 = d8a | d8b "d9" and d9 = d9a | d9b (lazy "d8")
    76 
    77 text {* Non-regular recursion is not allowed. *}
    78 (*
    79 domain ('a, 'b) altlist = ANil | ACons 'a "('b, 'a) altlist"
    80   -- "illegal direct recursion with different arguments"
    81 domain 'a nest = Nest1 'a | Nest2 "'a nest nest"
    82   -- "illegal direct recursion with different arguments"
    83 *)
    84 
    85 text {*
    86   Mutually-recursive datatypes must have all the same type arguments,
    87   not necessarily in the same order.
    88 *}
    89 
    90 domain ('a, 'b) list1 = Nil1 | Cons1 'a "('b, 'a) list2"
    91    and ('b, 'a) list2 = Nil2 | Cons2 'b "('a, 'b) list1"
    92 
    93 text {* Induction rules for flat datatypes have no admissibility side-condition. *}
    94 
    95 domain 'a flattree = Tip | Branch "'a flattree" "'a flattree"
    96 
    97 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"
    98 by (rule flattree.ind) -- "no admissibility requirement"
    99 
   100 text {* Trivial datatypes will produce a warning message. *}
   101 
   102 domain triv = Triv triv triv
   103   -- "domain Domain_ex.triv is empty!"
   104 
   105 lemma "(x::triv) = \<bottom>" by (induct x, simp_all)
   106 
   107 
   108 subsection {* Generated constants and theorems *}
   109 
   110 domain 'a tree = Leaf (lazy 'a) | Node (left :: "'a tree") (lazy right :: "'a tree")
   111 
   112 lemmas tree_abs_defined_iff =
   113   iso.abs_defined_iff [OF iso.intro [OF tree.abs_iso tree.rep_iso]]
   114 
   115 text {* Rules about ismorphism *}
   116 term tree_rep
   117 term tree_abs
   118 thm tree.rep_iso
   119 thm tree.abs_iso
   120 thm tree.iso_rews
   121 
   122 text {* Rules about constructors *}
   123 term Leaf
   124 term Node
   125 thm Leaf_def Node_def
   126 thm tree.exhaust
   127 thm tree.casedist
   128 thm tree.compacts
   129 thm tree.con_rews
   130 thm tree.dist_les
   131 thm tree.dist_eqs
   132 thm tree.inverts
   133 thm tree.injects
   134 
   135 text {* Rules about case combinator *}
   136 term tree_when
   137 thm tree.tree_when_def
   138 thm tree.when_rews
   139 
   140 text {* Rules about selectors *}
   141 term left
   142 term right
   143 thm tree.sel_rews
   144 
   145 text {* Rules about discriminators *}
   146 term is_Leaf
   147 term is_Node
   148 thm tree.dis_rews
   149 
   150 text {* Rules about pattern match combinators *}
   151 term Leaf_pat
   152 term Node_pat
   153 thm tree.pat_rews
   154 
   155 text {* Rules about monadic pattern match combinators *}
   156 term match_Leaf
   157 term match_Node
   158 thm tree.match_rews
   159 
   160 text {* Rules about take function *}
   161 term tree_take
   162 thm tree.take_def
   163 thm tree.take_0
   164 thm tree.take_Suc
   165 thm tree.take_rews
   166 thm tree.chain_take
   167 thm tree.take_take
   168 thm tree.deflation_take
   169 thm tree.take_lemma
   170 thm tree.lub_take
   171 thm tree.reach
   172 thm tree.finite_ind
   173 
   174 text {* Rules about finiteness predicate *}
   175 term tree_finite
   176 thm tree.finite_def
   177 thm tree.finites
   178 
   179 text {* Rules about bisimulation predicate *}
   180 term tree_bisim
   181 thm tree.bisim_def
   182 thm tree.coind
   183 
   184 text {* Induction rule *}
   185 thm tree.ind
   186 
   187 
   188 subsection {* Known bugs *}
   189 
   190 text {* Declaring a mixfix with spaces causes some strange parse errors. *}
   191 (*
   192 domain xx = xx ("x y")
   193   -- "Inner syntax error: unexpected end of input"
   194 
   195 domain 'a foo = foo (sel::"'a") ("a b")
   196   -- {* Inner syntax error at "= UU" *}
   197 *)
   198 
   199 text {*
   200   I don't know what is going on here.  The failed proof has to do with
   201   the finiteness predicate.
   202 *}
   203 
   204 domain foo = Foo (lazy "bar") and bar = Bar
   205   -- "Cannot prove induction rule"
   206 
   207 text {* Declaring class constraints on the LHS is currently broken. *}
   208 (*
   209 domain ('a::cpo) box = Box (lazy 'a)
   210   -- "Proof failed"
   211 *)
   212 
   213 text {*
   214   Class constraints on the RHS are not supported yet.  This feature is
   215   planned to replace the old-style LHS class constraints.
   216 *}
   217 (*
   218 domain 'a box = Box (lazy "'a::cpo")
   219   -- {* Inconsistent sort constraint for type variable "'a" *}
   220 *)
   221 
   222 end