converted Relation_Power to new-style theory
authorpaulson
Tue Dec 14 14:53:02 2004 +0100 (2004-12-14)
changeset 1541018914688a5fd
parent 15409 a063687d24eb
child 15411 1d195de59497
converted Relation_Power to new-style theory
src/HOL/IsaMakefile
src/HOL/Relation_Power.ML
src/HOL/Relation_Power.thy
     1.1 --- a/src/HOL/IsaMakefile	Tue Dec 14 10:45:16 2004 +0100
     1.2 +++ b/src/HOL/IsaMakefile	Tue Dec 14 14:53:02 2004 +0100
     1.3 @@ -93,8 +93,7 @@
     1.4    Lfp.thy List.ML List.thy Main.ML Main.thy Map.thy\
     1.5    Nat.ML Nat.thy NatArith.thy Power.thy PreList.thy Product_Type.thy \
     1.6    Refute.thy ROOT.ML \
     1.7 -  Recdef.thy Reconstruction.thy\
     1.8 -  Record.thy Relation.ML Relation.thy Relation_Power.ML \
     1.9 +  Recdef.thy Reconstruction.thy Record.thy Relation.ML Relation.thy \
    1.10    Relation_Power.thy LOrder.thy OrderedGroup.thy OrderedGroup.ML Ring_and_Field.thy\
    1.11    Set.ML Set.thy SetInterval.ML SetInterval.thy \
    1.12    Sum_Type.thy Tools/datatype_abs_proofs.ML Tools/datatype_aux.ML \
     2.1 --- a/src/HOL/Relation_Power.ML	Tue Dec 14 10:45:16 2004 +0100
     2.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.3 @@ -1,115 +0,0 @@
     2.4 -(*  Title:      HOL/Relation_Power.ML
     2.5 -    ID:         $Id$
     2.6 -    Author:     Tobias Nipkow
     2.7 -    Copyright   1996  TU Muenchen
     2.8 -*)
     2.9 -
    2.10 -Goal "!!R:: ('a*'a)set. R^1 = R";
    2.11 -by (Simp_tac 1);
    2.12 -qed "rel_pow_1";
    2.13 -Addsimps [rel_pow_1];
    2.14 -
    2.15 -Goal "(x,x) : R^0";
    2.16 -by (Simp_tac 1);
    2.17 -qed "rel_pow_0_I";
    2.18 -
    2.19 -Goal "[| (x,y) : R^n; (y,z):R |] ==> (x,z):R^(Suc n)";
    2.20 -by (Simp_tac  1);
    2.21 -by (Blast_tac 1);
    2.22 -qed "rel_pow_Suc_I";
    2.23 -
    2.24 -Goal "!z. (x,y) : R --> (y,z):R^n -->  (x,z):R^(Suc n)";
    2.25 -by (induct_tac "n" 1);
    2.26 -by (Simp_tac  1);
    2.27 -by (Asm_full_simp_tac 1);
    2.28 -by (Blast_tac 1);
    2.29 -qed_spec_mp "rel_pow_Suc_I2";
    2.30 -
    2.31 -Goal "!!R. [| (x,y) : R^0; x=y ==> P |] ==> P";
    2.32 -by (Asm_full_simp_tac 1);
    2.33 -qed "rel_pow_0_E";
    2.34 -
    2.35 -val [major,minor] = Goal
    2.36 -  "[| (x,z) : R^(Suc n);  !!y. [| (x,y) : R^n; (y,z) : R |] ==> P |] ==> P";
    2.37 -by (cut_facts_tac [major] 1);
    2.38 -by (Asm_full_simp_tac  1);
    2.39 -by (blast_tac (claset() addIs [minor]) 1);
    2.40 -qed "rel_pow_Suc_E";
    2.41 -
    2.42 -val [p1,p2,p3] = Goal
    2.43 -    "[| (x,z) : R^n;  [| n=0; x = z |] ==> P;        \
    2.44 -\       !!y m. [| n = Suc m; (x,y) : R^m; (y,z) : R |] ==> P  \
    2.45 -\    |] ==> P";
    2.46 -by (cut_facts_tac [p1] 1);
    2.47 -by (case_tac "n" 1);
    2.48 -by (asm_full_simp_tac (simpset() addsimps [p2]) 1);
    2.49 -by (Asm_full_simp_tac 1);
    2.50 -by (etac rel_compEpair 1);
    2.51 -by (REPEAT(ares_tac [p3] 1));
    2.52 -qed "rel_pow_E";
    2.53 -
    2.54 -Goal "!x z. (x,z):R^(Suc n) --> (? y. (x,y):R & (y,z):R^n)";
    2.55 -by (induct_tac "n" 1);
    2.56 -by (blast_tac (claset() addIs [rel_pow_0_I] 
    2.57 -	                addEs [rel_pow_0_E,rel_pow_Suc_E]) 1);
    2.58 -by (blast_tac (claset() addIs [rel_pow_Suc_I]  
    2.59 -	                addEs [rel_pow_0_E,rel_pow_Suc_E]) 1);
    2.60 -qed_spec_mp "rel_pow_Suc_D2";
    2.61 -
    2.62 -
    2.63 -Goal "!x y z. (x,y) : R^n & (y,z) : R --> (? w. (x,w) : R & (w,z) : R^n)";
    2.64 -by (induct_tac "n" 1);
    2.65 -by (ALLGOALS Asm_simp_tac);
    2.66 -by (Blast_tac 1);
    2.67 -qed_spec_mp "rel_pow_Suc_D2'";
    2.68 -
    2.69 -val [p1,p2,p3] = Goal
    2.70 -    "[| (x,z) : R^n;  [| n=0; x = z |] ==> P;        \
    2.71 -\       !!y m. [| n = Suc m; (x,y) : R; (y,z) : R^m |] ==> P  \
    2.72 -\    |] ==> P";
    2.73 -by (cut_facts_tac [p1] 1);
    2.74 -by (case_tac "n" 1);
    2.75 -by (asm_full_simp_tac (simpset() addsimps [p2]) 1);
    2.76 -by (Asm_full_simp_tac 1);
    2.77 -by (etac rel_compEpair 1);
    2.78 -by (dtac (conjI RS rel_pow_Suc_D2') 1);
    2.79 -by (assume_tac 1);
    2.80 -by (etac exE 1);
    2.81 -by (etac p3 1);
    2.82 -by (etac conjunct1 1);
    2.83 -by (etac conjunct2 1);
    2.84 -qed "rel_pow_E2";
    2.85 -
    2.86 -Goal "!!p. p:R^* ==> p : (UN n. R^n)";
    2.87 -by (split_all_tac 1);
    2.88 -by (etac rtrancl_induct 1);
    2.89 -by (ALLGOALS (blast_tac (claset() addIs [rel_pow_0_I,rel_pow_Suc_I])));
    2.90 -qed "rtrancl_imp_UN_rel_pow";
    2.91 -
    2.92 -Goal "!y. (x,y):R^n --> (x,y):R^*";
    2.93 -by (induct_tac "n" 1);
    2.94 -by (blast_tac (claset() addIs [rtrancl_refl] addEs [rel_pow_0_E]) 1);
    2.95 -by (blast_tac (claset() addEs [rel_pow_Suc_E]
    2.96 -                       addIs [rtrancl_into_rtrancl]) 1);
    2.97 -val lemma = result() RS spec RS mp;
    2.98 -
    2.99 -Goal "!!p. p:R^n ==> p:R^*";
   2.100 -by (split_all_tac 1);
   2.101 -by (etac lemma 1);
   2.102 -qed "rel_pow_imp_rtrancl";
   2.103 -
   2.104 -Goal "R^* = (UN n. R^n)";
   2.105 -by (blast_tac (claset() addIs [rtrancl_imp_UN_rel_pow, rel_pow_imp_rtrancl]) 1);
   2.106 -qed "rtrancl_is_UN_rel_pow";
   2.107 -
   2.108 -
   2.109 -Goal "!!r::('a * 'a)set. single_valued r ==> single_valued (r^n)";
   2.110 -by (rtac single_valuedI 1);
   2.111 -by (induct_tac "n" 1);
   2.112 - by (Simp_tac 1);
   2.113 -by (fast_tac (claset() addDs [single_valuedD] addEs [rel_pow_Suc_E]) 1);
   2.114 -qed_spec_mp "single_valued_rel_pow";
   2.115 -
   2.116 -
   2.117 -
   2.118 -
     3.1 --- a/src/HOL/Relation_Power.thy	Tue Dec 14 10:45:16 2004 +0100
     3.2 +++ b/src/HOL/Relation_Power.thy	Tue Dec 14 14:53:02 2004 +0100
     3.3 @@ -2,36 +2,133 @@
     3.4      ID:         $Id$
     3.5      Author:     Tobias Nipkow
     3.6      Copyright   1996  TU Muenchen
     3.7 -
     3.8 -R^n = R O ... O R, the n-fold composition of R
     3.9 -f^n = f o ... o f, the n-fold composition of f
    3.10 +*)
    3.11  
    3.12 -WARNING: due to the limits of Isabelle's type classes, ^ on functions and
    3.13 -relations has too general a domain, namely ('a * 'b)set and 'a => 'b.
    3.14 -This means that it may be necessary to attach explicit type constraints.
    3.15 -Examples: range(f^n) = A and Range(R^n) = B need constraints.
    3.16 -*)
    3.17 +header{*Powers of Relations and Functions*}
    3.18  
    3.19  theory Relation_Power
    3.20  imports Nat
    3.21  begin
    3.22  
    3.23  instance
    3.24 -  set :: (type) power ..  (* only ('a * 'a) set should be in power! *)
    3.25 +  set :: (type) power ..  
    3.26 +      --{* only type @{typ "('a * 'a) set"} should be in class @{text power}!*}
    3.27  
    3.28 +(*R^n = R O ... O R, the n-fold composition of R*)
    3.29  primrec (relpow)
    3.30    "R^0 = Id"
    3.31    "R^(Suc n) = R O (R^n)"
    3.32  
    3.33  
    3.34  instance
    3.35 -  fun :: (type, type) power ..  (* only 'a => 'a should be in power! *)
    3.36 +  fun :: (type, type) power ..
    3.37 +      --{* only type @{typ "'a => 'a"} should be in class @{text power}!*}
    3.38  
    3.39 +(*f^n = f o ... o f, the n-fold composition of f*)
    3.40  primrec (funpow)
    3.41    "f^0 = id"
    3.42    "f^(Suc n) = f o (f^n)"
    3.43  
    3.44 +text{*WARNING: due to the limits of Isabelle's type classes, exponentiation on
    3.45 +functions and relations has too general a domain, namely @{typ "('a * 'b)set"}
    3.46 +and @{typ "'a => 'b"}.  Explicit type constraints may therefore be necessary.
    3.47 +For example, @{term "range(f^n) = A"} and @{term "Range(R^n) = B"} need
    3.48 +constraints.*}
    3.49 +
    3.50  lemma funpow_add: "f ^ (m+n) = f^m o f^n"
    3.51  by(induct m) simp_all
    3.52  
    3.53 +lemma rel_pow_1: "!!R:: ('a*'a)set. R^1 = R"
    3.54 +by simp
    3.55 +declare rel_pow_1 [simp]
    3.56 +
    3.57 +lemma rel_pow_0_I: "(x,x) : R^0"
    3.58 +by simp
    3.59 +
    3.60 +lemma rel_pow_Suc_I: "[| (x,y) : R^n; (y,z):R |] ==> (x,z):R^(Suc n)"
    3.61 +apply (auto ); 
    3.62 +done
    3.63 +
    3.64 +lemma rel_pow_Suc_I2 [rule_format]:
    3.65 +     "\<forall>z. (x,y) : R --> (y,z):R^n -->  (x,z):R^(Suc n)"
    3.66 +apply (induct_tac "n", simp_all)
    3.67 +apply blast
    3.68 +done
    3.69 +
    3.70 +lemma rel_pow_0_E: "[| (x,y) : R^0; x=y ==> P |] ==> P"
    3.71 +by simp
    3.72 +
    3.73 +lemma rel_pow_Suc_E: 
    3.74 +     "[| (x,z) : R^(Suc n);  !!y. [| (x,y) : R^n; (y,z) : R |] ==> P |] ==> P"
    3.75 +by auto
    3.76 +
    3.77 +lemma rel_pow_E: 
    3.78 +    "[| (x,z) : R^n;  [| n=0; x = z |] ==> P;         
    3.79 +        !!y m. [| n = Suc m; (x,y) : R^m; (y,z) : R |] ==> P   
    3.80 +     |] ==> P"
    3.81 +by (case_tac "n", auto)
    3.82 +
    3.83 +lemma rel_pow_Suc_D2 [rule_format]:
    3.84 +     "\<forall>x z. (x,z):R^(Suc n) --> (\<exists>y. (x,y):R & (y,z):R^n)"
    3.85 +apply (induct_tac "n")
    3.86 +apply (blast intro: rel_pow_0_I elim: rel_pow_0_E rel_pow_Suc_E)
    3.87 +apply (blast intro: rel_pow_Suc_I elim: rel_pow_0_E rel_pow_Suc_E)
    3.88 +done
    3.89 +
    3.90 +
    3.91 +lemma rel_pow_Suc_D2':
    3.92 +     "\<forall>x y z. (x,y) : R^n & (y,z) : R --> (\<exists>w. (x,w) : R & (w,z) : R^n)"
    3.93 +by (induct_tac "n", simp_all, blast)
    3.94 +
    3.95 +lemma rel_pow_E2: 
    3.96 +    "[| (x,z) : R^n;  [| n=0; x = z |] ==> P;         
    3.97 +        !!y m. [| n = Suc m; (x,y) : R; (y,z) : R^m |] ==> P   
    3.98 +     |] ==> P"
    3.99 +apply (case_tac "n", simp) 
   3.100 +apply (cut_tac n=nat and R=R in rel_pow_Suc_D2', simp, blast) 
   3.101 +done
   3.102 +
   3.103 +lemma rtrancl_imp_UN_rel_pow: "!!p. p:R^* ==> p : (UN n. R^n)"
   3.104 +apply (simp only: split_tupled_all)
   3.105 +apply (erule rtrancl_induct)
   3.106 +apply (blast intro: rel_pow_0_I rel_pow_Suc_I)+
   3.107 +done
   3.108 +
   3.109 +lemma rel_pow_imp_rtrancl: "!!p. p:R^n ==> p:R^*"
   3.110 +apply (simp only: split_tupled_all)
   3.111 +apply (induct "n")
   3.112 +apply (blast intro: rtrancl_refl elim: rel_pow_0_E)
   3.113 +apply (blast elim: rel_pow_Suc_E intro: rtrancl_into_rtrancl)
   3.114 +done
   3.115 +
   3.116 +lemma rtrancl_is_UN_rel_pow: "R^* = (UN n. R^n)"
   3.117 +by (blast intro: rtrancl_imp_UN_rel_pow rel_pow_imp_rtrancl)
   3.118 +
   3.119 +
   3.120 +lemma single_valued_rel_pow [rule_format]:
   3.121 +     "!!r::('a * 'a)set. single_valued r ==> single_valued (r^n)"
   3.122 +apply (rule single_valuedI)
   3.123 +apply (induct_tac "n", simp)
   3.124 +apply (fast dest: single_valuedD elim: rel_pow_Suc_E)
   3.125 +done
   3.126 +
   3.127 +ML
   3.128 +{*
   3.129 +val funpow_add = thm "funpow_add";
   3.130 +val rel_pow_1 = thm "rel_pow_1";
   3.131 +val rel_pow_0_I = thm "rel_pow_0_I";
   3.132 +val rel_pow_Suc_I = thm "rel_pow_Suc_I";
   3.133 +val rel_pow_Suc_I2 = thm "rel_pow_Suc_I2";
   3.134 +val rel_pow_0_E = thm "rel_pow_0_E";
   3.135 +val rel_pow_Suc_E = thm "rel_pow_Suc_E";
   3.136 +val rel_pow_E = thm "rel_pow_E";
   3.137 +val rel_pow_Suc_D2 = thm "rel_pow_Suc_D2";
   3.138 +val rel_pow_Suc_D2 = thm "rel_pow_Suc_D2";
   3.139 +val rel_pow_E2 = thm "rel_pow_E2";
   3.140 +val rtrancl_imp_UN_rel_pow = thm "rtrancl_imp_UN_rel_pow";
   3.141 +val rel_pow_imp_rtrancl = thm "rel_pow_imp_rtrancl";
   3.142 +val rtrancl_is_UN_rel_pow = thm "rtrancl_is_UN_rel_pow";
   3.143 +val single_valued_rel_pow = thm "single_valued_rel_pow";
   3.144 +*}
   3.145 +
   3.146  end