Example for higher order quotients: Fractionals
authorslotosch
Fri Apr 04 16:03:11 1997 +0200 (1997-04-04)
changeset 2906171dedbc9bdb
parent 2905 9a4f353107da
child 2907 0e272e4c7cb2
Example for higher order quotients: Fractionals
src/HOL/Quot/FRACT.ML
src/HOL/Quot/FRACT.thy
src/HOL/Quot/NPAIR.ML
src/HOL/Quot/NPAIR.thy
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Quot/FRACT.ML	Fri Apr 04 16:03:11 1997 +0200
     1.3 @@ -0,0 +1,18 @@
     1.4 +(*  Title:      HOL/Quot/FRACT.ML
     1.5 +    ID:         $Id$
     1.6 +    Author:     Oscar Slotosch
     1.7 +    Copyright   1997 Technische Universitaet Muenchen
     1.8 +
     1.9 +*)
    1.10 +open FRACT;
    1.11 +
    1.12 +goalw thy [per_def,per_NP_def]
    1.13 +"(op ===)=(%x y.fst(rep_NP x)*snd(rep_NP y)=fst(rep_NP y)*snd(rep_NP x))";
    1.14 +fr refl;
    1.15 +qed "inst_NP_per";
    1.16 +
    1.17 +
    1.18 +goalw thy [half_def] "half = <[abs_NP(n,2*n)]>";
    1.19 +fr per_class_eqI;
    1.20 +by (simp_tac (!simpset addsimps [inst_NP_per]) 1);
    1.21 +qed "test";
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/HOL/Quot/FRACT.thy	Fri Apr 04 16:03:11 1997 +0200
     2.3 @@ -0,0 +1,23 @@
     2.4 +(*  Title:      HOL/Quot/FRACT.thy
     2.5 +    ID:         $Id$
     2.6 +    Author:     Oscar Slotosch
     2.7 +    Copyright   1997 Technische Universitaet Muenchen
     2.8 +
     2.9 +Example for higher order quotients: fractionals
    2.10 +*)
    2.11 +
    2.12 +FRACT = NPAIR + HQUOT +
    2.13 +instance 
    2.14 +	NP::per	
    2.15 +	{| (etac per_sym_NP 1) THEN (etac per_trans_NP 1) THEN (atac 1) |}
    2.16 +
    2.17 +(* now define fractions *)
    2.18 +
    2.19 +types fract = NP quot
    2.20 +
    2.21 +(* example for fractions *)
    2.22 +consts 
    2.23 +	half ::	"fract"
    2.24 +
    2.25 +defs    half_def    "half == <[abs_NP(1,2)]>"
    2.26 +end
    2.27 \ No newline at end of file
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/HOL/Quot/NPAIR.ML	Fri Apr 04 16:03:11 1997 +0200
     3.3 @@ -0,0 +1,19 @@
     3.4 +(*  Title:      HOL/Quot/NPAIR.ML
     3.5 +    ID:         $Id$
     3.6 +    Author:     Oscar Slotosch
     3.7 +    Copyright   1997 Technische Universitaet Muenchen
     3.8 +
     3.9 +*)
    3.10 +open NPAIR;
    3.11 +
    3.12 +goalw thy [rep_NP_def] "rep_NP(abs_NP np) = np";
    3.13 +auto();
    3.14 +qed "rep_abs_NP";
    3.15 +
    3.16 +Addsimps [rep_abs_NP];
    3.17 +
    3.18 +val prems = goalw thy [per_NP_def] "eqv (x::NP) y ==> eqv y x";
    3.19 +by (cut_facts_tac prems 1);
    3.20 +auto();
    3.21 +qed "per_sym_NP";
    3.22 +
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/HOL/Quot/NPAIR.thy	Fri Apr 04 16:03:11 1997 +0200
     4.3 @@ -0,0 +1,26 @@
     4.4 +(*  Title:      HOL/Quot/NPAIR.thy
     4.5 +    ID:         $Id$
     4.6 +    Author:     Oscar Slotosch
     4.7 +    Copyright   1997 Technische Universitaet Muenchen
     4.8 +
     4.9 +Example: define a PER on pairs of natural numbers (with embedding)
    4.10 +
    4.11 +*)
    4.12 +NPAIR = Arith + Prod + PER +  (* representation for rational numbers *)
    4.13 +
    4.14 +types np = "(nat * nat)" (* is needed for datatype *)
    4.15 +
    4.16 +datatype NP = abs_NP np
    4.17 +
    4.18 +consts	rep_NP :: "NP => nat * nat"
    4.19 +
    4.20 +defs    rep_NP_def "rep_NP x == (case x of abs_NP y => y)"
    4.21 +
    4.22 +(* NPAIR (continued) *)
    4.23 +defs	per_NP_def 
    4.24 +  "eqv ==(%x y.fst(rep_NP x)*snd(rep_NP y)=fst(rep_NP y)*snd(rep_NP x))"
    4.25 +
    4.26 +(* for proves of this rule see [Slo97diss] *)
    4.27 +rules
    4.28 +	per_trans_NP	"[| eqv (x::NP) y;eqv y z |] ==> eqv x z"
    4.29 +end
    4.30 \ No newline at end of file