src/HOL/Tools/transfer.ML

 (*  Title:      HOL/Tools/transfer.ML
     Author:     Brian Huffman, TU Muenchen
+    Author:     Ondrej Kuncar, TU Muenchen
 
 Generic theorem transfer method.
 *)
 
 signature TRANSFER =
 sig
   val prep_conv: conv
+  val get_transfer_raw: Proof.context -> thm list
   val get_relator_eq: Proof.context -> thm list
   val get_sym_relator_eq: Proof.context -> thm list
   val get_relator_eq_raw: Proof.context -> thm list
-  val get_transfer_raw: Proof.context -> thm list
+  val get_relator_domain: Proof.context -> thm list
   val transfer_add: attribute
   val transfer_del: attribute
+  val transfer_domain_add: attribute
+  val transfer_domain_del: attribute
   val transfer_rule_of_term: Proof.context -> term -> thm
   val transfer_tac: bool -> Proof.context -> int -> tactic
   val transfer_prover_tac: Proof.context -> int -> tactic
   val setup: theory -> theory
 end

   type T =
     { transfer_raw : thm Item_Net.T,
       known_frees : (string * typ) list,
       compound_rhs : unit Net.net,
       relator_eq : thm Item_Net.T,
-      relator_eq_raw : thm Item_Net.T }
+      relator_eq_raw : thm Item_Net.T,
+      relator_domain : thm Item_Net.T }
   val empty =
     { transfer_raw = Thm.full_rules,
       known_frees = [],
       compound_rhs = Net.empty,
       relator_eq = Thm.full_rules,
-      relator_eq_raw = Thm.full_rules }
+      relator_eq_raw = Thm.full_rules,
+      relator_domain = Thm.full_rules }
   val extend = I
   fun merge
     ( { transfer_raw = t1, known_frees = k1,
         compound_rhs = c1, relator_eq = r1,
-        relator_eq_raw = rw1 },
+        relator_eq_raw = rw1, relator_domain = rd1 },
       { transfer_raw = t2, known_frees = k2,
         compound_rhs = c2, relator_eq = r2,
-        relator_eq_raw = rw2 } ) =
+        relator_eq_raw = rw2, relator_domain = rd2 } ) =
     { transfer_raw = Item_Net.merge (t1, t2),
       known_frees = Library.merge (op =) (k1, k2),
       compound_rhs = Net.merge (K true) (c1, c2),
       relator_eq = Item_Net.merge (r1, r2),
-      relator_eq_raw = Item_Net.merge (rw1, rw2) }
+      relator_eq_raw = Item_Net.merge (rw1, rw2),
+      relator_domain = Item_Net.merge (rd1, rd2) }
 )
