Re: [isabelle] instance theorems

from Sean McLaughlin:


  How do you get at the theorems which prove the "instance" calls?
Eg. the proof term for

instance * :: (finite, finite) finite
  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)



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?


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 =
    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


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