-
Notifications
You must be signed in to change notification settings - Fork 0
/
string_prover.ml
70 lines (51 loc) · 2.51 KB
/
string_prover.ml
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
open Kernel
(****************************)
(* Printing functions *)
(****************************)
let rec string_of_term alpha_str = function
| Var v -> alpha_str v
| Fun (f, args) -> if List.length args = 0 then alpha_str f else
alpha_str f ^ "(" ^ (String.concat "," (List.map (string_of_term alpha_str) args)) ^ ")"
let rec string_of_formula alpha_str = function
| BOT -> "F"
| Atom (a, args) -> if List.length args = 0 then alpha_str a else
alpha_str a ^ "(" ^ (String.concat "," (List.map (string_of_term alpha_str) args)) ^ ")"
| Neg fm -> "~"^ string_of_formula alpha_str fm
| Disj (a, b) -> string_of_formula alpha_str a ^ " \\/ " ^ string_of_formula alpha_str b
| Conj (a, b) -> string_of_formula alpha_str a ^ " /\\ " ^ string_of_formula alpha_str b
| Imp (a, b) -> string_of_formula alpha_str a ^ " --> " ^ string_of_formula alpha_str b
| Exists (w, fm) -> "?" ^ alpha_str w ^ ". " ^ string_of_formula alpha_str fm
| Forall (w, fm) -> "!" ^ alpha_str w ^ ". " ^ string_of_formula alpha_str fm
let string_of_theorem alpha_str ((fms, c):'a theorem) =
let assms = if List.length fms = 0 then "" else (String.concat "," (List.map (string_of_formula alpha_str) fms)) in
let concl = string_of_formula alpha_str c in
"{ " ^ assms ^ " } |- " ^ concl
let print_theorem alpha_str thm = print_string (string_of_theorem alpha_str thm)
let default_print_theorem thm = print_theorem (fun x -> x) thm; print_newline()
(****************************)
(* Theorems *)
(****************************)
(* !x. P(x) --> P(x) *)
let thm_IMP_REFL =
let l1 = trivial (Atom ("p", [Var "x"])) in
let l2 = deduction_thm1 l1 in
all_intro l2 "x"
let _ = default_print_theorem thm_IMP_REFL
(****************************)
(* Tactics *)
(****************************)
(** Given a Theorem that has a toplevel double negation we return the theorem without double negation **)
let tactic_NNEG_ELIM (a1, (Neg (Neg fm)))=
let (a2, Disj (a, b)) = lem fm in
let b1 = conj_elim2 @@ conj_intro (trivial fm) (assume a (true_introduction)) in
let l1 = assume b (true_introduction) in
let l2 = neg_elim (a1, (Neg (Neg fm))) in
let l3 = deduction_thm1 l1 in
let l4 = modus_ponens l2 l3 in
let b2 = bottom_elim l4 fm in
print_theorem (fun x -> x) b1; print_newline();
print_theorem (fun x -> x) b2; print_newline();
disj_elim_cases (a2, Disj (a, b)) b1 b2
(****************************)
(* More Theorems *)
(****************************)