|
3071
|
1 |
(* Title: HOLCF/IOA/meta_theory/Sequence.ML
|
|
3275
|
2 |
ID: $Id$
|
|
15594
|
3 |
Author: Olaf Mller
|
|
3071
|
4 |
*)
|
|
|
5 |
|
|
|
6 |
(* ----------------------------------------------------------------------------------- *)
|
|
|
7 |
|
|
|
8 |
fun Seq_case_tac s i = res_inst_tac [("x",s)] Seq_cases i
|
|
17233
|
9 |
THEN hyp_subst_tac i THEN hyp_subst_tac (i+1) THEN hyp_subst_tac (i+2);
|
|
3071
|
10 |
|
|
|
11 |
(* on a>>s only simp_tac, as full_simp_tac is uncomplete and often causes errors *)
|
|
|
12 |
fun Seq_case_simp_tac s i = Seq_case_tac s i THEN Asm_simp_tac (i+2)
|
|
|
13 |
THEN Asm_full_simp_tac (i+1)
|
|
|
14 |
THEN Asm_full_simp_tac i;
|
|
|
15 |
|
|
|
16 |
(* rws are definitions to be unfolded for admissibility check *)
|
|
|
17 |
fun Seq_induct_tac s rws i = res_inst_tac [("x",s)] Seq_induct i
|
|
|
18 |
THEN (REPEAT_DETERM (CHANGED (Asm_simp_tac (i+1))))
|
|
4098
|
19 |
THEN simp_tac (simpset() addsimps rws) i;
|
|
3071
|
20 |
|
|
|
21 |
fun Seq_Finite_induct_tac i = etac Seq_Finite_ind i
|
|
|
22 |
THEN (REPEAT_DETERM (CHANGED (Asm_simp_tac i)));
|
|
|
23 |
|
|
|
24 |
fun pair_tac s = res_inst_tac [("p",s)] PairE
|
|
17233
|
25 |
THEN' hyp_subst_tac THEN' Asm_full_simp_tac;
|
|
3071
|
26 |
|
|
|
27 |
(* induction on a sequence of pairs with pairsplitting and simplification *)
|
|
17233
|
28 |
fun pair_induct_tac s rws i =
|
|
|
29 |
res_inst_tac [("x",s)] Seq_induct i
|
|
|
30 |
THEN pair_tac "a" (i+3)
|
|
|
31 |
THEN (REPEAT_DETERM (CHANGED (Simp_tac (i+1))))
|
|
4098
|
32 |
THEN simp_tac (simpset() addsimps rws) i;
|