Re: [isabelle] Isar syntax question



* Vadim Zaliva <vzaliva at cmu.edu> [2014-07-16 15:00 -0700]:
> I am learning Isar and have another naive question on the syntax:
> I am trying to do something like this in Isar:
> 
> 1: lemma
> 2:   shows "not something"
> 3: proof(rule ccontr)
> 4:  assume "something"
> 5:  thus False proof cases
> 6: 	...
> 7:   qed
> 8: qed
> 
> and get "*** Failed to refine any pending goal" error around line 5
> 
> Why this does not work? Something like this works instead:

The consequent of ccontr does not match your stated goal.

You want rather

  lemma "¬ something"
  proof (rule notI)
    assume "something"
    thus False
      sorry
  qed

Typing "find_theorems intro" after line 2 gives a list of applicable
rules. But, in fact, in this case Isar finds the right rule by itself:

  lemma "¬ something"
  proof
    assume "something"
    thus False
      sorry
  qed

Tim.

Attachment: signature.asc
Description: Digital signature



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