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