Re: [isabelle] A simple theorem

```On Tue, 20 Sep 2011, Mathieu Giorgino wrote:

```
```Le Mardi 20 Septembre 2011 10:12:10 John Munroe a écrit :
```
```Hi all,

Given

axiomatization
c :: real and
d :: real
where ax1 : "c > 0"
and ax2 : "d > 0"

does anyone know how to prove

lemma "c * d > 0"?

It seems using the facts ax1 ax2 isn't sufficient.
```
```
```
Just a stylistic note: raw axiomatizations affect the foundation of the logic, and can easily produce global inconsistency, where eveything breaks down.
```
```
In Isabelle/Isar local experimentation can be done within a proof context. Since Isabelle2011 there is also a stand-alone command for that: 'notepad'. Here is the example in that style:
```
begin
fix c :: real
fix d :: real
assume *: "c > 0"
assume **: "d > 0"
have "c * d > 0" sorry
end

Now you can proceed as suggested before ...

```
```Invoking Sledgehammer (with command "sledgehammer") immediately gives a
solution:
by (metis ax1 ax2 real_mult_order)

which can then be rewritten:
by (simp add: real_mult_order[OF ax1 ax2])

or even:
by (rule real_mult_order[OF ax1 ax2])
```
```

Makarius```

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