Commit 5c21c1f2 authored by Heiko Becker's avatar Heiko Becker
Browse files

Add proof that the predicate that should characterize floats actually characterizes a non-empty set

parent 99772064
......@@ -2,7 +2,7 @@
Formalization of the Abstract Syntax Tree of a subset used in the Daisy framework
*)
needs "Infra/tactics.hl";;
needs "/home/heiko/Git_Repos/hol-light/IEEE/make.ml";;
(*
Define expressions parametric over some value type V.
Will ease reasoning about different instantiations later.
......@@ -79,6 +79,40 @@ e (MESON_TAC[]);;
e (MESON_TAC[]);;
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();;
g `?(fmt:flformat) (x:real). is_float fmt x`;;
e (ASM_REWRITE_TAC[is_float;is_frac_and_exp;flr;flp]);;
e (EXISTS_TAC `mk_flformat(2,2)`);;
e (EXISTS_TAC `&1`);;
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 (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 (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();;
(*
Using the parametric expressions, define boolean expressions for conditionals
*)
......
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