Re: [isabelle] How do Isabelle use logic table to prove exist some, all, belong to



On Sun, 12 Apr 2015, Mandy Martin wrote:

it is difficult to imagine infinite disjunction and conjunction in truth table 1. does it mean that there are infinite disjunction to connect the final result columns of infinite truth tables, infinite conjunction to connect final result columns of infinite truth tables

Yes. A table can be easily infinite, you just draw "..." on the blackboard or paper and imagine the rest in your mind.


2.  i got a question about subgoal when prove simple logic, because when
   i prove in Isabelle, the only subgoal it the lemma itself.  i would
   like to know where do subgoals come from.without assumptions, where
   do subgoals come from?

Subgoals emerge by applying a rule backwards. E.g. you start with a goal "A & B" and apply the rule conjI: this produces subgoals A and B.

The Isar proof language has the virtue that it shows the structure of sub-proofs directly in the text, in correspondence to Natural Deduction rules that are applied (implicitly or explicitly). So you can just write out the resoning directly, letting the system do the internal bookkeeping of goals and rules:

notepad
begin

  -- "explicit rules"

  fix A B :: bool
  have "A â B â B â A"
  proof (rule impI)
    assume *: "A â B"
    from * have a: A by (rule conjunct1)
    from * have b: B by (rule conjunct2)
    from b and a show "B â A" by (rule conjI)
  qed

next

  -- "implicit rules"

  fix A B :: bool
  have "A â B â B â A"
  proof
    assume *: "A â B"
    from * have a: A ..
    from * have b: B ..
    from b and a show "B â A" ..
  qed

end


The Isabelle documentation provides more information on all that, tons of manuals and examples ...


	Makarius


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