Changeset 12763
- Timestamp:
- 30.10.2009 17:15:43 (3 weeks ago)
- Files:
-
- 1 modified
-
trunk/CspCASLProver/Utils.hs (modified) (7 diffs)
Legend:
- Unmodified
- Added
- Removed
-
trunk/CspCASLProver/Utils.hs
r12762 r12763 41 41 import qualified Common.Lib.Rel as Rel 42 42 43 import Comorphisms.CASL2PCFOL (mkEmbInjName, mkTransAxiomName )43 import Comorphisms.CASL2PCFOL (mkEmbInjName, mkTransAxiomName, mkIdAxiomName) 44 44 import Comorphisms.CASL2SubCFOL (mkNotDefBotAxiomName, mkTotalityAxiomName) 45 45 … … 185 185 in addTransitivityTheorem sorts sortRel 186 186 $ addAllInjectivityTheorems pfolSign sorts sortRel 187 $ addAllDecompositionTheorem pfolSign sorts sortRel187 $ addAllDecompositionTheorem caslSign pfolSign sorts sortRel 188 188 $ addSymmetryTheorem sorts 189 189 $ addReflexivityTheorem … … 228 228 229 229 -- | Add all the decoposition theorems and proofs 230 addAllDecompositionTheorem :: CASLSign.CASLSign -> [SORT] -> [(SORT,SORT)] -> 231 IsaTheory -> IsaTheory 232 addAllDecompositionTheorem pfolSign sorts sortRel isaTh = 230 addAllDecompositionTheorem :: CASLSign.CASLSign -> CASLSign.CASLSign 231 -> [SORT] -> [(SORT,SORT)] 232 -> IsaTheory -> IsaTheory 233 addAllDecompositionTheorem caslSign pfolSign sorts sortRel isaTh = 233 234 let tripples = [(s1,s2,s3) | 234 235 (s1,s2) <- sortRel, (s2',s3) <- sortRel, s2==s2'] 235 in foldl (addDecompositionTheorem pfolSign sorts sortRel) isaTh tripples 236 in foldl (addDecompositionTheorem caslSign pfolSign sorts) 237 isaTh tripples 236 238 237 239 -- | Add the decomposition theorem and proof which should be deduced … … 241 243 -- inj_T_U(inj_S_T(x)) = inj_S_U(x). As a work around, we need to 242 244 -- know all sorts to pass them on. 243 addDecompositionTheorem :: CASLSign.CASLSign -> [SORT] -> [(SORT,SORT)] -> 244 IsaTheory -> (SORT,SORT,SORT) -> IsaTheory 245 addDecompositionTheorem pfolSign sorts sortRel isaTh (s1,s2,s3) = 245 addDecompositionTheorem :: CASLSign.CASLSign -> CASLSign.CASLSign -> [SORT] 246 -> IsaTheory -> (SORT,SORT,SORT) 247 -> IsaTheory 248 addDecompositionTheorem caslSign pfolSign sorts isaTh (s1,s2,s3) = 246 249 let x = mkFree "x" 247 250 -- These 5 lines make use of currying … … 254 257 definedOp_s1 = getDefinedOp sorts s1 255 258 definedOp_s3 = getDefinedOp sorts s3 256 collectionTransAx = getCollectionTransAx sortRel 259 collectionIdentityAx = getCollectionIdentityAx caslSign 260 collectionTransAx = getCollectionTransAx caslSign 257 261 collectionTotAx = getCollectionTotAx pfolSign 258 262 collectionNotDefBotAx = getCollectionNotDefBotAx sorts … … 265 269 -- Case 1 266 270 Apply[SubgoalTac(definedOp_s1 x)] False, 267 Apply[Insert collectionTransAx] False, 271 Apply[Insert (collectionIdentityAx 272 ++ collectionTransAx)] False, 268 273 Apply[Simp] False, 269 274 Apply[SimpAdd Nothing collectionTotAx] False, … … 845 850 -- | Return the list of strings of all the transitivity axioms names produced by 846 851 -- the translation CASL2PCFOL; CASL2SubCFOL. 847 getCollectionTransAx :: [(SORT,SORT)] -> [String] 848 getCollectionTransAx sortRel = 849 [mkTransAxiomName s1 s2 s3 850 | (s1,s2) <- sortRel, (s2',s3) <- sortRel, s2==s2'] 852 getCollectionTransAx :: CASLSign.CASLSign -> [String] 853 getCollectionTransAx caslSign = 854 let sorts = Set.toList $ CASLSign.sortSet caslSign 855 allSupers s s' s'' = 856 (Set.member s' $ CASLSign.supersortsOf s caslSign) && 857 (Set.member s'' $ CASLSign.supersortsOf s' caslSign) && (s /= s'') 858 in [mkTransAxiomName s s' s'' 859 | s <- sorts, s' <- sorts, s'' <- sorts, allSupers s s' s''] 860 861 -- | Return the list of strings of all the identity axioms names produced by 862 -- the translation CASL2PCFOL; CASL2SubCFOL. 863 getCollectionIdentityAx :: CASLSign.CASLSign -> [String] 864 getCollectionIdentityAx caslSign = 865 let sorts = Set.toList $ CASLSign.sortSet caslSign 866 isomorphic s s' = (Set.member s $ CASLSign.supersortsOf s' caslSign) && 867 (Set.member s' $ CASLSign.supersortsOf s caslSign) 868 in [mkIdAxiomName s s' | s <- sorts, s' <- sorts, isomorphic s s']
