85 prefix for the Skolem constant. Result is a new theory*) |
85 prefix for the Skolem constant. Result is a new theory*) |
86 fun declare_skofuns s th thy = |
86 fun declare_skofuns s th thy = |
87 let val nref = ref 0 |
87 let val nref = ref 0 |
88 fun dec_sko (Const ("Ex",_) $ (xtp as Abs(_,T,p))) (thy, axs) = |
88 fun dec_sko (Const ("Ex",_) $ (xtp as Abs(_,T,p))) (thy, axs) = |
89 (*Existential: declare a Skolem function, then insert into body and continue*) |
89 (*Existential: declare a Skolem function, then insert into body and continue*) |
90 let val cname = Name.internal ("sko_" ^ s ^ "_" ^ Int.toString (inc nref)) |
90 let val cname = "sko_" ^ s ^ "_" ^ Int.toString (inc nref) |
91 val args0 = term_frees xtp (*get the formal parameter list*) |
91 val args0 = term_frees xtp (*get the formal parameter list*) |
92 val Ts = map type_of args0 |
92 val Ts = map type_of args0 |
93 val extraTs = rhs_extra_types (Ts ---> T) xtp |
93 val extraTs = rhs_extra_types (Ts ---> T) xtp |
94 val _ = if null extraTs then () else |
94 val _ = if null extraTs then () else |
95 warning ("Skolemization: extra type vars: " ^ |
95 warning ("Skolemization: extra type vars: " ^ |
96 commas_quote (map (Sign.string_of_typ thy) extraTs)); |
96 commas_quote (map (Sign.string_of_typ thy) extraTs)); |
97 val argsx = map (fn T => Free(gensym"vsk", T)) extraTs |
97 val argsx = map (fn T => Free(gensym"vsk", T)) extraTs |
98 val args = argsx @ args0 |
98 val args = argsx @ args0 |
99 val cT = extraTs ---> Ts ---> T |
99 val cT = extraTs ---> Ts ---> T |
100 val c = Const (Sign.full_name thy cname, cT) |
100 val c = Const (Sign.full_name thy cname, cT) |
101 val rhs = list_abs_free (map dest_Free args, HOLogic.choice_const T $ xtp) |
101 val rhs = list_abs_free (map dest_Free args, HOLogic.choice_const T $ xtp) |
244 fun abstract thy ct = |
244 fun abstract thy ct = |
245 if lambda_free (term_of ct) then (transfer thy (reflexive ct), []) |
245 if lambda_free (term_of ct) then (transfer thy (reflexive ct), []) |
246 else |
246 else |
247 case term_of ct of |
247 case term_of ct of |
248 Abs _ => |
248 Abs _ => |
249 let val cname = Name.internal ("llabs_" ^ s ^ "_" ^ Int.toString (inc nref)) |
249 let val cname = "llabs_" ^ s ^ "_" ^ Int.toString (inc nref) |
250 val _ = assert_eta_free ct; |
250 val _ = assert_eta_free ct; |
251 val (cvs,cta) = dest_abs_list ct |
251 val (cvs,cta) = dest_abs_list ct |
252 val (vs,Tvs) = ListPair.unzip (map (dest_Free o term_of) cvs) |
252 val (vs,Tvs) = ListPair.unzip (map (dest_Free o term_of) cvs) |
253 val _ = Output.debug (fn()=>"Nested lambda: " ^ string_of_cterm cta); |
253 val _ = Output.debug (fn()=>"Nested lambda: " ^ string_of_cterm cta); |
254 val (u'_th,defs) = abstract thy cta |
254 val (u'_th,defs) = abstract thy cta |
503 case Thmtab.lookup (ThmCache.get thy) th of |
503 case Thmtab.lookup (ThmCache.get thy) th of |
504 NONE => |
504 NONE => |
505 (case skolem thy (Thm.transfer thy th) of |
505 (case skolem thy (Thm.transfer thy th) of |
506 NONE => ([th],thy) |
506 NONE => ([th],thy) |
507 | SOME (cls,thy') => |
507 | SOME (cls,thy') => |
508 (Output.debug (fn () => "skolem_cache_thm: " ^ Int.toString (length cls) ^ |
508 (Output.debug (fn () => "skolem_cache_thm: " ^ Int.toString (length cls) ^ |
509 " clauses inserted into cache: " ^ name_or_string th); |
509 " clauses inserted into cache: " ^ name_or_string th); |
510 (cls, ThmCache.put (Thmtab.update (th,cls) (ThmCache.get thy')) thy'))) |
510 (cls, ThmCache.put (Thmtab.update (th,cls) (ThmCache.get thy')) thy'))) |
511 | SOME cls => (cls,thy); |
511 | SOME cls => (cls,thy); |
512 |
512 |
513 (*Exported function to convert Isabelle theorems into axiom clauses*) |
513 (*Exported function to convert Isabelle theorems into axiom clauses*) |