1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/src/HOL/Tools/Transfer/transfer.ML Thu Apr 10 17:48:18 2014 +0200
1.3 @@ -0,0 +1,868 @@
1.4 +(* Title: HOL/Tools/Transfer/transfer.ML
1.5 + Author: Brian Huffman, TU Muenchen
1.6 + Author: Ondrej Kuncar, TU Muenchen
1.7 +
1.8 +Generic theorem transfer method.
1.9 +*)
1.10 +
1.11 +signature TRANSFER =
1.12 +sig
1.13 + type pred_data
1.14 + val rel_eq_onp: pred_data -> thm
1.15 +
1.16 + val bottom_rewr_conv: thm list -> conv
1.17 + val top_rewr_conv: thm list -> conv
1.18 +
1.19 + val prep_conv: conv
1.20 + val get_transfer_raw: Proof.context -> thm list
1.21 + val get_relator_eq_item_net: Proof.context -> thm Item_Net.T
1.22 + val get_relator_eq: Proof.context -> thm list
1.23 + val get_sym_relator_eq: Proof.context -> thm list
1.24 + val get_relator_eq_raw: Proof.context -> thm list
1.25 + val get_relator_domain: Proof.context -> thm list
1.26 + val morph_pred_data: morphism -> pred_data -> pred_data
1.27 + val lookup_pred_data: Proof.context -> string -> pred_data option
1.28 + val update_pred_data: string -> pred_data -> Context.generic -> Context.generic
1.29 + val get_compound_lhs: Proof.context -> (term * thm) Item_Net.T
1.30 + val get_compound_rhs: Proof.context -> (term * thm) Item_Net.T
1.31 + val transfer_add: attribute
1.32 + val transfer_del: attribute
1.33 + val transfer_raw_add: thm -> Context.generic -> Context.generic
1.34 + val transfer_raw_del: thm -> Context.generic -> Context.generic
1.35 + val transferred_attribute: thm list -> attribute
1.36 + val untransferred_attribute: thm list -> attribute
1.37 + val prep_transfer_domain_thm: Proof.context -> thm -> thm
1.38 + val transfer_domain_add: attribute
1.39 + val transfer_domain_del: attribute
1.40 + val transfer_rule_of_term: Proof.context -> bool -> term -> thm
1.41 + val transfer_rule_of_lhs: Proof.context -> term -> thm
1.42 + val eq_tac: Proof.context -> int -> tactic
1.43 + val transfer_step_tac: Proof.context -> int -> tactic
1.44 + val transfer_tac: bool -> Proof.context -> int -> tactic
1.45 + val transfer_prover_tac: Proof.context -> int -> tactic
1.46 + val gen_frees_tac: (string * typ) list -> Proof.context -> int -> tactic
1.47 + val setup: theory -> theory
1.48 +end
1.49 +
1.50 +structure Transfer : TRANSFER =
1.51 +struct
1.52 +
1.53 +(** Theory Data **)
1.54 +
1.55 +val compound_xhs_empty_net = Item_Net.init (Thm.eq_thm_prop o pairself snd) (single o fst);
1.56 +val rewr_rules = Item_Net.init Thm.eq_thm_prop (single o fst o HOLogic.dest_eq
1.57 + o HOLogic.dest_Trueprop o Thm.concl_of);
1.58 +
1.59 +type pred_data = {rel_eq_onp: thm}
1.60 +
1.61 +val rel_eq_onp = #rel_eq_onp
1.62 +
1.63 +structure Data = Generic_Data
1.64 +(
1.65 + type T =
1.66 + { transfer_raw : thm Item_Net.T,
1.67 + known_frees : (string * typ) list,
1.68 + compound_lhs : (term * thm) Item_Net.T,
1.69 + compound_rhs : (term * thm) Item_Net.T,
1.70 + relator_eq : thm Item_Net.T,
1.71 + relator_eq_raw : thm Item_Net.T,
1.72 + relator_domain : thm Item_Net.T,
1.73 + pred_data : pred_data Symtab.table }
1.74 + val empty =
1.75 + { transfer_raw = Thm.intro_rules,
1.76 + known_frees = [],
1.77 + compound_lhs = compound_xhs_empty_net,
1.78 + compound_rhs = compound_xhs_empty_net,
1.79 + relator_eq = rewr_rules,
1.80 + relator_eq_raw = Thm.full_rules,
1.81 + relator_domain = Thm.full_rules,
1.82 + pred_data = Symtab.empty }
1.83 + val extend = I
1.84 + fun merge
1.85 + ( { transfer_raw = t1, known_frees = k1,
1.86 + compound_lhs = l1,
1.87 + compound_rhs = c1, relator_eq = r1,
1.88 + relator_eq_raw = rw1, relator_domain = rd1,
1.89 + pred_data = pd1 },
1.90 + { transfer_raw = t2, known_frees = k2,
1.91 + compound_lhs = l2,
1.92 + compound_rhs = c2, relator_eq = r2,
1.93 + relator_eq_raw = rw2, relator_domain = rd2,
1.94 + pred_data = pd2 } ) =
1.95 + { transfer_raw = Item_Net.merge (t1, t2),
1.96 + known_frees = Library.merge (op =) (k1, k2),
1.97 + compound_lhs = Item_Net.merge (l1, l2),
1.98 + compound_rhs = Item_Net.merge (c1, c2),
1.99 + relator_eq = Item_Net.merge (r1, r2),
1.100 + relator_eq_raw = Item_Net.merge (rw1, rw2),
1.101 + relator_domain = Item_Net.merge (rd1, rd2),
1.102 + pred_data = Symtab.merge (K true) (pd1, pd2) }
1.103 +)
1.104 +
1.105 +fun get_transfer_raw ctxt = ctxt
1.106 + |> (Item_Net.content o #transfer_raw o Data.get o Context.Proof)
1.107 +
1.108 +fun get_known_frees ctxt = ctxt
1.109 + |> (#known_frees o Data.get o Context.Proof)
1.110 +
1.111 +fun get_compound_lhs ctxt = ctxt
1.112 + |> (#compound_lhs o Data.get o Context.Proof)
1.113 +
1.114 +fun get_compound_rhs ctxt = ctxt
1.115 + |> (#compound_rhs o Data.get o Context.Proof)
1.116 +
1.117 +fun get_relator_eq_item_net ctxt = (#relator_eq o Data.get o Context.Proof) ctxt
1.118 +
1.119 +fun get_relator_eq ctxt = ctxt
1.120 + |> (Item_Net.content o #relator_eq o Data.get o Context.Proof)
1.121 + |> map safe_mk_meta_eq
1.122 +
1.123 +fun get_sym_relator_eq ctxt = ctxt
1.124 + |> (Item_Net.content o #relator_eq o Data.get o Context.Proof)
1.125 + |> map (Thm.symmetric o safe_mk_meta_eq)
1.126 +
1.127 +fun get_relator_eq_raw ctxt = ctxt
1.128 + |> (Item_Net.content o #relator_eq_raw o Data.get o Context.Proof)
1.129 +
1.130 +fun get_relator_domain ctxt = ctxt
1.131 + |> (Item_Net.content o #relator_domain o Data.get o Context.Proof)
1.132 +
1.133 +fun get_pred_data ctxt = ctxt
1.134 + |> (#pred_data o Data.get o Context.Proof)
1.135 +
1.136 +fun map_data f1 f2 f3 f4 f5 f6 f7 f8
1.137 + { transfer_raw, known_frees, compound_lhs, compound_rhs,
1.138 + relator_eq, relator_eq_raw, relator_domain, pred_data } =
1.139 + { transfer_raw = f1 transfer_raw,
1.140 + known_frees = f2 known_frees,
1.141 + compound_lhs = f3 compound_lhs,
1.142 + compound_rhs = f4 compound_rhs,
1.143 + relator_eq = f5 relator_eq,
1.144 + relator_eq_raw = f6 relator_eq_raw,
1.145 + relator_domain = f7 relator_domain,
1.146 + pred_data = f8 pred_data }
1.147 +
1.148 +fun map_transfer_raw f = map_data f I I I I I I I
1.149 +fun map_known_frees f = map_data I f I I I I I I
1.150 +fun map_compound_lhs f = map_data I I f I I I I I
1.151 +fun map_compound_rhs f = map_data I I I f I I I I
1.152 +fun map_relator_eq f = map_data I I I I f I I I
1.153 +fun map_relator_eq_raw f = map_data I I I I I f I I
1.154 +fun map_relator_domain f = map_data I I I I I I f I
1.155 +fun map_pred_data f = map_data I I I I I I I f
1.156 +
1.157 +fun add_transfer_thm thm = Data.map
1.158 + (map_transfer_raw (Item_Net.update thm) o
1.159 + map_compound_lhs
1.160 + (case HOLogic.dest_Trueprop (Thm.concl_of thm) of
1.161 + Const (@{const_name Rel}, _) $ _ $ (lhs as (_ $ _)) $ _ =>
1.162 + Item_Net.update (lhs, thm)
1.163 + | _ => I) o
1.164 + map_compound_rhs
1.165 + (case HOLogic.dest_Trueprop (Thm.concl_of thm) of
1.166 + Const (@{const_name Rel}, _) $ _ $ _ $ (rhs as (_ $ _)) =>
1.167 + Item_Net.update (rhs, thm)
1.168 + | _ => I) o
1.169 + map_known_frees (Term.add_frees (Thm.concl_of thm)))
1.170 +
1.171 +fun del_transfer_thm thm = Data.map
1.172 + (map_transfer_raw (Item_Net.remove thm) o
1.173 + map_compound_lhs
1.174 + (case HOLogic.dest_Trueprop (Thm.concl_of thm) of
1.175 + Const (@{const_name Rel}, _) $ _ $ (lhs as (_ $ _)) $ _ =>
1.176 + Item_Net.remove (lhs, thm)
1.177 + | _ => I) o
1.178 + map_compound_rhs
1.179 + (case HOLogic.dest_Trueprop (Thm.concl_of thm) of
1.180 + Const (@{const_name Rel}, _) $ _ $ _ $ (rhs as (_ $ _)) =>
1.181 + Item_Net.remove (rhs, thm)
1.182 + | _ => I))
1.183 +
1.184 +fun transfer_raw_add thm ctxt = add_transfer_thm thm ctxt
1.185 +fun transfer_raw_del thm ctxt = del_transfer_thm thm ctxt
1.186 +
1.187 +(** Conversions **)
1.188 +
1.189 +fun bottom_rewr_conv rewrs = Conv.bottom_conv (K (Conv.try_conv (Conv.rewrs_conv rewrs))) @{context}
1.190 +fun top_rewr_conv rewrs = Conv.top_conv (K (Conv.try_conv (Conv.rewrs_conv rewrs))) @{context}
1.191 +
1.192 +fun transfer_rel_conv conv =
1.193 + Conv.concl_conv ~1 (HOLogic.Trueprop_conv (Conv.fun2_conv (Conv.arg_conv conv)))
1.194 +
1.195 +val Rel_rule = Thm.symmetric @{thm Rel_def}
1.196 +
1.197 +fun dest_funcT cT =
1.198 + (case Thm.dest_ctyp cT of [T, U] => (T, U)
1.199 + | _ => raise TYPE ("dest_funcT", [Thm.typ_of cT], []))
1.200 +
1.201 +fun Rel_conv ct =
1.202 + let val (cT, cT') = dest_funcT (Thm.ctyp_of_term ct)
1.203 + val (cU, _) = dest_funcT cT'
1.204 + in Drule.instantiate' [SOME cT, SOME cU] [SOME ct] Rel_rule end
1.205 +
1.206 +(* Conversion to preprocess a transfer rule *)
1.207 +fun safe_Rel_conv ct =
1.208 + Conv.try_conv (HOLogic.Trueprop_conv (Conv.fun_conv (Conv.fun_conv Rel_conv))) ct
1.209 +
1.210 +fun prep_conv ct = (
1.211 + Conv.implies_conv safe_Rel_conv prep_conv
1.212 + else_conv
1.213 + safe_Rel_conv
1.214 + else_conv
1.215 + Conv.all_conv) ct
1.216 +
1.217 +(** Replacing explicit equalities with is_equality premises **)
1.218 +
1.219 +fun mk_is_equality t =
1.220 + Const (@{const_name is_equality}, Term.fastype_of t --> HOLogic.boolT) $ t
1.221 +
1.222 +val is_equality_lemma =
1.223 + @{lemma "(!!R. is_equality R ==> PROP (P R)) == PROP (P (op =))"
1.224 + by (unfold is_equality_def, rule, drule meta_spec,
1.225 + erule meta_mp, rule refl, simp)}
1.226 +
1.227 +fun gen_abstract_equalities ctxt (dest : term -> term * (term -> term)) thm =
1.228 + let
1.229 + val thy = Thm.theory_of_thm thm
1.230 + val prop = Thm.prop_of thm
1.231 + val (t, mk_prop') = dest prop
1.232 + (* Only consider "op =" at non-base types *)
1.233 + fun is_eq (Const (@{const_name HOL.eq}, Type ("fun", [T, _]))) =
1.234 + (case T of Type (_, []) => false | _ => true)
1.235 + | is_eq _ = false
1.236 + val add_eqs = Term.fold_aterms (fn t => if is_eq t then insert (op =) t else I)
1.237 + val eq_consts = rev (add_eqs t [])
1.238 + val eqTs = map (snd o dest_Const) eq_consts
1.239 + val used = Term.add_free_names prop []
1.240 + val names = map (K "") eqTs |> Name.variant_list used
1.241 + val frees = map Free (names ~~ eqTs)
1.242 + val prems = map (HOLogic.mk_Trueprop o mk_is_equality) frees
1.243 + val prop1 = mk_prop' (Term.subst_atomic (eq_consts ~~ frees) t)
1.244 + val prop2 = fold Logic.all frees (Logic.list_implies (prems, prop1))
1.245 + val cprop = Thm.cterm_of thy prop2
1.246 + val equal_thm = Raw_Simplifier.rewrite ctxt false [is_equality_lemma] cprop
1.247 + fun forall_elim thm = Thm.forall_elim_vars (Thm.maxidx_of thm + 1) thm
1.248 + in
1.249 + forall_elim (thm COMP (equal_thm COMP @{thm equal_elim_rule2}))
1.250 + end
1.251 + handle TERM _ => thm
1.252 +
1.253 +fun abstract_equalities_transfer ctxt thm =
1.254 + let
1.255 + fun dest prop =
1.256 + let
1.257 + val prems = Logic.strip_imp_prems prop
1.258 + val concl = HOLogic.dest_Trueprop (Logic.strip_imp_concl prop)
1.259 + val ((rel, x), y) = apfst Term.dest_comb (Term.dest_comb concl)
1.260 + in
1.261 + (rel, fn rel' =>
1.262 + Logic.list_implies (prems, HOLogic.mk_Trueprop (rel' $ x $ y)))
1.263 + end
1.264 + val contracted_eq_thm =
1.265 + Conv.fconv_rule (transfer_rel_conv (bottom_rewr_conv (get_relator_eq ctxt))) thm
1.266 + handle CTERM _ => thm
1.267 + in
1.268 + gen_abstract_equalities ctxt dest contracted_eq_thm
1.269 + end
1.270 +
1.271 +fun abstract_equalities_relator_eq ctxt rel_eq_thm =
1.272 + gen_abstract_equalities ctxt (fn x => (x, I))
1.273 + (rel_eq_thm RS @{thm is_equality_def [THEN iffD2]})
1.274 +
1.275 +fun abstract_equalities_domain ctxt thm =
1.276 + let
1.277 + fun dest prop =
1.278 + let
1.279 + val prems = Logic.strip_imp_prems prop
1.280 + val concl = HOLogic.dest_Trueprop (Logic.strip_imp_concl prop)
1.281 + val ((eq, dom), y) = apfst Term.dest_comb (Term.dest_comb concl)
1.282 + in
1.283 + (dom, fn dom' => Logic.list_implies (prems, HOLogic.mk_Trueprop (eq $ dom' $ y)))
1.284 + end
1.285 + fun transfer_rel_conv conv =
1.286 + Conv.concl_conv ~1 (HOLogic.Trueprop_conv (Conv.arg1_conv (Conv.arg_conv conv)))
1.287 + val contracted_eq_thm =
1.288 + Conv.fconv_rule (transfer_rel_conv (bottom_rewr_conv (get_relator_eq ctxt))) thm
1.289 + in
1.290 + gen_abstract_equalities ctxt dest contracted_eq_thm
1.291 + end
1.292 +
1.293 +
1.294 +(** Replacing explicit Domainp predicates with Domainp assumptions **)
1.295 +
1.296 +fun mk_Domainp_assm (T, R) =
1.297 + HOLogic.mk_eq ((Const (@{const_name Domainp}, Term.fastype_of T --> Term.fastype_of R) $ T), R)
1.298 +
1.299 +val Domainp_lemma =
1.300 + @{lemma "(!!R. Domainp T = R ==> PROP (P R)) == PROP (P (Domainp T))"
1.301 + by (rule, drule meta_spec,
1.302 + erule meta_mp, rule refl, simp)}
1.303 +
1.304 +fun fold_Domainp f (t as Const (@{const_name Domainp},_) $ (Var (_,_))) = f t
1.305 + | fold_Domainp f (t $ u) = fold_Domainp f t #> fold_Domainp f u
1.306 + | fold_Domainp f (Abs (_, _, t)) = fold_Domainp f t
1.307 + | fold_Domainp _ _ = I
1.308 +
1.309 +fun subst_terms tab t =
1.310 + let
1.311 + val t' = Termtab.lookup tab t
1.312 + in
1.313 + case t' of
1.314 + SOME t' => t'
1.315 + | NONE =>
1.316 + (case t of
1.317 + u $ v => (subst_terms tab u) $ (subst_terms tab v)
1.318 + | Abs (a, T, t) => Abs (a, T, subst_terms tab t)
1.319 + | t => t)
1.320 + end
1.321 +
1.322 +fun gen_abstract_domains ctxt (dest : term -> term * (term -> term)) thm =
1.323 + let
1.324 + val thy = Thm.theory_of_thm thm
1.325 + val prop = Thm.prop_of thm
1.326 + val (t, mk_prop') = dest prop
1.327 + val Domainp_tms = rev (fold_Domainp (fn t => insert op= t) t [])
1.328 + val Domainp_Ts = map (snd o dest_funT o snd o dest_Const o fst o dest_comb) Domainp_tms
1.329 + val used = Term.add_free_names t []
1.330 + val rels = map (snd o dest_comb) Domainp_tms
1.331 + val rel_names = map (fst o fst o dest_Var) rels
1.332 + val names = map (fn name => ("D" ^ name)) rel_names |> Name.variant_list used
1.333 + val frees = map Free (names ~~ Domainp_Ts)
1.334 + val prems = map (HOLogic.mk_Trueprop o mk_Domainp_assm) (rels ~~ frees);
1.335 + val t' = subst_terms (fold Termtab.update (Domainp_tms ~~ frees) Termtab.empty) t
1.336 + val prop1 = fold Logic.all frees (Logic.list_implies (prems, mk_prop' t'))
1.337 + val prop2 = Logic.list_rename_params (rev names) prop1
1.338 + val cprop = Thm.cterm_of thy prop2
1.339 + val equal_thm = Raw_Simplifier.rewrite ctxt false [Domainp_lemma] cprop
1.340 + fun forall_elim thm = Thm.forall_elim_vars (Thm.maxidx_of thm + 1) thm;
1.341 + in
1.342 + forall_elim (thm COMP (equal_thm COMP @{thm equal_elim_rule2}))
1.343 + end
1.344 + handle TERM _ => thm
1.345 +
1.346 +fun abstract_domains_transfer ctxt thm =
1.347 + let
1.348 + fun dest prop =
1.349 + let
1.350 + val prems = Logic.strip_imp_prems prop
1.351 + val concl = HOLogic.dest_Trueprop (Logic.strip_imp_concl prop)
1.352 + val ((rel, x), y) = apfst Term.dest_comb (Term.dest_comb concl)
1.353 + in
1.354 + (x, fn x' =>
1.355 + Logic.list_implies (prems, HOLogic.mk_Trueprop (rel $ x' $ y)))
1.356 + end
1.357 + in
1.358 + gen_abstract_domains ctxt dest thm
1.359 + end
1.360 +
1.361 +fun abstract_domains_relator_domain ctxt thm =
1.362 + let
1.363 + fun dest prop =
1.364 + let
1.365 + val prems = Logic.strip_imp_prems prop
1.366 + val concl = HOLogic.dest_Trueprop (Logic.strip_imp_concl prop)
1.367 + val ((rel, x), y) = apfst Term.dest_comb (Term.dest_comb concl)
1.368 + in
1.369 + (y, fn y' =>
1.370 + Logic.list_implies (prems, HOLogic.mk_Trueprop (rel $ x $ y')))
1.371 + end
1.372 + in
1.373 + gen_abstract_domains ctxt dest thm
1.374 + end
1.375 +
1.376 +fun detect_transfer_rules thm =
1.377 + let
1.378 + fun is_transfer_rule tm = case (HOLogic.dest_Trueprop tm) of
1.379 + (Const (@{const_name HOL.eq}, _)) $ ((Const (@{const_name Domainp}, _)) $ _) $ _ => false
1.380 + | _ $ _ $ _ => true
1.381 + | _ => false
1.382 + fun safe_transfer_rule_conv ctm =
1.383 + if is_transfer_rule (term_of ctm) then safe_Rel_conv ctm else Conv.all_conv ctm
1.384 + in
1.385 + Conv.fconv_rule (Conv.prems_conv ~1 safe_transfer_rule_conv) thm
1.386 + end
1.387 +
1.388 +(** Adding transfer domain rules **)
1.389 +
1.390 +fun prep_transfer_domain_thm ctxt thm =
1.391 + (abstract_equalities_domain ctxt o detect_transfer_rules) thm
1.392 +
1.393 +fun add_transfer_domain_thm thm ctxt = (add_transfer_thm o
1.394 + prep_transfer_domain_thm (Context.proof_of ctxt)) thm ctxt
1.395 +
1.396 +fun del_transfer_domain_thm thm ctxt = (del_transfer_thm o
1.397 + prep_transfer_domain_thm (Context.proof_of ctxt)) thm ctxt
1.398 +
1.399 +(** Transfer proof method **)
1.400 +
1.401 +val post_simps =
1.402 + @{thms transfer_forall_eq [symmetric]
1.403 + transfer_implies_eq [symmetric] transfer_bforall_unfold}
1.404 +
1.405 +fun gen_frees_tac keepers ctxt = SUBGOAL (fn (t, i) =>
1.406 + let
1.407 + val keepers = keepers @ get_known_frees ctxt
1.408 + val vs = rev (Term.add_frees t [])
1.409 + val vs' = filter_out (member (op =) keepers) vs
1.410 + in
1.411 + Induct.arbitrary_tac ctxt 0 vs' i
1.412 + end)
1.413 +
1.414 +fun mk_relT (T, U) = T --> U --> HOLogic.boolT
1.415 +
1.416 +fun mk_Rel t =
1.417 + let val T = fastype_of t
1.418 + in Const (@{const_name Transfer.Rel}, T --> T) $ t end
1.419 +
1.420 +fun transfer_rule_of_terms (prj : typ * typ -> typ) ctxt tab t u =
1.421 + let
1.422 + val thy = Proof_Context.theory_of ctxt
1.423 + (* precondition: prj(T,U) must consist of only TFrees and type "fun" *)
1.424 + fun rel (T as Type ("fun", [T1, T2])) (U as Type ("fun", [U1, U2])) =
1.425 + let
1.426 + val r1 = rel T1 U1
1.427 + val r2 = rel T2 U2
1.428 + val rT = fastype_of r1 --> fastype_of r2 --> mk_relT (T, U)
1.429 + in
1.430 + Const (@{const_name rel_fun}, rT) $ r1 $ r2
1.431 + end
1.432 + | rel T U =
1.433 + let
1.434 + val (a, _) = dest_TFree (prj (T, U))
1.435 + in
1.436 + Free (the (AList.lookup (op =) tab a), mk_relT (T, U))
1.437 + end
1.438 + fun zip _ thms (Bound i) (Bound _) = (nth thms i, [])
1.439 + | zip ctxt thms (Abs (x, T, t)) (Abs (y, U, u)) =
1.440 + let
1.441 + val ([x', y'], ctxt') = Variable.variant_fixes [x, y] ctxt
1.442 + val prop = mk_Rel (rel T U) $ Free (x', T) $ Free (y', U)
1.443 + val cprop = Thm.cterm_of thy (HOLogic.mk_Trueprop prop)
1.444 + val thm0 = Thm.assume cprop
1.445 + val (thm1, hyps) = zip ctxt' (thm0 :: thms) t u
1.446 + val ((r1, x), y) = apfst Thm.dest_comb (Thm.dest_comb (Thm.dest_arg cprop))
1.447 + val r2 = Thm.dest_fun2 (Thm.dest_arg (cprop_of thm1))
1.448 + val (a1, (b1, _)) = apsnd dest_funcT (dest_funcT (ctyp_of_term r1))
1.449 + val (a2, (b2, _)) = apsnd dest_funcT (dest_funcT (ctyp_of_term r2))
1.450 + val tinsts = [SOME a1, SOME b1, SOME a2, SOME b2]
1.451 + val insts = [SOME (Thm.dest_arg r1), SOME (Thm.dest_arg r2)]
1.452 + val rule = Drule.instantiate' tinsts insts @{thm Rel_abs}
1.453 + val thm2 = Thm.forall_intr x (Thm.forall_intr y (Thm.implies_intr cprop thm1))
1.454 + in
1.455 + (thm2 COMP rule, hyps)
1.456 + end
1.457 + | zip ctxt thms (f $ t) (g $ u) =
1.458 + let
1.459 + val (thm1, hyps1) = zip ctxt thms f g
1.460 + val (thm2, hyps2) = zip ctxt thms t u
1.461 + in
1.462 + (thm2 RS (thm1 RS @{thm Rel_app}), hyps1 @ hyps2)
1.463 + end
1.464 + | zip _ _ t u =
1.465 + let
1.466 + val T = fastype_of t
1.467 + val U = fastype_of u
1.468 + val prop = mk_Rel (rel T U) $ t $ u
1.469 + val cprop = Thm.cterm_of thy (HOLogic.mk_Trueprop prop)
1.470 + in
1.471 + (Thm.assume cprop, [cprop])
1.472 + end
1.473 + val r = mk_Rel (rel (fastype_of t) (fastype_of u))
1.474 + val goal = HOLogic.mk_Trueprop (r $ t $ u)
1.475 + val rename = Thm.trivial (cterm_of thy goal)
1.476 + val (thm, hyps) = zip ctxt [] t u
1.477 + in
1.478 + Drule.implies_intr_list hyps (thm RS rename)
1.479 + end
1.480 +
1.481 +(* create a lambda term of the same shape as the given term *)
1.482 +fun skeleton (is_atom : term -> bool) ctxt t =
1.483 + let
1.484 + fun dummy ctxt =
1.485 + let
1.486 + val (c, ctxt) = yield_singleton Variable.variant_fixes "a" ctxt
1.487 + in
1.488 + (Free (c, dummyT), ctxt)
1.489 + end
1.490 + fun go (Bound i) ctxt = (Bound i, ctxt)
1.491 + | go (Abs (x, _, t)) ctxt =
1.492 + let
1.493 + val (t', ctxt) = go t ctxt
1.494 + in
1.495 + (Abs (x, dummyT, t'), ctxt)
1.496 + end
1.497 + | go (tu as (t $ u)) ctxt =
1.498 + if is_atom tu andalso not (Term.is_open tu) then dummy ctxt else
1.499 + let
1.500 + val (t', ctxt) = go t ctxt
1.501 + val (u', ctxt) = go u ctxt
1.502 + in
1.503 + (t' $ u', ctxt)
1.504 + end
1.505 + | go _ ctxt = dummy ctxt
1.506 + in
1.507 + go t ctxt |> fst |> Syntax.check_term ctxt |>
1.508 + map_types (map_type_tfree (fn (a, _) => TFree (a, @{sort type})))
1.509 + end
1.510 +
1.511 +(** Monotonicity analysis **)
1.512 +
1.513 +(* TODO: Put extensible table in theory data *)
1.514 +val monotab =
1.515 + Symtab.make
1.516 + [(@{const_name transfer_implies}, [~1, 1]),
1.517 + (@{const_name transfer_forall}, [1])(*,
1.518 + (@{const_name implies}, [~1, 1]),
1.519 + (@{const_name All}, [1])*)]
1.520 +
1.521 +(*
1.522 +Function bool_insts determines the set of boolean-relation variables
1.523 +that can be instantiated to implies, rev_implies, or iff.
1.524 +
1.525 +Invariants: bool_insts p (t, u) requires that
1.526 + u :: _ => _ => ... => bool, and
1.527 + t is a skeleton of u
1.528 +*)
1.529 +fun bool_insts p (t, u) =
1.530 + let
1.531 + fun strip2 (t1 $ t2, u1 $ u2, tus) =
1.532 + strip2 (t1, u1, (t2, u2) :: tus)
1.533 + | strip2 x = x
1.534 + fun or3 ((a, b, c), (x, y, z)) = (a orelse x, b orelse y, c orelse z)
1.535 + fun go Ts p (Abs (_, T, t), Abs (_, _, u)) tab = go (T :: Ts) p (t, u) tab
1.536 + | go Ts p (t, u) tab =
1.537 + let
1.538 + val (a, _) = dest_TFree (Term.body_type (Term.fastype_of1 (Ts, t)))
1.539 + val (_, tf, tus) = strip2 (t, u, [])
1.540 + val ps_opt = case tf of Const (c, _) => Symtab.lookup monotab c | _ => NONE
1.541 + val tab1 =
1.542 + case ps_opt of
1.543 + SOME ps =>
1.544 + let
1.545 + val ps' = map (fn x => p * x) (take (length tus) ps)
1.546 + in
1.547 + fold I (map2 (go Ts) ps' tus) tab
1.548 + end
1.549 + | NONE => tab
1.550 + val tab2 = Symtab.make [(a, (p >= 0, p <= 0, is_none ps_opt))]
1.551 + in
1.552 + Symtab.join (K or3) (tab1, tab2)
1.553 + end
1.554 + val tab = go [] p (t, u) Symtab.empty
1.555 + fun f (a, (true, false, false)) = SOME (a, @{const implies})
1.556 + | f (a, (false, true, false)) = SOME (a, @{const rev_implies})
1.557 + | f (a, (true, true, _)) = SOME (a, HOLogic.eq_const HOLogic.boolT)
1.558 + | f _ = NONE
1.559 + in
1.560 + map_filter f (Symtab.dest tab)
1.561 + end
1.562 +
1.563 +fun retrieve_terms t net = map fst (Item_Net.retrieve net t)
1.564 +
1.565 +fun matches_list ctxt term =
1.566 + is_some o find_first (fn pat => Pattern.matches (Proof_Context.theory_of ctxt) (pat, term))
1.567 +
1.568 +fun transfer_rule_of_term ctxt equiv t : thm =
1.569 + let
1.570 + val compound_rhs = get_compound_rhs ctxt
1.571 + fun is_rhs t = compound_rhs |> retrieve_terms t |> matches_list ctxt t
1.572 + val s = skeleton is_rhs ctxt t
1.573 + val frees = map fst (Term.add_frees s [])
1.574 + val tfrees = map fst (Term.add_tfrees s [])
1.575 + fun prep a = "R" ^ Library.unprefix "'" a
1.576 + val (rnames, ctxt') = Variable.variant_fixes (map prep tfrees) ctxt
1.577 + val tab = tfrees ~~ rnames
1.578 + fun prep a = the (AList.lookup (op =) tab a)
1.579 + val thm = transfer_rule_of_terms fst ctxt' tab s t
1.580 + val binsts = bool_insts (if equiv then 0 else 1) (s, t)
1.581 + val cbool = @{ctyp bool}
1.582 + val relT = @{typ "bool => bool => bool"}
1.583 + val idx = Thm.maxidx_of thm + 1
1.584 + val thy = Proof_Context.theory_of ctxt
1.585 + fun tinst (a, _) = (ctyp_of thy (TVar ((a, idx), @{sort type})), cbool)
1.586 + fun inst (a, t) = (cterm_of thy (Var (Name.clean_index (prep a, idx), relT)), cterm_of thy t)
1.587 + in
1.588 + thm
1.589 + |> Thm.generalize (tfrees, rnames @ frees) idx
1.590 + |> Thm.instantiate (map tinst binsts, map inst binsts)
1.591 + end
1.592 +
1.593 +fun transfer_rule_of_lhs ctxt t : thm =
1.594 + let
1.595 + val compound_lhs = get_compound_lhs ctxt
1.596 + fun is_lhs t = compound_lhs |> retrieve_terms t |> matches_list ctxt t
1.597 + val s = skeleton is_lhs ctxt t
1.598 + val frees = map fst (Term.add_frees s [])
1.599 + val tfrees = map fst (Term.add_tfrees s [])
1.600 + fun prep a = "R" ^ Library.unprefix "'" a
1.601 + val (rnames, ctxt') = Variable.variant_fixes (map prep tfrees) ctxt
1.602 + val tab = tfrees ~~ rnames
1.603 + fun prep a = the (AList.lookup (op =) tab a)
1.604 + val thm = transfer_rule_of_terms snd ctxt' tab t s
1.605 + val binsts = bool_insts 1 (s, t)
1.606 + val cbool = @{ctyp bool}
1.607 + val relT = @{typ "bool => bool => bool"}
1.608 + val idx = Thm.maxidx_of thm + 1
1.609 + val thy = Proof_Context.theory_of ctxt
1.610 + fun tinst (a, _) = (ctyp_of thy (TVar ((a, idx), @{sort type})), cbool)
1.611 + fun inst (a, t) = (cterm_of thy (Var (Name.clean_index (prep a, idx), relT)), cterm_of thy t)
1.612 + in
1.613 + thm
1.614 + |> Thm.generalize (tfrees, rnames @ frees) idx
1.615 + |> Thm.instantiate (map tinst binsts, map inst binsts)
1.616 + end
1.617 +
1.618 +fun eq_rules_tac eq_rules = TRY o REPEAT_ALL_NEW (resolve_tac eq_rules)
1.619 + THEN_ALL_NEW rtac @{thm is_equality_eq}
1.620 +
1.621 +fun eq_tac ctxt = eq_rules_tac (get_relator_eq_raw ctxt)
1.622 +
1.623 +fun transfer_step_tac ctxt = (REPEAT_ALL_NEW (resolve_tac (get_transfer_raw ctxt))
1.624 + THEN_ALL_NEW (DETERM o eq_rules_tac (get_relator_eq_raw ctxt)))
1.625 +
1.626 +fun transfer_tac equiv ctxt i =
1.627 + let
1.628 + val pre_simps = @{thms transfer_forall_eq transfer_implies_eq}
1.629 + val start_rule =
1.630 + if equiv then @{thm transfer_start} else @{thm transfer_start'}
1.631 + val rules = get_transfer_raw ctxt
1.632 + val eq_rules = get_relator_eq_raw ctxt
1.633 + (* allow unsolved subgoals only for standard transfer method, not for transfer' *)
1.634 + val end_tac = if equiv then K all_tac else K no_tac
1.635 + val err_msg = "Transfer failed to convert goal to an object-logic formula"
1.636 + fun main_tac (t, i) =
1.637 + rtac start_rule i THEN
1.638 + (rtac (transfer_rule_of_term ctxt equiv (HOLogic.dest_Trueprop t))
1.639 + THEN_ALL_NEW
1.640 + (SOLVED' (REPEAT_ALL_NEW (resolve_tac rules) THEN_ALL_NEW (DETERM o eq_rules_tac eq_rules))
1.641 + ORELSE' end_tac)) (i + 1)
1.642 + handle TERM (_, ts) => raise TERM (err_msg, ts)
1.643 + in
1.644 + EVERY
1.645 + [rewrite_goal_tac ctxt pre_simps i THEN
1.646 + SUBGOAL main_tac i,
1.647 + (* FIXME: rewrite_goal_tac does unwanted eta-contraction *)
1.648 + rewrite_goal_tac ctxt post_simps i,
1.649 + Goal.norm_hhf_tac ctxt i]
1.650 + end
1.651 +
1.652 +fun transfer_prover_tac ctxt = SUBGOAL (fn (t, i) =>
1.653 + let
1.654 + val rhs = (snd o Term.dest_comb o HOLogic.dest_Trueprop) t
1.655 + val rule1 = transfer_rule_of_term ctxt false rhs
1.656 + val rules = get_transfer_raw ctxt
1.657 + val eq_rules = get_relator_eq_raw ctxt
1.658 + val expand_eq_in_rel = transfer_rel_conv (top_rewr_conv [@{thm rel_fun_eq[symmetric,THEN eq_reflection]}])
1.659 + in
1.660 + EVERY
1.661 + [CONVERSION prep_conv i,
1.662 + rtac @{thm transfer_prover_start} i,
1.663 + ((rtac rule1 ORELSE' (CONVERSION expand_eq_in_rel THEN' rtac rule1))
1.664 + THEN_ALL_NEW
1.665 + (REPEAT_ALL_NEW (resolve_tac rules) THEN_ALL_NEW (DETERM o eq_rules_tac eq_rules))) (i+1),
1.666 + rtac @{thm refl} i]
1.667 + end)
1.668 +
1.669 +(** Transfer attribute **)
1.670 +
1.671 +fun transferred ctxt extra_rules thm =
1.672 + let
1.673 + val start_rule = @{thm transfer_start}
1.674 + val start_rule' = @{thm transfer_start'}
1.675 + val rules = extra_rules @ get_transfer_raw ctxt
1.676 + val eq_rules = get_relator_eq_raw ctxt
1.677 + val err_msg = "Transfer failed to convert goal to an object-logic formula"
1.678 + val pre_simps = @{thms transfer_forall_eq transfer_implies_eq}
1.679 + val thm1 = Drule.forall_intr_vars thm
1.680 + val instT = rev (Term.add_tvars (Thm.full_prop_of thm1) [])
1.681 + |> map (fn v as ((a, _), S) => (v, TFree (a, S)))
1.682 + val thm2 = thm1
1.683 + |> Thm.certify_instantiate (instT, [])
1.684 + |> Raw_Simplifier.rewrite_rule ctxt pre_simps
1.685 + val ctxt' = Variable.declare_names (Thm.full_prop_of thm2) ctxt
1.686 + val t = HOLogic.dest_Trueprop (Thm.concl_of thm2)
1.687 + val rule = transfer_rule_of_lhs ctxt' t
1.688 + val tac =
1.689 + resolve_tac [thm2 RS start_rule', thm2 RS start_rule] 1 THEN
1.690 + (rtac rule
1.691 + THEN_ALL_NEW
1.692 + (SOLVED' (REPEAT_ALL_NEW (resolve_tac rules)
1.693 + THEN_ALL_NEW (DETERM o eq_rules_tac eq_rules)))) 1
1.694 + handle TERM (_, ts) => raise TERM (err_msg, ts)
1.695 + val thm3 = Goal.prove_internal ctxt' [] @{cpat "Trueprop ?P"} (K tac)
1.696 + val tnames = map (fst o dest_TFree o snd) instT
1.697 + in
1.698 + thm3
1.699 + |> Raw_Simplifier.rewrite_rule ctxt' post_simps
1.700 + |> Simplifier.norm_hhf ctxt'
1.701 + |> Drule.generalize (tnames, [])
1.702 + |> Drule.zero_var_indexes
1.703 + end
1.704 +(*
1.705 + handle THM _ => thm
1.706 +*)
1.707 +
1.708 +fun untransferred ctxt extra_rules thm =
1.709 + let
1.710 + val start_rule = @{thm untransfer_start}
1.711 + val rules = extra_rules @ get_transfer_raw ctxt
1.712 + val eq_rules = get_relator_eq_raw ctxt
1.713 + val err_msg = "Transfer failed to convert goal to an object-logic formula"
1.714 + val pre_simps = @{thms transfer_forall_eq transfer_implies_eq}
1.715 + val thm1 = Drule.forall_intr_vars thm
1.716 + val instT = rev (Term.add_tvars (Thm.full_prop_of thm1) [])
1.717 + |> map (fn v as ((a, _), S) => (v, TFree (a, S)))
1.718 + val thm2 = thm1
1.719 + |> Thm.certify_instantiate (instT, [])
1.720 + |> Raw_Simplifier.rewrite_rule ctxt pre_simps
1.721 + val ctxt' = Variable.declare_names (Thm.full_prop_of thm2) ctxt
1.722 + val t = HOLogic.dest_Trueprop (Thm.concl_of thm2)
1.723 + val rule = transfer_rule_of_term ctxt' true t
1.724 + val tac =
1.725 + rtac (thm2 RS start_rule) 1 THEN
1.726 + (rtac rule
1.727 + THEN_ALL_NEW
1.728 + (SOLVED' (REPEAT_ALL_NEW (resolve_tac rules)
1.729 + THEN_ALL_NEW (DETERM o eq_rules_tac eq_rules)))) 1
1.730 + handle TERM (_, ts) => raise TERM (err_msg, ts)
1.731 + val thm3 = Goal.prove_internal ctxt' [] @{cpat "Trueprop ?P"} (K tac)
1.732 + val tnames = map (fst o dest_TFree o snd) instT
1.733 + in
1.734 + thm3
1.735 + |> Raw_Simplifier.rewrite_rule ctxt' post_simps
1.736 + |> Simplifier.norm_hhf ctxt'
1.737 + |> Drule.generalize (tnames, [])
1.738 + |> Drule.zero_var_indexes
1.739 + end
1.740 +
1.741 +(** Methods and attributes **)
1.742 +
1.743 +val free = Args.context -- Args.term >> (fn (_, Free v) => v | (ctxt, t) =>
1.744 + error ("Bad free variable: " ^ Syntax.string_of_term ctxt t))
1.745 +
1.746 +val fixing = Scan.optional (Scan.lift (Args.$$$ "fixing" -- Args.colon)
1.747 + |-- Scan.repeat free) []
1.748 +
1.749 +fun transfer_method equiv : (Proof.context -> Proof.method) context_parser =
1.750 + fixing >> (fn vs => fn ctxt =>
1.751 + SIMPLE_METHOD' (gen_frees_tac vs ctxt THEN' transfer_tac equiv ctxt))
1.752 +
1.753 +val transfer_prover_method : (Proof.context -> Proof.method) context_parser =
1.754 + Scan.succeed (fn ctxt => SIMPLE_METHOD' (transfer_prover_tac ctxt))
1.755 +
1.756 +(* Attribute for transfer rules *)
1.757 +
1.758 +fun prep_rule ctxt =
1.759 + abstract_domains_transfer ctxt o abstract_equalities_transfer ctxt o Conv.fconv_rule prep_conv
1.760 +
1.761 +val transfer_add =
1.762 + Thm.declaration_attribute (fn thm => fn ctxt =>
1.763 + (add_transfer_thm o prep_rule (Context.proof_of ctxt)) thm ctxt)
1.764 +
1.765 +val transfer_del =
1.766 + Thm.declaration_attribute (fn thm => fn ctxt =>
1.767 + (del_transfer_thm o prep_rule (Context.proof_of ctxt)) thm ctxt)
1.768 +
1.769 +val transfer_attribute =
1.770 + Attrib.add_del transfer_add transfer_del
1.771 +
1.772 +(* Attributes for transfer domain rules *)
1.773 +
1.774 +val transfer_domain_add = Thm.declaration_attribute add_transfer_domain_thm
1.775 +
1.776 +val transfer_domain_del = Thm.declaration_attribute del_transfer_domain_thm
1.777 +
1.778 +val transfer_domain_attribute =
1.779 + Attrib.add_del transfer_domain_add transfer_domain_del
1.780 +
1.781 +(* Attributes for transferred rules *)
1.782 +
1.783 +fun transferred_attribute thms = Thm.rule_attribute
1.784 + (fn context => transferred (Context.proof_of context) thms)
1.785 +
1.786 +fun untransferred_attribute thms = Thm.rule_attribute
1.787 + (fn context => untransferred (Context.proof_of context) thms)
1.788 +
1.789 +val transferred_attribute_parser =
1.790 + Attrib.thms >> transferred_attribute
1.791 +
1.792 +val untransferred_attribute_parser =
1.793 + Attrib.thms >> untransferred_attribute
1.794 +
1.795 +fun morph_pred_data phi {rel_eq_onp} = {rel_eq_onp = Morphism.thm phi rel_eq_onp}
1.796 +
1.797 +fun lookup_pred_data ctxt type_name = Symtab.lookup (get_pred_data ctxt) type_name
1.798 + |> Option.map (morph_pred_data (Morphism.transfer_morphism (Proof_Context.theory_of ctxt)))
1.799 +
1.800 +fun update_pred_data type_name qinfo ctxt =
1.801 + Data.map (map_pred_data (Symtab.update (type_name, qinfo))) ctxt
1.802 +
1.803 +(* Theory setup *)
1.804 +
1.805 +val relator_eq_setup =
1.806 + let
1.807 + val name = @{binding relator_eq}
1.808 + fun add_thm thm context = context
1.809 + |> Data.map (map_relator_eq (Item_Net.update thm))
1.810 + |> Data.map (map_relator_eq_raw
1.811 + (Item_Net.update (abstract_equalities_relator_eq (Context.proof_of context) thm)))
1.812 + fun del_thm thm context = context
1.813 + |> Data.map (map_relator_eq (Item_Net.remove thm))
1.814 + |> Data.map (map_relator_eq_raw
1.815 + (Item_Net.remove (abstract_equalities_relator_eq (Context.proof_of context) thm)))
1.816 + val add = Thm.declaration_attribute add_thm
1.817 + val del = Thm.declaration_attribute del_thm
1.818 + val text = "declaration of relator equality rule (used by transfer method)"
1.819 + val content = Item_Net.content o #relator_eq o Data.get
1.820 + in
1.821 + Attrib.setup name (Attrib.add_del add del) text
1.822 + #> Global_Theory.add_thms_dynamic (name, content)
1.823 + end
1.824 +
1.825 +val relator_domain_setup =
1.826 + let
1.827 + val name = @{binding relator_domain}
1.828 + fun add_thm thm context =
1.829 + let
1.830 + val thm = abstract_domains_relator_domain (Context.proof_of context) thm
1.831 + in
1.832 + context |> Data.map (map_relator_domain (Item_Net.update thm)) |> add_transfer_domain_thm thm
1.833 + end
1.834 + fun del_thm thm context =
1.835 + let
1.836 + val thm = abstract_domains_relator_domain (Context.proof_of context) thm
1.837 + in
1.838 + context |> Data.map (map_relator_domain (Item_Net.remove thm)) |> del_transfer_domain_thm thm
1.839 + end
1.840 + val add = Thm.declaration_attribute add_thm
1.841 + val del = Thm.declaration_attribute del_thm
1.842 + val text = "declaration of relator domain rule (used by transfer method)"
1.843 + val content = Item_Net.content o #relator_domain o Data.get
1.844 + in
1.845 + Attrib.setup name (Attrib.add_del add del) text
1.846 + #> Global_Theory.add_thms_dynamic (name, content)
1.847 + end
1.848 +
1.849 +val setup =
1.850 + relator_eq_setup
1.851 + #> relator_domain_setup
1.852 + #> Attrib.setup @{binding transfer_rule} transfer_attribute
1.853 + "transfer rule for transfer method"
1.854 + #> Global_Theory.add_thms_dynamic
1.855 + (@{binding transfer_raw}, Item_Net.content o #transfer_raw o Data.get)
1.856 + #> Attrib.setup @{binding transfer_domain_rule} transfer_domain_attribute
1.857 + "transfer domain rule for transfer method"
1.858 + #> Attrib.setup @{binding transferred} transferred_attribute_parser
1.859 + "raw theorem transferred to abstract theorem using transfer rules"
1.860 + #> Attrib.setup @{binding untransferred} untransferred_attribute_parser
1.861 + "abstract theorem transferred to raw theorem using transfer rules"
1.862 + #> Global_Theory.add_thms_dynamic
1.863 + (@{binding relator_eq_raw}, Item_Net.content o #relator_eq_raw o Data.get)
1.864 + #> Method.setup @{binding transfer} (transfer_method true)
1.865 + "generic theorem transfer method"
1.866 + #> Method.setup @{binding transfer'} (transfer_method false)
1.867 + "generic theorem transfer method"
1.868 + #> Method.setup @{binding transfer_prover} transfer_prover_method
1.869 + "for proving transfer rules"
1.870 +
1.871 +end