153 val atomic = null o Logic.strip_assums_hyp; |
153 val atomic = null o Logic.strip_assums_hyp; |
154 |
154 |
155 (*ccs contains the names of the constants possessing congruence rules*) |
155 (*ccs contains the names of the constants possessing congruence rules*) |
156 fun add_hidden_vars ccs = |
156 fun add_hidden_vars ccs = |
157 let fun add_hvars tm hvars = case tm of |
157 let fun add_hvars tm hvars = case tm of |
158 Abs(_,_,body) => OldTerm.add_term_vars(body,hvars) |
158 Abs(_,_,body) => Misc_Legacy.add_term_vars(body,hvars) |
159 | _$_ => let val (f,args) = strip_comb tm |
159 | _$_ => let val (f,args) = strip_comb tm |
160 in case f of |
160 in case f of |
161 Const(c,T) => |
161 Const(c,T) => |
162 if member (op =) ccs c |
162 if member (op =) ccs c |
163 then fold_rev add_hvars args hvars |
163 then fold_rev add_hvars args hvars |
164 else OldTerm.add_term_vars (tm, hvars) |
164 else Misc_Legacy.add_term_vars (tm, hvars) |
165 | _ => OldTerm.add_term_vars (tm, hvars) |
165 | _ => Misc_Legacy.add_term_vars (tm, hvars) |
166 end |
166 end |
167 | _ => hvars; |
167 | _ => hvars; |
168 in add_hvars end; |
168 in add_hvars end; |
169 |
169 |
170 fun add_new_asm_vars new_asms = |
170 fun add_new_asm_vars new_asms = |
171 let fun itf (tm, at) vars = |
171 let fun itf (tm, at) vars = |
172 if at then vars else OldTerm.add_term_vars(tm,vars) |
172 if at then vars else Misc_Legacy.add_term_vars(tm,vars) |
173 fun add_list(tm,al,vars) = let val (_,tml) = strip_comb tm |
173 fun add_list(tm,al,vars) = let val (_,tml) = strip_comb tm |
174 in if length(tml)=length(al) |
174 in if length(tml)=length(al) |
175 then fold_rev itf (tml ~~ al) vars |
175 then fold_rev itf (tml ~~ al) vars |
176 else vars |
176 else vars |
177 end |
177 end |
195 val asms = tl(rev(tl(prems_of thm'))) |
195 val asms = tl(rev(tl(prems_of thm'))) |
196 val hvars = fold_rev (add_hidden_vars ccs) (lhs::rhs::asms) [] |
196 val hvars = fold_rev (add_hidden_vars ccs) (lhs::rhs::asms) [] |
197 val hvars = add_new_asm_vars new_asms (rhs,hvars) |
197 val hvars = add_new_asm_vars new_asms (rhs,hvars) |
198 fun it_asms asm hvars = |
198 fun it_asms asm hvars = |
199 if atomic asm then add_new_asm_vars new_asms (asm,hvars) |
199 if atomic asm then add_new_asm_vars new_asms (asm,hvars) |
200 else OldTerm.add_term_frees(asm,hvars) |
200 else Misc_Legacy.add_term_frees(asm,hvars) |
201 val hvars = fold_rev it_asms asms hvars |
201 val hvars = fold_rev it_asms asms hvars |
202 val hvs = map (#1 o dest_Var) hvars |
202 val hvs = map (#1 o dest_Var) hvars |
203 val refl1_tac = refl_tac 1 |
203 val refl1_tac = refl_tac 1 |
204 fun norm_step_tac st = st |> |
204 fun norm_step_tac st = st |> |
205 (case head_of(rhs_of_eq 1 st) of |
205 (case head_of(rhs_of_eq 1 st) of |
541 in Abs("", T, Const(eq,[fT,fT]--->eqT) $ lhs $ rhs) end; |
541 in Abs("", T, Const(eq,[fT,fT]--->eqT) $ lhs $ rhs) end; |
542 |
542 |
543 fun find_subst sg T = |
543 fun find_subst sg T = |
544 let fun find (thm::thms) = |
544 let fun find (thm::thms) = |
545 let val (Const(_,cT), va, vb) = dest_red(hd(prems_of thm)); |
545 let val (Const(_,cT), va, vb) = dest_red(hd(prems_of thm)); |
546 val [P] = subtract (op =) [va, vb] (OldTerm.add_term_vars (concl_of thm, [])); |
546 val [P] = subtract (op =) [va, vb] (Misc_Legacy.add_term_vars (concl_of thm, [])); |
547 val eqT::_ = binder_types cT |
547 val eqT::_ = binder_types cT |
548 in if Sign.typ_instance sg (T,eqT) then SOME(thm,va,vb,P) |
548 in if Sign.typ_instance sg (T,eqT) then SOME(thm,va,vb,P) |
549 else find thms |
549 else find thms |
550 end |
550 end |
551 | find [] = NONE |
551 | find [] = NONE |