# Re: [isabelle] type inference in HOL

```paolot at informatik.uni-bremen.de wrote:
```
```ok, thanks. Still, the example I had in mind was:

consts
consA :: "('a*bool)"

constdefs
consB_def : "consB == snd consA"
```
```
If you define consA as follows

consA == (arbitrary::'a, ALL (x::'a) (y::'a). x = y)

which is a perfectly legal definition, since 'a occurs
both on the left-hand and on the right-hand side, you
could still derive an inconsistency in a similar way
by using the (illegal) definition of consB.

Greetings,
Stefan

--
Dr. Stefan Berghofer               E-Mail: berghofe at in.tum.de
Institut fuer Informatik           Phone: +49 89 289 17328
Technische Universitaet Muenchen   Fax:   +49 89 289 17307
Boltzmannstr. 3                    Room: 01.11.059
85748 Garching, GERMANY            http://www.in.tum.de/~berghofe
```
```theory Inconsistency
imports Main
begin

(* a legal definition *)
constdefs
consA :: "'a * bool"
"consA == (arbitrary::'a, ALL (x::'a) (y::'a). x = y)"

consts
consB :: bool

(* not a legal definition *)
axioms
consB_def: "consB == snd consA"

lemma "True = False"
proof -
have "True = (ALL (x::unit) y. x = y)" by simp
also have "\<dots> = consB"
by (simp add: consA_def consB_def [where 'a=unit])
also have "\<dots> = (ALL (x::bool) y. x = y)"
by (simp add: consA_def consB_def [where 'a=bool])
also have "\<dots> = False" by auto
finally show ?thesis .
qed

end
```

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