# HG changeset patch # User haftmann # Date 1204144866 -3600 # Node ID 3bd9ac4e0b971d16d1c19ac2861d59760da78df7 # Parent ccc9007a71647a3ed96e1be283756a30ba928e7c added theory for reflected types diff -r ccc9007a7164 -r 3bd9ac4e0b97 src/HOL/Library/Eval.thy --- a/src/HOL/Library/Eval.thy Wed Feb 27 21:41:05 2008 +0100 +++ b/src/HOL/Library/Eval.thy Wed Feb 27 21:41:06 2008 +0100 @@ -7,105 +7,10 @@ theory Eval imports - ATP_Linkup Code_Message + RType Code_Index (* this theory is just imported for a term_of setup *) begin -subsection {* Type reflection *} - -subsubsection {* Definition *} - -types vname = message_string; -types "class" = message_string; -types sort = "class list" - -datatype "typ" = - Type message_string "typ list" - | TFree vname sort - -ML {* -structure Eval = -struct - -val mk_sort = HOLogic.mk_list @{typ class} o map Message_String.mk; - -fun mk_typ f (Type (tyco, tys)) = - @{term Type} $ Message_String.mk tyco - $ HOLogic.mk_list @{typ typ} (map (mk_typ f) tys) - | mk_typ f (TFree v) = - f v; - -end; -*} - - -subsubsection {* Class @{text typ_of} *} - -class typ_of = - fixes typ_of :: "'a\{} itself \ typ" - -ML {* -structure Eval = -struct - -open Eval; - -fun mk_typ_of ty = - Const (@{const_name typ_of}, Term.itselfT ty --> @{typ typ}) - $ Logic.mk_type ty; - -fun add_typ_of_def tyco thy = - let - val sorts = replicate (Sign.arity_number thy tyco) @{sort typ_of}; - val vs = Name.names Name.context "'a" sorts; - val ty = Type (tyco, map TFree vs); - val lhs = Const (@{const_name typ_of}, Term.itselfT ty --> @{typ typ}) - $ Free ("T", Term.itselfT ty); - val rhs = mk_typ (fn v => mk_typ_of (TFree v)) ty; - val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs)); - in - thy - |> TheoryTarget.instantiation ([tyco], vs, @{sort typ_of}) - |> `(fn lthy => Syntax.check_term lthy eq) - |-> (fn eq => Specification.definition (NONE, (("", []), eq))) - |> snd - |> Class.prove_instantiation_instance (K (Class.intro_classes_tac [])) - |> LocalTheory.exit - |> ProofContext.theory_of - end; - -end -*} - -(*setup {* -let - open Eval; -in - Eval.add_typ_of_def @{type_name prop} - #> Eval.add_typ_of_def @{type_name fun} - #> Eval.add_typ_of_def @{type_name itself} - #> Eval.add_typ_of_def @{type_name bool} - #> Eval.add_typ_of_def @{type_name set} - #> TypedefPackage.interpretation Eval.add_typ_of_def -end -*}*) - -subsubsection {* Code generator setup *} - -lemma [code func]: - "Type tyco1 tys1 = Type tyco2 tys2 \ tyco1 = tyco2 - \ list_all2 (op =) tys1 tys2" - by (auto simp add: list_all2_eq [symmetric]) - -code_type "typ" - (SML "Term.typ") - -code_const Type and TFree - (SML "Term.Type/ (_, _)" and "Term.TFree/ (_, _)") - -code_reserved SML Term - - subsection {* Term representation *} subsubsection {* Definitions *} @@ -113,7 +18,7 @@ datatype "term" = dummy_term definition - Const :: "message_string \ typ \ term" + Const :: "message_string \ rtype \ term" where "Const _ _ = dummy_term" @@ -124,10 +29,11 @@ code_datatype Const App + subsubsection {* Class @{term term_of} *} -class term_of = typ_of + - constrains typ_of :: "'a\{} itself \ typ" +class term_of = rtype + + constrains typ_of :: "'a\{} itself \ rtype" fixes term_of :: "'a \ term" lemma term_of_anything: "term_of x \ t" @@ -137,8 +43,6 @@ structure Eval = struct -open Eval; - fun mk_term f g (Const (c, ty)) = @{term Const} $ Message_String.mk c $ g ty | mk_term f g (t1 $ t2) = @@ -152,9 +56,6 @@ setup {* let - fun has_no_inst tyco sort thy = - not (can (Sorts.mg_domain (Sign.classes_of thy) tyco) - sort); fun add_term_of_def ty vs tyco thy = let val lhs = Const (@{const_name term_of}, ty --> @{typ term}) @@ -173,20 +74,18 @@ end; fun interpretator (tyco, (raw_vs, _)) thy = let + val has_inst = can (Sorts.mg_domain (Sign.classes_of thy) tyco) @{sort term_of}; val constrain_sort = curry (Sorts.inter_sort (Sign.classes_of thy)) @{sort term_of}; val vs = (map o apsnd) constrain_sort raw_vs; val ty = Type (tyco, map TFree vs); in thy - |> `(has_no_inst tyco @{sort typ_of}) - |-> (fn no_typ_of => no_typ_of ? Eval.add_typ_of_def tyco) - |> `(has_no_inst tyco @{sort term_of}) - |-> (fn no_term_of => no_term_of ? add_term_of_def ty vs tyco) + |> RType.perhaps_add_def tyco + |> not has_inst ? add_term_of_def ty vs tyco end; in - Eval.add_typ_of_def @{type_name fun} - #> Code.type_interpretation interpretator + Code.type_interpretation interpretator end *} @@ -198,7 +97,7 @@ map Free (Name.names Name.context "a" tys)); in (map_aterms (fn Free (v, ty) => Var ((v, 0), ty) | t => t) t, Eval.mk_term (fn (v, ty) => Eval.mk_term_of ty (Var ((v, 0), ty))) - (Eval.mk_typ (fn (v, sort) => Eval.mk_typ_of (TFree (v, sort)))) t) + (RType.mk (fn (v, sort) => RType.rtype (TFree (v, sort)))) t) end; fun prove_term_of_eq ty eq thy = let @@ -236,7 +135,7 @@ lemmas [code func del] = term.recs term.cases term.size lemma [code func, code func del]: "(t1\term) = t2 \ t1 = t2" .. -lemma [code func, code func del]: "(term_of \ typ \ term) = term_of" .. +lemma [code func, code func del]: "(term_of \ rtype \ term) = term_of" .. lemma [code func, code func del]: "(term_of \ term \ term) = term_of" .. lemma [code func, code func del]: "(term_of \ index \ term) = term_of" .. lemma [code func, code func del]: "(term_of \ message_string \ term) = term_of" .. @@ -335,7 +234,7 @@ end *} -hide (open) const Type TFree typ_of term_of +hide (open) const term_of hide const Const App dummy_term end diff -r ccc9007a7164 -r 3bd9ac4e0b97 src/HOL/Library/RType.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Library/RType.thy Wed Feb 27 21:41:06 2008 +0100 @@ -0,0 +1,109 @@ +(* Title: HOL/Library/RType.thy + ID: $Id$ + Author: Florian Haftmann, TU Muenchen +*) + +header {* Reflecting Pure types into HOL *} + +theory RType +imports Main Code_Message +begin + +datatype "rtype" = RType message_string "rtype list" + +class rtype = + fixes rtype :: "'a\{} itself \ rtype" +begin + +definition + rtype_of :: "'a \ rtype" +where + [simp]: "rtype_of x = rtype TYPE('a)" + +end + +setup {* +let + fun rtype_tr (*"_RTYPE"*) [ty] = + Lexicon.const @{const_syntax rtype} $ (Lexicon.const "_constrain" $ Lexicon.const "TYPE" $ + (Lexicon.const "itself" $ ty)) + | rtype_tr (*"_RTYPE"*) ts = raise TERM ("rtype_tr", ts); + fun rtype_tr' show_sorts (*"rtype"*) + (Type ("fun", [Type ("itself", [T]), _])) (Const (@{const_syntax TYPE}, _) :: ts) = + Term.list_comb (Lexicon.const "_RTYPE" $ Syntax.term_of_typ show_sorts T, ts) + | rtype_tr' _ T ts = raise Match; +in + Sign.add_syntax_i + [("_RTYPE", SimpleSyntax.read_typ "type => logic", Delimfix "(1RTYPE/(1'(_')))")] + #> Sign.add_trfuns ([], [("_RTYPE", rtype_tr)], [], []) + #> Sign.add_trfunsT [(@{const_syntax rtype}, rtype_tr')] +end +*} + +ML {* +structure RType = +struct + +fun mk f (Type (tyco, tys)) = + @{term RType} $ Message_String.mk tyco + $ HOLogic.mk_list @{typ rtype} (map (mk f) tys) + | mk f (TFree v) = + f v; + +fun rtype ty = + Const (@{const_name rtype}, Term.itselfT ty --> @{typ rtype}) + $ Logic.mk_type ty; + +fun add_def tyco thy = + let + val sorts = replicate (Sign.arity_number thy tyco) @{sort rtype}; + val vs = Name.names Name.context "'a" sorts; + val ty = Type (tyco, map TFree vs); + val lhs = Const (@{const_name rtype}, Term.itselfT ty --> @{typ rtype}) + $ Free ("T", Term.itselfT ty); + val rhs = mk (rtype o TFree) ty; + val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs)); + in + thy + |> TheoryTarget.instantiation ([tyco], vs, @{sort rtype}) + |> `(fn lthy => Syntax.check_term lthy eq) + |-> (fn eq => Specification.definition (NONE, (("", []), eq))) + |> snd + |> Class.prove_instantiation_instance (K (Class.intro_classes_tac [])) + |> LocalTheory.exit + |> ProofContext.theory_of + end; + +fun perhaps_add_def tyco thy = + let + val inst = can (Sorts.mg_domain (Sign.classes_of thy) tyco) @{sort rtype} + in if inst then thy else add_def tyco thy end; + +end; +*} + +setup {* + RType.add_def @{type_name prop} + #> RType.add_def @{type_name fun} + #> RType.add_def @{type_name itself} + #> RType.add_def @{type_name bool} + #> RType.add_def @{type_name set} + #> TypedefPackage.interpretation RType.perhaps_add_def +*} + +lemma [code func]: + "RType tyco1 tys1 = RType tyco2 tys2 \ tyco1 = tyco2 + \ list_all2 (op =) tys1 tys2" + by (auto simp add: list_all2_eq [symmetric]) + +code_type rtype + (SML "Term.typ") + +code_const RType + (SML "Term.Type/ (_, _)") + +code_reserved SML Term + +hide (open) const rtype RType + +end