equal
deleted
inserted
replaced
89 |
89 |
90 |
90 |
91 (* Theory dependencies. *) |
91 (* Theory dependencies. *) |
92 val acc_induct_rule = @{thm accp_induct_rule} |
92 val acc_induct_rule = @{thm accp_induct_rule} |
93 |
93 |
94 val ex1_implies_ex = @{thm FunDef.fundef_ex1_existence} |
94 val ex1_implies_ex = @{thm Fun_Def.fundef_ex1_existence} |
95 val ex1_implies_un = @{thm FunDef.fundef_ex1_uniqueness} |
95 val ex1_implies_un = @{thm Fun_Def.fundef_ex1_uniqueness} |
96 val ex1_implies_iff = @{thm FunDef.fundef_ex1_iff} |
96 val ex1_implies_iff = @{thm Fun_Def.fundef_ex1_iff} |
97 |
97 |
98 val acc_downward = @{thm accp_downward} |
98 val acc_downward = @{thm accp_downward} |
99 val accI = @{thm accp.accI} |
99 val accI = @{thm accp.accI} |
100 val case_split = @{thm HOL.case_split} |
100 val case_split = @{thm HOL.case_split} |
101 val fundef_default_value = @{thm FunDef.fundef_default_value} |
101 val fundef_default_value = @{thm Fun_Def.fundef_default_value} |
102 val not_acc_down = @{thm not_accp_down} |
102 val not_acc_down = @{thm not_accp_down} |
103 |
103 |
104 |
104 |
105 |
105 |
106 fun find_calls tree = |
106 fun find_calls tree = |
655 end |
655 end |
656 |
656 |
657 fun define_function fdefname (fname, mixfix) domT ranT G default lthy = |
657 fun define_function fdefname (fname, mixfix) domT ranT G default lthy = |
658 let |
658 let |
659 val f_def = |
659 val f_def = |
660 Abs ("x", domT, Const (@{const_name FunDef.THE_default}, ranT --> (ranT --> boolT) --> ranT) |
660 Abs ("x", domT, Const (@{const_name Fun_Def.THE_default}, ranT --> (ranT --> boolT) --> ranT) |
661 $ (default $ Bound 0) $ Abs ("y", ranT, G $ Bound 1 $ Bound 0)) |
661 $ (default $ Bound 0) $ Abs ("y", ranT, G $ Bound 1 $ Bound 0)) |
662 |> Syntax.check_term lthy |
662 |> Syntax.check_term lthy |
663 in |
663 in |
664 Local_Theory.define |
664 Local_Theory.define |
665 ((Binding.name (function_name fname), mixfix), |
665 ((Binding.name (function_name fname), mixfix), |
879 |
879 |
880 |
880 |
881 (** Termination rule **) |
881 (** Termination rule **) |
882 |
882 |
883 val wf_induct_rule = @{thm Wellfounded.wfP_induct_rule} |
883 val wf_induct_rule = @{thm Wellfounded.wfP_induct_rule} |
884 val wf_in_rel = @{thm FunDef.wf_in_rel} |
884 val wf_in_rel = @{thm Fun_Def.wf_in_rel} |
885 val in_rel_def = @{thm FunDef.in_rel_def} |
885 val in_rel_def = @{thm Fun_Def.in_rel_def} |
886 |
886 |
887 fun mk_nest_term_case thy globals R' ihyp clause = |
887 fun mk_nest_term_case thy globals R' ihyp clause = |
888 let |
888 let |
889 val Globals {z, ...} = globals |
889 val Globals {z, ...} = globals |
890 val ClauseInfo {cdata = ClauseContext {qs, cqs, ags, lhs, case_hyp, ...}, tree, |
890 val ClauseInfo {cdata = ClauseContext {qs, cqs, ags, lhs, case_hyp, ...}, tree, |
941 val acc_R = mk_acc domT R |
941 val acc_R = mk_acc domT R |
942 |
942 |
943 val R' = Free ("R", fastype_of R) |
943 val R' = Free ("R", fastype_of R) |
944 |
944 |
945 val Rrel = Free ("R", HOLogic.mk_setT (HOLogic.mk_prodT (domT, domT))) |
945 val Rrel = Free ("R", HOLogic.mk_setT (HOLogic.mk_prodT (domT, domT))) |
946 val inrel_R = Const (@{const_name FunDef.in_rel}, |
946 val inrel_R = Const (@{const_name Fun_Def.in_rel}, |
947 HOLogic.mk_setT (HOLogic.mk_prodT (domT, domT)) --> fastype_of R) $ Rrel |
947 HOLogic.mk_setT (HOLogic.mk_prodT (domT, domT)) --> fastype_of R) $ Rrel |
948 |
948 |
949 val wfR' = HOLogic.mk_Trueprop (Const (@{const_name Wellfounded.wfP}, |
949 val wfR' = HOLogic.mk_Trueprop (Const (@{const_name Wellfounded.wfP}, |
950 (domT --> domT --> boolT) --> boolT) $ R') |
950 (domT --> domT --> boolT) --> boolT) $ R') |
951 |> cterm_of thy (* "wf R'" *) |
951 |> cterm_of thy (* "wf R'" *) |