# Changeset 3529 for LTS/imp.ma

Ignore:
Timestamp:
Mar 12, 2015, 3:38:10 PM (5 years ago)
Message:

abitazione tipo instr_params in corso

File:
1 edited

Unmodified
Removed
• ## LTS/imp.ma

 r3528 include "basics/lists/list.ma". include "arithmetics/nat.ma". include "basics/bool.ma". include "Language.ma". (* Syntax *) Eq: expr → expr → condition | Not: condition → condition. inductive seq_i:Type[0]≝sNop: seq_i|sAss: seq_i|sInc: seq_i. definition seq_i_eq:seq_i→ seq_i → bool≝λs1,s2:seq_i.match s1 with [ sNop ⇒ match s2 with [sNop ⇒ true| _⇒ false] |sAss ⇒ match s2 with [sAss ⇒ true| _⇒ false] |sInc ⇒ match s2 with [sInc ⇒ true| _⇒ false] ]. lemma seq_i_eq_equality:∀s1,s2.seq_i_eq s1 s2=true ↔ s1=s2.#s1 #s2 cases s1 cases s2 normalize % #H destruct % qed. inductive io_i:Type[0]≝. definition io_i_eq:io_i→ io_i→ bool≝λi1,i2:io_i.true. lemma io_i_eq_equality:∀i1,i2.io_i_eq i1 i2=true ↔ i1=i2.#i1 #i2 cases i1 qed. let rec neqb n m ≝ match n with [ O ⇒ match m with [ O ⇒ true | S q ⇒ false] | S p ⇒ match m with [ O ⇒ false | S q ⇒ neqb p q] ]. axiom neqb_true_to_eq: ∀n,m:nat. neqb n m = true ↔ n = m. definition cond_i:Type[0]≝condition. let rec expr_eq (e1:expr) (e2:expr):bool≝ match e1 with [Var v1⇒ match e2 with [Var v2⇒ neqb v1 v2|_⇒ false] |Const v1⇒ match e2 with [Const v2⇒ neqb v1 v2|_⇒ false] |Plus le1 re1 ⇒ match e2 with [Plus le2 re2 ⇒ andb (expr_eq le1 le2) (expr_eq re1 re2)|_⇒ false] |Minus le1 re1 ⇒ match e2 with [Minus le2 re2 ⇒ andb (expr_eq le1 le2) (expr_eq re1 re2)|_⇒ false] ]. let rec cond_i_eq (c1:cond_i) (c2:cond_i):bool ≝ match c1 with [Eq e1 e2⇒ match c2 with [Eq f1 f2 ⇒ (andb (expr_eq e1 f1) (expr_eq e2 f2))|_⇒ false] |Not e⇒ match c2 with [Not f⇒ cond_i_eq e f|_⇒ false]]. lemma expr_eq_equality:∀e1,e2:expr.expr_eq e1 e2=true ↔e1=e2. #e1 #e2 elim e1 elim e2 normalize [#v #v' % #H elim v elim v' normalize in H; [%|#v2 #H' destruct lemma condition_eq_equality:∀c1,c2:condition.cond_i_eq c1 c2=true ↔ c1=c2. #c1 #c2 elim c1 elim c2 [#H1 #H2 #H3 #H4 % #H normalize in H; (* inductive cond_i:Type[0]≝cIfThenElse: cond_i. definition cond_i_eq:cond_i → cond_i → bool ≝λc1,c2:cond_i.true. lemma cond_i_eq_equality:∀c1,c2.cond_i_eq c1 c2=true ↔ c1=c2.#c1 #c2 cases c1 cases c2 % #_ % qed. *) (* inductive loop_i:Type[0]≝lWhile: loop_i. definition loop_i_eq:loop_i → loop_i → bool ≝λl1,l2:loop_i.true. lemma loop_i_eq_equality:∀l1,l2.loop_i_eq l1 l2=true ↔ l1=l2.#l1 #l2 cases l1 cases l2 % #_ % qed. *) (* let rec neqb n m ≝ match n with [ O ⇒ match m with [ O ⇒ true | S q ⇒ false] | S p ⇒ match m with [ O ⇒ false | S q ⇒ neqb p q] ]. axiom neqb_true_to_eq: ∀n,m:nat. neqb n m = true ↔ n = m. *) definition imp_instr_params: instr_params ≝ mk_instr_params ? ? ? ? ? ?. [@(mk_DeqSet seq_i seq_i_eq seq_i_eq_equality) |@(mk_DeqSet io_i io_i_eq io_i_eq_equality) |@(mk_DeqSet cond_i cond_i_eq cond_i_eq_equality) |@(mk_DeqSet loop_i loop_i_eq loop_i_eq_equality) |@(mk_DeqSet nat neqb neqb_true_to_eq) |@(mk_DeqSet nat neqb neqb_true_to_eq)].qed. (* | IfThenElse: condition → command → command → command*)
Note: See TracChangeset for help on using the changeset viewer.