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
|
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 (Imp (Var "p", 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)))
|
