src/HOLCF/ex/Domain_ex.thy
author huffman
Fri May 22 13:18:59 2009 -0700 (2009-05-22)
changeset 31232 689aa7da48cc
parent 30922 96d053e00ec0
child 35443 2e0f9516947e
permissions -rw-r--r--
define copy functions using combinators; add checking for failed proofs of induction rules
huffman@30920
     1
(*  Title:      HOLCF/ex/Domain_ex.thy
huffman@30920
     2
    Author:     Brian Huffman
huffman@30920
     3
*)
huffman@30920
     4
huffman@30920
     5
header {* Domain package examples *}
huffman@30920
     6
huffman@30920
     7
theory Domain_ex
huffman@30920
     8
imports HOLCF
huffman@30920
     9
begin
huffman@30920
    10
huffman@30920
    11
text {* Domain constructors are strict by default. *}
huffman@30920
    12
huffman@30920
    13
domain d1 = d1a | d1b "d1" "d1"
huffman@30920
    14
huffman@30920
    15
lemma "d1b\<cdot>\<bottom>\<cdot>y = \<bottom>" by simp
huffman@30920
    16
huffman@30920
    17
text {* Constructors can be made lazy using the @{text "lazy"} keyword. *}
huffman@30920
    18
huffman@30920
    19
domain d2 = d2a | d2b (lazy "d2")
huffman@30920
    20
huffman@30920
    21
lemma "d2b\<cdot>x \<noteq> \<bottom>" by simp
huffman@30920
    22
huffman@30920
    23
text {* Strict and lazy arguments may be mixed arbitrarily. *}
huffman@30920
    24
huffman@30920
    25
domain d3 = d3a | d3b (lazy "d2") "d2"
huffman@30920
    26
huffman@30920
    27
lemma "P (d3b\<cdot>x\<cdot>y = \<bottom>) \<longleftrightarrow> P (y = \<bottom>)" by simp
huffman@30920
    28
huffman@30920
    29
text {* Selectors can be used with strict or lazy constructor arguments. *}
huffman@30920
    30
huffman@30920
    31
domain d4 = d4a | d4b (lazy d4b_left :: "d2") (d4b_right :: "d2")
huffman@30920
    32
huffman@30920
    33
lemma "y \<noteq> \<bottom> \<Longrightarrow> d4b_left\<cdot>(d4b\<cdot>x\<cdot>y) = x" by simp
huffman@30920
    34
huffman@30920
    35
text {* Mixfix declarations can be given for data constructors. *}
huffman@30920
    36
huffman@30920
    37
domain d5 = d5a | d5b (lazy "d5") "d5" (infixl ":#:" 70)
huffman@30920
    38
huffman@30920
    39
lemma "d5a \<noteq> x :#: y :#: z" by simp
huffman@30920
    40
huffman@30920
    41
text {* Mixfix declarations can also be given for type constructors. *}
huffman@30920
    42
huffman@30920
    43
domain ('a, 'b) lazypair (infixl ":*:" 25) =
huffman@30920
    44
  lpair (lazy lfst :: 'a) (lazy lsnd :: 'b) (infixl ":*:" 75)
huffman@30920
    45
huffman@30920
    46
lemma "\<forall>p::('a :*: 'b). p \<sqsubseteq> lfst\<cdot>p :*: lsnd\<cdot>p"
huffman@30920
    47
by (rule allI, case_tac p, simp_all)
huffman@30920
    48
huffman@30920
    49
text {* Non-recursive constructor arguments can have arbitrary types. *}
huffman@30920
    50
huffman@30920
    51
domain ('a, 'b) d6 = d6 "int lift" "'a \<oplus> 'b u" (lazy "('a :*: 'b) \<times> ('b \<rightarrow> 'a)")
huffman@30920
    52
huffman@30920
    53
text {*
huffman@30920
    54
  Indirect recusion is allowed for sums, products, lifting, and the
huffman@30920
    55
  continuous function space.  However, the domain package currently
huffman@31232
    56
  cannot prove the induction rules.  A fix is planned for the next
huffman@31232
    57
  release.
huffman@30920
    58
*}
huffman@30920
    59
huffman@31232
    60
