347 val Ris = map (fn RCInfo {llRI, ...} => llRI) RCs |
347 val Ris = map (fn RCInfo {llRI, ...} => llRI) RCs |
348 val h_assums = map (fn RCInfo {h_assum, ...} => |
348 val h_assums = map (fn RCInfo {h_assum, ...} => |
349 Thm.assume (cterm_of thy (subst_bounds (rev qs, h_assum)))) RCs |
349 Thm.assume (cterm_of thy (subst_bounds (rev qs, h_assum)))) RCs |
350 |
350 |
351 val (eql, _) = |
351 val (eql, _) = |
352 Function_Ctx_Tree.rewrite_by_tree thy h ih_elim_case (Ris ~~ h_assums) tree |
352 Function_Ctx_Tree.rewrite_by_tree (Proof_Context.init_global thy) |
|
353 h ih_elim_case (Ris ~~ h_assums) tree |
353 |
354 |
354 val replace_lemma = (eql RS meta_eq_to_obj_eq) |
355 val replace_lemma = (eql RS meta_eq_to_obj_eq) |
355 |> Thm.implies_intr (cprop_of case_hyp) |
356 |> Thm.implies_intr (cprop_of case_hyp) |
356 |> fold_rev (Thm.implies_intr o cprop_of) h_assums |
357 |> fold_rev (Thm.implies_intr o cprop_of) h_assums |
357 |> fold_rev (Thm.implies_intr o cprop_of) ags |
358 |> fold_rev (Thm.implies_intr o cprop_of) ags |
481 let |
482 let |
482 val Globals {x, y, ranT, fvar, ...} = globals |
483 val Globals {x, y, ranT, fvar, ...} = globals |
483 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 |
484 val rhsC = Pattern.rewrite_term thy [(fvar, f)] [] rhs |
485 val rhsC = Pattern.rewrite_term thy [(fvar, f)] [] rhs |
485 |
486 |
486 val ih_intro_case = full_simplify (HOL_basic_ss addsimps [case_hyp]) ih_intro |
487 val ih_intro_case = |
|
488 full_simplify (Simplifier.global_context thy HOL_basic_ss addsimps [case_hyp]) ih_intro |
487 |
489 |
488 fun prep_RC (RCInfo {llRI, RIvs, CCas, ...}) = |
490 fun prep_RC (RCInfo {llRI, RIvs, CCas, ...}) = |
489 (llRI RS ih_intro_case) |
491 (llRI RS ih_intro_case) |
490 |> fold_rev (Thm.implies_intr o cprop_of) CCas |
492 |> fold_rev (Thm.implies_intr o cprop_of) CCas |
491 |> fold_rev (Thm.forall_intr o cterm_of thy o Free) RIvs |
493 |> fold_rev (Thm.forall_intr o cterm_of thy o Free) RIvs |
514 |
516 |
515 val exactly_one = |
517 val exactly_one = |
516 ex1I |> instantiate' [SOME (ctyp_of thy ranT)] [SOME P2, SOME (cterm_of thy rhsC)] |
518 ex1I |> instantiate' [SOME (ctyp_of thy ranT)] [SOME P2, SOME (cterm_of thy rhsC)] |
517 |> curry (op COMP) existence |
519 |> curry (op COMP) existence |
518 |> curry (op COMP) uniqueness |
520 |> curry (op COMP) uniqueness |
519 |> simplify (HOL_basic_ss addsimps [case_hyp RS sym]) |
521 |> simplify (Simplifier.global_context thy HOL_basic_ss addsimps [case_hyp RS sym]) |
520 |> Thm.implies_intr (cprop_of case_hyp) |
522 |> Thm.implies_intr (cprop_of case_hyp) |
521 |> fold_rev (Thm.implies_intr o cprop_of) ags |
523 |> fold_rev (Thm.implies_intr o cprop_of) ags |
522 |> fold_rev Thm.forall_intr cqs |
524 |> fold_rev Thm.forall_intr cqs |
523 |
525 |
524 val function_value = |
526 val function_value = |
729 |> (fn it => it COMP graph_is_function) |
731 |> (fn it => it COMP graph_is_function) |
730 |> Thm.implies_intr z_smaller |
732 |> Thm.implies_intr z_smaller |
731 |> Thm.forall_intr (cterm_of thy z) |
733 |> Thm.forall_intr (cterm_of thy z) |
732 |> (fn it => it COMP valthm) |
734 |> (fn it => it COMP valthm) |
733 |> Thm.implies_intr lhs_acc |
735 |> Thm.implies_intr lhs_acc |
734 |> asm_simplify (HOL_basic_ss addsimps [f_iff]) |
736 |> asm_simplify (Simplifier.global_context thy HOL_basic_ss addsimps [f_iff]) |
735 |> fold_rev (Thm.implies_intr o cprop_of) ags |
737 |> fold_rev (Thm.implies_intr o cprop_of) ags |
736 |> fold_rev forall_intr_rename (map fst oqs ~~ cqs) |
738 |> fold_rev forall_intr_rename (map fst oqs ~~ cqs) |
737 end |
739 end |
738 in |
740 in |
739 map2 mk_psimp clauses valthms |
741 map2 mk_psimp clauses valthms |
883 let |
885 let |
884 val Globals {z, ...} = globals |
886 val Globals {z, ...} = globals |
885 val ClauseInfo {cdata = ClauseContext {qs, cqs, ags, lhs, case_hyp, ...}, tree, |
887 val ClauseInfo {cdata = ClauseContext {qs, cqs, ags, lhs, case_hyp, ...}, tree, |
886 qglr=(oqs, _, _, _), ...} = clause |
888 qglr=(oqs, _, _, _), ...} = clause |
887 |
889 |
888 val ih_case = full_simplify (HOL_basic_ss addsimps [case_hyp]) ihyp |
890 val ih_case = |
|
891 full_simplify (Simplifier.global_context thy HOL_basic_ss addsimps [case_hyp]) ihyp |
889 |
892 |
890 fun step (fixes, assumes) (_ $ arg) u (sub,(hyps,thms)) = |
893 fun step (fixes, assumes) (_ $ arg) u (sub,(hyps,thms)) = |
891 let |
894 let |
892 val used = (u @ sub) |
895 val used = (u @ sub) |
893 |> map (fn (ctx,thm) => Function_Ctx_Tree.export_thm thy ctx thm) |
896 |> map (fn (ctx,thm) => Function_Ctx_Tree.export_thm thy ctx thm) |
973 |> fold Thm.implies_intr hyps |
976 |> fold Thm.implies_intr hyps |
974 |> Thm.implies_intr wfR' |
977 |> Thm.implies_intr wfR' |
975 |> Thm.forall_intr (cterm_of thy R') |
978 |> Thm.forall_intr (cterm_of thy R') |
976 |> Thm.forall_elim (cterm_of thy (inrel_R)) |
979 |> Thm.forall_elim (cterm_of thy (inrel_R)) |
977 |> curry op RS wf_in_rel |
980 |> curry op RS wf_in_rel |
978 |> full_simplify (HOL_basic_ss addsimps [in_rel_def]) |
981 |> full_simplify (Simplifier.global_context thy HOL_basic_ss addsimps [in_rel_def]) |
979 |> Thm.forall_intr (cterm_of thy Rrel) |
982 |> Thm.forall_intr (cterm_of thy Rrel) |
980 end |
983 end |
981 |
984 |
982 |
985 |
983 |
986 |