906 |> Thm.forall_intr (cterm_of thy Rrel) |
906 |> Thm.forall_intr (cterm_of thy Rrel) |
907 end |
907 end |
908 |
908 |
909 |
909 |
910 |
910 |
911 (* Tail recursion (probably very fragile) |
|
912 * |
|
913 * FIXME: |
|
914 * - Need to do forall_elim_vars on psimps: Unneccesary, if psimps would be taken from the same context. |
|
915 * - Must we really replace the fvar by f here? |
|
916 * - Splitting is not configured automatically: Problems with case? |
|
917 *) |
|
918 fun mk_trsimps octxt globals f G R f_def R_cases G_induct clauses psimps = |
|
919 let |
|
920 val Globals {domT, ranT, fvar, ...} = globals |
|
921 |
|
922 val R_cases = Thm.forall_elim_vars 0 R_cases (* FIXME: Should be already in standard form. *) |
|
923 |
|
924 val graph_implies_dom = (* "G ?x ?y ==> dom ?x" *) |
|
925 Goal.prove octxt ["x", "y"] [HOLogic.mk_Trueprop (G $ Free ("x", domT) $ Free ("y", ranT))] |
|
926 (HOLogic.mk_Trueprop (mk_acc domT R $ Free ("x", domT))) |
|
927 (fn {prems=[a], ...} => |
|
928 ((rtac (G_induct OF [a])) |
|
929 THEN_ALL_NEW rtac accI |
|
930 THEN_ALL_NEW etac R_cases |
|
931 THEN_ALL_NEW asm_full_simp_tac (simpset_of octxt)) 1) |
|
932 |
|
933 val default_thm = |
|
934 forall_intr_vars graph_implies_dom COMP (f_def COMP fundef_default_value) |
|
935 |
|
936 fun mk_trsimp clause psimp = |
|
937 let |
|
938 val ClauseInfo {qglr = (oqs, _, _, _), cdata = |
|
939 ClauseContext {ctxt, cqs, gs, lhs, rhs, ...}, ...} = clause |
|
940 val thy = ProofContext.theory_of ctxt |
|
941 val rhs_f = Pattern.rewrite_term thy [(fvar, f)] [] rhs |
|
942 |
|
943 val trsimp = Logic.list_implies(gs, |
|
944 HOLogic.mk_Trueprop (HOLogic.mk_eq(f $ lhs, rhs_f))) (* "f lhs = rhs" *) |
|
945 val lhs_acc = (mk_acc domT R $ lhs) (* "acc R lhs" *) |
|
946 fun simp_default_tac ss = |
|
947 asm_full_simp_tac (ss addsimps [default_thm, Let_def]) |
|
948 in |
|
949 Goal.prove ctxt [] [] trsimp (fn _ => |
|
950 rtac (instantiate' [] [SOME (cterm_of thy lhs_acc)] case_split) 1 |
|
951 THEN (rtac (Thm.forall_elim_vars 0 psimp) THEN_ALL_NEW assume_tac) 1 |
|
952 THEN (simp_default_tac (simpset_of ctxt) 1) |
|
953 THEN TRY ((etac not_acc_down 1) |
|
954 THEN ((etac R_cases) |
|
955 THEN_ALL_NEW (simp_default_tac (simpset_of ctxt))) 1)) |
|
956 |> fold_rev forall_intr_rename (map fst oqs ~~ cqs) |
|
957 end |
|
958 in |
|
959 map2 mk_trsimp clauses psimps |
|
960 end |
|
961 |
|
962 |
|
963 (* nominal *) |
911 (* nominal *) |
964 fun prepare_nominal_function config defname [((fname, fT), mixfix)] abstract_qglrs lthy = |
912 fun prepare_nominal_function config defname [((fname, fT), mixfix)] abstract_qglrs lthy = |
965 let |
913 let |
966 val FunctionConfig {domintros, tailrec, default=default_opt, ...} = config |
914 val FunctionConfig {domintros, default=default_opt, ...} = config |
967 |
915 |
968 val default_str = the_default "%x. undefined" default_opt (*FIXME dynamic scoping*) |
916 val default_str = the_default "%x. undefined" default_opt (*FIXME dynamic scoping*) |
969 val fvar = Free (fname, fT) |
917 val fvar = Free (fname, fT) |
970 val domT = domain_type fT |
918 val domT = domain_type fT |
971 val ranT = range_type fT |
919 val ranT = range_type fT |
1024 |
972 |
1025 val (goalstate, values) = PROFILE "prove_stuff" |
973 val (goalstate, values) = PROFILE "prove_stuff" |
1026 (prove_stuff lthy globals G f R xclauses complete compat |
974 (prove_stuff lthy globals G f R xclauses complete compat |
1027 compat_store G_elim G_eqvt) f_defthm |
975 compat_store G_elim G_eqvt) f_defthm |
1028 |
976 |
1029 val mk_trsimps = |
|
1030 mk_trsimps lthy globals f G R f_defthm R_elim G_induct xclauses |
|
1031 |
|
1032 fun mk_partial_rules provedgoal = |
977 fun mk_partial_rules provedgoal = |
1033 let |
978 let |
1034 val newthy = theory_of_thm provedgoal (*FIXME*) |
979 val newthy = theory_of_thm provedgoal (*FIXME*) |
1035 |
980 |
1036 val ((graph_is_function, complete_thm), _) = |
981 val ((graph_is_function, complete_thm), _) = |
1052 |
997 |
1053 val dom_intros = |
998 val dom_intros = |
1054 if domintros then SOME (PROFILE "Proving domain introduction rules" |
999 if domintros then SOME (PROFILE "Proving domain introduction rules" |
1055 (map (mk_domain_intro lthy globals R R_elim)) xclauses) |
1000 (map (mk_domain_intro lthy globals R R_elim)) xclauses) |
1056 else NONE |
1001 else NONE |
1057 val trsimps = if tailrec then SOME (mk_trsimps psimps) else NONE |
|
1058 |
1002 |
1059 in |
1003 in |
1060 FunctionResult {fs=[f], G=G, R=R, cases=complete_thm, |
1004 FunctionResult {fs=[f], G=G, R=R, cases=complete_thm, |
1061 psimps=psimps, simple_pinducts=[simple_pinduct], |
1005 psimps=psimps, simple_pinducts=[simple_pinduct], |
1062 termination=total_intro, trsimps=trsimps, |
1006 termination=total_intro, domintros=dom_intros} |
1063 domintros=dom_intros} |
|
1064 end |
1007 end |
1065 in |
1008 in |
1066 ((f, goalstate, mk_partial_rules), lthy) |
1009 ((f, goalstate, mk_partial_rules), lthy) |
1067 end |
1010 end |
1068 |
1011 |