38df2bfbe2de19e549aa812bab7c79fcf869b308Till MossakowskiDescription : Derive induction schemes from sort generation constraints
aabc0d2680ea5411d5a9c82c1b2ca1f4144ca18fRainer GrabbeCopyright : (c) Till Mossakowski, Rainer Grabbe and Uni Bremen 2002-2006
98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu ProdescuLicense : GPLv2 or higher, see LICENSE.txt
2eeec5240b424984e3ee26296da1eeab6c6d739eChristian MaederMaintainer : till@informatik.uni-bremen.de
38df2bfbe2de19e549aa812bab7c79fcf869b308Till MossakowskiStability : provisional
38df2bfbe2de19e549aa812bab7c79fcf869b308Till MossakowskiPortability : portable
38df2bfbe2de19e549aa812bab7c79fcf869b308Till MossakowskiWe provide both second-order induction schemes as well as their
38df2bfbe2de19e549aa812bab7c79fcf869b308Till Mossakowskiinstantiation to specific first-order formulas.
6baa40b661fa23201bf185527f0416006d55f5cdmcodescumodule CASL.Induction (inductionScheme, generateInductionLemmas, substitute) where
baef5e750fbc19bad340a3293a17ba34d4fabbedChristian Maederimport CASL.Quantification (flatVAR_DECLs)
8b66de47c89e252c907c8ed3a5ccd16dbccbfb3eChristian Maederimport Common.Utils (combine, number)
8b0bd90bc649e740c134ad0946e0d0409c3c96e6Christian Maederimport qualified Data.Set as Set
2df21ee905717748894ce0d1b775b2a01bef4a44Christian Maeder{- | derive a second-order induction scheme from a sort generation constraint
2df21ee905717748894ce0d1b775b2a01bef4a44Christian Maederthe second-order predicate variables are represented as predicate
2df21ee905717748894ce0d1b775b2a01bef4a44Christian Maedersymbols P[s], where s is a sort -}
8b0bd90bc649e740c134ad0946e0d0409c3c96e6Christian MaederinductionScheme :: FormExtension f => [Constraint] -> FORMULA f
38df2bfbe2de19e549aa812bab7c79fcf869b308Till MossakowskiinductionScheme constrs =
baef5e750fbc19bad340a3293a17ba34d4fabbedChristian Maeder induction $ map predSubst constrs
f64563593a58e0e9de073c21ae69a1a877cb4692Till Mossakowski where sorts = map newSort constrs
e194ab763147ac5df9c02fe40bdb5172013c36e8Christian Maeder injective = isInjectiveList sorts
baef5e750fbc19bad340a3293a17ba34d4fabbedChristian Maeder predSubst constr =
baef5e750fbc19bad340a3293a17ba34d4fabbedChristian Maeder (constr, \ t -> Predication predSymb [t] nullRange)
7b7ca7ef1ad99f1da0057cb8a6aa68cf6d04359bTill Mossakowski predSymb = Qual_pred_name ident typ nullRange
f7fe363b4d668402d4a604727418e99a48abf533Christian Maeder Id ts cs ps =
f7fe363b4d668402d4a604727418e99a48abf533Christian Maeder if injective then newSort constr else origSort constr
f7fe363b4d668402d4a604727418e99a48abf533Christian Maeder ident = Id [mkSimpleId $ genNamePrefix ++ "P_"
f7fe363b4d668402d4a604727418e99a48abf533Christian Maeder ++ showId (Id ts [] ps) ""] cs ps
38df2bfbe2de19e549aa812bab7c79fcf869b308Till Mossakowski typ = Pred_type [newSort constr] nullRange
2df21ee905717748894ce0d1b775b2a01bef4a44Christian Maeder{- | Function for derivation of first-order instances of sort generation
2df21ee905717748894ce0d1b775b2a01bef4a44Christian MaederGiven a list of formulas with a free sorted variable, instantiate the
2df21ee905717748894ce0d1b775b2a01bef4a44Christian Maedersort generation constraint for this list of formulas
2df21ee905717748894ce0d1b775b2a01bef4a44Christian MaederIt is assumed that the (original) sorts of the constraint
2df21ee905717748894ce0d1b775b2a01bef4a44Christian Maedermatch the sorts of the free variables -}
8b0bd90bc649e740c134ad0946e0d0409c3c96e6Christian MaederinstantiateSortGen :: FormExtension f
8b0bd90bc649e740c134ad0946e0d0409c3c96e6Christian Maeder => [(Constraint, (FORMULA f, (VAR, SORT)))] -> FORMULA f
baef5e750fbc19bad340a3293a17ba34d4fabbedChristian MaederinstantiateSortGen phis =
baef5e750fbc19bad340a3293a17ba34d4fabbedChristian Maeder induction (map substFormula phis)
7f4e941c6b36ee1f694734bb35d82e395a2796b5Christian Maeder where substFormula (c, (phi, (v, s))) = (c, \ t -> substitute v s t phi)
f57279093718fac174b661b128d03b5049ac467cTill Mossakowski-- | substitute a term for a variable in a formula
8b0bd90bc649e740c134ad0946e0d0409c3c96e6Christian Maedersubstitute :: FormExtension f => VAR -> SORT -> TERM f -> FORMULA f -> FORMULA f
7f4e941c6b36ee1f694734bb35d82e395a2796b5Christian Maedersubstitute v s t = foldFormula
7f4e941c6b36ee1f694734bb35d82e395a2796b5Christian Maeder (mapRecord id) { foldQual_var = \ t2 v2 s2 _ ->
7f4e941c6b36ee1f694734bb35d82e395a2796b5Christian Maeder if v == v2 && s == s2 then t else t2
66c74e6bb78d2c417fd8495b5dd267c6bd0acd5aChristian Maeder , foldQuantification = \ t2 q vs p r ->
7f4e941c6b36ee1f694734bb35d82e395a2796b5Christian Maeder if elem (v, s) $ flatVAR_DECLs vs
66c74e6bb78d2c417fd8495b5dd267c6bd0acd5aChristian Maeder then t2 else Quantification q vs p r
2df21ee905717748894ce0d1b775b2a01bef4a44Christian Maeder{- | derive an induction scheme from a sort generation constraint
2df21ee905717748894ce0d1b775b2a01bef4a44Christian Maederusing substitutions as induction predicates -}
8b0bd90bc649e740c134ad0946e0d0409c3c96e6Christian Maederinduction :: FormExtension f => [(Constraint, TERM f -> FORMULA f)] -> FORMULA f
2df21ee905717748894ce0d1b775b2a01bef4a44Christian Maederinduction constrSubsts =
baef5e750fbc19bad340a3293a17ba34d4fabbedChristian Maeder let mkVar i = mkSimpleId ("x_" ++ show i)
33185a20196bfe66410ce6e9449005f5680a1656Christian Maeder sortInfo = map (\ ((cs, sub), i) -> (sub, (mkVar i, newSort cs)))
8b66de47c89e252c907c8ed3a5ccd16dbccbfb3eChristian Maeder $ number constrSubsts
33185a20196bfe66410ce6e9449005f5680a1656Christian Maeder mkConclusion (subst, v) =
3a2de7e5a3c5da0a96c9563617ab332685a41cedChristian Maeder mkForall [uncurry mkVarDecl v] $ subst $ uncurry mkVarTerm v
1e56499b4f29cca2c2a8aa47183a4fc248ed29e3Christian Maeder inductionConclusion = conjunct $ map mkConclusion sortInfo
33185a20196bfe66410ce6e9449005f5680a1656Christian Maeder inductionPremises = map (mkPrems $ map snd constrSubsts) constrSubsts
2df21ee905717748894ce0d1b775b2a01bef4a44Christian Maeder inductionPremise = conjunct $ concat inductionPremises
2df21ee905717748894ce0d1b775b2a01bef4a44Christian Maeder in mkImpl inductionPremise inductionConclusion
2df21ee905717748894ce0d1b775b2a01bef4a44Christian Maeder{- | construct premise set for the induction scheme
2df21ee905717748894ce0d1b775b2a01bef4a44Christian Maederfor one sort in the constraint -}
8b0bd90bc649e740c134ad0946e0d0409c3c96e6Christian MaedermkPrems :: FormExtension f => [TERM f -> FORMULA f]
33185a20196bfe66410ce6e9449005f5680a1656Christian Maeder -> (Constraint, TERM f -> FORMULA f) -> [FORMULA f]
33185a20196bfe66410ce6e9449005f5680a1656Christian MaedermkPrems substs (constr, sub) = map (mkPrem substs sub) (opSymbs constr)
7b7ca7ef1ad99f1da0057cb8a6aa68cf6d04359bTill Mossakowski-- | construct a premise for the induction scheme for one constructor
8b0bd90bc649e740c134ad0946e0d0409c3c96e6Christian MaedermkPrem :: FormExtension f => [TERM f -> FORMULA f] -> (TERM f -> FORMULA f)
33185a20196bfe66410ce6e9449005f5680a1656Christian Maeder -> (OP_SYMB, [Int]) -> FORMULA f
33185a20196bfe66410ce6e9449005f5680a1656Christian MaedermkPrem substs subst (opSym@(Qual_op_name _ (Op_type _ argTypes _ _) _), idx) =
3a2de7e5a3c5da0a96c9563617ab332685a41cedChristian Maeder mkForall qVars phi
ead4d317053c9092c59a16de66cac61f619a1293Christian Maeder qVars = map (\ (a, i) -> mkVarDeclStr ("y_" ++ show i) a) $ number argTypes
f64563593a58e0e9de073c21ae69a1a877cb4692Till Mossakowski phi = if null indHyps then indConcl
1e56499b4f29cca2c2a8aa47183a4fc248ed29e3Christian Maeder else mkImpl (conjunct indHyps) indConcl
ead4d317053c9092c59a16de66cac61f619a1293Christian Maeder indConcl = subst $ mkAppl opSym $ map toQualVar qVars
7857e6ac0ed79540893dcb3e22af571ab2894932Till Mossakowski indHyps = mapMaybe indHyp (zip qVars idx)
baef5e750fbc19bad340a3293a17ba34d4fabbedChristian Maeder indHyp (v1, i) =
baef5e750fbc19bad340a3293a17ba34d4fabbedChristian Maeder if i < 0 then Nothing -- leave out sorts from outside the constraint
ead4d317053c9092c59a16de66cac61f619a1293Christian Maeder else Just $ (substs !! i) $ toQualVar v1
baef5e750fbc19bad340a3293a17ba34d4fabbedChristian MaedermkPrem _ _ (opSym, _) =
2df21ee905717748894ce0d1b775b2a01bef4a44Christian Maeder error ("CASL.Induction. mkPrems: "
f64563593a58e0e9de073c21ae69a1a877cb4692Till Mossakowski ++ "unqualified operation symbol occuring in constraint: "
f64563593a58e0e9de073c21ae69a1a877cb4692Till Mossakowski ++ show opSym)
33185a20196bfe66410ce6e9449005f5680a1656Christian Maeder-- | for goals try to generate additional implications based on induction
8b0bd90bc649e740c134ad0946e0d0409c3c96e6Christian MaedergenerateInductionLemmas :: FormExtension f => Bool
8b0bd90bc649e740c134ad0946e0d0409c3c96e6Christian Maeder -> (Sign f e, [Named (FORMULA f)]) -> (Sign f e, [Named (FORMULA f)])
8b0bd90bc649e740c134ad0946e0d0409c3c96e6Christian MaedergenerateInductionLemmas b (sig, sens) = let
2df21ee905717748894ce0d1b775b2a01bef4a44Christian Maeder sortGens = foldr (\ s cs -> case sentence s of
2df21ee905717748894ce0d1b775b2a01bef4a44Christian Maeder Sort_gen_ax c _ -> c : cs
2df21ee905717748894ce0d1b775b2a01bef4a44Christian Maeder _ -> cs) [] axs
8b0bd90bc649e740c134ad0946e0d0409c3c96e6Christian Maeder (axs, goals) = partition isAxiom sens
8b0bd90bc649e740c134ad0946e0d0409c3c96e6Christian Maeder in (sig, (if b then sens else axs)
8b0bd90bc649e740c134ad0946e0d0409c3c96e6Christian Maeder ++ generateInductionLemmasAux b sortGens goals)
ecf4047143afe26a351e9fb60827671bf5e2e30dChristian MaedergenerateInductionLemmasAux
8b0bd90bc649e740c134ad0946e0d0409c3c96e6Christian Maeder :: FormExtension f => Bool
8b0bd90bc649e740c134ad0946e0d0409c3c96e6Christian Maeder -- ^ if True create additional implication otherwise replace goals
8b0bd90bc649e740c134ad0946e0d0409c3c96e6Christian Maeder -> [[Constraint]] -- ^ the constraints of a theory
ecf4047143afe26a351e9fb60827671bf5e2e30dChristian Maeder -> [AS_Anno.Named (FORMULA f)] -- ^ all goals of a theory
2df21ee905717748894ce0d1b775b2a01bef4a44Christian Maeder -> [AS_Anno.Named (FORMULA f)]
2df21ee905717748894ce0d1b775b2a01bef4a44Christian Maeder{- ^ all the generated induction lemmas
2df21ee905717748894ce0d1b775b2a01bef4a44Christian Maederand the labels are derived from the goal-names -}
8b0bd90bc649e740c134ad0946e0d0409c3c96e6Christian MaedergenerateInductionLemmasAux b sort_gen_axs goals = let
aabc0d2680ea5411d5a9c82c1b2ca1f4144ca18fRainer Grabbe findVar s [] = error ("CASL.generateInductionLemmas:\n"
f7fe363b4d668402d4a604727418e99a48abf533Christian Maeder ++ "No VAR found of SORT " ++ show s ++ "!")
f7fe363b4d668402d4a604727418e99a48abf533Christian Maeder findVar s ((vl, sl) : lst) = if s == sl then vl else findVar s lst
aabc0d2680ea5411d5a9c82c1b2ca1f4144ca18fRainer Grabbe removeVarsort v s f = case f of
4332f307777b02f460ab77a5dfade89628cbc215Rainer Grabbe Quantification Universal varDecls formula rng ->
4332f307777b02f460ab77a5dfade89628cbc215Rainer Grabbe let vd' = newVarDecls varDecls
2df21ee905717748894ce0d1b775b2a01bef4a44Christian Maeder in if null vd' then formula
4332f307777b02f460ab77a5dfade89628cbc215Rainer Grabbe else Quantification Universal vd' formula rng
4332f307777b02f460ab77a5dfade89628cbc215Rainer Grabbe newVarDecls = filter (\ (Var_decl vs _ _) -> not $ null vs) .
4332f307777b02f460ab77a5dfade89628cbc215Rainer Grabbe map (\ var_decl@(Var_decl vars varsort r) ->
baef5e750fbc19bad340a3293a17ba34d4fabbedChristian Maeder if varsort == s
33185a20196bfe66410ce6e9449005f5680a1656Christian Maeder then Var_decl (filter (/= v) vars) s r
4332f307777b02f460ab77a5dfade89628cbc215Rainer Grabbe else var_decl)
8b0bd90bc649e740c134ad0946e0d0409c3c96e6Christian Maeder (uniQuantGoals, restGoals) =
8b0bd90bc649e740c134ad0946e0d0409c3c96e6Christian Maeder foldr ( \ goal (ul, rl) -> case sentence goal of
1626d36d680e01037b6ee7ba66925a1d61eebbe9Christian Maeder Quantification Universal varDecl _ _ ->
1626d36d680e01037b6ee7ba66925a1d61eebbe9Christian Maeder ((goal, flatVAR_DECLs varDecl) : ul, rl)
1626d36d680e01037b6ee7ba66925a1d61eebbe9Christian Maeder _ -> (ul, goal : rl)) ([], []) goals
2df21ee905717748894ce0d1b775b2a01bef4a44Christian Maeder {- For each constraint we get a list of goals out of uniQuantGoals
2df21ee905717748894ce0d1b775b2a01bef4a44Christian Maeder which contain the constraint's newSort. Afterwards all combinations
2df21ee905717748894ce0d1b775b2a01bef4a44Christian Maeder are created. -}
baef5e750fbc19bad340a3293a17ba34d4fabbedChristian Maeder constraintGoals = combine
baef5e750fbc19bad340a3293a17ba34d4fabbedChristian Maeder . map (\ c -> filter (any ((newSort c ==) . snd) . snd)
baef5e750fbc19bad340a3293a17ba34d4fabbedChristian Maeder uniQuantGoals)
8b0bd90bc649e740c134ad0946e0d0409c3c96e6Christian Maeder {- returns big list containing tuples of constraints and a matching
8b0bd90bc649e740c134ad0946e0d0409c3c96e6Christian Maeder combination (list) of goals. -}
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder concatMap (\ c -> map (\ combi -> (c, combi)) $ constraintGoals c)
1626d36d680e01037b6ee7ba66925a1d61eebbe9Christian Maeder singleDts = map head $ filter isSingle sort_gen_axs
1626d36d680e01037b6ee7ba66925a1d61eebbe9Christian Maeder indSorts = Set.fromList $ map newSort singleDts
1626d36d680e01037b6ee7ba66925a1d61eebbe9Christian Maeder (simpleIndGoals, rest2) = foldr (\ (gs, vs) (ul, rl) ->
1626d36d680e01037b6ee7ba66925a1d61eebbe9Christian Maeder case dropWhile (not . (`Set.member` indSorts) . snd) vs of
1626d36d680e01037b6ee7ba66925a1d61eebbe9Christian Maeder [] -> (ul, gs : rl)
1626d36d680e01037b6ee7ba66925a1d61eebbe9Christian Maeder (v, s) : _ -> case find ((== s) . newSort) singleDts of
1626d36d680e01037b6ee7ba66925a1d61eebbe9Christian Maeder Nothing -> (ul, gs : rl)
1626d36d680e01037b6ee7ba66925a1d61eebbe9Christian Maeder Just c -> ((gs, (v, s), c) : ul, rl)) ([], []) uniQuantGoals
1626d36d680e01037b6ee7ba66925a1d61eebbe9Christian Maeder toIndPrem (gs, (v, s), c) =
1626d36d680e01037b6ee7ba66925a1d61eebbe9Christian Maeder let f = removeVarsort v s $ sentence gs
1626d36d680e01037b6ee7ba66925a1d61eebbe9Christian Maeder sb t = substitute v s t f
1626d36d680e01037b6ee7ba66925a1d61eebbe9Christian Maeder ps = mkPrems [sb] (c, sb)
1626d36d680e01037b6ee7ba66925a1d61eebbe9Christian Maeder in gs { sentence = conjunct ps }
8b0bd90bc649e740c134ad0946e0d0409c3c96e6Christian Maeder map (\ (cons, formulas) ->
8b0bd90bc649e740c134ad0946e0d0409c3c96e6Christian Maeder let formula = instantiateSortGen
8b0bd90bc649e740c134ad0946e0d0409c3c96e6Christian Maeder $ map (\ (c, (f, varsorts)) ->
8b0bd90bc649e740c134ad0946e0d0409c3c96e6Christian Maeder let s = newSort c
8b0bd90bc649e740c134ad0946e0d0409c3c96e6Christian Maeder vs = findVar s varsorts
8b0bd90bc649e740c134ad0946e0d0409c3c96e6Christian Maeder in (c, (removeVarsort vs s $ sentence f, (vs, s))))
8b0bd90bc649e740c134ad0946e0d0409c3c96e6Christian Maeder $ zip cons formulas
f63170ab2ed53197f50e4575383e7981189c87dcChristian Maeder sName = tail $ concatMap (('_' :) . senAttr . fst) formulas
f63170ab2ed53197f50e4575383e7981189c87dcChristian Maeder ++ "_induction"
8b0bd90bc649e740c134ad0946e0d0409c3c96e6Christian Maeder in makeNamed sName formula
1626d36d680e01037b6ee7ba66925a1d61eebbe9Christian Maeder else map toIndPrem simpleIndGoals ++ rest2 ++ restGoals