From 35daecebcd3d2b251ec3bea284248fbcd0af2af1 Mon Sep 17 00:00:00 2001 From: aarne Date: Tue, 20 Dec 2005 14:20:42 +0000 Subject: [PATCH] CS's system S --- examples/systemS/Formula.gf | 20 +++++ examples/systemS/FormulaSymb.gf | 22 ++++++ examples/systemS/Precedence.gf | 42 ++++++++++ examples/systemS/Proof.gf | 23 ++++++ examples/systemS/ProofEng.gf | 133 ++++++++++++++++++++++++++++++++ examples/systemS/ProofSymb.gf | 84 ++++++++++++++++++++ examples/systemS/README | 65 ++++++++++++++++ examples/systemS/ex1.txt | 8 ++ examples/systemS/ex1eng.txt | 4 + examples/systemS/ex2.txt | 13 ++++ examples/systemS/ex2eng.txt | 7 ++ examples/systemS/ex4.txt | 13 ++++ examples/systemS/ex4eng.txt | 8 ++ examples/systemS/proof.gfcm | 113 +++++++++++++++++++++++++++ examples/systemS/test.gfs | 7 ++ 15 files changed, 562 insertions(+) create mode 100644 examples/systemS/Formula.gf create mode 100644 examples/systemS/FormulaSymb.gf create mode 100644 examples/systemS/Precedence.gf create mode 100644 examples/systemS/Proof.gf create mode 100644 examples/systemS/ProofEng.gf create mode 100644 examples/systemS/ProofSymb.gf create mode 100644 examples/systemS/README create mode 100644 examples/systemS/ex1.txt create mode 100644 examples/systemS/ex1eng.txt create mode 100644 examples/systemS/ex2.txt create mode 100644 examples/systemS/ex2eng.txt create mode 100644 examples/systemS/ex4.txt create mode 100644 examples/systemS/ex4eng.txt create mode 100644 examples/systemS/proof.gfcm create mode 100644 examples/systemS/test.gfs diff --git a/examples/systemS/Formula.gf b/examples/systemS/Formula.gf new file mode 100644 index 000000000..62bc67eb7 --- /dev/null +++ b/examples/systemS/Formula.gf @@ -0,0 +1,20 @@ +-- 20 Dec 2005, 9.45 + +abstract Formula = { + + cat + Formula ; + Term ; + + fun + And, Or, If : (_,_ : Formula) -> Formula ; + Not : Formula -> Formula ; + Abs : Formula ; + +---- All, Exist : (Term -> Formula) -> Formula ; + + -- to test + + A, B, C : Formula ; + +} \ No newline at end of file diff --git a/examples/systemS/FormulaSymb.gf b/examples/systemS/FormulaSymb.gf new file mode 100644 index 000000000..5c2360673 --- /dev/null +++ b/examples/systemS/FormulaSymb.gf @@ -0,0 +1,22 @@ +--# -path=.:prelude + +concrete FormulaSymb of Formula = open Precedence in { + + lincat + Formula, Term = PrecExp ; + + lin + And = infixL 3 "&" ; + Or = infixL 2 "v" ; + If = infixR 1 "->" ; + Not = prefixR 4 "~" ; + Abs = constant "_|_" ; + +---- All P = mkPrec 4 PR (paren ("All" ++ P.$0) ++ usePrec P 4) ; +---- Exist P = mkPrec 4 PR (paren ("Ex" ++ P.$0) ++ usePrec P 4) ; + + A = constant "A" ; + B = constant "B" ; + C = constant "C" ; + +} \ No newline at end of file diff --git a/examples/systemS/Precedence.gf b/examples/systemS/Precedence.gf new file mode 100644 index 000000000..7defd19aa --- /dev/null +++ b/examples/systemS/Precedence.gf @@ -0,0 +1,42 @@ +resource Precedence = open (Predef = Predef) in { + + param + PAssoc = PN | PL | PR ; + + oper + Prec : PType = Predef.Ints 4 ; + PrecExp : Type = {s : Str ; p : Prec ; a : PAssoc} ; + + mkPrec : Prec -> PAssoc -> Str -> PrecExp = \p,a,f -> + {s = f ; p = p ; a = a} ; + + usePrec : PrecExp -> Prec -> Str = \x,p -> + case < : Prec * Prec> of { + <3,4> | <2,3> | <2,4> => paren x.s ; + <1,1> | <1,0> | <0,0> => x.s ; + <1,_> | <0,_> => paren x.s ; + _ => x.s + } ; + + useTop : PrecExp -> Str = \e -> usePrec e 0 ; + + constant : Str -> PrecExp = mkPrec 4 PN ; + + infixN : Prec -> Str -> (_,_ : PrecExp) -> PrecExp = \p,f,x,y -> + mkPrec p PN (usePrec x (nextPrec p) ++ f ++ usePrec y (nextPrec p)) ; + infixL : Prec -> Str -> (_,_ : PrecExp) -> PrecExp = \p,f,x,y -> + mkPrec p PL (usePrec x p ++ f ++ usePrec y (nextPrec p)) ; + infixR : Prec -> Str -> (_,_ : PrecExp) -> PrecExp = \p,f,x,y -> + mkPrec p PR (usePrec x (nextPrec p) ++ f ++ usePrec y p) ; + + prefixR : Prec -> Str -> PrecExp -> PrecExp = \p,f,x -> + mkPrec p PR (f ++ usePrec x p) ; + + nextPrec : Prec -> Prec = \p -> case

