Example for higher order quotients: Fractionals

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Quot/FRACT.ML	Fri Apr 04 16:03:11 1997 +0200
@@ -0,0 +1,18 @@
+(*  Title:      HOL/Quot/FRACT.ML
+    ID:         $Id$
+    Author:     Oscar Slotosch
+    Copyright   1997 Technische Universitaet Muenchen
+
+*)
+open FRACT;
+
+goalw thy [per_def,per_NP_def]
+"(op ===)=(%x y.fst(rep_NP x)*snd(rep_NP y)=fst(rep_NP y)*snd(rep_NP x))";
+fr refl;
+qed "inst_NP_per";
+
+
+goalw thy [half_def] "half = <[abs_NP(n,2*n)]>";
+fr per_class_eqI;
+by (simp_tac (!simpset addsimps [inst_NP_per]) 1);
+qed "test";

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Quot/FRACT.thy	Fri Apr 04 16:03:11 1997 +0200
@@ -0,0 +1,23 @@
+(*  Title:      HOL/Quot/FRACT.thy
+    ID:         $Id$
+    Author:     Oscar Slotosch
+    Copyright   1997 Technische Universitaet Muenchen
+
+Example for higher order quotients: fractionals
+*)
+
+FRACT = NPAIR + HQUOT +
+instance 
+	NP::per	
+	{| (etac per_sym_NP 1) THEN (etac per_trans_NP 1) THEN (atac 1) |}
+
+(* now define fractions *)
+
+types fract = NP quot
+
+(* example for fractions *)
+consts 
+	half ::	"fract"
+
+defs    half_def    "half == <[abs_NP(1,2)]>"
+end
\ No newline at end of file

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Quot/NPAIR.ML	Fri Apr 04 16:03:11 1997 +0200
@@ -0,0 +1,19 @@
+(*  Title:      HOL/Quot/NPAIR.ML
+    ID:         $Id$
+    Author:     Oscar Slotosch
+    Copyright   1997 Technische Universitaet Muenchen
+
+*)
+open NPAIR;
+
+goalw thy [rep_NP_def] "rep_NP(abs_NP np) = np";
+auto();
+qed "rep_abs_NP";
+
+Addsimps [rep_abs_NP];
+
+val prems = goalw thy [per_NP_def] "eqv (x::NP) y ==> eqv y x";
+by (cut_facts_tac prems 1);
+auto();
+qed "per_sym_NP";
+

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Quot/NPAIR.thy	Fri Apr 04 16:03:11 1997 +0200
@@ -0,0 +1,26 @@
+(*  Title:      HOL/Quot/NPAIR.thy
+    ID:         $Id$
+    Author:     Oscar Slotosch
+    Copyright   1997 Technische Universitaet Muenchen
+
+Example: define a PER on pairs of natural numbers (with embedding)
+
+*)
+NPAIR = Arith + Prod + PER +  (* representation for rational numbers *)
+
+types np = "(nat * nat)" (* is needed for datatype *)
+
+datatype NP = abs_NP np
+
+consts	rep_NP :: "NP => nat * nat"
+
+defs    rep_NP_def "rep_NP x == (case x of abs_NP y => y)"
+
+(* NPAIR (continued) *)
+defs	per_NP_def 
+  "eqv ==(%x y.fst(rep_NP x)*snd(rep_NP y)=fst(rep_NP y)*snd(rep_NP x))"
+
+(* for proves of this rule see [Slo97diss] *)
+rules
+	per_trans_NP	"[| eqv (x::NP) y;eqv y z |] ==> eqv x z"
+end
\ No newline at end of file