author  huffman 
Sat, 27 Nov 2010 16:08:10 0800  
changeset 40774  0437dbc127b3 
parent 40501  src/HOLCF/Tutorial/Domain_ex.thy@2ed71459136e 
child 42151  4da4fc77664b 
permissions  rwrr 
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 {* Nonrecursive 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 
35585
555f26f00e47
skip proof of induction rule for indirectrecursive domain definitions
huffman
parents:
35497
diff
changeset

55 
continuous function space. However, the domain package does not 
555f26f00e47
skip proof of induction rule for indirectrecursive domain definitions
huffman
parents:
35497
diff
changeset

56 
generate an induction rule in terms of the constructors. 
30920
811ab0923a62
add HOLCF/ex/Domain_ex.thy, with example uses of the domain package
huffman
parents:
diff
changeset

57 
*} 
811ab0923a62
add HOLCF/ex/Domain_ex.thy, with example uses of the domain package
huffman
parents:
diff
changeset

58 

31232
689aa7da48cc
define copy functions using combinators; add checking for failed proofs of induction rules
huffman
parents:
30922
diff
changeset

59 
domain 'a d7 = d7a "'a d7 \<oplus> int lift"  d7b "'a \<otimes> 'a d7"  d7c (lazy "'a d7 \<rightarrow> 'a") 
36120  60 
 "Indirect recursion detected, skipping proofs of (co)induction rules" 
37000
41a22e7c1145
move some example files into new HOLCF/Tutorial directory
huffman
parents:
36120
diff
changeset

61 

41a22e7c1145
move some example files into new HOLCF/Tutorial directory
huffman
parents:
36120
diff
changeset

62 
text {* Note that @{text d7.induct} is absent. *} 
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 {* 
36120  65 
Indirect recursion is also allowed using previouslydefined datatypes. 
30920
811ab0923a62
add HOLCF/ex/Domain_ex.thy, with example uses of the domain package
huffman
parents:
diff
changeset

66 
*} 
36120  67 

30920
811ab0923a62
add HOLCF/ex/Domain_ex.thy, with example uses of the domain package
huffman
parents:
diff
changeset

68 
domain 'a slist = SNil  SCons 'a "'a slist" 
36120  69 

70 
domain 'a stree = STip  SBranch "'a stree slist" 

