# HG changeset patch # User paulson # Date 1103032382 -3600 # Node ID 18914688a5fd6578f3f580a2f23462c94d70e1d7 # Parent a063687d24ebf9e292f1782607ef8785be64f916 converted Relation_Power to new-style theory diff -r a063687d24eb -r 18914688a5fd src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Tue Dec 14 10:45:16 2004 +0100 +++ b/src/HOL/IsaMakefile Tue Dec 14 14:53:02 2004 +0100 @@ -93,8 +93,7 @@ Lfp.thy List.ML List.thy Main.ML Main.thy Map.thy\ Nat.ML Nat.thy NatArith.thy Power.thy PreList.thy Product_Type.thy \ Refute.thy ROOT.ML \ - Recdef.thy Reconstruction.thy\ - Record.thy Relation.ML Relation.thy Relation_Power.ML \ + Recdef.thy Reconstruction.thy Record.thy Relation.ML Relation.thy \ Relation_Power.thy LOrder.thy OrderedGroup.thy OrderedGroup.ML Ring_and_Field.thy\ Set.ML Set.thy SetInterval.ML SetInterval.thy \ Sum_Type.thy Tools/datatype_abs_proofs.ML Tools/datatype_aux.ML \ diff -r a063687d24eb -r 18914688a5fd src/HOL/Relation_Power.ML --- a/src/HOL/Relation_Power.ML Tue Dec 14 10:45:16 2004 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,115 +0,0 @@ -(* Title: HOL/Relation_Power.ML - ID: $Id$ - Author: Tobias Nipkow - Copyright 1996 TU Muenchen -*) - -Goal "!!R:: ('a*'a)set. R^1 = R"; -by (Simp_tac 1); -qed "rel_pow_1"; -Addsimps [rel_pow_1]; - -Goal "(x,x) : R^0"; -by (Simp_tac 1); -qed "rel_pow_0_I"; - -Goal "[| (x,y) : R^n; (y,z):R |] ==> (x,z):R^(Suc n)"; -by (Simp_tac 1); -by (Blast_tac 1); -qed "rel_pow_Suc_I"; - -Goal "!z. (x,y) : R --> (y,z):R^n --> (x,z):R^(Suc n)"; -by (induct_tac "n" 1); -by (Simp_tac 1); -by (Asm_full_simp_tac 1); -by (Blast_tac 1); -qed_spec_mp "rel_pow_Suc_I2"; - -Goal "!!R. [| (x,y) : R^0; x=y ==> P |] ==> P"; -by (Asm_full_simp_tac 1); -qed "rel_pow_0_E"; - -val [major,minor] = Goal - "[| (x,z) : R^(Suc n); !!y. [| (x,y) : R^n; (y,z) : R |] ==> P |] ==> P"; -by (cut_facts_tac [major] 1); -by (Asm_full_simp_tac 1); -by (blast_tac (claset() addIs [minor]) 1); -qed "rel_pow_Suc_E"; - -val [p1,p2,p3] = Goal - "[| (x,z) : R^n; [| n=0; x = z |] ==> P; \ -\ !!y m. [| n = Suc m; (x,y) : R^m; (y,z) : R |] ==> P \ -\ |] ==> P"; -by (cut_facts_tac [p1] 1); -by (case_tac "n" 1); -by (asm_full_simp_tac (simpset() addsimps [p2]) 1); -by (Asm_full_simp_tac 1); -by (etac rel_compEpair 1); -by (REPEAT(ares_tac [p3] 1)); -qed "rel_pow_E"; - -Goal "!x z. (x,z):R^(Suc n) --> (? y. (x,y):R & (y,z):R^n)"; -by (induct_tac "n" 1); -by (blast_tac (claset() addIs [rel_pow_0_I] - addEs [rel_pow_0_E,rel_pow_Suc_E]) 1); -by (blast_tac (claset() addIs [rel_pow_Suc_I] - addEs [rel_pow_0_E,rel_pow_Suc_E]) 1); -qed_spec_mp "rel_pow_Suc_D2"; - - -Goal "!x y z. (x,y) : R^n & (y,z) : R --> (? w. (x,w) : R & (w,z) : R^n)"; -by (induct_tac "n" 1); -by (ALLGOALS Asm_simp_tac); -by (Blast_tac 1); -qed_spec_mp "rel_pow_Suc_D2'"; - -val [p1,p2,p3] = Goal - "[| (x,z) : R^n; [| n=0; x = z |] ==> P; \ -\ !!y m. [| n = Suc m; (x,y) : R; (y,z) : R^m |] ==> P \ -\ |] ==> P"; -by (cut_facts_tac [p1] 1); -by (case_tac "n" 1); -by (asm_full_simp_tac (simpset() addsimps [p2]) 1); -by (Asm_full_simp_tac 1); -by (etac rel_compEpair 1); -by (dtac (conjI RS rel_pow_Suc_D2') 1); -by (assume_tac 1); -by (etac exE 1); -by (etac p3 1); -by (etac conjunct1 1); -by (etac conjunct2 1); -qed "rel_pow_E2"; - -Goal "!!p. p:R^* ==> p : (UN n. R^n)"; -by (split_all_tac 1); -by (etac rtrancl_induct 1); -by (ALLGOALS (blast_tac (claset() addIs [rel_pow_0_I,rel_pow_Suc_I]))); -qed "rtrancl_imp_UN_rel_pow"; - -Goal "!y. (x,y):R^n --> (x,y):R^*"; -by (induct_tac "n" 1); -by (blast_tac (claset() addIs [rtrancl_refl] addEs [rel_pow_0_E]) 1); -by (blast_tac (claset() addEs [rel_pow_Suc_E] - addIs [rtrancl_into_rtrancl]) 1); -val lemma = result() RS spec RS mp; - -Goal "!!p. p:R^n ==> p:R^*"; -by (split_all_tac 1); -by (etac lemma 1); -qed "rel_pow_imp_rtrancl"; - -Goal "R^* = (UN n. R^n)"; -by (blast_tac (claset() addIs [rtrancl_imp_UN_rel_pow, rel_pow_imp_rtrancl]) 1); -qed "rtrancl_is_UN_rel_pow"; - - -Goal "!!r::('a * 'a)set. single_valued r ==> single_valued (r^n)"; -by (rtac single_valuedI 1); -by (induct_tac "n" 1); - by (Simp_tac 1); -by (fast_tac (claset() addDs [single_valuedD] addEs [rel_pow_Suc_E]) 1); -qed_spec_mp "single_valued_rel_pow"; - - - - diff -r a063687d24eb -r 18914688a5fd src/HOL/Relation_Power.thy --- a/src/HOL/Relation_Power.thy Tue Dec 14 10:45:16 2004 +0100 +++ b/src/HOL/Relation_Power.thy Tue Dec 14 14:53:02 2004 +0100 @@ -2,36 +2,133 @@ ID: $Id$ Author: Tobias Nipkow Copyright 1996 TU Muenchen - -R^n = R O ... O R, the n-fold composition of R -f^n = f o ... o f, the n-fold composition of f +*) -WARNING: due to the limits of Isabelle's type classes, ^ on functions and -relations has too general a domain, namely ('a * 'b)set and 'a => 'b. -This means that it may be necessary to attach explicit type constraints. -Examples: range(f^n) = A and Range(R^n) = B need constraints. -*) +header{*Powers of Relations and Functions*} theory Relation_Power imports Nat begin instance - set :: (type) power .. (* only ('a * 'a) set should be in power! *) + set :: (type) power .. + --{* only type @{typ "('a * 'a) set"} should be in class @{text power}!*} +(*R^n = R O ... O R, the n-fold composition of R*) primrec (relpow) "R^0 = Id" "R^(Suc n) = R O (R^n)" instance - fun :: (type, type) power .. (* only 'a => 'a should be in power! *) + fun :: (type, type) power .. + --{* only type @{typ "'a => 'a"} should be in class @{text power}!*} +(*f^n = f o ... o f, the n-fold composition of f*) primrec (funpow) "f^0 = id" "f^(Suc n) = f o (f^n)" +text{*WARNING: due to the limits of Isabelle's type classes, exponentiation on +functions and relations has too general a domain, namely @{typ "('a * 'b)set"} +and @{typ "'a => 'b"}. Explicit type constraints may therefore be necessary. +For example, @{term "range(f^n) = A"} and @{term "Range(R^n) = B"} need +constraints.*} + lemma funpow_add: "f ^ (m+n) = f^m o f^n" by(induct m) simp_all +lemma rel_pow_1: "!!R:: ('a*'a)set. R^1 = R" +by simp +declare rel_pow_1 [simp] + +lemma rel_pow_0_I: "(x,x) : R^0" +by simp + +lemma rel_pow_Suc_I: "[| (x,y) : R^n; (y,z):R |] ==> (x,z):R^(Suc n)" +apply (auto ); +done + +lemma rel_pow_Suc_I2 [rule_format]: + "\z. (x,y) : R --> (y,z):R^n --> (x,z):R^(Suc n)" +apply (induct_tac "n", simp_all) +apply blast +done + +lemma rel_pow_0_E: "[| (x,y) : R^0; x=y ==> P |] ==> P" +by simp + +lemma rel_pow_Suc_E: + "[| (x,z) : R^(Suc n); !!y. [| (x,y) : R^n; (y,z) : R |] ==> P |] ==> P" +by auto + +lemma rel_pow_E: + "[| (x,z) : R^n; [| n=0; x = z |] ==> P; + !!y m. [| n = Suc m; (x,y) : R^m; (y,z) : R |] ==> P + |] ==> P" +by (case_tac "n", auto) + +lemma rel_pow_Suc_D2 [rule_format]: + "\x z. (x,z):R^(Suc n) --> (\y. (x,y):R & (y,z):R^n)" +apply (induct_tac "n") +apply (blast intro: rel_pow_0_I elim: rel_pow_0_E rel_pow_Suc_E) +apply (blast intro: rel_pow_Suc_I elim: rel_pow_0_E rel_pow_Suc_E) +done + + +lemma rel_pow_Suc_D2': + "\x y z. (x,y) : R^n & (y,z) : R --> (\w. (x,w) : R & (w,z) : R^n)" +by (induct_tac "n", simp_all, blast) + +lemma rel_pow_E2: + "[| (x,z) : R^n; [| n=0; x = z |] ==> P; + !!y m. [| n = Suc m; (x,y) : R; (y,z) : R^m |] ==> P + |] ==> P" +apply (case_tac "n", simp) +apply (cut_tac n=nat and R=R in rel_pow_Suc_D2', simp, blast) +done + +lemma rtrancl_imp_UN_rel_pow: "!!p. p:R^* ==> p : (UN n. R^n)" +apply (simp only: split_tupled_all) +apply (erule rtrancl_induct) +apply (blast intro: rel_pow_0_I rel_pow_Suc_I)+ +done + +lemma rel_pow_imp_rtrancl: "!!p. p:R^n ==> p:R^*" +apply (simp only: split_tupled_all) +apply (induct "n") +apply (blast intro: rtrancl_refl elim: rel_pow_0_E) +apply (blast elim: rel_pow_Suc_E intro: rtrancl_into_rtrancl) +done + +lemma rtrancl_is_UN_rel_pow: "R^* = (UN n. R^n)" +by (blast intro: rtrancl_imp_UN_rel_pow rel_pow_imp_rtrancl) + + +lemma single_valued_rel_pow [rule_format]: + "!!r::('a * 'a)set. single_valued r ==> single_valued (r^n)" +apply (rule single_valuedI) +apply (induct_tac "n", simp) +apply (fast dest: single_valuedD elim: rel_pow_Suc_E) +done + +ML +{* +val funpow_add = thm "funpow_add"; +val rel_pow_1 = thm "rel_pow_1"; +val rel_pow_0_I = thm "rel_pow_0_I"; +val rel_pow_Suc_I = thm "rel_pow_Suc_I"; +val rel_pow_Suc_I2 = thm "rel_pow_Suc_I2"; +val rel_pow_0_E = thm "rel_pow_0_E"; +val rel_pow_Suc_E = thm "rel_pow_Suc_E"; +val rel_pow_E = thm "rel_pow_E"; +val rel_pow_Suc_D2 = thm "rel_pow_Suc_D2"; +val rel_pow_Suc_D2 = thm "rel_pow_Suc_D2"; +val rel_pow_E2 = thm "rel_pow_E2"; +val rtrancl_imp_UN_rel_pow = thm "rtrancl_imp_UN_rel_pow"; +val rel_pow_imp_rtrancl = thm "rel_pow_imp_rtrancl"; +val rtrancl_is_UN_rel_pow = thm "rtrancl_is_UN_rel_pow"; +val single_valued_rel_pow = thm "single_valued_rel_pow"; +*} + end