483 val Globals {x, y, ranT, fvar, ...} = globals |
483 val Globals {x, y, ranT, fvar, ...} = globals |
484 val ClauseInfo {cdata = ClauseContext {lhs, rhs, cqs, ags, case_hyp, ...}, lGI, RCs, ...} = clausei |
484 val ClauseInfo {cdata = ClauseContext {lhs, rhs, cqs, ags, case_hyp, ...}, lGI, RCs, ...} = clausei |
485 val rhsC = Pattern.rewrite_term thy [(fvar, f)] [] rhs |
485 val rhsC = Pattern.rewrite_term thy [(fvar, f)] [] rhs |
486 |
486 |
487 val ih_intro_case = |
487 val ih_intro_case = |
488 full_simplify (Simplifier.global_context thy HOL_basic_ss addsimps [case_hyp]) ih_intro |
488 full_simplify (put_simpset HOL_basic_ss (Proof_Context.init_global thy) addsimps [case_hyp]) |
|
489 ih_intro |
489 |
490 |
490 fun prep_RC (RCInfo {llRI, RIvs, CCas, ...}) = |
491 fun prep_RC (RCInfo {llRI, RIvs, CCas, ...}) = |
491 (llRI RS ih_intro_case) |
492 (llRI RS ih_intro_case) |
492 |> fold_rev (Thm.implies_intr o cprop_of) CCas |
493 |> fold_rev (Thm.implies_intr o cprop_of) CCas |
493 |> fold_rev (Thm.forall_intr o cterm_of thy o Free) RIvs |
494 |> fold_rev (Thm.forall_intr o cterm_of thy o Free) RIvs |
517 |
518 |
518 val exactly_one = |
519 val exactly_one = |
519 ex1I |> instantiate' [SOME (ctyp_of thy ranT)] [SOME P2, SOME (cterm_of thy rhsC)] |
520 ex1I |> instantiate' [SOME (ctyp_of thy ranT)] [SOME P2, SOME (cterm_of thy rhsC)] |
520 |> curry (op COMP) existence |
521 |> curry (op COMP) existence |
521 |> curry (op COMP) uniqueness |
522 |> curry (op COMP) uniqueness |
522 |> simplify (Simplifier.global_context thy HOL_basic_ss addsimps [case_hyp RS sym]) |
523 |> simplify |
|
524 (put_simpset HOL_basic_ss (Proof_Context.init_global thy) addsimps [case_hyp RS sym]) |
523 |> Thm.implies_intr (cprop_of case_hyp) |
525 |> Thm.implies_intr (cprop_of case_hyp) |
524 |> fold_rev (Thm.implies_intr o cprop_of) ags |
526 |> fold_rev (Thm.implies_intr o cprop_of) ags |
525 |> fold_rev Thm.forall_intr cqs |
527 |> fold_rev Thm.forall_intr cqs |
526 |
528 |
527 val function_value = |
529 val function_value = |
732 |> (fn it => it COMP graph_is_function) |
734 |> (fn it => it COMP graph_is_function) |
733 |> Thm.implies_intr z_smaller |
735 |> Thm.implies_intr z_smaller |
734 |> Thm.forall_intr (cterm_of thy z) |
736 |> Thm.forall_intr (cterm_of thy z) |
735 |> (fn it => it COMP valthm) |
737 |> (fn it => it COMP valthm) |
736 |> Thm.implies_intr lhs_acc |
738 |> Thm.implies_intr lhs_acc |
737 |> asm_simplify (Simplifier.global_context thy HOL_basic_ss addsimps [f_iff]) |
739 |> asm_simplify (put_simpset HOL_basic_ss (Proof_Context.init_global thy) addsimps [f_iff]) |
738 |> fold_rev (Thm.implies_intr o cprop_of) ags |
740 |> fold_rev (Thm.implies_intr o cprop_of) ags |
739 |> fold_rev forall_intr_rename (map fst oqs ~~ cqs) |
741 |> fold_rev forall_intr_rename (map fst oqs ~~ cqs) |
740 end |
742 end |
741 in |
743 in |
742 map2 mk_psimp clauses valthms |
744 map2 mk_psimp clauses valthms |
887 val Globals {z, ...} = globals |
889 val Globals {z, ...} = globals |
888 val ClauseInfo {cdata = ClauseContext {qs, cqs, ags, lhs, case_hyp, ...}, tree, |
890 val ClauseInfo {cdata = ClauseContext {qs, cqs, ags, lhs, case_hyp, ...}, tree, |
889 qglr=(oqs, _, _, _), ...} = clause |
891 qglr=(oqs, _, _, _), ...} = clause |
890 |
892 |
891 val ih_case = |
893 val ih_case = |
892 full_simplify (Simplifier.global_context thy HOL_basic_ss addsimps [case_hyp]) ihyp |
894 full_simplify (put_simpset HOL_basic_ss (Proof_Context.init_global thy) addsimps [case_hyp]) |
|
895 ihyp |
893 |
896 |
894 fun step (fixes, assumes) (_ $ arg) u (sub,(hyps,thms)) = |
897 fun step (fixes, assumes) (_ $ arg) u (sub,(hyps,thms)) = |
895 let |
898 let |
896 val used = (u @ sub) |
899 val used = (u @ sub) |
897 |> map (fn (ctx,thm) => Function_Ctx_Tree.export_thm thy ctx thm) |
900 |> map (fn (ctx,thm) => Function_Ctx_Tree.export_thm thy ctx thm) |
977 |> fold Thm.implies_intr hyps |
980 |> fold Thm.implies_intr hyps |
978 |> Thm.implies_intr wfR' |
981 |> Thm.implies_intr wfR' |
979 |> Thm.forall_intr (cterm_of thy R') |
982 |> Thm.forall_intr (cterm_of thy R') |
980 |> Thm.forall_elim (cterm_of thy (inrel_R)) |
983 |> Thm.forall_elim (cterm_of thy (inrel_R)) |
981 |> curry op RS wf_in_rel |
984 |> curry op RS wf_in_rel |
982 |> full_simplify (Simplifier.global_context thy HOL_basic_ss addsimps [in_rel_def]) |
985 |> full_simplify (put_simpset HOL_basic_ss (Proof_Context.init_global thy) addsimps [in_rel_def]) |
983 |> Thm.forall_intr (cterm_of thy Rrel) |
986 |> Thm.forall_intr (cterm_of thy Rrel) |
984 end |
987 end |
985 |
988 |
986 |
989 |
987 |
990 |