Email Gateway (Aug 17 2022 at 13:46): Email Gateway (Aug 17 2022 at 13:46):From: Sean McLaughlin <seanmcl@cmu.edu>
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
Email Gateway (Aug 17 2022 at 13:46):From: Jeremy Dawson <Jeremy.Dawson@rsise.anu.edu.au>
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
Last updated: May 03 2024 at 08:18 UTC