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
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
|
(* type formula = False | Var of string | Imp of formula * formula
let rec string_of_formula = function
| False -> "F"
| Var s -> s
| Imp (f1, f2) -> "(" ^ (string_of_formula f1) ^ " -> " ^ (string_of_formula f2) ^ ")"
(* match (f1, f2) with
| (Var v1, Var v2) -> (string_of_formula f1) ^ " -> " ^ (string_of_formula f2)
| (Var v1, False) | (False, Var v1) -> (string_of_formula f1) ^ " -> " ^ (string_of_formula f2)
| (False, False) -> (string_of_formula f1) ^ " -> " ^ (string_of_formula f2)
| (f1, f2) -> "(" ^ (string_of_formula f1) ^ " -> " ^ (string_of_formula f2) ^ ")" *)
let pp_print_formula fmtr f =
Format.pp_print_string fmtr (string_of_formula f)
type verdict = { assump : formula list; concl : formula }
type theorem =
| Assumption of verdict
| ImpInsert of verdict * theorem
| ImpErase of verdict * theorem * theorem
| Contradiction of verdict * theorem
let get_verdict thm = match thm with
| Assumption f -> f
| ImpInsert (v, _) | ImpErase (v, _, _) | Contradiction (v, _) -> v
let assumptions thm = (get_verdict thm).assump
let consequence thm = (get_verdict thm).concl
let pp_print_theorem fmtr thm =
let open Format in
pp_open_hvbox fmtr 2;
begin match assumptions thm with
| [] -> ()
| f :: fs ->
pp_print_formula fmtr f;
fs |> List.iter (fun f ->
pp_print_string fmtr ",";
pp_print_space fmtr ();
pp_print_formula fmtr f);
pp_print_space fmtr ()
end;
pp_open_hbox fmtr ();
pp_print_string fmtr "⊢";
pp_print_space fmtr ();
pp_print_formula fmtr (consequence thm);
pp_close_box fmtr ();
pp_close_box fmtr ()
let by_assumption f =
Assumption { assump=[f]; concl=f }
let imp_i f thm =
let premise = get_verdict thm
in ImpInsert ({assump=(List.filter ((<>) f) premise.assump); concl=(Imp (f, premise.concl))}, thm)
let imp_e th1 th2 =
let premise1 = get_verdict th1 in
let premise2 = get_verdict th2 in
match premise1.concl with
| False | Var _ -> failwith "th1 conclusion is not implication"
| Imp (phi, psi) -> if phi <> premise2.concl then failwith "th1 conclusion's premise is not th2 premise conclusion" else
ImpErase ({assump=(premise1.assump @ premise2.assump); concl=(psi)}, th1, th2)
let bot_e f thm =
match get_verdict thm with
| {assump=ass; concl=False}-> (Contradiction ({assump=ass; concl=f}, thm))
| _ -> failwith "thm conclusion is not False"
let taut = (imp_i (Var "p") (by_assumption (Var "p")))
let taut2 = (imp_i (Var "p") (imp_i (Var "q") (by_assumption (Var "p"))))
let imppqr = Imp (Var "p", Imp (Var "q", Var "r"))
let imppq = Imp (Var "p", Var "q")
let imppr = Imp (Var "p", Var "r")
let taut3 = (imp_i (imppqr) (imp_i imppq (by_assumption imppr))) *)
type formula = False | Var of string | Imp of formula * formula
let rec string_of_formula f =
match f with
False -> "⊥"
| Var str -> str
| Imp (f1, f2) -> let str1 = string_of_formula f1 in
(match f1 with
Imp (_, _) -> "(" ^ str1 ^ ")"
| _ -> str1) ^ " ⇒ " ^ string_of_formula f2
;;
(* match (f1, f2) with
| (Var v1, Var v2) -> (string_of_formula f1) ^ " -> " ^ (string_of_formula f2)
| (Var v1, False) | (False, Var v1) -> (string_of_formula f1) ^ " -> " ^ (string_of_formula f2)
| (False, False) -> (string_of_formula f1) ^ " -> " ^ (string_of_formula f2)
| (f1, f2) -> "(" ^ (string_of_formula f1) ^ " -> " ^ (string_of_formula f2) ^ ")" *)
let pp_print_formula fmtr f =
Format.pp_print_string fmtr (string_of_formula f)
type theorem = { assump : formula list; concl : formula }
let assumptions thm = thm.assump
let consequence thm = thm.concl
let pp_print_theorem fmtr thm =
let open Format in
pp_open_hvbox fmtr 2;
begin match assumptions thm with
| [] -> ()
| f :: fs ->
pp_print_formula fmtr f;
fs |> List.iter (fun f ->
pp_print_string fmtr ",";
pp_print_space fmtr ();
pp_print_formula fmtr f);
pp_print_space fmtr ()
end;
pp_open_hbox fmtr ();
pp_print_string fmtr "⊢";
pp_print_space fmtr ();
pp_print_formula fmtr (consequence thm);
pp_close_box fmtr ();
pp_close_box fmtr ()
let by_assumption f =
{ assump=[f]; concl=f }
let imp_i f thm =
{ assump=(List.filter ((<>) f) thm.assump); concl=(Imp (f, thm.concl)) }
let imp_e th1 th2 =
match th1.concl with
| False | Var _ -> failwith "th1 conclusion is not implication"
| Imp (phi, psi) -> if phi <> th2.concl then failwith "th1 conclusion's premise is not th2 premise conclusion" else
{ assump = th1.assump @ th2.assump; concl = psi}
let bot_e f thm =
match thm with
| {assump=ass; concl=False} -> {assump=ass; concl=f}
| _ -> failwith "thm conclusion is not False"
|
