nipkow@10213: (* Title: HOL/Relation_Power.thy nipkow@10213: ID: $Id$ nipkow@10213: Author: Tobias Nipkow nipkow@10213: Copyright 1996 TU Muenchen paulson@15410: *) nipkow@11306: paulson@15410: header{*Powers of Relations and Functions*} nipkow@10213: nipkow@15131: theory Relation_Power haftmann@24996: imports Power nipkow@15131: begin nipkow@10213: nipkow@10213: instance wenzelm@18398: set :: (type) power .. paulson@15410: --{* only type @{typ "('a * 'a) set"} should be in class @{text power}!*} nipkow@10213: haftmann@25861: overloading haftmann@25861: relpow \ "power \ ('a \ 'a) set \ nat \ ('a \ 'a) set" (unchecked) haftmann@25861: begin haftmann@25861: haftmann@25861: text {* @{text "R ^ n = R O ... O R"}, the n-fold composition of @{text R} *} nipkow@10213: haftmann@25861: primrec relpow where haftmann@25861: "(R \ ('a \ 'a) set) ^ 0 = Id" haftmann@25861: | "(R \ ('a \ 'a) set) ^ Suc n = R O (R ^ n)" haftmann@25861: haftmann@25861: end nipkow@11305: nipkow@11306: instance haftmann@21414: "fun" :: (type, type) power .. paulson@15410: --{* only type @{typ "'a => 'a"} should be in class @{text power}!*} nipkow@11305: haftmann@25861: overloading haftmann@25861: funpow \ "power \ ('a \ 'a) \ nat \ 'a \ 'a" (unchecked) haftmann@25861: begin haftmann@25861: haftmann@25861: text {* @{text "f ^ n = f o ... o f"}, the n-fold composition of @{text f} *} haftmann@25861: haftmann@25861: primrec funpow where haftmann@25861: "(f \ 'a \ 'a) ^ 0 = id" haftmann@25861: | "(f \ 'a \ 'a) ^ Suc n = f o (f ^ n)" haftmann@25861: haftmann@25861: end nipkow@11305: paulson@15410: text{*WARNING: due to the limits of Isabelle's type classes, exponentiation on paulson@15410: functions and relations has too general a domain, namely @{typ "('a * 'b)set"} paulson@15410: and @{typ "'a => 'b"}. Explicit type constraints may therefore be necessary. paulson@15410: For example, @{term "range(f^n) = A"} and @{term "Range(R^n) = B"} need paulson@15410: constraints.*} paulson@15410: haftmann@21414: text {* haftmann@21414: Circumvent this problem for code generation: haftmann@21414: *} haftmann@21414: haftmann@25861: primrec haftmann@25861: fun_pow :: "nat \ ('a \ 'a) \ 'a \ 'a" haftmann@22737: where haftmann@25861: "fun_pow 0 f = id" haftmann@25861: | "fun_pow (Suc n) f = f o fun_pow n f" haftmann@21414: haftmann@25861: lemma funpow_fun_pow [code inline]: "f ^ n = fun_pow n f" haftmann@25861: unfolding funpow_def fun_pow_def .. haftmann@21414: nipkow@15112: lemma funpow_add: "f ^ (m+n) = f^m o f^n" wenzelm@18398: by (induct m) simp_all nipkow@15112: nipkow@18049: lemma funpow_swap1: "f((f^n) x) = (f^n)(f x)" nipkow@18049: proof - nipkow@18049: have "f((f^n) x) = (f^(n+1)) x" by simp wenzelm@18398: also have "\ = (f^n o f^1) x" by (simp only: funpow_add) nipkow@18049: also have "\ = (f^n)(f x)" by simp nipkow@18049: finally show ?thesis . nipkow@18049: qed nipkow@18049: wenzelm@18398: lemma rel_pow_1 [simp]: wenzelm@18398: fixes R :: "('a*'a)set" wenzelm@18398: shows "R^1 = R" wenzelm@18398: by simp paulson@15410: paulson@15410: lemma rel_pow_0_I: "(x,x) : R^0" wenzelm@18398: by simp paulson@15410: paulson@15410: lemma rel_pow_Suc_I: "[| (x,y) : R^n; (y,z):R |] ==> (x,z):R^(Suc n)" wenzelm@18398: by auto paulson@15410: wenzelm@18398: lemma rel_pow_Suc_I2: wenzelm@18398: "(x, y) : R \ (y, z) : R^n \ (x,z) : R^(Suc n)" wenzelm@20503: apply (induct n arbitrary: z) wenzelm@18398: apply simp wenzelm@18398: apply fastsimp wenzelm@18398: done paulson@15410: paulson@15410: lemma rel_pow_0_E: "[| (x,y) : R^0; x=y ==> P |] ==> P" wenzelm@18398: by simp paulson@15410: wenzelm@18398: lemma rel_pow_Suc_E: wenzelm@18398: "[| (x,z) : R^(Suc n); !!y. [| (x,y) : R^n; (y,z) : R |] ==> P |] ==> P" wenzelm@18398: by auto paulson@15410: wenzelm@18398: lemma rel_pow_E: wenzelm@18398: "[| (x,z) : R^n; [| n=0; x = z |] ==> P; wenzelm@18398: !!y m. [| n = Suc m; (x,y) : R^m; (y,z) : R |] ==> P paulson@15410: |] ==> P" wenzelm@18398: by (cases n) auto paulson@15410: wenzelm@18398: lemma rel_pow_Suc_D2: wenzelm@18398: "(x, z) : R^(Suc n) \ (\y. (x,y) : R & (y,z) : R^n)" wenzelm@20503: apply (induct n arbitrary: x z) wenzelm@18398: apply (blast intro: rel_pow_0_I elim: rel_pow_0_E rel_pow_Suc_E) wenzelm@18398: apply (blast intro: rel_pow_Suc_I elim: rel_pow_0_E rel_pow_Suc_E) wenzelm@18398: done paulson@15410: paulson@15410: lemma rel_pow_Suc_D2': wenzelm@18398: "\x y z. (x,y) : R^n & (y,z) : R --> (\w. (x,w) : R & (w,z) : R^n)" wenzelm@18398: by (induct n) (simp_all, blast) paulson@15410: wenzelm@18398: lemma rel_pow_E2: wenzelm@18398: "[| (x,z) : R^n; [| n=0; x = z |] ==> P; wenzelm@18398: !!y m. [| n = Suc m; (x,y) : R; (y,z) : R^m |] ==> P paulson@15410: |] ==> P" wenzelm@18398: apply (case_tac n, simp) wenzelm@18398: apply (cut_tac n=nat and R=R in rel_pow_Suc_D2', simp, blast) wenzelm@18398: done paulson@15410: paulson@15410: lemma rtrancl_imp_UN_rel_pow: "!!p. p:R^* ==> p : (UN n. R^n)" wenzelm@18398: apply (simp only: split_tupled_all) wenzelm@18398: apply (erule rtrancl_induct) wenzelm@18398: apply (blast intro: rel_pow_0_I rel_pow_Suc_I)+ wenzelm@18398: done paulson@15410: paulson@15410: lemma rel_pow_imp_rtrancl: "!!p. p:R^n ==> p:R^*" wenzelm@18398: apply (simp only: split_tupled_all) wenzelm@18398: apply (induct n) wenzelm@18398: apply (blast intro: rtrancl_refl elim: rel_pow_0_E) wenzelm@18398: apply (blast elim: rel_pow_Suc_E intro: rtrancl_into_rtrancl) wenzelm@18398: done paulson@15410: paulson@15410: lemma rtrancl_is_UN_rel_pow: "R^* = (UN n. R^n)" wenzelm@18398: by (blast intro: rtrancl_imp_UN_rel_pow rel_pow_imp_rtrancl) paulson@15410: kleing@25295: lemma trancl_power: kleing@25295: "x \ r^+ = (\n > 0. x \ r^n)" kleing@25295: apply (cases x) kleing@25295: apply simp kleing@25295: apply (rule iffI) kleing@25295: apply (drule tranclD2) kleing@25295: apply (clarsimp simp: rtrancl_is_UN_rel_pow) kleing@25295: apply (rule_tac x="Suc x" in exI) kleing@25295: apply (clarsimp simp: rel_comp_def) kleing@25295: apply fastsimp kleing@25295: apply clarsimp kleing@25295: apply (case_tac n, simp) kleing@25295: apply clarsimp kleing@25295: apply (drule rel_pow_imp_rtrancl) kleing@25295: apply fastsimp kleing@25295: done paulson@15410: wenzelm@18398: lemma single_valued_rel_pow: wenzelm@18398: "!!r::('a * 'a)set. single_valued r ==> single_valued (r^n)" wenzelm@18398: apply (rule single_valuedI) wenzelm@18398: apply (induct n) wenzelm@18398: apply simp wenzelm@18398: apply (fast dest: single_valuedD elim: rel_pow_Suc_E) wenzelm@18398: done paulson@15410: paulson@15410: ML paulson@15410: {* paulson@15410: val funpow_add = thm "funpow_add"; paulson@15410: val rel_pow_1 = thm "rel_pow_1"; paulson@15410: val rel_pow_0_I = thm "rel_pow_0_I"; paulson@15410: val rel_pow_Suc_I = thm "rel_pow_Suc_I"; paulson@15410: val rel_pow_Suc_I2 = thm "rel_pow_Suc_I2"; paulson@15410: val rel_pow_0_E = thm "rel_pow_0_E"; paulson@15410: val rel_pow_Suc_E = thm "rel_pow_Suc_E"; paulson@15410: val rel_pow_E = thm "rel_pow_E"; paulson@15410: val rel_pow_Suc_D2 = thm "rel_pow_Suc_D2"; paulson@15410: val rel_pow_Suc_D2 = thm "rel_pow_Suc_D2"; paulson@15410: val rel_pow_E2 = thm "rel_pow_E2"; paulson@15410: val rtrancl_imp_UN_rel_pow = thm "rtrancl_imp_UN_rel_pow"; paulson@15410: val rel_pow_imp_rtrancl = thm "rel_pow_imp_rtrancl"; paulson@15410: val rtrancl_is_UN_rel_pow = thm "rtrancl_is_UN_rel_pow"; paulson@15410: val single_valued_rel_pow = thm "single_valued_rel_pow"; paulson@15410: *} paulson@15410: nipkow@10213: end