664 rows = map (expnd c) rows}) |
664 rows = map (expnd c) rows}) |
665 (Utils.zip3 new_formals groups constraints) |
665 (Utils.zip3 new_formals groups constraints) |
666 val recursive_thms = map mk news |
666 val recursive_thms = map mk news |
667 val build_exists = Library.foldr |
667 val build_exists = Library.foldr |
668 (fn((x,t), th) => |
668 (fn((x,t), th) => |
669 Rules.CHOOSE (tych x, Rules.ASSUME (tych t)) th) |
669 Rules.CHOOSE ctxt (tych x, Rules.ASSUME (tych t)) th) |
670 val thms' = ListPair.map build_exists (vexl, recursive_thms) |
670 val thms' = ListPair.map build_exists (vexl, recursive_thms) |
671 val same_concls = Rules.EVEN_ORS thms' |
671 val same_concls = Rules.EVEN_ORS thms' |
672 in Rules.DISJ_CASESL thm' same_concls |
672 in Rules.DISJ_CASESL thm' same_concls |
673 end |
673 end |
674 end end |
674 end end |
693 val th0 = Rules.ASSUME (tych a_eq_v) |
693 val th0 = Rules.ASSUME (tych a_eq_v) |
694 val rows = map (fn x => ([x], (th0,[]))) pats |
694 val rows = map (fn x => ([x], (th0,[]))) pats |
695 in |
695 in |
696 Rules.GEN (tych a) |
696 Rules.GEN (tych a) |
697 (Rules.RIGHT_ASSOC ctxt |
697 (Rules.RIGHT_ASSOC ctxt |
698 (Rules.CHOOSE(tych v, ex_th0) |
698 (Rules.CHOOSE ctxt (tych v, ex_th0) |
699 (mk_case ty_info (vname::aname::names) |
699 (mk_case ty_info (vname::aname::names) |
700 thy {path=[v], rows=rows}))) |
700 thy {path=[v], rows=rows}))) |
701 end end; |
701 end end; |
702 |
702 |
703 |
703 |
808 * x = (v1,...,vn) |- M[x] |
808 * x = (v1,...,vn) |- M[x] |
809 * --------------------------------------------- |
809 * --------------------------------------------- |
810 * ?v1 ... vn. x = (v1,...,vn) |- M[x] |
810 * ?v1 ... vn. x = (v1,...,vn) |- M[x] |
811 * |
811 * |
812 *---------------------------------------------------------------------------*) |
812 *---------------------------------------------------------------------------*) |
813 fun LEFT_ABS_VSTRUCT tych thm = |
813 fun LEFT_ABS_VSTRUCT ctxt tych thm = |
814 let fun CHOOSER v (tm,thm) = |
814 let fun CHOOSER v (tm,thm) = |
815 let val ex_tm = USyntax.mk_exists{Bvar=v,Body=tm} |
815 let val ex_tm = USyntax.mk_exists{Bvar=v,Body=tm} |
816 in (ex_tm, Rules.CHOOSE(tych v, Rules.ASSUME (tych ex_tm)) thm) |
816 in (ex_tm, Rules.CHOOSE ctxt (tych v, Rules.ASSUME (tych ex_tm)) thm) |
817 end |
817 end |
818 val [veq] = filter (can USyntax.dest_eq) (#1 (Rules.dest_thm thm)) |
818 val [veq] = filter (can USyntax.dest_eq) (#1 (Rules.dest_thm thm)) |
819 val {lhs,rhs} = USyntax.dest_eq veq |
819 val {lhs,rhs} = USyntax.dest_eq veq |
820 val L = USyntax.free_vars_lr rhs |
820 val L = USyntax.free_vars_lr rhs |
821 in #2 (fold_rev CHOOSER L (veq,thm)) end; |
821 in #2 (fold_rev CHOOSER L (veq,thm)) end; |
852 domain) |
852 domain) |
853 val vtyped = tych v |
853 val vtyped = tych v |
854 val substs = map (Rules.SYM o Rules.ASSUME o tych o (curry HOLogic.mk_eq v)) pats |
854 val substs = map (Rules.SYM o Rules.ASSUME o tych o (curry HOLogic.mk_eq v)) pats |
855 val proved_cases1 = ListPair.map (fn (th,th') => Rules.SUBS ctxt [th]th') |
855 val proved_cases1 = ListPair.map (fn (th,th') => Rules.SUBS ctxt [th]th') |
856 (substs, proved_cases) |
856 (substs, proved_cases) |
857 val abs_cases = map (LEFT_ABS_VSTRUCT tych) proved_cases1 |
857 val abs_cases = map (LEFT_ABS_VSTRUCT ctxt tych) proved_cases1 |
858 val dant = Rules.GEN vtyped (Rules.DISJ_CASESL (Rules.ISPEC vtyped case_thm) abs_cases) |
858 val dant = Rules.GEN vtyped (Rules.DISJ_CASESL (Rules.ISPEC vtyped case_thm) abs_cases) |
859 val dc = Rules.MP Sinduct dant |
859 val dc = Rules.MP Sinduct dant |
860 val Parg_ty = type_of(#Bvar(USyntax.dest_forall(concl dc))) |
860 val Parg_ty = type_of(#Bvar(USyntax.dest_forall(concl dc))) |
861 val vars = map (gvvariant[Pname]) (USyntax.strip_prod_type Parg_ty) |
861 val vars = map (gvvariant[Pname]) (USyntax.strip_prod_type Parg_ty) |
862 val dc' = fold_rev (Rules.GEN o tych) vars |
862 val dc' = fold_rev (Rules.GEN o tych) vars |