misc tuning and clarification, notably wrt. flow of context;
--- 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
--- 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 *)
--- 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>\<open>True\<close> else fold_rev Term.lambda arg \<^const>\<open>False\<close>)) 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 "(\<And>x. P1 x \<Longrightarrow> P2 (f x)) \<Longrightarrow> (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>\<open>rel_fun\<close>, _) $ _ $ _ =>
@@ -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 =
--- 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
--- 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>\<open>relcompp\<close>, _) $ Const (\<^const_name>\<open>HOL.eq\<close>, _) $ _ =>
@@ -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>\<open>relcompp\<close>, _) $ t $ _ => print_generate_pcr_cr_eq_error lthy t
+ | Const (\<^const_name>\<open>relcompp\<close>, _) $ 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>\<open>top\<close>, _) =>
@@ -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 =
--- 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>\<open>POS\<close>, _) => map (Thm.transfer thy) (#pos_distr_rules rel_distr_thm)
- | Const (\<^const_name>\<open>NEG\<close>, _) => 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>\<open>POS\<close>, _) => map (Thm.transfer' ctxt) (#pos_distr_rules rel_distr_thm)
+ | Const (\<^const_name>\<open>NEG\<close>, _) => 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>\<open>POS\<close>, _) => true
- | Const (\<^const_name>\<open>NEG\<close>, _) => true
- | _ => false
+ | Const (\<^const_name>\<open>NEG\<close>, _) => 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 =
--- 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
--- 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>\<open>nat\<close>), Thm.cterm_of ctxt (HOLogic.mk_nat ax_no))])
+ Thm.instantiate ([], [((("i", 0), \<^typ>\<open>nat\<close>), 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
--- 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