domain 'a d7 = d7a "'a d7 \<oplus> int lift" | d7b "'a \<otimes> 'a d7" | d7c (lazy "'a d7 \<rightarrow> 'a")
huffman@30920
    61
huffman@31232
    62
thm d7.ind -- "currently replaced with dummy theorem"
huffman@30920
    63
huffman@30920
    64
text {*
huffman@30920
    65
  Indirect recursion using previously-defined datatypes is currently
huffman@30920
    66
  not allowed.  This restriction should go away by the next release.
huffman@30920
    67
*}
huffman@30920
    68
(*
huffman@30920
    69
domain 'a slist = SNil | SCons 'a "'a slist"
huffman@30920
    70
domain 'a stree = STip | SBranch "'a stree slist" -- "illegal indirect recursion"
huffman@30920
    71
*)
huffman@30920
    72
huffman@30920
    73
text {* Mutually-recursive datatypes can be defined using the @{text "and"} keyword. *}
huffman@30920
    74
huffman@30920
    75
domain d8 = d8a | d8b "d9" and d9 = d9a | d9b (lazy "d8")
huffman@30920
    76
huffman@30920
    77
text {* Non-regular recursion is not allowed. *}
huffman@30920
    78
(*
huffman@30920
    79
domain ('a, 'b) altlist = ANil | ACons 'a "('b, 'a) altlist"
huffman@30920
    80
  -- "illegal direct recursion with different arguments"
huffman@30920
    81
domain 'a nest = Nest1 'a | Nest2 "'a nest nest"
huffman@30920
    82
  -- "illegal direct recursion with different arguments"
huffman@30920
    83
*)
huffman@30920
    84
huffman@30920
    85
text {*
huffman@30920
    86
  Mutually-recursive datatypes must have all the same type arguments,
huffman@30920
    87
  not necessarily in the same order.
huffman@30920
    88
*}
huffman@30920
    89
huffman@30920
    90
domain ('a, 'b) list1 = Nil1 | Cons1 'a "('b, 'a) list2"
huffman@30920
    91
   and ('b, 'a) list2 = Nil2 | Cons2 'b "('a, 'b) list1"
huffman@30920
    92
huffman@30920
    93
text {* Induction rules for flat datatypes have no admissibility side-condition. *}
huffman@30920
    94
huffman@30920
    95
domain 'a flattree = Tip | Branch "'a flattree" "'a flattree"
huffman@30920
    96
huffman@30920
    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"
huffman@30920
    98
by (rule flattree.ind) -- "no admissibility requirement"
huffman@30920
    99
huffman@30920
   100
text {* Trivial datatypes will produce a warning message. *}
huffman@30920
   101
huffman@30920
   102
domain triv = triv1 triv triv
huffman@30920
   103
  -- "domain Domain_ex.triv is empty!"
huffman@30920
   104
huffman@30920
   105
lemma "(x::triv) = \<bottom>" by (induct x, simp_all)
huffman@30920
   106
huffman@30920
   107
huffman@30920
   108
subsection {* Generated constants and theorems *}
huffman@30920
   109
huffman@30920
   110
domain 'a tree = Leaf (lazy 'a) | Node (left :: "'a tree") (lazy right :: "'a tree")
huffman@30920
   111
huffman@30920
   112
lemmas tree_abs_defined_iff =
huffman@30920
   113
  iso.abs_defined_iff [OF iso.intro [OF tree.abs_iso tree.rep_iso]]
huffman@30920
   114
huffman@30920
   115
text {* Rules about ismorphism *}
huffman@30920
   116
term tree_rep
huffman@30920
   117
term tree_abs
huffman@30920
   118
thm tree.rep_iso
huffman@30920
   119
thm tree.abs_iso
huffman@30920
   120
thm tree.iso_rews
huffman@30920
   121
huffman@30920
   122
text {* Rules about constructors *}
huffman@30920
   123
term Leaf
huffman@30920
   124
term Node
huffman@30920
   125
thm tree.Leaf_def tree.Node_def
huffman@30920
   126
thm tree.exhaust
huffman@30920
   127
thm tree.casedist
huffman@30920
   128
thm tree.compacts
huffman@30920
   129
thm tree.con_rews
huffman@30920
   130
thm tree.dist_les
huffman@30920
   131
thm tree.dist_eqs
huffman@30920
   132
thm tree.inverts
huffman@30920
   133
