1 (* Title: HOLCF/Tools/Domain/domain_theorems.ML |
1 (* Title: HOLCF/Tools/Domain/domain_theorems.ML |
2 Author: David von Oheimb |
2 Author: David von Oheimb |
3 New proofs/tactics by Brian Huffman |
3 Author: Brian Huffman |
4 |
4 |
5 Proof generator for domain command. |
5 Proof generator for domain command. |
6 *) |
6 *) |
7 |
7 |
8 val HOLCF_ss = @{simpset}; |
8 val HOLCF_ss = @{simpset}; |
9 |
9 |
10 signature DOMAIN_THEOREMS = |
10 signature DOMAIN_THEOREMS = |
11 sig |
11 sig |
12 val theorems: Domain_Library.eq * Domain_Library.eq list -> theory -> thm list * theory; |
12 val theorems: Domain_Library.eq * Domain_Library.eq list -> theory -> thm list * theory; |
13 val comp_theorems: bstring * Domain_Library.eq list -> theory -> thm list * theory; |
13 val comp_theorems: bstring * Domain_Library.eq list -> theory -> thm list * theory; |
14 val quiet_mode: bool ref; |
14 val quiet_mode: bool Unsynchronized.ref; |
15 val trace_domain: bool ref; |
15 val trace_domain: bool Unsynchronized.ref; |
16 end; |
16 end; |
17 |
17 |
18 structure Domain_Theorems :> DOMAIN_THEOREMS = |
18 structure Domain_Theorems :> DOMAIN_THEOREMS = |
19 struct |
19 struct |
20 |
20 |
21 val quiet_mode = ref false; |
21 val quiet_mode = Unsynchronized.ref false; |
22 val trace_domain = ref false; |
22 val trace_domain = Unsynchronized.ref false; |
23 |
23 |
24 fun message s = if !quiet_mode then () else writeln s; |
24 fun message s = if !quiet_mode then () else writeln s; |
25 fun trace s = if !trace_domain then tracing s else (); |
25 fun trace s = if !trace_domain then tracing s else (); |
26 |
26 |
27 local |
27 local |