blob: 3de1b91b7173764dd8e6680a2de5772db176cec2 (
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
86
87
88
89
90
|
--# -path=.:prelude
concrete ProofSymb of Proof = FormulaSymb ** open Prelude, Precedence in {
flags startcat=Text ; unlexer=text ; lexer = text ;
lincat
Text, Proof = {s : Str} ;
[Formula] = {s : Str ; isnil : Bool} ;
lin
Start prems concl = continue [] (task prems.s concl.s) ;
Hypo = finish "Hypothesis" "Ø" ;
Implic prems concl = continue ["Implication strategy"] (task prems.s concl.s) ;
RedAbs form = continue ["Reductio ad absurdum"] (task neg abs)
where { neg = useTop (prefixR 4 "~" form) } ;
ExFalso form = finish (["Ex falso quodlibet"] ++ toProve form) "Ø" ; --- form
ConjSplit a b c =
continue ["Conjunction split"]
(task (useTop a ++ "," ++ useTop b) (useTop c)) ;
ModPon prems concl = continue ["Modus ponens"] (task prems.s concl.s) ;
Forget prems concl = continue "Forgetting" (task prems.s concl.s) ;
--
DeMorgan1 = \form, concl ->
continue ["de Morgan 1"] (task form.s concl.s) ;
DeMorgan2 = \form, concl ->
continue ["de Morgan 2"] (task form.s concl.s) ;
ImplicNeg forms concl =
continue ["Implication negation"] (task forms.s concl.s) ;
NegRewrite form forms =
let
neg = useTop (prefixR 4 "~" form) ;
impl = useTop (infixR 1 "->" form (constant "_|_")) ;
in
continue ["Negation rewrite"] (task forms.s impl) ;
--
BaseFormula = {
s = [] ;
isnil = True
} ;
ConsFormula f fs = {
s = useTop f ++ ifNotNil (\p -> "," ++ p) fs ;
isnil = False
} ;
oper
ifNotNil : (Str -> Str) -> {s : Str ; isnil : Bool} -> Str = \cons,prems ->
case prems.isnil of {
True => prems.s ;
False => cons prems.s
} ;
continue : Str -> Str -> {s : Str} -> {s : Str} = \label,task,proof -> {
s = label ++ new ++ task ++ new ++ line ++ proof.s
} ;
finish : Str -> Str -> {s : Str} = \label,task -> {
s = label ++ new ++ task
} ;
task : Str -> Str -> Str = \prems,concl ->
"[" ++ prems ++ "|-" ++ concl ++ "]" ;
new = variants {"&-" ; []} ; -- unlexing and parsing, respectively
line = "------------------------------" ;
abs = "_|_" ;
toProve : PrecExp -> Str = \c ->
variants {
[] ; -- for generation
useTop c -- for parsing
} ;
}
|
