Commit 8df73441 authored by Heiko Becker's avatar Heiko Becker
Browse files

Make all proofs "prove" proofs

parent 5c21c1f2
......@@ -20,20 +20,20 @@ let exp_INDUCT, exp_REC= define_type
show that real valued expressions can be evaluated
by constructing the corresponding function
*)
let exp_eval_EXISTS = prove_general_recursive_function_exists
`?exp_eval.
(!x (E:num->real). exp_eval (Var x) E = E x) /\
(!(v:real) E. exp_eval (Const v) E = v) /\
(!e1 e2 E. exp_eval (Plus e1 e2) E = (exp_eval e1) E + (exp_eval e2) E) /\
(!e1 e2 E. exp_eval (Sub e1 e2) E = (exp_eval e1) E - (exp_eval e2) E) /\
(!e1 e2 E. exp_eval (Mult e1 e2) E = (exp_eval e1) E * (exp_eval e2) E) /\
(!e1 e2 E. exp_eval (Div e1 e2) E = (exp_eval e1) E / (exp_eval e2) E)`;;
let eval_real_EXISTS = prove_general_recursive_function_exists
`?eval_real.
(!x (E:num->real). eval_real (Var x) E = E x) /\
(!(v:real) E. eval_real (Const v) E = v) /\
(!e1 e2 E. eval_real (Plus e1 e2) E = (eval_real e1) E + (eval_real e2) E) /\
(!e1 e2 E. eval_real (Sub e1 e2) E = (eval_real e1) E - (eval_real e2) E) /\
(!e1 e2 E. eval_real (Mult e1 e2) E = (eval_real e1) E * (eval_real e2) E) /\
(!e1 e2 E. eval_real (Div e1 e2) E = (eval_real e1) E / (eval_real e2) E)`;;
(*
Since HOL Light could prove the existence of the evaluation function,
we can define it using the defining equations from the theorem.
*)
let exp_eval_DEF = new_specification ["exp_eval"] exp_eval_EXISTS;;
let eval_real_DEF = new_specification ["eval_real"] eval_real_EXISTS;;
(*
Toy examples showing how to evaluate terms and functions in HOL Light
......@@ -46,7 +46,7 @@ let exp_eval_DEF = new_specification ["exp_eval"] exp_eval_EXISTS;;
Prove totality of expression evaluation for reals assuming totality of the environment
TODO: Make totality totality on occuring variables
*)
let exp_eval_total =
let eval_real_total =
prove (
`!(e:(real)exp) (s:num->real).
(!x:num. ?v:real. s x = v) ==>
......@@ -83,10 +83,11 @@ let exp_eval_total = top_thm();; *)
Next define a "float" type that we can use to plug in to the framework
We need to make a basic type definition because we want to approximate the reals by these floats and enforce a correlation between the parameters
*)
g `is_valid_flformat (2,2)`;;
e (ASM_REWRITE_TAC[is_valid_flformat]);;
e (REPEAT STRIP_TAC THEN ARITH_TAC);;
let p2_valid = top_thm();;
promote_all_values();;
let p2_valid = prove
(`is_valid_flformat (2,2)`,
ASM_REWRITE_TAC [is_valid_flformat] THEN REPEAT STRIP_TAC THEN ARITH_TAC);;
g `?(fmt:flformat) (x:real). is_float fmt x`;;
e (ASM_REWRITE_TAC[is_float;is_frac_and_exp;flr;flp]);;
......@@ -96,22 +97,67 @@ e (EXISTS_TAC `1`);;
e (EXISTS_TAC `&1:int`);;
e (STRIP_TAC THEN TRY (ARITH_TAC));;
e (DESTRUCT_TAC "rw_sound valid_rw" flformat_typbij);;
e (SUBGOAL_TAC "mk_dest_22" `dest_flformat(mk_flformat (2,2)) = (2,2)` [(ASM_MESON_TAC[p2_valid])]);;
e (SUBGOAL_TAC "mk_dest_22"
`dest_flformat(mk_flformat (2,2)) = (2,2)`
[(ASM_MESON_TAC[p2_valid])]);;
e (ASM_REWRITE_TAC[ASSUME `dest_flformat (mk_flformat (2,2)) = 2,2`]);;
e (STRIP_TAC THEN TRY (ARITH_TAC));;
e (ASM_REWRITE_TAC[REAL_ABS_1]);;
e (ASM_REWRITE_TAC [ipow]);;
e (SUBGOAL_TAC "num_0" `(&1):int - &2 + &1 = &0` [INT_ARITH_TAC]);;
e (ASM_REWRITE_TAC[]);;
e (ASM_REWRITE_TAC[REAL_ABS_1;ipow; (INT_REDUCE_CONV `(&1):int - &2 + &1`)]);;
e (REWRITE_TAC [(INT_REDUCE_CONV `(if &0:int <= &0:int
then &2:real pow num_of_int (&0)
else inv (&2:real pow num_of_int (-- &0)))`)]);;
e (SUBGOAL_TAC "pow_0_eq_1" `&2:real pow num_of_int (&0) = &1:real` [ALL_TAC]);;
e (ASM_REWRITE_TAC[NUM_OF_INT_OF_NUM;real_pow]);;
e (ASM_REWRITE_TAC[]);;
e (REAL_ARITH_TAC);;
let exists_float_type_pred = top_thm();;
e (SUBGOAL_TAC "pow_0_eq_1" `&2:real pow num_of_int (&0) = &1:real` [ASM_REWRITE_TAC[NUM_OF_INT_OF_NUM;real_pow]]);;
e (ASM_REWRITE_TAC[] THEN REAL_ARITH_TAC);;
let exists_float_type_pred =
prove
(`?(fmt:flformat) (x:real). is_float fmt x`,
let lemma1 = prove
(`is_valid_flformat (2,2)`,
ASM_REWRITE_TAC [is_valid_flformat] THEN REPEAT STRIP_TAC THEN
ARITH_TAC)
in
ASM_REWRITE_TAC [is_float; is_frac_and_exp; flr; flp] THEN
EXISTS_TAC `mk_flformat(2,2)` THEN
EXISTS_TAC `&1` THEN
EXISTS_TAC `1` THEN
EXISTS_TAC `&1:int` THEN
STRIP_TAC THENL [ARITH_TAC; ALL_TAC] THEN
DESTRUCT_TAC "rw_sound valid_rw" flformat_typbij THEN
SUBGOAL_TAC "mk_dest_22" `dest_flformat (mk_flformat (2,2)) = 2,2`
[ASM_MESON_TAC [lemma1]] THEN
ASM_REWRITE_TAC [ASSUME `dest_flformat (mk_flformat (2,2)) = 2,2`] THEN
STRIP_TAC THENL [ARITH_TAC; ALL_TAC] THEN
ASM_REWRITE_TAC [REAL_ABS_1; ipow; INT_REDUCE_CONV `(&1):int - &2 + &1`] THEN
REWRITE_TAC
[INT_REDUCE_CONV
`(if &0:int <= &0:int
then &2:real pow num_of_int (&0)
else inv (&2:real pow num_of_int (-- &0)))`] THEN
SUBGOAL_TAC "pow_0_eq_1" `&2:real pow num_of_int (&0) = &1:real`
[ASM_REWRITE_TAC [NUM_OF_INT_OF_NUM; real_pow]] THEN
ASM_REWRITE_TAC [] THEN REAL_ARITH_TAC);;
(*
For the moment, floats are simply axiomatized reals!
FIXME!!
*)
new_type_abbrev ("float",`:real`);;
let m_eps = define `m_eps:real = (&1)`;; (* TODO *)
let get_float = define
`get_float (x:real) = ?xf:real d:real. abs (d) <= m_eps /\ xf = x * (&1 + d)`;;
let eval_float_SIMPS =define
`(!x E:num->real. eval_float (Var x) E <=> get_float (E x)) /\
(!v:real E:num->real. eval_float (Const v) E <=> get_float v) /\
(!e1 e2 E. eval_float (Plus e1 e2) E <=>
((eval_float e1 E <=> v1) /\ (eval_float e2 E <=> v2) ==>
get_float (v1 + v2)))`;;
/\
(!e1 e2 E. eval_float (Sub e1 e2) E <=> get_float (eval_float E e1 - eval_float E e2)) /\
(!e1 e2 E. eval_float (Mult e1 e2) E <=> get_float (eval_float E e1 * eval_float E e2)) /\
(!e1 e2 E. eval_float (Div e1 e2) E <=> get_float (eval_float E e1 / eval_float E e2))`;;
(*
Using the parametric expressions, define boolean expressions for conditionals
......
......@@ -26,8 +26,6 @@ let latt_upd_SIMPS = define
(*
First the individual operator updates
*)
let m_eps = define `m_eps:real = (&1)`;; (* TODO *)
(* Exactly framework formula *)
let phi_for_intv = define
`phi_for_intv (iv:intv) (e:err) =
......
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