equal
deleted
inserted
replaced
79 (*** Dependency analysis for congruence rules ***) |
79 (*** Dependency analysis for congruence rules ***) |
80 |
80 |
81 fun branch_vars t = |
81 fun branch_vars t = |
82 let |
82 let |
83 val t' = snd (dest_all_all t) |
83 val t' = snd (dest_all_all t) |
84 val assumes = Logic.strip_imp_prems t' |
84 val (assumes, concl) = Logic.strip_horn t' |
85 val concl = Logic.strip_imp_concl t' |
|
86 in (fold (curry add_term_vars) assumes [], term_vars concl) |
85 in (fold (curry add_term_vars) assumes [], term_vars concl) |
87 end |
86 end |
88 |
87 |
89 fun cong_deps crule = |
88 fun cong_deps crule = |
90 let |
89 let |
102 |
101 |
103 (* Called on the INSTANTIATED branches of the congruence rule *) |
102 (* Called on the INSTANTIATED branches of the congruence rule *) |
104 fun mk_branch ctx t = |
103 fun mk_branch ctx t = |
105 let |
104 let |
106 val (ctx', fixes, impl) = dest_all_all_ctx ctx t |
105 val (ctx', fixes, impl) = dest_all_all_ctx ctx t |
107 val assms = Logic.strip_imp_prems impl |
106 val (assms, concl) = Logic.strip_horn impl |
108 in |
107 in |
109 (ctx', fixes, assms, rhs_of (Logic.strip_imp_concl impl)) |
108 (ctx', fixes, assms, rhs_of concl) |
110 end |
109 end |
111 |
110 |
112 fun find_cong_rule ctx fvar h ((r,dep)::rs) t = |
111 fun find_cong_rule ctx fvar h ((r,dep)::rs) t = |
113 (let |
112 (let |
114 val thy = ProofContext.theory_of ctx |
113 val thy = ProofContext.theory_of ctx |