src/HOL/Relation_Power.thy
 author wenzelm Mon Mar 16 18:24:30 2009 +0100 (2009-03-16) changeset 30549 d2d7874648bd parent 30079 293b896b9c25 child 30949 37f887b55e7f permissions -rw-r--r--
simplified method setup;
```     1 (*  Title:      HOL/Relation_Power.thy
```
```     2     Author:     Tobias Nipkow
```
```     3     Copyright   1996  TU Muenchen
```
```     4 *)
```
```     5
```
```     6 header{*Powers of Relations and Functions*}
```
```     7
```
```     8 theory Relation_Power
```
```     9 imports Power Transitive_Closure Plain
```
```    10 begin
```
```    11
```
```    12 instance
```
```    13   "fun" :: (type, type) power ..
```
```    14       --{* only type @{typ "'a => 'a"} should be in class @{text power}!*}
```
```    15
```
```    16 overloading
```
```    17   relpow \<equiv> "power \<Colon> ('a \<times> 'a) set \<Rightarrow> nat \<Rightarrow> ('a \<times> 'a) set"  (unchecked)
```
```    18 begin
```
```    19
```
```    20 text {* @{text "R ^ n = R O ... O R"}, the n-fold composition of @{text R} *}
```
```    21
```
```    22 primrec relpow where
```
```    23   "(R \<Colon> ('a \<times> 'a) set)  ^ 0 = Id"
```
```    24   | "(R \<Colon> ('a \<times> 'a) set) ^ Suc n = R O (R ^ n)"
```
```    25
```
```    26 end
```
```    27
```
```    28 overloading
```
```    29   funpow \<equiv> "power \<Colon>  ('a \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> 'a" (unchecked)
```
```    30 begin
```
```    31
```
```    32 text {* @{text "f ^ n = f o ... o f"}, the n-fold composition of @{text f} *}
```
```    33
```
```    34 primrec funpow where
```
```    35   "(f \<Colon> 'a \<Rightarrow> 'a) ^ 0 = id"
```
```    36   | "(f \<Colon> 'a \<Rightarrow> 'a) ^ Suc n = f o (f ^ n)"
```
```    37
```
```    38 end
```
```    39
```
```    40 text{*WARNING: due to the limits of Isabelle's type classes, exponentiation on
```
```    41 functions and relations has too general a domain, namely @{typ "('a * 'b)set"}
```
```    42 and @{typ "'a => 'b"}.  Explicit type constraints may therefore be necessary.
```
```    43 For example, @{term "range(f^n) = A"} and @{term "Range(R^n) = B"} need
```
```    44 constraints.*}
```
```    45
```
```    46 text {*
```
```    47   Circumvent this problem for code generation:
```
```    48 *}
```
```    49
```
```    50 primrec
```
```    51   fun_pow :: "nat \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a"
```
```    52 where
```
```    53   "fun_pow 0 f = id"
```
```    54   | "fun_pow (Suc n) f = f o fun_pow n f"
```
```    55
```
```    56 lemma funpow_fun_pow [code unfold]: "f ^ n = fun_pow n f"
```
```    57   unfolding funpow_def fun_pow_def ..
```
```    58
```
```    59 lemma funpow_add: "f ^ (m+n) = f^m o f^n"
```
```    60   by (induct m) simp_all
```
```    61
```
```    62 lemma funpow_swap1: "f((f^n) x) = (f^n)(f x)"
```
```    63 proof -
```
```    64   have "f((f^n) x) = (f^(n+1)) x" unfolding One_nat_def by simp
```
```    65   also have "\<dots>  = (f^n o f^1) x" by (simp only: funpow_add)
```
```    66   also have "\<dots> = (f^n)(f x)" unfolding One_nat_def by simp
```
```    67   finally show ?thesis .
```
```    68 qed
```
```    69
```
```    70 lemma rel_pow_1 [simp]:
```
```    71   fixes R :: "('a*'a)set"
```
```    72   shows "R^1 = R"
```
```    73   unfolding One_nat_def by simp
```
```    74
```
```    75 lemma rel_pow_0_I: "(x,x) : R^0"
```
```    76   by simp
```
```    77
```
```    78 lemma rel_pow_Suc_I: "[| (x,y) : R^n; (y,z):R |] ==> (x,z):R^(Suc n)"
```
```    79   by auto
```
```    80
```
```    81 lemma rel_pow_Suc_I2:
```
```    82     "(x, y) : R \<Longrightarrow> (y, z) : R^n \<Longrightarrow> (x,z) : R^(Suc n)"
```
```    83   apply (induct n arbitrary: z)
```
```    84    apply simp
```
```    85   apply fastsimp
```
```    86   done
```
```    87
```
```    88 lemma rel_pow_0_E: "[| (x,y) : R^0; x=y ==> P |] ==> P"
```
```    89   by simp
```
```    90
```
```    91 lemma rel_pow_Suc_E:
```
```    92     "[| (x,z) : R^(Suc n);  !!y. [| (x,y) : R^n; (y,z) : R |] ==> P |] ==> P"
```
```    93   by auto
```
```    94
```
```    95 lemma rel_pow_E:
```
```    96     "[| (x,z) : R^n;  [| n=0; x = z |] ==> P;
```
```    97         !!y m. [| n = Suc m; (x,y) : R^m; (y,z) : R |] ==> P
```
```    98      |] ==> P"
```
```    99   by (cases n) auto
```
```   100
```
```   101 lemma rel_pow_Suc_D2:
```
```   102     "(x, z) : R^(Suc n) \<Longrightarrow> (\<exists>y. (x,y) : R & (y,z) : R^n)"
```
```   103   apply (induct n arbitrary: x z)
```
```   104    apply (blast intro: rel_pow_0_I elim: rel_pow_0_E rel_pow_Suc_E)
```
```   105   apply (blast intro: rel_pow_Suc_I elim: rel_pow_0_E rel_pow_Suc_E)
```
```   106   done
```
```   107
```
```   108 lemma rel_pow_Suc_D2':
```
```   109     "\<forall>x y z. (x,y) : R^n & (y,z) : R --> (\<exists>w. (x,w) : R & (w,z) : R^n)"
```
```   110   by (induct n) (simp_all, blast)
```
```   111
```
```   112 lemma rel_pow_E2:
```
```   113     "[| (x,z) : R^n;  [| n=0; x = z |] ==> P;
```
```   114         !!y m. [| n = Suc m; (x,y) : R; (y,z) : R^m |] ==> P
```
```   115      |] ==> P"
```
```   116   apply (case_tac n, simp)
```
```   117   apply (cut_tac n=nat and R=R in rel_pow_Suc_D2', simp, blast)
```
```   118   done
```
```   119
```
```   120 lemma rtrancl_imp_UN_rel_pow: "!!p. p:R^* ==> p : (UN n. R^n)"
```
```   121   apply (simp only: split_tupled_all)
```
```   122   apply (erule rtrancl_induct)
```
```   123    apply (blast intro: rel_pow_0_I rel_pow_Suc_I)+
```
```   124   done
```
```   125
```
```   126 lemma rel_pow_imp_rtrancl: "!!p. p:R^n ==> p:R^*"
```
```   127   apply (simp only: split_tupled_all)
```
```   128   apply (induct n)
```
```   129    apply (blast intro: rtrancl_refl elim: rel_pow_0_E)
```
```   130   apply (blast elim: rel_pow_Suc_E intro: rtrancl_into_rtrancl)
```
```   131   done
```
```   132
```
```   133 lemma rtrancl_is_UN_rel_pow: "R^* = (UN n. R^n)"
```
```   134   by (blast intro: rtrancl_imp_UN_rel_pow rel_pow_imp_rtrancl)
```
```   135
```
```   136 lemma trancl_power:
```
```   137   "x \<in> r^+ = (\<exists>n > 0. x \<in> r^n)"
```
```   138   apply (cases x)
```
```   139   apply simp
```
```   140   apply (rule iffI)
```
```   141    apply (drule tranclD2)
```
```   142    apply (clarsimp simp: rtrancl_is_UN_rel_pow)
```
```   143    apply (rule_tac x="Suc x" in exI)
```
```   144    apply (clarsimp simp: rel_comp_def)
```
```   145    apply fastsimp
```
```   146   apply clarsimp
```
```   147   apply (case_tac n, simp)
```
```   148   apply clarsimp
```
```   149   apply (drule rel_pow_imp_rtrancl)
```
```   150   apply fastsimp
```
```   151   done
```
```   152
```
```   153 lemma single_valued_rel_pow:
```
```   154     "!!r::('a * 'a)set. single_valued r ==> single_valued (r^n)"
```
```   155   apply (rule single_valuedI)
```
```   156   apply (induct n)
```
```   157    apply simp
```
```   158   apply (fast dest: single_valuedD elim: rel_pow_Suc_E)
```
```   159   done
```
```   160
```
```   161 ML
```
```   162 {*
```
```   163 val funpow_add = thm "funpow_add";
```
```   164 val rel_pow_1 = thm "rel_pow_1";
```
```   165 val rel_pow_0_I = thm "rel_pow_0_I";
```
```   166 val rel_pow_Suc_I = thm "rel_pow_Suc_I";
```
```   167 val rel_pow_Suc_I2 = thm "rel_pow_Suc_I2";
```
```   168 val rel_pow_0_E = thm "rel_pow_0_E";
```
```   169 val rel_pow_Suc_E = thm "rel_pow_Suc_E";
```
```   170 val rel_pow_E = thm "rel_pow_E";
```
```   171 val rel_pow_Suc_D2 = thm "rel_pow_Suc_D2";
```
```   172 val rel_pow_Suc_D2 = thm "rel_pow_Suc_D2";
```
```   173 val rel_pow_E2 = thm "rel_pow_E2";
```
```   174 val rtrancl_imp_UN_rel_pow = thm "rtrancl_imp_UN_rel_pow";
```
```   175 val rel_pow_imp_rtrancl = thm "rel_pow_imp_rtrancl";
```
```   176 val rtrancl_is_UN_rel_pow = thm "rtrancl_is_UN_rel_pow";
```
```   177 val single_valued_rel_pow = thm "single_valued_rel_pow";
```
```   178 *}
```
```   179
```
```   180 end
```