+
+fun get_transfer_raw ctxt = ctxt
+  |> (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)
+
+fun get_compound_rhs ctxt = ctxt
+  |> (#compound_rhs 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
 

   |> map (Thm.symmetric o safe_mk_meta_eq)
 
 fun get_relator_eq_raw ctxt = ctxt
   |> (Item_Net.content o #relator_eq_raw o Data.get o Context.Proof)
 
-fun get_transfer_raw ctxt = ctxt
-  |> (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)
-
-fun get_compound_rhs ctxt = ctxt
-  |> (#compound_rhs o Data.get o Context.Proof)
-
-fun map_data f1 f2 f3 f4 f5
-  { transfer_raw, known_frees, compound_rhs, relator_eq, relator_eq_raw } =
+fun get_relator_domain ctxt = ctxt
+  |> (Item_Net.content o #relator_domain o Data.get o Context.Proof)
+
+fun map_data f1 f2 f3 f4 f5 f6
+  { transfer_raw, known_frees, compound_rhs, relator_eq, relator_eq_raw, relator_domain } =
   { transfer_raw = f1 transfer_raw,
     known_frees = f2 known_frees,
     compound_rhs = f3 compound_rhs,
     relator_eq = f4 relator_eq,
-    relator_eq_raw = f5 relator_eq_raw }
-
-fun map_transfer_raw f = map_data f I I I I
-fun map_known_frees f = map_data I f I I I
-fun map_compound_rhs f = map_data I I f I I
-fun map_relator_eq f = map_data I I I f I
-fun map_relator_eq_raw f = map_data I I I I f
+    relator_eq_raw = f5 relator_eq_raw,
+    relator_domain = f6 relator_domain }
+
+fun map_transfer_raw f = map_data f I I I I I
+fun map_known_frees f = map_data I f I I I I
+fun map_compound_rhs f = map_data I I f I I I
+fun map_relator_eq f = map_data I I I f I I
+fun map_relator_eq_raw f = map_data I I I I f I
+fun map_relator_domain f = map_data I I I I I f
 
 fun add_transfer_thm thm = Data.map
   (map_transfer_raw (Item_Net.update thm) o
    map_compound_rhs
      (case HOLogic.dest_Trueprop (Thm.concl_of thm) of
-        _ $ _ $ (rhs as (_ $ _)) => Net.insert_term (K true) (rhs, ())
+        (Const (@{const_name Rel}, _)) $ _ $ _ $ (rhs as (_ $ _)) => Net.insert_term (K true) (rhs, ())
       | _ => I) o
    map_known_frees (Term.add_frees (Thm.concl_of thm)))
 
 fun del_transfer_thm thm = Data.map (map_transfer_raw (Item_Net.remove thm))
 

   let val (cT, cT') = dest_funcT (Thm.ctyp_of_term ct)
       val (cU, _) = dest_funcT cT'
   in Drule.instantiate' [SOME cT, SOME cU] [SOME ct] Rel_rule end
 
 (* Conversion to preprocess a transfer rule *)
-fun strip_args n = funpow n (fst o dest_comb)
-
 fun safe_Rel_conv ct =
-  let
-    val head = ct |> term_of |> HOLogic.dest_Trueprop |> strip_args 2
-    fun is_known (Const (s, _)) = (s = @{const_name DOM})
-      | is_known _ = false
-  in
-    if not (is_known head)
-      then HOLogic.Trueprop_conv (Conv.fun_conv (Conv.fun_conv Rel_conv)) ct
-    else Conv.all_conv ct
-  end
-  handle TERM _ => Conv.all_conv ct
-;
+  Conv.try_conv (HOLogic.Trueprop_conv (Conv.fun_conv (Conv.fun_conv Rel_conv))) ct
 
 fun prep_conv ct = (
       Conv.implies_conv safe_Rel_conv prep_conv
       else_conv
       safe_Rel_conv

 
 fun abstract_equalities_relator_eq rel_eq_thm =
   gen_abstract_equalities (fn x => (x, I))
     (rel_eq_thm RS @{thm is_equality_def [THEN iffD2]})
 
+fun abstract_equalities_domain thm =
+  let
+    fun dest prop =
+      let
+        val prems = Logic.strip_imp_prems prop
+        val concl = HOLogic.dest_Trueprop (Logic.strip_imp_concl prop)
+        val ((dom, x), y) = apfst Term.dest_comb (Term.dest_comb concl)
+      in
+        (x $ y, fn comb' =>
+          let 
+            val (x', y') = dest_comb comb'
+          in
+            Logic.list_implies (prems, HOLogic.mk_Trueprop (dom $ x' $ y'))
+          end)
+      end
+  in
+    gen_abstract_equalities dest thm
+  end 
+
+
+(** Replacing explicit Domainp predicates with Domainp assumptions **)
+
+fun mk_Domainp_assm (T, R) =
+  HOLogic.mk_eq ((Const (@{const_name Domainp}, Term.fastype_of T --> Term.fastype_of R) $ T), R)
+
+val Domainp_lemma =
+  @{lemma "(!!R. Domainp T = R ==> PROP (P R)) == PROP (P (Domainp T))"
+    by (rule, drule meta_spec,
+      erule meta_mp, rule refl, simp)}
+
+fun fold_Domainp f (t as Const (@{const_name Domainp},_) $ (Var (_,_))) = f t
+  | fold_Domainp f (t $ u) = fold_Domainp f t #> fold_Domainp f u
+  | fold_Domainp f (Abs (_, _, t)) = fold_Domainp f t
+  | fold_Domainp _ _ = I
+
+fun subst_terms tab t = 
+  let
+    val t' = Termtab.lookup tab t
+  in
+    case t' of
+      SOME t' => t'
+      | NONE => 
+        (case t of
+          u $ v => (subst_terms tab u) $ (subst_terms tab v)
+          | Abs (a, T, t) => Abs (a, T, subst_terms tab t)
+          | t => t)
+  end
+
+fun gen_abstract_domains (dest : term -> term * (term -> term)) thm =
+  let
+    val thy = Thm.theory_of_thm thm
+    val prop = Thm.prop_of thm
+    val (t, mk_prop') = dest prop
+    val Domainp_tms = rev (fold_Domainp (fn t => insert op= t) t [])
+    val Domainp_Ts = map (snd o dest_funT o snd o dest_Const o fst o dest_comb) Domainp_tms
+    val used = Term.add_free_names t []
+    val rels = map (snd o dest_comb) Domainp_tms
+    val rel_names = map (fst o fst o dest_Var) rels
+    val names = map (fn name => ("D" ^ name)) rel_names |> Name.variant_list used
+    val frees = map Free (names ~~ Domainp_Ts)
+    val prems = map (HOLogic.mk_Trueprop o mk_Domainp_assm) (rels ~~ frees);
+    val t' = subst_terms (fold Termtab.update (Domainp_tms ~~ frees) Termtab.empty) t
+    val prop1 = fold Logic.all frees (Logic.list_implies (prems, mk_prop' t'))
+    val prop2 = Logic.list_rename_params (rev names) prop1
+    val cprop = Thm.cterm_of thy prop2
+    val equal_thm = Raw_Simplifier.rewrite false [Domainp_lemma] cprop
+    fun forall_elim thm = Thm.forall_elim_vars (Thm.maxidx_of thm + 1) thm;
+  in
+    forall_elim (thm COMP (equal_thm COMP @{thm equal_elim_rule2}))
+  end
+    handle TERM _ => thm
+
+fun abstract_domains_transfer thm =
+  let
+    fun dest prop =
+      let
+        val prems = Logic.strip_imp_prems prop
+        val concl = HOLogic.dest_Trueprop (Logic.strip_imp_concl prop)
+        val ((rel, x), y) = apfst Term.dest_comb (Term.dest_comb concl)
+      in
+        (x, fn x' =>
+          Logic.list_implies (prems, HOLogic.mk_Trueprop (rel $ x' $ y)))
+      end
+  in
+    gen_abstract_domains dest thm
+  end
+
+fun detect_transfer_rules thm =
+  let
+    fun is_transfer_rule tm = case (HOLogic.dest_Trueprop tm) of
+      (Const (@{const_name HOL.eq}, _)) $ ((Const (@{const_name Domainp}, _)) $ _) $ _ => false
+      | _ $ _ $ _ => true
+      | _ => false
+    fun safe_transfer_rule_conv ctm =
+      if is_transfer_rule (term_of ctm) then safe_Rel_conv ctm else Conv.all_conv ctm
+  in
+    Conv.fconv_rule (Conv.prems_conv ~1 safe_transfer_rule_conv) thm
+  end
+
+(** Adding transfer domain rules **)
+
+fun add_transfer_domain_thm thm = 
+  (add_transfer_thm o abstract_equalities_domain o detect_transfer_rules) thm
+
+fun del_transfer_domain_thm thm = 
+  (del_transfer_thm o abstract_equalities_domain o detect_transfer_rules) thm
 
 (** Transfer proof method **)
 
 val post_simps =
   @{thms transfer_forall_eq [symmetric]

 val transfer_prover_method : (Proof.context -> Method.method) context_parser =
   Scan.succeed (fn ctxt => SIMPLE_METHOD' (transfer_prover_tac ctxt))
 
 (* Attribute for transfer rules *)
 
-val prep_rule = abstract_equalities_transfer o Conv.fconv_rule prep_conv
+val prep_rule = abstract_domains_transfer o abstract_equalities_transfer o Conv.fconv_rule prep_conv
 
 val transfer_add =
   Thm.declaration_attribute (add_transfer_thm o prep_rule)
 
 val transfer_del =
   Thm.declaration_attribute (del_transfer_thm o prep_rule)
 
 val transfer_attribute =
   Attrib.add_del transfer_add transfer_del
+
+(* Attributes for transfer domain rules *)
+
+val transfer_domain_add = Thm.declaration_attribute add_transfer_domain_thm
+
+val transfer_domain_del = Thm.declaration_attribute del_transfer_domain_thm
+
+val transfer_domain_attribute =
+  Attrib.add_del transfer_domain_add transfer_domain_del
 
 (* Theory setup *)
 
 val relator_eq_setup =
   let

   in
     Attrib.setup name (Attrib.add_del add del) text
     #> Global_Theory.add_thms_dynamic (name, content)
   end
 
+val relator_domain_setup =
+  let
+    val name = @{binding relator_domain}
+    fun add_thm thm = Data.map (map_relator_domain (Item_Net.update thm))
+      #> add_transfer_domain_thm thm
+    fun del_thm thm = Data.map (map_relator_domain (Item_Net.remove thm))
+      #> del_transfer_domain_thm thm
+    val add = Thm.declaration_attribute add_thm
+    val del = Thm.declaration_attribute del_thm
+    val text = "declaration of relator domain rule (used by transfer method)"
+    val content = Item_Net.content o #relator_domain o Data.get
+  in
+    Attrib.setup name (Attrib.add_del add del) text
+    #> Global_Theory.add_thms_dynamic (name, content)
+  end
+
+
 val setup =
   relator_eq_setup
+  #> relator_domain_setup
   #> Attrib.setup @{binding transfer_rule} transfer_attribute
      "transfer rule for transfer method"
   #> Global_Theory.add_thms_dynamic
      (@{binding transfer_raw}, Item_Net.content o #transfer_raw o Data.get)
+  #> Attrib.setup @{binding transfer_domain_rule} transfer_domain_attribute
+     "transfer domain rule for transfer method"
   #> Global_Theory.add_thms_dynamic
      (@{binding relator_eq_raw}, Item_Net.content o #relator_eq_raw o Data.get)
   #> Method.setup @{binding transfer} (transfer_method true)
      "generic theorem transfer method"
   #> Method.setup @{binding transfer'} (transfer_method false)