class itself works around a problem with class interpretation in class finite
authorhaftmann
Tue Feb 26 20:38:16 2008 +0100 (2008-02-26)
changeset 261514a9b8f15ce7f
parent 26150 f6bd8686b71e
child 26152 cf2cccf17d6d
class itself works around a problem with class interpretation in class finite
src/HOL/Typedef.thy
     1.1 --- a/src/HOL/Typedef.thy	Tue Feb 26 20:38:15 2008 +0100
     1.2 +++ b/src/HOL/Typedef.thy	Tue Feb 26 20:38:16 2008 +0100
     1.3 @@ -114,4 +114,61 @@
     1.4    #> TypedefCodegen.setup
     1.5  *}
     1.6  
     1.7 +text {* This class is just a workaround for classes without parameters;
     1.8 +  it shall disappear as soon as possible. *}
     1.9 +
    1.10 +class itself = type + 
    1.11 +  fixes itself :: "'a itself"
    1.12 +
    1.13 +setup {*
    1.14 +let fun add_itself tyco thy =
    1.15 +  let
    1.16 +    val vs = Name.names Name.context "'a"
    1.17 +      (replicate (Sign.arity_number thy tyco) @{sort type});
    1.18 +    val ty = Type (tyco, map TFree vs);
    1.19 +    val lhs = Const (@{const_name itself}, Term.itselfT ty);
    1.20 +    val rhs = Logic.mk_type ty;
    1.21 +    val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs));
    1.22 +  in
    1.23 +    thy
    1.24 +    |> TheoryTarget.instantiation ([tyco], vs, @{sort itself})
    1.25 +    |> `(fn lthy => Syntax.check_term lthy eq)
    1.26 +    |-> (fn eq => Specification.definition (NONE, (("", []), eq)))
    1.27 +    |> snd
    1.28 +    |> Class.prove_instantiation_instance (K (Class.intro_classes_tac []))
    1.29 +    |> LocalTheory.exit
    1.30 +    |> ProofContext.theory_of
    1.31 +  end
    1.32 +in TypedefPackage.interpretation add_itself end
    1.33 +*}
    1.34 +
    1.35 +instantiation bool :: itself
    1.36 +begin
    1.37 +
    1.38 +definition "itself = TYPE(bool)"
    1.39 +
    1.40 +instance ..
    1.41 +
    1.42  end
    1.43 +
    1.44 +instantiation "fun" :: ("type", "type") itself
    1.45 +begin
    1.46 +
    1.47 +definition "itself = TYPE('a \<Rightarrow> 'b)"
    1.48 +
    1.49 +instance ..
    1.50 +
    1.51 +end
    1.52 +
    1.53 +instantiation "set" :: ("type") itself
    1.54 +begin
    1.55 +
    1.56 +definition "itself = TYPE('a set)"
    1.57 +
    1.58 +instance ..
    1.59 +
    1.60 +end
    1.61 +
    1.62 +hide (open) const itself
    1.63 +
    1.64 +end