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