Induction.hs revision 3d3889e0cefcdce9b3f43c53aaa201943ac2e895
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
ca010363454de207082dfaa4b753531ce2a34551Christian MaederModule : $Header$
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian MaederDescription : Derive induction schemes from sort generation constraints
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian MaederCopyright : (c) Till Mossakowski, Rainer Grabbe and Uni Bremen 2002-2006
97018cf5fa25b494adffd7e9b4e87320dae6bf47Christian MaederLicense : GPLv2 or higher, see LICENSE.txt
3f69b6948966979163bdfe8331c38833d5d90ecdChristian MaederMaintainer : till@informatik.uni-bremen.de
ca010363454de207082dfaa4b753531ce2a34551Christian MaederStability : provisional
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian MaederPortability : portable
79d11c2e3ad242ebb241f5d4a5e98a674c0b986fChristian MaederWe provide both second-order induction schemes as well as their
ca010363454de207082dfaa4b753531ce2a34551Christian Maederinstantiation to specific first-order formulas.
ac142c1b088711f911018d8108a64be80b2f2a58Christian Maedermodule CASL.Induction (inductionScheme, generateInductionLemmas) where
ac142c1b088711f911018d8108a64be80b2f2a58Christian Maederimport CASL.Quantification (flatVAR_DECLs)
ca010363454de207082dfaa4b753531ce2a34551Christian Maederimport Common.Utils (combine, number)
53301de22afd7190981b363b57c48df86fcb50f7Christian Maederimport qualified Data.Set as Set
23f8d286586ff38a9e73052b2c7c04c62c5c638fChristian Maeder{- | derive a second-order induction scheme from a sort generation constraint
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maederthe second-order predicate variables are represented as predicate
962036a37b92afb04ac0725cde9f20e599c04c5fChristian Maedersymbols P[s], where s is a sort -}
e68f45f355ed9d4026ee9baff5aa75aa7c911cc2Christian MaederinductionScheme :: FormExtension f => [Constraint] -> FORMULA f
ad270004874ce1d0697fb30d7309f180553bb315Christian MaederinductionScheme constrs =
fc8c6570c7b4ee13f375eb607bed2290438573bfChristian Maeder induction $ map predSubst constrs
83cc27e4ca7cf1a4bb5f4a8df17d3e6d44e6f1eaChristian Maeder where sorts = map newSort constrs
53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder injective = isInjectiveList sorts
028f19cdb09d52bb2fd207399b6fa874540d1670Christian Maeder predSubst constr =
975642b989852fc24119c59cf40bc1af653608ffChristian Maeder (constr, \ t -> Predication predSymb [t] nullRange)
83cc27e4ca7cf1a4bb5f4a8df17d3e6d44e6f1eaChristian Maeder predSymb = Qual_pred_name ident typ nullRange
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder Id ts cs ps =
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder if injective then newSort constr else origSort constr
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder ident = Id [mkSimpleId $ genNamePrefix ++ "P_"
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder ++ showId (Id ts [] ps) ""] cs ps
fc8c6570c7b4ee13f375eb607bed2290438573bfChristian Maeder typ = Pred_type [newSort constr] nullRange
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder{- | Function for derivation of first-order instances of sort generation
53301de22afd7190981b363b57c48df86fcb50f7Christian MaederGiven a list of formulas with a free sorted variable, instantiate the
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maedersort generation constraint for this list of formulas
53301de22afd7190981b363b57c48df86fcb50f7Christian MaederIt is assumed that the (original) sorts of the constraint
53301de22afd7190981b363b57c48df86fcb50f7Christian Maedermatch the sorts of the free variables -}
0a39036fa485579a7b7c81cdd44a412392571927Christian MaederinstantiateSortGen :: FormExtension f
da2b959c50c95309d8eb8b24174249c2847e74b5Christian Maeder => [(Constraint, (FORMULA f, (VAR, SORT)))] -> FORMULA f
0a39036fa485579a7b7c81cdd44a412392571927Christian MaederinstantiateSortGen phis =
0a39036fa485579a7b7c81cdd44a412392571927Christian Maeder induction (map substFormula phis)
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder where substFormula (c, (phi, (v, s))) = (c, \ t -> substitute v s t phi)
962036a37b92afb04ac0725cde9f20e599c04c5fChristian Maeder-- | substitute a term for a variable in a formula
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maedersubstitute :: FormExtension f => VAR -> SORT -> TERM f -> FORMULA f -> FORMULA f
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maedersubstitute v s t = foldFormula
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder (mapRecord id) { foldQual_var = \ t2 v2 s2 _ ->
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder if v == v2 && s == s2 then t else t2
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder , foldQuantification = \ t2 q vs p r ->
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder if elem (v, s) $ flatVAR_DECLs vs
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder then t2 else Quantification q vs p r
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder{- | derive an induction scheme from a sort generation constraint
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maederusing substitutions as induction predicates -}
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maederinduction :: FormExtension f => [(Constraint, TERM f -> FORMULA f)] -> FORMULA f
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maederinduction constrSubsts =
6e2c88c65d50b2e44f7afa165e6a5fac0724f08cChristian Maeder let mkVar i = mkSimpleId ("x_" ++ show i)
6e2c88c65d50b2e44f7afa165e6a5fac0724f08cChristian Maeder sortInfo = map (\ ((cs, sub), i) -> (sub, (mkVar i, newSort cs)))
6e2c88c65d50b2e44f7afa165e6a5fac0724f08cChristian Maeder $ number constrSubsts
1eb10c0c30323eed3cc21082fd242cd09a612dc5Christian Maeder mkConclusion (subst, v) =
1eb10c0c30323eed3cc21082fd242cd09a612dc5Christian Maeder mkForall [uncurry mkVarDecl v] $ subst $ uncurry mkVarTerm v
1eb10c0c30323eed3cc21082fd242cd09a612dc5Christian Maeder inductionConclusion = conjunct $ map mkConclusion sortInfo
1eb10c0c30323eed3cc21082fd242cd09a612dc5Christian Maeder inductionPremises = map (mkPrems $ map snd constrSubsts) constrSubsts
c2c1ca07d7f3c2228b66599a7fb37b90fe6fb3bcChristian Maeder inductionPremise = conjunct $ concat inductionPremises
6e2c88c65d50b2e44f7afa165e6a5fac0724f08cChristian Maeder in mkImpl inductionPremise inductionConclusion
6e2c88c65d50b2e44f7afa165e6a5fac0724f08cChristian Maeder{- | construct premise set for the induction scheme
1eb10c0c30323eed3cc21082fd242cd09a612dc5Christian Maederfor one sort in the constraint -}
c2c1ca07d7f3c2228b66599a7fb37b90fe6fb3bcChristian MaedermkPrems :: FormExtension f => [TERM f -> FORMULA f]
c2c1ca07d7f3c2228b66599a7fb37b90fe6fb3bcChristian Maeder -> (Constraint, TERM f -> FORMULA f) -> [FORMULA f]
c2c1ca07d7f3c2228b66599a7fb37b90fe6fb3bcChristian MaedermkPrems substs (constr, sub) = map (mkPrem substs sub) (opSymbs constr)
6e2c88c65d50b2e44f7afa165e6a5fac0724f08cChristian Maeder-- | construct a premise for the induction scheme for one constructor
1eb10c0c30323eed3cc21082fd242cd09a612dc5Christian MaedermkPrem :: FormExtension f => [TERM f -> FORMULA f] -> (TERM f -> FORMULA f)
6e2c88c65d50b2e44f7afa165e6a5fac0724f08cChristian Maeder -> (OP_SYMB, [Int]) -> FORMULA f
6e2c88c65d50b2e44f7afa165e6a5fac0724f08cChristian MaedermkPrem substs subst (opSym@(Qual_op_name _ (Op_type _ argTypes _ _) _), idx) =
d591a82b32594f0992b27477cacb00b97226c9c8Christian Maeder mkForall qVars phi
d591a82b32594f0992b27477cacb00b97226c9c8Christian Maeder qVars = map (\ (a, i) -> mkVarDeclStr ("y_" ++ show i) a) $ number argTypes
6e2c88c65d50b2e44f7afa165e6a5fac0724f08cChristian Maeder phi = if null indHyps then indConcl
6e2c88c65d50b2e44f7afa165e6a5fac0724f08cChristian Maeder else mkImpl (conjunct indHyps) indConcl
d591a82b32594f0992b27477cacb00b97226c9c8Christian Maeder indConcl = subst $ mkAppl opSym $ map toQualVar qVars
d591a82b32594f0992b27477cacb00b97226c9c8Christian Maeder indHyps = mapMaybe indHyp (zip qVars idx)
d591a82b32594f0992b27477cacb00b97226c9c8Christian Maeder indHyp (v1, i) =
6e2c88c65d50b2e44f7afa165e6a5fac0724f08cChristian Maeder if i < 0 then Nothing -- leave out sorts from outside the constraint
d591a82b32594f0992b27477cacb00b97226c9c8Christian Maeder else Just $ (substs !! i) $ toQualVar v1
da2b959c50c95309d8eb8b24174249c2847e74b5Christian MaedermkPrem _ _ (opSym, _) =
dcb9ff0e2c2379735acce7073196508d455e0b01Christian Maeder error ("CASL.Induction. mkPrems: "
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder ++ "unqualified operation symbol occuring in constraint: "
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder ++ show opSym)
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder-- | for goals try to generate additional implications based on induction
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian MaedergenerateInductionLemmas :: FormExtension f => Bool
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder -> (Sign f e, [Named (FORMULA f)]) -> (Sign f e, [Named (FORMULA f)])
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian MaedergenerateInductionLemmas b (sig, sens) = let
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder sortGens = foldr (\ s cs -> case sentence s of
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder Sort_gen_ax c _ -> c : cs
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder _ -> cs) [] axs
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder (axs, goals) = partition isAxiom sens
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder in (sig, (if b then sens else axs)
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder ++ generateInductionLemmasAux b sortGens goals)
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian MaedergenerateInductionLemmasAux
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder :: FormExtension f => Bool
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder -- ^ if True create additional implication otherwise replace goals
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder -> [[Constraint]] -- ^ the constraints of a theory
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder -> [AS_Anno.Named (FORMULA f)] -- ^ all goals of a theory
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder -> [AS_Anno.Named (FORMULA f)]
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder{- ^ all the generated induction lemmas
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maederand the labels are derived from the goal-names -}
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian MaedergenerateInductionLemmasAux b sort_gen_axs goals = let
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder findVar s [] = error ("CASL.generateInductionLemmas:\n"
639732746d7c3a586790043b452a4cbdd29a3fc3Christian Maeder ++ "No VAR found of SORT " ++ show s ++ "!")
639732746d7c3a586790043b452a4cbdd29a3fc3Christian Maeder findVar s ((vl, sl) : lst) = if s == sl then vl else findVar s lst
639732746d7c3a586790043b452a4cbdd29a3fc3Christian Maeder removeVarsort v s f = case f of
639732746d7c3a586790043b452a4cbdd29a3fc3Christian Maeder Quantification Universal varDecls formula rng ->
639732746d7c3a586790043b452a4cbdd29a3fc3Christian Maeder let vd' = newVarDecls varDecls
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder in if null vd' then formula
d591a82b32594f0992b27477cacb00b97226c9c8Christian Maeder else Quantification Universal vd' formula rng
d591a82b32594f0992b27477cacb00b97226c9c8Christian Maeder newVarDecls = filter (\ (Var_decl vs _ _) -> not $ null vs) .
6e2c88c65d50b2e44f7afa165e6a5fac0724f08cChristian Maeder map (\ var_decl@(Var_decl vars varsort r) ->
d591a82b32594f0992b27477cacb00b97226c9c8Christian Maeder if varsort == s
6e2c88c65d50b2e44f7afa165e6a5fac0724f08cChristian Maeder then Var_decl (filter (/= v) vars) s r
d591a82b32594f0992b27477cacb00b97226c9c8Christian Maeder else var_decl)
d591a82b32594f0992b27477cacb00b97226c9c8Christian Maeder (uniQuantGoals, restGoals) =
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder foldr ( \ goal (ul, rl) -> case sentence goal of
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder Quantification Universal varDecl _ _ ->
6e2c88c65d50b2e44f7afa165e6a5fac0724f08cChristian Maeder ((goal, flatVAR_DECLs varDecl) : ul, rl)
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder _ -> (ul, goal : rl)) ([], []) goals
6e2c88c65d50b2e44f7afa165e6a5fac0724f08cChristian Maeder {- For each constraint we get a list of goals out of uniQuantGoals
6e2c88c65d50b2e44f7afa165e6a5fac0724f08cChristian Maeder which contain the constraint's newSort. Afterwards all combinations
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder are created. -}
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder constraintGoals = combine
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder . map (\ c -> filter (any ((newSort c ==) . snd) . snd)
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder uniQuantGoals)
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder {- returns big list containing tuples of constraints and a matching
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder combination (list) of goals. -}
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder concatMap (\ c -> map (\ combi -> (c, combi)) $ constraintGoals c)
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder singleDts = map head $ filter isSingle sort_gen_axs
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder indSorts = Set.fromList $ map newSort singleDts
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder (simpleIndGoals, rest2) = foldr (\ (gs, vs) (ul, rl) ->
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder case dropWhile (not . (`Set.member` indSorts) . snd) vs of
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder [] -> (ul, gs : rl)
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder (v, s) : _ -> case find ((== s) . newSort) singleDts of
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder Nothing -> (ul, gs : rl)
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder Just c -> ((gs, (v, s), c) : ul, rl)) ([], []) uniQuantGoals
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder toIndPrem (gs, (v, s), c) =
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder let f = removeVarsort v s $ sentence gs
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder sb t = substitute v s t f
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder ps = mkPrems [sb] (c, sb)
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder in gs { sentence = conjunct ps }
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder map (\ (cons, formulas) ->
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder let formula = instantiateSortGen
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder $ map (\ (c, (f, varsorts)) ->
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder let s = newSort c
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder vs = findVar s varsorts
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder in (c, (removeVarsort vs s $ sentence f, (vs, s))))
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder $ zip cons formulas
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder sName = tail $ concatMap (('_' :) . senAttr . fst) formulas
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder ++ "_induction"
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder in makeNamed sName formula
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder else map toIndPrem simpleIndGoals ++ rest2 ++ restGoals