Maxine branch

abelian_proof.py

@@ -7,13 +7,13 @@
 
 G = group('G','*')
 abelianG = forall(['x', 'y'], G, Eq(Mult(['x', 'y']), Mult(['y','x']),G))
-p = Proof('Simple Abelian Proof', forall(['x'], G, Eq(Mult(['x', 'x']), G.elements['e'],G)), goal=abelianG)
+p = Proof('Simple Abelian Proof', forall(['x'], G, Eq(Mult(['x', 'x']), Mult([G.elements['e']]),G)), goal=abelianG)
 p.introGroup(G)
 p.introElement(G,'a')
 p.introElement(G,'b')
 p.closure(G,'a','b')
-p.accessAssumption()
-p.forallElim(4,['a * b'])
+p.accessAssumption() # this and below one
+p.forallElim(4,['a * b']) # combine two steps
 p.leftMult('a',5)
 p.forallElim(4,['a'])
 p.substituteRHS(6,7)

element.py

@@ -34,6 +34,7 @@ def mult(self,other, group): # this is just for representation
         elif binOp in self.elementName and ')' != self.elementName[-1]:
             return "(" + self.elementName + ")" + binOp + other.elementName
         else:
+
             return self.elementName + binOp + other.elementName
 
     def addToGroup(self, group):

group.py

@@ -1,6 +1,6 @@
 exec(compile(source=open('element.py').read(), filename='element.py', mode='exec'))
-from logicObjects import identity, Mult, inverse
-
+from logicObjects import identity, Mult
+from element import *
 
 class group:
     # TRUTHS for all classes - need to add more here
@@ -15,7 +15,7 @@ class group:
     def __init__(self, name, binOp, additionalGroupProperties = None):
         self.groupName = name
         self.binaryOperator = binOp
-        self.elements.update({self.identity_identifier:Mult([identity(self)])})
+        self.elements.update({self.identity_identifier:identity(self)})
         if additionalGroupProperties != None:
             self.groupProperties.update(additionalGroupProperties)
 
@@ -41,7 +41,7 @@ def newInverse(self, elementName):
     # declare new element in group with elementName
     def newElement(self,elementName):
         if elementName not in self.elements:
-            self.elements.update({elementName:Mult([element(elementName,self)])})
+            self.elements.update({elementName:element(elementName,self)})
         else:
             print("Sorry, that element already exists!")
 
@@ -53,7 +53,7 @@ def mulElements(self, elem1, elem2): # should this return an equation?
             try:
                 gelem1 = self.elements[elem1]
                 gelem2 = self.elements[elem2]
-                result = gelem1 * gelem2 # need to specify which group we are multiplying in
+                result = Mult([gelem1 ,gelem2]) # need to specify which group we are multiplying in
                 self.elements.update({repr(result):result}) # is this the right?
             except:
                 print("Sorry, one or both of these elements are not in the group!")

inverse_of_ab.py

@@ -0,0 +1,26 @@
+from enum import unique
+from telnetlib import GA
+from proof import *
+from element import *
+from group import *
+from integer import *
+from logicObjects import *
+
+G = group('G','*')
+ab_inverse = forall(['a','b'], G, Eq(Mult([inverse('b',G),inverse('a',G)]),Mult([inverse(Mult(['a','b']),G)]),G))
+p = Proof('Inverse of ab Proof', assumption = None, goal = ab_inverse)
+p.introGroup(G)
+p.introElement(G,'a')
+p.introElement(G,'b')
+p.closure(G,'a','b')
+p.introInverse(G, Mult(['a','b']))
+p.rightMultInverse('b',4)
+p.inverseElimLHS(5)
+p.identleft(6)
+p.identright(7)
+p.rightMultInverse('a',8)
+p.inverseElimLHS(9)
+p.identleft(10)
+p.switchSidesOfEqual(11)
+p.forAllIntroduction(12,["a","b"],[1,2])
+p.qed(13)

logicObjects.py

@@ -31,7 +31,10 @@ def replace(self, var, expr):
         #print(self.products,var.products,expr.products)
         while i < len(self.products):
                 if self.products[i:i+len(var.products)] == var.products:
-                    new_products += expr.products
+                    if isinstance(expr,Mult):
+                        new_products += expr.products
+                    else:
+                        new_products.append(expr)
                     i+=len(var.products)
                 else:
                     new_products.append(self.products[i])
@@ -253,6 +256,11 @@ def __init__ (self, prpty, pg):
 
 ## Special types of elements/groups
 
+# class element_(element):
+#     def __init__(self, pg, elementName):
+#         elementName = elementName
+#         super().__init__(elementName, pg)
+
 class identity(element):
     def __init__(self, pg):
         elementName = pg.identity_identifier
@@ -264,12 +272,24 @@ def __init__(self, pg):
         pg.addElementProperty(idnty,elementName)
 
 class inverse(element):
-    def __init__(self, elementName, pg):
-        inverseName = '(' + elementName + ")^(-1)"
+    def __init__(self, object, pg):
+        if type(object) == str:
+            elementName = object
+            inverseName = elementName + "^(-1)"
+            # lhs = Mult([inverseName,pg.elements[object]])
+        else:
+            elementName = repr(object)
+            inverseName = "(" + elementName + ")" + "^(-1)"
+            # lhs = Mult([inverseName]+object.products)
         super().__init__(inverseName, pg)
-        lhs = Mult([inverseName,elementName]) # self or elementName?
-        rhs = Mult([pg.identity_identifier])
-        inverseEq = Eq(lhs,rhs,pg)
-        pg.addGroupProperty(inverseEq, "Inverse of " + elementName)
+        self.inverseName = inverseName
+        self.elementName = elementName
+    def __repr__(self):
+        return self.inverseName
+         # self or elementName?
+        # rhs = Mult([pg.identity_identifier])
+        # inverseEq = Eq(lhs,rhs,pg)
+        # pg.addGroupProperty(inverseEq, "Inverse of " + elementName)
+
 
 ## TO DO: class generator(element):