of { + 4 => 4 ; + n => Predef.plus n 1 + } ; + + paren : Str -> Str = \s -> "(" ++ s ++ ")" ; + +} diff --git a/examples/systemS/Proof.gf b/examples/systemS/Proof.gf new file mode 100644 index 000000000..06a6f1c68 --- /dev/null +++ b/examples/systemS/Proof.gf @@ -0,0 +1,23 @@ +abstract Proof = Formula ** { + + cat + Text ; + Proof ; + [Formula] ; + + fun + Start : [Formula] -> Formula -> Proof -> Text ; + + Hypo : Proof ; + Implic : [Formula] -> Formula -> Proof -> Proof ; + RedAbs : Formula -> Proof -> Proof ; + ExFalso : Formula -> Proof ; + ConjSplit : Formula -> Formula -> Formula -> Proof -> Proof ; + ModPon : [Formula] -> Formula -> Proof -> Proof ; + Forget : [Formula] -> Formula -> Proof -> Proof ; + + DeMorgan1, DeMorgan2 : Formula -> Formula -> Proof -> Proof ; + ImplicNeg : [Formula] -> Formula -> Proof -> Proof ; + NegRewrite : Formula -> [Formula] -> Proof -> Proof ; + +} diff --git a/examples/systemS/ProofEng.gf b/examples/systemS/ProofEng.gf new file mode 100644 index 000000000..612e228c8 --- /dev/null +++ b/examples/systemS/ProofEng.gf @@ -0,0 +1,133 @@ +--# -path=.:prelude + +concrete ProofEng 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 proof = { + s = ifNotNil (\p -> "Suppose" ++ p ++ ".") prems ++ + ["We will show that"] ++ useTop concl ++ "." ++ + proof.s + } ; + + Hypo = { + s = new ++ ["But this holds trivially ."] + } ; + + Implic prems concl proof = { + s = new ++ ["It is enough to"] ++ + ifNotNil (\p -> "assume" ++ p ++ "and") prems ++ + "show" ++ concl.s ++ + "." ++ + proof.s ; + } ; + + RedAbs form proof = + let neg = useTop (prefixR 4 "~" form) in { + s = new ++ ["To that end , we will assume"] ++ + neg ++ + ["and show"] ++ "_|_" ++ + "." ++ + new ++ ["So let us assume that"] ++ + neg ++ + "." ++ + proof.s + } ; + + ExFalso form = { + s = new ++ ["Hence we get"] ++ + useTop form ++ ["as desired"] ++ + "." + } ; + + ConjSplit a b c proof = { + s = new ++ ["So by splitting we get"] ++ + useTop a ++ "," ++ useTop b ++ + toProve c ++ + "." ++ + proof.s + } ; + + ModPon prems concl proof = { + s = new ++ ["Then , by Modus ponens , we get"] ++ prems.s ++ + toProve concl ++ + "." ++ + proof.s + } ; + + Forget prems concl proof = { + s = new ++ ["In particular we get"] ++ prems.s ++ + toProve concl ++ + "." ++ + proof.s + } ; + +-- + + DeMorgan1 = \form, concl, proof -> { + s = new ++ ["Then , by the first de Morgan's law , we get"] ++ useTop form ++ + toProve concl ++ + "." ++ + proof.s + } ; + + DeMorgan2 = \form, concl, proof -> { + s = new ++ ["Then , by the second de Morgan's law , we get"] ++ useTop form ++ + toProve concl ++ + "." ++ + proof.s + } ; + + ImplicNeg forms concl proof = { + s = new ++ ["By implication negation , we get"] ++ forms.s ++ + toProve concl ++ + "." ++ + proof.s + } ; + + NegRewrite form forms proof = + let + neg = useTop (prefixR 4 "~" form) ; + impl = useTop (infixR 1 "->" form (constant "_|_")) ; + in { + s = new ++ ["Thus , by rewriting"] ++ + neg ++ + ifNotNil (\p -> ["we may assume"] ++ p ++ "and") forms ++ + "show" ++ impl ++ + "." ++ + proof.s + } ; + +-- + + 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 + } ; + + new = variants {"&-" ; []} ; -- unlexing and parsing, respectively + + toProve : PrecExp -> Str = \c -> + variants { + [] ; -- for generation + ["to prove"] ++ useTop c -- for parsing + } ; + +} diff --git a/examples/systemS/ProofSymb.gf b/examples/systemS/ProofSymb.gf new file mode 100644 index 000000000..4ff18ca14 --- /dev/null +++ b/examples/systemS/ProofSymb.gf @@ -0,0 +1,84 @@ +--# -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"] ++ form.s) "Ø" ; --- 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 = "_|_" ; + +} \ No newline at end of file diff --git a/examples/systemS/README b/examples/systemS/README new file mode 100644 index 000000000..ebbd92ce6 --- /dev/null +++ b/examples/systemS/README @@ -0,0 +1,65 @@ +AR 20/12/2005 + +This is a translator of a part of the proof system +by Claes Strannegård, as defined in the manuscript +"Translating Formal Proofs into English". + +The functionality is to translate between a formal +and an informal notation for proofs. + +As examples, we provide 3 of the 4 examples in +Strannegård's paper. His example 3 is left as exercise. + +A good way to start is + + % gf B -> A ] +------------------------------ Implication strategy +[ A |- B -> A ] +------------------------------ Implication strategy +[ A , B |- A ] +------------------------------ Hypothesis +Ø + diff --git a/examples/systemS/ex1eng.txt b/examples/systemS/ex1eng.txt new file mode 100644 index 000000000..255440486 --- /dev/null +++ b/examples/systemS/ex1eng.txt @@ -0,0 +1,4 @@ +We will show that A -> B -> A. +It is enough to assume A and show B -> A. +It is enough to assume A, B and show A. +But this holds trivially. diff --git a/examples/systemS/ex2.txt b/examples/systemS/ex2.txt new file mode 100644 index 000000000..1dffb6bf9 --- /dev/null +++ b/examples/systemS/ex2.txt @@ -0,0 +1,13 @@ +[ A -> B |- ~ B -> ~ A ] +------------------------------ Implication strategy +[ A -> B , ~ B |- ~ A ] +------------------------------ Negation rewrite +[ A -> B , ~ B |- A -> _|_ ] +------------------------------ Implication strategy +[ A , A -> B , ~ B |- _|_ ] +------------------------------ Modus ponens +[ A , A -> B , B , ~ B |- _|_ ] +------------------------------ Forgetting +[ B , ~ B |- _|_ ] +------------------------------ Ex falso quodlibet _|_ +Ø diff --git a/examples/systemS/ex2eng.txt b/examples/systemS/ex2eng.txt new file mode 100644 index 000000000..f1ef836ae --- /dev/null +++ b/examples/systemS/ex2eng.txt @@ -0,0 +1,7 @@ +Suppose A -> B. We will show that ~ B -> ~ A. +It is enough to assume A -> B, ~ B and show ~ A. +Thus, by rewriting ~ A we may assume A -> B, ~ B and show A -> _|_. +It is enough to assume A, A -> B, ~ B and show _|_. +Then, by Modus ponens, we get A, A -> B, B, ~ B to prove _|_. +In particular we get B, ~ B to prove _|_. +Hence we get _|_ as desired. diff --git a/examples/systemS/ex4.txt b/examples/systemS/ex4.txt new file mode 100644 index 000000000..7a91011da --- /dev/null +++ b/examples/systemS/ex4.txt @@ -0,0 +1,13 @@ +[ |- (A -> B) v (B -> A) ] +------------------------------ Reductio ad absurdum +[ ~ ((A -> B) v (B -> A)) |- _|_ ] +------------------------------ de Morgan 1 +[ ~ (A -> B) & ~ (B -> A) |- _|_ ] +------------------------------ Conjunction split +[ ~ (A -> B), ~ (B -> A) |- _|_ ] +------------------------------ Implication negation +[ A, ~ (B -> A) |- _|_ ] +------------------------------ Implication negation +[ A, ~ A |- _|_ ] +------------------------------ Ex falso quodlibet _|_ +Ø diff --git a/examples/systemS/ex4eng.txt b/examples/systemS/ex4eng.txt new file mode 100644 index 000000000..3ad4f3549 --- /dev/null +++ b/examples/systemS/ex4eng.txt @@ -0,0 +1,8 @@ +We will show that (A -> B) v (B -> A). +To that end, we will assume ~ ((A -> B) v (B -> A)) and show _|_. +So let us assume that ~ ((A -> B) v (B -> A)). +Then, by the first de Morgan's law, we get ~ (A -> B) & ~ (B -> A) to prove _|_. +So by splitting we get ~ (A -> B), ~ (B -> A) to prove _|_. +By implication negation, we get A, ~ (B -> A) to prove _|_. +By implication negation, we get A, ~ A to prove _|_. +Hence we get _|_ as desired. diff --git a/examples/systemS/proof.gfcm b/examples/systemS/proof.gfcm new file mode 100644 index 000000000..6e9692769 --- /dev/null +++ b/examples/systemS/proof.gfcm @@ -0,0 +1,113 @@ +concrete ProofSymb of Proof=FormulaSymb**open Prelude,Precedence in{flags modulesize=n27;flags startcat=Text;flags unlexer=text;flags lexer=text;A in FormulaSymb; +Abs in FormulaSymb; +And in FormulaSymb; +B in FormulaSymb; +lin BaseFormula:Proof.ListFormula=\->{s=[];isnil=};"[]"; +C in FormulaSymb; +lin ConjSplit:Proof.Proof=\Formula@0,Formula@1,Formula@2,Proof@3->{s="Conjunction"++"split"++(variants{"&-"[]}++("["++(table{p1:Ints 4;p2:Ints 4}{{p1=0;p2=0}{p1=1;p2=0}{p1=1;p2=1}{p1=2;p2=0}{p1=2;p2=1}{p1=2;p2=2}{p1=3;p2=0}{p1=3;p2=1}{p1=3;p2=2}{p1=3;p2=3}{p1=4;p2=0}{p1=4;p2=1}{p1=4;p2=2}{p1=4;p2=3}{p1=4;p2=4}=>Formula@0.s;{p1=0;p2=1}{p1=0;p2=2}{p1=0;p2=3}{p1=0;p2=4}{p1=1;p2=2}{p1=1;p2=3}{p1=1;p2=4}{p1=2;p2=3}{p1=2;p2=4}{p1=3;p2=4}=>"("++(Formula@0.s++")")}!{p1=Formula@0.p;p2=0}++(","++table{p1:Ints 4;p2:Ints 4}{{p1=0;p2=0}{p1=1;p2=0}{p1=1;p2=1}{p1=2;p2=0}{p1=2;p2=1}{p1=2;p2=2}{p1=3;p2=0}{p1=3;p2=1}{p1=3;p2=2}{p1=3;p2=3}{p1=4;p2=0}{p1=4;p2=1}{p1=4;p2=2}{p1=4;p2=3}{p1=4;p2=4}=>Formula@1.s;{p1=0;p2=1}{p1=0;p2=2}{p1=0;p2=3}{p1=0;p2=4}{p1=1;p2=2}{p1=1;p2=3}{p1=1;p2=4}{p1=2;p2=3}{p1=2;p2=4}{p1=3;p2=4}=>"("++(Formula@1.s++")")}!{p1=Formula@1.p;p2=0})++("|-"++(table{p1:Ints 4;p2:Ints 4}{{p1=0;p2=0}{p1=1;p2=0}{p1=1;p2=1}{p1=2;p2=0}{p1=2;p2=1}{p1=2;p2=2}{p1=3;p2=0}{p1=3;p2=1}{p1=3;p2=2}{p1=3;p2=3}{p1=4;p2=0}{p1=4;p2=1}{p1=4;p2=2}{p1=4;p2=3}{p1=4;p2=4}=>Formula@2.s;{p1=0;p2=1}{p1=0;p2=2}{p1=0;p2=3}{p1=0;p2=4}{p1=1;p2=2}{p1=1;p2=3}{p1=1;p2=4}{p1=2;p2=3}{p1=2;p2=4}{p1=3;p2=4}=>"("++(Formula@2.s++")")}!{p1=Formula@2.p;p2=0}++"]")))++(variants{"&-"[]}++("------------------------------"++Proof@3.s))))};"(Conjunction split)&- ([ (Formula_0 , Formula_1)|- Formula_2 ])&- ------------------------------ Proof_3"; +lin ConsFormula:Proof.ListFormula=\Formula@0,ListFormula@1->{s=table{p1:Ints 4;p2:Ints 4}{{p1=0;p2=0}{p1=1;p2=0}{p1=1;p2=1}{p1=2;p2=0}{p1=2;p2=1}{p1=2;p2=2}{p1=3;p2=0}{p1=3;p2=1}{p1=3;p2=2}{p1=3;p2=3}{p1=4;p2=0}{p1=4;p2=1}{p1=4;p2=2}{p1=4;p2=3}{p1=4;p2=4}=>Formula@0.s;{p1=0;p2=1}{p1=0;p2=2}{p1=0;p2=3}{p1=0;p2=4}{p1=1;p2=2}{p1=1;p2=3}{p1=1;p2=4}{p1=2;p2=3}{p1=2;p2=4}{p1=3;p2=4}=>"("++(Formula@0.s++")")}!{p1=Formula@0.p;p2=0}++table Prelude.Bool{(Prelude.True)=>ListFormula@1.s;(Prelude.False)=>","++ListFormula@1.s}!(ListFormula@1.isnil);isnil=};"Formula_0 ListFormula_1"; +lin DeMorgan1:Proof.Proof=\Formula@0,Formula@1,Proof@2->{s="de"++("Morgan"++"1")++(variants{"&-"[]}++("["++(Formula@0.s++("|-"++(Formula@1.s++"]")))++(variants{"&-"[]}++("------------------------------"++Proof@2.s))))};"(de Morgan 1)&- ([ Formula_0 |- Formula_1 ])&- ------------------------------ Proof_2"; +lin DeMorgan2:Proof.Proof=\Formula@0,Formula@1,Proof@2->{s="de"++("Morgan"++"2")++(variants{"&-"[]}++("["++(Formula@0.s++("|-"++(Formula@1.s++"]")))++(variants{"&-"[]}++("------------------------------"++Proof@2.s))))};"(de Morgan 2)&- ([ Formula_0 |- Formula_1 ])&- ------------------------------ Proof_2"; +lin ExFalso:Proof.Proof=\Formula@0->{s="Ex"++("falso"++"quodlibet")++Formula@0.s++(variants{"&-"[]}++"Ø")};"((Ex falso quodlibet)Formula_0)&- Ø"; +lin Forget:Proof.Proof=\ListFormula@0,Formula@1,Proof@2->{s="Forgetting"++(variants{"&-"[]}++("["++(ListFormula@0.s++("|-"++(Formula@1.s++"]")))++(variants{"&-"[]}++("------------------------------"++Proof@2.s))))};"Forgetting &- ([ ListFormula_0 |- Formula_1 ])&- ------------------------------ Proof_2"; +Formula in FormulaSymb; +lin Hypo:Proof.Proof=\->{s="Hypothesis"++(variants{"&-"[]}++"Ø")};"Hypothesis &- Ø"; +If in FormulaSymb; +lin Implic:Proof.Proof=\ListFormula@0,Formula@1,Proof@2->{s="Implication"++"strategy"++(variants{"&-"[]}++("["++(ListFormula@0.s++("|-"++(Formula@1.s++"]")))++(variants{"&-"[]}++("------------------------------"++Proof@2.s))))};"(Implication strategy)&- ([ ListFormula_0 |- Formula_1 ])&- ------------------------------ Proof_2"; +lin ImplicNeg:Proof.Proof=\ListFormula@0,Formula@1,Proof@2->{s="Implication"++"negation"++(variants{"&-"[]}++("["++(ListFormula@0.s++("|-"++(Formula@1.s++"]")))++(variants{"&-"[]}++("------------------------------"++Proof@2.s))))};"(Implication negation)&- ([ ListFormula_0 |- Formula_1 ])&- ------------------------------ Proof_2"; +lincat ListFormula={s:Str;isnil:Prelude.Bool}={s=str@0;isnil=};"ListFormula"; +lin ModPon:Proof.Proof=\ListFormula@0,Formula@1,Proof@2->{s="Modus"++"ponens"++(variants{"&-"[]}++("["++(ListFormula@0.s++("|-"++(Formula@1.s++"]")))++(variants{"&-"[]}++("------------------------------"++Proof@2.s))))};"(Modus ponens)&- ([ ListFormula_0 |- Formula_1 ])&- ------------------------------ Proof_2"; +lin NegRewrite:Proof.Proof=\Formula@0,ListFormula@1,Proof@2->{s="Negation"++"rewrite"++(variants{"&-"[]}++("["++(ListFormula@1.s++("|-"++(table{p1:Ints 4;p2:Ints 4}{{p1=0;p2=0}{p1=1;p2=0}{p1=1;p2=1}{p1=2;p2=0}{p1=2;p2=1}{p1=2;p2=2}{p1=3;p2=0}{p1=3;p2=1}{p1=3;p2=2}{p1=3;p2=3}{p1=4;p2=0}{p1=4;p2=1}{p1=4;p2=2}{p1=4;p2=3}{p1=4;p2=4}=>Formula@0.s;{p1=0;p2=1}{p1=0;p2=2}{p1=0;p2=3}{p1=0;p2=4}{p1=1;p2=2}{p1=1;p2=3}{p1=1;p2=4}{p1=2;p2=3}{p1=2;p2=4}{p1=3;p2=4}=>"("++(Formula@0.s++")")}!{p1=Formula@0.p;p2=2}++("->"++"_|_")++"]")))++(variants{"&-"[]}++("------------------------------"++Proof@2.s))))};"(Negation rewrite)&- ([ ListFormula_1 |- (Formula_0 -> _|_)])&- ------------------------------ Proof_2"; +Not in FormulaSymb; +Or in FormulaSymb; +lincat Proof={s:Str}={s=str@0};"Proof"; +lin RedAbs:Proof.Proof=\Formula@0,Proof@1->{s="Reductio"++("ad"++"absurdum")++(variants{"&-"[]}++("["++("~"++table{p1:Ints 4;p2:Ints 4}{{p1=0;p2=0}{p1=1;p2=0}{p1=1;p2=1}{p1=2;p2=0}{p1=2;p2=1}{p1=2;p2=2}{p1=3;p2=0}{p1=3;p2=1}{p1=3;p2=2}{p1=3;p2=3}{p1=4;p2=0}{p1=4;p2=1}{p1=4;p2=2}{p1=4;p2=3}{p1=4;p2=4}=>Formula@0.s;{p1=0;p2=1}{p1=0;p2=2}{p1=0;p2=3}{p1=0;p2=4}{p1=1;p2=2}{p1=1;p2=3}{p1=1;p2=4}{p1=2;p2=3}{p1=2;p2=4}{p1=3;p2=4}=>"("++(Formula@0.s++")")}!{p1=Formula@0.p;p2=4}++("|-"++("_|_"++"]")))++(variants{"&-"[]}++("------------------------------"++Proof@1.s))))};"(Reductio ad absurdum)&- ([ (~ Formula_0)|- _|_ ])&- ------------------------------ Proof_1"; +lin Start:Proof.Text=\ListFormula@0,Formula@1,Proof@2->{s=variants{"&-"[]}++("["++(ListFormula@0.s++("|-"++(Formula@1.s++"]")))++(variants{"&-"[]}++("------------------------------"++Proof@2.s)))};"&- ([ ListFormula_0 |- Formula_1 ])&- ------------------------------ Proof_2"; +Term in FormulaSymb; +lincat Text={s:Str}={s=str@0};"Text"; +} +concrete ProofEng of Proof=FormulaSymb**open Prelude,Precedence in{flags modulesize=n27;flags startcat=Text;flags unlexer=text;flags lexer=text;A in FormulaSymb; +Abs in FormulaSymb; +And in FormulaSymb; +B in FormulaSymb; +lin BaseFormula:Proof.ListFormula=\->{s=[];isnil=};"[]"; +C in FormulaSymb; +lin ConjSplit:Proof.Proof=\Formula@0,Formula@1,Formula@2,Proof@3->{s=variants{"&-"[]}++("So"++("by"++("splitting"++("we"++"get")))++(table{p1:Ints 4;p2:Ints 4}{{p1=0;p2=0}{p1=1;p2=0}{p1=1;p2=1}{p1=2;p2=0}{p1=2;p2=1}{p1=2;p2=2}{p1=3;p2=0}{p1=3;p2=1}{p1=3;p2=2}{p1=3;p2=3}{p1=4;p2=0}{p1=4;p2=1}{p1=4;p2=2}{p1=4;p2=3}{p1=4;p2=4}=>Formula@0.s;{p1=0;p2=1}{p1=0;p2=2}{p1=0;p2=3}{p1=0;p2=4}{p1=1;p2=2}{p1=1;p2=3}{p1=1;p2=4}{p1=2;p2=3}{p1=2;p2=4}{p1=3;p2=4}=>"("++(Formula@0.s++")")}!{p1=Formula@0.p;p2=0}++(","++(table{p1:Ints 4;p2:Ints 4}{{p1=0;p2=0}{p1=1;p2=0}{p1=1;p2=1}{p1=2;p2=0}{p1=2;p2=1}{p1=2;p2=2}{p1=3;p2=0}{p1=3;p2=1}{p1=3;p2=2}{p1=3;p2=3}{p1=4;p2=0}{p1=4;p2=1}{p1=4;p2=2}{p1=4;p2=3}{p1=4;p2=4}=>Formula@1.s;{p1=0;p2=1}{p1=0;p2=2}{p1=0;p2=3}{p1=0;p2=4}{p1=1;p2=2}{p1=1;p2=3}{p1=1;p2=4}{p1=2;p2=3}{p1=2;p2=4}{p1=3;p2=4}=>"("++(Formula@1.s++")")}!{p1=Formula@1.p;p2=0}++(variants{[]("to"++"prove"++table{p1:Ints 4;p2:Ints 4}{{p1=0;p2=0}{p1=1;p2=0}{p1=1;p2=1}{p1=2;p2=0}{p1=2;p2=1}{p1=2;p2=2}{p1=3;p2=0}{p1=3;p2=1}{p1=3;p2=2}{p1=3;p2=3}{p1=4;p2=0}{p1=4;p2=1}{p1=4;p2=2}{p1=4;p2=3}{p1=4;p2=4}=>Formula@2.s;{p1=0;p2=1}{p1=0;p2=2}{p1=0;p2=3}{p1=0;p2=4}{p1=1;p2=2}{p1=1;p2=3}{p1=1;p2=4}{p1=2;p2=3}{p1=2;p2=4}{p1=3;p2=4}=>"("++(Formula@2.s++")")}!{p1=Formula@2.p;p2=0})}++("."++Proof@3.s))))))};"&- (So by splitting we get)Formula_0 , Formula_1 [] . Proof_3"; +lin ConsFormula:Proof.ListFormula=\Formula@0,ListFormula@1->{s=table{p1:Ints 4;p2:Ints 4}{{p1=0;p2=0}{p1=1;p2=0}{p1=1;p2=1}{p1=2;p2=0}{p1=2;p2=1}{p1=2;p2=2}{p1=3;p2=0}{p1=3;p2=1}{p1=3;p2=2}{p1=3;p2=3}{p1=4;p2=0}{p1=4;p2=1}{p1=4;p2=2}{p1=4;p2=3}{p1=4;p2=4}=>Formula@0.s;{p1=0;p2=1}{p1=0;p2=2}{p1=0;p2=3}{p1=0;p2=4}{p1=1;p2=2}{p1=1;p2=3}{p1=1;p2=4}{p1=2;p2=3}{p1=2;p2=4}{p1=3;p2=4}=>"("++(Formula@0.s++")")}!{p1=Formula@0.p;p2=0}++table Prelude.Bool{(Prelude.True)=>ListFormula@1.s;(Prelude.False)=>","++ListFormula@1.s}!(ListFormula@1.isnil);isnil=};"Formula_0 ListFormula_1"; +lin DeMorgan1:Proof.Proof=\Formula@0,Formula@1,Proof@2->{s=variants{"&-"[]}++("Then"++(","++("by"++("the"++("first"++("de"++("Morgan's"++("law"++(","++("we"++"get")))))))))++(table{p1:Ints 4;p2:Ints 4}{{p1=0;p2=0}{p1=1;p2=0}{p1=1;p2=1}{p1=2;p2=0}{p1=2;p2=1}{p1=2;p2=2}{p1=3;p2=0}{p1=3;p2=1}{p1=3;p2=2}{p1=3;p2=3}{p1=4;p2=0}{p1=4;p2=1}{p1=4;p2=2}{p1=4;p2=3}{p1=4;p2=4}=>Formula@0.s;{p1=0;p2=1}{p1=0;p2=2}{p1=0;p2=3}{p1=0;p2=4}{p1=1;p2=2}{p1=1;p2=3}{p1=1;p2=4}{p1=2;p2=3}{p1=2;p2=4}{p1=3;p2=4}=>"("++(Formula@0.s++")")}!{p1=Formula@0.p;p2=0}++(variants{[]("to"++"prove"++table{p1:Ints 4;p2:Ints 4}{{p1=0;p2=0}{p1=1;p2=0}{p1=1;p2=1}{p1=2;p2=0}{p1=2;p2=1}{p1=2;p2=2}{p1=3;p2=0}{p1=3;p2=1}{p1=3;p2=2}{p1=3;p2=3}{p1=4;p2=0}{p1=4;p2=1}{p1=4;p2=2}{p1=4;p2=3}{p1=4;p2=4}=>Formula@1.s;{p1=0;p2=1}{p1=0;p2=2}{p1=0;p2=3}{p1=0;p2=4}{p1=1;p2=2}{p1=1;p2=3}{p1=1;p2=4}{p1=2;p2=3}{p1=2;p2=4}{p1=3;p2=4}=>"("++(Formula@1.s++")")}!{p1=Formula@1.p;p2=0})}++("."++Proof@2.s))))};"&- (Then , by the first de Morgan's law , we get)Formula_0 [] . Proof_2"; +lin DeMorgan2:Proof.Proof=\Formula@0,Formula@1,Proof@2->{s=variants{"&-"[]}++("Then"++(","++("by"++("the"++("second"++("de"++("Morgan's"++("law"++(","++("we"++"get")))))))))++(table{p1:Ints 4;p2:Ints 4}{{p1=0;p2=0}{p1=1;p2=0}{p1=1;p2=1}{p1=2;p2=0}{p1=2;p2=1}{p1=2;p2=2}{p1=3;p2=0}{p1=3;p2=1}{p1=3;p2=2}{p1=3;p2=3}{p1=4;p2=0}{p1=4;p2=1}{p1=4;p2=2}{p1=4;p2=3}{p1=4;p2=4}=>Formula@0.s;{p1=0;p2=1}{p1=0;p2=2}{p1=0;p2=3}{p1=0;p2=4}{p1=1;p2=2}{p1=1;p2=3}{p1=1;p2=4}{p1=2;p2=3}{p1=2;p2=4}{p1=3;p2=4}=>"("++(Formula@0.s++")")}!{p1=Formula@0.p;p2=0}++(variants{[]("to"++"prove"++table{p1:Ints 4;p2:Ints 4}{{p1=0;p2=0}{p1=1;p2=0}{p1=1;p2=1}{p1=2;p2=0}{p1=2;p2=1}{p1=2;p2=2}{p1=3;p2=0}{p1=3;p2=1}{p1=3;p2=2}{p1=3;p2=3}{p1=4;p2=0}{p1=4;p2=1}{p1=4;p2=2}{p1=4;p2=3}{p1=4;p2=4}=>Formula@1.s;{p1=0;p2=1}{p1=0;p2=2}{p1=0;p2=3}{p1=0;p2=4}{p1=1;p2=2}{p1=1;p2=3}{p1=1;p2=4}{p1=2;p2=3}{p1=2;p2=4}{p1=3;p2=4}=>"("++(Formula@1.s++")")}!{p1=Formula@1.p;p2=0})}++("."++Proof@2.s))))};"&- (Then , by the second de Morgan's law , we get)Formula_0 [] . Proof_2"; +lin ExFalso:Proof.Proof=\Formula@0->{s=variants{"&-"[]}++("Hence"++("we"++"get")++(table{p1:Ints 4;p2:Ints 4}{{p1=0;p2=0}{p1=1;p2=0}{p1=1;p2=1}{p1=2;p2=0}{p1=2;p2=1}{p1=2;p2=2}{p1=3;p2=0}{p1=3;p2=1}{p1=3;p2=2}{p1=3;p2=3}{p1=4;p2=0}{p1=4;p2=1}{p1=4;p2=2}{p1=4;p2=3}{p1=4;p2=4}=>Formula@0.s;{p1=0;p2=1}{p1=0;p2=2}{p1=0;p2=3}{p1=0;p2=4}{p1=1;p2=2}{p1=1;p2=3}{p1=1;p2=4}{p1=2;p2=3}{p1=2;p2=4}{p1=3;p2=4}=>"("++(Formula@0.s++")")}!{p1=Formula@0.p;p2=0}++("as"++"desired"++".")))};"&- (Hence we get)Formula_0 (as desired)."; +lin Forget:Proof.Proof=\ListFormula@0,Formula@1,Proof@2->{s=variants{"&-"[]}++("In"++("particular"++("we"++"get"))++(ListFormula@0.s++(variants{[]("to"++"prove"++table{p1:Ints 4;p2:Ints 4}{{p1=0;p2=0}{p1=1;p2=0}{p1=1;p2=1}{p1=2;p2=0}{p1=2;p2=1}{p1=2;p2=2}{p1=3;p2=0}{p1=3;p2=1}{p1=3;p2=2}{p1=3;p2=3}{p1=4;p2=0}{p1=4;p2=1}{p1=4;p2=2}{p1=4;p2=3}{p1=4;p2=4}=>Formula@1.s;{p1=0;p2=1}{p1=0;p2=2}{p1=0;p2=3}{p1=0;p2=4}{p1=1;p2=2}{p1=1;p2=3}{p1=1;p2=4}{p1=2;p2=3}{p1=2;p2=4}{p1=3;p2=4}=>"("++(Formula@1.s++")")}!{p1=Formula@1.p;p2=0})}++("."++Proof@2.s))))};"&- (In particular we get)ListFormula_0 [] . Proof_2"; +Formula in FormulaSymb; +lin Hypo:Proof.Proof=\->{s=variants{"&-"[]}++("But"++("this"++("holds"++("trivially"++"."))))};"&- But this holds trivially ."; +If in FormulaSymb; +lin Implic:Proof.Proof=\ListFormula@0,Formula@1,Proof@2->{s=variants{"&-"[]}++("It"++("is"++("enough"++"to"))++(table Prelude.Bool{(Prelude.True)=>ListFormula@0.s;(Prelude.False)=>"assume"++(ListFormula@0.s++"and")}!(ListFormula@0.isnil)++("show"++(Formula@1.s++("."++Proof@2.s)))))};"&- (It is enough to)ListFormula_0 show Formula_1 . Proof_2"; +lin ImplicNeg:Proof.Proof=\ListFormula@0,Formula@1,Proof@2->{s=variants{"&-"[]}++("By"++("implication"++("negation"++(","++("we"++"get"))))++(ListFormula@0.s++(variants{[]("to"++"prove"++table{p1:Ints 4;p2:Ints 4}{{p1=0;p2=0}{p1=1;p2=0}{p1=1;p2=1}{p1=2;p2=0}{p1=2;p2=1}{p1=2;p2=2}{p1=3;p2=0}{p1=3;p2=1}{p1=3;p2=2}{p1=3;p2=3}{p1=4;p2=0}{p1=4;p2=1}{p1=4;p2=2}{p1=4;p2=3}{p1=4;p2=4}=>Formula@1.s;{p1=0;p2=1}{p1=0;p2=2}{p1=0;p2=3}{p1=0;p2=4}{p1=1;p2=2}{p1=1;p2=3}{p1=1;p2=4}{p1=2;p2=3}{p1=2;p2=4}{p1=3;p2=4}=>"("++(Formula@1.s++")")}!{p1=Formula@1.p;p2=0})}++("."++Proof@2.s))))};"&- (By implication negation , we get)ListFormula_0 [] . Proof_2"; +lincat ListFormula={s:Str;isnil:Prelude.Bool}={s=str@0;isnil=};"ListFormula"; +lin ModPon:Proof.Proof=\ListFormula@0,Formula@1,Proof@2->{s=variants{"&-"[]}++("Then"++(","++("by"++("Modus"++("ponens"++(","++("we"++"get"))))))++(ListFormula@0.s++(variants{[]("to"++"prove"++table{p1:Ints 4;p2:Ints 4}{{p1=0;p2=0}{p1=1;p2=0}{p1=1;p2=1}{p1=2;p2=0}{p1=2;p2=1}{p1=2;p2=2}{p1=3;p2=0}{p1=3;p2=1}{p1=3;p2=2}{p1=3;p2=3}{p1=4;p2=0}{p1=4;p2=1}{p1=4;p2=2}{p1=4;p2=3}{p1=4;p2=4}=>Formula@1.s;{p1=0;p2=1}{p1=0;p2=2}{p1=0;p2=3}{p1=0;p2=4}{p1=1;p2=2}{p1=1;p2=3}{p1=1;p2=4}{p1=2;p2=3}{p1=2;p2=4}{p1=3;p2=4}=>"("++(Formula@1.s++")")}!{p1=Formula@1.p;p2=0})}++("."++Proof@2.s))))};"&- (Then , by Modus ponens , we get)ListFormula_0 [] . Proof_2"; +lin NegRewrite:Proof.Proof=\Formula@0,ListFormula@1,Proof@2->{s=variants{"&-"[]}++("Thus"++(","++("by"++"rewriting"))++("~"++table{p1:Ints 4;p2:Ints 4}{{p1=0;p2=0}{p1=1;p2=0}{p1=1;p2=1}{p1=2;p2=0}{p1=2;p2=1}{p1=2;p2=2}{p1=3;p2=0}{p1=3;p2=1}{p1=3;p2=2}{p1=3;p2=3}{p1=4;p2=0}{p1=4;p2=1}{p1=4;p2=2}{p1=4;p2=3}{p1=4;p2=4}=>Formula@0.s;{p1=0;p2=1}{p1=0;p2=2}{p1=0;p2=3}{p1=0;p2=4}{p1=1;p2=2}{p1=1;p2=3}{p1=1;p2=4}{p1=2;p2=3}{p1=2;p2=4}{p1=3;p2=4}=>"("++(Formula@0.s++")")}!{p1=Formula@0.p;p2=4}++(table Prelude.Bool{(Prelude.True)=>ListFormula@1.s;(Prelude.False)=>"we"++("may"++"assume")++(ListFormula@1.s++"and")}!(ListFormula@1.isnil)++("show"++(table{p1:Ints 4;p2:Ints 4}{{p1=0;p2=0}{p1=1;p2=0}{p1=1;p2=1}{p1=2;p2=0}{p1=2;p2=1}{p1=2;p2=2}{p1=3;p2=0}{p1=3;p2=1}{p1=3;p2=2}{p1=3;p2=3}{p1=4;p2=0}{p1=4;p2=1}{p1=4;p2=2}{p1=4;p2=3}{p1=4;p2=4}=>Formula@0.s;{p1=0;p2=1}{p1=0;p2=2}{p1=0;p2=3}{p1=0;p2=4}{p1=1;p2=2}{p1=1;p2=3}{p1=1;p2=4}{p1=2;p2=3}{p1=2;p2=4}{p1=3;p2=4}=>"("++(Formula@0.s++")")}!{p1=Formula@0.p;p2=2}++("->"++"_|_")++("."++Proof@2.s))))))};"&- (Thus , by rewriting)(~ Formula_0)ListFormula_1 show (Formula_0 -> _|_). Proof_2"; +Not in FormulaSymb; +Or in FormulaSymb; +lincat Proof={s:Str}={s=str@0};"Proof"; +lin RedAbs:Proof.Proof=\Formula@0,Proof@1->{s=variants{"&-"[]}++("To"++("that"++("end"++(","++("we"++("will"++"assume")))))++("~"++table{p1:Ints 4;p2:Ints 4}{{p1=0;p2=0}{p1=1;p2=0}{p1=1;p2=1}{p1=2;p2=0}{p1=2;p2=1}{p1=2;p2=2}{p1=3;p2=0}{p1=3;p2=1}{p1=3;p2=2}{p1=3;p2=3}{p1=4;p2=0}{p1=4;p2=1}{p1=4;p2=2}{p1=4;p2=3}{p1=4;p2=4}=>Formula@0.s;{p1=0;p2=1}{p1=0;p2=2}{p1=0;p2=3}{p1=0;p2=4}{p1=1;p2=2}{p1=1;p2=3}{p1=1;p2=4}{p1=2;p2=3}{p1=2;p2=4}{p1=3;p2=4}=>"("++(Formula@0.s++")")}!{p1=Formula@0.p;p2=4}++("and"++"show"++("_|_"++("."++(variants{"&-"[]}++("So"++("let"++("us"++("assume"++"that")))++("~"++table{p1:Ints 4;p2:Ints 4}{{p1=0;p2=0}{p1=1;p2=0}{p1=1;p2=1}{p1=2;p2=0}{p1=2;p2=1}{p1=2;p2=2}{p1=3;p2=0}{p1=3;p2=1}{p1=3;p2=2}{p1=3;p2=3}{p1=4;p2=0}{p1=4;p2=1}{p1=4;p2=2}{p1=4;p2=3}{p1=4;p2=4}=>Formula@0.s;{p1=0;p2=1}{p1=0;p2=2}{p1=0;p2=3}{p1=0;p2=4}{p1=1;p2=2}{p1=1;p2=3}{p1=1;p2=4}{p1=2;p2=3}{p1=2;p2=4}{p1=3;p2=4}=>"("++(Formula@0.s++")")}!{p1=Formula@0.p;p2=4}++("."++Proof@1.s)))))))))};"&- (To that end , we will assume)(~ Formula_0)(and show)_|_ . &- (So let us assume that)(~ Formula_0). Proof_1"; +lin Start:Proof.Text=\ListFormula@0,Formula@1,Proof@2->{s=table Prelude.Bool{(Prelude.True)=>ListFormula@0.s;(Prelude.False)=>"Suppose"++(ListFormula@0.s++".")}!(ListFormula@0.isnil)++("We"++("will"++("show"++"that"))++(table{p1:Ints 4;p2:Ints 4}{{p1=0;p2=0}{p1=1;p2=0}{p1=1;p2=1}{p1=2;p2=0}{p1=2;p2=1}{p1=2;p2=2}{p1=3;p2=0}{p1=3;p2=1}{p1=3;p2=2}{p1=3;p2=3}{p1=4;p2=0}{p1=4;p2=1}{p1=4;p2=2}{p1=4;p2=3}{p1=4;p2=4}=>Formula@1.s;{p1=0;p2=1}{p1=0;p2=2}{p1=0;p2=3}{p1=0;p2=4}{p1=1;p2=2}{p1=1;p2=3}{p1=1;p2=4}{p1=2;p2=3}{p1=2;p2=4}{p1=3;p2=4}=>"("++(Formula@1.s++")")}!{p1=Formula@1.p;p2=0}++("."++Proof@2.s)))};"ListFormula_0 (We will show that)Formula_1 . Proof_2"; +Term in FormulaSymb; +lincat Text={s:Str}={s=str@0};"Text"; +} +abstract Proof=Formula**{flags modulesize=n27;A in Formula; +Abs in Formula; +And in Formula; +B in Formula; +fun BaseFormula:Proof.ListFormula=data; +C in Formula; +fun ConjSplit:(h_:Formula.Formula)->(h_:Formula.Formula)->(h_:Formula.Formula)->(h_:Proof.Proof)->Proof.Proof={}; +fun ConsFormula:(h_:Formula.Formula)->(h_:Proof.ListFormula)->Proof.ListFormula=data; +fun DeMorgan1:(h_:Formula.Formula)->(h_:Formula.Formula)->(h_:Proof.Proof)->Proof.Proof={}; +fun DeMorgan2:(h_:Formula.Formula)->(h_:Formula.Formula)->(h_:Proof.Proof)->Proof.Proof={}; +fun ExFalso:(h_:Formula.Formula)->Proof.Proof={}; +fun Forget:(h_:Proof.ListFormula)->(h_:Formula.Formula)->(h_:Proof.Proof)->Proof.Proof={}; +Formula in Formula; +fun Hypo:Proof.Proof={}; +If in Formula; +fun Implic:(h_:Proof.ListFormula)->(h_:Formula.Formula)->(h_:Proof.Proof)->Proof.Proof={}; +fun ImplicNeg:(h_:Proof.ListFormula)->(h_:Formula.Formula)->(h_:Proof.Proof)->Proof.Proof={}; +cat ListFormula[]=; +fun ModPon:(h_:Proof.ListFormula)->(h_:Formula.Formula)->(h_:Proof.Proof)->Proof.Proof={}; +fun NegRewrite:(h_:Formula.Formula)->(h_:Proof.ListFormula)->(h_:Proof.Proof)->Proof.Proof={}; +Not in Formula; +Or in Formula; +cat Proof[]=; +fun RedAbs:(h_:Formula.Formula)->(h_:Proof.Proof)->Proof.Proof={}; +fun Start:(h_:Proof.ListFormula)->(h_:Formula.Formula)->(h_:Proof.Proof)->Proof.Text={}; +Term in Formula; +cat Text[]=; +} +concrete FormulaSymb of Formula=open Precedence in{flags modulesize=n10;lin A:Formula.Formula=\->{s="A";p=4;a=};"A"; +lin Abs:Formula.Formula=\->{s="_|_";p=4;a=};"_|_"; +lin And:Formula.Formula=\Formula@0,Formula@1->{s=table{p1:Ints 4;p2:Ints 4}{{p1=0;p2=0}{p1=1;p2=0}{p1=1;p2=1}{p1=2;p2=0}{p1=2;p2=1}{p1=2;p2=2}{p1=3;p2=0}{p1=3;p2=1}{p1=3;p2=2}{p1=3;p2=3}{p1=4;p2=0}{p1=4;p2=1}{p1=4;p2=2}{p1=4;p2=3}{p1=4;p2=4}=>Formula@0.s;{p1=0;p2=1}{p1=0;p2=2}{p1=0;p2=3}{p1=0;p2=4}{p1=1;p2=2}{p1=1;p2=3}{p1=1;p2=4}{p1=2;p2=3}{p1=2;p2=4}{p1=3;p2=4}=>"("++(Formula@0.s++")")}!{p1=Formula@0.p;p2=3}++("&"++table{p1:Ints 4;p2:Ints 4}{{p1=0;p2=0}{p1=1;p2=0}{p1=1;p2=1}{p1=2;p2=0}{p1=2;p2=1}{p1=2;p2=2}{p1=3;p2=0}{p1=3;p2=1}{p1=3;p2=2}{p1=3;p2=3}{p1=4;p2=0}{p1=4;p2=1}{p1=4;p2=2}{p1=4;p2=3}{p1=4;p2=4}=>Formula@1.s;{p1=0;p2=1}{p1=0;p2=2}{p1=0;p2=3}{p1=0;p2=4}{p1=1;p2=2}{p1=1;p2=3}{p1=1;p2=4}{p1=2;p2=3}{p1=2;p2=4}{p1=3;p2=4}=>"("++(Formula@1.s++")")}!{p1=Formula@1.p;p2=4});p=3;a=};"Formula_0 & Formula_1"; +lin B:Formula.Formula=\->{s="B";p=4;a=};"B"; +lin C:Formula.Formula=\->{s="C";p=4;a=};"C"; +lincat Formula={s:Str;p:Ints 4;a:Precedence.PAssoc}={s=str@0;p=0;a=};"Formula"; +lin If:Formula.Formula=\Formula@0,Formula@1->{s=table{p1:Ints 4;p2:Ints 4}{{p1=0;p2=0}{p1=1;p2=0}{p1=1;p2=1}{p1=2;p2=0}{p1=2;p2=1}{p1=2;p2=2}{p1=3;p2=0}{p1=3;p2=1}{p1=3;p2=2}{p1=3;p2=3}{p1=4;p2=0}{p1=4;p2=1}{p1=4;p2=2}{p1=4;p2=3}{p1=4;p2=4}=>Formula@0.s;{p1=0;p2=1}{p1=0;p2=2}{p1=0;p2=3}{p1=0;p2=4}{p1=1;p2=2}{p1=1;p2=3}{p1=1;p2=4}{p1=2;p2=3}{p1=2;p2=4}{p1=3;p2=4}=>"("++(Formula@0.s++")")}!{p1=Formula@0.p;p2=2}++("->"++table{p1:Ints 4;p2:Ints 4}{{p1=0;p2=0}{p1=1;p2=0}{p1=1;p2=1}{p1=2;p2=0}{p1=2;p2=1}{p1=2;p2=2}{p1=3;p2=0}{p1=3;p2=1}{p1=3;p2=2}{p1=3;p2=3}{p1=4;p2=0}{p1=4;p2=1}{p1=4;p2=2}{p1=4;p2=3}{p1=4;p2=4}=>Formula@1.s;{p1=0;p2=1}{p1=0;p2=2}{p1=0;p2=3}{p1=0;p2=4}{p1=1;p2=2}{p1=1;p2=3}{p1=1;p2=4}{p1=2;p2=3}{p1=2;p2=4}{p1=3;p2=4}=>"("++(Formula@1.s++")")}!{p1=Formula@1.p;p2=1});p=1;a=};"Formula_0 -> Formula_1"; +lin Not:Formula.Formula=\Formula@0->{s="~"++table{p1:Ints 4;p2:Ints 4}{{p1=0;p2=0}{p1=1;p2=0}{p1=1;p2=1}{p1=2;p2=0}{p1=2;p2=1}{p1=2;p2=2}{p1=3;p2=0}{p1=3;p2=1}{p1=3;p2=2}{p1=3;p2=3}{p1=4;p2=0}{p1=4;p2=1}{p1=4;p2=2}{p1=4;p2=3}{p1=4;p2=4}=>Formula@0.s;{p1=0;p2=1}{p1=0;p2=2}{p1=0;p2=3}{p1=0;p2=4}{p1=1;p2=2}{p1=1;p2=3}{p1=1;p2=4}{p1=2;p2=3}{p1=2;p2=4}{p1=3;p2=4}=>"("++(Formula@0.s++")")}!{p1=Formula@0.p;p2=4};p=4;a=};"~ Formula_0"; +lin Or:Formula.Formula=\Formula@0,Formula@1->{s=table{p1:Ints 4;p2:Ints 4}{{p1=0;p2=0}{p1=1;p2=0}{p1=1;p2=1}{p1=2;p2=0}{p1=2;p2=1}{p1=2;p2=2}{p1=3;p2=0}{p1=3;p2=1}{p1=3;p2=2}{p1=3;p2=3}{p1=4;p2=0}{p1=4;p2=1}{p1=4;p2=2}{p1=4;p2=3}{p1=4;p2=4}=>Formula@0.s;{p1=0;p2=1}{p1=0;p2=2}{p1=0;p2=3}{p1=0;p2=4}{p1=1;p2=2}{p1=1;p2=3}{p1=1;p2=4}{p1=2;p2=3}{p1=2;p2=4}{p1=3;p2=4}=>"("++(Formula@0.s++")")}!{p1=Formula@0.p;p2=2}++("v"++table{p1:Ints 4;p2:Ints 4}{{p1=0;p2=0}{p1=1;p2=0}{p1=1;p2=1}{p1=2;p2=0}{p1=2;p2=1}{p1=2;p2=2}{p1=3;p2=0}{p1=3;p2=1}{p1=3;p2=2}{p1=3;p2=3}{p1=4;p2=0}{p1=4;p2=1}{p1=4;p2=2}{p1=4;p2=3}{p1=4;p2=4}=>Formula@1.s;{p1=0;p2=1}{p1=0;p2=2}{p1=0;p2=3}{p1=0;p2=4}{p1=1;p2=2}{p1=1;p2=3}{p1=1;p2=4}{p1=2;p2=3}{p1=2;p2=4}{p1=3;p2=4}=>"("++(Formula@1.s++")")}!{p1=Formula@1.p;p2=3});p=2;a=};"Formula_0 v Formula_1"; +lincat Term={s:Str;p:Ints 4;a:Precedence.PAssoc}={s=str@0;p=0;a=};"Term"; +} +abstract Formula={flags modulesize=n10;fun A:Formula.Formula={}; +fun Abs:Formula.Formula={}; +fun And:(h_:Formula.Formula)->(h_:Formula.Formula)->Formula.Formula={}; +fun B:Formula.Formula={}; +fun C:Formula.Formula={}; +cat Formula[]=; +fun If:(h_:Formula.Formula)->(h_:Formula.Formula)->Formula.Formula={}; +fun Not:(h_:Formula.Formula)->Formula.Formula={}; +fun Or:(h_:Formula.Formula)->(h_:Formula.Formula)->Formula.Formula={}; +cat Term[]=; +} +resource Precedence=open Predef in{flags modulesize=n1;param PAssoc=PN|PL|PR; +} +resource Prelude=open Predef in{flags modulesize=n2;param Bool=True|False; +param ENumber=E0|E1|E2|Emore; +} +resource Predef={flags modulesize=n1;param PBool=PTrue|PFalse; +} diff --git a/examples/systemS/test.gfs b/examples/systemS/test.gfs new file mode 100644 index 000000000..db5e64cbf --- /dev/null +++ b/examples/systemS/test.gfs @@ -0,0 +1,7 @@ +i proof.gfcm +rf ex1.txt | p -tr -lang=ProofSymb | l -lang=ProofEng +rf ex2.txt | p -tr -lang=ProofSymb | l -lang=ProofEng +rf ex4.txt | p -tr -lang=ProofSymb | l -lang=ProofEng +rf ex1eng.txt | p -tr -lang=ProofEng | l -lang=ProofSymb +rf ex2eng.txt | p -tr -lang=ProofEng | l -lang=ProofSymb +rf ex4eng.txt | p -tr -lang=ProofEng | l -lang=ProofSymb