Commit 81dc70ea by Heiko Becker

### Forgot boolean exps

parent e2dd604f
 ... ... @@ -2,26 +2,6 @@ Formalization of the Abstract Syntax Tree of a subset used in the Daisy framework *) needs "exps.hl";; (* Using the parametric expressions, define boolean expressions for conditionals *) let bexp_INDUCT, bexp_REC = define_type "bexp = leq (V)exp (V)exp | less (V)exp (V)exp";; (* Define evaluation of booleans for reals *) let bval_SIMPS = define `(bval (leq e1 e2) (E:num->real) = (exp_eval e1 E) <= (exp_eval e2 E)) /\ (bval (less e1 e2) E = (exp_eval e1 E) < (exp_eval e2 E))`;; (* Simplify arithmetic later by making > >= only abbreviations *) let gr_simps = define `gr = \(e1:(V)exp). \(e2:(V)exp). less e2 e1`;; let greq_simps = define `greq = \(e1:(V)exp). \(e2:(V)exp). leq e2 e1`;; (* Next define what a program is. Currently no loops, only conditionals and assignments ... ...
 ... ... @@ -71,119 +71,22 @@ let is_valid_err_float = define (&n = err_fun id \/ --(&n) = err_fun id) /\ abs (&n) <= m_eps`;; (* Prove totality of expression evaluation for reals assuming totality of the environment TODO: Make totality totality on occuring variables Using the parametric expressions, define boolean expressions for conditionals *) 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();; *) let bexp_INDUCT, bexp_REC = define_type "bexp = leq (V)exp (V)exp | less (V)exp (V)exp";; (* 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 Define evaluation of booleans for reals *) 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 is_abs_float = define `is_abs_float (x:real) <=> ?xf:real d:real. abs (d) <= m_eps /\ xf = x * (&1 + d)`;; let bval_SIMPS = define `(bval (leq e1 e2) (E:num->real) (eval:(V)exp->(num->real)->real) = (eval e1 E) <= (eval e2 E)) /\ (bval (less e1 e2) E eval = (eval e1 E) < (eval e2 E))`;; let eval_float_RULES, eval_float_INDUCT, eval_float_CASES = new_inductive_definition `(!x (E:num->real). is_abs_float (E x) ==> eval_float (Var x) E (E x)) /\ (!v:real E:num->real. is_abs_float v ==> eval_float (Const v) E v) /\ (!e1 e2 E. eval_float e1 E v1 /\ eval_float e2 E v2 ==> is_abs_float 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))`;; (* Simplify arithmetic later by making > >= only abbreviations *) let gr_simps = define `gr = \(e1:(V)exp). \(e2:(V)exp). less e2 e1`;; let greq_simps = define `greq = \(e1:(V)exp). \(e2:(V)exp). leq e2 e1`;;
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!