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: paulson@15410: (*R^n = R O ... O R, the n-fold composition of R*) haftmann@24304: primrec (unchecked relpow) nipkow@10213: "R^0 = Id" nipkow@10213: "R^(Suc n) = R O (R^n)" nipkow@10213: 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: paulson@15410: (*f^n = f o ... o f, the n-fold composition of f*) haftmann@24304: primrec (unchecked funpow) nipkow@11305: "f^0 = id" nipkow@11305: "f^(Suc n) = f o (f^n)" 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@21414: definition haftmann@22737: funpow :: "nat \ ('a \ 'a) \ 'a \ 'a" haftmann@22737: where haftmann@21414: funpow_def: "funpow n f = f ^ n" haftmann@21414: haftmann@21414: lemmas [code inline] = funpow_def [symmetric] haftmann@21414: haftmann@21414: lemma [code func]: haftmann@21414: "funpow 0 f = id" haftmann@21414: "funpow (Suc n) f = f o funpow n f" haftmann@21414: unfolding funpow_def by simp_all 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: 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