# HG changeset patch
# User slotosch
# Date 860162474 -7200
# Node ID fc10751254aac247d45bb0b12576ea05c82f3a62
# Parent  d1d5a0acbf7249ff33a488ce5b26cc3cb9b4802d
(partial) equivalecne relations. classes er<per

diff -r d1d5a0acbf72 -r fc10751254aa src/HOL/Quot/PER.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Quot/PER.ML	Fri Apr 04 16:01:14 1997 +0200
@@ -0,0 +1,19 @@
+(*  Title:      HOL/Quot/PER.ML
+    ID:         $Id$
+    Author:     Oscar Slotosch
+    Copyright   1997 Technische Universitaet Muenchen
+
+*)
+open PER;
+
+goalw thy [fun_per_def,per_def] "f===g=(!x y.x:D&y:D&x===y-->f x===g y)";
+br refl 1;
+qed "inst_fun_per";
+
+(* Witness that quot is not empty *)
+goal thy "?z:{s.? r.!y.y:s=y===r}";
+fr CollectI;
+by (res_inst_tac [("x","x")] exI 1);
+br allI 1;
+br mem_Collect_eq 1;
+qed "quotNE";
diff -r d1d5a0acbf72 -r fc10751254aa src/HOL/Quot/PER.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Quot/PER.thy	Fri Apr 04 16:01:14 1997 +0200
@@ -0,0 +1,20 @@
+(*  Title:      HOL/Quot/PER.thy
+    ID:         $Id$
+    Author:     Oscar Slotosch
+    Copyright   1997 Technische Universitaet Muenchen
+
+instances for per - makes PER higher order
+*)
+
+PER = PER0 +  (* instance for per *)
+
+(* does not work 
+instance fun  :: (per,per)per (per_sym_fun,per_trans_fun)
+
+needss explicite proofs:
+*)
+
+instance fun  :: (per,per)per   
+{| (etac per_sym_fun 1) THEN (etac per_trans_fun 1) THEN (atac 1) |}
+
+end
diff -r d1d5a0acbf72 -r fc10751254aa src/HOL/Quot/PER0.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Quot/PER0.ML	Fri Apr 04 16:01:14 1997 +0200
@@ -0,0 +1,115 @@
+(*  Title:      HOL/Quot/PER0.ML
+    ID:         $Id$
+    Author:     Oscar Slotosch
+    Copyright   1997 Technische Universitaet Muenchen
+
+*)
+open PER0;
+
+(* derive the characteristic axioms *)
+val prems = goalw thy [per_def] "x === y ==> y === x";
+by (cut_facts_tac prems 1);
+be ax_per_sym 1;
+qed "per_sym";
+
+val prems = goalw thy [per_def] "[| x === y; y === z |] ==> x === z";
+by (cut_facts_tac prems 1);
+be ax_per_trans 1;
+ba 1;
+qed "per_trans";
+
+goalw thy [per_def] "(x::'a::er) === x";
+br ax_er_refl 1;
+qed "er_refl";
+
+(* now everything works without axclasses *)
+
+goal thy "x===y=y===x";
+br iffI 1;
+be per_sym 1;
+be per_sym 1;
+qed "per_sym2";
+
+val prems = goal  thy "x===y ==> x===x";
+by (cut_facts_tac prems 1);
+br per_trans 1;ba 1;
+be per_sym 1;
+qed "sym2refl1";
+
+val prems = goal  thy "x===y ==> y===y";
+by (cut_facts_tac prems 1);
+br per_trans 1;ba 2;
+be per_sym 1;
+qed "sym2refl2";
+
+val prems = goalw thy [Domain] "x:D ==> x === x";
+by (cut_facts_tac prems 1);
+by (fast_tac set_cs 1);
+qed "DomainD";
+
+val prems = goalw thy [Domain] "x === x ==> x:D";
+by (cut_facts_tac prems 1);
+by (fast_tac set_cs 1);
+qed "DomainI";
+
+goal thy "x:D = x===x";
+br iffI 1;
+be DomainD 1;
+be DomainI 1;
+qed "DomainEq";
+
+goal thy "(~ x === y) = (~ y === x)";
+br (per_sym2 RS arg_cong) 1;
+qed "per_not_sym";
+
+(* show that PER work only on D *)
+val prems = goal thy "x===y ==> x:D";
+by (cut_facts_tac prems 1);
+be (sym2refl1 RS DomainI) 1;
+qed "DomainI_left"; 
+
+val prems = goal thy "x===y ==> y:D";
+by (cut_facts_tac prems 1);
+be (sym2refl2 RS DomainI) 1;
+qed "DomainI_right"; 
+
+val prems = goalw thy [Domain] "x~:D ==> ~x===y";
+by (cut_facts_tac prems 1);
+by (res_inst_tac [("Q","x===y")] (excluded_middle RS disjE) 1);ba 1;
+bd sym2refl1 1;
+by (fast_tac set_cs 1);
+qed "notDomainE1"; 
+
+val prems = goalw thy [Domain] "x~:D ==> ~y===x";
+by (cut_facts_tac prems 1);
+by (res_inst_tac [("Q","y===x")] (excluded_middle RS disjE) 1);ba 1;
+bd sym2refl2 1;
+by (fast_tac set_cs 1);
+qed "notDomainE2"; 
+
+(* theorems for equivalence relations *)
+goal thy "(x::'a::er) : D";
+br DomainI 1;
+br er_refl 1;
+qed "er_Domain";
+
+(* witnesses for "=>" ::(per,per)per  *)
+val prems = goalw thy [fun_per_def]"eqv (x::'a::per => 'b::per) y ==> eqv y x";
+by (cut_facts_tac prems 1);
+by (safe_tac HOL_cs);
+by (asm_full_simp_tac (HOL_ss addsimps [per_sym2]) 1);
+qed "per_sym_fun";
+
+val prems = goalw thy [fun_per_def]
+	"[| eqv (f::'a::per=>'b::per) g;eqv g h|] ==> eqv f h";
+by (cut_facts_tac prems 1);
+by (safe_tac HOL_cs);
+by (REPEAT (dtac spec 1));
+by (res_inst_tac [("y","g y")] per_trans 1);
+br mp 1;ba 1;
+by (Asm_simp_tac 1);
+br mp 1;ba 1;
+by (asm_simp_tac (!simpset addsimps [sym2refl2]) 1);
+qed "per_trans_fun";
+
+
diff -r d1d5a0acbf72 -r fc10751254aa src/HOL/Quot/PER0.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Quot/PER0.thy	Fri Apr 04 16:01:14 1997 +0200
@@ -0,0 +1,37 @@
+(*  Title:      HOL/Quot/PER0.thy
+    ID:         $Id$
+    Author:     Oscar Slotosch
+    Copyright   1997 Technische Universitaet Muenchen
+
+Definition of classes per and er for (partial) equivalence classes
+The polymorphic constant eqv is only for the definition of PERs
+The characteristic constant === (sim) is available on the class per
+
+*)
+
+PER0 = Set + (* partial equivalence relations *)
+
+consts  (* polymorphic constant for (partial) equivalence relations *)
+        eqv    :: "'a::term => 'a => bool" 
+
+axclass per < term
+	(* axioms for partial equivalence relations *)
+        ax_per_sym      "eqv x y ==> eqv y x"
+        ax_per_trans    "[|eqv x y; eqv y z|] ==> eqv x z"
+
+axclass er < per
+	ax_er_refl	"eqv x x"
+
+consts  (* characteristic constant and Domain for per *)
+        "==="     :: "'a::per => 'a => bool" (infixl 55)
+        D         :: "'a::per set"
+defs
+        per_def         "(op ===) == eqv"
+        Domain          "D=={x.x===x}"
+(* define ==== on and function type => *)
+        fun_per_def     "eqv f g == !x y.x:D & y:D & x===y --> f x === g y"
+
+syntax (symbols)
+  "op ==="   :: "['a,'a::per] => bool"        (infixl "\\<sim>" 50)
+
+end