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.