# HG changeset patch # User kuncar # Date 1354208060 -3600 # Node ID 986598b0efd11392c8d71e88d03fb91d1d59edcb # Parent cb4bdcbfdb8d557475c44a76c9339ffee405fcac parametrized correspondence relation: more robust procedure - don't ignore sorts; tuned diff -r cb4bdcbfdb8d -r 986598b0efd1 src/HOL/Tools/Lifting/lifting_setup.ML --- a/src/HOL/Tools/Lifting/lifting_setup.ML Thu Nov 29 14:29:29 2012 +0100 +++ b/src/HOL/Tools/Lifting/lifting_setup.ML Thu Nov 29 17:54:20 2012 +0100 @@ -48,28 +48,28 @@ fun define_pcrel crel lthy = let - val pcrel = Morphism.term (Local_Theory.target_morphism lthy) crel - val [crel_poly] = Variable.polymorphic lthy [pcrel] - val rty_raw = (domain_type o fastype_of) crel_poly - val (quot_thm, assms) = Lifting_Term.prove_param_quot_thm lthy rty_raw - val args = map (fn (_, q_thm) => quot_thm_crel q_thm) assms - val parametrized_relator = quot_thm_crel quot_thm - val [rty, rty'] = (binder_types o fastype_of) parametrized_relator + val (fixed_crel, lthy) = yield_singleton Variable.importT_terms crel lthy + val [rty', qty] = (binder_types o fastype_of) fixed_crel + val (param_rel, args) = Lifting_Term.generate_parametrized_relator lthy rty' + val rty_raw = (domain_type o range_type o fastype_of) param_rel val thy = Proof_Context.theory_of lthy val tyenv_match = Sign.typ_match thy (rty_raw, rty') Vartab.empty - val crel_subst = Envir.subst_term (tyenv_match,Vartab.empty) crel_poly - val lthy = Variable.declare_names parametrized_relator lthy - val (crel_typed, lthy) = yield_singleton Variable.importT_terms crel_subst lthy - val qty = (domain_type o range_type o fastype_of) crel_typed + val param_rel_subst = Envir.subst_term (tyenv_match,Vartab.empty) param_rel + val args_subst = map (Envir.subst_term (tyenv_match,Vartab.empty)) args + val lthy = Variable.declare_names fixed_crel lthy + val (instT, lthy) = Variable.importT_inst (param_rel_subst :: args_subst) lthy + val args_fixed = (map (Term_Subst.instantiate (instT, []))) args_subst + val param_rel_fixed = Term_Subst.instantiate (instT, []) param_rel_subst + val rty = (domain_type o fastype_of) param_rel_fixed val relcomp_op = Const (@{const_name "relcompp"}, (rty --> rty' --> HOLogic.boolT) --> (rty' --> qty --> HOLogic.boolT) --> rty --> qty --> HOLogic.boolT) - val relator_type = foldr1 (op -->) ((map type_of args) @ [rty, qty, HOLogic.boolT]) + val relator_type = foldr1 (op -->) ((map type_of args_fixed) @ [rty, qty, HOLogic.boolT]) val qty_name = (fst o dest_Type) qty val pcrel_name = Binding.prefix_name "pcr_" ((Binding.name o Long_Name.base_name) qty_name) - val lhs = Library.foldl (op $) ((Free (Binding.name_of pcrel_name, relator_type)), args) - val rhs = relcomp_op $ parametrized_relator $ crel_typed + val lhs = Library.foldl (op $) ((Free (Binding.name_of pcrel_name, relator_type)), args_fixed) + val rhs = relcomp_op $ param_rel_fixed $ fixed_crel; val definition_term = Logic.mk_equals (lhs, rhs) val ((_, (_, def_thm)), lthy) = Specification.definition ((SOME (pcrel_name, SOME relator_type, NoSyn)), ((Binding.empty, []), definition_term)) lthy diff -r cb4bdcbfdb8d -r 986598b0efd1 src/HOL/Tools/Lifting/lifting_term.ML --- a/src/HOL/Tools/Lifting/lifting_term.ML Thu Nov 29 14:29:29 2012 +0100 +++ b/src/HOL/Tools/Lifting/lifting_term.ML Thu Nov 29 17:54:20 2012 +0100 @@ -16,7 +16,9 @@ val equiv_relation: Proof.context -> typ * typ -> term - val prove_param_quot_thm: Proof.context -> typ -> thm * (typ * thm) list + val prove_param_quot_thm: Proof.context -> typ -> thm * (typ * thm) list * Proof.context + + val generate_parametrized_relator: Proof.context -> typ -> term * term list end structure Lifting_Term: LIFTING_TERM = @@ -238,14 +240,33 @@ fun equiv_relation ctxt (rty, qty) = quot_thm_rel (prove_quot_thm ctxt (rty, qty)) -fun get_fresh_Q_t ctxt = +val get_fresh_Q_t = let - val Q_t = Syntax.read_term ctxt "Trueprop (Quotient R Abs Rep T)" - val ctxt = Variable.declare_names Q_t ctxt + val Q_t = @{term "Trueprop (Quotient R Abs Rep T)"} val frees_Q_t = Term.add_free_names Q_t [] - val (_, ctxt) = Variable.variant_fixes frees_Q_t ctxt + val tfrees_Q_t = rev (Term.add_tfree_names Q_t []) in - (Q_t, ctxt) + fn ctxt => + let + fun rename_free_var tab (Free (name, typ)) = Free (the_default name (AList.lookup op= tab name),typ) + | rename_free_var _ t = t + + fun rename_free_vars tab = map_aterms (rename_free_var tab) + + fun rename_free_tvars tab = + map_types (map_type_tfree (fn (name, sort) => TFree (the_default name (AList.lookup op= tab name), sort))) + + val (new_frees_Q_t, ctxt) = Variable.variant_fixes frees_Q_t ctxt + val tab_frees = frees_Q_t ~~ new_frees_Q_t + + val (new_tfrees_Q_t, ctxt) = Variable.invent_types (replicate (length tfrees_Q_t) []) ctxt + val tab_tfrees = tfrees_Q_t ~~ (fst o split_list) new_tfrees_Q_t + + val renamed_Q_t = rename_free_vars tab_frees Q_t + val renamed_Q_t = rename_free_tvars tab_tfrees renamed_Q_t + in + (renamed_Q_t, ctxt) + end end fun prove_param_quot_thm ctxt ty = @@ -265,7 +286,7 @@ in (args MRSL (get_rel_quot_thm ctxt s), table_ctxt) end - | generate (ty as (TVar _)) (table, ctxt) = + | generate (ty as (TFree _)) (table, ctxt) = if AList.defined (op=) table ty then (the (AList.lookup (op=) table ty), (table, ctxt)) else @@ -277,12 +298,23 @@ in (Q_thm, (table', ctxt')) end - | generate _ _ = error "generate_param_quot_thm: TFree" + | generate _ _ = error "generate_param_quot_thm: TVar" - val (param_quot_thm, (table, _)) = generate ty ([], ctxt) + val (param_quot_thm, (table, ctxt)) = generate ty ([], ctxt) in - (param_quot_thm, rev table) + (param_quot_thm, rev table, ctxt) end handle QUOT_THM_INTERNAL pretty_msg => raise PARAM_QUOT_THM (ty, pretty_msg) +fun generate_parametrized_relator ctxt ty = + let + val orig_ctxt = ctxt + val (quot_thm, table, ctxt) = prove_param_quot_thm ctxt ty + val parametrized_relator = quot_thm_crel quot_thm + val args = map (fn (_, q_thm) => quot_thm_crel q_thm) table + val exported_terms = Variable.exportT_terms ctxt orig_ctxt (parametrized_relator :: args) + in + (hd exported_terms, tl exported_terms) + end + end;