equal
deleted
inserted
replaced
69 Long_Name.implode (old_skolem_const_prefix :: map string_of_int [i, j, num_T_args]) |
69 Long_Name.implode (old_skolem_const_prefix :: map string_of_int [i, j, num_T_args]) |
70 |
70 |
71 fun conceal_old_skolem_terms i old_skolems t = |
71 fun conceal_old_skolem_terms i old_skolems t = |
72 if exists_Const (curry (op =) \<^const_name>\<open>Meson.skolem\<close> o fst) t then |
72 if exists_Const (curry (op =) \<^const_name>\<open>Meson.skolem\<close> o fst) t then |
73 let |
73 let |
74 fun aux old_skolems |
74 fun aux old_skolems (t as \<^Const_>\<open>Meson.skolem T for _\<close>) = |
75 (t as (Const (\<^const_name>\<open>Meson.skolem\<close>, Type (_, [_, T])) $ _)) = |
|
76 let |
75 let |
77 val (old_skolems, s) = |
76 val (old_skolems, s) = |
78 if i = ~1 then |
77 if i = ~1 then |
79 (old_skolems, \<^const_name>\<open>undefined\<close>) |
78 (old_skolems, \<^const_name>\<open>undefined\<close>) |
80 else |
79 else |
112 fun reveal_lam_lifted lifted = |
111 fun reveal_lam_lifted lifted = |
113 map_aterms (fn t as Const (s, _) => |
112 map_aterms (fn t as Const (s, _) => |
114 if String.isPrefix lam_lifted_prefix s then |
113 if String.isPrefix lam_lifted_prefix s then |
115 (case AList.lookup (op =) lifted s of |
114 (case AList.lookup (op =) lifted s of |
116 SOME t => |
115 SOME t => |
117 Const (\<^const_name>\<open>Metis.lambda\<close>, dummyT) |
116 \<^Const>\<open>Metis.lambda dummyT\<close> $ |
118 $ map_types (map_type_tvar (K dummyT)) (reveal_lam_lifted lifted t) |
117 map_types (map_type_tvar (K dummyT)) (reveal_lam_lifted lifted t) |
119 | NONE => t) |
118 | NONE => t) |
120 else |
119 else |
121 t |
120 t |
122 | t => t) |
121 | t => t) |
123 |
122 |
188 end |
187 end |
189 | NONE => some (Isa_Raw TrueI)) |
188 | NONE => some (Isa_Raw TrueI)) |
190 end |
189 end |
191 | metis_axiom_of_atp _ _ _ _ = raise Fail "not CNF -- expected formula" |
190 | metis_axiom_of_atp _ _ _ _ = raise Fail "not CNF -- expected formula" |
192 |
191 |
193 fun eliminate_lam_wrappers (Const (\<^const_name>\<open>Metis.lambda\<close>, _) $ t) = eliminate_lam_wrappers t |
192 fun eliminate_lam_wrappers \<^Const_>\<open>Metis.lambda _ for t\<close> = eliminate_lam_wrappers t |
194 | eliminate_lam_wrappers (t $ u) = eliminate_lam_wrappers t $ eliminate_lam_wrappers u |
193 | eliminate_lam_wrappers (t $ u) = eliminate_lam_wrappers t $ eliminate_lam_wrappers u |
195 | eliminate_lam_wrappers (Abs (s, T, t)) = Abs (s, T, eliminate_lam_wrappers t) |
194 | eliminate_lam_wrappers (Abs (s, T, t)) = Abs (s, T, eliminate_lam_wrappers t) |
196 | eliminate_lam_wrappers t = t |
195 | eliminate_lam_wrappers t = t |
197 |
196 |
198 (* Function to generate metis clauses, including comb and type clauses *) |
197 (* Function to generate metis clauses, including comb and type clauses *) |