Commit a4e7059f authored by Heiko Becker's avatar Heiko Becker
Browse files

Fix 2 failures

parent 9d635a47
......@@ -18,6 +18,6 @@ let eq_give_goal (eq:term) (impl:term) proj =
let eq_give_left eq impl = eq_give_goal eq impl fst;;
let eq_give_right eq impl = eq_give_goal eq impl snd;;
let contradiction (t:term) (th:xthm) =
SUBGOAL_TAC "" `F` [MP_TAC (ASSUME t) THEN ASM_REWRITE_TAC [prove_constructors_distinct th]]
let contradiction (t:term) (ty:string) =
SUBGOAL_TAC "" `F` [MP_TAC (ASSUME t) THEN ASM_REWRITE_TAC [distinctness ty]]
THEN FIRST_ASSUM CONTR_TAC;;
......@@ -30,7 +30,7 @@ let sstep_RULES,sstep_INDUCT,sstep_CASES = new_inductive_definition
(!(c:(real)bexp) s t eps
(env:num->real).
bval eps env c T ==>
sstep (Ite c s t) env eps s env) /\
sstep (Ite c s t) env eps s env) /\
(!(c:(real)bexp) s t eps
(env:num->real).
bval eps env c F ==>
......@@ -44,10 +44,10 @@ let sstep_RULES,sstep_INDUCT,sstep_CASES = new_inductive_definition
Analogously define Big Step semantics for the Daisy language,
parametric by the evaluation function*)
let bstep_RULES,bstep_INDUCT,bstep_CASES = new_inductive_definition
`(!x (e:(real)exp) s (env:num->real) (v:real) eps
`(!x (e:(real)exp) s s' (env:num->real) (v:real) eps
(env2:num->real).
eval_exp eps env e v /\
bstep s (upd_env x v env) eps s env2 ==>
bstep s (upd_env x v env) eps s' env2 ==>
bstep (Let x e s) env eps s env2) /\
(!(c:(real)bexp) s1 s2 t eps
(env:num->real)
......
......@@ -86,8 +86,8 @@ e (CHEAT_TAC);;
e (CHANGED_TAC(ASM_REWRITE_TAC [(ASSUME `a:num = v:num`)]));;
does not work
*)
e (contradiction `(Var a):(real)exp = Const n` exp_REC);;
e (contradiction `(Var a):(real)exp = Binop b e1 e2` exp_REC);;
e (contradiction `(Var a):(real)exp = Const n` "exp");;
e (contradiction `(Var a):(real)exp = Binop b e1 e2` "exp");;
(* FINISH FIRST INVERSION, START SECOND *)
e (SUBGOAL_TAC "v2_eq_env_a" `env a = v2` [ALL_TAC]);;
e (MP_TAC (ASSUME `eval_exp (&0) env (Var a) v2`));;
......@@ -101,8 +101,8 @@ e (CHEAT_TAC);;
e (CHANGED_TAC(ASM_REWRITE_TAC [(ASSUME `a:num = v:num`)]));;
does not work
*)
e (contradiction `(Var a):(real)exp = Const n` exp_REC);;
e (contradiction `(Var a):(real)exp = Binop b e1 e2` exp_REC);;
e (contradiction `(Var a):(real)exp = Const n` "exp");;
e (contradiction `(Var a):(real)exp = Binop b e1 e2` "exp");;
(* INVERSIONS FINISHED, now rewrite *)
e (CHEAT_TAC);; (* FIXME *)
(* First inversion *)
......@@ -110,7 +110,7 @@ e (SUBGOAL_TAC "delta_0" `?d. d = &0 /\ v1 = perturb a d` [ALL_TAC]);;
e (MP_TAC (ASSUME `eval_exp (&0) env (Const a) v1`));;
e (ONCE_REWRITE_TAC [eval_exp_CASES]);;
e (STRIP_TAC);;
e (contradiction `(Const a):(real)exp = Var v` exp_REC);;
e (contradiction `(Const a):(real)exp = Var v` "exp");;
(* equivalence proof as above *)
e (SUBGOAL_TAC "" `a = n` [CHEAT_TAC]);;
e (EXISTS_TAC `delta:real`);;
......@@ -120,13 +120,13 @@ e (MATCH_MP_TAC (ASSUME `abs delta <= &0 ==> delta = &0`));;
e (ASM_MESON_TAC[]);;
e (ASM_REWRITE_TAC[]);;
e (CHEAT_TAC);; (* FIXME: Rewrites *)
e (contradiction `(Const a):(real)exp = Binop b e1 e2` exp_REC);;
e (contradiction `(Const a):(real)exp = Binop b e1 e2` "exp");;
(* Second inversion *)
e (SUBGOAL_TAC "delta_0" `?d. d = &0 /\ v2 = perturb a d` [ALL_TAC]);;
e (MP_TAC (ASSUME `eval_exp (&0) env (Const a) v2`));;
e (ONCE_REWRITE_TAC [eval_exp_CASES]);;
e (STRIP_TAC);;
e (contradiction `(Const a):(real)exp = Var v` exp_REC);;
e (contradiction `(Const a):(real)exp = Var v` "exp");;
(* equivalence proof as above *)
e (SUBGOAL_TAC "" `a = n` [CHEAT_TAC]);;
e (EXISTS_TAC `delta:real`);;
......@@ -136,15 +136,15 @@ e (MATCH_MP_TAC (ASSUME `abs delta <= &0 ==> delta = &0`));;
e (ASM_MESON_TAC[]);;
e (ASM_REWRITE_TAC[]);;
e (CHEAT_TAC);; (* FIXME: Rewrites *)
e (contradiction `(Const a):(real)exp = Binop b e1 e2` exp_REC);;
e (contradiction `(Const a):(real)exp = Binop b e1 e2` "exp");;
e (CHEAT_TAC);; (*Rewrites *)
(* Induction step *)
e (SUBGOAL_TAC "" `?v11 v12. eval_exp (&0) env a1 v11 /\ eval_exp (&0) env a2 v12` [ALL_TAC]);;
e (MP_TAC (ASSUME `eval_exp (&0) env (Binop a0 a1 a2) v1`));;
e (ONCE_REWRITE_TAC [eval_exp_CASES]);;
e (STRIP_TAC);;
e (contradiction `(Binop a0 a1 a2):(real)exp = Var v` exp_REC);;
e (contradiction `(Binop a0 a1 a2):(real)exp = Const n` exp_REC);;
e (contradiction `(Binop a0 a1 a2):(real)exp = Var v` "exp");;
e (contradiction `(Binop a0 a1 a2):(real)exp = Const n` "exp");;
e (EXISTS_TAC `v1:real`);;
e (EXISTS_TAC `v1:real`);;
e (STRIP_TAC);;
......
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