[Hol-info] Rewriting and Types in HOL-Light

[Heiko B. <s9h...@st...>]

Hello everyone,

I have another question on HOL-Light. This time I am stuck with some 
rewriting in a proof.

I have defined an inductive type and want to prove an "inversion" lemma 
for it:

g `!eps env v val.
   eval_exp eps env (Var v) val ==> val = env v`;;

I have been able to do the proof until I arrive at a subgoal which I 
think is easy to proof but I cannot find the appropriate tactic to do it:

val it : xgoalstack = 1 subgoal (4 total)

   0 [`val = env v2`] (val_eq)
   1 [`v = v2`]

`v = v2`

The script I used is:

e (ONCE_REWRITE_TAC[eval_exp_CASES]);;
e (INTRO_TAC "!eps env v val; cases");;
e (REMOVE_THEN "cases" (DESTRUCT_TAC "var | const | bin"));;
(* Var case *)
e (REMOVE_THEN "var" (DESTRUCT_TAC "@v2. var_eq val_eq"));;
e (SUBGOAL_TAC "v_eq_v2" `v = v2` [REMOVE_THEN "var_eq" (MP_TAC) THEN 
ONCE_REWRITE_TAC[injectivity "exp"]]);;
e (DISCH_TAC);;
e (EXPAND_TAC "v2");;
e (ONCE_REWRITE_TAC[ASSUME `v = v2`]);

Since the last two tactics do not change the goal in any way my 
questions in this case are:

1) How can I use the assumption 1 and rewrite it inside my goal?

2) Is there an easier way of closing the proof, since I already derived 
the goal I have?

3) (A little unrelated) Can I make HOL-Light annotate all terms in my 
goal with their derived type?

I have added my formalization below.


Thank you (once again) in advance.

Best regards,

Heiko


------------------------------------------------------------

let binop_IND, binop_REC = define_type
   "binop = Plus | Sub | Mult | Div ";;
(*
   Define an evaluation function for binary operators.
*)
let eval_binop = new_recursive_definition binop_REC
   `(eval_binop Plus v1 v2 = v1 + v2) /\
   (eval_binop Sub v1 v2 = v1 - v2) /\
   (eval_binop Mult v1 v2 = v1 * v2) /\
   (eval_binop Div v1 v2 = v1 / v2)`;;

let exp_IND, exp_REC= define_type
   "exp = Var num
   | Const V
   | Binop binop exp exp";;

let perturb = define `(perturb:real->real->real) = \r e. r * ((&1) + e)`;;
new_type_abbrev ("env_ty",`:num->real`);;

let eval_exp_RULES, eval_exp_IND, eval_exp_CASES = new_inductive_definition
   `(!eps env v.
       eval_exp eps env (Var v) (env v)) /\
   (!eps env n delta.
      abs delta <= eps ==>
      eval_exp eps env (Const n) (perturb n delta)) /\
   (!eps env b e1 e2 v1 v2 delta.
      eval_exp eps env e1 v1 /\
      eval_exp eps env e2 v2 /\
      abs delta <= eps ==>
      eval_exp eps env (Binop b e1 e2) (perturb (eval_binop b v1 v2) 
delta))`;;