thm tree.injects
huffman@30920
   134
huffman@30920
   135
text {* Rules about case combinator *}
huffman@30920
   136
term tree_when
huffman@30920
   137
thm tree.when_def
huffman@30920
   138
thm tree.when_rews
huffman@30920
   139
huffman@30920
   140
text {* Rules about selectors *}
huffman@30920
   141
term left
huffman@30920
   142
term right
huffman@30920
   143
thm tree.sel_rews
huffman@30920
   144
huffman@30920
   145
text {* Rules about discriminators *}
huffman@30920
   146
term is_Leaf
huffman@30920
   147
term is_Node
huffman@30920
   148
thm tree.dis_rews
huffman@30920
   149
huffman@30920
   150
text {* Rules about pattern match combinators *}
huffman@30920
   151
term Leaf_pat
huffman@30920
   152
term Node_pat
huffman@30920
   153
thm tree.pat_rews
huffman@30920
   154
huffman@30920
   155
text {* Rules about monadic pattern match combinators *}
huffman@30920
   156
term match_Leaf
huffman@30920
   157
term match_Node
huffman@30920
   158
thm tree.match_rews
huffman@30920
   159
huffman@30920
   160
text {* Rules about copy function *}
huffman@30920
   161
term tree_copy
huffman@30920
   162
thm tree.copy_def
huffman@30920
   163
thm tree.copy_rews
huffman@30920
   164
huffman@30920
   165
text {* Rules about take function *}
huffman@30920
   166
term tree_take
huffman@30920
   167
thm tree.take_def
huffman@30920
   168
thm tree.take_rews
huffman@30920
   169
thm tree.take_lemmas
huffman@30920
   170
thm tree.finite_ind
huffman@30920
   171
huffman@30920
   172
text {* Rules about finiteness predicate *}
huffman@30920
   173
term tree_finite
huffman@30920
   174
thm tree.finite_def
huffman@30920
   175
thm tree.finites
huffman@30920
   176
huffman@30920
   177
text {* Rules about bisimulation predicate *}
huffman@30920
   178
term tree_bisim
huffman@30920
   179
thm tree.bisim_def
huffman@30920
   180
thm tree.coind
huffman@30920
   181
huffman@30920
   182
text {* Induction rule *}
huffman@30920
   183
thm tree.ind
huffman@30920
   184
huffman@30920
   185
huffman@30920
   186
subsection {* Known bugs *}
huffman@30920
   187
huffman@30920
   188
text {* Declaring a mixfix with spaces causes some strange parse errors. *}
huffman@30920
   189
(*
huffman@30920
   190
domain xx = xx ("x y")
huffman@30920
   191
  -- "Inner syntax error: unexpected end of input"
huffman@30920
   192
huffman@30920
   193
domain 'a foo = foo (sel::"'a") ("a b")
huffman@30920
   194
  -- {* Inner syntax error at "= UU" *}
huffman@30920
   195
*)
huffman@30920
   196
huffman@30920
   197
text {*
huffman@30920
   198
  I don't know what is going on here.  The failed proof has to do with
huffman@30920
   199
  the finiteness predicate.
huffman@30920
   200
*}
huffman@30920
   201
(*
huffman@30920
   202
domain foo = Foo (lazy "bar") and bar = Bar
huffman@30920
   203
  -- "Tactic failed."
huffman@30920
   204
*)
huffman@30920
   205
huffman@30922
   206
text {* Declaring class constraints on the LHS is currently broken. *}
huffman@30922
   207
(*
huffman@30922
   208
domain ('a::cpo) box = Box (lazy 'a)
huffman@30922
   209
  -- "Malformed YXML encoding: multiple results"
huffman@30922
   210
*)
huffman@30922
   211
huffman@30922
   212
text {*
huffman@30922
   213
  Class constraints on the RHS are not supported yet.  This feature is
huffman@30922
   214
  planned to replace the old-style LHS class constraints.
huffman@30922
   215
*}
huffman@30922
   216
(*
huffman@30922
   217
domain 'a box = Box (lazy "'a::cpo")
huffman@30922
   218
  -- {* Inconsistent sort constraint for type variable "'a" *}
huffman@30922
   219
*)
huffman@30922
   220
huffman@30920
   221
end