Commit 1b86a3f4 authored by Asma Tafat-Bouzid's avatar Asma Tafat-Bouzid
Browse files

blocking semantics

parent e1c01e09
......@@ -303,6 +303,11 @@ function subst_term (t:term) (r:ident) (v:ident) : term =
predicate fresh_in_term (id:ident) (t:term) =
id.ident_index > t.term_maxvar
lemma fresh_in_binop:
forall t t':term, op:operator, v:ident.
fresh_in_term v (mk_tbin t op t') ->
fresh_in_term v t /\ fresh_in_term v t'
lemma eval_msubst_term:
forall e:term, sigma:env, pi:stack, x:mident, v:ident.
fresh_in_term v e ->
......@@ -96,6 +96,11 @@ Existing Instance term_WhyType.
Axiom term_node_WhyType : WhyType term_node.
Existing Instance term_node_WhyType.
Scheme term_induc := Induction for term Sort Prop
with term_node_induc := Induction for term_node Sort Prop.
Print term_induc.
(* Why3 assumption *)
Definition term_maxvar(v:term): Z := match v with
| (mk_term x x1) => x1
......@@ -154,6 +159,8 @@ Inductive fmla :=
Axiom fmla_WhyType : WhyType fmla.
Existing Instance fmla_WhyType.
Print fmla_ind.
(* Why3 assumption *)
Inductive stmt :=
| Sskip : stmt
......@@ -365,6 +372,10 @@ Axiom subst_term_def : forall (t:term) (r:ident) (v:ident),
Definition fresh_in_term(id:ident) (t:term): Prop :=
((term_maxvar t) < (ident_index id))%Z.
Axiom fresh_in_binop : forall (t:term) (t':term) (op:operator) (v:ident),
(fresh_in_term v (mk_tbin t op t')) -> ((fresh_in_term v t) /\
(fresh_in_term v t')).
Require Import Why3.
Ltac ae := why3 "alt-ergo" timelimit 3.
......@@ -374,17 +385,31 @@ Theorem eval_msubst_term : forall (e:term) (sigma:(map mident value))
(pi:(list (ident* value)%type)) (x:mident) (v:ident), (fresh_in_term v
e) -> ((eval_term sigma pi (msubst_term e x v)) = (eval_term (set sigma x
(get_stack v pi)) pi e)).
induction e.
destruct t.
Check term_induc.
intros e.
apply term_induc with (P := fun e =>
forall (sigma : map mident value) (pi : list (ident * value))
(x : mident) (v : ident),
fresh_in_term v e ->
eval_term sigma pi (msubst_term e x v) =
eval_term (set sigma x (get_stack v pi)) pi e)
(P0 := fun t =>
forall (i : int) (sigma : map mident value) (pi : list (ident * value))
(x : mident) (v : ident),
fresh_in_term v (mk_term t i) ->
eval_term sigma pi (msubst_term (mk_term t i) x v) =
eval_term (set sigma x (get_stack v pi)) pi (mk_term t i)).
(* mk_term*)
(* Value *)
(* Var *)
intros sigma pi x v H.
intros i i0 sigma pi x v H.
rewrite (msubst_term_def (mk_term (Tvar i) z)).
rewrite (msubst_term_def (mk_term (Tvar i) i0)).
(* Ref *)
intros sigma pi x v H.
intros m i sigma pi x v H.
destruct (mident_decide m x).
(* m = x*)
......@@ -392,7 +417,18 @@ ae.
(* m <> x*)
(* Bin *)
(*Il manque le bon schema d'induction*)
intros t H1.
intros op t' H2.
intros i sigma pi x v H3.
rewrite (msubst_term_def (mk_term (Tbin t op t') i)).
rewrite H1.
rewrite H2; auto.
apply fresh_in_binop with (t:=t) (t':=t') (op := op).
apply fresh_in_binop with (t:=t) (t':=t') (op := op);
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment