# Re: [isabelle] instance theorems

from Sean McLaughlin:
Hello,
How do you get at the theorems which prove the "instance" calls?
Eg. the proof term for
instance * :: (finite, finite) finite
proof
show "finite (UNIV :: ('a � 'b) set)"
proof (rule finite_Prod_UNIV)
show "finite (UNIV :: 'a set)" by (rule finite)
show "finite (UNIV :: 'b set)" by (rule finite)
qed
qed
Thanks,
Sean
Firstly - which I try to reply to Sean's email,
I get a window full of gibberish (this is on Mozilla thunderbird),

`does anyone else have this problem? or know what is different about
``Sean's email?
`
Secondly:
I'm not aware of how you can get the actual theorems,
but I think the information you want is printed by

`print_theory (I'm not sure, because that command produces more output
``than my terminal window's scroll buffer).
`
So what I do is:
(* print theory or parts of it *)
fun pfthy thy =
let
val ptl as [ names, theory_data, proof_data, name_prefix,
classes, default, witness, syntactic, logical, arities,
consts, finals, axioms, oracles ] =
Display.pretty_full_theory thy ;
in { all = ptl, names = names, theory_data = theory_data,
proof_data = proof_data, name_prefix = name_prefix,
classes = classes, default = default, witness = witness,
syntactic = syntactic, logical = logical, arities = arities,

` consts = consts, finals = finals, axioms = axioms, oracles =
``oracles }
` end ;
show_path () ;
val _ = print "end of gen.ML" ;
(*
val pthy = pfthy thy ;
Pretty.writelns (#all pthy) ;
Pretty.writeln (#proof_data pthy) ;
Pretty.writeln (#arities pthy) ;
Pretty.writeln (#classes pthy) ;
*)
The line
Pretty.writeln (#classes pthy) ;
gives the information I assume you want:
(since the subclass relation is transitive there are a lot more
subclass relations than those proved as instance theorems).
Pretty.writeln (#arities pthy) ;
gives the information about types being members of classes, again,
those actually proved as instance theorems and their consequences
Jeremy

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