From a5232f7e5b8f6ca988696f3870f019113edb8d90 Mon Sep 17 00:00:00 2001
From: aarne <aarne@cs.chalmers.se>
Date: Mon, 27 Nov 2006 10:54:26 +0000
Subject: part of Logic implemented generically

---
 examples/logic/LogicI.gf | 44 ++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 44 insertions(+)
 create mode 100644 examples/logic/LogicI.gf

(limited to 'examples/logic/LogicI.gf')

diff --git a/examples/logic/LogicI.gf b/examples/logic/LogicI.gf
new file mode 100644
index 000000000..c9c374622
--- /dev/null
+++ b/examples/logic/LogicI.gf
@@ -0,0 +1,44 @@
+incomplete concrete LogicI of Logic = 
+  open 
+    LexTheory,
+    Prooftext, 
+    Grammar, 
+    Constructors, 
+    Combinators 
+  in {
+
+lincat 
+  Prop  = Prooftext.Prop ;
+  Proof = Prooftext.Proof ;
+  Dom   = Typ ;
+  Elem  = Object ;
+  Hypo  = Label ;
+  Text  = Section ;
+
+lin
+  Disj A B = coord or_Conj A B ;
+  Impl A B = coord ifthen_DConj A B ;
+
+  Abs = mkS (pred have_V2 (mkNP we_Pron) (mkNP (mkDet IndefArt) contradiction_N)) ;
+
+  DisjIl A B a = proof a (proof afortiori (coord or_Conj A B)) ;
+  DisjIr A B b = proof b (proof afortiori (coord or_Conj A B)) ;
+
+  DisjE A B C c b1 b2 =
+    appendText
+      c 
+      (appendText
+        (appendText
+           (cases (mkNum n2)) 
+           (proofs 
+             (appendText (assumption A) b1)
+             (appendText (assumption B) b2)))
+        (proof therefore C)) ;
+
+  ImplI A B b = 
+    proof (assumption A) (appendText b (proof therefore (coord ifthen_DConj A B))) ;
+
+  Hypoth A h = proof hypothesis A ;
+
+
+}
\ No newline at end of file
-- 
cgit v1.2.3