Changeset 10619 for trunk/Comorphisms/CspCASL2IsabelleHOL.hs
- Timestamp:
- 01.09.2008 18:29:05 (15 months ago)
- Files:
-
- 1 modified
-
trunk/Comorphisms/CspCASL2IsabelleHOL.hs (modified) (15 diffs)
Legend:
- Unmodified
- Added
- Removed
-
trunk/Comorphisms/CspCASL2IsabelleHOL.hs
r10574 r10619 30 30 import CspCASL.AS_CspCASL 31 31 import CspCASL.Trans_CspProver 32 import CspCASL.Trans_Consts 32 33 import CspCASL.SignCSP 33 34 import qualified Data.List as List … … 88 89 -- Next add the preAlpabet construction to the IsabelleHOL code 89 90 return $ addCspCaslSentences ccSens 91 $ addAllIntegrationTheorems sortList ccSign 90 92 $ addAllChooseFunctions sortList 91 93 $ addAllBarTypes sortList … … 107 109 -- | Add a list of CspCASL sentences to an Isabelle theory 108 110 addCspCaslSentences :: [Named CspCASLSentence] -> IsaTheory -> IsaTheory 109 addCspCaslSentences namedSens isaTh = foldl addCspCaslSentence isaTh namedSens 111 addCspCaslSentences namedSens isaTh = 112 -- Create datatype for process names 113 -- crate constant 114 -- create primrec 115 -- create list of equations -- one for each sentence 116 foldl addCspCaslSentence isaTh namedSens 110 117 111 118 -- | Add a single CspCASL sentence to an Isabelle theory … … 211 218 test1 = if (sort == sort') then [binEq x y] else [] 212 219 test2 = if (Set.member sort sort'SuperSet) 213 then [binEq x ( termAppl (getInjectionOp sort' sort)y)]220 then [binEq x (mkInjection sort' sort y)] 214 221 else [] 215 222 test3 = if (Set.member sort' sortSuperSet) 216 then [binEq ( termAppl (getInjectionOp sort sort')x) y]223 then [binEq (mkInjection sort sort' x) y] 217 224 else [] 218 225 test4 = if (null commonSuperList) 219 226 then [] 220 227 else map test4_atSort commonSuperList 221 test4_atSort s = binEq ( termAppl (getInjectionOp sort s)x)222 ( termAppl (getInjectionOp sort' s)y)228 test4_atSort s = binEq (mkInjection sort s x) 229 (mkInjection sort' s y) 223 230 in binEq lhs rhs 224 231 eqs = map mkEq sortList … … 293 300 let x = mkFree "x" 294 301 y = mkFree "y" 295 injOp = getInjectionOp s1 s2 296 injX = termAppl injOp x 297 injY = termAppl injOp y 302 injX = mkInjection s1 s2 x 303 injY = mkInjection s1 s2 y 298 304 definedOp_s1 = getDefinedOp sorts s1 299 305 definedOp_s2 = getDefinedOp sorts s2 … … 339 345 addDecompositionTheorem pfolSign sorts sortRel isaTh (s1,s2,s3) = 340 346 let x = mkFree "x" 341 injOp_s1_s2 = getInjectionOp s1 s2 342 injOp_s2_s3 = getInjectionOp s2 s3 343 injOp_s1_s3 = getInjectionOp s1 s3 344 inj_s1_s2_s3 = termAppl injOp_s2_s3 (termAppl injOp_s1_s2 x) 345 inj_s1_s3 = termAppl injOp_s1_s3 x 347 -- These 5 lines make use of currying 348 injOp_s1_s2 = mkInjection s1 s2 349 injOp_s2_s3 = mkInjection s2 s3 350 injOp_s1_s3 = mkInjection s1 s3 351 inj_s1_s2_s3_x = injOp_s2_s3 (injOp_s1_s2 x) 352 inj_s1_s3_x = injOp_s1_s3 x 353 346 354 definedOp_s1 = getDefinedOp sorts s1 347 355 definedOp_s3 = getDefinedOp sorts s3 … … 352 360 name = getDecompositionThmName(s1, s2, s3) 353 361 conds = [] 354 concl = binEq inj_s1_s2_s3 inj_s1_s3355 356 proof' = IsaProof [Apply(CaseTac (definedOp_s3 inj_s1_s2_s3 )),362 concl = binEq inj_s1_s2_s3_x inj_s1_s3_x 363 364 proof' = IsaProof [Apply(CaseTac (definedOp_s3 inj_s1_s2_s3_x)), 357 365 -- Case 1 358 366 Apply(SubgoalTac(definedOp_s1 x)), … … 363 371 -- Case 2 364 372 Apply(SubgoalTac( 365 termAppl notOp(definedOp_s3 inj_s1_s3 ))),373 termAppl notOp(definedOp_s3 inj_s1_s3_x))), 366 374 Apply(SimpAdd Nothing collectionNotDefBotAx), 367 375 Apply(SimpAdd Nothing collectionTotAx)] … … 473 481 addAllChooseFunctions :: [SORT] -> IsaTheory -> IsaTheory 474 482 addAllChooseFunctions sorts isaTh = 475 foldl addChooseFunctions isaTh sorts 483 let isaTh' = foldl addChooseFunction isaTh sorts --add function and def 484 in foldl addChooseFunctionLemma isaTh' sorts --add theorem and proof 476 485 477 486 -- | Add a single choose function for a given sort to an Isabelle … … 479 488 -- consts choose_Nat :: "Alphabet => Nat" 480 489 -- defs choose_Nat_def: "choose_Nat x == contents{y . class(C_Nat y) = x}" 481 482 addChooseFunctions :: IsaTheory -> SORT -> IsaTheory 483 addChooseFunctions isaTh sort = 490 addChooseFunction :: IsaTheory -> SORT -> IsaTheory 491 addChooseFunction isaTh sort = 484 492 let --constant 485 493 alphabetType = Type {typeId = alphabetS, 486 typeSort = [], 487 typeArgs =[]} 488 sortType = Type {typeId = convertSort2String sort, typeSort = [], 489 typeArgs =[]} 494 typeSort = [], 495 typeArgs =[]} 496 sortType = Type {typeId = convertSort2String sort, 497 typeSort = [], 498 typeArgs =[]} 490 499 chooseFunName = mkChooseFunName sort 491 500 chooseFunType = mkFunType alphabetType sortType … … 500 509 lhs = chooseOp x 501 510 rhs = contentsOp (Set subset) 511 in addDef chooseFunName lhs rhs -- Add defintion to theory 512 $ addConst chooseFunName chooseFunType isaTh -- Add constant to theory 513 514 -- | Add a single choose function lemma for a given sort to an 515 -- Isabelle theory. The following Isabelle code is produced by this 516 -- function: lemma "choose_Nat (class (C_Nat x)) = x". The proof is 517 -- also produced. 518 519 addChooseFunctionLemma :: IsaTheory -> SORT -> IsaTheory 520 addChooseFunctionLemma isaTh sort = 521 let sortType = Type {typeId = convertSort2String sort, 522 typeSort = [], 523 typeArgs =[]} 524 chooseFunName = mkChooseFunName sort 525 x = mkFree "x" 526 y = mkFree "y" 527 chooseOp = termAppl (conDouble chooseFunName) 528 sortConsOp = termAppl (conDouble (mkPreAlphabetConstructor sort)) 502 529 -- theorm 503 530 subgoalTacTermLhsBinEq = binEq (classOp $ sortConsOp y) … … 516 543 Apply(Auto)] 517 544 Done 518 in addThreomWithProof chooseFunName thmConds thmConcl proof' -- Add theorem 519 $ addDef chooseFunName lhs rhs -- Add defintion to theory 520 $ addConst chooseFunName chooseFunType isaTh -- Add constant to theory 545 in addThreomWithProof chooseFunName thmConds thmConcl proof' isaTh 546 547 -- | Add all the integration theorems. We need to know all the sorts 548 -- to produce all the theorems. 549 addAllIntegrationTheorems :: [SORT] -> CspCASLSign -> IsaTheory -> IsaTheory 550 addAllIntegrationTheorems sorts ccSign isaTh = 551 let pairs = [(s1,s2) | s1 <- sorts, s2 <- sorts] 552 in foldl (addIntegrationTheorem_A ccSign) isaTh pairs 553 554 -- | Add Integration theorem A -- Compare to elements of the Alphabet. 555 -- We add the integration theorem based on the sorts of both 556 -- elements of the alphabet. We need to know the subsort relation to 557 -- find the highest common sort, but we pass in the CC signature for 558 -- use in function calls. 559 addIntegrationTheorem_A :: CspCASLSign -> IsaTheory -> (SORT,SORT) -> IsaTheory 560 addIntegrationTheorem_A ccSign isaTh (s1,s2) = 561 let sortRel = Rel.toList(CASLSign.sortRel ccSign) 562 s1SuperSet = CASLSign.supersortsOf s1 ccSign 563 s2SuperSet = CASLSign.supersortsOf s2 ccSign 564 commonSuperList = Set.toList (Set.intersection 565 (Set.insert s1 s1SuperSet) 566 (Set.insert s2 s2SuperSet)) 567 x = mkFree "x" 568 y = mkFree "y" 569 s1ConsOp = termAppl (conDouble (mkPreAlphabetConstructor s1)) 570 s2ConsOp = termAppl (conDouble (mkPreAlphabetConstructor s2)) 571 rhs = binEq (classOp $ s1ConsOp x) (classOp $ s2ConsOp y) 572 lhs = if (null commonSuperList) 573 then false 574 else 575 -- pick any common sort - we should pick the top most one. 576 let s' = head commonSuperList 577 in binEq (mkInjection s1 s' x) (mkInjection s2 s' y) 578 thmConds = [] 579 thmConcl = binEq rhs lhs 580 -- theorem names for proof 581 colInjThmNames = getColInjectivityThmName sortRel 582 colDecompThmNames = getColDecompositionThmName sortRel 583 proof' = IsaProof [Apply (SimpAdd Nothing ["quot_equality"]), 584 Apply (Other ("unfold " ++ preAlphabetSimS 585 ++ "_def")), 586 Apply (AutoSimpAdd Nothing 587 (colDecompThmNames ++ colInjThmNames))] 588 Done 589 in addThreomWithProof "IntegrationTheorem_A" thmConds thmConcl proof' isaTh 521 590 522 591 -- Function to help keep strings consistent … … 531 600 binEq_PreAlphabet = binVNameAppl eq_PreAlphabetV 532 601 533 alphabetS :: String534 alphabetS = "Alphabet"535 536 barExtS :: String537 barExtS = "_Bar"538 539 classS :: String540 classS = "class"541 542 classOp :: Term -> Term543 classOp = termAppl (conDouble classS)544 602 545 603 quotEqualityS :: String … … 574 632 equivTypeClassS = "equiv" 575 633 576 -- | Return the injection name of the injection from one sort to another 634 -- | Return the term representing the injection of a term from one sort to another 635 -- note: the term is returned if both sorts are the same 577 636 -- This function is not implemented in a satisfactory way 578 getInjectionOp :: SORT -> SORT-> Term579 getInjectionOp s s'=637 mkInjection :: SORT -> SORT -> Term -> Term 638 mkInjection s s' t = 580 639 let injName = getInjectionName s s' 581 640 replace string c s1 = concat (map (\x -> if x==c 582 641 then s1 583 642 else [x]) string) 584 in Const { 585 termName= VName { 586 new = ("X_" ++ injName), 587 altSyn = Just (AltSyntax ((replace injName '_' "'_") 588 ++ "/'(_')") [3] 999) 589 }, 590 termType = Hide { 591 typ = Type { 592 typeId ="dummy", 593 typeSort = [IsaClass "type"], 594 typeArgs = [] 595 }, 596 kon = NA, 597 arit= Nothing 598 } 599 } 600 643 injOp = Const { 644 termName= VName { 645 new = ("X_" ++ injName), 646 altSyn = Just (AltSyntax ((replace injName '_' "'_") 647 ++ "/'(_')") [3] 999) 648 }, 649 termType = Hide { 650 typ = Type { 651 typeId ="dummy", 652 typeSort = [IsaClass "type"], 653 typeArgs = [] 654 }, 655 kon = NA, 656 arit= Nothing 657 } 658 } 659 in if s == s' 660 then t 661 else termAppl injOp t 601 662 602 663 -- | Return the name of the injection as it is used in the alternative … … 706 767 in map mkNotDefBotAxName [0 .. (length(sorts) - 1)] 707 768 708 -- Convert a SORT to a string709 convertSort2String :: SORT -> String710 convertSort2String s = show s711 712 769 -- Function that returns the constructor of PreAlphabet for a given sort 713 770 mkPreAlphabetConstructor :: SORT -> String
