--- a/src/HOLCF/IOA/meta_theory/Sequence.thy Sat May 27 21:18:51 2006 +0200
+++ b/src/HOLCF/IOA/meta_theory/Sequence.thy Sun May 28 19:54:20 2006 +0200
@@ -1124,6 +1124,45 @@
apply auto
done
-ML {* use_legacy_bindings (the_context ()) *}
+
+
+ML {*
+
+local
+ val Seq_cases = thm "Seq_cases"
+ val Seq_induct = thm "Seq_induct"
+ val Seq_Finite_ind = thm "Seq_Finite_ind"
+in
+
+fun Seq_case_tac s i = res_inst_tac [("x",s)] Seq_cases i
+ THEN hyp_subst_tac i THEN hyp_subst_tac (i+1) THEN hyp_subst_tac (i+2);
+
+(* on a>>s only simp_tac, as full_simp_tac is uncomplete and often causes errors *)
+fun Seq_case_simp_tac s i = Seq_case_tac s i THEN SIMPSET' asm_simp_tac (i+2)
+ THEN SIMPSET' asm_full_simp_tac (i+1)
+ THEN SIMPSET' asm_full_simp_tac i;
+
+(* rws are definitions to be unfolded for admissibility check *)
+fun Seq_induct_tac s rws i = res_inst_tac [("x",s)] Seq_induct i
+ THEN (REPEAT_DETERM (CHANGED (SIMPSET' asm_simp_tac (i+1))))
+ THEN SIMPSET' (fn ss => simp_tac (ss addsimps rws)) i;
+
+fun Seq_Finite_induct_tac i = etac Seq_Finite_ind i
+ THEN (REPEAT_DETERM (CHANGED (SIMPSET' asm_simp_tac i)));
+
+fun pair_tac s = res_inst_tac [("p",s)] PairE
+ THEN' hyp_subst_tac THEN' SIMPSET' asm_full_simp_tac;
+
+(* induction on a sequence of pairs with pairsplitting and simplification *)
+fun pair_induct_tac s rws i =
+ res_inst_tac [("x",s)] Seq_induct i
+ THEN pair_tac "a" (i+3)
+ THEN (REPEAT_DETERM (CHANGED (SIMPSET' simp_tac (i+1))))
+ THEN SIMPSET' (fn ss => simp_tac (ss addsimps rws)) i;
end
+
+*}
+
+
+end