author | wenzelm |
Tue, 29 Mar 2011 17:47:11 +0200 | |
changeset 42151 | 4da4fc77664b |
parent 41292 | 2b7bc8d9fd6e |
child 58880 | 0baae4311a9f |
permissions | -rw-r--r-- |
42151 | 1 |
(* Title: HOL/HOLCF/Library/Char_Discrete.thy |
41112
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
2 |
Author: Brian Huffman |
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
3 |
*) |
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
4 |
|
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
5 |
header {* Discrete cpo instance for 8-bit char type *} |
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
6 |
|
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
7 |
theory Char_Discrete |
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
8 |
imports HOLCF |
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
9 |
begin |
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
10 |
|
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
11 |
subsection {* Discrete cpo instance for @{typ nibble}. *} |
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
12 |
|
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
13 |
instantiation nibble :: discrete_cpo |
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
14 |
begin |
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
15 |
|
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
16 |
definition below_nibble_def: |
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
17 |
"(x::nibble) \<sqsubseteq> y \<longleftrightarrow> x = y" |
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
18 |
|
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
19 |
instance proof |
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
20 |
qed (rule below_nibble_def) |
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
21 |
|
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
22 |
end |
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
23 |
|
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
24 |
text {* |
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
25 |
TODO: implement a command to automate discrete predomain instances. |
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
26 |
*} |
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
27 |
|
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
28 |
instantiation nibble :: predomain |
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
29 |
begin |
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
30 |
|
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
31 |
definition |
41292
2b7bc8d9fd6e
use deflations over type 'udom u' to represent predomains;
huffman
parents:
41112
diff
changeset
|
32 |
"(liftemb :: nibble u \<rightarrow> udom u) \<equiv> liftemb oo u_map\<cdot>(\<Lambda> x. Discr x)" |
41112
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
33 |
|
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
34 |
definition |
41292
2b7bc8d9fd6e
use deflations over type 'udom u' to represent predomains;
huffman
parents:
41112
diff
changeset
|
35 |
"(liftprj :: udom u \<rightarrow> nibble u) \<equiv> u_map\<cdot>(\<Lambda> y. undiscr y) oo liftprj" |
41112
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
36 |
|
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
37 |
definition |
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
38 |
"liftdefl \<equiv> (\<lambda>(t::nibble itself). LIFTDEFL(nibble discr))" |
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
39 |
|
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
40 |
instance proof |
41292
2b7bc8d9fd6e
use deflations over type 'udom u' to represent predomains;
huffman
parents:
41112
diff
changeset
|
41 |
show "ep_pair liftemb (liftprj :: udom u \<rightarrow> nibble u)" |
41112
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
42 |
unfolding liftemb_nibble_def liftprj_nibble_def |
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
43 |
apply (rule ep_pair_comp) |
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
44 |
apply (rule ep_pair_u_map) |
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
45 |
apply (simp add: ep_pair.intro) |
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
46 |
apply (rule predomain_ep) |
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
47 |
done |
41292
2b7bc8d9fd6e
use deflations over type 'udom u' to represent predomains;
huffman
parents:
41112
diff
changeset
|
48 |
show "cast\<cdot>LIFTDEFL(nibble) = liftemb oo (liftprj :: udom u \<rightarrow> nibble u)" |
41112
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
49 |
unfolding liftemb_nibble_def liftprj_nibble_def liftdefl_nibble_def |
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
50 |
apply (simp add: cast_liftdefl cfcomp1 u_map_map) |
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
51 |
apply (simp add: ID_def [symmetric] u_map_ID) |
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
52 |
done |
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
53 |
qed |
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
54 |
|
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
55 |
end |
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
56 |
|
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
57 |
subsection {* Discrete cpo instance for @{typ char}. *} |
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
58 |
|
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
59 |
instantiation char :: discrete_cpo |
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
60 |
begin |
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
61 |
|
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
62 |
definition below_char_def: |
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
63 |
"(x::char) \<sqsubseteq> y \<longleftrightarrow> x = y" |
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
64 |
|
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
65 |
instance proof |
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
66 |
qed (rule below_char_def) |
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
67 |
|
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
68 |
end |
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
69 |
|
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
70 |
text {* |
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
71 |
TODO: implement a command to automate discrete predomain instances. |
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
72 |
*} |
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
73 |
|
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
74 |
instantiation char :: predomain |
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
75 |
begin |
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
76 |
|
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
77 |
definition |
41292
2b7bc8d9fd6e
use deflations over type 'udom u' to represent predomains;
huffman
parents:
41112
diff
changeset
|
78 |
"(liftemb :: char u \<rightarrow> udom u) \<equiv> liftemb oo u_map\<cdot>(\<Lambda> x. Discr x)" |
41112
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
79 |
|
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
80 |
definition |
41292
2b7bc8d9fd6e
use deflations over type 'udom u' to represent predomains;
huffman
parents:
41112
diff
changeset
|
81 |
"(liftprj :: udom u \<rightarrow> char u) \<equiv> u_map\<cdot>(\<Lambda> y. undiscr y) oo liftprj" |
41112
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
82 |
|
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
83 |
definition |
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
84 |
"liftdefl \<equiv> (\<lambda>(t::char itself). LIFTDEFL(char discr))" |
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
85 |
|
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
86 |
instance proof |
41292
2b7bc8d9fd6e
use deflations over type 'udom u' to represent predomains;
huffman
parents:
41112
diff
changeset
|
87 |
show "ep_pair liftemb (liftprj :: udom u \<rightarrow> char u)" |
41112
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
88 |
unfolding liftemb_char_def liftprj_char_def |
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
89 |
apply (rule ep_pair_comp) |
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
90 |
apply (rule ep_pair_u_map) |
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
91 |
apply (simp add: ep_pair.intro) |
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
92 |
apply (rule predomain_ep) |
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
93 |
done |
41292
2b7bc8d9fd6e
use deflations over type 'udom u' to represent predomains;
huffman
parents:
41112
diff
changeset
|
94 |
show "cast\<cdot>LIFTDEFL(char) = liftemb oo (liftprj :: udom u \<rightarrow> char u)" |
41112
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
95 |
unfolding liftemb_char_def liftprj_char_def liftdefl_char_def |
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
96 |
apply (simp add: cast_liftdefl cfcomp1 u_map_map) |
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
97 |
apply (simp add: ID_def [symmetric] u_map_ID) |
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
98 |
done |
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
99 |
qed |
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
100 |
|
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
101 |
end |
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
102 |
|
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
103 |
subsection {* Using chars with Fixrec *} |
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
104 |
|
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
105 |
definition match_Char :: "char \<rightarrow> (nibble \<rightarrow> nibble \<rightarrow> 'a match) \<rightarrow> 'a match" |
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
106 |
where "match_Char = (\<Lambda> c k. case c of Char a b \<Rightarrow> k\<cdot>a\<cdot>b)" |
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
107 |
|
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
108 |
lemma match_Char_simps [simp]: |
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
109 |
"match_Char\<cdot>(Char a b)\<cdot>k = k\<cdot>a\<cdot>b" |
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
110 |
by (simp add: match_Char_def) |
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
111 |
|
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
112 |
definition match_Nibble0 :: "nibble \<rightarrow> 'a match \<rightarrow> 'a match" |
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
113 |
where "match_Nibble0 = (\<Lambda> c k. if c = Nibble0 then k else Fixrec.fail)" |
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
114 |
|
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
115 |
definition match_Nibble1 :: "nibble \<rightarrow> 'a match \<rightarrow> 'a match" |
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
116 |
where "match_Nibble1 = (\<Lambda> c k. if c = Nibble1 then k else Fixrec.fail)" |
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
117 |
|
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
118 |
definition match_Nibble2 :: "nibble \<rightarrow> 'a match \<rightarrow> 'a match" |
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
119 |
where "match_Nibble2 = (\<Lambda> c k. if c = Nibble2 then k else Fixrec.fail)" |
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
120 |
|
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
121 |
definition match_Nibble3 :: "nibble \<rightarrow> 'a match \<rightarrow> 'a match" |
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
122 |
where "match_Nibble3 = (\<Lambda> c k. if c = Nibble3 then k else Fixrec.fail)" |
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
123 |
|
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
124 |
definition match_Nibble4 :: "nibble \<rightarrow> 'a match \<rightarrow> 'a match" |
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
125 |
where "match_Nibble4 = (\<Lambda> c k. if c = Nibble4 then k else Fixrec.fail)" |
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
126 |
|
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
127 |
definition match_Nibble5 :: "nibble \<rightarrow> 'a match \<rightarrow> 'a match" |
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
128 |
where "match_Nibble5 = (\<Lambda> c k. if c = Nibble5 then k else Fixrec.fail)" |
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
129 |
|
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
130 |
definition match_Nibble6 :: "nibble \<rightarrow> 'a match \<rightarrow> 'a match" |
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
131 |
where "match_Nibble6 = (\<Lambda> c k. if c = Nibble6 then k else Fixrec.fail)" |
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
132 |
|
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
133 |
definition match_Nibble7 :: "nibble \<rightarrow> 'a match \<rightarrow> 'a match" |
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
134 |
where "match_Nibble7 = (\<Lambda> c k. if c = Nibble7 then k else Fixrec.fail)" |
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
135 |
|
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
136 |
definition match_Nibble8 :: "nibble \<rightarrow> 'a match \<rightarrow> 'a match" |
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
137 |
where "match_Nibble8 = (\<Lambda> c k. if c = Nibble8 then k else Fixrec.fail)" |
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
138 |
|
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
139 |
definition match_Nibble9 :: "nibble \<rightarrow> 'a match \<rightarrow> 'a match" |
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
140 |
where "match_Nibble9 = (\<Lambda> c k. if c = Nibble9 then k else Fixrec.fail)" |
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
141 |
|
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
142 |
definition match_NibbleA :: "nibble \<rightarrow> 'a match \<rightarrow> 'a match" |
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
143 |
where "match_NibbleA = (\<Lambda> c k. if c = NibbleA then k else Fixrec.fail)" |
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
144 |
|
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
145 |
definition match_NibbleB :: "nibble \<rightarrow> 'a match \<rightarrow> 'a match" |
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
146 |
where "match_NibbleB = (\<Lambda> c k. if c = NibbleB then k else Fixrec.fail)" |
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
147 |
|
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
148 |
definition match_NibbleC :: "nibble \<rightarrow> 'a match \<rightarrow> 'a match" |
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
149 |
where "match_NibbleC = (\<Lambda> c k. if c = NibbleC then k else Fixrec.fail)" |
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
150 |
|
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
151 |
definition match_NibbleD :: "nibble \<rightarrow> 'a match \<rightarrow> 'a match" |
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
152 |
where "match_NibbleD = (\<Lambda> c k. if c = NibbleD then k else Fixrec.fail)" |
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
153 |
|
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
154 |
definition match_NibbleE :: "nibble \<rightarrow> 'a match \<rightarrow> 'a match" |
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
155 |
where "match_NibbleE = (\<Lambda> c k. if c = NibbleE then k else Fixrec.fail)" |
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
156 |
|
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
157 |
definition match_NibbleF :: "nibble \<rightarrow> 'a match \<rightarrow> 'a match" |
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
158 |
where "match_NibbleF = (\<Lambda> c k. if c = NibbleF then k else Fixrec.fail)" |
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
159 |
|
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
160 |
lemma match_Nibble0_simps [simp]: |
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
161 |
"match_Nibble0\<cdot>c\<cdot>k = (if c = Nibble0 then k else Fixrec.fail)" |
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
162 |
by (simp add: match_Nibble0_def) |
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
163 |
|
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
164 |
lemma match_Nibble1_simps [simp]: |
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
165 |
"match_Nibble1\<cdot>c\<cdot>k = (if c = Nibble1 then k else Fixrec.fail)" |
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
166 |
by (simp add: match_Nibble1_def) |
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
167 |
|
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
168 |
lemma match_Nibble2_simps [simp]: |
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
169 |
"match_Nibble2\<cdot>c\<cdot>k = (if c = Nibble2 then k else Fixrec.fail)" |
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
170 |
by (simp add: match_Nibble2_def) |
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
171 |
|
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
172 |
lemma match_Nibble3_simps [simp]: |
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
173 |
"match_Nibble3\<cdot>c\<cdot>k = (if c = Nibble3 then k else Fixrec.fail)" |
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
174 |
by (simp add: match_Nibble3_def) |
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
175 |
|
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
176 |
lemma match_Nibble4_simps [simp]: |
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
177 |
"match_Nibble4\<cdot>c\<cdot>k = (if c = Nibble4 then k else Fixrec.fail)" |
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
178 |
by (simp add: match_Nibble4_def) |
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
179 |
|
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
180 |
lemma match_Nibble5_simps [simp]: |
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
181 |
"match_Nibble5\<cdot>c\<cdot>k = (if c = Nibble5 then k else Fixrec.fail)" |
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
182 |
by (simp add: match_Nibble5_def) |
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
183 |
|
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
184 |
lemma match_Nibble6_simps [simp]: |
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
185 |
"match_Nibble6\<cdot>c\<cdot>k = (if c = Nibble6 then k else Fixrec.fail)" |
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
186 |
by (simp add: match_Nibble6_def) |
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
187 |
|
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
188 |
lemma match_Nibble7_simps [simp]: |
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
189 |
"match_Nibble7\<cdot>c\<cdot>k = (if c = Nibble7 then k else Fixrec.fail)" |
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
190 |
by (simp add: match_Nibble7_def) |
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
191 |
|
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
192 |
lemma match_Nibble8_simps [simp]: |
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
193 |
"match_Nibble8\<cdot>c\<cdot>k = (if c = Nibble8 then k else Fixrec.fail)" |
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
194 |
by (simp add: match_Nibble8_def) |
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
195 |
|
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
196 |
lemma match_Nibble9_simps [simp]: |
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
197 |
"match_Nibble9\<cdot>c\<cdot>k = (if c = Nibble9 then k else Fixrec.fail)" |
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
198 |
by (simp add: match_Nibble9_def) |
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
199 |
|
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
200 |
lemma match_NibbleA_simps [simp]: |
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
201 |
"match_NibbleA\<cdot>c\<cdot>k = (if c = NibbleA then k else Fixrec.fail)" |
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
202 |
by (simp add: match_NibbleA_def) |
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
203 |
|
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
204 |
lemma match_NibbleB_simps [simp]: |
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
205 |
"match_NibbleB\<cdot>c\<cdot>k = (if c = NibbleB then k else Fixrec.fail)" |
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
206 |
by (simp add: match_NibbleB_def) |
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
207 |
|
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
208 |
lemma match_NibbleC_simps [simp]: |
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
209 |
"match_NibbleC\<cdot>c\<cdot>k = (if c = NibbleC then k else Fixrec.fail)" |
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
210 |
by (simp add: match_NibbleC_def) |
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
211 |
|
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
212 |
lemma match_NibbleD_simps [simp]: |
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
213 |
"match_NibbleD\<cdot>c\<cdot>k = (if c = NibbleD then k else Fixrec.fail)" |
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
214 |
by (simp add: match_NibbleD_def) |
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
215 |
|
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
216 |
lemma match_NibbleE_simps [simp]: |
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
217 |
"match_NibbleE\<cdot>c\<cdot>k = (if c = NibbleE then k else Fixrec.fail)" |
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
218 |
by (simp add: match_NibbleE_def) |
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
219 |
|
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
220 |
lemma match_NibbleF_simps [simp]: |
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
221 |
"match_NibbleF\<cdot>c\<cdot>k = (if c = NibbleF then k else Fixrec.fail)" |
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
222 |
by (simp add: match_NibbleF_def) |
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
223 |
|
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
224 |
setup {* |
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
225 |
Fixrec.add_matchers |
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
226 |
[ (@{const_name Char}, @{const_name match_Char}), |
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
227 |
(@{const_name Nibble0}, @{const_name match_Nibble0}), |
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
228 |
(@{const_name Nibble1}, @{const_name match_Nibble1}), |
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
229 |
(@{const_name Nibble2}, @{const_name match_Nibble2}), |
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
230 |
(@{const_name Nibble3}, @{const_name match_Nibble3}), |
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
231 |
(@{const_name Nibble4}, @{const_name match_Nibble4}), |
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
232 |
(@{const_name Nibble5}, @{const_name match_Nibble5}), |
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
233 |
(@{const_name Nibble6}, @{const_name match_Nibble6}), |
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
234 |
(@{const_name Nibble7}, @{const_name match_Nibble7}), |
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
235 |
(@{const_name Nibble8}, @{const_name match_Nibble8}), |
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
236 |
(@{const_name Nibble9}, @{const_name match_Nibble9}), |
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
237 |
(@{const_name NibbleA}, @{const_name match_NibbleA}), |
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
238 |
(@{const_name NibbleB}, @{const_name match_NibbleB}), |
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
239 |
(@{const_name NibbleC}, @{const_name match_NibbleC}), |
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
240 |
(@{const_name NibbleD}, @{const_name match_NibbleD}), |
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
241 |
(@{const_name NibbleE}, @{const_name match_NibbleE}), |
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
242 |
(@{const_name NibbleF}, @{const_name match_NibbleF}) ] |
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
243 |
*} |
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
244 |
|
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
245 |
end |