722 local infix 5 ==> |
722 local infix 5 ==> |
723 fun (tm1 ==> tm2) = S.mk_imp{ant = tm1, conseq = tm2} |
723 fun (tm1 ==> tm2) = S.mk_imp{ant = tm1, conseq = tm2} |
724 in |
724 in |
725 fun build_ih f P (pat,TCs) = |
725 fun build_ih f P (pat,TCs) = |
726 let val globals = S.free_vars_lr pat |
726 let val globals = S.free_vars_lr pat |
727 fun nested tm = isSome (S.find_term (curry (op aconv) f) tm) |
727 fun nested tm = is_some (S.find_term (curry (op aconv) f) tm) |
728 fun dest_TC tm = |
728 fun dest_TC tm = |
729 let val (cntxt,R_y_pat) = S.strip_imp(#2(S.strip_forall tm)) |
729 let val (cntxt,R_y_pat) = S.strip_imp(#2(S.strip_forall tm)) |
730 val (R,y,_) = S.dest_relation R_y_pat |
730 val (R,y,_) = S.dest_relation R_y_pat |
731 val P_y = if (nested tm) then R_y_pat ==> P$y else P$y |
731 val P_y = if (nested tm) then R_y_pat ==> P$y else P$y |
732 in case cntxt |
732 in case cntxt |
751 fun (tm1 ==> tm2) = S.mk_imp{ant = tm1, conseq = tm2} |
751 fun (tm1 ==> tm2) = S.mk_imp{ant = tm1, conseq = tm2} |
752 in |
752 in |
753 fun build_ih f (P,SV) (pat,TCs) = |
753 fun build_ih f (P,SV) (pat,TCs) = |
754 let val pat_vars = S.free_vars_lr pat |
754 let val pat_vars = S.free_vars_lr pat |
755 val globals = pat_vars@SV |
755 val globals = pat_vars@SV |
756 fun nested tm = isSome (S.find_term (curry (op aconv) f) tm) |
756 fun nested tm = is_some (S.find_term (curry (op aconv) f) tm) |
757 fun dest_TC tm = |
757 fun dest_TC tm = |
758 let val (cntxt,R_y_pat) = S.strip_imp(#2(S.strip_forall tm)) |
758 let val (cntxt,R_y_pat) = S.strip_imp(#2(S.strip_forall tm)) |
759 val (R,y,_) = S.dest_relation R_y_pat |
759 val (R,y,_) = S.dest_relation R_y_pat |
760 val P_y = if (nested tm) then R_y_pat ==> P$y else P$y |
760 val P_y = if (nested tm) then R_y_pat ==> P$y else P$y |
761 in case cntxt |
761 in case cntxt |
784 *---------------------------------------------------------------------------*) |
784 *---------------------------------------------------------------------------*) |
785 fun prove_case f thy (tm,TCs_locals,thm) = |
785 fun prove_case f thy (tm,TCs_locals,thm) = |
786 let val tych = Thry.typecheck thy |
786 let val tych = Thry.typecheck thy |
787 val antc = tych(#ant(S.dest_imp tm)) |
787 val antc = tych(#ant(S.dest_imp tm)) |
788 val thm' = R.SPEC_ALL thm |
788 val thm' = R.SPEC_ALL thm |
789 fun nested tm = isSome (S.find_term (curry (op aconv) f) tm) |
789 fun nested tm = is_some (S.find_term (curry (op aconv) f) tm) |
790 fun get_cntxt TC = tych(#ant(S.dest_imp(#2(S.strip_forall(concl TC))))) |
790 fun get_cntxt TC = tych(#ant(S.dest_imp(#2(S.strip_forall(concl TC))))) |
791 fun mk_ih ((TC,locals),th2,nested) = |
791 fun mk_ih ((TC,locals),th2,nested) = |
792 R.GENL (map tych locals) |
792 R.GENL (map tych locals) |
793 (if nested then R.DISCH (get_cntxt TC) th2 handle U.ERR _ => th2 |
793 (if nested then R.DISCH (get_cntxt TC) th2 handle U.ERR _ => th2 |
794 else if S.is_imp (concl TC) then R.IMP_TRANS TC th2 |
794 else if S.is_imp (concl TC) then R.IMP_TRANS TC th2 |