# HG changeset patch # User wenzelm # Date 1559646857 -7200 # Node ID c61b7af108a6dc832a0f87cee534338b7158a651 # Parent 2f9623aa1eebe02837b953ce5a6924ec7bf3e779 misc tuning and clarification, notably wrt. flow of context; diff -r 2f9623aa1eeb -r c61b7af108a6 src/HOL/Tools/Transfer/transfer.ML --- a/src/HOL/Tools/Transfer/transfer.ML Tue Jun 04 13:09:24 2019 +0200 +++ b/src/HOL/Tools/Transfer/transfer.ML Tue Jun 04 13:14:17 2019 +0200 @@ -124,36 +124,27 @@ pred_data = Symtab.merge (K true) (pd1, pd2) } ) -fun get_transfer_raw ctxt = ctxt - |> (Item_Net.content o #transfer_raw o Data.get o Context.Proof) +val get_transfer_raw = Item_Net.content o #transfer_raw o Data.get o Context.Proof -fun get_known_frees ctxt = ctxt - |> (#known_frees o Data.get o Context.Proof) +val get_known_frees = #known_frees o Data.get o Context.Proof -fun get_compound_lhs ctxt = ctxt - |> (#compound_lhs o Data.get o Context.Proof) +val get_compound_lhs = #compound_lhs o Data.get o Context.Proof -fun get_compound_rhs ctxt = ctxt - |> (#compound_rhs o Data.get o Context.Proof) +val get_compound_rhs = #compound_rhs o Data.get o Context.Proof -fun get_relator_eq_item_net ctxt = (#relator_eq o Data.get o Context.Proof) ctxt +val get_relator_eq_item_net = #relator_eq o Data.get o Context.Proof -fun get_relator_eq ctxt = ctxt - |> (Item_Net.content o #relator_eq o Data.get o Context.Proof) - |> map safe_mk_meta_eq +val get_relator_eq = + map safe_mk_meta_eq o Item_Net.content o #relator_eq o Data.get o Context.Proof -fun get_sym_relator_eq ctxt = ctxt - |> (Item_Net.content o #relator_eq o Data.get o Context.Proof) - |> map (Thm.symmetric o safe_mk_meta_eq) +val get_sym_relator_eq = + map (Thm.symmetric o safe_mk_meta_eq) o Item_Net.content o #relator_eq o Data.get o Context.Proof -fun get_relator_eq_raw ctxt = ctxt - |> (Item_Net.content o #relator_eq_raw o Data.get o Context.Proof) +val get_relator_eq_raw = Item_Net.content o #relator_eq_raw o Data.get o Context.Proof -fun get_relator_domain ctxt = ctxt - |> (Item_Net.content o #relator_domain o Data.get o Context.Proof) +val get_relator_domain = Item_Net.content o #relator_domain o Data.get o Context.Proof -fun get_pred_data ctxt = ctxt - |> (#pred_data o Data.get o Context.Proof) +val get_pred_data = #pred_data o Data.get o Context.Proof fun map_data f1 f2 f3 f4 f5 f6 f7 f8 { transfer_raw, known_frees, compound_lhs, compound_rhs, @@ -358,7 +349,7 @@ in forall_elim (thm COMP (equal_thm COMP @{thm equal_elim_rule2})) end - handle TERM _ => thm + handle TERM _ => thm fun abstract_domains_transfer ctxt thm = let @@ -404,14 +395,14 @@ (** Adding transfer domain rules **) -fun prep_transfer_domain_thm ctxt thm = - (abstract_equalities_domain ctxt o detect_transfer_rules) thm +fun prep_transfer_domain_thm ctxt = + abstract_equalities_domain ctxt o detect_transfer_rules -fun add_transfer_domain_thm thm ctxt = (add_transfer_thm o - prep_transfer_domain_thm (Context.proof_of ctxt)) thm ctxt +fun add_transfer_domain_thm thm ctxt = + (add_transfer_thm o prep_transfer_domain_thm (Context.proof_of ctxt)) thm ctxt -fun del_transfer_domain_thm thm ctxt = (del_transfer_thm o - prep_transfer_domain_thm (Context.proof_of ctxt)) thm ctxt +fun del_transfer_domain_thm thm ctxt = + (del_transfer_thm o prep_transfer_domain_thm (Context.proof_of ctxt)) thm ctxt (** Transfer proof method **) @@ -495,32 +486,26 @@ end (* create a lambda term of the same shape as the given term *) -fun skeleton (is_atom : term -> bool) ctxt t = +fun skeleton is_atom = let fun dummy ctxt = - let - val (c, ctxt) = yield_singleton Variable.variant_fixes "a" ctxt - in - (Free (c, dummyT), ctxt) - end - fun go (Bound i) ctxt = (Bound i, ctxt) - | go (Abs (x, _, t)) ctxt = - let - val (t', ctxt) = go t ctxt - in - (Abs (x, dummyT, t'), ctxt) - end - | go (tu as (t $ u)) ctxt = - if is_atom tu andalso not (Term.is_open tu) then dummy ctxt else - let - val (t', ctxt) = go t ctxt - val (u', ctxt) = go u ctxt - in - (t' $ u', ctxt) - end - | go _ ctxt = dummy ctxt + let val (c, ctxt') = yield_singleton Variable.variant_fixes "a" ctxt + in (Free (c, dummyT), ctxt') end + fun skel (Bound i) ctxt = (Bound i, ctxt) + | skel (Abs (x, _, t)) ctxt = + let val (t', ctxt) = skel t ctxt + in (Abs (x, dummyT, t'), ctxt) end + | skel (tu as t $ u) ctxt = + if is_atom tu andalso not (Term.is_open tu) then dummy ctxt + else + let + val (t', ctxt) = skel t ctxt + val (u', ctxt) = skel u ctxt + in (t' $ u', ctxt) end + | skel _ ctxt = dummy ctxt in - go t ctxt |> fst |> Syntax.check_term ctxt + fn ctxt => fn t => + fst (skel t ctxt) |> Syntax.check_term ctxt (* FIXME avoid syntax operation!? *) end (** Monotonicity analysis **) @@ -580,7 +565,7 @@ fun matches_list ctxt term = is_some o find_first (fn pat => Pattern.matches (Proof_Context.theory_of ctxt) (pat, term)) -fun transfer_rule_of_term ctxt equiv t : thm = +fun transfer_rule_of_term ctxt equiv t = let val compound_rhs = get_compound_rhs ctxt fun is_rhs t = compound_rhs |> retrieve_terms t |> matches_list ctxt t @@ -599,11 +584,11 @@ ((Name.clean_index (prep a, idx), \<^typ>\bool \ bool \ bool\), Thm.cterm_of ctxt' t) in thm - |> Thm.generalize (tfrees, rnames @ frees) idx - |> Thm.instantiate (map tinst binsts, map inst binsts) + |> Thm.generalize (tfrees, rnames @ frees) idx + |> Thm.instantiate (map tinst binsts, map inst binsts) end -fun transfer_rule_of_lhs ctxt t : thm = +fun transfer_rule_of_lhs ctxt t = let val compound_lhs = get_compound_lhs ctxt fun is_lhs t = compound_lhs |> retrieve_terms t |> matches_list ctxt t @@ -622,8 +607,8 @@ ((Name.clean_index (prep a, idx), \<^typ>\bool \ bool \ bool\), Thm.cterm_of ctxt' t) in thm - |> Thm.generalize (tfrees, rnames @ frees) idx - |> Thm.instantiate (map tinst binsts, map inst binsts) + |> Thm.generalize (tfrees, rnames @ frees) idx + |> Thm.instantiate (map tinst binsts, map inst binsts) end fun eq_rules_tac ctxt eq_rules = @@ -719,11 +704,8 @@ fun transferred ctxt extra_rules thm = let - val start_rule = @{thm transfer_start} - val start_rule' = @{thm transfer_start'} val rules = extra_rules @ get_transfer_raw ctxt val eq_rules = get_relator_eq_raw ctxt - val err_msg = "Transfer failed to convert goal to an object-logic formula" val pre_simps = @{thms transfer_forall_eq transfer_implies_eq} val thm1 = Drule.forall_intr_vars thm val instT = @@ -733,24 +715,22 @@ |> Thm.instantiate (instT, []) |> Raw_Simplifier.rewrite_rule ctxt pre_simps val ctxt' = Variable.declare_names (Thm.full_prop_of thm2) ctxt - val t = HOLogic.dest_Trueprop (Thm.concl_of thm2) - val rule = transfer_rule_of_lhs ctxt' t - val tac = - resolve_tac ctxt' [thm2 RS start_rule', thm2 RS start_rule] 1 THEN - (resolve_tac ctxt' [rule] - THEN_ALL_NEW - (SOLVED' (REPEAT_ALL_NEW (resolve_tac ctxt' rules) - THEN_ALL_NEW (DETERM o eq_rules_tac ctxt' eq_rules)))) 1 - handle TERM (_, ts) => raise TERM (err_msg, ts) - val goal = Thm.cterm_of ctxt' (HOLogic.mk_Trueprop (Var (("P", 0), \<^typ>\bool\))) - val thm3 = Goal.prove_internal ctxt' [] goal (K tac) - val tnames = map (fst o dest_TFree o Thm.typ_of o snd) instT + val rule = transfer_rule_of_lhs ctxt' (HOLogic.dest_Trueprop (Thm.concl_of thm2)) in - thm3 - |> Raw_Simplifier.rewrite_rule ctxt' post_simps - |> Simplifier.norm_hhf ctxt' - |> Drule.generalize (tnames, []) - |> Drule.zero_var_indexes + Goal.prove_internal ctxt' [] + (Thm.cterm_of ctxt' (HOLogic.mk_Trueprop (Var (("P", 0), \<^typ>\bool\)))) + (fn _ => + resolve_tac ctxt' [thm2 RS @{thm transfer_start'}, thm2 RS @{thm transfer_start}] 1 THEN + (resolve_tac ctxt' [rule] + THEN_ALL_NEW + (SOLVED' (REPEAT_ALL_NEW (resolve_tac ctxt' rules) + THEN_ALL_NEW (DETERM o eq_rules_tac ctxt' eq_rules)))) 1 + handle TERM (_, ts) => + raise TERM ("Transfer failed to convert goal to an object-logic formula", ts)) + |> Raw_Simplifier.rewrite_rule ctxt' post_simps + |> Simplifier.norm_hhf ctxt' + |> Drule.generalize (map (fst o dest_TFree o Thm.typ_of o snd) instT, []) + |> Drule.zero_var_indexes end (* handle THM _ => thm @@ -758,10 +738,8 @@ fun untransferred ctxt extra_rules thm = let - val start_rule = @{thm untransfer_start} val rules = extra_rules @ get_transfer_raw ctxt val eq_rules = get_relator_eq_raw ctxt - val err_msg = "Transfer failed to convert goal to an object-logic formula" val pre_simps = @{thms transfer_forall_eq transfer_implies_eq} val thm1 = Drule.forall_intr_vars thm val instT = @@ -773,22 +751,21 @@ val ctxt' = Variable.declare_names (Thm.full_prop_of thm2) ctxt val t = HOLogic.dest_Trueprop (Thm.concl_of thm2) val rule = transfer_rule_of_term ctxt' true t - val tac = - resolve_tac ctxt' [thm2 RS start_rule] 1 THEN - (resolve_tac ctxt' [rule] - THEN_ALL_NEW - (SOLVED' (REPEAT_ALL_NEW (resolve_tac ctxt' rules) - THEN_ALL_NEW (DETERM o eq_rules_tac ctxt' eq_rules)))) 1 - handle TERM (_, ts) => raise TERM (err_msg, ts) - val goal = Thm.cterm_of ctxt' (HOLogic.mk_Trueprop (Var (("P", 0), \<^typ>\bool\))) - val thm3 = Goal.prove_internal ctxt' [] goal (K tac) - val tnames = map (fst o dest_TFree o Thm.typ_of o snd) instT in - thm3 - |> Raw_Simplifier.rewrite_rule ctxt' post_simps - |> Simplifier.norm_hhf ctxt' - |> Drule.generalize (tnames, []) - |> Drule.zero_var_indexes + Goal.prove_internal ctxt' [] + (Thm.cterm_of ctxt' (HOLogic.mk_Trueprop (Var (("P", 0), \<^typ>\bool\)))) + (fn _ => + resolve_tac ctxt' [thm2 RS @{thm untransfer_start}] 1 THEN + (resolve_tac ctxt' [rule] + THEN_ALL_NEW + (SOLVED' (REPEAT_ALL_NEW (resolve_tac ctxt' rules) + THEN_ALL_NEW (DETERM o eq_rules_tac ctxt' eq_rules)))) 1 + handle TERM (_, ts) => + raise TERM ("Transfer failed to convert goal to an object-logic formula", ts)) + |> Raw_Simplifier.rewrite_rule ctxt' post_simps + |> Simplifier.norm_hhf ctxt' + |> Drule.generalize (map (fst o dest_TFree o Thm.typ_of o snd) instT, []) + |> Drule.zero_var_indexes end (** Methods and attributes **) @@ -863,7 +840,8 @@ map_pred_data' morph_thm morph_thm (map morph_thm) end -fun lookup_pred_data ctxt type_name = Symtab.lookup (get_pred_data ctxt) type_name +fun lookup_pred_data ctxt type_name = + Symtab.lookup (get_pred_data ctxt) type_name |> Option.map (morph_pred_data (Morphism.transfer_morphism' ctxt)) fun update_pred_data type_name qinfo ctxt = diff -r 2f9623aa1eeb -r c61b7af108a6 src/HOL/Tools/Transfer/transfer_bnf.ML --- a/src/HOL/Tools/Transfer/transfer_bnf.ML Tue Jun 04 13:09:24 2019 +0200 +++ b/src/HOL/Tools/Transfer/transfer_bnf.ML Tue Jun 04 13:14:17 2019 +0200 @@ -72,55 +72,56 @@ constraint_def |> Thm.prop_of |> HOLogic.dest_Trueprop |> fst o HOLogic.dest_eq |> head_of |> fst o dest_Const val live = live_of_bnf bnf - val (((As, Bs), Ds), ctxt) = ctxt + val (((As, Bs), Ds), ctxt') = ctxt |> mk_TFrees live ||>> mk_TFrees live ||>> mk_TFrees' (map Type.sort_of_atyp (deads_of_bnf bnf)) val relator = mk_rel_of_bnf Ds As Bs bnf val relsT = map2 mk_pred2T As Bs - val (args, ctxt) = Ctr_Sugar_Util.mk_Frees "R" relsT ctxt + val (args, ctxt'') = Ctr_Sugar_Util.mk_Frees "R" relsT ctxt' val concl = HOLogic.mk_Trueprop (mk_relation_constraint constr_name (list_comb (relator, args))) val assms = map (HOLogic.mk_Trueprop o (mk_relation_constraint constr_name)) args val goal = Logic.list_implies (assms, concl) in - (goal, ctxt) + (goal, ctxt'') end fun prove_relation_side_constraint ctxt bnf constraint_def = let - val old_ctxt = ctxt - val (goal, ctxt) = generate_relation_constraint_goal ctxt bnf constraint_def - val thm = Goal.prove_sorry ctxt [] [] goal - (fn {context = ctxt, prems = _} => side_constraint_tac bnf [constraint_def] ctxt 1) - |> Thm.close_derivation + val (goal, ctxt') = generate_relation_constraint_goal ctxt bnf constraint_def in - Drule.zero_var_indexes (singleton (Variable.export ctxt old_ctxt) thm) + Goal.prove_sorry ctxt' [] [] goal (fn {context = goal_ctxt, ...} => + side_constraint_tac bnf [constraint_def] goal_ctxt 1) + |> Thm.close_derivation + |> singleton (Variable.export ctxt' ctxt) + |> Drule.zero_var_indexes end fun prove_relation_bi_constraint ctxt bnf constraint_def side_constraints = let - val old_ctxt = ctxt - val (goal, ctxt) = generate_relation_constraint_goal ctxt bnf constraint_def - val thm = Goal.prove_sorry ctxt [] [] goal - (fn {context = ctxt, prems = _} => bi_constraint_tac constraint_def side_constraints ctxt 1) - |> Thm.close_derivation + val (goal, ctxt') = generate_relation_constraint_goal ctxt bnf constraint_def in - Drule.zero_var_indexes (singleton (Variable.export ctxt old_ctxt) thm) + Goal.prove_sorry ctxt' [] [] goal (fn {context = goal_ctxt, ...} => + bi_constraint_tac constraint_def side_constraints goal_ctxt 1) + |> Thm.close_derivation + |> singleton (Variable.export ctxt' ctxt) + |> Drule.zero_var_indexes end -val defs = [("left_total_rel", @{thm left_total_alt_def}), ("right_total_rel", @{thm right_total_alt_def}), +val defs = + [("left_total_rel", @{thm left_total_alt_def}), ("right_total_rel", @{thm right_total_alt_def}), ("left_unique_rel", @{thm left_unique_alt_def}), ("right_unique_rel", @{thm right_unique_alt_def})] -fun prove_relation_constraints bnf lthy = +fun prove_relation_constraints bnf ctxt = let val transfer_attr = @{attributes [transfer_rule]} val Tname = base_name_of_bnf bnf - val defs = map (apsnd (prove_relation_side_constraint lthy bnf)) defs - val bi_total = prove_relation_bi_constraint lthy bnf @{thm bi_total_alt_def} + val defs = map (apsnd (prove_relation_side_constraint ctxt bnf)) defs + val bi_total = prove_relation_bi_constraint ctxt bnf @{thm bi_total_alt_def} [snd (nth defs 0), snd (nth defs 1)] - val bi_unique = prove_relation_bi_constraint lthy bnf @{thm bi_unique_alt_def} + val bi_unique = prove_relation_bi_constraint ctxt bnf @{thm bi_unique_alt_def} [snd (nth defs 2), snd (nth defs 3)] val defs = ("bi_total_rel", bi_total) :: ("bi_unique_rel", bi_unique) :: defs in @@ -174,23 +175,23 @@ fun prove_Domainp_rel ctxt bnf pred_def = 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' (map Type.sort_of_atyp (deads_of_bnf bnf)) val relator = mk_rel_of_bnf Ds As Bs bnf val relsT = map2 mk_pred2T As Bs - val (args, ctxt) = Ctr_Sugar_Util.mk_Frees "R" relsT ctxt + val (args, ctxt'') = Ctr_Sugar_Util.mk_Frees "R" relsT ctxt' val lhs = mk_Domainp (list_comb (relator, args)) val rhs = Term.list_comb (mk_pred_of_bnf Ds As bnf, map mk_Domainp args) val goal = HOLogic.mk_eq (lhs, rhs) |> HOLogic.mk_Trueprop - val thm = Goal.prove_sorry ctxt [] [] goal - (fn {context = ctxt, prems = _} => Domainp_tac bnf pred_def 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, ...} => + Domainp_tac bnf pred_def goal_ctxt 1) + |> Thm.close_derivation + |> singleton (Variable.export ctxt'' ctxt) + |> Drule.zero_var_indexes end fun predicator bnf lthy = @@ -232,8 +233,8 @@ (* simplification rules for the predicator *) -fun lookup_defined_pred_data lthy name = - case Transfer.lookup_pred_data lthy name of +fun lookup_defined_pred_data ctxt name = + case Transfer.lookup_pred_data ctxt name of SOME data => data | NONE => raise NO_PRED_DATA ()