src/HOL/Tools/transfer.ML
author wenzelm
Sat Mar 22 18:19:57 2014 +0100 (2014-03-22)
changeset 56254 a2dd9200854d
parent 55945 e96383acecf9
child 56520 3373f5d1e074
permissions -rw-r--r--
more antiquotations;
     1 (*  Title:      HOL/Tools/transfer.ML
     2     Author:     Brian Huffman, TU Muenchen
     3     Author:     Ondrej Kuncar, TU Muenchen
     4 
     5 Generic theorem transfer method.
     6 *)
     7 
     8 signature TRANSFER =
     9 sig
    10   val bottom_rewr_conv: thm list -> conv
    11   val top_rewr_conv: thm list -> conv
    12 
    13   val prep_conv: conv
    14   val get_transfer_raw: Proof.context -> thm list
    15   val get_relator_eq_item_net: Proof.context -> thm Item_Net.T
    16   val get_relator_eq: Proof.context -> thm list
    17   val get_sym_relator_eq: Proof.context -> thm list
    18   val get_relator_eq_raw: Proof.context -> thm list
    19   val get_relator_domain: Proof.context -> thm list
    20   val get_compound_lhs: Proof.context -> (term * thm) Item_Net.T
    21   val get_compound_rhs: Proof.context -> (term * thm) Item_Net.T
    22   val transfer_add: attribute
    23   val transfer_del: attribute
    24   val transfer_raw_add: thm -> Context.generic -> Context.generic
    25   val transfer_raw_del: thm -> Context.generic -> Context.generic
    26   val transferred_attribute: thm list -> attribute
    27   val untransferred_attribute: thm list -> attribute
    28   val prep_transfer_domain_thm: Proof.context -> thm -> thm
    29   val transfer_domain_add: attribute
    30   val transfer_domain_del: attribute
    31   val transfer_rule_of_term: Proof.context -> bool -> term -> thm
    32   val transfer_rule_of_lhs: Proof.context -> term -> thm
    33   val eq_tac: Proof.context -> int -> tactic
    34   val transfer_step_tac: Proof.context -> int -> tactic
    35   val transfer_tac: bool -> Proof.context -> int -> tactic
    36   val transfer_prover_tac: Proof.context -> int -> tactic
    37   val gen_frees_tac: (string * typ) list -> Proof.context -> int -> tactic
    38   val setup: theory -> theory
    39 end
    40 
    41 structure Transfer : TRANSFER =
    42 struct
    43 
    44 (** Theory Data **)
    45 
    46 val compound_xhs_empty_net = Item_Net.init (Thm.eq_thm_prop o pairself snd) (single o fst);
    47 val rewr_rules = Item_Net.init Thm.eq_thm_prop (single o fst o HOLogic.dest_eq 
    48   o HOLogic.dest_Trueprop o Thm.concl_of);
    49 
    50 structure Data = Generic_Data
    51 (
    52   type T =
    53     { transfer_raw : thm Item_Net.T,
    54       known_frees : (string * typ) list,
    55       compound_lhs : (term * thm) Item_Net.T,
    56       compound_rhs : (term * thm) Item_Net.T,
    57       relator_eq : thm Item_Net.T,
    58       relator_eq_raw : thm Item_Net.T,
    59       relator_domain : thm Item_Net.T }
    60   val empty =
    61     { transfer_raw = Thm.intro_rules,
    62       known_frees = [],
    63       compound_lhs = compound_xhs_empty_net,
    64       compound_rhs = compound_xhs_empty_net,
    65       relator_eq = rewr_rules,
    66       relator_eq_raw = Thm.full_rules,
    67       relator_domain = Thm.full_rules }
    68   val extend = I
    69   fun merge
    70     ( { transfer_raw = t1, known_frees = k1,
    71         compound_lhs = l1,
    72         compound_rhs = c1, relator_eq = r1,
    73         relator_eq_raw = rw1, relator_domain = rd1 },
    74       { transfer_raw = t2, known_frees = k2,
    75         compound_lhs = l2,
    76         compound_rhs = c2, relator_eq = r2,
    77         relator_eq_raw = rw2, relator_domain = rd2 } ) =
    78     { transfer_raw = Item_Net.merge (t1, t2),
    79       known_frees = Library.merge (op =) (k1, k2),
    80       compound_lhs = Item_Net.merge (l1, l2),
    81       compound_rhs = Item_Net.merge (c1, c2),
    82       relator_eq = Item_Net.merge (r1, r2),
    83       relator_eq_raw = Item_Net.merge (rw1, rw2),
    84       relator_domain = Item_Net.merge (rd1, rd2) }
    85 )
    86 
    87 fun get_transfer_raw ctxt = ctxt
    88   |> (Item_Net.content o #transfer_raw o Data.get o Context.Proof)
    89 
    90 fun get_known_frees ctxt = ctxt
    91   |> (#known_frees o Data.get o Context.Proof)
    92 
    93 fun get_compound_lhs ctxt = ctxt
    94   |> (#compound_lhs o Data.get o Context.Proof)
    95 
    96 fun get_compound_rhs ctxt = ctxt
    97   |> (#compound_rhs o Data.get o Context.Proof)
    98 
    99 fun get_relator_eq_item_net ctxt = (#relator_eq o Data.get o Context.Proof) ctxt
   100 
   101 fun get_relator_eq ctxt = ctxt
   102   |> (Item_Net.content o #relator_eq o Data.get o Context.Proof)
   103   |> map safe_mk_meta_eq
   104 
   105 fun get_sym_relator_eq ctxt = ctxt
   106   |> (Item_Net.content o #relator_eq o Data.get o Context.Proof)
   107   |> map (Thm.symmetric o safe_mk_meta_eq)
   108 
   109 fun get_relator_eq_raw ctxt = ctxt
   110   |> (Item_Net.content o #relator_eq_raw o Data.get o Context.Proof)
   111 
   112 fun get_relator_domain ctxt = ctxt
   113   |> (Item_Net.content o #relator_domain o Data.get o Context.Proof)
   114 
   115 fun map_data f1 f2 f3 f4 f5 f6 f7
   116   { transfer_raw, known_frees, compound_lhs, compound_rhs,
   117     relator_eq, relator_eq_raw, relator_domain } =
   118   { transfer_raw = f1 transfer_raw,
   119     known_frees = f2 known_frees,
   120     compound_lhs = f3 compound_lhs,
   121     compound_rhs = f4 compound_rhs,
   122     relator_eq = f5 relator_eq,
   123     relator_eq_raw = f6 relator_eq_raw,
   124     relator_domain = f7 relator_domain }
   125 
   126 fun map_transfer_raw   f = map_data f I I I I I I
   127 fun map_known_frees    f = map_data I f I I I I I
   128 fun map_compound_lhs   f = map_data I I f I I I I
   129 fun map_compound_rhs   f = map_data I I I f I I I
   130 fun map_relator_eq     f = map_data I I I I f I I
   131 fun map_relator_eq_raw f = map_data I I I I I f I
   132 fun map_relator_domain f = map_data I I I I I I f
   133 
   134 fun add_transfer_thm thm = Data.map
   135   (map_transfer_raw (Item_Net.update thm) o
   136    map_compound_lhs
   137      (case HOLogic.dest_Trueprop (Thm.concl_of thm) of
   138         Const (@{const_name Rel}, _) $ _ $ (lhs as (_ $ _)) $ _ =>
   139           Item_Net.update (lhs, thm)
   140       | _ => I) o
   141    map_compound_rhs
   142      (case HOLogic.dest_Trueprop (Thm.concl_of thm) of
   143         Const (@{const_name Rel}, _) $ _ $ _ $ (rhs as (_ $ _)) =>
   144           Item_Net.update (rhs, thm)
   145       | _ => I) o
   146    map_known_frees (Term.add_frees (Thm.concl_of thm)))
   147 
   148 fun del_transfer_thm thm = Data.map 
   149   (map_transfer_raw (Item_Net.remove thm) o
   150    map_compound_lhs
   151      (case HOLogic.dest_Trueprop (Thm.concl_of thm) of
   152         Const (@{const_name Rel}, _) $ _ $ (lhs as (_ $ _)) $ _ =>
   153           Item_Net.remove (lhs, thm)
   154       | _ => I) o
   155    map_compound_rhs
   156      (case HOLogic.dest_Trueprop (Thm.concl_of thm) of
   157         Const (@{const_name Rel}, _) $ _ $ _ $ (rhs as (_ $ _)) =>
   158           Item_Net.remove (rhs, thm)
   159       | _ => I))
   160 
   161 fun transfer_raw_add thm ctxt = add_transfer_thm thm ctxt
   162 fun transfer_raw_del thm ctxt = del_transfer_thm thm ctxt
   163 
   164 (** Conversions **)
   165 
   166 fun bottom_rewr_conv rewrs = Conv.bottom_conv (K (Conv.try_conv (Conv.rewrs_conv rewrs))) @{context}
   167 fun top_rewr_conv rewrs = Conv.top_conv (K (Conv.try_conv (Conv.rewrs_conv rewrs))) @{context}
   168 
   169 fun transfer_rel_conv conv = 
   170   Conv.concl_conv ~1 (HOLogic.Trueprop_conv (Conv.fun2_conv (Conv.arg_conv conv)))
   171 
   172 val Rel_rule = Thm.symmetric @{thm Rel_def}
   173 
   174 fun dest_funcT cT =
   175   (case Thm.dest_ctyp cT of [T, U] => (T, U)
   176     | _ => raise TYPE ("dest_funcT", [Thm.typ_of cT], []))
   177 
   178 fun Rel_conv ct =
   179   let val (cT, cT') = dest_funcT (Thm.ctyp_of_term ct)
   180       val (cU, _) = dest_funcT cT'
   181   in Drule.instantiate' [SOME cT, SOME cU] [SOME ct] Rel_rule end
   182 
   183 (* Conversion to preprocess a transfer rule *)
   184 fun safe_Rel_conv ct =
   185   Conv.try_conv (HOLogic.Trueprop_conv (Conv.fun_conv (Conv.fun_conv Rel_conv))) ct
   186 
   187 fun prep_conv ct = (
   188       Conv.implies_conv safe_Rel_conv prep_conv
   189       else_conv
   190       safe_Rel_conv
   191       else_conv
   192       Conv.all_conv) ct
   193 
   194 (** Replacing explicit equalities with is_equality premises **)
   195 
   196 fun mk_is_equality t =
   197   Const (@{const_name is_equality}, Term.fastype_of t --> HOLogic.boolT) $ t
   198 
   199 val is_equality_lemma =
   200   @{lemma "(!!R. is_equality R ==> PROP (P R)) == PROP (P (op =))"
   201     by (unfold is_equality_def, rule, drule meta_spec,
   202       erule meta_mp, rule refl, simp)}
   203 
   204 fun gen_abstract_equalities ctxt (dest : term -> term * (term -> term)) thm =
   205   let
   206     val thy = Thm.theory_of_thm thm
   207     val prop = Thm.prop_of thm
   208     val (t, mk_prop') = dest prop
   209     (* Only consider "op =" at non-base types *)
   210     fun is_eq (Const (@{const_name HOL.eq}, Type ("fun", [T, _]))) =
   211         (case T of Type (_, []) => false | _ => true)
   212       | is_eq _ = false
   213     val add_eqs = Term.fold_aterms (fn t => if is_eq t then insert (op =) t else I)
   214     val eq_consts = rev (add_eqs t [])
   215     val eqTs = map (snd o dest_Const) eq_consts
   216     val used = Term.add_free_names prop []
   217     val names = map (K "") eqTs |> Name.variant_list used
   218     val frees = map Free (names ~~ eqTs)
   219     val prems = map (HOLogic.mk_Trueprop o mk_is_equality) frees
   220     val prop1 = mk_prop' (Term.subst_atomic (eq_consts ~~ frees) t)
   221     val prop2 = fold Logic.all frees (Logic.list_implies (prems, prop1))
   222     val cprop = Thm.cterm_of thy prop2
   223     val equal_thm = Raw_Simplifier.rewrite ctxt false [is_equality_lemma] cprop
   224     fun forall_elim thm = Thm.forall_elim_vars (Thm.maxidx_of thm + 1) thm
   225   in
   226     forall_elim (thm COMP (equal_thm COMP @{thm equal_elim_rule2}))
   227   end
   228     handle TERM _ => thm
   229 
   230 fun abstract_equalities_transfer ctxt thm =
   231   let
   232     fun dest prop =
   233       let
   234         val prems = Logic.strip_imp_prems prop
   235         val concl = HOLogic.dest_Trueprop (Logic.strip_imp_concl prop)
   236         val ((rel, x), y) = apfst Term.dest_comb (Term.dest_comb concl)
   237       in
   238         (rel, fn rel' =>
   239           Logic.list_implies (prems, HOLogic.mk_Trueprop (rel' $ x $ y)))
   240       end
   241     val contracted_eq_thm = 
   242       Conv.fconv_rule (transfer_rel_conv (bottom_rewr_conv (get_relator_eq ctxt))) thm
   243       handle CTERM _ => thm
   244   in
   245     gen_abstract_equalities ctxt dest contracted_eq_thm
   246   end
   247 
   248 fun abstract_equalities_relator_eq ctxt rel_eq_thm =
   249   gen_abstract_equalities ctxt (fn x => (x, I))
   250     (rel_eq_thm RS @{thm is_equality_def [THEN iffD2]})
   251 
   252 fun abstract_equalities_domain ctxt thm =
   253   let
   254     fun dest prop =
   255       let
   256         val prems = Logic.strip_imp_prems prop
   257         val concl = HOLogic.dest_Trueprop (Logic.strip_imp_concl prop)
   258         val ((eq, dom), y) = apfst Term.dest_comb (Term.dest_comb concl)
   259       in
   260         (dom, fn dom' => Logic.list_implies (prems, HOLogic.mk_Trueprop (eq $ dom' $ y)))
   261       end
   262     fun transfer_rel_conv conv = 
   263       Conv.concl_conv ~1 (HOLogic.Trueprop_conv (Conv.arg1_conv (Conv.arg_conv conv)))
   264     val contracted_eq_thm = 
   265       Conv.fconv_rule (transfer_rel_conv (bottom_rewr_conv (get_relator_eq ctxt))) thm
   266   in
   267     gen_abstract_equalities ctxt dest contracted_eq_thm
   268   end 
   269 
   270 
   271 (** Replacing explicit Domainp predicates with Domainp assumptions **)
   272 
   273 fun mk_Domainp_assm (T, R) =
   274   HOLogic.mk_eq ((Const (@{const_name Domainp}, Term.fastype_of T --> Term.fastype_of R) $ T), R)
   275 
   276 val Domainp_lemma =
   277   @{lemma "(!!R. Domainp T = R ==> PROP (P R)) == PROP (P (Domainp T))"
   278     by (rule, drule meta_spec,
   279       erule meta_mp, rule refl, simp)}
   280 
   281 fun fold_Domainp f (t as Const (@{const_name Domainp},_) $ (Var (_,_))) = f t
   282   | fold_Domainp f (t $ u) = fold_Domainp f t #> fold_Domainp f u
   283   | fold_Domainp f (Abs (_, _, t)) = fold_Domainp f t
   284   | fold_Domainp _ _ = I
   285 
   286 fun subst_terms tab t = 
   287   let
   288     val t' = Termtab.lookup tab t
   289   in
   290     case t' of
   291       SOME t' => t'
   292       | NONE => 
   293         (case t of
   294           u $ v => (subst_terms tab u) $ (subst_terms tab v)
   295           | Abs (a, T, t) => Abs (a, T, subst_terms tab t)
   296           | t => t)
   297   end
   298 
   299 fun gen_abstract_domains ctxt (dest : term -> term * (term -> term)) thm =
   300   let
   301     val thy = Thm.theory_of_thm thm
   302     val prop = Thm.prop_of thm
   303     val (t, mk_prop') = dest prop
   304     val Domainp_tms = rev (fold_Domainp (fn t => insert op= t) t [])
   305     val Domainp_Ts = map (snd o dest_funT o snd o dest_Const o fst o dest_comb) Domainp_tms
   306     val used = Term.add_free_names t []
   307     val rels = map (snd o dest_comb) Domainp_tms
   308     val rel_names = map (fst o fst o dest_Var) rels
   309     val names = map (fn name => ("D" ^ name)) rel_names |> Name.variant_list used
   310     val frees = map Free (names ~~ Domainp_Ts)
   311     val prems = map (HOLogic.mk_Trueprop o mk_Domainp_assm) (rels ~~ frees);
   312     val t' = subst_terms (fold Termtab.update (Domainp_tms ~~ frees) Termtab.empty) t
   313     val prop1 = fold Logic.all frees (Logic.list_implies (prems, mk_prop' t'))
   314     val prop2 = Logic.list_rename_params (rev names) prop1
   315     val cprop = Thm.cterm_of thy prop2
   316     val equal_thm = Raw_Simplifier.rewrite ctxt false [Domainp_lemma] cprop
   317     fun forall_elim thm = Thm.forall_elim_vars (Thm.maxidx_of thm + 1) thm;
   318   in
   319     forall_elim (thm COMP (equal_thm COMP @{thm equal_elim_rule2}))
   320   end
   321     handle TERM _ => thm
   322 
   323 fun abstract_domains_transfer ctxt thm =
   324   let
   325     fun dest prop =
   326       let
   327         val prems = Logic.strip_imp_prems prop
   328         val concl = HOLogic.dest_Trueprop (Logic.strip_imp_concl prop)
   329         val ((rel, x), y) = apfst Term.dest_comb (Term.dest_comb concl)
   330       in
   331         (x, fn x' =>
   332           Logic.list_implies (prems, HOLogic.mk_Trueprop (rel $ x' $ y)))
   333       end
   334   in
   335     gen_abstract_domains ctxt dest thm
   336   end
   337 
   338 fun detect_transfer_rules thm =
   339   let
   340     fun is_transfer_rule tm = case (HOLogic.dest_Trueprop tm) of
   341       (Const (@{const_name HOL.eq}, _)) $ ((Const (@{const_name Domainp}, _)) $ _) $ _ => false
   342       | _ $ _ $ _ => true
   343       | _ => false
   344     fun safe_transfer_rule_conv ctm =
   345       if is_transfer_rule (term_of ctm) then safe_Rel_conv ctm else Conv.all_conv ctm
   346   in
   347     Conv.fconv_rule (Conv.prems_conv ~1 safe_transfer_rule_conv) thm
   348   end
   349 
   350 (** Adding transfer domain rules **)
   351 
   352 fun prep_transfer_domain_thm ctxt thm = 
   353   (abstract_equalities_domain ctxt o detect_transfer_rules) thm 
   354 
   355 fun add_transfer_domain_thm thm ctxt = (add_transfer_thm o 
   356   prep_transfer_domain_thm (Context.proof_of ctxt)) thm ctxt
   357 
   358 fun del_transfer_domain_thm thm ctxt = (del_transfer_thm o 
   359   prep_transfer_domain_thm (Context.proof_of ctxt)) thm ctxt
   360 
   361 (** Transfer proof method **)
   362 
   363 val post_simps =
   364   @{thms transfer_forall_eq [symmetric]
   365     transfer_implies_eq [symmetric] transfer_bforall_unfold}
   366 
   367 fun gen_frees_tac keepers ctxt = SUBGOAL (fn (t, i) =>
   368   let
   369     val keepers = keepers @ get_known_frees ctxt
   370     val vs = rev (Term.add_frees t [])
   371     val vs' = filter_out (member (op =) keepers) vs
   372   in
   373     Induct.arbitrary_tac ctxt 0 vs' i
   374   end)
   375 
   376 fun mk_relT (T, U) = T --> U --> HOLogic.boolT
   377 
   378 fun mk_Rel t =
   379   let val T = fastype_of t
   380   in Const (@{const_name Transfer.Rel}, T --> T) $ t end
   381 
   382 fun transfer_rule_of_terms (prj : typ * typ -> typ) ctxt tab t u =
   383   let
   384     val thy = Proof_Context.theory_of ctxt
   385     (* precondition: prj(T,U) must consist of only TFrees and type "fun" *)
   386     fun rel (T as Type ("fun", [T1, T2])) (U as Type ("fun", [U1, U2])) =
   387         let
   388           val r1 = rel T1 U1
   389           val r2 = rel T2 U2
   390           val rT = fastype_of r1 --> fastype_of r2 --> mk_relT (T, U)
   391         in
   392           Const (@{const_name rel_fun}, rT) $ r1 $ r2
   393         end
   394       | rel T U =
   395         let
   396           val (a, _) = dest_TFree (prj (T, U))
   397         in
   398           Free (the (AList.lookup (op =) tab a), mk_relT (T, U))
   399         end
   400     fun zip _ thms (Bound i) (Bound _) = (nth thms i, [])
   401       | zip ctxt thms (Abs (x, T, t)) (Abs (y, U, u)) =
   402         let
   403           val ([x', y'], ctxt') = Variable.variant_fixes [x, y] ctxt
   404           val prop = mk_Rel (rel T U) $ Free (x', T) $ Free (y', U)
   405           val cprop = Thm.cterm_of thy (HOLogic.mk_Trueprop prop)
   406           val thm0 = Thm.assume cprop
   407           val (thm1, hyps) = zip ctxt' (thm0 :: thms) t u
   408           val ((r1, x), y) = apfst Thm.dest_comb (Thm.dest_comb (Thm.dest_arg cprop))
   409           val r2 = Thm.dest_fun2 (Thm.dest_arg (cprop_of thm1))
   410           val (a1, (b1, _)) = apsnd dest_funcT (dest_funcT (ctyp_of_term r1))
   411           val (a2, (b2, _)) = apsnd dest_funcT (dest_funcT (ctyp_of_term r2))
   412           val tinsts = [SOME a1, SOME b1, SOME a2, SOME b2]
   413           val insts = [SOME (Thm.dest_arg r1), SOME (Thm.dest_arg r2)]
   414           val rule = Drule.instantiate' tinsts insts @{thm Rel_abs}
   415           val thm2 = Thm.forall_intr x (Thm.forall_intr y (Thm.implies_intr cprop thm1))
   416         in
   417           (thm2 COMP rule, hyps)
   418         end
   419       | zip ctxt thms (f $ t) (g $ u) =
   420         let
   421           val (thm1, hyps1) = zip ctxt thms f g
   422           val (thm2, hyps2) = zip ctxt thms t u
   423         in
   424           (thm2 RS (thm1 RS @{thm Rel_app}), hyps1 @ hyps2)
   425         end
   426       | zip _ _ t u =
   427         let
   428           val T = fastype_of t
   429           val U = fastype_of u
   430           val prop = mk_Rel (rel T U) $ t $ u
   431           val cprop = Thm.cterm_of thy (HOLogic.mk_Trueprop prop)
   432         in
   433           (Thm.assume cprop, [cprop])
   434         end
   435     val r = mk_Rel (rel (fastype_of t) (fastype_of u))
   436     val goal = HOLogic.mk_Trueprop (r $ t $ u)
   437     val rename = Thm.trivial (cterm_of thy goal)
   438     val (thm, hyps) = zip ctxt [] t u
   439   in
   440     Drule.implies_intr_list hyps (thm RS rename)
   441   end
   442 
   443 (* create a lambda term of the same shape as the given term *)
   444 fun skeleton (is_atom : term -> bool) ctxt t =
   445   let
   446     fun dummy ctxt =
   447       let
   448         val (c, ctxt) = yield_singleton Variable.variant_fixes "a" ctxt
   449       in
   450         (Free (c, dummyT), ctxt)
   451       end
   452     fun go (Bound i) ctxt = (Bound i, ctxt)
   453       | go (Abs (x, _, t)) ctxt =
   454         let
   455           val (t', ctxt) = go t ctxt
   456         in
   457           (Abs (x, dummyT, t'), ctxt)
   458         end
   459       | go (tu as (t $ u)) ctxt =
   460         if is_atom tu andalso not (Term.is_open tu) then dummy ctxt else
   461         let
   462           val (t', ctxt) = go t ctxt
   463           val (u', ctxt) = go u ctxt
   464         in
   465           (t' $ u', ctxt)
   466         end
   467       | go _ ctxt = dummy ctxt
   468   in
   469     go t ctxt |> fst |> Syntax.check_term ctxt |>
   470       map_types (map_type_tfree (fn (a, _) => TFree (a, @{sort type})))
   471   end
   472 
   473 (** Monotonicity analysis **)
   474 
   475 (* TODO: Put extensible table in theory data *)
   476 val monotab =
   477   Symtab.make
   478     [(@{const_name transfer_implies}, [~1, 1]),
   479      (@{const_name transfer_forall}, [1])(*,
   480      (@{const_name implies}, [~1, 1]),
   481      (@{const_name All}, [1])*)]
   482 
   483 (*
   484 Function bool_insts determines the set of boolean-relation variables
   485 that can be instantiated to implies, rev_implies, or iff.
   486 
   487 Invariants: bool_insts p (t, u) requires that
   488   u :: _ => _ => ... => bool, and
   489   t is a skeleton of u
   490 *)
   491 fun bool_insts p (t, u) =
   492   let
   493     fun strip2 (t1 $ t2, u1 $ u2, tus) =
   494         strip2 (t1, u1, (t2, u2) :: tus)
   495       | strip2 x = x
   496     fun or3 ((a, b, c), (x, y, z)) = (a orelse x, b orelse y, c orelse z)
   497     fun go Ts p (Abs (_, T, t), Abs (_, _, u)) tab = go (T :: Ts) p (t, u) tab
   498       | go Ts p (t, u) tab =
   499         let
   500           val (a, _) = dest_TFree (Term.body_type (Term.fastype_of1 (Ts, t)))
   501           val (_, tf, tus) = strip2 (t, u, [])
   502           val ps_opt = case tf of Const (c, _) => Symtab.lookup monotab c | _ => NONE
   503           val tab1 =
   504             case ps_opt of
   505               SOME ps =>
   506               let
   507                 val ps' = map (fn x => p * x) (take (length tus) ps)
   508               in
   509                 fold I (map2 (go Ts) ps' tus) tab
   510               end
   511             | NONE => tab
   512           val tab2 = Symtab.make [(a, (p >= 0, p <= 0, is_none ps_opt))]
   513         in
   514           Symtab.join (K or3) (tab1, tab2)
   515         end
   516     val tab = go [] p (t, u) Symtab.empty
   517     fun f (a, (true, false, false)) = SOME (a, @{const implies})
   518       | f (a, (false, true, false)) = SOME (a, @{const rev_implies})
   519       | f (a, (true, true, _))      = SOME (a, HOLogic.eq_const HOLogic.boolT)
   520       | f _                         = NONE
   521   in
   522     map_filter f (Symtab.dest tab)
   523   end
   524 
   525 fun retrieve_terms t net = map fst (Item_Net.retrieve net t)
   526   
   527 fun matches_list ctxt term = 
   528   is_some o find_first (fn pat => Pattern.matches (Proof_Context.theory_of ctxt) (pat, term))
   529 
   530 fun transfer_rule_of_term ctxt equiv t : thm =
   531   let
   532     val compound_rhs = get_compound_rhs ctxt
   533     fun is_rhs t = compound_rhs |> retrieve_terms t |> matches_list ctxt t
   534     val s = skeleton is_rhs ctxt t
   535     val frees = map fst (Term.add_frees s [])
   536     val tfrees = map fst (Term.add_tfrees s [])
   537     fun prep a = "R" ^ Library.unprefix "'" a
   538     val (rnames, ctxt') = Variable.variant_fixes (map prep tfrees) ctxt
   539     val tab = tfrees ~~ rnames
   540     fun prep a = the (AList.lookup (op =) tab a)
   541     val thm = transfer_rule_of_terms fst ctxt' tab s t
   542     val binsts = bool_insts (if equiv then 0 else 1) (s, t)
   543     val cbool = @{ctyp bool}
   544     val relT = @{typ "bool => bool => bool"}
   545     val idx = Thm.maxidx_of thm + 1
   546     val thy = Proof_Context.theory_of ctxt
   547     fun tinst (a, _) = (ctyp_of thy (TVar ((a, idx), @{sort type})), cbool)
   548     fun inst (a, t) = (cterm_of thy (Var (Name.clean_index (prep a, idx), relT)), cterm_of thy t)
   549   in
   550     thm
   551       |> Thm.generalize (tfrees, rnames @ frees) idx
   552       |> Thm.instantiate (map tinst binsts, map inst binsts)
   553   end
   554 
   555 fun transfer_rule_of_lhs ctxt t : thm =
   556   let
   557     val compound_lhs = get_compound_lhs ctxt
   558     fun is_lhs t = compound_lhs |> retrieve_terms t |> matches_list ctxt t
   559     val s = skeleton is_lhs ctxt t
   560     val frees = map fst (Term.add_frees s [])
   561     val tfrees = map fst (Term.add_tfrees s [])
   562     fun prep a = "R" ^ Library.unprefix "'" a
   563     val (rnames, ctxt') = Variable.variant_fixes (map prep tfrees) ctxt
   564     val tab = tfrees ~~ rnames
   565     fun prep a = the (AList.lookup (op =) tab a)
   566     val thm = transfer_rule_of_terms snd ctxt' tab t s
   567     val binsts = bool_insts 1 (s, t)
   568     val cbool = @{ctyp bool}
   569     val relT = @{typ "bool => bool => bool"}
   570     val idx = Thm.maxidx_of thm + 1
   571     val thy = Proof_Context.theory_of ctxt
   572     fun tinst (a, _) = (ctyp_of thy (TVar ((a, idx), @{sort type})), cbool)
   573     fun inst (a, t) = (cterm_of thy (Var (Name.clean_index (prep a, idx), relT)), cterm_of thy t)
   574   in
   575     thm
   576       |> Thm.generalize (tfrees, rnames @ frees) idx
   577       |> Thm.instantiate (map tinst binsts, map inst binsts)
   578   end
   579 
   580 fun eq_rules_tac eq_rules = TRY o REPEAT_ALL_NEW (resolve_tac eq_rules) 
   581   THEN_ALL_NEW rtac @{thm is_equality_eq}
   582 
   583 fun eq_tac ctxt = eq_rules_tac (get_relator_eq_raw ctxt)
   584 
   585 fun transfer_step_tac ctxt = (REPEAT_ALL_NEW (resolve_tac (get_transfer_raw ctxt)) 
   586   THEN_ALL_NEW (DETERM o eq_rules_tac (get_relator_eq_raw ctxt)))
   587 
   588 fun transfer_tac equiv ctxt i =
   589   let
   590     val pre_simps = @{thms transfer_forall_eq transfer_implies_eq}
   591     val start_rule =
   592       if equiv then @{thm transfer_start} else @{thm transfer_start'}
   593     val rules = get_transfer_raw ctxt
   594     val eq_rules = get_relator_eq_raw ctxt
   595     (* allow unsolved subgoals only for standard transfer method, not for transfer' *)
   596     val end_tac = if equiv then K all_tac else K no_tac
   597     val err_msg = "Transfer failed to convert goal to an object-logic formula"
   598     fun main_tac (t, i) =
   599       rtac start_rule i THEN
   600       (rtac (transfer_rule_of_term ctxt equiv (HOLogic.dest_Trueprop t))
   601         THEN_ALL_NEW
   602           (SOLVED' (REPEAT_ALL_NEW (resolve_tac rules) THEN_ALL_NEW (DETERM o eq_rules_tac eq_rules))
   603             ORELSE' end_tac)) (i + 1)
   604         handle TERM (_, ts) => raise TERM (err_msg, ts)
   605   in
   606     EVERY
   607       [rewrite_goal_tac ctxt pre_simps i THEN
   608        SUBGOAL main_tac i,
   609        (* FIXME: rewrite_goal_tac does unwanted eta-contraction *)
   610        rewrite_goal_tac ctxt post_simps i,
   611        Goal.norm_hhf_tac ctxt i]
   612   end
   613 
   614 fun transfer_prover_tac ctxt = SUBGOAL (fn (t, i) =>
   615   let
   616     val rhs = (snd o Term.dest_comb o HOLogic.dest_Trueprop) t
   617     val rule1 = transfer_rule_of_term ctxt false rhs
   618     val rules = get_transfer_raw ctxt
   619     val eq_rules = get_relator_eq_raw ctxt
   620     val expand_eq_in_rel = transfer_rel_conv (top_rewr_conv [@{thm rel_fun_eq[symmetric,THEN eq_reflection]}])
   621   in
   622     EVERY
   623       [CONVERSION prep_conv i,
   624        rtac @{thm transfer_prover_start} i,
   625        ((rtac rule1 ORELSE' (CONVERSION expand_eq_in_rel THEN' rtac rule1))
   626         THEN_ALL_NEW
   627          (REPEAT_ALL_NEW (resolve_tac rules) THEN_ALL_NEW (DETERM o eq_rules_tac eq_rules))) (i+1),
   628        rtac @{thm refl} i]
   629   end)
   630 
   631 (** Transfer attribute **)
   632 
   633 fun transferred ctxt extra_rules thm =
   634   let
   635     val start_rule = @{thm transfer_start}
   636     val start_rule' = @{thm transfer_start'}
   637     val rules = extra_rules @ get_transfer_raw ctxt
   638     val eq_rules = get_relator_eq_raw ctxt
   639     val err_msg = "Transfer failed to convert goal to an object-logic formula"
   640     val pre_simps = @{thms transfer_forall_eq transfer_implies_eq}
   641     val thm1 = Drule.forall_intr_vars thm
   642     val instT = rev (Term.add_tvars (Thm.full_prop_of thm1) [])
   643                 |> map (fn v as ((a, _), S) => (v, TFree (a, S)))
   644     val thm2 = thm1
   645       |> Thm.certify_instantiate (instT, [])
   646       |> Raw_Simplifier.rewrite_rule ctxt pre_simps
   647     val ctxt' = Variable.declare_names (Thm.full_prop_of thm2) ctxt
   648     val t = HOLogic.dest_Trueprop (Thm.concl_of thm2)
   649     val rule = transfer_rule_of_lhs ctxt' t
   650     val tac =
   651       resolve_tac [thm2 RS start_rule', thm2 RS start_rule] 1 THEN
   652       (rtac rule
   653         THEN_ALL_NEW
   654           (SOLVED' (REPEAT_ALL_NEW (resolve_tac rules)
   655             THEN_ALL_NEW (DETERM o eq_rules_tac eq_rules)))) 1
   656         handle TERM (_, ts) => raise TERM (err_msg, ts)
   657     val thm3 = Goal.prove_internal ctxt' [] @{cpat "Trueprop ?P"} (K tac)
   658     val tnames = map (fst o dest_TFree o snd) instT
   659   in
   660     thm3
   661       |> Raw_Simplifier.rewrite_rule ctxt' post_simps
   662       |> Simplifier.norm_hhf ctxt'
   663       |> Drule.generalize (tnames, [])
   664       |> Drule.zero_var_indexes
   665   end
   666 (*
   667     handle THM _ => thm
   668 *)
   669 
   670 fun untransferred ctxt extra_rules thm =
   671   let
   672     val start_rule = @{thm untransfer_start}
   673     val rules = extra_rules @ get_transfer_raw ctxt
   674     val eq_rules = get_relator_eq_raw ctxt
   675     val err_msg = "Transfer failed to convert goal to an object-logic formula"
   676     val pre_simps = @{thms transfer_forall_eq transfer_implies_eq}
   677     val thm1 = Drule.forall_intr_vars thm
   678     val instT = rev (Term.add_tvars (Thm.full_prop_of thm1) [])
   679                 |> map (fn v as ((a, _), S) => (v, TFree (a, S)))
   680     val thm2 = thm1
   681       |> Thm.certify_instantiate (instT, [])
   682       |> Raw_Simplifier.rewrite_rule ctxt pre_simps
   683     val ctxt' = Variable.declare_names (Thm.full_prop_of thm2) ctxt
   684     val t = HOLogic.dest_Trueprop (Thm.concl_of thm2)
   685     val rule = transfer_rule_of_term ctxt' true t
   686     val tac =
   687       rtac (thm2 RS start_rule) 1 THEN
   688       (rtac rule
   689         THEN_ALL_NEW
   690           (SOLVED' (REPEAT_ALL_NEW (resolve_tac rules)
   691             THEN_ALL_NEW (DETERM o eq_rules_tac eq_rules)))) 1
   692         handle TERM (_, ts) => raise TERM (err_msg, ts)
   693     val thm3 = Goal.prove_internal ctxt' [] @{cpat "Trueprop ?P"} (K tac)
   694     val tnames = map (fst o dest_TFree o snd) instT
   695   in
   696     thm3
   697       |> Raw_Simplifier.rewrite_rule ctxt' post_simps
   698       |> Simplifier.norm_hhf ctxt'
   699       |> Drule.generalize (tnames, [])
   700       |> Drule.zero_var_indexes
   701   end
   702 
   703 (** Methods and attributes **)
   704 
   705 val free = Args.context -- Args.term >> (fn (_, Free v) => v | (ctxt, t) =>
   706   error ("Bad free variable: " ^ Syntax.string_of_term ctxt t))
   707 
   708 val fixing = Scan.optional (Scan.lift (Args.$$$ "fixing" -- Args.colon)
   709   |-- Scan.repeat free) []
   710 
   711 fun transfer_method equiv : (Proof.context -> Proof.method) context_parser =
   712   fixing >> (fn vs => fn ctxt =>
   713     SIMPLE_METHOD' (gen_frees_tac vs ctxt THEN' transfer_tac equiv ctxt))
   714 
   715 val transfer_prover_method : (Proof.context -> Proof.method) context_parser =
   716   Scan.succeed (fn ctxt => SIMPLE_METHOD' (transfer_prover_tac ctxt))
   717 
   718 (* Attribute for transfer rules *)
   719 
   720 fun prep_rule ctxt = 
   721   abstract_domains_transfer ctxt o abstract_equalities_transfer ctxt o Conv.fconv_rule prep_conv
   722 
   723 val transfer_add =
   724   Thm.declaration_attribute (fn thm => fn ctxt => 
   725     (add_transfer_thm o prep_rule (Context.proof_of ctxt)) thm ctxt)
   726 
   727 val transfer_del =
   728   Thm.declaration_attribute (fn thm => fn ctxt => 
   729     (del_transfer_thm o prep_rule (Context.proof_of ctxt)) thm ctxt)
   730 
   731 val transfer_attribute =
   732   Attrib.add_del transfer_add transfer_del
   733 
   734 (* Attributes for transfer domain rules *)
   735 
   736 val transfer_domain_add = Thm.declaration_attribute add_transfer_domain_thm
   737 
   738 val transfer_domain_del = Thm.declaration_attribute del_transfer_domain_thm
   739 
   740 val transfer_domain_attribute =
   741   Attrib.add_del transfer_domain_add transfer_domain_del
   742 
   743 (* Attributes for transferred rules *)
   744 
   745 fun transferred_attribute thms = Thm.rule_attribute
   746   (fn context => transferred (Context.proof_of context) thms)
   747 
   748 fun untransferred_attribute thms = Thm.rule_attribute
   749   (fn context => untransferred (Context.proof_of context) thms)
   750 
   751 val transferred_attribute_parser =
   752   Attrib.thms >> transferred_attribute
   753 
   754 val untransferred_attribute_parser =
   755   Attrib.thms >> untransferred_attribute
   756 
   757 (* Theory setup *)
   758 
   759 val relator_eq_setup =
   760   let
   761     val name = @{binding relator_eq}
   762     fun add_thm thm context = context
   763       |> Data.map (map_relator_eq (Item_Net.update thm))
   764       |> Data.map (map_relator_eq_raw
   765           (Item_Net.update (abstract_equalities_relator_eq (Context.proof_of context) thm)))
   766     fun del_thm thm context = context
   767       |> Data.map (map_relator_eq (Item_Net.remove thm))
   768       |> Data.map (map_relator_eq_raw
   769           (Item_Net.remove (abstract_equalities_relator_eq (Context.proof_of context) thm)))
   770     val add = Thm.declaration_attribute add_thm
   771     val del = Thm.declaration_attribute del_thm
   772     val text = "declaration of relator equality rule (used by transfer method)"
   773     val content = Item_Net.content o #relator_eq o Data.get
   774   in
   775     Attrib.setup name (Attrib.add_del add del) text
   776     #> Global_Theory.add_thms_dynamic (name, content)
   777   end
   778 
   779 val relator_domain_setup =
   780   let
   781     val name = @{binding relator_domain}
   782     fun add_thm thm = Data.map (map_relator_domain (Item_Net.update thm))
   783       #> add_transfer_domain_thm thm
   784     fun del_thm thm = Data.map (map_relator_domain (Item_Net.remove thm))
   785       #> del_transfer_domain_thm thm
   786     val add = Thm.declaration_attribute add_thm
   787     val del = Thm.declaration_attribute del_thm
   788     val text = "declaration of relator domain rule (used by transfer method)"
   789     val content = Item_Net.content o #relator_domain o Data.get
   790   in
   791     Attrib.setup name (Attrib.add_del add del) text
   792     #> Global_Theory.add_thms_dynamic (name, content)
   793   end
   794 
   795 
   796 val setup =
   797   relator_eq_setup
   798   #> relator_domain_setup
   799   #> Attrib.setup @{binding transfer_rule} transfer_attribute
   800      "transfer rule for transfer method"
   801   #> Global_Theory.add_thms_dynamic
   802      (@{binding transfer_raw}, Item_Net.content o #transfer_raw o Data.get)
   803   #> Attrib.setup @{binding transfer_domain_rule} transfer_domain_attribute
   804      "transfer domain rule for transfer method"
   805   #> Attrib.setup @{binding transferred} transferred_attribute_parser
   806      "raw theorem transferred to abstract theorem using transfer rules"
   807   #> Attrib.setup @{binding untransferred} untransferred_attribute_parser
   808      "abstract theorem transferred to raw theorem using transfer rules"
   809   #> Global_Theory.add_thms_dynamic
   810      (@{binding relator_eq_raw}, Item_Net.content o #relator_eq_raw o Data.get)
   811   #> Method.setup @{binding transfer} (transfer_method true)
   812      "generic theorem transfer method"
   813   #> Method.setup @{binding transfer'} (transfer_method false)
   814      "generic theorem transfer method"
   815   #> Method.setup @{binding transfer_prover} transfer_prover_method
   816      "for proving transfer rules"
   817 
   818 end