# HG changeset patch # User wenzelm # Date 1559654096 -7200 # Node ID 59258a3192bf12da2d4b3cc8b39ccd29055e35c0 # Parent 34bc296374ee2d81c7f369fe7769d5339b232d0e misc tuning and clarification, notably wrt. flow of context; diff -r 34bc296374ee -r 59258a3192bf src/HOL/Tools/Lifting/lifting_bnf.ML --- a/src/HOL/Tools/Lifting/lifting_bnf.ML Tue Jun 04 15:14:19 2019 +0200 +++ b/src/HOL/Tools/Lifting/lifting_bnf.ML Tue Jun 04 15:14:56 2019 +0200 @@ -48,14 +48,13 @@ fun prove_Quotient_map bnf ctxt = let val live = live_of_bnf bnf - val old_ctxt = ctxt - val (((As, Bs), Ds), ctxt) = ctxt + val (((As, Bs), Ds), ctxt') = ctxt |> mk_TFrees live ||>> mk_TFrees live ||>> mk_TFrees (dead_of_bnf bnf) val argTss = map2 (fn a => fn b => [mk_pred2T a a, a --> b, b --> a,mk_pred2T a b]) As Bs - val ((argss, argss'), ctxt) = - @{fold_map 2} mk_Frees ["R", "Abs", "Rep", "T"] (transpose argTss) ctxt + val ((argss, argss'), ctxt'') = ctxt' + |> @{fold_map 2} mk_Frees ["R", "Abs", "Rep", "T"] (transpose argTss) |>> `transpose val assms = map (mk_Quotient #> HOLogic.mk_Trueprop) argss @@ -65,11 +64,12 @@ val T_rel = list_comb (mk_rel_of_bnf Ds As Bs bnf, nth argss' 3) val concl = mk_Quotient [R_rel, Abs_map, Rep_map, T_rel] |> HOLogic.mk_Trueprop val goal = Logic.list_implies (assms, concl) - val thm = Goal.prove_sorry ctxt [] [] goal - (fn {context = ctxt, prems = _} => Quotient_tac bnf ctxt 1) - |> Thm.close_derivation in - Drule.zero_var_indexes (singleton (Variable.export ctxt old_ctxt) thm) + Goal.prove_sorry ctxt'' [] [] goal + (fn {context = goal_ctxt, ...} => Quotient_tac bnf goal_ctxt 1) + |> Thm.close_derivation + |> singleton (Variable.export ctxt'' ctxt) + |> Drule.zero_var_indexes end diff -r 34bc296374ee -r 59258a3192bf src/HOL/Tools/Lifting/lifting_def.ML --- a/src/HOL/Tools/Lifting/lifting_def.ML Tue Jun 04 15:14:19 2019 +0200 +++ b/src/HOL/Tools/Lifting/lifting_def.ML Tue Jun 04 15:14:56 2019 +0200 @@ -168,7 +168,7 @@ in case mono_eq_prover ctxt prop of SOME thm => SOME (thm RS rule) - | NONE => NONE + | NONE => NONE end (* @@ -181,7 +181,7 @@ using Lifting_Term.merge_transfer_relations *) -fun generate_parametric_transfer_rule ctxt transfer_rule parametric_transfer_rule = +fun generate_parametric_transfer_rule ctxt0 transfer_rule parametric_transfer_rule = let fun preprocess ctxt thm = let @@ -235,21 +235,21 @@ end val thm = - inst_relcomppI ctxt parametric_transfer_rule transfer_rule + inst_relcomppI ctxt0 parametric_transfer_rule transfer_rule OF [parametric_transfer_rule, transfer_rule] - val preprocessed_thm = preprocess ctxt thm - val orig_ctxt = ctxt - val (fixed_thm, ctxt) = yield_singleton (apfst snd oo Variable.import true) preprocessed_thm ctxt + val preprocessed_thm = preprocess ctxt0 thm + val (fixed_thm, ctxt1) = ctxt0 + |> yield_singleton (apfst snd oo Variable.import true) preprocessed_thm val assms = cprems_of fixed_thm val add_transfer_rule = Thm.attribute_declaration Transfer.transfer_add - val (prems, ctxt) = fold_map Thm.assume_hyps assms ctxt - val ctxt = Context.proof_map (fold add_transfer_rule prems) ctxt + val (prems, ctxt2) = ctxt1 |> fold_map Thm.assume_hyps assms + val ctxt3 = ctxt2 |> Context.proof_map (fold add_transfer_rule prems) val zipped_thm = fixed_thm |> undisch_all - |> zip_transfer_rules ctxt + |> zip_transfer_rules ctxt3 |> implies_intr_list assms - |> singleton (Variable.export ctxt orig_ctxt) + |> singleton (Variable.export ctxt3 ctxt0) in zipped_thm end @@ -539,19 +539,17 @@ in if no_no_code lthy (rty, qty) then let - val lthy = (snd oo Local_Theory.note) - ((Binding.empty, [register_code_eq_attrib]), [encoded_code_eq]) lthy - val opt_code_eq = Data.get (Context.Theory (Proof_Context.theory_of lthy)) + val lthy' = lthy + |> (#2 oo Local_Theory.note) ((Binding.empty, [register_code_eq_attrib]), [encoded_code_eq]) + val opt_code_eq = Data.get (Context.Theory (Proof_Context.theory_of lthy')) val code_eq = if is_some opt_code_eq then the opt_code_eq else UNKNOWN_EQ (* UNKNOWN_EQ means that we are in a locale and we do not know which code equation is going to be used. This is going to be resolved at the point when an interpretation of the locale is executed. *) - val lthy = Local_Theory.declaration {syntax = false, pervasive = true} - (K (Data.put NONE)) lthy - in - (code_eq, lthy) - end + val lthy'' = lthy' + |> Local_Theory.declaration {syntax = false, pervasive = true} (K (Data.put NONE)) + in (code_eq, lthy'') end else (NONE_EQ, lthy) end @@ -569,27 +567,27 @@ par_thms - a parametricity theorem for rhs *) -fun add_lift_def (config: config) (binding, mx) qty rhs rsp_thm par_thms lthy = +fun add_lift_def (config: config) (binding, mx) qty rhs rsp_thm par_thms lthy0 = let val rty = fastype_of rhs - val quot_thm = Lifting_Term.prove_quot_thm lthy (rty, qty) + val quot_thm = Lifting_Term.prove_quot_thm lthy0 (rty, qty) val absrep_trm = 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 forced_rhs = force_rty_type lthy0 rty_forced rhs val lhs = Free (Binding.name_of binding, qty) val prop = Logic.mk_equals (lhs, absrep_trm $ forced_rhs) - val (_, prop') = Local_Defs.cert_def lthy (K []) prop + val (_, prop') = Local_Defs.cert_def lthy0 (K []) prop val (_, newrhs) = Local_Defs.abs_def prop' val var = ((#notes config = false ? Binding.concealed) binding, mx) val def_name = Thm.make_def_binding (#notes config) (#1 var) - val ((lift_const, (_ , def_thm)), lthy) = - Local_Theory.define (var, ((def_name, []), newrhs)) lthy + val ((lift_const, (_ , def_thm)), lthy1) = lthy0 + |> Local_Theory.define (var, ((def_name, []), newrhs)) - val transfer_rules = generate_transfer_rules lthy quot_thm rsp_thm def_thm par_thms + val transfer_rules = generate_transfer_rules lthy1 quot_thm rsp_thm def_thm par_thms - val abs_eq_thm = generate_abs_eq lthy def_thm rsp_thm quot_thm - val opt_rep_eq_thm = generate_rep_eq lthy def_thm rsp_thm (rty_forced, qty) + val abs_eq_thm = generate_abs_eq lthy1 def_thm rsp_thm quot_thm + val opt_rep_eq_thm = generate_rep_eq lthy1 def_thm rsp_thm (rty_forced, qty) fun notes names = let @@ -608,15 +606,16 @@ else map_filter (fn (_, attrs, thms) => if null attrs then NONE else SOME (Binding.empty_atts, [(thms, attrs)])) notes end - val (code_eq, lthy) = register_code_eq abs_eq_thm opt_rep_eq_thm (rty_forced, qty) lthy + val (code_eq, lthy2) = lthy1 + |> register_code_eq abs_eq_thm opt_rep_eq_thm (rty_forced, qty) val lift_def = mk_lift_def rty_forced qty newrhs lift_const def_thm rsp_thm abs_eq_thm opt_rep_eq_thm code_eq transfer_rules in - lthy - |> Local_Theory.open_target |> snd - |> Local_Theory.notes (notes (#notes config)) |> snd - |> `(fn lthy => morph_lift_def (Local_Theory.target_morphism lthy) lift_def) - ||> Local_Theory.close_target + lthy2 + |> Local_Theory.open_target |> snd + |> Local_Theory.notes (notes (#notes config)) |> snd + |> `(fn lthy => morph_lift_def (Local_Theory.target_morphism lthy) lift_def) + ||> Local_Theory.close_target end (* This is not very cheap way of getting the rules but we have only few active @@ -632,24 +631,24 @@ Symtab.fold (fn (_, data) => fn l => collect data l) table [] end -fun prepare_lift_def add_lift_def var qty rhs par_thms lthy = +fun prepare_lift_def add_lift_def var qty rhs par_thms ctxt = let - val rsp_rel = Lifting_Term.equiv_relation lthy (fastype_of rhs, qty) + val rsp_rel = Lifting_Term.equiv_relation ctxt (fastype_of rhs, qty) val rty_forced = (domain_type o fastype_of) rsp_rel; - val forced_rhs = force_rty_type lthy rty_forced rhs; + val forced_rhs = force_rty_type ctxt rty_forced rhs; val cr_to_pcr_conv = HOLogic.Trueprop_conv (Conv.fun2_conv - (Raw_Simplifier.rewrite lthy false (get_cr_pcr_eqs lthy))) + (Raw_Simplifier.rewrite ctxt false (get_cr_pcr_eqs ctxt))) val (prsp_tm, rsp_prsp_eq) = HOLogic.mk_Trueprop (rsp_rel $ forced_rhs $ forced_rhs) - |> Thm.cterm_of lthy + |> Thm.cterm_of ctxt |> cr_to_pcr_conv |> `Thm.concl_of |>> Logic.dest_equals |>> snd val to_rsp = rsp_prsp_eq RS Drule.equal_elim_rule2 - val opt_proven_rsp_thm = try_prove_reflexivity lthy prsp_tm + val opt_proven_rsp_thm = try_prove_reflexivity ctxt prsp_tm - fun after_qed internal_rsp_thm lthy = - add_lift_def var qty rhs (internal_rsp_thm RS to_rsp) par_thms lthy + fun after_qed internal_rsp_thm = + add_lift_def var qty rhs (internal_rsp_thm RS to_rsp) par_thms in case opt_proven_rsp_thm of SOME thm => (NONE, K (after_qed thm)) @@ -663,7 +662,8 @@ case goal of SOME goal => let - val rsp_thm = Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, ...} => tac ctxt) + val rsp_thm = + Goal.prove_sorry lthy [] [] goal (tac o #context) |> Thm.close_derivation in after_qed rsp_thm lthy @@ -671,7 +671,6 @@ | NONE => after_qed Drule.dummy_thm lthy end -fun lift_def config var qty rhs tac par_thms lthy = gen_lift_def (add_lift_def config) - var qty rhs tac par_thms lthy +val lift_def = gen_lift_def o add_lift_def end (* structure *) diff -r 34bc296374ee -r 59258a3192bf src/HOL/Tools/Lifting/lifting_def_code_dt.ML --- a/src/HOL/Tools/Lifting/lifting_def_code_dt.ML Tue Jun 04 15:14:19 2019 +0200 +++ b/src/HOL/Tools/Lifting/lifting_def_code_dt.ML Tue Jun 04 15:14:56 2019 +0200 @@ -226,8 +226,8 @@ fun bundle_name_of_bundle_binding binding phi context = Name_Space.full_name (Name_Space.naming_of context) (Morphism.binding phi binding); -fun prove_schematic_quot_thm actions ctxt = Lifting_Term.prove_schematic_quot_thm actions - (Lifting_Info.get_quotients ctxt) ctxt +fun prove_schematic_quot_thm actions ctxt = + Lifting_Term.prove_schematic_quot_thm actions (Lifting_Info.get_quotients ctxt) ctxt fun prove_code_dt (rty, qty) lthy = let @@ -245,24 +245,25 @@ fun R_conv rel_eq_onps = Transfer.top_sweep_rewr_conv @{thms eq_onp_top_eq_eq[symmetric, THEN eq_reflection]} then_conv Transfer.bottom_rewr_conv rel_eq_onps - val (ret_lift_def, lthy) = add_lift_def (#lift_config config) var qty rhs rsp_thm par_thms lthy + val (ret_lift_def, lthy1) = add_lift_def (#lift_config config) var qty rhs rsp_thm par_thms lthy in if (not (#code_dt config) orelse (code_eq_of_lift_def ret_lift_def <> NONE_EQ) andalso (code_eq_of_lift_def ret_lift_def <> UNKNOWN_EQ)) (* Let us try even in case of UNKNOWN_EQ. If this leads to problems, the user can always say that they do not want this workaround. *) - then (ret_lift_def, lthy) + then (ret_lift_def, lthy1) else let - val lift_def = inst_of_lift_def lthy qty ret_lift_def + val lift_def = inst_of_lift_def lthy1 qty ret_lift_def val rty = rty_of_lift_def lift_def val rty_ret = body_type rty val qty_ret = body_type qty - val (lthy, rel_eq_onps) = prove_code_dt (rty_ret, qty_ret) lthy - val code_dt = code_dt_of lthy (rty_ret, qty_ret) + val (lthy2, rel_eq_onps) = prove_code_dt (rty_ret, qty_ret) lthy1 + val code_dt = code_dt_of lthy2 (rty_ret, qty_ret) in - if is_none code_dt orelse is_none (rep_isom_data_of_code_dt (the code_dt)) then (ret_lift_def, lthy) + if is_none code_dt orelse is_none (rep_isom_data_of_code_dt (the code_dt)) + then (ret_lift_def, lthy2) else let val code_dt = the code_dt @@ -270,29 +271,28 @@ val rep_isom_data = code_dt |> rep_isom_data_of_code_dt |> the val pointer = pointer_of_rep_isom_data rep_isom_data val quot_active = - Lifting_Info.lookup_restore_data lthy pointer |> the |> #quotient |> #quot_thm - |> Lifting_Info.lookup_quot_thm_quotients lthy |> is_some + Lifting_Info.lookup_restore_data lthy2 pointer |> the |> #quotient |> #quot_thm + |> Lifting_Info.lookup_quot_thm_quotients lthy2 |> is_some val qty_code_dt_bundle_name = bundle_name_of_rep_isom_data rep_isom_data val rep_isom = mk_rep_isom_of_code_dt qty_ret code_dt |> the - val lthy = if quot_active then lthy else Bundle.includes [qty_code_dt_bundle_name] lthy + val lthy3 = if quot_active then lthy2 else Bundle.includes [qty_code_dt_bundle_name] lthy2 fun qty_isom_of_rep_isom rep = rep |> dest_Const |> snd |> domain_type val qty_isom = qty_isom_of_rep_isom rep_isom val f'_var = (Binding.suffix_name "_aux" (fst var), NoSyn); val f'_qty = strip_type qty |> fst |> rpair qty_isom |> op ---> - val f'_rsp_rel = Lifting_Term.equiv_relation lthy (rty, f'_qty); + val f'_rsp_rel = Lifting_Term.equiv_relation lthy3 (rty, f'_qty); val rsp = rsp_thm_of_lift_def lift_def val rel_eq_onps_conv = HOLogic.Trueprop_conv (Conv.fun2_conv (ret_rel_conv (R_conv rel_eq_onps))) val rsp_norm = Conv.fconv_rule rel_eq_onps_conv rsp val f'_rsp_goal = HOLogic.mk_Trueprop (f'_rsp_rel $ rhs $ rhs); - val f'_rsp = Goal.prove_sorry lthy [] [] f'_rsp_goal + val f'_rsp = Goal.prove_sorry lthy3 [] [] f'_rsp_goal (fn {context = ctxt, prems = _} => HEADGOAL (CONVERSION (rel_eq_onps_conv) THEN' rtac ctxt rsp_norm)) |> Thm.close_derivation - val (f'_lift_def, lthy) = add_lift_def ld_no_notes f'_var f'_qty rhs f'_rsp [] lthy - val f'_lift_def = inst_of_lift_def lthy f'_qty f'_lift_def + val (f'_lift_def, lthy4) = add_lift_def ld_no_notes f'_var f'_qty rhs f'_rsp [] lthy3 + val f'_lift_def = inst_of_lift_def lthy4 f'_qty f'_lift_def val f'_lift_const = mk_lift_const_of_lift_def f'_qty f'_lift_def - val args_lthy = lthy - val (args, lthy) = mk_Frees "x" (binder_types qty) lthy + val (args, args_ctxt) = mk_Frees "x" (binder_types qty) lthy4 val f_alt_def_goal_lhs = list_comb (lift_const_of_lift_def lift_def, args); val f_alt_def_goal_rhs = rep_isom $ list_comb (f'_lift_const, args); val f_alt_def_goal = HOLogic.mk_Trueprop (HOLogic.mk_eq (f_alt_def_goal_lhs, f_alt_def_goal_rhs)); @@ -300,26 +300,26 @@ EVERY' [Transfer.gen_frees_tac [] ctxt, DETERM o Transfer.transfer_tac true ctxt, SELECT_GOAL (Local_Defs.unfold0_tac ctxt [id_apply]), rtac ctxt refl] i; val rep_isom_transfer = transfer_of_rep_isom_data rep_isom_data - val (_, transfer_lthy) = + val (_, transfer_ctxt) = Proof_Context.note_thms "" - (Binding.empty_atts, [([rep_isom_transfer], [Transfer.transfer_add])]) lthy - val f_alt_def = Goal.prove_sorry transfer_lthy [] [] f_alt_def_goal - (fn {context = ctxt, prems = _} => HEADGOAL (f_alt_def_tac ctxt)) + (Binding.empty_atts, [([rep_isom_transfer], [Transfer.transfer_add])]) args_ctxt + val f_alt_def = + Goal.prove_sorry transfer_ctxt [] [] f_alt_def_goal + (fn {context = goal_ctxt, ...} => HEADGOAL (f_alt_def_tac goal_ctxt)) |> Thm.close_derivation - |> singleton (Variable.export lthy args_lthy) - val lthy = args_lthy - val lthy = lthy + |> singleton (Variable.export args_ctxt lthy4) (* FIXME proper transfer_ctxt!? *) + val lthy5 = lthy4 |> Local_Theory.note ((Binding.empty, @{attributes [code]}), [f_alt_def]) |> snd (* if processing a mutual datatype (there is a cycle!) the corresponding quotient will be needed later and will be forgotten later *) |> (if quot_active then I else Lifting_Setup.lifting_forget pointer) in - (ret_lift_def, lthy) + (ret_lift_def, lthy5) end end end -and mk_rep_isom qty_isom_bundle (rty, qty, qty_isom) lthy = +and mk_rep_isom qty_isom_bundle (rty, qty, qty_isom) lthy0 = let (* logical definition of qty qty_isom isomorphism *) val uTname = unique_Tname (rty, qty) @@ -328,24 +328,23 @@ fun lift_isom_tac ctxt = HEADGOAL (eq_onp_to_top_tac ctxt THEN' (rtac ctxt @{thm id_transfer})); - val (rep_isom_lift_def, lthy) = - lthy + val (rep_isom_lift_def, lthy1) = lthy0 |> Local_Theory.open_target |> snd |> lift_def ld_no_notes (Binding.qualify_name true uTname "Rep_isom", NoSyn) (qty_isom --> qty) (HOLogic.id_const rty) lift_isom_tac [] - |>> inst_of_lift_def lthy (qty_isom --> qty); - val (abs_isom, lthy) = - lthy + |>> inst_of_lift_def lthy0 (qty_isom --> qty); + val (abs_isom, lthy2) = lthy1 |> lift_def ld_no_notes (Binding.qualify_name true uTname "Abs_isom", NoSyn) (qty --> qty_isom) (HOLogic.id_const rty) lift_isom_tac [] |>> mk_lift_const_of_lift_def (qty --> qty_isom); val rep_isom = lift_const_of_lift_def rep_isom_lift_def - val pointer = Lifting_Setup.pointer_of_bundle_binding lthy qty_isom_bundle - fun code_dt phi context = code_dt_of lthy (rty, qty) |> the |> - update_rep_isom rep_isom (transfer_rules_of_lift_def rep_isom_lift_def |> hd) - (bundle_name_of_bundle_binding qty_isom_bundle phi context) pointer; - val lthy = lthy + val pointer = Lifting_Setup.pointer_of_bundle_binding lthy2 qty_isom_bundle + fun code_dt phi context = + code_dt_of lthy2 (rty, qty) |> the + |> update_rep_isom rep_isom (transfer_rules_of_lift_def rep_isom_lift_def |> hd) + (bundle_name_of_bundle_binding qty_isom_bundle phi context) pointer; + val lthy3 = lthy2 |> Local_Theory.declaration {syntax = false, pervasive = true} (fn phi => fn context => Data.map (Item_Net.update (morph_code_dt phi (code_dt phi context))) context) |> Local_Theory.close_target @@ -354,7 +353,7 @@ and selectors for qty_isom *) val (rty_name, typs) = dest_Type rty val (_, qty_typs) = dest_Type qty - val fp = BNF_FP_Def_Sugar.fp_sugar_of lthy rty_name + val fp = BNF_FP_Def_Sugar.fp_sugar_of lthy3 rty_name val fp = if is_some fp then the fp else error ("code_dt: " ^ quote rty_name ^ " is not a datatype.") val ctr_sugar = fp |> #fp_ctr_sugar |> #ctr_sugar @@ -365,7 +364,7 @@ val n = length ctrs; val ks = 1 upto n; - val (xss, _) = mk_Freess "x" ctr_Tss lthy; + val (xss, _) = mk_Freess "x" ctr_Tss lthy3; fun sel_retT (rty' as Type (s, rtys'), qty' as Type (s', qtys')) = if (rty', qty') = (rty, qty) then qty_isom else (if s = s' @@ -377,7 +376,7 @@ fun lazy_prove_code_dt (rty, qty) lthy = if is_none (code_dt_of lthy (rty, qty)) then prove_code_dt (rty, qty) lthy |> fst else lthy; - val lthy = fold2 (fold2 (lazy_prove_code_dt oo pair)) ctr_Tss sel_retTs lthy + val lthy4 = fold2 (fold2 (lazy_prove_code_dt oo pair)) ctr_Tss sel_retTs lthy3 val sel_argss = @{map 4} (fn k => fn xs => @{map 2} (fn x => fn qty_ret => (k, qty_ret, (xs, x)))) ks xss xss sel_retTs; @@ -398,7 +397,7 @@ (if k = k' then (fold_rev Term.lambda xs x, wits) else gen_undef_wit Ts wits)) ctr_Tss ks [] end; fun mk_sel_rhs arg = - let val (sel_rhs, wits) = mk_sel_case_args lthy ctr_Tss ks arg + let val (sel_rhs, wits) = mk_sel_case_args lthy4 ctr_Tss ks arg in (arg |> #2, wits, list_comb (mk_sel_casex arg, sel_rhs)) end; fun mk_dis_case_args args k = map (fn (k', arg) => (if k = k' then fold_rev Term.lambda arg \<^const>\True\ else fold_rev Term.lambda arg \<^const>\False\)) args; @@ -407,9 +406,9 @@ val dis_qty = qty_isom --> HOLogic.boolT; val dis_names = map (fn k => Binding.qualify_name true uTname ("dis" ^ string_of_int k)) ks; - val (diss, lthy) = @{fold_map 2} (fn b => fn rhs => fn lthy => + val (diss, lthy5) = @{fold_map 2} (fn b => fn rhs => fn lthy => lift_def ld_no_notes (b, NoSyn) dis_qty rhs (K all_tac) [] lthy - |>> mk_lift_const_of_lift_def dis_qty) dis_names dis_rhs lthy + |>> mk_lift_const_of_lift_def dis_qty) dis_names dis_rhs lthy4 val unfold_lift_sel_rsp = @{lemma "(\x. P1 x \ P2 (f x)) \ (rel_fun (eq_onp P1) (eq_onp P2)) f f" by (simp add: eq_onp_same_args rel_fun_eq_onp_rel)} @@ -422,16 +421,16 @@ EVERY' [hyp_subst_tac ctxt, (* does not kill wits because = was rewritten to eq_onp top *) Raw_Simplifier.rewrite_goal_tac ctxt (map safe_mk_meta_eq dt_rules), REPEAT_DETERM o etac ctxt conjE, assume_tac ctxt])) i - val pred_simps = Transfer.lookup_pred_data lthy (Tname rty) |> the |> Transfer.pred_simps + val pred_simps = Transfer.lookup_pred_data lthy5 (Tname rty) |> the |> Transfer.pred_simps val sel_tac = lift_sel_tac (#exhaust ctr_sugar) (#case_thms ctr_sugar @ pred_simps) val sel_names = map (fn (k, xs) => map (fn k' => Binding.qualify_name true uTname ("sel" ^ string_of_int k ^ string_of_int k')) (1 upto length xs)) (ks ~~ ctr_Tss); - val (selss, lthy) = @{fold_map 2} (@{fold_map 2} (fn b => fn (qty_ret, wits, rhs) => fn lthy => + val (selss, lthy6) = @{fold_map 2} (@{fold_map 2} (fn b => fn (qty_ret, wits, rhs) => fn lthy => lift_def_code_dt { code_dt = true, lift_config = ld_no_notes } (b, NoSyn) (qty_isom --> qty_ret) rhs (HEADGOAL o sel_tac wits) [] lthy - |>> mk_lift_const_of_lift_def (qty_isom --> qty_ret))) sel_names sel_rhs lthy + |>> mk_lift_const_of_lift_def (qty_isom --> qty_ret))) sel_names sel_rhs lthy5 (* now we can execute the qty qty_isom isomorphism *) fun mk_type_definition newT oldT RepC AbsC A = @@ -450,30 +449,31 @@ (map safe_mk_meta_eq @{thms id_apply simp_thms Ball_def}), rtac ctxt TrueI] i; - val (_, transfer_lthy) = + val (_, transfer_ctxt) = Proof_Context.note_thms "" (Binding.empty_atts, [(@{thms right_total_UNIV_transfer}, [Transfer.transfer_add]), - (@{thms Domain_eq_top}, [Transfer.transfer_domain_add])]) lthy; + (@{thms Domain_eq_top}, [Transfer.transfer_domain_add])]) lthy6; - val quot_thm_isom = Goal.prove_sorry transfer_lthy [] [] typedef_goal - (fn {context = ctxt, prems = _} => typ_isom_tac ctxt 1) + val quot_thm_isom = + Goal.prove_sorry transfer_ctxt [] [] typedef_goal + (fn {context = goal_ctxt, ...} => typ_isom_tac goal_ctxt 1) |> Thm.close_derivation - |> singleton (Variable.export transfer_lthy lthy) + |> singleton (Variable.export transfer_ctxt lthy6) |> (fn thm => @{thm UNIV_typedef_to_Quotient} OF [thm, @{thm reflexive}]) val qty_isom_name = Tname qty_isom; val quot_isom_rep = let - val (quotients : Lifting_Term.quotients) = Symtab.insert (Lifting_Info.quotient_eq) (qty_isom_name, - {quot_thm = quot_thm_isom, pcr_info = NONE}) Symtab.empty + val (quotients : Lifting_Term.quotients) = + Symtab.insert (Lifting_Info.quotient_eq) + (qty_isom_name, {quot_thm = quot_thm_isom, pcr_info = NONE}) Symtab.empty val id_actions = { constr = K I, lift = K I, comp_lift = K I } in fn ctxt => fn (rty, qty) => Lifting_Term.prove_schematic_quot_thm id_actions quotients ctxt (rty, qty) () |> fst |> Lifting_Term.force_qty_type ctxt qty |> quot_thm_rep end; - val x_lthy = lthy - val (x, lthy) = yield_singleton (mk_Frees "x") qty_isom lthy; + val (x, x_ctxt) = yield_singleton (mk_Frees "x") qty_isom lthy6; fun mk_ctr ctr ctr_Ts sels = let @@ -488,7 +488,7 @@ end; in @{fold 3} (fn sel => fn ctr_T => fn sel_ret_T => fn ctr => - ctr $ rep_isom lthy (sel $ x) (ctr_T, sel_ret_T)) sels ctr_Ts sel_ret_Ts ctr + ctr $ rep_isom x_ctxt (sel $ x) (ctr_T, sel_ret_T)) sels ctr_Ts sel_ret_Ts ctr end; (* stolen from Metis *) @@ -535,26 +535,25 @@ the datatype fp. Otherwise rep_isom_code_tac could fail (especially transfer in it) is such a way that it is not easy to infer the problem with sorts. *) - val _ = yield_singleton (mk_Frees "x") (#T fp) lthy |> fst |> force_typ lthy qty + val _ = yield_singleton (mk_Frees "x") (#T fp) x_ctxt |> fst |> force_typ x_ctxt qty - val rep_isom_code = Goal.prove_sorry lthy [] [] rep_isom_code_goal - (fn {context = ctxt, prems = _} => rep_isom_code_tac ctr_sugar ctxt 1) + val rep_isom_code = + Goal.prove_sorry x_ctxt [] [] rep_isom_code_goal + (fn {context = goal_ctxt, ...} => rep_isom_code_tac ctr_sugar goal_ctxt 1) |> Thm.close_derivation - |> singleton(Variable.export lthy x_lthy) - val lthy = x_lthy - val lthy = - lthy - |> snd o Local_Theory.note ((Binding.empty, @{attributes [code]}), [rep_isom_code]) - |> Lifting_Setup.lifting_forget pointer + |> singleton(Variable.export x_ctxt lthy6) in - ((selss, diss, rep_isom_code), lthy) + lthy6 + |> snd o Local_Theory.note ((Binding.empty, @{attributes [code]}), [rep_isom_code]) + |> Lifting_Setup.lifting_forget pointer + |> pair (selss, diss, rep_isom_code) end -and constr qty (quot_thm, (lthy, rel_eq_onps)) = +and constr qty (quot_thm, (lthy0, rel_eq_onps)) = let - val quot_thm = Lifting_Term.force_qty_type lthy qty quot_thm + val quot_thm = Lifting_Term.force_qty_type lthy0 qty quot_thm val (rty, qty) = quot_thm_rty_qty quot_thm val rty_name = Tname rty; - val pred_data = Transfer.lookup_pred_data lthy rty_name + val pred_data = Transfer.lookup_pred_data lthy0 rty_name val pred_data = if is_some pred_data then the pred_data else error ("code_dt: " ^ quote rty_name ^ " is not a datatype.") val rel_eq_onp = safe_mk_meta_eq (Transfer.rel_eq_onp pred_data); @@ -563,12 +562,11 @@ then_conv Conv.rewr_conv rel_eq_onp val quot_thm = Conv.fconv_rule(HOLogic.Trueprop_conv (Quotient_R_conv R_conv)) quot_thm; in - if is_none (code_dt_of lthy (rty, qty)) then + if is_none (code_dt_of lthy0 (rty, qty)) then let val non_empty_pred = quot_thm RS @{thm type_definition_Quotient_not_empty} val pred = quot_thm_rel quot_thm |> dest_comb |> snd; - val (pred, lthy) = - lthy + val (pred, lthy1) = lthy0 |> Local_Theory.open_target |> snd |> yield_singleton (Variable.import_terms true) pred; val TFrees = Term.add_tfreesT qty [] @@ -578,29 +576,29 @@ SELECT_GOAL (Local_Defs.unfold0_tac ctxt [mem_Collect_eq]) THEN' assume_tac ctxt) i val uTname = unique_Tname (rty, qty) val Tdef_set = HOLogic.mk_Collect ("x", rty, pred $ Free("x", rty)); - val ((_, tcode_dt), lthy) = conceal_naming_result (typedef (Binding.concealed uTname, TFrees, NoSyn) - Tdef_set NONE (fn lthy => HEADGOAL (non_empty_typedef_tac non_empty_pred lthy))) lthy; + val ((_, tcode_dt), lthy2) = lthy1 + |> conceal_naming_result + (typedef (Binding.concealed uTname, TFrees, NoSyn) + Tdef_set NONE (fn lthy => HEADGOAL (non_empty_typedef_tac non_empty_pred lthy))); val type_definition_thm = tcode_dt |> snd |> #type_definition; val qty_isom = tcode_dt |> fst |> #abs_type; - val (binding, lthy) = - lthy - |> conceal_naming_result (Lifting_Setup.setup_by_typedef_thm - { notes = false } type_definition_thm) + val (binding, lthy3) = lthy2 + |> conceal_naming_result + (Lifting_Setup.setup_by_typedef_thm {notes = false} type_definition_thm) ||> Local_Theory.close_target val (wit, wit_thm) = mk_witness quot_thm; val code_dt = mk_code_dt rty qty wit wit_thm NONE; - val lthy = lthy + val lthy4 = lthy3 |> update_code_dt code_dt |> mk_rep_isom binding (rty, qty, qty_isom) |> snd in - (quot_thm, (lthy, rel_eq_onps)) + (quot_thm, (lthy4, rel_eq_onps)) end else - (quot_thm, (lthy, rel_eq_onps)) + (quot_thm, (lthy0, rel_eq_onps)) end -and lift_def_code_dt config var qty rhs tac par_thms lthy = gen_lift_def (add_lift_def_code_dt config) - var qty rhs tac par_thms lthy +and lift_def_code_dt config = gen_lift_def (add_lift_def_code_dt config) (** from parsed parameters to the config record **) @@ -634,9 +632,9 @@ [@{thm pcr_Domainp_total}, @{thm pcr_Domainp_par_left_total}, @{thm pcr_Domainp_par}, @{thm pcr_Domainp}] in -fun mk_readable_rsp_thm_eq tm lthy = +fun mk_readable_rsp_thm_eq tm ctxt = let - val ctm = Thm.cterm_of lthy tm + val ctm = Thm.cterm_of ctxt tm fun assms_rewr_conv tactic rule ct = let @@ -685,18 +683,18 @@ @{thm rel_fun_def[THEN eq_reflection]}] fun binop_conv2 cv1 cv2 = Conv.combination_conv (Conv.arg_conv cv1) cv2 val eq_onp_assms_tac_rules = @{thm left_unique_OO} :: - eq_onp_assms_tac_fixed_rules @ (Transfer.get_transfer_raw lthy) + eq_onp_assms_tac_fixed_rules @ (Transfer.get_transfer_raw ctxt) val intro_top_rule = @{thm eq_onp_top_eq_eq[symmetric, THEN eq_reflection]} val kill_tops = Transfer.top_sweep_rewr_conv [@{thm eq_onp_top_eq_eq[THEN eq_reflection]}] val eq_onp_assms_tac = (CONVERSION kill_tops THEN' - TRY o REPEAT_ALL_NEW (resolve_tac lthy eq_onp_assms_tac_rules) - THEN_ALL_NEW (DETERM o Transfer.eq_tac lthy)) 1 + TRY o REPEAT_ALL_NEW (resolve_tac ctxt eq_onp_assms_tac_rules) + THEN_ALL_NEW (DETERM o Transfer.eq_tac ctxt)) 1 val relator_eq_onp_conv = Conv.bottom_conv (K (Conv.try_conv (assms_rewrs_conv eq_onp_assms_tac - (intro_top_rule :: Lifting_Info.get_relator_eq_onp_rules lthy)))) lthy + (intro_top_rule :: Lifting_Info.get_relator_eq_onp_rules ctxt)))) ctxt then_conv kill_tops val relator_eq_conv = Conv.bottom_conv - (K (Conv.try_conv (Conv.rewrs_conv (Transfer.get_relator_eq lthy)))) lthy + (K (Conv.try_conv (Conv.rewrs_conv (Transfer.get_relator_eq ctxt)))) ctxt in case (Thm.term_of ctm) of Const (\<^const_name>\rel_fun\, _) $ _ $ _ => @@ -705,18 +703,18 @@ end val unfold_ret_val_invs = Conv.bottom_conv - (K (Conv.try_conv (Conv.rewr_conv @{thm eq_onp_same_args[THEN eq_reflection]}))) lthy + (K (Conv.try_conv (Conv.rewr_conv @{thm eq_onp_same_args[THEN eq_reflection]}))) ctxt val unfold_inv_conv = - Conv.top_sweep_conv (K (Conv.rewr_conv @{thm eq_onp_def[THEN eq_reflection]})) lthy + Conv.top_sweep_conv (K (Conv.rewr_conv @{thm eq_onp_def[THEN eq_reflection]})) ctxt val simp_conv = HOLogic.Trueprop_conv (Conv.fun2_conv simp_arrows_conv) val univq_conv = Conv.rewr_conv @{thm HOL.all_simps(6)[symmetric, THEN eq_reflection]} - val univq_prenex_conv = Conv.top_conv (K (Conv.try_conv univq_conv)) lthy + val univq_prenex_conv = Conv.top_conv (K (Conv.try_conv univq_conv)) ctxt val beta_conv = Thm.beta_conversion true val eq_thm = (simp_conv then_conv univq_prenex_conv then_conv beta_conv then_conv unfold_ret_val_invs then_conv unfold_inv_conv) ctm in - Object_Logic.rulify lthy (eq_thm RS Drule.equal_elim_rule2) + Object_Logic.rulify ctxt (eq_thm RS Drule.equal_elim_rule2) end end @@ -772,40 +770,39 @@ error error_msg end -fun lift_def_cmd (params, raw_var, rhs_raw, par_xthms) lthy = +fun lift_def_cmd (params, raw_var, rhs_raw, par_xthms) lthy0 = let val config = evaluate_params params - val ((binding, SOME qty, mx), lthy) = Proof_Context.read_var raw_var lthy + val ((binding, SOME qty, mx), lthy1) = Proof_Context.read_var raw_var lthy0 val var = (binding, mx) - val rhs = Syntax.read_term lthy rhs_raw - val par_thms = Attrib.eval_thms lthy par_xthms - val (goal, after_qed) = prepare_lift_def (add_lift_def_code_dt config) var qty rhs par_thms lthy + val rhs = Syntax.read_term lthy1 rhs_raw + val par_thms = Attrib.eval_thms lthy1 par_xthms + val (goal, after_qed) = lthy1 + |> prepare_lift_def (add_lift_def_code_dt config) var qty rhs par_thms val (goal, after_qed) = case goal of NONE => (goal, K (after_qed Drule.dummy_thm)) | SOME prsp_tm => let - val readable_rsp_thm_eq = mk_readable_rsp_thm_eq prsp_tm lthy + val readable_rsp_thm_eq = mk_readable_rsp_thm_eq prsp_tm lthy1 val (readable_rsp_tm, _) = Logic.dest_implies (Thm.prop_of readable_rsp_thm_eq) - val readable_rsp_tm_tnames = rename_to_tnames lthy readable_rsp_tm + val readable_rsp_tm_tnames = rename_to_tnames lthy1 readable_rsp_tm fun after_qed' [[thm]] lthy = let - val internal_rsp_thm = Goal.prove lthy [] [] prsp_tm - (fn {context = ctxt, ...} => - rtac ctxt readable_rsp_thm_eq 1 THEN Proof_Context.fact_tac ctxt [thm] 1) - in - after_qed internal_rsp_thm lthy - end - in - (SOME readable_rsp_tm_tnames, after_qed') - end + val internal_rsp_thm = + Goal.prove lthy [] [] prsp_tm (fn {context = goal_ctxt, ...} => + rtac goal_ctxt readable_rsp_thm_eq 1 THEN + Proof_Context.fact_tac goal_ctxt [thm] 1) + in after_qed internal_rsp_thm lthy end + in (SOME readable_rsp_tm_tnames, after_qed') end fun after_qed_with_err_handling thmss ctxt = (after_qed thmss ctxt - handle Lifting_Term.QUOT_THM (rty, qty, msg) => quot_thm_err lthy (rty, qty) msg) + handle Lifting_Term.QUOT_THM (rty, qty, msg) => quot_thm_err lthy1 (rty, qty) msg) handle Lifting_Term.CHECK_RTY (rty_schematic, rty_forced) => - check_rty_err lthy (rty_schematic, rty_forced) (raw_var, rhs_raw); + check_rty_err lthy1 (rty_schematic, rty_forced) (raw_var, rhs_raw); in - Proof.theorem NONE (snd oo after_qed_with_err_handling) [map (rpair []) (the_list goal)] lthy + lthy1 + |> Proof.theorem NONE (snd oo after_qed_with_err_handling) [map (rpair []) (the_list goal)] end fun lift_def_cmd_with_err_handling (params, (raw_var, rhs_raw, par_xthms)) lthy = diff -r 34bc296374ee -r 59258a3192bf src/HOL/Tools/Lifting/lifting_info.ML --- a/src/HOL/Tools/Lifting/lifting_info.ML Tue Jun 04 15:14:19 2019 +0200 +++ b/src/HOL/Tools/Lifting/lifting_info.ML Tue Jun 04 15:14:56 2019 +0200 @@ -124,18 +124,18 @@ fun map_restore_data f = map_data I I I I f I fun map_no_code_types f = map_data I I I I I f -val get_quot_maps' = #quot_maps o Data.get -val get_quotients' = #quotients o Data.get -val get_reflexivity_rules' = #reflexivity_rules o Data.get -val get_relator_distr_data' = #relator_distr_data o Data.get -val get_restore_data' = #restore_data o Data.get -val get_no_code_types' = #no_code_types o Data.get +val get_quot_maps' = #quot_maps o Data.get +val get_quotients' = #quotients o Data.get +val get_reflexivity_rules' = #reflexivity_rules o Data.get +val get_relator_distr_data' = #relator_distr_data o Data.get +val get_restore_data' = #restore_data o Data.get +val get_no_code_types' = #no_code_types o Data.get -fun get_quot_maps ctxt = get_quot_maps' (Context.Proof ctxt) -fun get_quotients ctxt = get_quotients' (Context.Proof ctxt) -fun get_relator_distr_data ctxt = get_relator_distr_data' (Context.Proof ctxt) -fun get_restore_data ctxt = get_restore_data' (Context.Proof ctxt) -fun get_no_code_types ctxt = get_no_code_types' (Context.Proof ctxt) +val get_quot_maps = get_quot_maps' o Context.Proof +val get_quotients = get_quotients' o Context.Proof +val get_relator_distr_data = get_relator_distr_data' o Context.Proof +val get_restore_data = get_restore_data' o Context.Proof +val get_no_code_types = get_no_code_types' o Context.Proof (* info about Quotient map theorems *) @@ -228,7 +228,7 @@ in case lookup_quotients ctxt qty_full_name of SOME quotient => if compare_data quotient then SOME quotient else NONE - | NONE => NONE + | NONE => NONE end fun update_quotients type_name qinfo context = @@ -293,7 +293,7 @@ (* info about reflexivity rules *) -fun get_reflexivity_rules ctxt = Item_Net.content (get_reflexivity_rules' (Context.Proof ctxt)) +val get_reflexivity_rules = Item_Net.content o get_reflexivity_rules' o Context.Proof fun add_reflexivity_rule thm = Data.map (map_reflexivity_rules (Item_Net.update thm)) val add_reflexivity_rule_attribute = Thm.declaration_attribute add_reflexivity_rule diff -r 34bc296374ee -r 59258a3192bf src/HOL/Tools/Lifting/lifting_setup.ML --- a/src/HOL/Tools/Lifting/lifting_setup.ML Tue Jun 04 15:14:19 2019 +0200 +++ b/src/HOL/Tools/Lifting/lifting_setup.ML Tue Jun 04 15:14:56 2019 +0200 @@ -44,16 +44,16 @@ val def_term = Abs ("x", rty, Abs ("y", qty, rep_fun_graph)) val qty_name = (Binding.name o Long_Name.base_name o fst o dest_Type) qty val crel_name = Binding.prefix_name "cr_" qty_name - val (fixed_def_term, lthy) = yield_singleton (Variable.importT_terms) def_term lthy - val ((_, (_ , def_thm)), lthy) = + val (fixed_def_term, lthy1) = lthy |> yield_singleton (Variable.importT_terms) def_term + val ((_, (_ , def_thm)), lthy2) = if #notes config then Local_Theory.define - ((crel_name, NoSyn), ((Thm.def_binding crel_name, []), fixed_def_term)) lthy + ((crel_name, NoSyn), ((Thm.def_binding crel_name, []), fixed_def_term)) lthy1 else Local_Theory.define - ((Binding.concealed crel_name, NoSyn), (Binding.empty_atts, fixed_def_term)) lthy + ((Binding.concealed crel_name, NoSyn), (Binding.empty_atts, fixed_def_term)) lthy1 in - (def_thm, lthy) + (def_thm, lthy2) end fun print_define_pcrel_warning msg = @@ -66,18 +66,18 @@ warning warning_msg end -fun define_pcrel (config: config) crel lthy = +fun define_pcrel (config: config) crel lthy0 = let - val (fixed_crel, lthy) = yield_singleton Variable.importT_terms crel lthy + val (fixed_crel, lthy1) = yield_singleton Variable.importT_terms crel lthy0 val [rty', qty] = (binder_types o fastype_of) fixed_crel - val (param_rel, args) = Lifting_Term.generate_parametrized_relator lthy rty' + val (param_rel, args) = Lifting_Term.generate_parametrized_relator lthy1 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 tyenv_match = Sign.typ_match (Proof_Context.theory_of lthy1) (rty_raw, rty') Vartab.empty 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 (instT, lthy2) = lthy1 + |> Variable.declare_names fixed_crel + |> Variable.importT_inst (param_rel_subst :: args_subst) 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 @@ -98,18 +98,18 @@ let val ((_, rhs), prove) = Local_Defs.derived_def lthy (K []) {conditional = true} definition_term; - val ((_, (_, raw_th)), lthy) = + val ((_, (_, raw_th)), lthy') = Local_Theory.define ((Binding.concealed pcrel_name, NoSyn), (Binding.empty_atts, rhs)) lthy; - val th = prove lthy raw_th; + val th = prove lthy' raw_th; in - (th, lthy) + (th, lthy') end - val (def_thm, lthy) = if #notes config then note_def lthy else raw_def lthy + val (def_thm, lthy3) = if #notes config then note_def lthy2 else raw_def lthy2 in - (SOME def_thm, lthy) + (SOME def_thm, lthy3) end - handle Lifting_Term.PARAM_QUOT_THM (_, msg) => (print_define_pcrel_warning msg; (NONE, lthy)) + handle Lifting_Term.PARAM_QUOT_THM (_, msg) => (print_define_pcrel_warning msg; (NONE, lthy0)) local @@ -143,13 +143,12 @@ val inst = (#1 (dest_Var var), Thm.cterm_of ctxt' (HOLogic.eq_const (TFree fresh_var))) in (inst, ctxt') end - val orig_lthy = lthy - val (args_inst, lthy) = fold_map make_inst args lthy + val (args_inst, args_ctxt) = fold_map make_inst args lthy val pcr_cr_eq = pcr_rel_def - |> infer_instantiate lthy args_inst + |> infer_instantiate args_ctxt args_inst |> Conv.fconv_rule (Conv.arg_conv (Conv.arg1_conv - (Transfer.bottom_rewr_conv (Transfer.get_relator_eq lthy)))) + (Transfer.bottom_rewr_conv (Transfer.get_relator_eq args_ctxt)))) in case (Thm.term_of o Thm.rhs_of) pcr_cr_eq of Const (\<^const_name>\relcompp\, _) $ Const (\<^const_name>\HOL.eq\, _) $ _ => @@ -158,13 +157,14 @@ pcr_cr_eq |> Conv.fconv_rule (Conv.arg_conv (Conv.rewr_conv eq_OO_meta)) |> HOLogic.mk_obj_eq - |> singleton (Variable.export lthy orig_lthy) - val lthy = (#notes config ? (Local_Theory.note - ((Binding.qualify_name true qty_name "pcr_cr_eq", []), [thm]) #> snd)) lthy + |> singleton (Variable.export args_ctxt lthy) + val lthy' = args_ctxt (* FIXME lthy!? *) + |> #notes config ? + (Local_Theory.note ((Binding.qualify_name true qty_name "pcr_cr_eq", []), [thm]) #> #2) in - (thm, lthy) + (thm, lthy') end - | Const (\<^const_name>\relcompp\, _) $ t $ _ => print_generate_pcr_cr_eq_error lthy t + | Const (\<^const_name>\relcompp\, _) $ t $ _ => print_generate_pcr_cr_eq_error args_ctxt t | _ => error "generate_pcr_cr_eq: implementation error" end end @@ -234,38 +234,40 @@ fun lifting_bundle qty_full_name qinfo lthy = let + val thy = Proof_Context.theory_of lthy + val binding = Binding.qualify_name true (qty_full_name |> Long_Name.base_name |> Binding.name) "lifting" val morphed_binding = Morphism.binding (Local_Theory.target_morphism lthy) binding - val bundle_name = Name_Space.full_name (Name_Space.naming_of - (Context.Theory (Proof_Context.theory_of lthy))) morphed_binding + val bundle_name = + Name_Space.full_name (Name_Space.naming_of (Context.Theory thy)) morphed_binding fun phi_qinfo phi = Lifting_Info.transform_quotient phi qinfo - val thy = Proof_Context.theory_of lthy val dummy_thm = Thm.transfer thy Drule.dummy_thm val restore_lifting_att = ([dummy_thm], [map (Token.make_string o rpair Position.none) ["Lifting.lifting_restore_internal", bundle_name]]) in - lthy - |> Local_Theory.declaration {syntax = false, pervasive = true} - (fn phi => Lifting_Info.init_restore_data bundle_name (phi_qinfo phi)) - |> Bundle.bundle ((binding, [restore_lifting_att])) [] - |> pair binding + lthy + |> Local_Theory.declaration {syntax = false, pervasive = true} + (fn phi => Lifting_Info.init_restore_data bundle_name (phi_qinfo phi)) + |> Bundle.bundle ((binding, [restore_lifting_att])) [] + |> pair binding end fun setup_lifting_infr config quot_thm opt_reflp_thm lthy = let val _ = quot_thm_sanity_check lthy quot_thm val (_, qty) = quot_thm_rty_qty quot_thm - val (pcrel_def, lthy) = define_pcrel config (quot_thm_crel quot_thm) lthy + val (pcrel_def, lthy1) = define_pcrel config (quot_thm_crel quot_thm) lthy (**) - val pcrel_def = Option.map (Morphism.thm (Local_Theory.target_morphism lthy)) pcrel_def + val pcrel_def = Option.map (Morphism.thm (Local_Theory.target_morphism lthy1)) pcrel_def (**) - val (pcr_cr_eq, lthy) = case pcrel_def of - SOME pcrel_def => apfst SOME (define_pcr_cr_eq config lthy pcrel_def) - | NONE => (NONE, lthy) + val (pcr_cr_eq, lthy2) = + case pcrel_def of + SOME pcrel_def => apfst SOME (define_pcr_cr_eq config lthy1 pcrel_def) + | NONE => (NONE, lthy1) val pcr_info = case pcrel_def of SOME pcrel_def => SOME { pcrel_def = pcrel_def, pcr_cr_eq = the pcr_cr_eq } | NONE => NONE @@ -273,18 +275,19 @@ val qty_full_name = (fst o dest_Type) qty fun quot_info phi = Lifting_Info.transform_quotient phi quotients val reflexivity_rule_attr = Attrib.internal (K Lifting_Info.add_reflexivity_rule_attribute) - val lthy = case opt_reflp_thm of - SOME reflp_thm => lthy - |> (snd oo Local_Theory.note) ((Binding.empty, [reflexivity_rule_attr]), - [reflp_thm RS @{thm reflp_ge_eq}]) - |> define_code_constr quot_thm - | NONE => lthy - |> define_abs_type quot_thm + val lthy3 = + case opt_reflp_thm of + SOME reflp_thm => + lthy2 + |> (#2 oo Local_Theory.note) + ((Binding.empty, [reflexivity_rule_attr]), [reflp_thm RS @{thm reflp_ge_eq}]) + |> define_code_constr quot_thm + | NONE => lthy2 |> define_abs_type quot_thm in - lthy - |> Local_Theory.declaration {syntax = false, pervasive = true} + lthy3 + |> Local_Theory.declaration {syntax = false, pervasive = true} (fn phi => Lifting_Info.update_quotients qty_full_name (quot_info phi)) - |> lifting_bundle qty_full_name quotients + |> lifting_bundle qty_full_name quotients end local @@ -321,7 +324,7 @@ val OO_rules = @{thms left_total_OO left_unique_OO right_total_OO right_unique_OO bi_total_OO bi_unique_OO} in - fun parametrize_class_constraint ctxt pcr_def constraint = + fun parametrize_class_constraint ctxt0 pcr_def constraint = let fun generate_transfer_rule pcr_def constraint goal ctxt = let @@ -368,14 +371,14 @@ Pretty.str thm_name, Pretty.str " transfer rule found:", Pretty.brk 1] @ - Pretty.commas (map (Syntax.pretty_term ctxt) non_trivial_assms)) + Pretty.commas (map (Syntax.pretty_term ctxt0) non_trivial_assms)) |> Pretty.string_of |> warning end end val goal = make_goal pcr_def constraint - val thm = generate_transfer_rule pcr_def constraint goal ctxt + val thm = generate_transfer_rule pcr_def constraint goal ctxt0 val _ = check_assms thm in thm @@ -439,7 +442,7 @@ reduced_assm RS thm end in - fun parametrize_domain dom_thm (pcr_info : Lifting_Info.pcr) ctxt = + fun parametrize_domain dom_thm (pcr_info : Lifting_Info.pcr) ctxt0 = let fun reduce_first_assm ctxt rules thm = let @@ -456,11 +459,11 @@ val pcr_Domainp_par_left_total = (dom_thm RS @{thm pcr_Domainp_par_left_total}) |> fold_Domainp_pcrel pcrel_def - |> reduce_first_assm ctxt (Lifting_Info.get_reflexivity_rules ctxt) + |> reduce_first_assm ctxt0 (Lifting_Info.get_reflexivity_rules ctxt0) val pcr_Domainp_par = (dom_thm RS @{thm pcr_Domainp_par}) |> fold_Domainp_pcrel pcrel_def - |> reduce_Domainp ctxt (Transfer.get_relator_domain ctxt) + |> reduce_Domainp ctxt0 (Transfer.get_relator_domain ctxt0) val pcr_Domainp = (dom_thm RS @{thm pcr_Domainp}) |> fold_Domainp_pcrel pcrel_def @@ -513,10 +516,10 @@ opt_par_thm - a parametricity theorem for R *) -fun setup_by_quotient (config: config) quot_thm opt_reflp_thm opt_par_thm lthy = +fun setup_by_quotient (config: config) quot_thm opt_reflp_thm opt_par_thm lthy0 = let (**) - val quot_thm = Morphism.thm (Local_Theory.target_morphism lthy) quot_thm + val quot_thm = Morphism.thm (Local_Theory.target_morphism lthy0) quot_thm (**) val (rty, qty) = quot_thm_rty_qty quot_thm val induct_attr = Attrib.internal (K (Induct.induct_type (fst (dest_Type qty)))) @@ -558,21 +561,17 @@ notes2 @ notes1 @ notes end - fun generate_parametric_rel_eq lthy transfer_rule opt_param_thm = - option_fold transfer_rule (Lifting_Def.generate_parametric_transfer_rule lthy transfer_rule) opt_param_thm - handle Lifting_Term.MERGE_TRANSFER_REL msg => - let - val error_msg = cat_lines - ["Generation of a parametric transfer rule for the quotient relation failed.", - (Pretty.string_of (Pretty.block - [Pretty.str "Reason:", Pretty.brk 2, msg]))] - in - error error_msg - end + fun generate_parametric_rel_eq ctxt transfer_rule opt_param_thm = + option_fold transfer_rule + (Lifting_Def.generate_parametric_transfer_rule ctxt transfer_rule) opt_param_thm + handle Lifting_Term.MERGE_TRANSFER_REL msg => + error (cat_lines + ["Generation of a parametric transfer rule for the quotient relation failed.", + (Pretty.string_of (Pretty.block [Pretty.str "Reason:", Pretty.brk 2, msg]))]) - fun setup_transfer_rules_par lthy notes = + fun setup_transfer_rules_par ctxt notes = let - val pcrel_info = (the (get_pcrel_info lthy qty_full_name)) + val pcrel_info = the (get_pcrel_info ctxt qty_full_name) val pcrel_def = #pcrel_def pcrel_info val notes1 = case opt_reflp_thm of @@ -580,12 +579,12 @@ let val left_total = ([quot_thm, reflp_thm] MRSL @{thm Quotient_left_total}) val bi_total = ([quot_thm, reflp_thm] MRSL @{thm Quotient_bi_total}) - val domain_thms = parametrize_total_domain left_total pcrel_def lthy - val id_abs_transfer = generate_parametric_id lthy rty - (Lifting_Term.parametrize_transfer_rule lthy + val domain_thms = parametrize_total_domain left_total pcrel_def ctxt + val id_abs_transfer = generate_parametric_id ctxt rty + (Lifting_Term.parametrize_transfer_rule ctxt ([quot_thm, reflp_thm] MRSL @{thm Quotient_id_abs_transfer})) - val left_total = parametrize_class_constraint lthy pcrel_def left_total - val bi_total = parametrize_class_constraint lthy pcrel_def bi_total + val left_total = parametrize_class_constraint ctxt pcrel_def left_total + val bi_total = parametrize_class_constraint ctxt pcrel_def bi_total val thms = [("id_abs_transfer", [id_abs_transfer], @{attributes [transfer_rule]}), ("left_total", [left_total], @{attributes [transfer_rule]}), @@ -593,19 +592,19 @@ in map_thms qualify I thms @ map_thms qualify I domain_thms end - | NONE => + | NONE => let - val thms = parametrize_domain dom_thm pcrel_info lthy + val thms = parametrize_domain dom_thm pcrel_info ctxt in map_thms qualify I thms end - val rel_eq_transfer = generate_parametric_rel_eq lthy - (Lifting_Term.parametrize_transfer_rule lthy (quot_thm RS @{thm Quotient_rel_eq_transfer})) + val rel_eq_transfer = generate_parametric_rel_eq ctxt + (Lifting_Term.parametrize_transfer_rule ctxt (quot_thm RS @{thm Quotient_rel_eq_transfer})) opt_par_thm - val right_unique = parametrize_class_constraint lthy pcrel_def + val right_unique = parametrize_class_constraint ctxt pcrel_def (quot_thm RS @{thm Quotient_right_unique}) - val right_total = parametrize_class_constraint lthy pcrel_def + val right_total = parametrize_class_constraint ctxt pcrel_def (quot_thm RS @{thm Quotient_right_total}) val notes2 = map_thms qualify I [("rel_eq_transfer", [rel_eq_transfer], @{attributes [transfer_rule]}), @@ -617,15 +616,15 @@ fun setup_rules lthy = let - val thms = if is_some (get_pcrel_info lthy qty_full_name) - then setup_transfer_rules_par lthy notes1 else setup_transfer_rules_nonpar notes1 - in - notes (#notes config) thms lthy - end + val thms = + if is_some (get_pcrel_info lthy qty_full_name) + then setup_transfer_rules_par lthy notes1 + else setup_transfer_rules_nonpar notes1 + in notes (#notes config) thms lthy end in - lthy - |> setup_lifting_infr config quot_thm opt_reflp_thm - ||> setup_rules + lthy0 + |> setup_lifting_infr config quot_thm opt_reflp_thm + ||> setup_rules end (* @@ -636,12 +635,12 @@ typedef_thm - a typedef theorem (type_definition Rep Abs S) *) -fun setup_by_typedef_thm config typedef_thm lthy = +fun setup_by_typedef_thm config typedef_thm lthy0 = let val (_ $ rep_fun $ _ $ typedef_set) = (HOLogic.dest_Trueprop o Thm.prop_of) typedef_thm - val (T_def, lthy) = define_crel config rep_fun lthy + val (T_def, lthy1) = define_crel config rep_fun lthy0 (**) - val T_def = Morphism.thm (Local_Theory.target_morphism lthy) T_def + val T_def = Morphism.thm (Local_Theory.target_morphism lthy1) T_def (**) val quot_thm = case typedef_set of Const (\<^const_name>\top\, _) => @@ -686,9 +685,9 @@ map_thms qualify (fn thm => [typedef_thm, T_def] MRSL thm) thms @ notes1 @ notes end - fun setup_transfer_rules_par lthy notes = + fun setup_transfer_rules_par ctxt notes = let - val pcrel_info = (the (get_pcrel_info lthy qty_full_name)) + val pcrel_info = (the (get_pcrel_info ctxt qty_full_name)) val pcrel_def = #pcrel_def pcrel_info val notes1 = @@ -697,11 +696,11 @@ let val left_total = ([quot_thm, reflp_thm] MRSL @{thm Quotient_left_total}) val bi_total = ([quot_thm, reflp_thm] MRSL @{thm Quotient_bi_total}) - val domain_thms = parametrize_total_domain left_total pcrel_def lthy - val left_total = parametrize_class_constraint lthy pcrel_def left_total - val bi_total = parametrize_class_constraint lthy pcrel_def bi_total - val id_abs_transfer = generate_parametric_id lthy rty - (Lifting_Term.parametrize_transfer_rule lthy + val domain_thms = parametrize_total_domain left_total pcrel_def ctxt + val left_total = parametrize_class_constraint ctxt pcrel_def left_total + val bi_total = parametrize_class_constraint ctxt pcrel_def bi_total + val id_abs_transfer = generate_parametric_id ctxt rty + (Lifting_Term.parametrize_transfer_rule ctxt ([quot_thm, reflp_thm] MRSL @{thm Quotient_id_abs_transfer})) val thms = [("left_total", [left_total], @{attributes [transfer_rule]}), @@ -712,17 +711,17 @@ end | NONE => let - val thms = parametrize_domain dom_thm pcrel_info lthy + val thms = parametrize_domain dom_thm pcrel_info ctxt in map_thms qualify I thms end - val notes2 = map_thms qualify (fn thm => generate_parametric_id lthy rty - (Lifting_Term.parametrize_transfer_rule lthy ([typedef_thm, T_def] MRSL thm))) + val notes2 = map_thms qualify (fn thm => generate_parametric_id ctxt rty + (Lifting_Term.parametrize_transfer_rule ctxt ([typedef_thm, T_def] MRSL thm))) [("rep_transfer", @{thms typedef_rep_transfer}, @{attributes [transfer_rule]})]; val notes3 = map_thms qualify - (fn thm => parametrize_class_constraint lthy pcrel_def ([typedef_thm, T_def] MRSL thm)) + (fn thm => parametrize_class_constraint ctxt pcrel_def ([typedef_thm, T_def] MRSL thm)) [("left_unique", @{thms typedef_left_unique}, @{attributes [transfer_rule]}), ("right_unique", @{thms typedef_right_unique},@{attributes [transfer_rule]}), ("bi_unique", @{thms typedef_bi_unique}, @{attributes [transfer_rule]}), @@ -735,15 +734,15 @@ fun setup_rules lthy = let - val thms = if is_some (get_pcrel_info lthy qty_full_name) - then setup_transfer_rules_par lthy notes1 else setup_transfer_rules_nonpar notes1 - in - notes (#notes config) thms lthy - end + val thms = + if is_some (get_pcrel_info lthy qty_full_name) + then setup_transfer_rules_par lthy notes1 + else setup_transfer_rules_nonpar notes1 + in notes (#notes config) thms lthy end in - lthy - |> setup_lifting_infr config quot_thm opt_reflp_thm - ||> setup_rules + lthy1 + |> setup_lifting_infr config quot_thm opt_reflp_thm + ||> setup_rules end fun setup_lifting_cmd xthm opt_reflp_xthm opt_par_xthm lthy = @@ -918,7 +917,7 @@ ctxt |> lifting_restore (#quotient restore_info) |> fold_rev Transfer.transfer_raw_add (Item_Net.content (#transfer_rules restore_info)) - | NONE => ctxt + | NONE => ctxt end val lifting_restore_internal_attribute_setup = @@ -1034,7 +1033,7 @@ Local_Theory.declaration {syntax = false, pervasive = true} (fn phi => Lifting_Info.add_transfer_rules_in_restore_data pointer (new_transfer_rules refresh_data lthy phi)) lthy - | NONE => error "The lifting bundle refers to non-existent restore data." + | NONE => error "The lifting bundle refers to non-existent restore data." end fun lifting_update_cmd bundle_name lthy = diff -r 34bc296374ee -r 59258a3192bf src/HOL/Tools/Lifting/lifting_term.ML --- a/src/HOL/Tools/Lifting/lifting_term.ML Tue Jun 04 15:14:19 2019 +0200 +++ b/src/HOL/Tools/Lifting/lifting_term.ML Tue Jun 04 15:14:56 2019 +0200 @@ -53,12 +53,8 @@ type quotients = Lifting_Info.quotient Symtab.table fun match ctxt err ty_pat ty = - let - val thy = Proof_Context.theory_of ctxt - in - Sign.typ_match thy (ty_pat, ty) Vartab.empty - handle Type.TYPE_MATCH => err ctxt ty_pat ty - end + Sign.typ_match (Proof_Context.theory_of ctxt) (ty_pat, ty) Vartab.empty + handle Type.TYPE_MATCH => err ctxt ty_pat ty fun equiv_match_err ctxt ty_pat ty = let @@ -82,11 +78,7 @@ Pretty.str "found."]) fun get_quot_thm quotients ctxt s = - let - val thy = Proof_Context.theory_of ctxt - in - Thm.transfer thy (#quot_thm (get_quot_data quotients s)) - end + Thm.transfer' ctxt (#quot_thm (get_quot_data quotients s)) fun has_pcrel_info quotients s = is_some (#pcr_info (get_quot_data quotients s)) @@ -99,51 +91,34 @@ Pretty.str "found."]) fun get_pcrel_def quotients ctxt s = - let - val thy = Proof_Context.theory_of ctxt - in - Thm.transfer thy (#pcrel_def (get_pcrel_info quotients s)) - end + Thm.transfer' ctxt (#pcrel_def (get_pcrel_info quotients s)) fun get_pcr_cr_eq quotients ctxt s = - let - val thy = Proof_Context.theory_of ctxt - in - Thm.transfer thy (#pcr_cr_eq (get_pcrel_info quotients s)) - end + Thm.transfer' ctxt (#pcr_cr_eq (get_pcrel_info quotients s)) fun get_rel_quot_thm ctxt s = - let - val thy = Proof_Context.theory_of ctxt - in - (case Lifting_Info.lookup_quot_maps ctxt s of - SOME map_data => Thm.transfer thy (#rel_quot_thm map_data) - | NONE => raise QUOT_THM_INTERNAL (Pretty.block + (case Lifting_Info.lookup_quot_maps ctxt s of + SOME map_data => Thm.transfer' ctxt (#rel_quot_thm map_data) + | NONE => raise QUOT_THM_INTERNAL (Pretty.block [Pretty.str ("No relator for the type " ^ quote s), Pretty.brk 1, Pretty.str "found."])) - end - + fun get_rel_distr_rules ctxt s tm = - let - val thy = Proof_Context.theory_of ctxt - in - (case Lifting_Info.lookup_relator_distr_data ctxt s of - SOME rel_distr_thm => ( - case tm of - Const (\<^const_name>\POS\, _) => map (Thm.transfer thy) (#pos_distr_rules rel_distr_thm) - | Const (\<^const_name>\NEG\, _) => map (Thm.transfer thy) (#neg_distr_rules rel_distr_thm) - ) - | NONE => raise QUOT_THM_INTERNAL (Pretty.block + (case Lifting_Info.lookup_relator_distr_data ctxt s of + SOME rel_distr_thm => + (case tm of + Const (\<^const_name>\POS\, _) => map (Thm.transfer' ctxt) (#pos_distr_rules rel_distr_thm) + | Const (\<^const_name>\NEG\, _) => map (Thm.transfer' ctxt) (#neg_distr_rules rel_distr_thm)) + | NONE => raise QUOT_THM_INTERNAL (Pretty.block [Pretty.str ("No relator distr. data for the type " ^ quote s), Pretty.brk 1, Pretty.str "found."])) - end fun is_id_quot thm = Thm.eq_thm_prop (thm, @{thm identity_quotient}) -fun zip_Tvars ctxt type_name rty_Tvars qty_Tvars = - case try (get_rel_quot_thm ctxt) type_name of +fun zip_Tvars ctxt0 type_name rty_Tvars qty_Tvars = + case try (get_rel_quot_thm ctxt0) type_name of NONE => rty_Tvars ~~ qty_Tvars | SOME rel_quot_thm => let @@ -181,27 +156,26 @@ val qty = Type (type_name, qty_Tvars) val rel_quot_thm_concl = (Logic.strip_imp_concl o Thm.prop_of) rel_quot_thm val schematic_rel_absT = quot_term_absT rel_quot_thm_concl; - val thy = Proof_Context.theory_of ctxt val absT = rty --> qty val schematic_absT = absT - |> Logic.type_map (singleton (Variable.polymorphic ctxt)) + |> Logic.type_map (singleton (Variable.polymorphic ctxt0)) |> Logic.incr_tvar (maxidx_of_typ schematic_rel_absT + 1) (* because absT can already contain schematic variables from rty patterns *) val maxidx = Term.maxidx_of_typs [schematic_rel_absT, schematic_absT] - val _ = Sign.typ_unify thy (schematic_rel_absT, schematic_absT) (Vartab.empty,maxidx) - handle Type.TUNIFY => equiv_univ_err ctxt schematic_rel_absT schematic_absT + val _ = + Sign.typ_unify (Proof_Context.theory_of ctxt0) (schematic_rel_absT, schematic_absT) + (Vartab.empty, maxidx) + handle Type.TUNIFY => equiv_univ_err ctxt0 schematic_rel_absT schematic_absT val subs = raw_match (schematic_rel_absT, absT) Vartab.empty val rel_quot_thm_prems = (Logic.strip_imp_prems o Thm.prop_of) rel_quot_thm in - map (dest_funT o - Envir.subst_type subs o - quot_term_absT) - rel_quot_thm_prems + map (dest_funT o Envir.subst_type subs o quot_term_absT) rel_quot_thm_prems end -fun gen_rty_is_TVar quotients ctxt qty = qty |> Tname |> get_quot_thm quotients ctxt |> - quot_thm_rty_qty |> fst |> is_TVar +fun gen_rty_is_TVar quotients ctxt qty = + qty |> Tname |> get_quot_thm quotients ctxt + |> quot_thm_rty_qty |> fst |> is_TVar fun gen_instantiate_rtys quotients ctxt (rty, (qty as Type (qty_name, _))) = let @@ -307,25 +281,19 @@ fun force_qty_type ctxt qty quot_thm = let - val thy = Proof_Context.theory_of ctxt val (_, qty_schematic) = quot_thm_rty_qty quot_thm - val match_env = Sign.typ_match thy (qty_schematic, qty) Vartab.empty + val match_env = Sign.typ_match (Proof_Context.theory_of ctxt) (qty_schematic, qty) Vartab.empty fun prep_ty (x, (S, ty)) = ((x, S), Thm.ctyp_of ctxt ty) val ty_inst = Vartab.fold (cons o prep_ty) match_env [] - in - Thm.instantiate (ty_inst, []) quot_thm - end + in Thm.instantiate (ty_inst, []) quot_thm end fun check_rty_type ctxt rty quot_thm = let - val thy = Proof_Context.theory_of ctxt val (rty_forced, _) = quot_thm_rty_qty quot_thm val rty_schematic = Logic.type_map (singleton (Variable.polymorphic ctxt)) rty - val _ = Sign.typ_match thy (rty_schematic, rty_forced) Vartab.empty + val _ = Sign.typ_match (Proof_Context.theory_of ctxt) (rty_schematic, rty_forced) Vartab.empty handle Type.TYPE_MATCH => raise CHECK_RTY (rty_schematic, rty_forced) - in - () - end + in () end (* The function tries to prove that rty and qty form a quotient. @@ -344,9 +312,7 @@ val (schematic_quot_thm, _) = prove_schematic_quot_thm id_actions quotients ctxt (rty, qty) () val quot_thm = force_qty_type ctxt qty schematic_quot_thm val _ = check_rty_type ctxt rty quot_thm - in - quot_thm - end + in quot_thm end end (* @@ -370,26 +336,28 @@ val tfrees_Q_t = rev (Term.add_tfree_names Q_t []) in 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 + 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 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 + 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 (* @@ -402,39 +370,29 @@ to the corresponding assumption in the returned theorem. *) -fun prove_param_quot_thm ctxt ty = +fun prove_param_quot_thm ctxt0 ty = let - fun generate (ty as Type (s, tys)) (table_ctxt as (table, ctxt)) = - if null tys - then - let - val instantiated_id_quot_thm = - Thm.instantiate' [SOME (Thm.ctyp_of ctxt ty)] [] @{thm identity_quotient} - in - (instantiated_id_quot_thm, (table, ctxt)) - end - else - let - val (args, table_ctxt) = fold_map generate tys table_ctxt - in - (args MRSL (get_rel_quot_thm ctxt s), table_ctxt) - end + fun generate (ty as Type (s, tys)) (table, ctxt) = + if null tys then + let + val instantiated_id_quot_thm = + Thm.instantiate' [SOME (Thm.ctyp_of ctxt ty)] [] @{thm identity_quotient} + in (instantiated_id_quot_thm, (table, ctxt)) end + else + let val (args, table_ctxt') = fold_map generate tys (table, ctxt) + in (args MRSL (get_rel_quot_thm ctxt s), table_ctxt') end | generate ty (table, ctxt) = - if AList.defined (op=) table ty - then (the (AList.lookup (op=) table ty), (table, ctxt)) - else - let - val (Q_t, ctxt') = get_fresh_Q_t ctxt - val Q_thm = Thm.assume (Thm.cterm_of ctxt' Q_t) - val table' = (ty, Q_thm) :: table - in - (Q_thm, (table', ctxt')) - end + if AList.defined (op =) table ty + then (the (AList.lookup (op =) table ty), (table, ctxt)) + else + let + val (Q_t, ctxt') = get_fresh_Q_t ctxt + val Q_thm = Thm.assume (Thm.cterm_of ctxt' Q_t) + val table' = (ty, Q_thm) :: table + in (Q_thm, (table', ctxt')) end - val (param_quot_thm, (table, ctxt)) = generate ty ([], ctxt) - in - (param_quot_thm, rev table, ctxt) - end + val (param_quot_thm, (table, ctxt1)) = generate ty ([], ctxt0) + in (param_quot_thm, rev table, ctxt1) end handle QUOT_THM_INTERNAL pretty_msg => raise PARAM_QUOT_THM (ty, pretty_msg) (* @@ -446,11 +404,10 @@ fun generate_parametrized_relator ctxt ty = let - val orig_ctxt = ctxt - val (quot_thm, table, ctxt) = prove_param_quot_thm ctxt ty + 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) + val exported_terms = Variable.exportT_terms ctxt' ctxt (parametrized_relator :: args) in (hd exported_terms, tl exported_terms) end @@ -487,7 +444,7 @@ fun rewrs_imp rules = first_imp (map rewr_imp rules) in - fun gen_merge_transfer_relations quotients ctxt ctm = + fun gen_merge_transfer_relations quotients ctxt0 ctm = let val ctm = Thm.dest_arg ctm val tm = Thm.term_of ctm @@ -498,14 +455,15 @@ fun prove_extra_assms ctxt ctm distr_rule = let - fun prove_assm assm = try (Goal.prove ctxt [] [] (Thm.term_of assm)) - (fn _ => SOLVED' (REPEAT_ALL_NEW (resolve_tac ctxt (Transfer.get_transfer_raw ctxt))) 1) + fun prove_assm assm = + try (Goal.prove ctxt [] [] (Thm.term_of assm)) (fn _ => (* FIXME proper goal_ctxt!? *) + SOLVED' (REPEAT_ALL_NEW (resolve_tac ctxt (Transfer.get_transfer_raw ctxt))) 1) fun is_POS_or_NEG ctm = case (head_of o Thm.term_of o Thm.dest_arg) ctm of Const (\<^const_name>\POS\, _) => true - | Const (\<^const_name>\NEG\, _) => true - | _ => false + | Const (\<^const_name>\NEG\, _) => true + | _ => false val inst_distr_rule = rewr_imp distr_rule ctm val extra_assms = filter_out is_POS_or_NEG (cprems_of inst_distr_rule) @@ -518,7 +476,7 @@ fun cannot_merge_error_msg () = Pretty.block [Pretty.str "Rewriting (merging) of this term has failed:", Pretty.brk 1, - Syntax.pretty_term ctxt rel] + Syntax.pretty_term ctxt0 rel] in case get_args 2 rel of @@ -530,25 +488,25 @@ in if same_type_constrs (rty', qty) then let - val distr_rules = get_rel_distr_rules ctxt ((fst o dest_Type) rty') (head_of tm) - val distr_rule = get_first (prove_extra_assms ctxt ctm) distr_rules + val distr_rules = get_rel_distr_rules ctxt0 ((fst o dest_Type) rty') (head_of tm) + val distr_rule = get_first (prove_extra_assms ctxt0 ctm) distr_rules in case distr_rule of NONE => raise MERGE_TRANSFER_REL (cannot_merge_error_msg ()) - | SOME distr_rule => (map (gen_merge_transfer_relations quotients ctxt) - (cprems_of distr_rule)) - MRSL distr_rule + | SOME distr_rule => + map (gen_merge_transfer_relations quotients ctxt0) (cprems_of distr_rule) + MRSL distr_rule end else let - val pcrel_def = get_pcrel_def quotients ctxt ((fst o dest_Type) qty) + val pcrel_def = get_pcrel_def quotients ctxt0 ((fst o dest_Type) qty) val pcrel_const = (head_of o fst o Logic.dest_equals o Thm.prop_of) pcrel_def in if same_constants pcrel_const (head_of trans_rel) then let val unfolded_ctm = Thm.rhs_of (Conv.arg1_conv (Conv.arg_conv (Conv.rewr_conv pcrel_def)) ctm) val distr_rule = rewrs_imp @{thms POS_pcr_rule NEG_pcr_rule} unfolded_ctm - val result = (map (gen_merge_transfer_relations quotients ctxt) + val result = (map (gen_merge_transfer_relations quotients ctxt0) (cprems_of distr_rule)) MRSL distr_rule val fold_pcr_rel = Conv.rewr_conv (Thm.symmetric pcrel_def) in @@ -572,8 +530,8 @@ (e.g., (rel_S R) OO (pcr_T op=) --> pcr_T R using the definition pcr_T R = (rel_S R) OO cr_T). *) - fun merge_transfer_relations ctxt ctm = gen_merge_transfer_relations - (Lifting_Info.get_quotients ctxt) ctxt ctm + fun merge_transfer_relations ctxt ctm = + gen_merge_transfer_relations (Lifting_Info.get_quotients ctxt) ctxt ctm end fun gen_parametrize_transfer_rule quotients ctxt thm = diff -r 34bc296374ee -r 59258a3192bf src/HOL/Tools/Lifting/lifting_util.ML --- a/src/HOL/Tools/Lifting/lifting_util.ML Tue Jun 04 15:14:19 2019 +0200 +++ b/src/HOL/Tools/Lifting/lifting_util.ML Tue Jun 04 15:14:56 2019 +0200 @@ -128,7 +128,6 @@ end fun conceal_naming_result f lthy = - let val old_lthy = lthy - in lthy |> Proof_Context.concealed |> f ||> Proof_Context.restore_naming old_lthy end; + lthy |> Proof_Context.concealed |> f ||> Proof_Context.restore_naming lthy; end diff -r 34bc296374ee -r 59258a3192bf src/HOL/Tools/Meson/meson_clausify.ML --- a/src/HOL/Tools/Meson/meson_clausify.ML Tue Jun 04 15:14:19 2019 +0200 +++ b/src/HOL/Tools/Meson/meson_clausify.ML Tue Jun 04 15:14:56 2019 +0200 @@ -363,27 +363,26 @@ (* Convert a theorem to CNF, with additional premises due to skolemization. *) fun cnf_axiom ctxt0 new_skolem combinators ax_no th = let - val thy = Proof_Context.theory_of ctxt0 - val choice_ths = choice_theorems thy - val (opt, (nnf_th, ctxt)) = + val choice_ths = choice_theorems (Proof_Context.theory_of ctxt0) + val (opt, (nnf_th, ctxt1)) = nnf_axiom choice_ths new_skolem ax_no th ctxt0 fun clausify th = make_cnf (if new_skolem orelse null choice_ths then [] - else map (old_skolem_theorem_of_def ctxt) (old_skolem_defs th)) - th ctxt - val (cnf_ths, ctxt) = clausify nnf_th + else map (old_skolem_theorem_of_def ctxt1) (old_skolem_defs th)) + th ctxt1 + val (cnf_ths, ctxt2) = clausify nnf_th fun intr_imp ct th = - Thm.instantiate ([], [((("i", 0), \<^typ>\nat\), Thm.cterm_of ctxt (HOLogic.mk_nat ax_no))]) + Thm.instantiate ([], [((("i", 0), \<^typ>\nat\), Thm.cterm_of ctxt2 (HOLogic.mk_nat ax_no))]) (zero_var_indexes @{thm skolem_COMBK_D}) RS Thm.implies_intr ct th in - (opt |> Option.map (I #>> singleton (Variable.export ctxt ctxt0) + (opt |> Option.map (I #>> singleton (Variable.export ctxt2 ctxt0) ##> (Thm.term_of #> HOLogic.dest_Trueprop - #> singleton (Variable.export_terms ctxt ctxt0))), - cnf_ths |> map (combinators ? introduce_combinators_in_theorem ctxt + #> singleton (Variable.export_terms ctxt2 ctxt0))), + cnf_ths |> map (combinators ? introduce_combinators_in_theorem ctxt2 #> (case opt of SOME (_, ct) => intr_imp ct | NONE => I)) - |> Variable.export ctxt ctxt0 + |> Variable.export ctxt2 ctxt0 |> finish_cnf |> map Thm.close_derivation) end diff -r 34bc296374ee -r 59258a3192bf src/HOL/Tools/SMT/smt_replay.ML --- a/src/HOL/Tools/SMT/smt_replay.ML Tue Jun 04 15:14:19 2019 +0200 +++ b/src/HOL/Tools/SMT/smt_replay.ML Tue Jun 04 15:14:56 2019 +0200 @@ -186,14 +186,14 @@ |> map (fn ithm as (_, thm) => (ithm, Thm.cprop_of thm aconvc ct)) in -fun add_asserted tab_update tab_empty p_extract cond outer_ctxt rewrite_rules assms steps ctxt = +fun add_asserted tab_update tab_empty p_extract cond outer_ctxt rewrite_rules assms steps ctxt0 = let - val eqs = map (rewrite ctxt [rewrite_true_rule]) rewrite_rules + val eqs = map (rewrite ctxt0 [rewrite_true_rule]) rewrite_rules val eqs' = union Thm.eq_thm eqs prep_rules val assms_net = assms - |> map (apsnd (rewrite ctxt eqs')) + |> map (apsnd (rewrite ctxt0 eqs')) |> map (apsnd (Conv.fconv_rule Thm.eta_conversion)) |> thm_net_of snd @@ -229,7 +229,7 @@ else cx end - in fold add steps (([], []), (ctxt, tab_empty)) end + in fold add steps (([], []), (ctxt0, tab_empty)) end end