65 val (uncond_rule, cprems) = IsaND.allify_conditions cert (rev Ts') rule'; |
65 val (uncond_rule, cprems) = IsaND.allify_conditions cert (rev Ts') rule'; |
66 |
66 |
67 (* using these names create lambda-abstracted version of the rule *) |
67 (* using these names create lambda-abstracted version of the rule *) |
68 val abstractions = rev (Ts' ~~ tonames); |
68 val abstractions = rev (Ts' ~~ tonames); |
69 val abstract_rule = |
69 val abstract_rule = |
70 Library.foldl (fn (th,((n,ty),ct)) => Thm.abstract_rule n ct th) |
70 fold (fn ((n, ty), ct) => Thm.abstract_rule n ct) |
71 (uncond_rule, abstractions); |
71 abstractions uncond_rule; |
72 in (cprems, abstract_rule) end; |
72 in (cprems, abstract_rule) end; |
73 |
73 |
74 |
74 |
75 (* given names to avoid, and vars that need to be fixed, it gives |
75 (* given names to avoid, and vars that need to be fixed, it gives |
76 unique new names to the vars so that they can be fixed as free |
76 unique new names to the vars so that they can be fixed as free |
81 ie ?z in C ?z ?x ==> A ?x ?y = B ?x ?y *) |
81 ie ?z in C ?z ?x ==> A ?x ?y = B ?x ?y *) |
82 fun mk_renamings ctxt tgt rule_inst = |
82 fun mk_renamings ctxt tgt rule_inst = |
83 let |
83 let |
84 val rule_conds = Thm.prems_of rule_inst; |
84 val rule_conds = Thm.prems_of rule_inst; |
85 val (_, cond_vs) = |
85 val (_, cond_vs) = |
86 Library.foldl (fn ((tyvs, vs), t) => |
86 fold (fn t => fn (tyvs, vs) => |
87 (union (op =) (Misc_Legacy.term_tvars t) tyvs, |
87 (union (op =) (Misc_Legacy.term_tvars t) tyvs, |
88 union (op =) (map Term.dest_Var (Misc_Legacy.term_vars t)) vs)) |
88 union (op =) (map Term.dest_Var (Misc_Legacy.term_vars t)) vs)) rule_conds ([], []); |
89 (([], []), rule_conds); |
|
90 val termvars = map Term.dest_Var (Misc_Legacy.term_vars tgt); |
89 val termvars = map Term.dest_Var (Misc_Legacy.term_vars tgt); |
91 val vars_to_fix = union (op =) termvars cond_vs; |
90 val vars_to_fix = union (op =) termvars cond_vs; |
92 val ys = IsaND.variant_names ctxt (tgt :: rule_conds) (map (fst o fst) vars_to_fix); |
91 val ys = IsaND.variant_names ctxt (tgt :: rule_conds) (map (fst o fst) vars_to_fix); |
93 in map2 (fn (xi, T) => fn y => ((xi, T), Free (y, T))) vars_to_fix ys end; |
92 in map2 (fn (xi, T) => fn y => ((xi, T), Free (y, T))) vars_to_fix ys end; |
94 |
93 |
95 (* make a new fresh typefree instantiation for the given tvar *) |
94 (* make a new fresh typefree instantiation for the given tvar *) |
96 fun new_tfree (tv as (ix,sort), (pairs,used)) = |
95 fun new_tfree (tv as (ix,sort)) (pairs, used) = |
97 let val v = singleton (Name.variant_list used) (string_of_indexname ix) |
96 let val v = singleton (Name.variant_list used) (string_of_indexname ix) |
98 in ((ix,(sort,TFree(v,sort)))::pairs, v::used) end; |
97 in ((ix,(sort,TFree(v,sort)))::pairs, v::used) end; |
99 |
98 |
100 |
99 |
101 (* make instantiations to fix type variables that are not |
100 (* make instantiations to fix type variables that are not |
102 already instantiated (in ignore_ixs) from the list of terms. *) |
101 already instantiated (in ignore_ixs) from the list of terms. *) |
103 fun mk_fixtvar_tyinsts ignore_insts ts = |
102 fun mk_fixtvar_tyinsts ignore_insts ts = |
104 let |
103 let |
105 val ignore_ixs = map fst ignore_insts; |
104 val ignore_ixs = map fst ignore_insts; |
106 val (tvars, tfrees) = |
105 val (tvars, tfrees) = |
107 List.foldr (fn (t, (varixs, tfrees)) => |
106 fold_rev (fn t => fn (varixs, tfrees) => |
108 (Misc_Legacy.add_term_tvars (t,varixs), |
107 (Misc_Legacy.add_term_tvars (t,varixs), |
109 Misc_Legacy.add_term_tfrees (t,tfrees))) ([],[]) ts; |
108 Misc_Legacy.add_term_tfrees (t,tfrees))) ts ([], []); |
110 val unfixed_tvars = filter (fn (ix,s) => not (member (op =) ignore_ixs ix)) tvars; |
109 val unfixed_tvars = filter (fn (ix,s) => not (member (op =) ignore_ixs ix)) tvars; |
111 val (fixtyinsts, _) = List.foldr new_tfree ([], map fst tfrees) unfixed_tvars |
110 val (fixtyinsts, _) = fold_rev new_tfree unfixed_tvars ([], map fst tfrees) |
112 in (fixtyinsts, tfrees) end; |
111 in (fixtyinsts, tfrees) end; |
113 |
112 |
114 |
113 |
115 (* cross-instantiate the instantiations - ie for each instantiation |
114 (* cross-instantiate the instantiations - ie for each instantiation |
116 replace all occurances in other instantiations - no loops are possible |
115 replace all occurances in other instantiations - no loops are possible |
174 val FakeTs_tyinst = map (apsnd (Term.typ_subst_TVars term_typ_inst)) FakeTs; |
173 val FakeTs_tyinst = map (apsnd (Term.typ_subst_TVars term_typ_inst)) FakeTs; |
175 val Ts_tyinst = map (apsnd (Term.typ_subst_TVars term_typ_inst)) Ts; |
174 val Ts_tyinst = map (apsnd (Term.typ_subst_TVars term_typ_inst)) Ts; |
176 |
175 |
177 (* type-instantiate the var instantiations *) |
176 (* type-instantiate the var instantiations *) |
178 val insts_tyinst = |
177 val insts_tyinst = |
179 List.foldr (fn ((ix,(ty,t)),insts_tyinst) => |
178 fold_rev (fn (ix, (ty, t)) => fn insts_tyinst => |
180 (ix, (Term.typ_subst_TVars term_typ_inst ty, Term.subst_TVars term_typ_inst t)) |
179 (ix, (Term.typ_subst_TVars term_typ_inst ty, Term.subst_TVars term_typ_inst t)) |
181 :: insts_tyinst) |
180 :: insts_tyinst) unprepinsts []; |
182 [] unprepinsts; |
|
183 |
181 |
184 (* cross-instantiate *) |
182 (* cross-instantiate *) |
185 val insts_tyinst_inst = cross_inst insts_tyinst; |
183 val insts_tyinst_inst = cross_inst insts_tyinst; |
186 |
184 |
187 (* create certms of instantiations *) |
185 (* create certms of instantiations *) |