# HG changeset patch # User wenzelm # Date 981312174 -3600 # Node ID a5404c70982f707b662c1160e7fb6d8de12cce5f # Parent 026007eb2ccc76eea71162b716424e172bafba2c moved from Induct/ to Library/ diff -r 026007eb2ccc -r a5404c70982f src/HOL/Induct/Perm.ML --- a/src/HOL/Induct/Perm.ML Sun Feb 04 19:41:47 2001 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,165 +0,0 @@ -(* Title: HOL/ex/Perm.ML - ID: $Id$ - Author: Lawrence C Paulson, Cambridge University Computer Laboratory - Copyright 1995 University of Cambridge - -Permutations: example of an inductive definition -*) - -(*It would be nice to prove (for "multiset", defined on HOL/ex/Sorting.thy) - xs <~~> ys = (ALL x. multiset xs x = multiset ys x) -*) - -AddIs perm.intrs; - -Goal "l <~~> l"; -by (induct_tac "l" 1); -by Auto_tac; -qed "perm_refl"; -AddIffs [perm_refl]; - -(** Some examples of rule induction on permutations **) - -(*The form of the premise lets the induction bind xs and ys.*) -Goal "xs <~~> ys ==> xs=[] --> ys=[]"; -by (etac perm.induct 1); -by (ALLGOALS Asm_simp_tac); -bind_thm ("xperm_empty_imp", (* [] <~~> ys ==> ys=[] *) - [refl, result()] MRS rev_mp); - -(*This more general theorem is easier to understand!*) -Goal "xs <~~> ys ==> length(xs) = length(ys)"; -by (etac perm.induct 1); -by (ALLGOALS Asm_simp_tac); -qed "perm_length"; - -Goal "[] <~~> xs ==> xs=[]"; -by (dtac perm_length 1); -by Auto_tac; -qed "perm_empty_imp"; - -Goal "xs <~~> ys ==> ys <~~> xs"; -by (etac perm.induct 1); -by Auto_tac; -qed "perm_sym"; - -Goal "xs <~~> ys ==> x mem xs --> x mem ys"; -by (etac perm.induct 1); -by Auto_tac; -val perm_mem_lemma = result(); - -bind_thm ("perm_mem", perm_mem_lemma RS mp); - -(** Ways of making new permutations **) - -(*We can insert the head anywhere in the list*) -Goal "a # xs @ ys <~~> xs @ a # ys"; -by (induct_tac "xs" 1); -by Auto_tac; -qed "perm_append_Cons"; - -Goal "xs@ys <~~> ys@xs"; -by (induct_tac "xs" 1); -by (ALLGOALS Simp_tac); -by (blast_tac (claset() addIs [perm_append_Cons]) 1); -qed "perm_append_swap"; - -Goal "a # xs <~~> xs @ [a]"; -by (rtac perm.trans 1); -by (rtac perm_append_swap 2); -by (Simp_tac 1); -qed "perm_append_single"; - -Goal "rev xs <~~> xs"; -by (induct_tac "xs" 1); -by (ALLGOALS Simp_tac); -by (blast_tac (claset() addIs [perm_sym, perm_append_single]) 1); -qed "perm_rev"; - -Goal "xs <~~> ys ==> l@xs <~~> l@ys"; -by (induct_tac "l" 1); -by Auto_tac; -qed "perm_append1"; - -Goal "xs <~~> ys ==> xs@l <~~> ys@l"; -by (blast_tac (claset() addSIs [perm_append_swap, perm_append1]) 1); -qed "perm_append2"; - -(** Further results mostly by Thomas Marthedal Rasmussen **) - -Goal "([] <~~> xs) = (xs = [])"; -by (blast_tac (claset() addIs [perm_empty_imp]) 1); -qed "perm_empty"; -AddIffs [perm_empty]; - -Goal "(xs <~~> []) = (xs = [])"; -by Auto_tac; -by (etac (perm_sym RS perm_empty_imp) 1); -qed "perm_empty2"; -AddIffs [perm_empty2]; - -Goal "ys <~~> xs ==> xs=[y] --> ys=[y]"; -by (etac perm.induct 1); -by Auto_tac; -qed_spec_mp "perm_sing_imp"; - -Goal "(ys <~~> [y]) = (ys = [y])"; -by (blast_tac (claset() addIs [perm_sing_imp]) 1); -qed "perm_sing_eq"; -AddIffs [perm_sing_eq]; - -Goal "([y] <~~> ys) = (ys = [y])"; -by (blast_tac (claset() addDs [perm_sym]) 1); -qed "perm_sing_eq2"; -AddIffs [perm_sing_eq2]; - -Goal "x:set ys --> ys <~~> x#(remove x ys)"; -by (induct_tac "ys" 1); -by Auto_tac; -qed_spec_mp "perm_remove"; - -Goal "remove x (remove y l) = remove y (remove x l)"; -by (induct_tac "l" 1); -by Auto_tac; -qed "remove_commute"; - -(*Congruence rule*) -Goal "xs <~~> ys ==> remove z xs <~~> remove z ys"; -by (etac perm.induct 1); -by Auto_tac; -qed "perm_remove_perm"; - -Goal "remove z (z#xs) = xs"; -by Auto_tac; -qed "remove_hd"; -Addsimps [remove_hd]; - -Goal "z#xs <~~> z#ys ==> xs <~~> ys"; -by (dres_inst_tac [("z","z")] perm_remove_perm 1); -by Auto_tac; -qed "cons_perm_imp_perm"; - -Goal "(z#xs <~~> z#ys) = (xs <~~> ys)"; -by (blast_tac (claset() addIs [cons_perm_imp_perm]) 1); -qed "cons_perm_eq"; -AddIffs [cons_perm_eq]; - -Goal "ALL xs ys. zs@xs <~~> zs@ys --> xs <~~> ys"; -by (rev_induct_tac "zs" 1); -by (ALLGOALS Full_simp_tac); -by (Blast_tac 1); -qed_spec_mp "append_perm_imp_perm"; - -Goal "(zs@xs <~~> zs@ys) = (xs <~~> ys)"; -by (blast_tac (claset() addIs [append_perm_imp_perm, perm_append1]) 1); -qed "perm_append1_eq"; -AddIffs [perm_append1_eq]; - -Goal "(xs@zs <~~> ys@zs) = (xs <~~> ys)"; -by (safe_tac (claset() addSIs [perm_append2])); -by (rtac append_perm_imp_perm 1); -by (rtac (perm_append_swap RS perm.trans) 1); -(*The previous step helps this blast_tac call succeed quickly.*) -by (blast_tac (claset() addIs [perm_append_swap]) 1); -qed "perm_append2_eq"; -AddIffs [perm_append2_eq]; diff -r 026007eb2ccc -r a5404c70982f src/HOL/Induct/Perm.thy --- a/src/HOL/Induct/Perm.thy Sun Feb 04 19:41:47 2001 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,32 +0,0 @@ -(* Title: HOL/ex/Perm.thy - ID: $Id$ - Author: Lawrence C Paulson, Cambridge University Computer Laboratory - Copyright 1995 University of Cambridge - -Permutations: example of an inductive definition -*) - -Perm = Main + - -consts perm :: "('a list * 'a list) set" -syntax "@perm" :: ['a list, 'a list] => bool ("_ <~~> _" [50,50] 50) - -translations - "x <~~> y" == "(x,y) : perm" - -inductive perm - intrs - Nil "[] <~~> []" - swap "y#x#l <~~> x#y#l" - Cons "xs <~~> ys ==> z#xs <~~> z#ys" - trans "[| xs <~~> ys; ys <~~> zs |] ==> xs <~~> zs" - - -consts - remove :: ['a, 'a list] => 'a list - -primrec - "remove x [] = []" - "remove x (y#ys) = (if x=y then ys else y#remove x ys)" - -end diff -r 026007eb2ccc -r a5404c70982f src/HOL/Library/Permutation.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Library/Permutation.thy Sun Feb 04 19:42:54 2001 +0100 @@ -0,0 +1,199 @@ +(* Title: HOL/Library/Permutation.thy + ID: $Id$ + Author: Lawrence C Paulson, Cambridge University Computer Laboratory + Copyright 1995 University of Cambridge + +TODO: it would be nice to prove (for "multiset", defined on +HOL/ex/Sorting.thy) xs <~~> ys = (\x. multiset xs x = multiset ys x) +*) + +header {* + \title{Permutations} + \author{Lawrence C Paulson and Thomas M Rasmussen} +*} + +theory Permutation = Main: + +consts + perm :: "('a list * 'a list) set" + +syntax + "_perm" :: "'a list => 'a list => bool" ("_ <~~> _" [50, 50] 50) +translations + "x <~~> y" == "(x, y) \ perm" + +inductive perm + intros [intro] + Nil: "[] <~~> []" + swap: "y # x # l <~~> x # y # l" + Cons: "xs <~~> ys ==> z # xs <~~> z # ys" + trans: "xs <~~> ys ==> ys <~~> zs ==> xs <~~> zs" + +lemma perm_refl [iff]: "l <~~> l" + apply (induct l) + apply auto + done + + +subsection {* Some examples of rule induction on permutations *} + +lemma xperm_empty_imp_aux: "xs <~~> ys ==> xs = [] --> ys = []" + -- {* the form of the premise lets the induction bind @{term xs} and @{term ys} *} + apply (erule perm.induct) + apply (simp_all (no_asm_simp)) + done + +lemma xperm_empty_imp: "[] <~~> ys ==> ys = []" + apply (insert xperm_empty_imp_aux) + apply blast + done + + +text {* + \medskip This more general theorem is easier to understand! + *} + +lemma perm_length: "xs <~~> ys ==> length xs = length ys" + apply (erule perm.induct) + apply simp_all + done + +lemma perm_empty_imp: "[] <~~> xs ==> xs = []" + apply (drule perm_length) + apply auto + done + +lemma perm_sym: "xs <~~> ys ==> ys <~~> xs" + apply (erule perm.induct) + apply auto + done + +lemma perm_mem [rule_format]: "xs <~~> ys ==> x mem xs --> x mem ys" + apply (erule perm.induct) + apply auto + done + + +subsection {* Ways of making new permutations *} + +text {* + We can insert the head anywhere in the list. +*} + +lemma perm_append_Cons: "a # xs @ ys <~~> xs @ a # ys" + apply (induct xs) + apply auto + done + +lemma perm_append_swap: "xs @ ys <~~> ys @ xs" + apply (induct xs) + apply simp_all + apply (blast intro: perm_append_Cons) + done + +lemma perm_append_single: "a # xs <~~> xs @ [a]" + apply (rule perm.trans) + prefer 2 + apply (rule perm_append_swap) + apply simp + done + +lemma perm_rev: "rev xs <~~> xs" + apply (induct xs) + apply simp_all + apply (blast intro: perm_sym perm_append_single) + done + +lemma perm_append1: "xs <~~> ys ==> l @ xs <~~> l @ ys" + apply (induct l) + apply auto + done + +lemma perm_append2: "xs <~~> ys ==> xs @ l <~~> ys @ l" + apply (blast intro!: perm_append_swap perm_append1) + done + + +subsection {* Further results *} + +lemma perm_empty [iff]: "([] <~~> xs) = (xs = [])" + apply (blast intro: perm_empty_imp) + done + +lemma perm_empty2 [iff]: "(xs <~~> []) = (xs = [])" + apply auto + apply (erule perm_sym [THEN perm_empty_imp]) + done + +lemma perm_sing_imp [rule_format]: "ys <~~> xs ==> xs = [y] --> ys = [y]" + apply (erule perm.induct) + apply auto + done + +lemma perm_sing_eq [iff]: "(ys <~~> [y]) = (ys = [y])" + apply (blast intro: perm_sing_imp) + done + +lemma perm_sing_eq2 [iff]: "([y] <~~> ys) = (ys = [y])" + apply (blast dest: perm_sym) + done + + +subsection {* Removing elements *} + +consts + remove :: "'a => 'a list => 'a list" +primrec + "remove x [] = []" + "remove x (y # ys) = (if x = y then ys else y # remove x ys)" + +lemma perm_remove: "x \ set ys ==> ys <~~> x # remove x ys" + apply (induct ys) + apply auto + done + +lemma remove_commute: "remove x (remove y l) = remove y (remove x l)" + apply (induct l) + apply auto + done + + +text {* \medskip Congruence rule *} + +lemma perm_remove_perm: "xs <~~> ys ==> remove z xs <~~> remove z ys" + apply (erule perm.induct) + apply auto + done + +lemma remove_hd [simp]: "remove z (z # xs) = xs" + apply auto + done + +lemma cons_perm_imp_perm: "z # xs <~~> z # ys ==> xs <~~> ys" + apply (drule_tac z = z in perm_remove_perm) + apply auto + done + +lemma cons_perm_eq [iff]: "(z#xs <~~> z#ys) = (xs <~~> ys)" + apply (blast intro: cons_perm_imp_perm) + done + +lemma append_perm_imp_perm: "!!xs ys. zs @ xs <~~> zs @ ys ==> xs <~~> ys" + apply (induct zs rule: rev_induct) + apply (simp_all (no_asm_use)) + apply blast + done + +lemma perm_append1_eq [iff]: "(zs @ xs <~~> zs @ ys) = (xs <~~> ys)" + apply (blast intro: append_perm_imp_perm perm_append1) + done + +lemma perm_append2_eq [iff]: "(xs @ zs <~~> ys @ zs) = (xs <~~> ys)" + apply (safe intro!: perm_append2) + apply (rule append_perm_imp_perm) + apply (rule perm_append_swap [THEN perm.trans]) + -- {* the previous step helps this @{text blast} call succeed quickly *} + apply (blast intro: perm_append_swap) + done + +end