blob: 2c939fdec531f29895cb39cdded3639062c0754a (
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
76
77
78
79
80
81
82
83
84
85
|
open Logic
type context = (string * formula) list
type goalDesc = context * formula
type proof
type goal
(** Zamienia ukończony dowód na twierdzenie *)
val qed : proof -> theorem
(** Zwraca liczbę pozostałych w dowodze celów (0 <-> dowód jest gotowy i można go zakończyć) *)
val numGoals : proof -> int
(** Zwraca listę celów w danym dowodzie *)
val goals : proof -> goalDesc list
(** Tworzy pusty dowód podanego twierdzenia *)
val proof : context -> formula -> proof
(** Zwraca (assm, phi), gdzie assm oraz phi to odpowiednio dostępne
założenia oraz formuła do udowodnienia w aktywnym podcelu *)
val goal : goal -> goalDesc
(** Ustawia aktywny cel w danym dowodzie *)
val focus : int -> proof -> goal
(** Zapomina informację o celu *)
val unfocus : goal -> proof
(** Zmienia (cyklicznie) aktywny cel na następny/poprzedni *)
val next : goal -> goal
val prev : goal -> goal
(** Wywołanie intro name pf odpowiada regule wprowadzania implikacji.
To znaczy aktywna dziura wypełniana jest regułą:
(nowy aktywny cel)
(name,ψ) :: Γ ⊢ φ
-----------------(→I)
Γ ⊢ ψ → φ
Jeśli aktywny cel nie jest implikacją, wywołanie kończy się błędem *)
val intro : string -> goal -> goal
(** Wywołanie apply ψ₀ pf odpowiada jednocześnie eliminacji implikacji
i eliminacji fałszu. Tzn. jeśli do udowodnienia jest φ, a ψ₀ jest
postaci ψ₁ → ... → ψn → φ to aktywna dziura wypełniana jest regułami
(nowy aktywny cel) (nowy cel)
Γ ⊢ ψ₀ Γ ⊢ ψ₁
----------------------(→E) (nowy cel)
... Γ ⊢ ψn
----------------------------(→E)
Γ ⊢ φ
Natomiast jeśli ψ₀ jest postaci ψ₁ → ... → ψn → ⊥ to aktywna dziura
wypełniana jest regułami
(nowy aktywny cel) (nowy cel)
Γ ⊢ ψ₀ Γ ⊢ ψ₁
----------------------(→E) (nowy cel)
... Γ ⊢ ψn
----------------------------(→E)
Γ ⊢ ⊥
-----(⊥E)
Γ ⊢ φ *)
val apply : formula -> goal -> goal
(** Wywołanie `apply_thm thm pf` działa podobnie do
`apply (Logic.consequence thm) pf`, tyle że aktywna dziura od razu
jest wypełniana dowodem thm, a otrzymane drzewo nie jest
sfokusowane na żadnym z celów.
*)
val apply_thm : theorem -> goal -> proof
(** Wywołanie `apply_assm name pf` działa tak jak
`apply (Logic.by_assumption f) pf`, gdzie f jest założeniem o
nazwie name
*)
val apply_assm : string -> goal -> proof
val pp_print_proof : Format.formatter -> proof -> unit
val pp_print_goal : Format.formatter -> goal -> unit
|
