Commit 2ea7e35e authored by MARCHE Claude's avatar MARCHE Claude

prevent unstability of induction transformation, update sessions

parent 68cb044a
......@@ -363,14 +363,14 @@ lemma subst_fresh :
(* msubst (Flet x t f) id id' = Flet x (msubst_term t id id') (msubst f id id') *)
lemma eval_msubst_term:
forall e:term, sigma:env, pi:stack, x:mident, v:ident.
forall e "induction":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.
forall f "induction":fmla, sigma:env, pi:stack, x:mident, v:ident.
fresh_in_fmla v f ->
(eval_fmla sigma pi (msubst f x v) <->
eval_fmla (IdMap.set sigma x (get_stack v pi)) pi f)
......@@ -382,7 +382,7 @@ lemma eval_msubst:
(* eval_fmla sigma (Cons(x, (get_stack v pi)) pi) f) *)
lemma eval_swap_term:
forall t:term, sigma:env, pi l:stack, id1 id2:ident, v1 v2:value.
forall t "induction":term, sigma:env, pi l:stack, id1 id2:ident, v1 v2:value.
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)
......@@ -394,7 +394,7 @@ lemma eval_swap_term_2:
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.
forall f "induction":fmla, sigma:env, pi l:stack, id1 id2:ident, v1 v2:value.
id1 <> id2 ->
(eval_fmla sigma (l++(Cons (id1,v1) (Cons (id2,v2) pi))) f <->
eval_fmla sigma (l++(Cons (id2,v2) (Cons (id1,v1) pi))) f)
......@@ -796,7 +796,7 @@ predicate stmt_writes (s:stmt) (w:Set.set mident) =
(* ce lemme sert pour prouver distrib_conj, dans le cas de la sequence (et c'est tout !) *)
lemma monotonicity:
forall s:stmt, p q:fmla.
forall s "induction":stmt, p q:fmla.
valid_fmla (Fimplies p q)
-> valid_fmla (Fimplies (wp s p) (wp s q) )
......@@ -813,20 +813,20 @@ predicate stmt_writes (s:stmt) (w:Set.set mident) =
(* ce lemme sert pour wp_reduction dans le cas du while (et c'est tout !) *)
lemma distrib_conj:
forall s:stmt, sigma:env, pi:stack, p q:fmla.
forall s "induction":stmt, sigma:env, pi:stack, p q:fmla.
(eval_fmla sigma pi (wp s p)) /\
(eval_fmla sigma pi (wp s q)) ->
eval_fmla sigma pi (wp s (Fand p q))
lemma wp_reduction:
forall sigma sigma':env, pi pi':stack, s s':stmt.
forall sigma sigma':env, pi pi':stack, s "induction":stmt, s':stmt.
one_step sigma pi s sigma' pi' s' ->
forall q:fmla.
eval_fmla sigma pi (wp s q) ->
eval_fmla sigma' pi' (wp s' q)
lemma progress:
forall s:stmt, sigma:env, pi:stack,
forall s "induction":stmt, sigma:env, pi:stack,
sigmat: type_env, pit: type_stack, q:fmla.
compatible_env sigma sigmat pi pit ->
type_stmt sigmat pit s ->
......
......@@ -422,14 +422,14 @@ lemma subst_fresh :
(* msubst (Flet x t f) id id' = Flet x (msubst_term t id id') (msubst f id id') *)
lemma eval_msubst_term:
forall e:term, sigma:env, pi:stack, x:mident, v:ident.
forall e "induction":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.
forall f "induction":fmla, sigma:env, pi:stack, x:mident, v:ident.
fresh_in_fmla v f ->
(eval_fmla sigma pi (msubst f x v) <->
eval_fmla (IdMap.set sigma x (get_stack v pi)) pi f)
......@@ -441,38 +441,38 @@ lemma eval_msubst:
(* eval_fmla sigma (Cons(x, (get_stack v pi)) pi) f) *)
lemma eval_swap_term:
forall t:term, sigma:env, pi l:stack, id1 id2:ident, v1 v2:value.
forall t "induction":term, sigma:env, pi l:stack, id1 id2:ident, v1 v2:value.
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.
forall t "induction":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.
forall f "induction":fmla, sigma:env, pi l:stack, id1 id2:ident, v1 v2:value.
id1 <> id2 ->
(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.
forall f "induction":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.
forall t "induction":term, sigma:env, pi:stack, id:ident, v:value.
fresh_in_term id t ->
eval_term sigma (Cons (id,v) pi) t = eval_term sigma pi t
(* Need it for monotonicity*)
lemma eval_change_free :
forall f:fmla, id:ident, v:value.
forall f "induction":fmla, id:ident, v:value.
fresh_in_fmla id f ->
forall sigma:env, pi:stack.
(eval_fmla sigma (Cons (id,v) pi) f <-> eval_fmla sigma pi f)
......@@ -881,18 +881,18 @@ predicate expr_writes (s:expr) (w:Set.set mident) =
(* subst (wp e q) id id' = wp e (subst q id id') *)
lemma monotonicity:
forall s:expr, p q:fmla.
forall s "induction":expr, p q:fmla.
valid_fmla (Fimplies p q)
-> valid_fmla (Fimplies (wp s p) (wp s q) )
lemma distrib_conj:
forall s:expr, sigma:env, pi:stack, p q:fmla.
forall s "induction":expr, sigma:env, pi:stack, p q:fmla.
(eval_fmla sigma pi (wp s p)) /\
(eval_fmla sigma pi (wp s q)) ->
eval_fmla sigma pi (wp s (Fand p q))
lemma wp_reduction:
forall sigma sigma':env, pi pi':stack, s s':expr.
forall sigma sigma':env, pi pi':stack, s "induction":expr, s':expr.
one_step sigma pi s sigma' pi' s' ->
forall q:fmla.
eval_fmla sigma pi (wp s q) ->
......
......@@ -459,25 +459,25 @@ predicate fresh_in_fmla (id:ident) (f:fmla) =
(* Needed for monotonicity and wp_reduction *)
lemma eval_msubst_term:
forall e:term, sigma:env, pi:stack, x:mident, v:ident.
forall e "induction":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
lemma eval_msubst:
forall f:fmla, sigma:env, pi:stack, x:mident, v:ident.
forall f "induction":fmla, sigma:env, pi:stack, x:mident, v:ident.
fresh_in_fmla v f ->
(eval_fmla sigma pi (msubst f x v) <->
eval_fmla (IdMap.set sigma x (get_stack v pi)) pi f)
lemma eval_swap_term:
forall t:term, sigma:env, pi l:stack, id1 id2:ident, v1 v2:value.
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)
forall t "induction":term, sigma:env, pi l:stack, id1 id2:ident, v1 v2:value.
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_gen:
forall f:fmla, sigma:env, pi l:stack, id1 id2:ident, v1 v2:value.
forall f "induction":fmla, sigma:env, pi l:stack, id1 id2:ident, v1 v2:value.
id1 <> id2 ->
(eval_fmla sigma (l++(Cons (id1,v1) (Cons (id2,v2) pi))) f <->
eval_fmla sigma (l++(Cons (id2,v2) (Cons (id1,v1) pi))) f)
......@@ -489,13 +489,13 @@ lemma eval_swap:
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.
forall t "induction":term, sigma:env, pi:stack, id:ident, v:value.
fresh_in_term id t ->
eval_term sigma (Cons (id,v) pi) t = eval_term sigma pi t
(* Need it for monotonicity*)
lemma eval_change_free :
forall f:fmla, sigma:env, pi:stack, id:ident, v:value.
forall f "induction":fmla, sigma:env, pi:stack, id:ident, v:value.
fresh_in_fmla id f ->
(eval_fmla sigma (Cons (id,v) pi) f <-> eval_fmla sigma pi f)
......@@ -683,7 +683,7 @@ function wp (s:stmt) (q:fmla) : fmla =
eval_fmla sigma pi (wp s (abstract_effects s q))
lemma monotonicity:
forall s:stmt, p q:fmla.
forall s "induction":stmt, p q:fmla.
valid_fmla (Fimplies p q)
-> valid_fmla (Fimplies (wp s p) (wp s q) )
......@@ -699,7 +699,7 @@ function wp (s:stmt) (q:fmla) : fmla =
*)
lemma distrib_conj:
forall s:stmt, sigma:env, pi:stack, p q:fmla.
forall s "induction":stmt, sigma:env, pi:stack, p q:fmla.
(eval_fmla sigma pi (wp s p)) /\
(eval_fmla sigma pi (wp s q)) ->
eval_fmla sigma pi (wp s (Fand p q))
......@@ -712,7 +712,7 @@ function wp (s:stmt) (q:fmla) : fmla =
eval_fmla sigma' pi' (wp s' q)
lemma progress:
forall s:stmt, sigma:env, pi:stack,
forall s "induction":stmt, sigma:env, pi:stack,
sigmat: type_env, pit: type_stack, q:fmla.
compatible_env sigma sigmat pi pit ->
type_stmt sigmat pit s ->
......
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "/home/marche/why3/share/why3session.dtd">
<!DOCTYPE why3session SYSTEM "/usr/local/share/why3/why3session.dtd">
<why3session shape_version="2">
<prover
id="0"
......@@ -20,7 +20,7 @@
<file
name="../wp_total.mlw"
verified="false"
expanded="false">
expanded="true">
<theory
name="Imp"
locfile="../wp_total.mlw"
......@@ -415,7 +415,7 @@
locfile="../wp_total.mlw"
loclnum="343" loccnumb="10" loccnume="12"
expl="parameter wp"
sum="ca36efc8b3606fb37e394c56407b804c"
sum="917c9fa392280fcd2eec55d072558486"
proved="false"
expanded="true"
shape="CV0aSskipavalid_tripleV1V0V1aSseqVVavalid_tripleV5V0V1Iavalid_tripleV5V2V4FIavalid_tripleV4V3V1FaSassignVVavalid_tripleasubstV1V6V7V0V1aSifVVVavalid_tripleaFandaFimpliesaFtermV8V12aFimpliesaFnotaFtermV8V11V0V1Iavalid_tripleV12V9V1FIavalid_tripleV11V10V1FaSassertVavalid_tripleaFimpliesV13V1V0V1aSwhileVVVavalid_tripleaFandV15aFandaFimpliesaFandaFtermV14V15V17aFimpliesaFandaFnotaFtermV14V15V1V0V1Iavalid_tripleV17V16V15FF">
......@@ -439,7 +439,7 @@
locfile="../wp_total.mlw"
loclnum="343" loccnumb="10" loccnume="12"
expl="postcondition"
sum="d6cc82e1eaea36ec027025bacc29124d"
sum="9790cc1fd417477f9e71930a1c81388e"
proved="true"
expanded="false"
shape="CV0aSskipavalid_tripleV1V0V1aSseqVVtaSassignVVtaSifVVVtaSassertVtaSwhileVVVtF">
......@@ -459,7 +459,7 @@
locfile="../wp_total.mlw"
loclnum="343" loccnumb="10" loccnume="12"
expl="postcondition"
sum="76687642530d6b2b926881d6a1b65459"
sum="04f0b357e67561b63482717b70b66b65"
proved="true"
expanded="false"
shape="CV0aSskiptaSseqVVavalid_tripleV5V0V1Iavalid_tripleV5V2V4FIavalid_tripleV4V3V1FaSassignVVtaSifVVVtaSassertVtaSwhileVVVtF">
......@@ -479,7 +479,7 @@
locfile="../wp_total.mlw"
loclnum="343" loccnumb="10" loccnume="12"
expl="postcondition"
sum="f18c418c598f9362ab0c1259acc1e691"
sum="af5162dc3c2c5e55234e4760311c4a0d"
proved="true"
expanded="false"
shape="CV0aSskiptaSseqVVtaSassignVVavalid_tripleasubstV1V4V5V0V1aSifVVVtaSassertVtaSwhileVVVtF">
......@@ -499,7 +499,7 @@
locfile="../wp_total.mlw"
loclnum="343" loccnumb="10" loccnume="12"
expl="postcondition"
sum="f530afffd2fb136a2c17c31939ae49c9"
sum="0015418a278db9380a70ae36fb85ba8f"
proved="true"
expanded="false"
shape="CV0aSskiptaSseqVVtaSassignVVtaSifVVVavalid_tripleaFandaFimpliesaFtermV6V10aFimpliesaFnotaFtermV6V9V0V1Iavalid_tripleV10V7V1FIavalid_tripleV9V8V1FaSassertVtaSwhileVVVtF">
......@@ -535,7 +535,7 @@
locfile="../wp_total.mlw"
loclnum="343" loccnumb="10" loccnume="12"
expl="postcondition"
sum="e21e50f41a61c72f110c52d0ced8b9b4"
sum="13135c21d0766e2ebdd73c1232062160"
proved="true"
expanded="true"
shape="CV0aSskiptaSseqVVtaSassignVVtaSifVVVtaSassertVavalid_tripleaFimpliesV9V1V0V1aSwhileVVVtF">
......@@ -580,7 +580,7 @@
locfile="../wp_total.mlw"
loclnum="343" loccnumb="10" loccnume="12"
expl="postcondition"
sum="abb6c6de1c3af669e9cd8cd046a9d4ae"
sum="683f99e64794b63acf4f60f0bab99bd6"
proved="false"
expanded="true"
shape="CV0aSskiptaSseqVVtaSassignVVtaSifVVVtaSassertVtaSwhileVVVavalid_tripleaFandV11aFandaFimpliesaFandaFtermV10V11V13aFimpliesaFandaFnotaFtermV10V11V1V0V1Iavalid_tripleV13V12V11FF">
......
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