30920
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 
text {* Mutuallyrecursive 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

73 

811ab0923a62
add HOLCF/ex/Domain_ex.thy, with example uses of the domain package
huffman
parents:
diff
changeset

74 
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

75 

811ab0923a62
add HOLCF/ex/Domain_ex.thy, with example uses of the domain package
huffman
parents:
diff
changeset

76 
text {* Nonregular recursion is not allowed. *} 
811ab0923a62
add HOLCF/ex/Domain_ex.thy, with example uses of the domain package
huffman
parents:
diff
changeset

77 
(* 
811ab0923a62
add HOLCF/ex/Domain_ex.thy, with example uses of the domain package
huffman
parents:
diff
changeset

78 
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

79 
 "illegal direct recursion with different arguments" 
811ab0923a62
add HOLCF/ex/Domain_ex.thy, with example uses of the domain package
huffman
parents:
diff
changeset

80 
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

81 
 "illegal direct recursion with different arguments" 
811ab0923a62
add HOLCF/ex/Domain_ex.thy, with example uses of the domain package
huffman
parents:
diff
changeset

82 
*) 
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 
text {* 
811ab0923a62
add HOLCF/ex/Domain_ex.thy, with example uses of the domain package
huffman
parents:
diff
changeset

85 
Mutuallyrecursive 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

86 
not necessarily in the same order. 
811ab0923a62
add HOLCF/ex/Domain_ex.thy, with example uses of the domain package
huffman
parents:
diff
changeset

87 
*} 
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 
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

90 
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

91 

811ab0923a62
add HOLCF/ex/Domain_ex.thy, with example uses of the domain package
huffman
parents:
diff
changeset

92 
text {* Induction rules for flat datatypes have no admissibility sidecondition. *} 
811ab0923a62
add HOLCF/ex/Domain_ex.thy, with example uses of the domain package
huffman
parents:
diff
changeset

93 

811ab0923a62
add HOLCF/ex/Domain_ex.thy, with example uses of the domain package
huffman
parents:
diff
changeset

94 
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

95 

811ab0923a62
add HOLCF/ex/Domain_ex.thy, with example uses of the domain package
huffman
parents:
diff
changeset

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" 
35781
b7738ab762b1
renamed some lemmas generated by the domain package
huffman
parents:
35661
diff
changeset

97 
by (rule flattree.induct)  "no admissibility requirement" 
30920
811ab0923a62
add HOLCF/ex/Domain_ex.thy, with example uses of the domain package
huffman
parents:
diff
changeset

98 

811ab0923a62
add HOLCF/ex/Domain_ex.thy, with example uses of the domain package
huffman
parents:
diff
changeset

99 
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

100 

35443
2e0f9516947e
change domain package's treatment of variable names in theorems to be like datatype package
huffman
parents:
31232
diff
changeset

101 
domain triv = Triv triv triv 
37000
41a22e7c1145
move some example files into new HOLCF/Tutorial directory
huffman
parents:
36120
diff
changeset

102 
 "domain @{text Domain_ex.triv} is empty!" 
30920
811ab0923a62
add HOLCF/ex/Domain_ex.thy, with example uses of the domain package
huffman
parents:
diff
changeset

103 

811ab0923a62
add HOLCF/ex/Domain_ex.thy, with example uses of the domain package
huffman
parents:
diff
changeset

104 
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

105 

36120  106 
text {* Lazy constructor arguments may have unpointed types. *} 
107 

40501
2ed71459136e
allow unpointed lazy arguments for definitional domain package
huffman
parents:
40329
diff
changeset

108 
domain natlist = nnil  ncons (lazy "nat discr") natlist 
36120  109 

110 
text {* Class constraints may be given for type parameters on the LHS. *} 

111 

40501
2ed71459136e
allow unpointed lazy arguments for definitional domain package
huffman
parents:
40329
diff
changeset

112 
domain ('a::predomain) box = Box (lazy 'a) 
40329
73f2b99b549d
change default_sort of HOLCF from pcpo to bifinite; rename command 'new_domain' to 'domain'; rename 'domain' to 'domain (unsafe)'
huffman
parents:
40321
diff
changeset

113 

40501
2ed71459136e
allow unpointed lazy arguments for definitional domain package
huffman
parents:
40329
diff
changeset

114 
domain ('a::countable) stream = snil  scons (lazy "'a discr") "'a stream" 
36120  115 

30920
811ab0923a62
add HOLCF/ex/Domain_ex.thy, with example uses of the domain package
huffman
parents:
diff
changeset

116 

811ab0923a62
add HOLCF/ex/Domain_ex.thy, with example uses of the domain package
huffman
parents:
diff
changeset

117 
subsection {* Generated constants and theorems *} 
811ab0923a62
add HOLCF/ex/Domain_ex.thy, with example uses of the domain package
huffman
parents:
diff
changeset

118 

35661
ede27eb8e94b
don't generate rule foo.finites for nonflat domains; use take_induct rule to prove induction rule
huffman
parents:
35642
diff
changeset

119 
domain 'a tree = Leaf (lazy 'a)  Node (left :: "'a tree") (right :: "'a tree") 
30920
811ab0923a62
add HOLCF/ex/Domain_ex.thy, with example uses of the domain package
huffman
parents:
diff
changeset

120 

40321
d065b195ec89
rename lemmas *_defined_iff and *_strict_iff to *_bottom_iff
huffman
parents:
40213
diff
changeset

121 
lemmas tree_abs_bottom_iff = 
d065b195ec89
rename lemmas *_defined_iff and *_strict_iff to *_bottom_iff
huffman
parents:
40213
diff
changeset

122 
iso.abs_bottom_iff [OF iso.intro [OF tree.abs_iso tree.rep_iso]] 
30920
811ab0923a62
add HOLCF/ex/Domain_ex.thy, with example uses of the domain package
huffman
parents:
diff
changeset

123 

811ab0923a62
add HOLCF/ex/Domain_ex.thy, with example uses of the domain package
huffman
parents:
diff
changeset

124 
text {* Rules about ismorphism *} 
811ab0923a62
add HOLCF/ex/Domain_ex.thy, with example uses of the domain package
huffman
parents:
diff
changeset

125 
term tree_rep 
811ab0923a62
add HOLCF/ex/Domain_ex.thy, with example uses of the domain package
huffman
parents:
diff
changeset

126 
term tree_abs 
811ab0923a62
add HOLCF/ex/Domain_ex.thy, with example uses of the domain package
huffman
parents:
diff
changeset

127 
thm tree.rep_iso 
811ab0923a62
add HOLCF/ex/Domain_ex.thy, with example uses of the domain package
huffman
parents:
diff
changeset

128 
thm tree.abs_iso 
811ab0923a62
add HOLCF/ex/Domain_ex.thy, with example uses of the domain package
huffman
parents:
diff
changeset

129 
thm tree.iso_rews 
811ab0923a62
add HOLCF/ex/Domain_ex.thy, with example uses of the domain package
huffman
parents:
diff
changeset

130 

811ab0923a62
add HOLCF/ex/Domain_ex.thy, with example uses of the domain package
huffman
parents:
diff
changeset

131 
text {* Rules about constructors *} 
811ab0923a62
add HOLCF/ex/Domain_ex.thy, with example uses of the domain package
huffman
parents:
diff
changeset

132 
term Leaf 
811ab0923a62
add HOLCF/ex/Domain_ex.thy, with example uses of the domain package
huffman
parents:
diff
changeset

133 
term Node 
35444  134 
thm Leaf_def Node_def 
35781
b7738ab762b1
renamed some lemmas generated by the domain package
huffman
parents:
35661
diff
changeset

135 
thm tree.nchotomy 
30920
811ab0923a62
add HOLCF/ex/Domain_ex.thy, with example uses of the domain package
huffman
parents:
diff
changeset

136 
thm tree.exhaust 
811ab0923a62
add HOLCF/ex/Domain_ex.thy, with example uses of the domain package
huffman
parents:
diff
changeset

137 
thm tree.compacts 
811ab0923a62
add HOLCF/ex/Domain_ex.thy, with example uses of the domain package
huffman
parents:
diff
changeset

138 
thm tree.con_rews 
811ab0923a62
add HOLCF/ex/Domain_ex.thy, with example uses of the domain package
huffman
parents:
diff
changeset

139 
thm tree.dist_les 
811ab0923a62
add HOLCF/ex/Domain_ex.thy, with example uses of the domain package
huffman
parents:
diff
changeset

140 
thm tree.dist_eqs 
811ab0923a62
add HOLCF/ex/Domain_ex.thy, with example uses of the domain package
huffman
parents:
diff
changeset

141 
thm tree.inverts 
811ab0923a62
add HOLCF/ex/Domain_ex.thy, with example uses of the domain package
huffman
parents:
diff
changeset

142 
thm tree.injects 
811ab0923a62
add HOLCF/ex/Domain_ex.thy, with example uses of the domain package
huffman
parents:
diff
changeset

143 

811ab0923a62
add HOLCF/ex/Domain_ex.thy, with example uses of the domain package
huffman
parents:
diff
changeset

144 
text {* Rules about case combinator *} 
40213
b63e966564da
rename case combinators generated by domain package to 'foo_case' instead of 'foo_when'
huffman
parents:
37109
diff
changeset

145 
term tree_case 
b63e966564da
rename case combinators generated by domain package to 'foo_case' instead of 'foo_when'
huffman
parents:
37109
diff
changeset

146 
thm tree.tree_case_def 
b63e966564da
rename case combinators generated by domain package to 'foo_case' instead of 'foo_when'
huffman
parents:
37109
diff
changeset

147 
thm tree.case_rews 
30920
811ab0923a62
add HOLCF/ex/Domain_ex.thy, with example uses of the domain package
huffman
parents:
diff
changeset

148 

811ab0923a62
add HOLCF/ex/Domain_ex.thy, with example uses of the domain package
huffman
parents:
diff
changeset

149 
text {* Rules about selectors *} 
811ab0923a62
add HOLCF/ex/Domain_ex.thy, with example uses of the domain package
huffman
parents:
diff
changeset

150 
term left 
811ab0923a62
add HOLCF/ex/Domain_ex.thy, with example uses of the domain package
huffman
parents:
diff
changeset

151 
term right 
811ab0923a62
add HOLCF/ex/Domain_ex.thy, with example uses of the domain package
huffman
parents:
diff
changeset

152 
thm tree.sel_rews 
811ab0923a62
add HOLCF/ex/Domain_ex.thy, with example uses of the domain package
huffman
parents:
diff
changeset

153 

811ab0923a62
add HOLCF/ex/Domain_ex.thy, with example uses of the domain package
huffman
parents:
diff
changeset

154 
text {* Rules about discriminators *} 
811ab0923a62
add HOLCF/ex/Domain_ex.thy, with example uses of the domain package
huffman
parents:
diff
changeset

155 
term is_Leaf 
811ab0923a62
add HOLCF/ex/Domain_ex.thy, with example uses of the domain package
huffman
parents:
diff
changeset

156 
term is_Node 
811ab0923a62
add HOLCF/ex/Domain_ex.thy, with example uses of the domain package
huffman
parents:
diff
changeset

157 
thm tree.dis_rews 
811ab0923a62
add HOLCF/ex/Domain_ex.thy, with example uses of the domain package
huffman
parents:
diff
changeset

158 

811ab0923a62
add HOLCF/ex/Domain_ex.thy, with example uses of the domain package
huffman
parents:
diff
changeset

159 
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

160 
term match_Leaf 
811ab0923a62
add HOLCF/ex/Domain_ex.thy, with example uses of the domain package
huffman
parents:
diff
changeset

161 
term match_Node 
811ab0923a62
add HOLCF/ex/Domain_ex.thy, with example uses of the domain package
huffman
parents:
diff
changeset

162 
thm tree.match_rews 
811ab0923a62
add HOLCF/ex/Domain_ex.thy, with example uses of the domain package
huffman
parents:
diff
changeset

163 

811ab0923a62
add HOLCF/ex/Domain_ex.thy, with example uses of the domain package
huffman
parents:
diff
changeset

164 
text {* Rules about take function *} 
811ab0923a62
add HOLCF/ex/Domain_ex.thy, with example uses of the domain package
huffman
parents:
diff
changeset

165 
term tree_take 
811ab0923a62
add HOLCF/ex/Domain_ex.thy, with example uses of the domain package
huffman
parents:
diff
changeset

166 
thm tree.take_def 
35494
45c9a8278faf
domain package no longer generates copy functions; all proofs use take functions instead
huffman
parents:
35444
diff
changeset

167 
thm tree.take_0 
45c9a8278faf
domain package no longer generates copy functions; all proofs use take functions instead
huffman
parents:
35444
diff
changeset

168 
thm tree.take_Suc 
30920
811ab0923a62
add HOLCF/ex/Domain_ex.thy, with example uses of the domain package
huffman
parents:
diff
changeset

169 
thm tree.take_rews 
35494
45c9a8278faf
domain package no longer generates copy functions; all proofs use take functions instead
huffman
parents:
35444
diff
changeset

170 
thm tree.chain_take 
45c9a8278faf
domain package no longer generates copy functions; all proofs use take functions instead
huffman
parents:
35444
diff
changeset

171 
thm tree.take_take 
45c9a8278faf
domain package no longer generates copy functions; all proofs use take functions instead
huffman
parents:
35444
diff
changeset

172 
thm tree.deflation_take 
35781
b7738ab762b1
renamed some lemmas generated by the domain package
huffman
parents:
35661
diff
changeset

173 
thm tree.take_below 
35642
f478d5a9d238
generate separate qualified theorem name for each type's reach and take_lemma
huffman
parents:
35585
diff
changeset

174 
thm tree.take_lemma 
35585
555f26f00e47
skip proof of induction rule for indirectrecursive domain definitions
huffman
parents:
35497
diff
changeset

175 
thm tree.lub_take 
35494
45c9a8278faf
domain package no longer generates copy functions; all proofs use take functions instead
huffman
parents:
35444
diff
changeset

176 
thm tree.reach 
35781
b7738ab762b1
renamed some lemmas generated by the domain package
huffman
parents:
35661
diff
changeset

177 
thm tree.finite_induct 
30920
811ab0923a62
add HOLCF/ex/Domain_ex.thy, with example uses of the domain package
huffman
parents:
diff
changeset

178 

811ab0923a62
add HOLCF/ex/Domain_ex.thy, with example uses of the domain package
huffman
parents:
diff
changeset

179 
text {* Rules about finiteness predicate *} 
811ab0923a62
add HOLCF/ex/Domain_ex.thy, with example uses of the domain package
huffman
parents:
diff
changeset

180 
term tree_finite 
811ab0923a62
add HOLCF/ex/Domain_ex.thy, with example uses of the domain package
huffman
parents:
diff
changeset

181 
thm tree.finite_def 
35661
ede27eb8e94b
don't generate rule foo.finites for nonflat domains; use take_induct rule to prove induction rule
huffman
parents:
35642
diff
changeset

182 
thm tree.finite (* only generated for flat datatypes *) 
30920
811ab0923a62
add HOLCF/ex/Domain_ex.thy, with example uses of the domain package
huffman
parents:
diff
changeset

183 

811ab0923a62
add HOLCF/ex/Domain_ex.thy, with example uses of the domain package
huffman
parents:
diff
changeset

184 
text {* Rules about bisimulation predicate *} 
811ab0923a62
add HOLCF/ex/Domain_ex.thy, with example uses of the domain package
huffman
parents:
diff
changeset

185 
term tree_bisim 
811ab0923a62
add HOLCF/ex/Domain_ex.thy, with example uses of the domain package
huffman
parents:
diff
changeset

186 
thm tree.bisim_def 
35781
b7738ab762b1
renamed some lemmas generated by the domain package
huffman
parents:
35661
diff
changeset

187 
thm tree.coinduct 
30920
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 
text {* Induction rule *} 
35781
b7738ab762b1
renamed some lemmas generated by the domain package
huffman
parents:
35661
diff
changeset

190 
thm tree.induct 
30920
811ab0923a62
add HOLCF/ex/Domain_ex.thy, with example uses of the domain package
huffman
parents:
diff
changeset

191 

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 
subsection {* Known bugs *} 
811ab0923a62
add HOLCF/ex/Domain_ex.thy, with example uses of the domain package
huffman
parents:
diff
changeset

194 

811ab0923a62
add HOLCF/ex/Domain_ex.thy, with example uses of the domain package
huffman
parents:
diff
changeset

195 
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

196 
(* 
811ab0923a62
add HOLCF/ex/Domain_ex.thy, with example uses of the domain package
huffman
parents:
diff
changeset

197 
domain xx = xx ("x y") 
811ab0923a62
add HOLCF/ex/Domain_ex.thy, with example uses of the domain package
huffman
parents:
diff
changeset

198 
 "Inner syntax error: unexpected end of input" 
30922  199 
*) 
200 

30920
811ab0923a62
add HOLCF/ex/Domain_ex.thy, with example uses of the domain package
huffman
parents:
diff
changeset

201 
end 