Commit e5d57657 by Heiko Becker

### Add attic containing old work, currently for reference if I forget how I did...

`Add attic containing old work, currently for reference if I forget how I did stuff. Will be removed later`
parent 8df73441
 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. *) let exp_INDUCT, exp_REC= define_type "exp = Var num | Const V | Plus exp exp | Sub exp exp | Mult exp exp | Div exp exp";; (* Since we want to stay with real values for the moment, show that real valued expressions can be evaluated by constructing the corresponding function *) 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 eval_real_DEF = new_specification ["eval_real"] eval_real_EXISTS;; (* Toy examples showing how to evaluate terms and functions in HOL Light let test = `exp_eval (Const (&1)) (\x. &1)`;; let test = REWRITE_CONV[exp_eval_DEF] test;; rhs (concl test);; *) (* Prove totality of expression evaluation for reals assuming totality of the environment TODO: Make totality totality on occuring variables *) let eval_real_total = prove ( `!(e:(real)exp) (s:num->real). (!x:num. ?v:real. s x = v) ==> ?v. exp_eval e s = v`, MATCH_MP_TAC exp_INDUCT THEN REPEAT STRIP_TAC THEN MESON_TAC[]);; (* More formal proof, to get feeling about tactics. TODO: Time consumption compared? g `!e (s:num->real). (!x:num. ?v:real. s x = v) ==> ?v. exp_eval e s = v`;; e (MATCH_MP_TAC exp_INDUCT THEN REPEAT STRIP_TAC);; e (SPECIALIZE `a:num` `!(x:num). ?(v:real). (s:num->real) x = v`);; e (SPECIALIZE `a:num` `!(x:num). ?(v:real). (s:num->real) x = v`);; e (DESTRUCT_TAC "@v. v_def" (ASSUME `?(v:real). (s:num->real) a = v`));; e (EXISTS_TAC `v:real`);; e (ASM_REWRITE_TAC[exp_eval_SIMPS]);; e (EXISTS_TAC `a:real`);; e (REWRITE_TAC [exp_eval_SIMPS]);; e (SPECIALIZE `s:num->real` `!s. (!x. ?v. s x = v) ==> (?v. exp_eval a0 s = v)`);; e (SUBGOAL_TAC "val_def_a0" `?v. exp_eval a0 s = v` [ALL_TAC]);; e (MATCH_MP_TAC (ASSUME `(!x. ?v. s x = v) ==> (?v. exp_eval a0 s = v)`) THEN ASM_REWRITE_TAC[]);; e (SPECIALIZE `s:num->real` `!s. (!x. ?v. s x = v) ==> (?v. exp_eval a1 s = v)`);; e (SUBGOAL_TAC "val_def_a1" `?v. exp_eval a1 s = v` [ALL_TAC]);; e (MATCH_MP_TAC (ASSUME `(!x. ?v. s x = v) ==> (?v. exp_eval a1 s = v)`) THEN ASM_REWRITE_TAC[]);; e (DESTRUCT_TAC "@v1. v1_def" (ASSUME `?v. exp_eval a0 s = v`));; e (DESTRUCT_TAC "@v2. v2_def" (ASSUME `?v. exp_eval a1 s = v`));; e (EXISTS_TAC `(v1:real) + (v2:real)` THEN ASM_REWRITE_TAC[exp_eval_SIMPS]);; e (MESON_TAC[]);; 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 *) 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]);; 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;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` [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))`;;
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