misc tuning and clarification, notably wrt. flow of context;

--- 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>\<open>bool \<Rightarrow> bool \<Rightarrow> bool\<close>), 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>\<open>bool \<Rightarrow> bool \<Rightarrow> bool\<close>), 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>\<open>bool\<close>)))
-    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>\<open>bool\<close>))))
+      (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>\<open>bool\<close>)))
-    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>\<open>bool\<close>))))
+      (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 =

--- 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 ()