# 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:
```
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.