19 structure Legacy_Transfer : LEGACY_TRANSFER = |
19 structure Legacy_Transfer : LEGACY_TRANSFER = |
20 struct |
20 struct |
21 |
21 |
22 (* data administration *) |
22 (* data administration *) |
23 |
23 |
24 val direction_of = Thm.dest_binop o Thm.dest_arg o cprop_of; |
24 val direction_of = Thm.dest_binop o Thm.dest_arg o Thm.cprop_of; |
25 |
25 |
26 val transfer_morphism_key = Drule.strip_imp_concl (Thm.cprop_of @{thm transfer_morphismI}); |
26 val transfer_morphism_key = Drule.strip_imp_concl (Thm.cprop_of @{thm transfer_morphismI}); |
27 |
27 |
28 fun check_morphism_key ctxt key = |
28 fun check_morphism_key ctxt key = |
29 let |
29 let |
87 fun get_by_prop context t = |
87 fun get_by_prop context t = |
88 let |
88 let |
89 val tys = map snd (Term.add_vars t []); |
89 val tys = map snd (Term.add_vars t []); |
90 val _ = if null tys then error "Transfer: unable to guess instance" else (); |
90 val _ = if null tys then error "Transfer: unable to guess instance" else (); |
91 val tyss = splits (curry Type.could_unify) tys; |
91 val tyss = splits (curry Type.could_unify) tys; |
92 val get_ty = typ_of o ctyp_of_term o fst o direction_of; |
92 val get_ty = Thm.typ_of o Thm.ctyp_of_term o fst o direction_of; |
93 val insts = map_filter (fn tys => get_first (fn (k, e) => |
93 val insts = map_filter (fn tys => get_first (fn (k, e) => |
94 if Type.could_unify (hd tys, range_type (get_ty k)) |
94 if Type.could_unify (hd tys, range_type (get_ty k)) |
95 then SOME (direction_of k, transfer_rules_of e) |
95 then SOME (direction_of k, transfer_rules_of e) |
96 else NONE) (Data.get context)) tyss; |
96 else NONE) (Data.get context)) tyss; |
97 val _ = if null insts then |
97 val _ = if null insts then |
112 val (aT, bT) = (Term.range_type T, Term.domain_type T); |
112 val (aT, bT) = (Term.range_type T, Term.domain_type T); |
113 |
113 |
114 (* determine variables to transfer *) |
114 (* determine variables to transfer *) |
115 val ctxt3 = ctxt2 |
115 val ctxt3 = ctxt2 |
116 |> Variable.declare_thm thm |
116 |> Variable.declare_thm thm |
117 |> Variable.declare_term (term_of a) |
117 |> Variable.declare_term (Thm.term_of a) |
118 |> Variable.declare_term (term_of D); |
118 |> Variable.declare_term (Thm.term_of D); |
119 val vars = filter (fn ((v, _), T) => Type.could_unify (T, aT) andalso |
119 val vars = filter (fn ((v, _), T) => Type.could_unify (T, aT) andalso |
120 not (member (op =) leave v)) (Term.add_vars (Thm.prop_of thm) []); |
120 not (member (op =) leave v)) (Term.add_vars (Thm.prop_of thm) []); |
121 val c_vars = map (Proof_Context.cterm_of ctxt3 o Var) vars; |
121 val c_vars = map (Proof_Context.cterm_of ctxt3 o Var) vars; |
122 val (vs', ctxt4) = Variable.variant_fixes (map (fst o fst) vars) ctxt3; |
122 val (vs', ctxt4) = Variable.variant_fixes (map (fst o fst) vars) ctxt3; |
123 val c_vars' = map (Proof_Context.cterm_of ctxt3 o (fn v => Free (v, bT))) vs'; |
123 val c_vars' = map (Proof_Context.cterm_of ctxt3 o (fn v => Free (v, bT))) vs'; |
129 val simpset = |
129 val simpset = |
130 put_simpset HOL_ss ctxt5 addsimps (inj @ embed @ return) |
130 put_simpset HOL_ss ctxt5 addsimps (inj @ embed @ return) |
131 |> fold Simplifier.add_cong cong; |
131 |> fold Simplifier.add_cong cong; |
132 val thm' = thm |
132 val thm' = thm |
133 |> Drule.cterm_instantiate (c_vars ~~ c_exprs') |
133 |> Drule.cterm_instantiate (c_vars ~~ c_exprs') |
134 |> fold_rev Thm.implies_intr (map cprop_of hyps) |
134 |> fold_rev Thm.implies_intr (map Thm.cprop_of hyps) |
135 |> Simplifier.asm_full_simplify simpset |
135 |> Simplifier.asm_full_simplify simpset |
136 in singleton (Variable.export ctxt5 ctxt1) thm' end; |
136 in singleton (Variable.export ctxt5 ctxt1) thm' end; |
137 |
137 |
138 fun transfer_thm_multiple insts leave ctxt thm = |
138 fun transfer_thm_multiple insts leave ctxt thm = |
139 map (fn inst => transfer_thm inst leave ctxt thm) insts; |
139 map (fn inst => transfer_thm inst leave ctxt thm) insts; |