blob: 5e6aa09fae55afc524a8a24bd7c49e7257d6dec3 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
|
(*Generated by Lem from bool.lem.*)
open HolKernel Parse boolLib bossLib;
val _ = numLib.prefer_num();
val _ = new_theory "lem_bool"
(* The type bool is hard-coded, so are true and false *)
(* ----------------------- *)
(* not *)
(* ----------------------- *)
(*val not : bool -> bool*)
(*let not b= match b with
| true -> false
| false -> true
end*)
(* ----------------------- *)
(* and *)
(* ----------------------- *)
(*val && [and] : bool -> bool -> bool*)
(*let && b1 b2= match (b1, b2) with
| (true, true) -> true
| _ -> false
end*)
(* ----------------------- *)
(* or *)
(* ----------------------- *)
(*val || [or] : bool -> bool -> bool*)
(*let || b1 b2= match (b1, b2) with
| (false, false) -> false
| _ -> true
end*)
(* ----------------------- *)
(* implication *)
(* ----------------------- *)
(*val --> [imp] : bool -> bool -> bool*)
(*let --> b1 b2= match (b1, b2) with
| (true, false) -> false
| _ -> true
end*)
(* ----------------------- *)
(* equivalence *)
(* ----------------------- *)
(*val <-> [equiv] : bool -> bool -> bool*)
(*let <-> b1 b2= match (b1, b2) with
| (true, true) -> true
| (false, false) -> true
| _ -> false
end*)
(* ----------------------- *)
(* xor *)
(* ----------------------- *)
(*val xor : bool -> bool -> bool*)
val _ = export_theory()
|
