# HG changeset patch # User kuncar # Date 1337188640 -7200 # Node ID 70375fa2679d9e0caa3435ad2b002725c30c955f # Parent 756f30eac7926b60426af2e8086a5f043cd8c07b generate abs_eq, use it as a code equation for total quotients; no_abs_code renamed to no_code; added no_code for quotient_type command diff -r 756f30eac792 -r 70375fa2679d src/HOL/Library/Float.thy --- a/src/HOL/Library/Float.thy Wed May 16 19:15:45 2012 +0200 +++ b/src/HOL/Library/Float.thy Wed May 16 19:17:20 2012 +0200 @@ -19,7 +19,7 @@ lemma type_definition_float': "type_definition real float_of float" using type_definition_float unfolding real_of_float_def . -setup_lifting (no_abs_code) type_definition_float' +setup_lifting (no_code) type_definition_float' lemmas float_of_inject[simp] diff -r 756f30eac792 -r 70375fa2679d src/HOL/Lifting.thy --- a/src/HOL/Lifting.thy Wed May 16 19:15:45 2012 +0200 +++ b/src/HOL/Lifting.thy Wed May 16 19:17:20 2012 +0200 @@ -82,10 +82,31 @@ using a unfolding Quotient_def by blast +lemma Quotient_rep_abs_fold_unmap: + assumes "x' \ Abs x" and "R x x" and "Rep x' \ Rep' x'" + shows "R (Rep' x') x" +proof - + have "R (Rep x') x" using assms(1-2) Quotient_rep_abs by auto + then show ?thesis using assms(3) by simp +qed + +lemma Quotient_Rep_eq: + assumes "x' \ Abs x" + shows "Rep x' \ Rep x'" +by simp + lemma Quotient_rel_abs: "R r s \ Abs r = Abs s" using a unfolding Quotient_def by blast +lemma Quotient_rel_abs2: + assumes "R (Rep x) y" + shows "x = Abs y" +proof - + from assms have "Abs (Rep x) = Abs y" by (auto intro: Quotient_rel_abs) + then show ?thesis using assms(1) by (simp add: Quotient_abs_rep) +qed + lemma Quotient_symp: "symp R" using a unfolding Quotient_def using sympI by (metis (full_types)) diff -r 756f30eac792 -r 70375fa2679d src/HOL/Quotient_Examples/Lift_FSet.thy --- a/src/HOL/Quotient_Examples/Lift_FSet.thy Wed May 16 19:15:45 2012 +0200 +++ b/src/HOL/Quotient_Examples/Lift_FSet.thy Wed May 16 19:17:20 2012 +0200 @@ -81,6 +81,10 @@ done qed +text {* We can export code: *} + +export_code fnil fcons fappend fmap ffilter fset in SML + text {* Note that the generated transfer rule contains a composition of relations. The transfer rule is not yet very useful in this form. *} diff -r 756f30eac792 -r 70375fa2679d src/HOL/Relation.thy --- a/src/HOL/Relation.thy Wed May 16 19:15:45 2012 +0200 +++ b/src/HOL/Relation.thy Wed May 16 19:17:20 2012 +0200 @@ -173,6 +173,11 @@ obtains "r x x" using assms by (auto dest: refl_onD simp add: reflp_def) +lemma reflpD: + assumes "reflp r" + shows "r x x" + using assms by (auto elim: reflpE) + lemma refl_on_Int: "refl_on A r ==> refl_on B s ==> refl_on (A \ B) (r \ s)" by (unfold refl_on_def) blast diff -r 756f30eac792 -r 70375fa2679d src/HOL/Tools/Lifting/lifting_def.ML --- a/src/HOL/Tools/Lifting/lifting_def.ML Wed May 16 19:15:45 2012 +0200 +++ b/src/HOL/Tools/Lifting/lifting_def.ML Wed May 16 19:17:20 2012 +0200 @@ -30,6 +30,14 @@ fun get_binder_types (Type ("fun", [T, U]), Type ("fun", [V, W])) = (T, V) :: get_binder_types (U, W) | get_binder_types _ = [] +fun get_binder_types_by_rel (Const (@{const_name "fun_rel"}, _) $ _ $ S) (Type ("fun", [T, U]), Type ("fun", [V, W])) = + (T, V) :: get_binder_types_by_rel S (U, W) + | get_binder_types_by_rel _ _ = [] + +fun get_body_type_by_rel (Const (@{const_name "fun_rel"}, _) $ _ $ S) (Type ("fun", [_, U]), Type ("fun", [_, V])) = + get_body_type_by_rel S (U, V) + | get_body_type_by_rel _ (U, V) = (U, V) + fun force_rty_type ctxt rty rhs = let val thy = Proof_Context.theory_of ctxt @@ -75,9 +83,14 @@ Const (@{const_name "map_fun"}, _) $ _ $ _ => (Conv.arg_conv unfold_conv then_conv Conv.rewr_conv map_fun_unfolded) ctm | _ => Conv.all_conv ctm - val try_beta_conv = Conv.try_conv (Thm.beta_conversion false) in - (Conv.arg_conv (Conv.fun_conv unfold_conv then_conv try_beta_conv)) ctm + (Conv.fun_conv unfold_conv) ctm + end + +fun unfold_fun_maps_beta ctm = + let val try_beta_conv = Conv.try_conv (Thm.beta_conversion false) + in + (unfold_fun_maps then_conv try_beta_conv) ctm end fun prove_rel ctxt rsp_thm (rty, qty) = @@ -121,7 +134,7 @@ Const (@{const_name HOL.eq}, _) $ _ $ _ => abs_rep_thm | Const (@{const_name invariant}, _) $ _ $ _ $ _ => abs_rep_thm RS @{thm invariant_to_eq} | _ => raise CODE_CERT_GEN "relation is neither equality nor invariant" - val unfolded_def = Conv.fconv_rule unfold_fun_maps def_thm + val unfolded_def = Conv.fconv_rule (Conv.arg_conv unfold_fun_maps_beta) def_thm val unabs_def = unabs_all_def ctxt unfolded_def val rep = (cterm_of thy o Lifting_Term.quot_thm_rep) quot_thm val rep_refl = Thm.reflexive rep RS @{thm meta_eq_to_obj_eq} @@ -131,53 +144,150 @@ simplify_code_eq ctxt code_cert end -fun is_abstype ctxt typ = +fun generate_trivial_rep_eq ctxt def_thm = let - val thy = Proof_Context.theory_of ctxt - val type_name = (fst o dest_Type) typ + val unfolded_def = Conv.fconv_rule (Conv.arg_conv unfold_fun_maps_beta) def_thm + val code_eq = unabs_all_def ctxt unfolded_def + val simp_code_eq = simplify_code_eq ctxt code_eq in - (snd oo Code.get_type) thy type_name + simp_code_eq end - + +fun generate_rep_eq ctxt def_thm rsp_thm (rty, qty) = + if body_type rty = body_type qty then + SOME (generate_trivial_rep_eq ctxt def_thm) + else + let + val (rty_body, qty_body) = get_body_types (rty, qty) + val quot_thm = Lifting_Term.prove_quot_thm ctxt (rty_body, qty_body) + in + if can_generate_code_cert quot_thm then + SOME (generate_code_cert ctxt def_thm rsp_thm (rty, qty)) + else + NONE + end -fun define_code_cert code_eqn_thm_name def_thm rsp_thm (rty, qty) lthy = +fun generate_abs_eq ctxt def_thm rsp_thm quot_thm = let - val (rty_body, qty_body) = get_body_types (rty, qty) - val quot_thm = Lifting_Term.prove_quot_thm lthy (rty_body, qty_body) + fun refl_tac ctxt = + let + fun intro_reflp_tac (t, i) = + let + val concl_pat = Drule.strip_imp_concl (cprop_of @{thm reflpD}) + val insts = Thm.first_order_match (concl_pat, t) + in + rtac (Drule.instantiate_normalize insts @{thm reflpD}) i + end + handle Pattern.MATCH => no_tac + + val fun_rel_meta_eq = mk_meta_eq @{thm fun_rel_eq} + val conv = Conv.bottom_conv (K (Conv.try_conv (Conv.rewr_conv fun_rel_meta_eq))) ctxt + val rules = Lifting_Info.get_reflp_preserve_rules ctxt + in + EVERY' [CSUBGOAL intro_reflp_tac, + CONVERSION conv, + REPEAT_ALL_NEW (resolve_tac rules)] + end + + fun try_prove_prem ctxt prop = + SOME (Goal.prove ctxt [] [] prop (fn {context, ...} => refl_tac context 1)) + handle ERROR _ => NONE + + val abs_eq_with_assms = + let + val (rty, qty) = Lifting_Term.quot_thm_rty_qty quot_thm + val rel = Lifting_Term.quot_thm_rel quot_thm + val ty_args = get_binder_types_by_rel rel (rty, qty) + val body_type = get_body_type_by_rel rel (rty, qty) + val quot_ret_thm = Lifting_Term.prove_quot_thm ctxt body_type + + val rep_abs_folded_unmapped_thm = + let + val rep_id = [quot_thm, def_thm] MRSL @{thm Quotient_Rep_eq} + val ctm = Thm.dest_equals_lhs (cprop_of rep_id) + val unfolded_maps_eq = unfold_fun_maps ctm + val t1 = [quot_thm, def_thm, rsp_thm] MRSL @{thm Quotient_rep_abs_fold_unmap} + val prems_pat = (hd o Drule.cprems_of) t1 + val insts = Thm.first_order_match (prems_pat, cprop_of unfolded_maps_eq) + in + unfolded_maps_eq RS (Drule.instantiate_normalize insts t1) + end + in + rep_abs_folded_unmapped_thm + |> fold (fn _ => fn thm => thm RS @{thm fun_relD2}) ty_args + |> (fn x => x RS (@{thm Quotient_rel_abs2} OF [quot_ret_thm])) + end + + val prems = prems_of abs_eq_with_assms + val indexed_prems = map_index (apfst (fn x => x + 1)) prems + val indexed_assms = map (apsnd (try_prove_prem ctxt)) indexed_prems + val proved_assms = map (apsnd the) (filter (is_some o snd) indexed_assms) + val abs_eq = fold_rev (fn (i, assms) => fn thm => assms RSN (i, thm)) proved_assms abs_eq_with_assms in - if can_generate_code_cert quot_thm then + simplify_code_eq ctxt abs_eq + end + +fun define_code_using_abs_eq abs_eq_thm lthy = + if null (Logic.strip_imp_prems(prop_of abs_eq_thm)) then + (snd oo Local_Theory.note) ((Binding.empty, [Code.add_default_eqn_attrib]), [abs_eq_thm]) lthy + else + lthy + +fun define_code_using_rep_eq maybe_rep_eq_thm lthy = + case maybe_rep_eq_thm of + SOME rep_eq_thm => let - val code_cert = generate_code_cert lthy def_thm rsp_thm (rty, qty) val add_abs_eqn_attribute = Thm.declaration_attribute (fn thm => Context.mapping (Code.add_abs_eqn thm) I) val add_abs_eqn_attrib = Attrib.internal (K add_abs_eqn_attribute); - val lthy' = - (snd oo Local_Theory.note) ((code_eqn_thm_name, []), [code_cert]) lthy in - if is_abstype lthy qty_body then - (snd oo Local_Theory.note) ((Binding.empty, [add_abs_eqn_attrib]), [code_cert]) lthy' - else - lthy' + (snd oo Local_Theory.note) ((Binding.empty, [add_abs_eqn_attrib]), [rep_eq_thm]) lthy end + | NONE => lthy + +fun has_constr ctxt quot_thm = + let + val thy = Proof_Context.theory_of ctxt + val abs_fun = Lifting_Term.quot_thm_abs quot_thm + in + if is_Const abs_fun then + Code.is_constr thy ((fst o dest_Const) abs_fun) else - lthy + false end -fun define_code_eq code_eqn_thm_name def_thm lthy = +fun has_abstr ctxt quot_thm = let - val unfolded_def = Conv.fconv_rule unfold_fun_maps def_thm - val code_eq = unabs_all_def lthy unfolded_def - val simp_code_eq = simplify_code_eq lthy code_eq + val thy = Proof_Context.theory_of ctxt + val abs_fun = Lifting_Term.quot_thm_abs quot_thm in - lthy - |> (snd oo Local_Theory.note) ((code_eqn_thm_name, [Code.add_default_eqn_attrib]), [simp_code_eq]) + if is_Const abs_fun then + Code.is_abstr thy ((fst o dest_Const) abs_fun) + else + false end -fun define_code code_eqn_thm_name def_thm rsp_thm (rty, qty) lthy = - if body_type rty = body_type qty then - define_code_eq code_eqn_thm_name def_thm lthy - else - define_code_cert code_eqn_thm_name def_thm rsp_thm (rty, qty) lthy +fun define_code abs_eq_thm maybe_rep_eq_thm (rty, qty) lthy = + let + val (rty_body, qty_body) = get_body_types (rty, qty) + in + if rty_body = qty_body then + if null (Logic.strip_imp_prems(prop_of abs_eq_thm)) then + (snd oo Local_Theory.note) ((Binding.empty, [Code.add_default_eqn_attrib]), [abs_eq_thm]) lthy + else + (snd oo Local_Theory.note) ((Binding.empty, [Code.add_default_eqn_attrib]), [the maybe_rep_eq_thm]) lthy + else + let + val body_quot_thm = Lifting_Term.prove_quot_thm lthy (rty_body, qty_body) + in + if has_constr lthy body_quot_thm then + define_code_using_abs_eq abs_eq_thm lthy + else if has_abstr lthy body_quot_thm then + define_code_using_rep_eq maybe_rep_eq_thm lthy + else + lthy + end + end (* Defines an operation on an abstract type in terms of a corresponding operation @@ -186,15 +296,15 @@ var - a binding and a mixfix of the new constant being defined qty - an abstract type of the new constant rhs - a term representing the new constant on the raw level - rsp_thm - a respectfulness theorem in the internal form (like (R ===> R ===> R) f f), + rsp_thm - a respectfulness theorem in the internal tagged form (like '(R ===> R ===> R) f f'), i.e. "(Lifting_Term.equiv_relation (fastype_of rhs, qty)) $ rhs $ rhs" *) fun add_lift_def var qty rhs rsp_thm lthy = let val rty = fastype_of rhs - val quotient_thm = Lifting_Term.prove_quot_thm lthy (rty, qty) - val absrep_trm = Lifting_Term.quot_thm_abs quotient_thm + val quot_thm = Lifting_Term.prove_quot_thm lthy (rty, qty) + val absrep_trm = Lifting_Term.quot_thm_abs quot_thm val rty_forced = (domain_type o fastype_of) absrep_trm val forced_rhs = force_rty_type lthy rty_forced rhs val lhs = Free (Binding.print (#1 var), qty) @@ -205,21 +315,29 @@ val ((_, (_ , def_thm)), lthy') = Local_Theory.define (var, ((Thm.def_binding (#1 var), []), newrhs)) lthy - val transfer_thm = ([quotient_thm, rsp_thm, def_thm] MRSL @{thm Quotient_to_transfer}) + val transfer_thm = ([quot_thm, rsp_thm, def_thm] MRSL @{thm Quotient_to_transfer}) |> Raw_Simplifier.rewrite_rule (Transfer.get_relator_eq lthy') + + val abs_eq_thm = generate_abs_eq lthy' def_thm rsp_thm quot_thm + val maybe_rep_eq_thm = generate_rep_eq lthy' def_thm rsp_thm (rty_forced, qty) fun qualify defname suffix = Binding.qualified true suffix defname val lhs_name = (#1 var) val rsp_thm_name = qualify lhs_name "rsp" - val code_eqn_thm_name = qualify lhs_name "rep_eq" + val abs_eq_thm_name = qualify lhs_name "abs_eq" + val rep_eq_thm_name = qualify lhs_name "rep_eq" val transfer_thm_name = qualify lhs_name "transfer" val transfer_attr = Attrib.internal (K Transfer.transfer_add) in lthy' |> (snd oo Local_Theory.note) ((rsp_thm_name, []), [rsp_thm]) |> (snd oo Local_Theory.note) ((transfer_thm_name, [transfer_attr]), [transfer_thm]) - |> define_code code_eqn_thm_name def_thm rsp_thm (rty_forced, qty) + |> (snd oo Local_Theory.note) ((abs_eq_thm_name, []), [abs_eq_thm]) + |> (case maybe_rep_eq_thm of + SOME rep_eq_thm => (snd oo Local_Theory.note) ((rep_eq_thm_name, []), [rep_eq_thm]) + | NONE => I) + |> define_code abs_eq_thm maybe_rep_eq_thm (rty_forced, qty) end fun mk_readable_rsp_thm_eq tm lthy = @@ -253,7 +371,7 @@ (binop_conv2 left_conv simp_arrows_conv then_conv unfold_conv) ctm | _ => invariant_commute_conv ctm end - + val unfold_ret_val_invs = Conv.bottom_conv (K (Conv.try_conv (Conv.rewr_conv @{thm invariant_same_args}))) lthy val simp_conv = Trueprop_conv (Conv.fun2_conv simp_arrows_conv) diff -r 756f30eac792 -r 70375fa2679d src/HOL/Tools/Lifting/lifting_setup.ML --- a/src/HOL/Tools/Lifting/lifting_setup.ML Wed May 16 19:15:45 2012 +0200 +++ b/src/HOL/Tools/Lifting/lifting_setup.ML Wed May 16 19:17:20 2012 +0200 @@ -36,8 +36,26 @@ (def_thm, lthy'') end -fun define_abs_type gen_abs_code quot_thm lthy = - if gen_abs_code andalso Lifting_Def.can_generate_code_cert quot_thm then +fun define_code_constr gen_code quot_thm lthy = + let + val abs = Lifting_Term.quot_thm_abs quot_thm + val abs_background = Morphism.term (Local_Theory.target_morphism lthy) abs + in + if gen_code andalso is_Const abs_background then + let + val (const_name, typ) = dest_Const abs_background + val fake_term = Logic.mk_type typ + val (fixed_fake_term, lthy') = yield_singleton(Variable.importT_terms) fake_term lthy + val fixed_type = Logic.dest_type fixed_fake_term + in + Local_Theory.background_theory(Code.add_datatype [(const_name, fixed_type)]) lthy' + end + else + lthy + end + +fun define_abs_type gen_code quot_thm lthy = + if gen_code andalso Lifting_Def.can_generate_code_cert quot_thm then let val abs_type_thm = quot_thm RS @{thm Quotient_abs_rep} val add_abstype_attribute = @@ -76,31 +94,37 @@ @ (map Pretty.string_of errs))) end -fun setup_lifting_infr gen_abs_code quot_thm lthy = +fun setup_lifting_infr gen_code quot_thm maybe_reflp_thm lthy = let val _ = quot_thm_sanity_check lthy quot_thm val (_, qtyp) = Lifting_Term.quot_thm_rty_qty quot_thm val qty_full_name = (fst o dest_Type) qtyp val quotients = { quot_thm = quot_thm } fun quot_info phi = Lifting_Info.transform_quotients phi quotients + val lthy' = case maybe_reflp_thm of + SOME reflp_thm => lthy + |> (snd oo Local_Theory.note) ((Binding.empty, [Lifting_Info.add_reflp_preserve_rule_attrib]), + [reflp_thm]) + |> define_code_constr gen_code quot_thm + | NONE => lthy + |> define_abs_type gen_code quot_thm in - lthy + lthy' |> Local_Theory.declaration {syntax = false, pervasive = true} (fn phi => Lifting_Info.update_quotients qty_full_name (quot_info phi)) - |> define_abs_type gen_abs_code quot_thm end (* Sets up the Lifting package by a quotient theorem. - gen_abs_code - flag if an abstract type given by quot_thm should be registred + gen_code - flag if an abstract type given by quot_thm should be registred as an abstract type in the code generator quot_thm - a quotient theorem (Quotient R Abs Rep T) maybe_reflp_thm - a theorem saying that a relation from quot_thm is reflexive (in the form "reflp R") *) -fun setup_by_quotient gen_abs_code quot_thm maybe_reflp_thm lthy = +fun setup_by_quotient gen_code quot_thm maybe_reflp_thm lthy = let val transfer_attr = Attrib.internal (K Transfer.transfer_add) val (_, qty) = Lifting_Term.quot_thm_rty_qty quot_thm @@ -117,8 +141,6 @@ [[quot_thm, reflp_thm] MRSL @{thm Quotient_total_abs_induct}]) |> (snd oo Local_Theory.note) ((qualify "abs_eq_iff", []), [[quot_thm, reflp_thm] MRSL @{thm Quotient_total_abs_eq_iff}]) - |> (snd oo Local_Theory.note) ((Binding.empty, [Lifting_Info.add_reflp_preserve_rule_attrib]), - [reflp_thm]) | NONE => lthy |> (snd oo Local_Theory.note) ((qualify "All_transfer", [transfer_attr]), [quot_thm RS @{thm Quotient_All_transfer}]) @@ -136,18 +158,18 @@ [quot_thm RS @{thm Quotient_right_total}]) |> (snd oo Local_Theory.note) ((qualify "rel_eq_transfer", [transfer_attr]), [quot_thm RS @{thm Quotient_rel_eq_transfer}]) - |> setup_lifting_infr gen_abs_code quot_thm + |> setup_lifting_infr gen_code quot_thm maybe_reflp_thm end (* Sets up the Lifting package by a typedef theorem. - gen_abs_code - flag if an abstract type given by typedef_thm should be registred + gen_code - flag if an abstract type given by typedef_thm should be registred as an abstract type in the code generator typedef_thm - a typedef theorem (type_definition Rep Abs S) *) -fun setup_by_typedef_thm gen_abs_code typedef_thm lthy = +fun setup_by_typedef_thm gen_code typedef_thm lthy = let val transfer_attr = Attrib.internal (K Transfer.transfer_add) val (_ $ rep_fun $ _ $ typedef_set) = (HOLogic.dest_Trueprop o prop_of) typedef_thm @@ -166,7 +188,7 @@ fun qualify suffix = Binding.qualified true suffix qty_name val simplify = Raw_Simplifier.rewrite_rule [mk_meta_eq @{thm mem_Collect_eq}] - val lthy'' = case typedef_set of + val (maybe_reflp_thm, lthy'') = case typedef_set of Const ("Orderings.top_class.top", _) => let val equivp_thm = typedef_thm RS @{thm UNIV_typedef_to_equivp} @@ -177,8 +199,7 @@ [[quot_thm, reflp_thm] MRSL @{thm Quotient_bi_total}]) |> (snd oo Local_Theory.note) ((qualify "id_abs_transfer", [transfer_attr]), [[quot_thm, reflp_thm] MRSL @{thm Quotient_id_abs_transfer}]) - |> (snd oo Local_Theory.note) ((Binding.empty, [Lifting_Info.add_reflp_preserve_rule_attrib]), - [reflp_thm]) + |> pair (SOME reflp_thm) end | _ => lthy' |> (snd oo Local_Theory.note) ((qualify "All_transfer", [transfer_attr]), @@ -187,6 +208,7 @@ [[typedef_thm, T_def] MRSL @{thm typedef_Ex_transfer}]) |> (snd oo Local_Theory.note) ((qualify "forall_transfer", [transfer_attr]), [simplify ([typedef_thm, T_def] MRSL @{thm typedef_forall_transfer})]) + |> pair NONE in lthy'' |> (snd oo Local_Theory.note) ((qualify "bi_unique", [transfer_attr]), @@ -197,10 +219,10 @@ [[quot_thm] MRSL @{thm Quotient_right_unique}]) |> (snd oo Local_Theory.note) ((qualify "right_total", [transfer_attr]), [[quot_thm] MRSL @{thm Quotient_right_total}]) - |> setup_lifting_infr gen_abs_code quot_thm + |> setup_lifting_infr gen_code quot_thm maybe_reflp_thm end -fun setup_lifting_cmd gen_abs_code xthm opt_reflp_xthm lthy = +fun setup_lifting_cmd gen_code xthm opt_reflp_xthm lthy = let val input_thm = singleton (Attrib.eval_thms lthy) xthm val input_term = (HOLogic.dest_Trueprop o prop_of) input_thm @@ -223,14 +245,14 @@ val reflp_thm = singleton (Attrib.eval_thms lthy) reflp_xthm val _ = sanity_check_reflp_thm reflp_thm in - setup_by_quotient gen_abs_code input_thm (SOME reflp_thm) lthy + setup_by_quotient gen_code input_thm (SOME reflp_thm) lthy end - | NONE => setup_by_quotient gen_abs_code input_thm NONE lthy + | NONE => setup_by_quotient gen_code input_thm NONE lthy fun setup_typedef () = case opt_reflp_xthm of SOME _ => error "The reflexivity theorem cannot be specified if the type_definition theorem is used." - | NONE => setup_by_typedef_thm gen_abs_code input_thm lthy + | NONE => setup_by_typedef_thm gen_code input_thm lthy in case input_term of (Const (@{const_name Quotient}, _) $ _ $ _ $ _ $ _) => setup_quotient () @@ -238,12 +260,12 @@ | _ => error "Unsupported type of a theorem. Only Quotient or type_definition are supported." end -val opt_gen_abs_code = - Scan.optional (@{keyword "("} |-- Parse.!!! ((Parse.reserved "no_abs_code" >> K false) --| @{keyword ")"})) true +val opt_gen_code = + Scan.optional (@{keyword "("} |-- Parse.!!! ((Parse.reserved "no_code" >> K false) --| @{keyword ")"})) true val _ = Outer_Syntax.local_theory @{command_spec "setup_lifting"} "Setup lifting infrastructure" - (opt_gen_abs_code -- Parse_Spec.xthm -- Scan.option Parse_Spec.xthm >> - (fn ((gen_abs_code, xthm), opt_reflp_xthm) => setup_lifting_cmd gen_abs_code xthm opt_reflp_xthm)) + (opt_gen_code -- Parse_Spec.xthm -- Scan.option Parse_Spec.xthm >> + (fn ((gen_code, xthm), opt_reflp_xthm) => setup_lifting_cmd gen_code xthm opt_reflp_xthm)) end; diff -r 756f30eac792 -r 70375fa2679d src/HOL/Tools/Quotient/quotient_type.ML --- a/src/HOL/Tools/Quotient/quotient_type.ML Wed May 16 19:15:45 2012 +0200 +++ b/src/HOL/Tools/Quotient/quotient_type.ML Wed May 16 19:17:20 2012 +0200 @@ -9,12 +9,12 @@ val can_generate_code_cert: thm -> bool val add_quotient_type: ((string list * binding * mixfix) * (typ * term * bool) * - ((binding * binding) option)) * thm -> local_theory -> Quotient_Info.quotients * local_theory + ((binding * binding) option * bool)) * thm -> local_theory -> Quotient_Info.quotients * local_theory val quotient_type: ((string list * binding * mixfix) * (typ * term * bool) * - ((binding * binding) option)) list -> Proof.context -> Proof.state + ((binding * binding) option * bool)) list -> Proof.context -> Proof.state - val quotient_type_cmd: (((((string list * binding) * mixfix) * string) * (bool * string)) * + val quotient_type_cmd: ((((((bool * string list) * binding) * mixfix) * string) * (bool * string)) * (binding * binding) option) list -> Proof.context -> Proof.state end; @@ -132,7 +132,7 @@ (def_thm, lthy'') end; -fun setup_lifting_package quot3_thm equiv_thm lthy = +fun setup_lifting_package gen_code quot3_thm equiv_thm lthy = let val (_ $ _ $ abs_fun $ _) = (HOLogic.dest_Trueprop o prop_of) quot3_thm val (T_def, lthy') = define_cr_rel equiv_thm abs_fun lthy @@ -150,11 +150,11 @@ ) in lthy' - |> Lifting_Setup.setup_by_quotient false quot_thm reflp_thm + |> Lifting_Setup.setup_by_quotient gen_code quot_thm reflp_thm |> (snd oo Local_Theory.note) ((quotient_thm_name, []), [quot_thm]) end -fun init_quotient_infr quot_thm equiv_thm lthy = +fun init_quotient_infr gen_code quot_thm equiv_thm lthy = let val (_ $ rel $ abs $ rep) = (HOLogic.dest_Trueprop o prop_of) quot_thm val (qtyp, rtyp) = (dest_funT o fastype_of) rep @@ -170,11 +170,11 @@ (fn phi => Quotient_Info.update_quotients qty_full_name (quot_info phi) #> Quotient_Info.update_abs_rep qty_full_name (abs_rep_info phi)) |> define_abs_type quot_thm - |> setup_lifting_package quot_thm equiv_thm + |> setup_lifting_package gen_code quot_thm equiv_thm end (* main function for constructing a quotient type *) -fun add_quotient_type (((vs, qty_name, mx), (rty, rel, partial), opt_morphs), equiv_thm) lthy = +fun add_quotient_type (((vs, qty_name, mx), (rty, rel, partial), (opt_morphs, gen_code)), equiv_thm) lthy = let val part_equiv = if partial @@ -226,7 +226,7 @@ quot_thm = quotient_thm} val lthy4 = lthy3 - |> init_quotient_infr quotient_thm equiv_thm + |> init_quotient_infr gen_code quotient_thm equiv_thm |> (snd oo Local_Theory.note) ((equiv_thm_name, if partial then [] else [Attrib.internal (K Quotient_Info.equiv_rules_add)]), @@ -307,6 +307,7 @@ - the partial flag (a boolean) - the relation according to which the type is quotient - optional names of morphisms (rep/abs) + - flag if code should be generated by Lifting package it opens a proof-state in which one has to show that the relations are equivalence relations @@ -336,7 +337,7 @@ fun quotient_type_cmd specs lthy = let - fun parse_spec (((((vs, qty_name), mx), rty_str), (partial, rel_str)), opt_morphs) lthy = + fun parse_spec ((((((gen_code, vs), qty_name), mx), rty_str), (partial, rel_str)), opt_morphs) lthy = let val rty = Syntax.read_typ lthy rty_str val tmp_lthy1 = Variable.declare_typ rty lthy @@ -346,7 +347,7 @@ |> Syntax.check_term tmp_lthy1 val tmp_lthy2 = Variable.declare_term rel tmp_lthy1 in - (((vs, qty_name, mx), (rty, rel, partial), opt_morphs), tmp_lthy2) + (((vs, qty_name, mx), (rty, rel, partial), (opt_morphs, gen_code)), tmp_lthy2) end val (spec', _) = fold_map parse_spec specs lthy @@ -354,11 +355,14 @@ quotient_type spec' lthy end +val opt_gen_code = + Scan.optional (@{keyword "("} |-- (Parse.reserved "no_code" >> K false) --| Parse.!!! @{keyword ")"}) true + val partial = Scan.optional (Parse.reserved "partial" -- @{keyword ":"} >> K true) false val quotspec_parser = Parse.and_list1 - ((Parse.type_args -- Parse.binding) -- + ((opt_gen_code -- Parse.type_args -- Parse.binding) -- (* FIXME Parse.type_args_constrained and standard treatment of sort constraints *) Parse.opt_mixfix -- (@{keyword "="} |-- Parse.typ) -- (@{keyword "/"} |-- (partial -- Parse.term)) -- diff -r 756f30eac792 -r 70375fa2679d src/HOL/Transfer.thy --- a/src/HOL/Transfer.thy Wed May 16 19:15:45 2012 +0200 +++ b/src/HOL/Transfer.thy Wed May 16 19:17:20 2012 +0200 @@ -26,6 +26,11 @@ shows "B (f x) (g y)" using assms by (simp add: fun_rel_def) +lemma fun_relD2: + assumes "(A ===> B) f g" and "A x x" + shows "B (f x) (g x)" + using assms unfolding fun_rel_def by auto + lemma fun_relE: assumes "(A ===> B) f g" and "A x y" obtains "B (f x) (g y)"