Re: [isabelle] apply (cases a b c)



Johannes, thanks for the hint.

I think I have a slightly different situation. I have induction rule in the form:

inductive X :: "type ==> bool"
  c1 : X ...
| c2 : X ...

and I need to prove something like this:

X a ==> X b ==> X f(a,b)

I am trying to write ISAR proof individually considering
all combination of (c1,c2) constructors for 'a' and 'b':

case(a=c1,b=c1)
case(a=c1,b=c2)
case(a=c2,b=c1)
case(a=c2,b=c2)

I was looking for something like this:

proof(cases a b rule: X.cases)

Alternatively perhaps there is a way to nest proof methods applying

proof(cases a rule: X.cases)

and 

proof(cases b rule: X.cases)

sequentially?

I am sorry about such naive question, I am new to Isabelle. Thanks!

Vadim


On Jul 8, 2014, at 01:28 , Johannes Hölzl <hoelzl at in.tum.de> wrote:

> case_product should work with any case-style theorem of the form
>  R x y ==> (case one over x y ==> P) ==> (case two over x y ==> P) ==>
> P
> (where R is the inductive predicate. it is optional)
> 
> So you can write:
> 
>  dt.cases[case_product dt.cases]
> 
> - Johannes
> 
> 
> 
> Am Montag, den 07.07.2014, 18:55 -0700 schrieb Vadim Zaliva:
>> Hi!
>> 
>> If there is a way to use case_product attribute for inductive definitions?
>> For example if I have "inductive dt ..." it gives me dt.cases but no dt.exhaust.
>> Thanks!
>> 
>> Vadim
>> 
>> On Jun 20, 2014, at 06:58 , Johannes Hölzl <hoelzl at in.tum.de> wrote:
>> 
>>> You can use the case_product attribute:
>>> 
>>> by (cases a b rule: dt.exhaust[case_product dt.exhaust]) 
>>>    simp_all
>>> 
>>> And yes, I think it would be worth to extend the case method.
>>> 
>>> - Johannes
>>> 
>>> Am Freitag, den 20.06.2014, 15:53 +0200 schrieb Timothy Bourke:
>>>> Is there a built-in way to generate subgoals for all cases of a set of
>>>> variables?
>>>> 
>>>> For instance, suppose I have the definitions:
>>>> 
>>>> datatype dt = Num int | Infinity
>>>> 
>>>> fun plus :: "dt ⇒ dt ⇒ dt"
>>>> where
>>>>   "plus Infinity _ = Infinity"
>>>> | "plus _ Infinity = Infinity"
>>>> | "plus (Num a) (Num b) = Num (a + b)"
>>>> 
>>>> And now that I want to show:
>>>> 
>>>> lemma "plus a b = plus b a"
>>>> 
>>>> I would like to be able to type:
>>>>   by (cases a b) simp_all
>>>> 
>>>> But this is not supported.
>>>> 
>>>> I know that I can type:
>>>> by (tactic "(List.foldl (op THEN_ALL_NEW) (fn i => all_tac)
>>>>               (List.map (Induct_Tacs.case_tac @{context}) ["a", "b"]) 1)")
>>>>    simp_all
>>>> 
>>>> But somehow this is not very pleasing!
>>>> 
>>>> So, is there a good way to do this?
>>>> 
>>>> Would it be worth extending the cases method?
>>>> 
>>>> Tim.
>>>> 
>>> 
>>> 
>>> 
>> 
>> Sincerely,
>> Vadim Zaliva
>> 
>> --
>> CMU ECE PhD student
>> Mobile: +1(510)220-1060
>> Skype: vzaliva
>> 
> 
> 

Sincerely,
Vadim Zaliva





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