1079 |
1079 |
1080 |
1080 |
1081 ML {* |
1081 ML {* |
1082 |
1082 |
1083 fun Seq_case_tac ctxt s i = |
1083 fun Seq_case_tac ctxt s i = |
1084 Rule_Insts.res_inst_tac ctxt [((("x", 0), Position.none), s)] @{thm Seq_cases} i |
1084 Rule_Insts.res_inst_tac ctxt [((("x", 0), Position.none), s)] [] @{thm Seq_cases} i |
1085 THEN hyp_subst_tac ctxt i THEN hyp_subst_tac ctxt (i+1) THEN hyp_subst_tac ctxt (i+2); |
1085 THEN hyp_subst_tac ctxt i THEN hyp_subst_tac ctxt (i+1) THEN hyp_subst_tac ctxt (i+2); |
1086 |
1086 |
1087 (* on a>>s only simp_tac, as full_simp_tac is uncomplete and often causes errors *) |
1087 (* on a>>s only simp_tac, as full_simp_tac is uncomplete and often causes errors *) |
1088 fun Seq_case_simp_tac ctxt s i = |
1088 fun Seq_case_simp_tac ctxt s i = |
1089 Seq_case_tac ctxt s i |
1089 Seq_case_tac ctxt s i |
1091 THEN asm_full_simp_tac ctxt (i+1) |
1091 THEN asm_full_simp_tac ctxt (i+1) |
1092 THEN asm_full_simp_tac ctxt i; |
1092 THEN asm_full_simp_tac ctxt i; |
1093 |
1093 |
1094 (* rws are definitions to be unfolded for admissibility check *) |
1094 (* rws are definitions to be unfolded for admissibility check *) |
1095 fun Seq_induct_tac ctxt s rws i = |
1095 fun Seq_induct_tac ctxt s rws i = |
1096 Rule_Insts.res_inst_tac ctxt [((("x", 0), Position.none), s)] @{thm Seq_induct} i |
1096 Rule_Insts.res_inst_tac ctxt [((("x", 0), Position.none), s)] [] @{thm Seq_induct} i |
1097 THEN (REPEAT_DETERM (CHANGED (asm_simp_tac ctxt (i+1)))) |
1097 THEN (REPEAT_DETERM (CHANGED (asm_simp_tac ctxt (i+1)))) |
1098 THEN simp_tac (ctxt addsimps rws) i; |
1098 THEN simp_tac (ctxt addsimps rws) i; |
1099 |
1099 |
1100 fun Seq_Finite_induct_tac ctxt i = |
1100 fun Seq_Finite_induct_tac ctxt i = |
1101 etac @{thm Seq_Finite_ind} i |
1101 etac @{thm Seq_Finite_ind} i |
1102 THEN (REPEAT_DETERM (CHANGED (asm_simp_tac ctxt i))); |
1102 THEN (REPEAT_DETERM (CHANGED (asm_simp_tac ctxt i))); |
1103 |
1103 |
1104 fun pair_tac ctxt s = |
1104 fun pair_tac ctxt s = |
1105 Rule_Insts.res_inst_tac ctxt [((("p", 0), Position.none), s)] @{thm PairE} |
1105 Rule_Insts.res_inst_tac ctxt [((("p", 0), Position.none), s)] [] @{thm PairE} |
1106 THEN' hyp_subst_tac ctxt THEN' asm_full_simp_tac ctxt; |
1106 THEN' hyp_subst_tac ctxt THEN' asm_full_simp_tac ctxt; |
1107 |
1107 |
1108 (* induction on a sequence of pairs with pairsplitting and simplification *) |
1108 (* induction on a sequence of pairs with pairsplitting and simplification *) |
1109 fun pair_induct_tac ctxt s rws i = |
1109 fun pair_induct_tac ctxt s rws i = |
1110 Rule_Insts.res_inst_tac ctxt [((("x", 0), Position.none), s)] @{thm Seq_induct} i |
1110 Rule_Insts.res_inst_tac ctxt [((("x", 0), Position.none), s)] [] @{thm Seq_induct} i |
1111 THEN pair_tac ctxt "a" (i+3) |
1111 THEN pair_tac ctxt "a" (i+3) |
1112 THEN (REPEAT_DETERM (CHANGED (simp_tac ctxt (i+1)))) |
1112 THEN (REPEAT_DETERM (CHANGED (simp_tac ctxt (i+1)))) |
1113 THEN simp_tac (ctxt addsimps rws) i; |
1113 THEN simp_tac (ctxt addsimps rws) i; |
1114 |
1114 |
1115 *} |
1115 *} |