Commit edc13e4a authored by MARCHE Claude's avatar MARCHE Claude

menage dans blocking_semantics5

parent b86cceea
......@@ -440,28 +440,45 @@ theory FreshVariables
use import SemOp
use import list.Append
predicate var_occurs_in_term (x:ident) (t:term) =
(** [fresh_in_term id t] is true when [id] does not occur in [t] *)
predicate fresh_in_term (x:ident) (t:term) =
match t with
| Tvalue _ -> false
| Tvar i -> x=i
| Tderef _ -> false
| Tbin t1 _ t2 -> var_occurs_in_term x t1 \/ var_occurs_in_term x t2
| Tvalue _ -> true
| Tvar i -> x <> i
| Tderef _ -> true
| Tbin t1 _ t2 -> fresh_in_term x t1 /\ fresh_in_term x t2
end
(*
lemma fresh_in_binop:
forall t t':term, op:operator, v:ident.
fresh_in_term v (Tbin t op t') ->
fresh_in_term v t /\ fresh_in_term v t'
*)
predicate fresh_in_fmla (id:ident) (f:fmla) =
match f with
| Fterm e -> fresh_in_term id e
| Fand f1 f2 | Fimplies f1 f2 ->
fresh_in_fmla id f1 /\ fresh_in_fmla id f2
| Fnot f -> fresh_in_fmla id f
| Flet y t f -> id <> y /\ fresh_in_term id t /\ fresh_in_fmla id f
| Fforall y ty f -> id <> y /\ fresh_in_fmla id f
end
(** substitution of a reference [r] by a logic variable [v]
warning: proper behavior only guaranted if [v] is "fresh",
i.e index(v) > term_maxvar(t) *)
warning: proper behavior only guaranted if [v] is fresh *)
function msubst_term (t:term) (r:mident) (v:ident) : term =
match t with
| Tvalue _ | Tvar _ -> t
| Tderef x -> if r = x then Tvar v else t
| Tbin t1 op t2 ->
Tbin (msubst_term t1 r v) op (msubst_term t2 r v)
Tbin (msubst_term t1 r v) op (msubst_term t2 r v)
end
(*
function subst_term (t:term) (r:ident) (v:ident) : term =
match t with
| Tvalue _ | Tderef _ -> t
......@@ -471,25 +488,6 @@ function subst_term (t:term) (r:ident) (v:ident) : term =
Tbin (subst_term t1 r v) op (subst_term t2 r v)
end
(** [fresh_in_term id t] is true when [id] does not occur in [t] *)
predicate fresh_in_term (id:ident) (t:term) =
not (var_occurs_in_term id t)
lemma fresh_in_binop:
forall t t':term, op:operator, v:ident.
fresh_in_term v (Tbin t op t') ->
fresh_in_term v t /\ fresh_in_term v t'
predicate fresh_in_fmla (id:ident) (f:fmla) =
match f with
| Fterm e -> fresh_in_term id e
| Fand f1 f2 | Fimplies f1 f2 ->
fresh_in_fmla id f1 /\ fresh_in_fmla id f2
| Fnot f -> fresh_in_fmla id f
| Flet y t f -> id <> y /\ fresh_in_term id t /\ fresh_in_fmla id f
| Fforall y ty f -> id <> y /\ fresh_in_fmla id f
end
function subst (f:fmla) (x:ident) (v:ident) : fmla =
match f with
| Fterm e -> Fterm (subst_term e x v)
......@@ -499,6 +497,7 @@ function subst (f:fmla) (x:ident) (v:ident) : fmla =
| Flet y t f -> Flet y (subst_term t x v) (subst f x v)
| Fforall y ty f -> Fforall y ty (subst f x v)
end
*)
function msubst (f:fmla) (x:mident) (v:ident) : fmla =
match f with
......@@ -510,21 +509,25 @@ function msubst (f:fmla) (x:mident) (v:ident) : fmla =
| Fforall y ty f -> Fforall y ty (msubst f x v)
end
(*
lemma subst_fresh_term :
forall t:term, x:ident, v:ident.
fresh_in_term x t -> subst_term t x v = t
*)
(*
lemma subst_fresh :
forall f:fmla, x:ident, v:ident.
fresh_in_fmla x f -> subst f x v = f
*)
(* Needed for monotonicity and wp_reduction *)
lemma eval_msubst_term:
forall e:term, sigma:env, pi:stack, x:mident, v:ident.
fresh_in_term v e ->
eval_term sigma pi (msubst_term e x v) =
eval_term (IdMap.set sigma x (get_stack v pi)) pi e
(* Need it for monotonicity and wp_reduction *)
lemma eval_msubst:
forall f:fmla, sigma:env, pi:stack, x:mident, v:ident.
fresh_in_fmla v f ->
......@@ -537,11 +540,13 @@ id1 <> id2 ->
(eval_term sigma (l++(Cons (id1,v1) (Cons (id2,v2) pi))) t =
eval_term sigma (l++(Cons (id2,v2) (Cons (id1,v1) pi))) t)
(*
lemma eval_swap_term_2:
forall t:term, sigma:env, pi:stack, id1 id2:ident, v1 v2:value.
id1 <> id2 ->
(eval_term sigma (Cons (id1,v1) (Cons (id2,v2) pi)) t =
eval_term sigma (Cons (id2,v2) (Cons (id1,v1) pi)) t)
*)
lemma eval_swap:
forall f:fmla, sigma:env, pi l:stack, id1 id2:ident, v1 v2:value.
......@@ -549,12 +554,14 @@ lemma eval_swap:
(eval_fmla sigma (l++(Cons (id1,v1) (Cons (id2,v2) pi))) f <->
eval_fmla sigma (l++(Cons (id2,v2) (Cons (id1,v1) pi))) f)
(*
lemma eval_swap_2:
forall f:fmla, id1 id2:ident, v1 v2:value.
id1 <> id2 ->
forall sigma:env, pi:stack.
(eval_fmla sigma (Cons (id1,v1) (Cons (id2,v2) pi)) f <->
eval_fmla sigma (Cons (id2,v2) (Cons (id1,v1) pi)) f)
*)
lemma eval_term_change_free :
forall t:term, sigma:env, pi:stack, id:ident, v:value.
......@@ -569,17 +576,6 @@ lemma eval_change_free :
(eval_fmla sigma (Cons (id,v) pi) f <-> eval_fmla sigma pi f)
predicate fresh_in_stmt (id:ident) (s:stmt) =
match s with
| Sskip -> true
| Sseq s1 s2 -> fresh_in_stmt id s1 /\ fresh_in_stmt id s2
| Sassign _ t -> fresh_in_term id t
| Sif t s1 s2 -> fresh_in_term id t /\ fresh_in_stmt id s1 /\ fresh_in_stmt id s2
| Sassert f -> fresh_in_fmla id f
| Swhile cond inv body -> fresh_in_term id cond /\ fresh_in_fmla id inv /\ fresh_in_stmt id body
end
end
......
Markdown is supported
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