implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
authorhuffman
Sat Jun 08 19:40:19 2013 -0700 (2013-06-08)
changeset 52354acb4f932dd24
parent 52353 dba3d398c322
child 52355 ebd1f6918663
implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
src/HOL/Quotient_Examples/Lift_FSet.thy
src/HOL/Tools/transfer.ML
src/HOL/Transfer.thy
     1.1 --- a/src/HOL/Quotient_Examples/Lift_FSet.thy	Fri Jun 07 22:17:22 2013 -0400
     1.2 +++ b/src/HOL/Quotient_Examples/Lift_FSet.thy	Sat Jun 08 19:40:19 2013 -0700
     1.3 @@ -136,34 +136,22 @@
     1.4    but sometimes more convenient. *}
     1.5  
     1.6  lemma "fmap f (fmap g xs) = fmap (f \<circ> g) xs"
     1.7 -  apply transfer'
     1.8 -  apply (rule map_map)
     1.9 -  done
    1.10 +  using map_map [Transfer.transferred] .
    1.11  
    1.12  lemma "ffilter p (fmap f xs) = fmap f (ffilter (p \<circ> f) xs)"
    1.13 -  apply transfer'
    1.14 -  apply (rule filter_map)
    1.15 -  done
    1.16 +  using filter_map [Transfer.transferred] .
    1.17  
    1.18  lemma "ffilter p (ffilter q xs) = ffilter (\<lambda>x. q x \<and> p x) xs"
    1.19 -  apply transfer'
    1.20 -  apply (rule filter_filter)
    1.21 -  done
    1.22 +  using filter_filter [Transfer.transferred] .
    1.23  
    1.24  lemma "fset (fcons x xs) = insert x (fset xs)"
    1.25 -  apply transfer
    1.26 -  apply (rule set.simps)
    1.27 -  done
    1.28 +  using set.simps(2) [Transfer.transferred] .
    1.29  
    1.30  lemma "fset (fappend xs ys) = fset xs \<union> fset ys"
    1.31 -  apply transfer
    1.32 -  apply (rule set_append)
    1.33 -  done
    1.34 +  using set_append [Transfer.transferred] .
    1.35  
    1.36  lemma "fset (fconcat xss) = (\<Union>xs\<in>fset xss. fset xs)"
    1.37 -  apply transfer
    1.38 -  apply (rule set_concat)
    1.39 -  done
    1.40 +  using set_concat [Transfer.transferred] .
    1.41  
    1.42  lemma "\<forall>x\<in>fset xs. f x = g x \<Longrightarrow> fmap f xs = fmap g xs"
    1.43    apply transfer
    1.44 @@ -176,7 +164,7 @@
    1.45    done
    1.46  
    1.47  lemma "fconcat (fmap (\<lambda>x. fcons x fnil) xs) = xs"
    1.48 -  apply transfer'
    1.49 +  apply transfer
    1.50    apply simp
    1.51    done
    1.52  
    1.53 @@ -184,8 +172,6 @@
    1.54    by (induct xsss, simp_all)
    1.55  
    1.56  lemma "fconcat (fmap fconcat xss) = fconcat (fconcat xss)"
    1.57 -  apply transfer'
    1.58 -  apply (rule concat_map_concat)
    1.59 -  done
    1.60 +  using concat_map_concat [Transfer.transferred] .
    1.61  
    1.62  end
     2.1 --- a/src/HOL/Tools/transfer.ML	Fri Jun 07 22:17:22 2013 -0400
     2.2 +++ b/src/HOL/Tools/transfer.ML	Sat Jun 08 19:40:19 2013 -0700
     2.3 @@ -15,11 +15,14 @@
     2.4    val get_relator_domain: Proof.context -> thm list
     2.5    val transfer_add: attribute
     2.6    val transfer_del: attribute
     2.7 +  val transferred_attribute: thm list -> attribute
     2.8    val transfer_domain_add: attribute
     2.9    val transfer_domain_del: attribute
    2.10 -  val transfer_rule_of_term: Proof.context -> term -> thm
    2.11 +  val transfer_rule_of_term: Proof.context -> bool -> term -> thm
    2.12 +  val transfer_rule_of_lhs: Proof.context -> term -> thm
    2.13    val transfer_tac: bool -> Proof.context -> int -> tactic
    2.14    val transfer_prover_tac: Proof.context -> int -> tactic
    2.15 +  val gen_frees_tac: (string * typ) list -> Proof.context -> int -> tactic
    2.16    val setup: theory -> theory
    2.17  end
    2.18  
    2.19 @@ -33,13 +36,15 @@
    2.20    type T =
    2.21      { transfer_raw : thm Item_Net.T,
    2.22        known_frees : (string * typ) list,
    2.23 +      compound_lhs : unit Net.net,
    2.24        compound_rhs : unit Net.net,
    2.25        relator_eq : thm Item_Net.T,
    2.26        relator_eq_raw : thm Item_Net.T,
    2.27        relator_domain : thm Item_Net.T }
    2.28    val empty =
    2.29 -    { transfer_raw = Thm.full_rules,
    2.30 +    { transfer_raw = Thm.intro_rules,
    2.31        known_frees = [],
    2.32 +      compound_lhs = Net.empty,
    2.33        compound_rhs = Net.empty,
    2.34        relator_eq = Thm.full_rules,
    2.35        relator_eq_raw = Thm.full_rules,
    2.36 @@ -47,13 +52,16 @@
    2.37    val extend = I
    2.38    fun merge
    2.39      ( { transfer_raw = t1, known_frees = k1,
    2.40 +        compound_lhs = l1,
    2.41          compound_rhs = c1, relator_eq = r1,
    2.42          relator_eq_raw = rw1, relator_domain = rd1 },
    2.43        { transfer_raw = t2, known_frees = k2,
    2.44 +        compound_lhs = l2,
    2.45          compound_rhs = c2, relator_eq = r2,
    2.46          relator_eq_raw = rw2, relator_domain = rd2 } ) =
    2.47      { transfer_raw = Item_Net.merge (t1, t2),
    2.48        known_frees = Library.merge (op =) (k1, k2),
    2.49 +      compound_lhs = Net.merge (K true) (l1, l2),
    2.50        compound_rhs = Net.merge (K true) (c1, c2),
    2.51        relator_eq = Item_Net.merge (r1, r2),
    2.52        relator_eq_raw = Item_Net.merge (rw1, rw2),
    2.53 @@ -66,6 +74,9 @@
    2.54  fun get_known_frees ctxt = ctxt
    2.55    |> (#known_frees o Data.get o Context.Proof)
    2.56  
    2.57 +fun get_compound_lhs ctxt = ctxt
    2.58 +  |> (#compound_lhs o Data.get o Context.Proof)
    2.59 +
    2.60  fun get_compound_rhs ctxt = ctxt
    2.61    |> (#compound_rhs o Data.get o Context.Proof)
    2.62  
    2.63 @@ -83,27 +94,36 @@
    2.64  fun get_relator_domain ctxt = ctxt
    2.65    |> (Item_Net.content o #relator_domain o Data.get o Context.Proof)
    2.66  
    2.67 -fun map_data f1 f2 f3 f4 f5 f6
    2.68 -  { transfer_raw, known_frees, compound_rhs, relator_eq, relator_eq_raw, relator_domain } =
    2.69 +fun map_data f1 f2 f3 f4 f5 f6 f7
    2.70 +  { transfer_raw, known_frees, compound_lhs, compound_rhs,
    2.71 +    relator_eq, relator_eq_raw, relator_domain } =
    2.72    { transfer_raw = f1 transfer_raw,
    2.73      known_frees = f2 known_frees,
    2.74 -    compound_rhs = f3 compound_rhs,
    2.75 -    relator_eq = f4 relator_eq,
    2.76 -    relator_eq_raw = f5 relator_eq_raw,
    2.77 -    relator_domain = f6 relator_domain }
    2.78 +    compound_lhs = f3 compound_lhs,
    2.79 +    compound_rhs = f4 compound_rhs,
    2.80 +    relator_eq = f5 relator_eq,
    2.81 +    relator_eq_raw = f6 relator_eq_raw,
    2.82 +    relator_domain = f7 relator_domain }
    2.83  
    2.84 -fun map_transfer_raw f = map_data f I I I I I
    2.85 -fun map_known_frees f = map_data I f I I I I
    2.86 -fun map_compound_rhs f = map_data I I f I I I
    2.87 -fun map_relator_eq f = map_data I I I f I I
    2.88 -fun map_relator_eq_raw f = map_data I I I I f I
    2.89 -fun map_relator_domain f = map_data I I I I I f
    2.90 +fun map_transfer_raw   f = map_data f I I I I I I
    2.91 +fun map_known_frees    f = map_data I f I I I I I
    2.92 +fun map_compound_lhs   f = map_data I I f I I I I
    2.93 +fun map_compound_rhs   f = map_data I I I f I I I
    2.94 +fun map_relator_eq     f = map_data I I I I f I I
    2.95 +fun map_relator_eq_raw f = map_data I I I I I f I
    2.96 +fun map_relator_domain f = map_data I I I I I I f
    2.97  
    2.98  fun add_transfer_thm thm = Data.map
    2.99    (map_transfer_raw (Item_Net.update thm) o
   2.100 +   map_compound_lhs
   2.101 +     (case HOLogic.dest_Trueprop (Thm.concl_of thm) of
   2.102 +        Const (@{const_name Rel}, _) $ _ $ (lhs as (_ $ _)) $ _ =>
   2.103 +          Net.insert_term_safe (K true) (lhs, ())
   2.104 +      | _ => I) o
   2.105     map_compound_rhs
   2.106       (case HOLogic.dest_Trueprop (Thm.concl_of thm) of
   2.107 -        (Const (@{const_name Rel}, _)) $ _ $ _ $ (rhs as (_ $ _)) => Net.insert_term (K true) (rhs, ())
   2.108 +        Const (@{const_name Rel}, _) $ _ $ _ $ (rhs as (_ $ _)) =>
   2.109 +          Net.insert_term_safe (K true) (rhs, ())
   2.110        | _ => I) o
   2.111     map_known_frees (Term.add_frees (Thm.concl_of thm)))
   2.112  
   2.113 @@ -148,8 +168,11 @@
   2.114      val thy = Thm.theory_of_thm thm
   2.115      val prop = Thm.prop_of thm
   2.116      val (t, mk_prop') = dest prop
   2.117 -    val add_eqs = Term.fold_aterms
   2.118 -      (fn t as Const (@{const_name HOL.eq}, _) => insert (op =) t | _ => I)
   2.119 +    (* Only consider "op =" at non-base types *)
   2.120 +    fun is_eq (Const (@{const_name HOL.eq}, Type ("fun", [T, _]))) =
   2.121 +        (case T of Type (_, []) => false | _ => true)
   2.122 +      | is_eq _ = false
   2.123 +    val add_eqs = Term.fold_aterms (fn t => if is_eq t then insert (op =) t else I)
   2.124      val eq_consts = rev (add_eqs t [])
   2.125      val eqTs = map (snd o dest_Const) eq_consts
   2.126      val used = Term.add_free_names prop []
   2.127 @@ -308,13 +331,11 @@
   2.128    let val T = fastype_of t
   2.129    in Const (@{const_name Transfer.Rel}, T --> T) $ t end
   2.130  
   2.131 -fun transfer_rule_of_terms ctxt tab t u =
   2.132 +fun transfer_rule_of_terms (prj : typ * typ -> typ) ctxt tab t u =
   2.133    let
   2.134      val thy = Proof_Context.theory_of ctxt
   2.135 -    (* precondition: T must consist of only TFrees and function space *)
   2.136 -    fun rel (T as TFree (a, _)) U =
   2.137 -          Free (the (AList.lookup (op =) tab a), mk_relT (T, U))
   2.138 -      | rel (T as Type ("fun", [T1, T2])) (U as Type ("fun", [U1, U2])) =
   2.139 +    (* precondition: prj(T,U) must consist of only TFrees and type "fun" *)
   2.140 +    fun rel (T as Type ("fun", [T1, T2])) (U as Type ("fun", [U1, U2])) =
   2.141          let
   2.142            val r1 = rel T1 U1
   2.143            val r2 = rel T2 U2
   2.144 @@ -322,7 +343,12 @@
   2.145          in
   2.146            Const (@{const_name fun_rel}, rT) $ r1 $ r2
   2.147          end
   2.148 -      | rel T U = raise TYPE ("rel", [T, U], [])
   2.149 +      | rel T U =
   2.150 +        let
   2.151 +          val (a, _) = dest_TFree (prj (T, U))
   2.152 +        in
   2.153 +          Free (the (AList.lookup (op =) tab a), mk_relT (T, U))
   2.154 +        end
   2.155      fun zip _ thms (Bound i) (Bound _) = (nth thms i, [])
   2.156        | zip ctxt thms (Abs (x, T, t)) (Abs (y, U, u)) =
   2.157          let
   2.158 @@ -349,15 +375,15 @@
   2.159          in
   2.160            (thm2 RS (thm1 RS @{thm Rel_app}), hyps1 @ hyps2)
   2.161          end
   2.162 -      | zip _ _ (t as Free (_, T)) u =
   2.163 +      | zip _ _ t u =
   2.164          let
   2.165 +          val T = fastype_of t
   2.166            val U = fastype_of u
   2.167            val prop = mk_Rel (rel T U) $ t $ u
   2.168            val cprop = Thm.cterm_of thy (HOLogic.mk_Trueprop prop)
   2.169          in
   2.170            (Thm.assume cprop, [cprop])
   2.171          end
   2.172 -      | zip _ _ t u = raise TERM ("zip_relterm", [t, u])
   2.173      val r = mk_Rel (rel (fastype_of t) (fastype_of u))
   2.174      val goal = HOLogic.mk_Trueprop (r $ t $ u)
   2.175      val rename = Thm.trivial (cterm_of thy goal)
   2.176 @@ -366,42 +392,136 @@
   2.177      Drule.implies_intr_list hyps (thm RS rename)
   2.178    end
   2.179  
   2.180 -fun transfer_rule_of_term ctxt t =
   2.181 +(* create a lambda term of the same shape as the given term *)
   2.182 +fun skeleton (is_atom : term -> bool) ctxt t =
   2.183    let
   2.184 -    val compound_rhs = get_compound_rhs ctxt
   2.185 -    val is_rhs = not o null o Net.unify_term compound_rhs
   2.186      fun dummy ctxt =
   2.187        let
   2.188          val (c, ctxt) = yield_singleton Variable.variant_fixes "a" ctxt
   2.189        in
   2.190          (Free (c, dummyT), ctxt)
   2.191        end
   2.192 -    (* create a lambda term of the same shape as the given term *)
   2.193 -    fun skeleton (Bound i) ctxt = (Bound i, ctxt)
   2.194 -      | skeleton (Abs (x, _, t)) ctxt =
   2.195 +    fun go (Bound i) ctxt = (Bound i, ctxt)
   2.196 +      | go (Abs (x, _, t)) ctxt =
   2.197          let
   2.198 -          val (t', ctxt) = skeleton t ctxt
   2.199 +          val (t', ctxt) = go t ctxt
   2.200          in
   2.201            (Abs (x, dummyT, t'), ctxt)
   2.202          end
   2.203 -      | skeleton (tu as (t $ u)) ctxt =
   2.204 -        if is_rhs tu andalso not (Term.is_open tu) then dummy ctxt else
   2.205 +      | go (tu as (t $ u)) ctxt =
   2.206 +        if is_atom tu andalso not (Term.is_open tu) then dummy ctxt else
   2.207          let
   2.208 -          val (t', ctxt) = skeleton t ctxt
   2.209 -          val (u', ctxt) = skeleton u ctxt
   2.210 +          val (t', ctxt) = go t ctxt
   2.211 +          val (u', ctxt) = go u ctxt
   2.212          in
   2.213            (t' $ u', ctxt)
   2.214          end
   2.215 -      | skeleton _ ctxt = dummy ctxt
   2.216 -    val s = skeleton t ctxt |> fst |> Syntax.check_term ctxt |>
   2.217 +      | go _ ctxt = dummy ctxt
   2.218 +  in
   2.219 +    go t ctxt |> fst |> Syntax.check_term ctxt |>
   2.220        map_types (map_type_tfree (fn (a, _) => TFree (a, HOLogic.typeS)))
   2.221 +  end
   2.222 +
   2.223 +(** Monotonicity analysis **)
   2.224 +
   2.225 +(* TODO: Put extensible table in theory data *)
   2.226 +val monotab =
   2.227 +  Symtab.make
   2.228 +    [(@{const_name transfer_implies}, [~1, 1]),
   2.229 +     (@{const_name transfer_forall}, [1])(*,
   2.230 +     (@{const_name implies}, [~1, 1]),
   2.231 +     (@{const_name All}, [1])*)]
   2.232 +
   2.233 +(*
   2.234 +Function bool_insts determines the set of boolean-relation variables
   2.235 +that can be instantiated to implies, rev_implies, or iff.
   2.236 +
   2.237 +Invariants: bool_insts p (t, u) requires that
   2.238 +  u :: _ => _ => ... => bool, and
   2.239 +  t is a skeleton of u
   2.240 +*)
   2.241 +fun bool_insts p (t, u) =
   2.242 +  let
   2.243 +    fun strip2 (t1 $ t2, u1 $ u2, tus) =
   2.244 +        strip2 (t1, u1, (t2, u2) :: tus)
   2.245 +      | strip2 x = x
   2.246 +    fun or3 ((a, b, c), (x, y, z)) = (a orelse x, b orelse y, c orelse z)
   2.247 +    fun go Ts p (Abs (_, T, t), Abs (_, _, u)) tab = go (T :: Ts) p (t, u) tab
   2.248 +      | go Ts p (t, u) tab =
   2.249 +        let
   2.250 +          val (a, _) = dest_TFree (Term.body_type (Term.fastype_of1 (Ts, t)))
   2.251 +          val (_, tf, tus) = strip2 (t, u, [])
   2.252 +          val ps_opt = case tf of Const (c, _) => Symtab.lookup monotab c | _ => NONE
   2.253 +          val tab1 =
   2.254 +            case ps_opt of
   2.255 +              SOME ps =>
   2.256 +              let
   2.257 +                val ps' = map (fn x => p * x) (take (length tus) ps)
   2.258 +              in
   2.259 +                fold I (map2 (go Ts) ps' tus) tab
   2.260 +              end
   2.261 +            | NONE => tab
   2.262 +          val tab2 = Symtab.make [(a, (p >= 0, p <= 0, is_none ps_opt))]
   2.263 +        in
   2.264 +          Symtab.join (K or3) (tab1, tab2)
   2.265 +        end
   2.266 +    val tab = go [] p (t, u) Symtab.empty
   2.267 +    fun f (a, (true, false, false)) = SOME (a, @{const implies})
   2.268 +      | f (a, (false, true, false)) = SOME (a, @{const rev_implies})
   2.269 +      | f (a, (true, true, _))      = SOME (a, HOLogic.eq_const HOLogic.boolT)
   2.270 +      | f _                         = NONE
   2.271 +  in
   2.272 +    map_filter f (Symtab.dest tab)
   2.273 +  end
   2.274 +
   2.275 +fun transfer_rule_of_term ctxt equiv t : thm =
   2.276 +  let
   2.277 +    val compound_rhs = get_compound_rhs ctxt
   2.278 +    val is_rhs = not o null o Net.unify_term compound_rhs
   2.279 +    val s = skeleton is_rhs ctxt t
   2.280      val frees = map fst (Term.add_frees s [])
   2.281      val tfrees = map fst (Term.add_tfrees s [])
   2.282      fun prep a = "R" ^ Library.unprefix "'" a
   2.283      val (rnames, ctxt') = Variable.variant_fixes (map prep tfrees) ctxt
   2.284 -    val thm = transfer_rule_of_terms ctxt' (tfrees ~~ rnames) s t
   2.285 +    val tab = tfrees ~~ rnames
   2.286 +    fun prep a = the (AList.lookup (op =) tab a)
   2.287 +    val thm = transfer_rule_of_terms fst ctxt' tab s t
   2.288 +    val binsts = bool_insts (if equiv then 0 else 1) (s, t)
   2.289 +    val cbool = @{ctyp bool}
   2.290 +    val relT = @{typ "bool => bool => bool"}
   2.291 +    val idx = Thm.maxidx_of thm + 1
   2.292 +    val thy = Proof_Context.theory_of ctxt
   2.293 +    fun tinst (a, _) = (ctyp_of thy (TVar ((a, idx), HOLogic.typeS)), cbool)
   2.294 +    fun inst (a, t) = (cterm_of thy (Var (Name.clean_index (prep a, idx), relT)), cterm_of thy t)
   2.295    in
   2.296 -    Thm.generalize (tfrees, rnames @ frees) (Thm.maxidx_of thm + 1) thm
   2.297 +    thm
   2.298 +      |> Thm.generalize (tfrees, rnames @ frees) idx
   2.299 +      |> Thm.instantiate (map tinst binsts, map inst binsts)
   2.300 +  end
   2.301 +
   2.302 +fun transfer_rule_of_lhs ctxt t : thm =
   2.303 +  let
   2.304 +    val compound_lhs = get_compound_lhs ctxt
   2.305 +    val is_lhs = not o null o Net.unify_term compound_lhs
   2.306 +    val s = skeleton is_lhs ctxt t
   2.307 +    val frees = map fst (Term.add_frees s [])
   2.308 +    val tfrees = map fst (Term.add_tfrees s [])
   2.309 +    fun prep a = "R" ^ Library.unprefix "'" a
   2.310 +    val (rnames, ctxt') = Variable.variant_fixes (map prep tfrees) ctxt
   2.311 +    val tab = tfrees ~~ rnames
   2.312 +    fun prep a = the (AList.lookup (op =) tab a)
   2.313 +    val thm = transfer_rule_of_terms snd ctxt' tab t s
   2.314 +    val binsts = bool_insts 1 (s, t)
   2.315 +    val cbool = @{ctyp bool}
   2.316 +    val relT = @{typ "bool => bool => bool"}
   2.317 +    val idx = Thm.maxidx_of thm + 1
   2.318 +    val thy = Proof_Context.theory_of ctxt
   2.319 +    fun tinst (a, _) = (ctyp_of thy (TVar ((a, idx), HOLogic.typeS)), cbool)
   2.320 +    fun inst (a, t) = (cterm_of thy (Var (Name.clean_index (prep a, idx), relT)), cterm_of thy t)
   2.321 +  in
   2.322 +    thm
   2.323 +      |> Thm.generalize (tfrees, rnames @ frees) idx
   2.324 +      |> Thm.instantiate (map tinst binsts, map inst binsts)
   2.325    end
   2.326  
   2.327  fun eq_tac eq_rules = TRY o REPEAT_ALL_NEW (resolve_tac eq_rules) THEN_ALL_NEW rtac @{thm is_equality_eq}
   2.328 @@ -409,7 +529,7 @@
   2.329  fun transfer_tac equiv ctxt i =
   2.330    let
   2.331      val pre_simps = @{thms transfer_forall_eq transfer_implies_eq}
   2.332 -    val start_rule = 
   2.333 +    val start_rule =
   2.334        if equiv then @{thm transfer_start} else @{thm transfer_start'}
   2.335      val rules = get_transfer_raw ctxt
   2.336      val eq_rules = get_relator_eq_raw ctxt
   2.337 @@ -418,7 +538,7 @@
   2.338      val err_msg = "Transfer failed to convert goal to an object-logic formula"
   2.339      fun main_tac (t, i) =
   2.340        rtac start_rule i THEN
   2.341 -      (rtac (transfer_rule_of_term ctxt (HOLogic.dest_Trueprop t))
   2.342 +      (rtac (transfer_rule_of_term ctxt equiv (HOLogic.dest_Trueprop t))
   2.343          THEN_ALL_NEW
   2.344            (SOLVED' (REPEAT_ALL_NEW (resolve_tac rules) THEN_ALL_NEW (DETERM o eq_tac eq_rules))
   2.345              ORELSE' end_tac)) (i + 1)
   2.346 @@ -429,13 +549,13 @@
   2.347         SUBGOAL main_tac i,
   2.348         (* FIXME: rewrite_goal_tac does unwanted eta-contraction *)
   2.349         rewrite_goal_tac post_simps i,
   2.350 -       rtac @{thm _} i]
   2.351 +       Goal.norm_hhf_tac i]
   2.352    end
   2.353  
   2.354  fun transfer_prover_tac ctxt = SUBGOAL (fn (t, i) =>
   2.355    let
   2.356      val rhs = (snd o Term.dest_comb o HOLogic.dest_Trueprop) t
   2.357 -    val rule1 = transfer_rule_of_term ctxt rhs
   2.358 +    val rule1 = transfer_rule_of_term ctxt false rhs
   2.359      val rules = get_transfer_raw ctxt
   2.360      val eq_rules = get_relator_eq_raw ctxt
   2.361    in
   2.362 @@ -447,6 +567,45 @@
   2.363         rtac @{thm refl} i]
   2.364    end)
   2.365  
   2.366 +(** Transfer attribute **)
   2.367 +
   2.368 +fun transferred ctxt extra_rules thm =
   2.369 +  let
   2.370 +    val start_rule = @{thm transfer_start}
   2.371 +    val start_rule' = @{thm transfer_start'}
   2.372 +    val rules = extra_rules @ get_transfer_raw ctxt
   2.373 +    val eq_rules = get_relator_eq_raw ctxt
   2.374 +    val err_msg = "Transfer failed to convert goal to an object-logic formula"
   2.375 +    val pre_simps = @{thms transfer_forall_eq transfer_implies_eq}
   2.376 +    val thm1 = Drule.forall_intr_vars thm
   2.377 +    val instT = rev (Term.add_tvars (Thm.full_prop_of thm1) [])
   2.378 +                |> map (fn v as ((a, _), S) => (v, TFree (a, S)))
   2.379 +    val thm2 = thm1
   2.380 +      |> Thm.certify_instantiate (instT, [])
   2.381 +      |> Raw_Simplifier.rewrite_rule pre_simps
   2.382 +    val ctxt' = Variable.declare_names (Thm.full_prop_of thm2) ctxt
   2.383 +    val t = HOLogic.dest_Trueprop (Thm.concl_of thm2)
   2.384 +    val rule = transfer_rule_of_lhs ctxt' t
   2.385 +    val tac =
   2.386 +      resolve_tac [thm2 RS start_rule', thm2 RS start_rule] 1 THEN
   2.387 +      (rtac rule
   2.388 +        THEN_ALL_NEW
   2.389 +          (SOLVED' (REPEAT_ALL_NEW (resolve_tac rules)
   2.390 +            THEN_ALL_NEW (DETERM o eq_tac eq_rules)))) 1
   2.391 +        handle TERM (_, ts) => raise TERM (err_msg, ts)
   2.392 +    val thm3 = Goal.prove_internal [] @{cpat "Trueprop ?P"} (K tac)
   2.393 +    val tnames = map (fst o dest_TFree o snd) instT
   2.394 +  in
   2.395 +    thm3
   2.396 +      |> Raw_Simplifier.rewrite_rule post_simps
   2.397 +      |> Raw_Simplifier.norm_hhf
   2.398 +      |> Drule.generalize (tnames, [])
   2.399 +      |> Drule.zero_var_indexes
   2.400 +  end
   2.401 +(*
   2.402 +    handle THM _ => thm
   2.403 +*)
   2.404 +
   2.405  (** Methods and attributes **)
   2.406  
   2.407  val free = Args.context -- Args.term >> (fn (_, Free v) => v | (ctxt, t) =>
   2.408 @@ -484,6 +643,14 @@
   2.409  val transfer_domain_attribute =
   2.410    Attrib.add_del transfer_domain_add transfer_domain_del
   2.411  
   2.412 +(* Attributes for transferred rules *)
   2.413 +
   2.414 +fun transferred_attribute thms = Thm.rule_attribute
   2.415 +  (fn context => transferred (Context.proof_of context) thms)
   2.416 +
   2.417 +val transferred_attribute_parser =
   2.418 +  Attrib.thms >> transferred_attribute
   2.419 +
   2.420  (* Theory setup *)
   2.421  
   2.422  val relator_eq_setup =
   2.423 @@ -528,6 +695,8 @@
   2.424       (@{binding transfer_raw}, Item_Net.content o #transfer_raw o Data.get)
   2.425    #> Attrib.setup @{binding transfer_domain_rule} transfer_domain_attribute
   2.426       "transfer domain rule for transfer method"
   2.427 +  #> Attrib.setup @{binding transferred} transferred_attribute_parser
   2.428 +     "raw theorem transferred to abstract theorem using transfer rules"
   2.429    #> Global_Theory.add_thms_dynamic
   2.430       (@{binding relator_eq_raw}, Item_Net.content o #relator_eq_raw o Data.get)
   2.431    #> Method.setup @{binding transfer} (transfer_method true)
     3.1 --- a/src/HOL/Transfer.thy	Fri Jun 07 22:17:22 2013 -0400
     3.2 +++ b/src/HOL/Transfer.thy	Sat Jun 08 19:40:19 2013 -0700
     3.3 @@ -61,6 +61,11 @@
     3.4  lemma is_equality_eq: "is_equality (op =)"
     3.5    unfolding is_equality_def by simp
     3.6  
     3.7 +text {* Reverse implication for monotonicity rules *}
     3.8 +
     3.9 +definition rev_implies where
    3.10 +  "rev_implies x y \<longleftrightarrow> (y \<longrightarrow> x)"
    3.11 +
    3.12  text {* Handling of meta-logic connectives *}
    3.13  
    3.14  definition transfer_forall where
    3.15 @@ -252,14 +257,31 @@
    3.16  
    3.17  text {* Transfer rules using implication instead of equality on booleans. *}
    3.18  
    3.19 +lemma transfer_forall_transfer [transfer_rule]:
    3.20 +  "bi_total A \<Longrightarrow> ((A ===> op =) ===> op =) transfer_forall transfer_forall"
    3.21 +  "right_total A \<Longrightarrow> ((A ===> op =) ===> implies) transfer_forall transfer_forall"
    3.22 +  "right_total A \<Longrightarrow> ((A ===> implies) ===> implies) transfer_forall transfer_forall"
    3.23 +  "bi_total A \<Longrightarrow> ((A ===> op =) ===> rev_implies) transfer_forall transfer_forall"
    3.24 +  "bi_total A \<Longrightarrow> ((A ===> rev_implies) ===> rev_implies) transfer_forall transfer_forall"
    3.25 +  unfolding transfer_forall_def rev_implies_def fun_rel_def right_total_def bi_total_def
    3.26 +  by metis+
    3.27 +
    3.28 +lemma transfer_implies_transfer [transfer_rule]:
    3.29 +  "(op =        ===> op =        ===> op =       ) transfer_implies transfer_implies"
    3.30 +  "(rev_implies ===> implies     ===> implies    ) transfer_implies transfer_implies"
    3.31 +  "(rev_implies ===> op =        ===> implies    ) transfer_implies transfer_implies"
    3.32 +  "(op =        ===> implies     ===> implies    ) transfer_implies transfer_implies"
    3.33 +  "(op =        ===> op =        ===> implies    ) transfer_implies transfer_implies"
    3.34 +  "(implies     ===> rev_implies ===> rev_implies) transfer_implies transfer_implies"
    3.35 +  "(implies     ===> op =        ===> rev_implies) transfer_implies transfer_implies"
    3.36 +  "(op =        ===> rev_implies ===> rev_implies) transfer_implies transfer_implies"
    3.37 +  "(op =        ===> op =        ===> rev_implies) transfer_implies transfer_implies"
    3.38 +  unfolding transfer_implies_def rev_implies_def fun_rel_def by auto
    3.39 +
    3.40  lemma eq_imp_transfer [transfer_rule]:
    3.41    "right_unique A \<Longrightarrow> (A ===> A ===> op \<longrightarrow>) (op =) (op =)"
    3.42    unfolding right_unique_alt_def .
    3.43  
    3.44 -lemma forall_imp_transfer [transfer_rule]:
    3.45 -  "right_total A \<Longrightarrow> ((A ===> op \<longrightarrow>) ===> op \<longrightarrow>) transfer_forall transfer_forall"
    3.46 -  unfolding right_total_alt_def transfer_forall_def .
    3.47 -
    3.48  lemma eq_transfer [transfer_rule]:
    3.49    assumes "bi_unique A"
    3.50    shows "(A ===> A ===> op =) (op =) (op =)"