author  huffman 
Tue, 02 Mar 2010 00:34:26 0800  
changeset 35494  45c9a8278faf 
parent 35444  73f645fdd4ff 
child 35497  979706bd5c16 
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 
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 previouslydefined 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 {* 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

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 {* Nonregular 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 
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

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 sidecondition. *} 
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  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  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  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  209 
text {* Declaring class constraints on the LHS is currently broken. *} 
210 
(* 

211 
domain ('a::cpo) box = Box (lazy 'a) 

212 
 "Malformed YXML encoding: multiple results" 

213 
*) 

214 

215 
text {* 

216 
Class constraints on the RHS are not supported yet. This feature is 

217 
planned to replace the oldstyle LHS class constraints. 

218 
*} 

219 
(* 

220 
domain 'a box = Box (lazy "'a::cpo") 

221 
 {* Inconsistent sort constraint for type variable "'a" *} 

222 
*) 

223 

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

224 
end 