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