Re: [isabelle] Two questions of a beginner



On Fri, 18 Jan 2013, Peter Lammich wrote:

Not an answer for a beginner: I'm frequently using the following code,
that gives you a method rprems, that does exactly the requested thing
(see examples below the code).

(* EXAMPLES: *)


lemma "\<lbrakk> A\<Longrightarrow>B; B\<Longrightarrow>C; A \<rbrakk>
\<Longrightarrow> C"
 apply (rprems 2) -- "Explicitely specify number of premise"
 apply (rprems 1)
 .

lemma "\<lbrakk> A\<Longrightarrow>B; B\<Longrightarrow>C; A \<rbrakk>
\<Longrightarrow> C"
 apply (rprems) -- "Resolve with any matching premise,
   first to last, backtracking"
 apply (rprems)

These numbers within proofs scripts are not nice. Many years ago, some people thinking about structured proofs devised ways to name subgoals and subgoals premises, instead of numbering them. But I did not find this very convincing either. It was one of the early achievements of Isar to manage without that -- and thus continuing the way Larry introduced elim/dest resolution without physical addressing.

So where are the applications? This thread was started as beginner questions, to warm up how things are usually done.


	Makarius





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