Re: [isabelle] Discharging one (trivial) case without nesting the proof



On 05/19/2013 07:02 PM, Joachim Breitner wrote:
         lemma "Q S → P S"
         proof
           assume "Q S"
           show "P S"
           proof(cases "S = {}")
             assume True thus "P S" by simp
           next
             assume False
             then obtain "x ∈ S" by auto
             ..
             show "P S"
           qed
         qed

Instead, you could write:

lemma "Q S --> P S"
proof
  assume "Q S"
  show "P S"
  proof (cases "S = {}")
    assume "S ~= {}"
    then obtain "x : S" by auto
    ...
    show "P S"
  qed simp
qed

which looks (I guess) very similar to what you suggested:

     lemma "Q S → P S"
     proof
       assume "Q S"
       trivially "S ~= {}"
       proof
         assume "~ ~ S = {}"
         show "P S" by simp
       qed
       then obtain "x ∈ S" by auto
       ..
       show "P S"
     qed


Maybe I do not get your main point?

cheers

chris




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