Email Gateway (Aug 19 2022 at 14:36): Email Gateway (Aug 19 2022 at 14:36):From: Timothy Bourke <tim@tbrk.org>
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.
signature.asc
Email Gateway (Aug 19 2022 at 14:37):From: Johannes Hölzl <hoelzl@in.tum.de>
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.
Email Gateway (Aug 19 2022 at 14:37):From: Brian Huffman <huffman.brian.c@gmail.com>
You can also use the custom induct or cases rules provided by the "fun" command.
lemma "plus a b = plus b a"
apply (cases "(a, b)" rule: plus.cases)
or
lemma "plus a b = plus b a"
apply (induct a b rule: plus.induct)
These give you one case corresponding to each equation in plus.simps,
which may be a different set of cases than you would get with the
case_product rule.
Email Gateway (Aug 19 2022 at 15:14):From: Johannes Hölzl <hoelzl@in.tum.de>
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]
Email Gateway (Aug 19 2022 at 15:14):From: Vadim Zaliva <vzaliva@cmu.edu>
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
Sincerely,
Vadim Zaliva
Email Gateway (Aug 19 2022 at 15:15):From: Vadim Zaliva <vzaliva@cmu.edu>
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
Sincerely,
Vadim Zaliva
Email Gateway (Aug 19 2022 at 15:15):From: Johannes Hölzl <hoelzl@in.tum.de>
Hm, do you need case distinction over X at all?
Why not:
proof (cases a b rule: type.exhaust[case_product type.exhaust])
Where type is the name of your type.
But maybe I didn't understand your goal. But for this I need more
information, for example the definition of your predicate X and type
"type" and the theorem you want to proof. You can also attach your
theory development if you want.
Last updated: Apr 25 2024 at 20:15 UTC