Re: [isabelle] dest_Trueprop question



Dimitrios Vytiniotis wrote:
Hello all, I am puzzled over the first issue and need
some advice on the second.


Second issue (advice)
=======================================================
I have a datatype which has only one constructor that takes a pair.
Values of this datatype are paired with naturals and
contained in a list. I have very often
found out that when I do induction on the list to prove a theorem,
in the inductive case I often have to do
a "by(cases "x", cases "snd x", blast)"
which I hate but want to do it in a one-line step because it is
a very ``obvious'' fact for the reader of the proof. How do I do
this elegantly (e.g with a single tactic like
(cases_deep_break "x", auto) or similar)

thanks!
-d




Dimitrios,

I don't know if the following would help, but of the following,
case_tac_frees does case_tac for all free variables
and case_tac_params does it for all parameters, ie, variables
in a subgoal quantified by !!


fun case_tacs (str :: strs) sg state =
    ((case_tac str THEN_ALL_NEW case_tacs strs) sg state
    handle _ => case_tacs strs sg state)
  | case_tacs [] sg state = all_tac state ;

fun case_tac_frees sg state =
  let val tm = nth (prems_of state, sg-1) ;
    fun freename (Free (name, ty)) = name ;
  in case_tacs (map freename (term_frees tm)) sg state end ;

fun case_tac_params sg state =
  let val tm = nth (prems_of state, sg-1) ;
    val params = (strip_qnt_vars "all" tm) ;
  in case_tacs (map fst params) sg state end ;


Alternatively you can just construct your own "exhaust" theorem
(for example, case_tac "x" where x is a list seems to be equivalent to
(res_inst_tac [("y", "x")] list.exhaust))

Regards,

Jeremy





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.