*To*: Mandy Martin <tesleft at hotmail.com>*Subject*: Re: [isabelle] How do Isabelle use logic table to prove exist some, all, belong to*From*: Makarius <makarius at sketis.net>*Date*: Sat, 11 Apr 2015 23:02:19 +0200 (CEST)*Cc*: isabelle-users <isabelle-users at cl.cam.ac.uk>, Harry Butterworth <heb1001 at gmail.com>*In-reply-to*: <BAY167-W55B791C7DA1B29B07ACB9FB6F90@phx.gbl>*References*: <CAPWZQLq=pbRwXZC0N9h46L7eh=Qqyt2EO6e71v_ecfBcq75RpQ@mail.gmail.com>, <CAPWZQLqH=SKgFohEqyWt_3uJsC2XK8EjeZ2=B_Hfg=t04C8M0w@mail.gmail.com>, <3DC7F053-2741-4CCB-92DA-7112B3E192B0@cam.ac.uk>, <BAY167-W115A944EF99DD33F513BDB6B6FB0@phx.gbl>, <52F398EA-D07E-4B60-A23A-1FE0E96E2266@cam.ac.uk>, <CAMUwPhxoY2qMpvA4-X6sBDhWvcbW9h=K+mM4w=SXzy+LmeWrhw@mail.gmail.com>, <alpine.LNX.2.00.1504112150180.54341@lxbroy10.informatik.tu-muenchen.de> <BAY167-W55B791C7DA1B29B07ACB9FB6F90@phx.gbl>*User-agent*: Alpine 2.00 (LNX 1167 2008-08-23)

On Sun, 12 Apr 2015, Mandy Martin wrote:

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

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?

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

Makarius

**References**:**[isabelle] Fwd: [Isabelle] Failed to parse prop***From:*Martin Lee

**Re: [isabelle] Fwd: [Isabelle] Failed to parse prop***From:*Larry Paulson

**[isabelle] How do Isabelle use logic table to prove exist some, all, belong to***From:*Mandy Martin

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

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

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

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

- Previous by Date: Re: [isabelle] How do Isabelle use logic table to prove exist some, all, belong to
- Next by Date: Re: [isabelle] Isabelle2015-RC0 available for testing
- Previous by Thread: Re: [isabelle] How do Isabelle use logic table to prove exist some, all, belong to
- Next by Thread: Re: [isabelle] Fwd: [Isabelle] Failed to parse prop
- Cl-isabelle-users April 2015 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list