--- 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 \
--- 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";
-
-
-
-
--- 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]:
+ "\<forall>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]:
+ "\<forall>x z. (x,z):R^(Suc n) --> (\<exists>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':
+ "\<forall>x y z. (x,y) : R^n & (y,z) : R --> (\<exists>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