259 fun is_type_surely_infinite ctxt sound infinite_Ts T = |
259 fun is_type_surely_infinite ctxt sound infinite_Ts T = |
260 tiny_card_of_type ctxt sound (map (rpair 0) infinite_Ts) 1 T = 0 |
260 tiny_card_of_type ctxt sound (map (rpair 0) infinite_Ts) 1 T = 0 |
261 |
261 |
262 (* Simple simplifications to ensure that sort annotations don't leave a trail of |
262 (* Simple simplifications to ensure that sort annotations don't leave a trail of |
263 spurious "True"s. *) |
263 spurious "True"s. *) |
264 fun s_not (Const (\<^const_name>\<open>All\<close>, T) $ Abs (s, T', t')) = |
264 fun s_not \<^Const_>\<open>All T for \<open>Abs (s, T', t')\<close>\<close> = \<^Const>\<open>Ex T for \<open>Abs (s, T', s_not t')\<close>\<close> |
265 Const (\<^const_name>\<open>Ex\<close>, T) $ Abs (s, T', s_not t') |
265 | s_not \<^Const_>\<open>Ex T for \<open>Abs (s, T', t')\<close>\<close> = \<^Const>\<open>All T for \<open>Abs (s, T', s_not t')\<close>\<close> |
266 | s_not (Const (\<^const_name>\<open>Ex\<close>, T) $ Abs (s, T', t')) = |
266 | s_not \<^Const_>\<open>implies for t1 t2\<close> = \<^Const>\<open>conj for t1 \<open>s_not t2\<close>\<close> |
267 Const (\<^const_name>\<open>All\<close>, T) $ Abs (s, T', s_not t') |
267 | s_not \<^Const_>\<open>conj for t1 t2\<close> = \<^Const>\<open>disj for \<open>s_not t1\<close> \<open>s_not t2\<close>\<close> |
268 | s_not (\<^const>\<open>HOL.implies\<close> $ t1 $ t2) = \<^const>\<open>HOL.conj\<close> $ t1 $ s_not t2 |
268 | s_not \<^Const_>\<open>disj for t1 t2\<close> = \<^Const>\<open>conj for \<open>s_not t1\<close> \<open>s_not t2\<close>\<close> |
269 | s_not (\<^const>\<open>HOL.conj\<close> $ t1 $ t2) = |
269 | s_not \<^Const_>\<open>False\<close> = \<^Const>\<open>True\<close> |
270 \<^const>\<open>HOL.disj\<close> $ s_not t1 $ s_not t2 |
270 | s_not \<^Const_>\<open>True\<close> = \<^Const>\<open>False\<close> |
271 | s_not (\<^const>\<open>HOL.disj\<close> $ t1 $ t2) = |
271 | s_not \<^Const_>\<open>Not for t\<close> = t |
272 \<^const>\<open>HOL.conj\<close> $ s_not t1 $ s_not t2 |
272 | s_not t = \<^Const>\<open>Not for t\<close> |
273 | s_not (\<^const>\<open>False\<close>) = \<^const>\<open>True\<close> |
273 |
274 | s_not (\<^const>\<open>True\<close>) = \<^const>\<open>False\<close> |
274 fun s_conj (\<^Const_>\<open>True\<close>, t2) = t2 |
275 | s_not (\<^const>\<open>Not\<close> $ t) = t |
275 | s_conj (t1, \<^Const_>\<open>True\<close>) = t1 |
276 | s_not t = \<^const>\<open>Not\<close> $ t |
276 | s_conj (\<^Const_>\<open>False\<close>, _) = \<^Const>\<open>False\<close> |
277 |
277 | s_conj (_, \<^Const_>\<open>False\<close>) = \<^Const>\<open>False\<close> |
278 fun s_conj (\<^const>\<open>True\<close>, t2) = t2 |
|
279 | s_conj (t1, \<^const>\<open>True\<close>) = t1 |
|
280 | s_conj (\<^const>\<open>False\<close>, _) = \<^const>\<open>False\<close> |
|
281 | s_conj (_, \<^const>\<open>False\<close>) = \<^const>\<open>False\<close> |
|
282 | s_conj (t1, t2) = if t1 aconv t2 then t1 else HOLogic.mk_conj (t1, t2) |
278 | s_conj (t1, t2) = if t1 aconv t2 then t1 else HOLogic.mk_conj (t1, t2) |
283 |
279 |
284 fun s_disj (\<^const>\<open>False\<close>, t2) = t2 |
280 fun s_disj (\<^Const_>\<open>False\<close>, t2) = t2 |
285 | s_disj (t1, \<^const>\<open>False\<close>) = t1 |
281 | s_disj (t1, \<^Const_>\<open>False\<close>) = t1 |
286 | s_disj (\<^const>\<open>True\<close>, _) = \<^const>\<open>True\<close> |
282 | s_disj (\<^Const_>\<open>True\<close>, _) = \<^Const>\<open>True\<close> |
287 | s_disj (_, \<^const>\<open>True\<close>) = \<^const>\<open>True\<close> |
283 | s_disj (_, \<^Const_>\<open>True\<close>) = \<^Const>\<open>True\<close> |
288 | s_disj (t1, t2) = if t1 aconv t2 then t1 else HOLogic.mk_disj (t1, t2) |
284 | s_disj (t1, t2) = if t1 aconv t2 then t1 else HOLogic.mk_disj (t1, t2) |
289 |
285 |
290 fun s_imp (\<^const>\<open>True\<close>, t2) = t2 |
286 fun s_imp (\<^Const_>\<open>True\<close>, t2) = t2 |
291 | s_imp (t1, \<^const>\<open>False\<close>) = s_not t1 |
287 | s_imp (t1, \<^Const_>\<open>False\<close>) = s_not t1 |
292 | s_imp (\<^const>\<open>False\<close>, _) = \<^const>\<open>True\<close> |
288 | s_imp (\<^Const_>\<open>False\<close>, _) = \<^Const>\<open>True\<close> |
293 | s_imp (_, \<^const>\<open>True\<close>) = \<^const>\<open>True\<close> |
289 | s_imp (_, \<^Const_>\<open>True\<close>) = \<^Const>\<open>True\<close> |
294 | s_imp p = HOLogic.mk_imp p |
290 | s_imp p = HOLogic.mk_imp p |
295 |
291 |
296 fun s_iff (\<^const>\<open>True\<close>, t2) = t2 |
292 fun s_iff (\<^Const_>\<open>True\<close>, t2) = t2 |
297 | s_iff (t1, \<^const>\<open>True\<close>) = t1 |
293 | s_iff (t1, \<^Const_>\<open>True\<close>) = t1 |
298 | s_iff (\<^const>\<open>False\<close>, t2) = s_not t2 |
294 | s_iff (\<^Const_>\<open>False\<close>, t2) = s_not t2 |
299 | s_iff (t1, \<^const>\<open>False\<close>) = s_not t1 |
295 | s_iff (t1, \<^Const_>\<open>False\<close>) = s_not t1 |
300 | s_iff (t1, t2) = if t1 aconv t2 then \<^const>\<open>True\<close> else HOLogic.eq_const HOLogic.boolT $ t1 $ t2 |
296 | s_iff (t1, t2) = if t1 aconv t2 then \<^Const>\<open>True\<close> else HOLogic.eq_const HOLogic.boolT $ t1 $ t2 |
301 |
297 |
302 fun close_form t = |
298 fun close_form t = |
303 fold (fn ((s, i), T) => fn t' => |
299 fold (fn ((s, i), T) => fn t' => |
304 Logic.all_const T $ Abs (s, T, abstract_over (Var ((s, i), T), t'))) |
300 Logic.all_const T $ Abs (s, T, abstract_over (Var ((s, i), T), t'))) |
305 (Term.add_vars t []) t |
301 (Term.add_vars t []) t |
350 |> Thm.prop_of |> Logic.dest_equals |> snd |
346 |> Thm.prop_of |> Logic.dest_equals |> snd |
351 else |
347 else |
352 t |
348 t |
353 |
349 |
354 fun unextensionalize_def t = |
350 fun unextensionalize_def t = |
355 case t of |
351 (case t of |
356 \<^const>\<open>Trueprop\<close> $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ lhs $ rhs) => |
352 \<^Const_>\<open>Trueprop for \<^Const_>\<open>HOL.eq _ for lhs rhs\<close>\<close> => |
357 (case strip_comb lhs of |
353 (case strip_comb lhs of |
358 (c as Const (_, T), args) => |
354 (c as Const (_, T), args) => |
359 if forall is_Var args andalso not (has_duplicates (op =) args) then |
355 if forall is_Var args andalso not (has_duplicates (op =) args) then |
360 \<^const>\<open>Trueprop\<close> |
356 \<^Const>\<open>Trueprop for \<^Const>\<open>HOL.eq T for c \<open>fold_rev lambda args rhs\<close>\<close>\<close> |
361 $ (Const (\<^const_name>\<open>HOL.eq\<close>, T --> T --> \<^typ>\<open>bool\<close>) |
357 else t |
362 $ c $ fold_rev lambda args rhs) |
358 | _ => t) |
363 else |
359 | _ => t) |
364 t |
|
365 | _ => t) |
|
366 | _ => t |
|
367 |
360 |
368 (* Converts an elim-rule into an equivalent theorem that does not have the |
361 (* Converts an elim-rule into an equivalent theorem that does not have the |
369 predicate variable. Leaves other theorems unchanged. We simply instantiate |
362 predicate variable. Leaves other theorems unchanged. We simply instantiate |
370 the conclusion variable to "False". (Cf. "transform_elim_theorem" in |
363 the conclusion variable to "False". (Cf. "transform_elim_theorem" in |
371 "Meson_Clausify".) *) |
364 "Meson_Clausify".) *) |
372 fun transform_elim_prop t = |
365 fun transform_elim_prop t = |
373 case Logic.strip_imp_concl t of |
366 case Logic.strip_imp_concl t of |
374 \<^const>\<open>Trueprop\<close> $ Var (z, \<^typ>\<open>bool\<close>) => |
367 \<^Const_>\<open>Trueprop for \<open>Var (z, \<^typ>\<open>bool\<close>)\<close>\<close> => subst_Vars [(z, \<^Const>\<open>False\<close>)] t |
375 subst_Vars [(z, \<^const>\<open>False\<close>)] t |
368 | Var (z, \<^Type>\<open>prop\<close>) => subst_Vars [(z, \<^prop>\<open>False\<close>)] t |
376 | Var (z, \<^typ>\<open>prop\<close>) => subst_Vars [(z, \<^prop>\<open>False\<close>)] t |
|
377 | _ => t |
369 | _ => t |
378 |
370 |
379 fun specialize_type thy (s, T) t = |
371 fun specialize_type thy (s, T) t = |
380 let |
372 let |
381 fun subst_for (Const (s', T')) = |
373 fun subst_for (Const (s', T')) = |