392 val Globals {h, domT, ranT, x, ...} = globals |
392 val Globals {h, domT, ranT, x, ...} = globals |
393 |
393 |
394 (* Inductive Hypothesis: !!z. (z,x):R ==> EX!y. (z,y):G *) |
394 (* Inductive Hypothesis: !!z. (z,x):R ==> EX!y. (z,y):G *) |
395 val ihyp = Logic.all_const domT $ Abs ("z", domT, |
395 val ihyp = Logic.all_const domT $ Abs ("z", domT, |
396 Logic.mk_implies (HOLogic.mk_Trueprop (R $ Bound 0 $ x), |
396 Logic.mk_implies (HOLogic.mk_Trueprop (R $ Bound 0 $ x), |
397 HOLogic.mk_Trueprop (Const (@{const_name Ex1}, (ranT --> boolT) --> boolT) $ |
397 HOLogic.mk_Trueprop (Const (\<^const_name>\<open>Ex1\<close>, (ranT --> boolT) --> boolT) $ |
398 Abs ("y", ranT, G $ Bound 1 $ Bound 0)))) |
398 Abs ("y", ranT, G $ Bound 1 $ Bound 0)))) |
399 |> Thm.cterm_of ctxt |
399 |> Thm.cterm_of ctxt |
400 |
400 |
401 val ihyp_thm = Thm.assume ihyp |> Thm.forall_elim_vars 0 |
401 val ihyp_thm = Thm.assume ihyp |> Thm.forall_elim_vars 0 |
402 val ih_intro = ihyp_thm RS (f_def RS ex1_implies_ex) |
402 val ih_intro = ihyp_thm RS (f_def RS ex1_implies_ex) |
492 let |
492 let |
493 val f_def_binding = |
493 val f_def_binding = |
494 Thm.make_def_binding (Config.get lthy function_internals) |
494 Thm.make_def_binding (Config.get lthy function_internals) |
495 (derived_name_suffix defname "_sumC") |
495 (derived_name_suffix defname "_sumC") |
496 val f_def = |
496 val f_def = |
497 Abs ("x", domT, Const (@{const_name Fun_Def.THE_default}, ranT --> (ranT --> boolT) --> ranT) |
497 Abs ("x", domT, Const (\<^const_name>\<open>Fun_Def.THE_default\<close>, ranT --> (ranT --> boolT) --> ranT) |
498 $ (default $ Bound 0) $ Abs ("y", ranT, G $ Bound 1 $ Bound 0)) |
498 $ (default $ Bound 0) $ Abs ("y", ranT, G $ Bound 1 $ Bound 0)) |
499 |> Syntax.check_term lthy |
499 |> Syntax.check_term lthy |
500 in |
500 in |
501 lthy |> Local_Theory.define |
501 lthy |> Local_Theory.define |
502 ((Binding.map_name (suffix "C") fname, mixfix), ((f_def_binding, []), f_def)) |
502 ((Binding.map_name (suffix "C") fname, mixfix), ((f_def_binding, []), f_def)) |
775 |
775 |
776 val ([Rn], ctxt') = Variable.variant_fixes ["R"] ctxt |
776 val ([Rn], ctxt') = Variable.variant_fixes ["R"] ctxt |
777 val R' = Free (Rn, fastype_of R) |
777 val R' = Free (Rn, fastype_of R) |
778 |
778 |
779 val Rrel = Free (Rn, HOLogic.mk_setT (HOLogic.mk_prodT (domT, domT))) |
779 val Rrel = Free (Rn, HOLogic.mk_setT (HOLogic.mk_prodT (domT, domT))) |
780 val inrel_R = Const (@{const_name Fun_Def.in_rel}, |
780 val inrel_R = Const (\<^const_name>\<open>Fun_Def.in_rel\<close>, |
781 HOLogic.mk_setT (HOLogic.mk_prodT (domT, domT)) --> fastype_of R) $ Rrel |
781 HOLogic.mk_setT (HOLogic.mk_prodT (domT, domT)) --> fastype_of R) $ Rrel |
782 |
782 |
783 val wfR' = HOLogic.mk_Trueprop (Const (@{const_name Wellfounded.wfP}, |
783 val wfR' = HOLogic.mk_Trueprop (Const (\<^const_name>\<open>Wellfounded.wfP\<close>, |
784 (domT --> domT --> boolT) --> boolT) $ R') |
784 (domT --> domT --> boolT) --> boolT) $ R') |
785 |> Thm.cterm_of ctxt' (* "wf R'" *) |
785 |> Thm.cterm_of ctxt' (* "wf R'" *) |
786 |
786 |
787 (* Inductive Hypothesis: !!z. (z,x):R' ==> z : acc R *) |
787 (* Inductive Hypothesis: !!z. (z,x):R' ==> z : acc R *) |
788 val ihyp = Logic.all_const domT $ Abs ("z", domT, |
788 val ihyp = Logic.all_const domT $ Abs ("z", domT, |