20 |
20 |
21 |
21 |
22 (** Some examples of rule induction on permutations **) |
22 (** Some examples of rule induction on permutations **) |
23 |
23 |
24 (*The form of the premise lets the induction bind xs and ys.*) |
24 (*The form of the premise lets the induction bind xs and ys.*) |
25 Goal "!!xs. xs <~~> ys ==> xs=[] --> ys=[]"; |
25 Goal "xs <~~> ys ==> xs=[] --> ys=[]"; |
26 by (etac perm.induct 1); |
26 by (etac perm.induct 1); |
27 by (ALLGOALS Asm_simp_tac); |
27 by (ALLGOALS Asm_simp_tac); |
28 qed "perm_Nil_lemma"; |
28 qed "perm_Nil_lemma"; |
29 |
29 |
30 (*A more general version is actually easier to understand!*) |
30 (*A more general version is actually easier to understand!*) |
31 Goal "!!xs. xs <~~> ys ==> length(xs) = length(ys)"; |
31 Goal "xs <~~> ys ==> length(xs) = length(ys)"; |
32 by (etac perm.induct 1); |
32 by (etac perm.induct 1); |
33 by (ALLGOALS Asm_simp_tac); |
33 by (ALLGOALS Asm_simp_tac); |
34 qed "perm_length"; |
34 qed "perm_length"; |
35 |
35 |
36 Goal "!!xs. xs <~~> ys ==> ys <~~> xs"; |
36 Goal "xs <~~> ys ==> ys <~~> xs"; |
37 by (etac perm.induct 1); |
37 by (etac perm.induct 1); |
38 by (REPEAT (ares_tac perm.intrs 1)); |
38 by (REPEAT (ares_tac perm.intrs 1)); |
39 qed "perm_sym"; |
39 qed "perm_sym"; |
40 |
40 |
41 Goal "!!xs. [| xs <~~> ys |] ==> x mem xs --> x mem ys"; |
41 Goal "[| xs <~~> ys |] ==> x mem xs --> x mem ys"; |
42 by (etac perm.induct 1); |
42 by (etac perm.induct 1); |
43 by (Fast_tac 4); |
43 by (Fast_tac 4); |
44 by (ALLGOALS Asm_simp_tac); |
44 by (ALLGOALS Asm_simp_tac); |
45 val perm_mem_lemma = result(); |
45 val perm_mem_lemma = result(); |
46 |
46 |
82 by (Simp_tac 1); |
82 by (Simp_tac 1); |
83 by (rtac (perm_append_single RS perm_sym RS perm.trans) 1); |
83 by (rtac (perm_append_single RS perm_sym RS perm.trans) 1); |
84 by (etac perm.Cons 1); |
84 by (etac perm.Cons 1); |
85 qed "perm_rev"; |
85 qed "perm_rev"; |
86 |
86 |
87 Goal "!!xs. xs <~~> ys ==> l@xs <~~> l@ys"; |
87 Goal "xs <~~> ys ==> l@xs <~~> l@ys"; |
88 by (list.induct_tac "l" 1); |
88 by (list.induct_tac "l" 1); |
89 by (Simp_tac 1); |
89 by (Simp_tac 1); |
90 by (asm_simp_tac (simpset() addsimps [perm.Cons]) 1); |
90 by (asm_simp_tac (simpset() addsimps [perm.Cons]) 1); |
91 qed "perm_append1"; |
91 qed "perm_append1"; |
92 |
92 |
93 Goal "!!xs. xs <~~> ys ==> xs@l <~~> ys@l"; |
93 Goal "xs <~~> ys ==> xs@l <~~> ys@l"; |
94 by (rtac (perm_append_swap RS perm.trans) 1); |
94 by (rtac (perm_append_swap RS perm.trans) 1); |
95 by (etac (perm_append1 RS perm.trans) 1); |
95 by (etac (perm_append1 RS perm.trans) 1); |
96 by (rtac perm_append_swap 1); |
96 by (rtac perm_append_swap 1); |
97 qed "perm_append2"; |
97 qed "perm_append2"; |
98 |
98 |