Changeset 24 for Csemantics/Csyntax.ma
 Timestamp:
 Aug 27, 2010, 1:21:50 PM (11 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Csemantics/Csyntax.ma
r4 r24 224 224  LSdefault: statement → labeled_statements 225 225  LScase: int → statement → labeled_statements → labeled_statements. 226 227 nlet rec statement_ind2 228 (P:statement → Prop) (Q:labeled_statements → Prop) 229 (Ssk:P Sskip) 230 (Sas:∀e1,e2. P (Sassign e1 e2)) 231 (Sca:∀eo,e,args. P (Scall eo e args)) 232 (Ssq:∀s1,s2. P s1 → P s2 → P (Ssequence s1 s2)) 233 (Sif:∀e,s1,s2. P s1 → P s2 → P (Sifthenelse e s1 s2)) 234 (Swh:∀e,s. P s → P (Swhile e s)) 235 (Sdo:∀e,s. P s → P (Sdowhile e s)) 236 (Sfo:∀s1,e,s2,s3. P s1 → P s2 → P s3 → P (Sfor s1 e s2 s3)) 237 (Sbr:P Sbreak) 238 (Sco:P Scontinue) 239 (Sre:∀eo. P (Sreturn eo)) 240 (Ssw:∀e,ls. Q ls → P (Sswitch e ls)) 241 (Sla:∀l,s. P s → P (Slabel l s)) 242 (Sgo:∀l. P (Sgoto l)) 243 (LSd:∀s. P s → Q (LSdefault s)) 244 (LSc:∀i,s,t. P s → Q t → Q (LScase i s t)) 245 (s:statement) on s : P s ≝ 246 match s with 247 [ Sskip ⇒ Ssk 248  Sassign e1 e2 ⇒ Sas e1 e2 249  Scall eo e args ⇒ Sca eo e args 250  Ssequence s1 s2 ⇒ Ssq s1 s2 251 (statement_ind2 P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo LSd LSc s1) 252 (statement_ind2 P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo LSd LSc s2) 253  Sifthenelse e s1 s2 ⇒ Sif e s1 s2 254 (statement_ind2 P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo LSd LSc s1) 255 (statement_ind2 P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo LSd LSc s2) 256  Swhile e s ⇒ Swh e s 257 (statement_ind2 P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo LSd LSc s) 258  Sdowhile e s ⇒ Sdo e s 259 (statement_ind2 P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo LSd LSc s) 260  Sfor s1 e s2 s3 ⇒ Sfo s1 e s2 s3 261 (statement_ind2 P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo LSd LSc s1) 262 (statement_ind2 P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo LSd LSc s2) 263 (statement_ind2 P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo LSd LSc s3) 264  Sbreak ⇒ Sbr 265  Scontinue ⇒ Sco 266  Sreturn eo ⇒ Sre eo 267  Sswitch e ls ⇒ Ssw e ls 268 (labeled_statements_ind2 P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo LSd LSc ls) 269  Slabel l s ⇒ Sla l s 270 (statement_ind2 P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo LSd LSc s) 271  Sgoto l ⇒ Sgo l 272 ] 273 and labeled_statements_ind2 274 (P:statement → Prop) (Q:labeled_statements → Prop) 275 (Ssk:P Sskip) 276 (Sas:∀e1,e2. P (Sassign e1 e2)) 277 (Sca:∀eo,e,args. P (Scall eo e args)) 278 (Ssq:∀s1,s2. P s1 → P s2 → P (Ssequence s1 s2)) 279 (Sif:∀e,s1,s2. P s1 → P s2 → P (Sifthenelse e s1 s2)) 280 (Swh:∀e,s. P s → P (Swhile e s)) 281 (Sdo:∀e,s. P s → P (Sdowhile e s)) 282 (Sfo:∀s1,e,s2,s3. P s1 → P s2 → P s3 → P (Sfor s1 e s2 s3)) 283 (Sbr:P Sbreak) 284 (Sco:P Scontinue) 285 (Sre:∀eo. P (Sreturn eo)) 286 (Ssw:∀e,ls. Q ls → P (Sswitch e ls)) 287 (Sla:∀l,s. P s → P (Slabel l s)) 288 (Sgo:∀l. P (Sgoto l)) 289 (LSd:∀s. P s → Q (LSdefault s)) 290 (LSc:∀i,s,t. P s → Q t → Q (LScase i s t)) 291 (ls:labeled_statements) on ls : Q ls ≝ 292 match ls with 293 [ LSdefault s ⇒ LSd s 294 (statement_ind2 P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo LSd LSc s) 295  LScase i s t ⇒ LSc i s t 296 (statement_ind2 P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo LSd LSc s) 297 (labeled_statements_ind2 P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo LSd LSc t) 298 ]. 299 300 ndefinition statement_ind ≝ λP,Ssk,Sas,Sca,Ssq,Sif,Swh,Sdo,Sfo,Sbr,Sco,Sre,Ssw,Sla,Sgo. 301 statement_ind2 P (λ_.True) Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo 302 (λ_,_. I) (λ_,_,_,_,_.I). 226 303 227 304 (* * ** Functions *)
Note: See TracChangeset
for help on using the changeset viewer.