equal
deleted
inserted
replaced
92 (* ==> library *) |
92 (* ==> library *) |
93 fun unordered_pairs [] = [] |
93 fun unordered_pairs [] = [] |
94 | unordered_pairs (x::xs) = map (pair x) (x::xs) @ unordered_pairs xs |
94 | unordered_pairs (x::xs) = map (pair x) (x::xs) @ unordered_pairs xs |
95 |
95 |
96 |
96 |
97 (* FIXME cf. Term.exists_subterm *) |
97 (* Replaces Frees by name. Works with loose Bounds. *) |
98 fun forall_aterms P (t $ u) = forall_aterms P t andalso forall_aterms P u |
|
99 | forall_aterms P (Abs (_, _, t)) = forall_aterms P t |
|
100 | forall_aterms P a = P a |
|
101 |
|
102 (* FIXME cf. Term.exists_subterm *) |
|
103 fun exists_aterm P = not o forall_aterms (not o P) |
|
104 |
|
105 |
|
106 |
|
107 (* Replaces Frees by name. Probably quicker than Pattern.rewrite_terms, and works with loose Bounds. *) |
|
108 fun replace_frees assoc = |
98 fun replace_frees assoc = |
109 map_aterms (fn c as Free (n, _) => the_default c (AList.lookup (op =) assoc n) |
99 map_aterms (fn c as Free (n, _) => the_default c (AList.lookup (op =) assoc n) |
110 | t => t) |
100 | t => t) |
111 |
101 |
112 |
102 |
114 | rename_bound n _ = raise Match |
104 | rename_bound n _ = raise Match |
115 |
105 |
116 fun mk_forall_rename (n, v) = |
106 fun mk_forall_rename (n, v) = |
117 rename_bound n o Logic.all v |
107 rename_bound n o Logic.all v |
118 |
108 |
119 val dummy_term = Free ("", dummyT) |
|
120 |
|
121 fun forall_intr_rename (n, cv) thm = |
109 fun forall_intr_rename (n, cv) thm = |
122 let |
110 let |
123 val allthm = forall_intr cv thm |
111 val allthm = forall_intr cv thm |
124 val (_ $ abs) = prop_of allthm |
112 val (_ $ abs) = prop_of allthm |
125 in |
113 in |
126 Thm.rename_boundvars abs (Abs (n, dummyT, dummy_term)) allthm |
114 Thm.rename_boundvars abs (Abs (n, dummyT, Term.dummy_pattern dummyT)) allthm |
127 end |
115 end |
128 |
116 |
129 |
117 |
130 (* Returns the frees in a term in canonical order, excluding the fixes from the context *) |
118 (* Returns the frees in a term in canonical order, excluding the fixes from the context *) |
131 fun frees_in_term ctxt t = |
119 fun frees_in_term ctxt t = |