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.