[isabelle] case_names and consumes



Hello everyone,

i've got a case rule which has the following form:

lemma case_rule[consumes 2, case_names case1 case2]:
  assumes "precond1"
  assumes "precond2"
  assumes "case1 ==> Q"
  assumes "case2 ==> Q"
  shows "Q"
  sorry

The first two assumptions are preconditions, so I'd like to have these two consumed by cases.

This works fine, if I'm really supplying two facts to the cases method:

lemma
  assumes "precond1" and "precond2"
  shows Q
using assms proof (cases rule: case_rule)
print_cases
(* cases:
 *   case1:
 *     let "?case" = "?Q"
 *     assume "case1"
 *   case2:
 *     let "?case" = "?Q"
 *     assume "case2"
 *)
oops

but if I supply only one fact, cases consumes this fact without complaining, but after that, the case names are wrong (in Isabelle 2009-2), because three goals instead of two remain:

lemma
  assumes "precond1"
  shows Q
using assms proof (cases rule: case_rule)
print_cases
(* cases:
 *  case1:
 *     let "?case" = "precond2"
 *   case2:
 *     let "?case" = "?Q"
 *     assume "case1"
 *)
oops

This seems wrong to me as the isar reference manual specifies that the case names apply to the suffix of the list of premises (which works fine if I don't specify consumes).

Independent from that, I wonder why print_cases pretends that there is a ?case-binding which does not exist in reality, i.e.

  case case1 then show ?case ...

fails because ?case is not bound. For a case distinction theorem like the above (but without consumes-declaration) such a binding would seem quite useful to me.

  -- Lars
theory Test imports Main begin

consts precond1 :: bool
consts precond2 :: bool
consts case1 :: bool
consts case2 :: bool

lemma case_rule[consumes 2, case_names case1 case2]:
  assumes "precond1"
  assumes "precond2"
  assumes "case1 \<Longrightarrow> Q"
  assumes "case2 \<Longrightarrow> Q"
  shows "Q"
  sorry

lemma
  assumes "precond1" and "precond2"
  shows Q
using assms proof (cases rule: case_rule)
print_cases
oops

lemma
  assumes "precond1"
  shows Q
using assms proof (cases rule: case_rule)
print_cases
oops

end


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