20   that are represented by predicates.
24   "equivp E \<equiv> \<forall>x y. E x y = (E x = E y)"
27   "reflp E \<equiv> \<forall>x. E x x"
30   "symp E \<equiv> \<forall>x y. E x y \<longrightarrow> E y x"
33   "transp E \<equiv> \<forall>x y z. E x y \<and> E y z \<longrightarrow> E x z"
36   shows "equivp E = (reflp E \<and> symp E \<and> transp E)"
41   shows "equivp E \<Longrightarrow> E x x"
45   shows "equivp E \<Longrightarrow> E x y \<Longrightarrow> E y x"
49   shows "equivp E \<Longrightarrow> E x y \<Longrightarrow> E y z \<Longrightarrow> E x z"
53   assumes "reflp R" "symp R" "transp R"
58   shows "equivp (op =)"
65   "part_equivp E \<equiv> (\<exists>x. E x x) \<and> (\<forall>x y. E x y = (E x x \<and> E y y \<and> (E x = E y)))"
68   assumes a: "equivp E"
75   assumes e: "part_equivp R"
76   and a: "R x y"
77   shows "R y x"
82   shows "part_equivp R \<Longrightarrow> \<exists>d. d \<in> (\<lambda>c. \<exists>x. R x x \<and> c = R x)"
96   "r1 OOO r2 \<equiv> r1 OO r2 OO r1"
99   shows "((op =) OOO R) = R"
107   "Respects R x \<equiv> R x x"
110   shows "(x \<in> Respects R) = R x x"
119 [simp]: "fun_map f g h x = g (h (f x))"
124 [simp]: "fun_rel E1 E2 f g = (\<forall>x y. E1 x y \<longrightarrow> E2 (f x) (g y))"
127   assumes "\<And>a b. P a b \<Longrightarrow> Q (x a) (y b)"
128   shows "(P ===> Q) x y"
132   shows "(id ---> id) = id"
136   shows "((op =) ===> (op =)) = (op =)"
145      (\<forall>r s. E r s = (E r r \<and> E s s \<and> (Abs r = Abs s)))"
148   assumes a: "Quotient E Abs Rep"
149   shows "Abs (Rep a) = a"
155   assumes a: "Quotient E Abs Rep"
156   shows "E (Rep a) (Rep a)"
162   assumes a: "Quotient E Abs Rep"
163   shows " E r s = (E r r \<and> E s s \<and> (Abs r = Abs s))"
169   assumes a: "Quotient R Abs Rep"
170   shows "R (Rep a) (Rep b) = (a = b)"
176   assumes a: "Quotient R Abs Rep"
177   shows "R r r \<Longrightarrow> R (Rep (Abs r)) r"
182   assumes a: "Quotient E Abs Rep"
183   shows "E r s \<Longrightarrow> Abs r = Abs s"
188   assumes a: "Quotient E Abs Rep"
194   assumes a: "Quotient E Abs Rep"
200   shows "Quotient (op =) id id"
205   assumes q1: "Quotient R1 abs1 rep1"
206   and     q2: "Quotient R2 abs2 rep2"
207   shows "Quotient (R1 ===> R2) (rep1 ---> abs2) (abs1 ---> rep2)"
209   have "\<forall>a. (rep1 ---> abs2) ((abs1 ---> rep2) a) = a"
215   have "\<forall>a. (R1 ===> R2) ((abs1 ---> rep2) a) ((abs1 ---> rep2) a)"
221         (rep1 ---> abs2) r  = (rep1 ---> abs2) s)"
234   show "Quotient (R1 ===> R2) (rep1 ---> abs2) (abs1 ---> rep2)"
239   assumes a: "Quotient R Abs Rep"
240   shows "Abs o Rep = id"
245   assumes q: "Quotient R Abs Rep"
246   and     a: "R xa xb" "R ya yb"
247   shows "R xa ya = R xb yb"
253   assumes q1: "Quotient R1 Abs1 Rep1"
254   and     q2: "Quotient R2 Abs2 Rep2"
255   shows "(Rep1 ---> Abs2) (\<lambda>x. Rep2 (f (Abs1 x))) = (\<lambda>x. f x)"
261   assumes q1: "Quotient R1 Abs1 Rep1"
262   and     q2: "Quotient R2 Abs2 Rep2"
263   shows "(Rep1 ---> Abs2) (\<lambda>x. (Abs1 ---> Rep2) f x) = (\<lambda>x. f x)"
269   assumes q: "Quotient R Abs Rep"
270   and     a: "R x1 x2"
271   shows "R x1 (Rep (Abs x2))"
276   assumes q: "Quotient R Abs Rep"
277   and     a: "R x1 x2"
278   shows "R (Rep (Abs x1)) x2"
290   fixes f g::"'a \<Rightarrow> 'c"
291   assumes q: "Quotient R1 Abs1 Rep1"
292   and     a: "(R1 ===> R2) f g" "R1 x y"
293   shows "R2 (f x) (g y)"
297   assumes a: "(R1 ===> R2) f g" "R1 x y"
298   shows "R2 (f x) (g y)"
304   fixes P :: "'a \<Rightarrow> bool"
305   assumes a: "equivp R"
306   shows "Ball (Respects R) P = (All P)"
312   fixes P :: "'a \<Rightarrow> bool"
313   assumes a: "equivp R"
314   shows "Bex (Respects R) P = (Ex P)"
320   assumes a: "\<And>x. R x \<Longrightarrow> P x \<longrightarrow> Q x"
321   shows "All P \<longrightarrow> Ball R Q"
325   assumes a: "\<And>x. R x \<Longrightarrow> Q x \<longrightarrow> P x"
326   shows "Bex R Q \<longrightarrow> Ex P"
330   assumes a: "equivp R"
331   shows "(\<And>x. (Q x \<longrightarrow> P x)) \<Longrightarrow> Ball (Respects R) Q \<longrightarrow> All P"
335   assumes a: "equivp R"
336   shows "(\<And>x. (Q x \<longrightarrow> P x)) \<Longrightarrow> Ex Q \<longrightarrow> Bex (Respects R) P"
340   fixes P::"'a \<Rightarrow> bool"
342   assumes a: "equivp R2"
343   shows   "(Ball (Respects (R1 ===> R2)) (\<lambda>f. P (f x)) = All (\<lambda>f. P (f x)))"
356   assumes a: "equivp R2"
357   shows   "(Bex (Respects (R1 ===> R2)) (\<lambda>f. P (f x)) = Ex (\<lambda>f. P (f x)))"
369   assumes a: "!x :: 'a. (P x --> Q x)"
370   and     b: "All P"
375   assumes a: "!x :: 'a. (P x --> Q x)"
376   and     b: "Ex P"
381   assumes a: "!x :: 'a. (R x --> P x --> Q x)"
382   and     b: "Ball R P"
383   shows "Ball R Q"
387   assumes a: "!x :: 'a. (R x --> P x --> Q x)"
388   and     b: "Bex R P"
389   shows "Bex R Q"
394   assumes "\<And>y. (\<forall>x\<in>P. A x y) \<longrightarrow> (\<forall>x. B x y)"
395   shows "(\<forall>x\<in>P. \<forall>y. A x y) \<longrightarrow> (\<forall>x. \<forall>y. B x y)"
399   assumes "(\<exists>y. \<exists>x. A x y) \<longrightarrow> (\<exists>y. \<exists>x\<in>P. B x y)"
400   shows "(\<exists>x. \<exists>y. A x y) \<longrightarrow> (\<exists>x\<in>P. \<exists>y. B x y)"
406   Babs :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b"
408   "x \<in> p \<Longrightarrow> Babs p m x = m x"
411   assumes q: "Quotient R1 Abs1 Rep1"
412   and     a: "(R1 ===> R2) f g"
413   shows      "(R1 ===> R2) (Babs (Respects R1) f) (Babs (Respects R1) g)"
422   assumes q1: "Quotient R1 Abs1 Rep1"
423   and     q2: "Quotient R2 Abs2 Rep2"
424   shows "((Rep1 ---> Abs2) (Babs (Respects R1) ((Abs1 ---> Rep2) f))) = f"
433   assumes q: "Quotient R1 Abs Rep"
434   shows "((R1 ===> R2) (Babs (Respects R1) f) (Babs (Respects R1) g)) = ((R1 ===> R2) f g)"
447   shows "equivp R \<Longrightarrow> Babs (Respects R) P = P"
453   assumes a: "(R ===> (op =)) f g"
454   shows "Ball (Respects R) f = Ball (Respects R) g"
458   assumes a: "(R ===> (op =)) f g"
459   shows "(Bex (Respects R) f = Bex (Respects R) g)"
463   assumes a: "(R ===> (op =)) f g"
464   shows "Ex1 (\<lambda>x. x \<in> Respects R \<and> f x) = Ex1 (\<lambda>x. x \<in> Respects R \<and> g x)"
470   assumes a: "Quotient R absf repf"
471   shows "Ball (Respects R) ((absf ---> id) f) = All f"
476   assumes a: "Quotient R absf repf"
477   shows "Bex (Respects R) ((absf ---> id) f) = Ex f"
484   Bex1_rel :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool"
486   "Bex1_rel R P \<longleftrightarrow> (\<exists>x \<in> Respects R. P x) \<and> (\<forall>x \<in> Respects R. \<forall>y \<in> Respects R. ((P x \<and> P y) \<longrightarrow> (R x y)))"
489   "\<lbrakk>\<forall>xa ya. R xa ya \<longrightarrow> x xa = y ya; Bex1_rel R x\<rbrakk> \<Longrightarrow> Bex1_rel R y"
508   "\<lbrakk>\<forall>xa ya. R xa ya \<longrightarrow> x xa = y ya; Bex1_rel R y\<rbrakk> \<Longrightarrow> Bex1_rel R x"
527   assumes a: "Quotient R absf repf"
528   shows "((R ===> op =) ===> op =) (Bex1_rel R) (Bex1_rel R)"
539   assumes a: "Quotient R absf repf"
540   shows "((absf ---> id) ---> id) (Bex1_rel R) f = Ex1 f"
575   shows "(\<exists>!x\<in>Respects R. P x) \<longrightarrow> (Bex1_rel R (\<lambda>x. P x))"
587   assumes a: "equivp R"
588   shows "(\<exists>!x. P x) \<longrightarrow> Bex1_rel R P"
606   assumes a: "Quotient R Abs Rep"
607   shows "(R ===> R ===> op =) R R"
614   assumes q1: "Quotient R1 Abs1 Rep1"
615   and     q2: "Quotient R2 Abs2 Rep2"
616   and     q3: "Quotient R3 Abs3 Rep3"
617   shows "((Abs2 ---> Rep3) ---> (Abs1 ---> Rep2) ---> (Rep1 ---> Abs3)) op \<circ> = op \<circ>"
618   and   "(id ---> (Abs1 ---> id) ---> Rep1 ---> id) op \<circ> = op \<circ>"
623   "((R2 ===> R3) ===> (R1 ===> R2) ===> (R1 ===> R3)) op \<circ> op \<circ>"
624   "(op = ===> (R1 ===> op =) ===> R1 ===> op =) op \<circ> op \<circ>"
628   assumes a: "Quotient R absf repf"
629   shows "absf (if a then repf b else repf c) = (if a then b else c)"
633   assumes q: "Quotient R Abs Rep"
634   shows "(id ---> Rep ---> Rep ---> Abs) If = If"
639   assumes q: "Quotient R Abs Rep"
640   shows "(op = ===> R ===> R ===> R) If If"
644   assumes q1: "Quotient R1 Abs1 Rep1"
645   and     q2: "Quotient R2 Abs2 Rep2"
646   shows "(Rep2 ---> (Abs2 ---> Rep1) ---> Abs1) Let = Let"
651   shows "(R1 ===> (R1 ===> R2) ===> R2) Let Let"
655   fixes R :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
656   and   Abs :: "('a \<Rightarrow> bool) \<Rightarrow> 'b"
657   and   Rep :: "'b \<Rightarrow> ('a \<Rightarrow> bool)"
658   assumes equivp: "part_equivp R"
659   and     rep_prop: "\<And>y. \<exists>x. R x x \<and> Rep y = R x"
660   and     rep_inverse: "\<And>x. Abs (Rep x) = x"
661   and     abs_inverse: "\<And>c. (\<exists>x. ((R x x) \<and> (c = R x))) \<Longrightarrow> (Rep (Abs c)) = c"
662   and     rep_inject: "\<And>x y. (Rep x = Rep y) = (x = y)"
668   "abs x \<equiv> Abs (R x)"
673   "rep a = Eps (Rep a)"
676   assumes a: "R r r"
677   shows "Rep (Abs (R r)) = R r"
682   assumes a: "R r r"
683   and b: "R s s"
684   shows "Abs (R r) = Abs (R s) \<longleftrightarrow> R r = R s"
688   assumes "R r r"
689   shows "R (Eps (R r)) = R r"
695   shows "Quotient R abs rep"
699     show "Abs (R (Eps (Rep a))) = a"
701     show "R r s \<longleftrightarrow> R r r \<and> R s s \<and> (Abs (R r) = Abs (R s))"
752   about the lifted theorem in a tactic.
755   "Quot_True (x :: 'a) \<equiv> True"
758   shows QT_all: "Quot_True (All P) \<Longrightarrow> Quot_True P"
759   and   QT_ex:  "Quot_True (Ex P) \<Longrightarrow> Quot_True P"
760   and   QT_ex1: "Quot_True (Ex1 P) \<Longrightarrow> Quot_True P"
761   and   QT_lam: "Quot_True (\<lambda>x. P x) \<Longrightarrow> (\<And>x. Quot_True (P x))"
762   and   QT_ext: "(\<And>x. Quot_True (a x) \<Longrightarrow> f x = g x) \<Longrightarrow> (Quot_True a \<Longrightarrow> f = g)"
765 lemma QT_imp: "Quot_True a \<equiv> Quot_True b"