Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Isar and induction?

Email Gateway (Aug 18 2022 at 10:31):

From: Alexander Krauss <krauss@in.tum.de>
Hi David,

In the last line of the following proof I am tring to use a known
fact (that is something that appears in the prems list of facts) by
placing it between \<langle> and \<rangle>.
Am I unable to refer to facts like this?

In recent Isabelle versions (post-2005 developer's version, I believe),
you can refer to literal facts using backquotes. They are just converted
to the small angle brackets in printed theory sources.

lemma "A --> A"
proof
assume "A"

from A show "A" .
qed

Note that there are also other ways to reference facts:

• If you are inside a "case", the name of the case refers to a list of
  assumptions

• You can use prems(i) (where i is a number). This actually works for
  any list of facts.

using p proof (induct rule: lts.fat_act.induct) --" fixing: P
fails to parse"

The "fixing" option is now called "arbitrary".

Question 2.

The next thing I tried was
from prems tinAB [where t = s and A = A and P = (Abs P) and Q
= (Abs Q)] show ?case

but this failed to parse.

so I rewrote tinAA replacing P by Abs P and Q by Abs Q. Thus I used.

from prems tinAB [where t = s and A = A and P = P and Q = Q] show
?case

Have I missed some thing or are the right hand side of these equalities
very restricted?

You are missing quotes:

from prems tinAB [where t = s and A = A and P ="(Abs P)"
and Q = "(Abs Q)"] show ?case

Every term or type ("inner syntax") must be quoted. Just for single
symbols, the quotes can be ommitted.

Question 3. I have defined parallel composition but the transitions in
this definition are the union of three somewhat complexe sets. I will
frequently need to split these transitions into the three cases and
proove my results for each case (set).

I haven't looked very closely at your specific instance... but in
general you want a rule which can be used as an elimination rule. This
should have the following format (more or less):

lemma mytrans_cases:
"t : trans (par P A Q)
==> ((fst_tran t : trans P & ...) ==> C)
==> ((snd_tran t : trans Q & ...) ==> C)
==> (!!a. (act t : trans P & a : liftobs A ...) ==> C)
==> C"

Here is a simple example that actually works:

definition
"myRel P = {(x,y). P x y | P y x}"

lemma myRel_cases[consumes 1]:
"[| (x,y) : myRel P;
P x y ==> A;
P y x ==> A |]
==> A"
unfolding myRel_def
by blast

lemma example: "(x,y) : myRel P ==> something"
proof -
assume "(x,y) : myRel P"
thus something
proof (cases rule:myRel_cases)
assume "P x y" thus something sorry
next
assume "P y x" thus something sorry
qed
qed

Note that the existentials in your lemma become universals in the
cases-theorem, since you are working "on the left hand side of the arrow".

The "consumes 1" attribute tells the "cases" method to resolve one
premise with the assumptions in your actual proof. To get a clearer
understanding of what happens here, just leave it out and see what changes.

If you need the splitting very often, you can also give names to the
different cases, which makes proofs look nicer. For the simple example:

lemma myRel_cases[consumes 1, case_names foo bar]:
"[| (x,y) : myRel P;
P x y ==> A;
P y x ==> A |]
==> A"
unfolding myRel_def
by blast

lemma "(x,y) : myRel P ==> something"
proof -
assume "(x,y) : myRel P"
thus something
proof (cases rule:myRel_cases)
case foo thus something sorry
next
case bar thus something sorry
qed
qed

You will be excited about how pretty your proofs can become :-)

Alex

Last updated: May 03 2024 at 04:19 UTC