# HG changeset patch # User nipkow # Date 965039606 -7200 # Node ID d7e354c16dc6bd89f9e577acea8643f325a2146b # Parent 9506127f6fbba1405a8ec9abd6acba4dea9f549f Never used and not relevant. diff -r 9506127f6fbb -r d7e354c16dc6 src/HOL/Quot/FRACT.ML --- a/src/HOL/Quot/FRACT.ML Sun Jul 30 13:06:20 2000 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,17 +0,0 @@ -(* Title: HOL/Quot/FRACT.ML - ID: $Id$ - Author: Oscar Slotosch - Copyright 1997 Technische Universitaet Muenchen - -*) - -Goalw [per_def,per_NP_def] -"(op ===)=(%x y. fst(rep_NP x)*snd(rep_NP y)=fst(rep_NP y)*snd(rep_NP x))"; -by (rtac refl 1); -qed "inst_NP_per"; - - -Goalw [half_def] "half = <[abs_NP(n,#2*n)]>"; -by (rtac per_class_eqI 1); -by (simp_tac (simpset() addsimps [inst_NP_per]) 1); -qed "test"; diff -r 9506127f6fbb -r d7e354c16dc6 src/HOL/Quot/FRACT.thy --- a/src/HOL/Quot/FRACT.thy Sun Jul 30 13:06:20 2000 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,23 +0,0 @@ -(* Title: HOL/Quot/FRACT.thy - ID: $Id$ - Author: Oscar Slotosch - Copyright 1997 Technische Universitaet Muenchen - -Example for higher order quotients: fractions -*) - -FRACT = NPAIR + HQUOT + -instance - NP::per - {| (etac per_trans_NP 1) THEN (atac 1) THEN (etac per_sym_NP 1) |} - -(* now define fractions *) - -types fract = NP quot - -(* example for fractions *) -consts - half :: "fract" - -defs half_def "half == <[abs_NP(1,2)]>" -end diff -r 9506127f6fbb -r d7e354c16dc6 src/HOL/Quot/HQUOT.ML --- a/src/HOL/Quot/HQUOT.ML Sun Jul 30 13:06:20 2000 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,156 +0,0 @@ -(* Title: HOL/Quot/HQUOT.ML - ID: $Id$ - Author: Oscar Slotosch - Copyright 1997 Technische Universitaet Muenchen - -*) - -(* first prove some helpful lemmas *) -Goalw [quot_def] "{y. y===x}:quot"; -by (Asm_simp_tac 1); -by (blast_tac (claset() addIs [per_sym]) 1); -qed "per_class_rep_quot"; - -Goal "Rep_quot a = Rep_quot b ==> a=b"; -by (rtac (Rep_quot_inverse RS subst) 1); -by (res_inst_tac [("t","a")] (Rep_quot_inverse RS subst) 1); -by (Asm_simp_tac 1); -qed "quot_eq"; - -(* prepare induction and exhaustiveness *) -Goal "!s. s:quot --> P (Abs_quot s) ==> P x"; -by (rtac (Abs_quot_inverse RS subst) 1); -by (rtac Rep_quot 1); -by (dres_inst_tac [("x","Rep_quot x")] spec 1); -by (asm_full_simp_tac (HOL_ss addsimps [Rep_quot,Rep_quot_inverse]) 1); -qed "all_q"; - -Goal "? s. s:quot & x=Abs_quot s"; -by (res_inst_tac [("x","Rep_quot x")] exI 1); -by (asm_full_simp_tac (HOL_ss addsimps [Rep_quot,Rep_quot_inverse]) 1); -qed "exh_q"; - -(* some lemmas for the equivalence classes *) - -(* equality and symmetry for equivalence classes *) -Goalw [peclass_def] "x===y==><[x]>=<[y]>"; -by (res_inst_tac [("f","Abs_quot")] arg_cong 1); -by (rtac Collect_cong 1); -by (rtac iffI 1); -by (etac per_trans 1);by (assume_tac 1); -by (etac per_trans 1); -by (etac per_sym 1); -qed "per_class_eqI"; - -Goalw [peclass_def] "<[(x::'a::er)]>=<[y]>==>x===y"; -by (dres_inst_tac [("f","Rep_quot")] arg_cong 1); -by (asm_full_simp_tac(HOL_ss addsimps [Abs_quot_inverse,per_class_rep_quot])1); -by (dres_inst_tac [("c","x")] equalityCE 1);by (assume_tac 3); -by Safe_tac; -by (blast_tac (claset() addIs [er_refl]) 1); -qed "er_class_eqE"; - -Goalw [peclass_def] "[|x:D;<[x]>=<[y]>|]==>x===y"; -by (dtac DomainD 1); -by (dres_inst_tac [("f","Rep_quot")] arg_cong 1); -by (asm_full_simp_tac(HOL_ss addsimps [Abs_quot_inverse,per_class_rep_quot])1); -by (dres_inst_tac [("c","x")] equalityCE 1);by (assume_tac 3); -by Auto_tac; -qed "per_class_eqE"; - -Goal "<[(x::'a::er)]>=<[y]>=x===y"; -by (rtac iffI 1); -by (etac er_class_eqE 1); -by (etac per_class_eqI 1); -qed "er_class_eq"; - -Goal "x:D==><[x]>=<[y]>=x===y"; -by (rtac iffI 1); -by (etac per_class_eqE 1);by (assume_tac 1); -by (etac per_class_eqI 1); -qed "per_class_eq"; - -(* inequality *) -Goal "[|x:D;~x===y|]==><[x]>~=<[y]>"; -by (rtac notI 1); -by (dtac per_class_eqE 1); -by Auto_tac; -qed "per_class_neqI"; - -Goal "~(x::'a::er)===y==><[x]>~=<[y]>"; -by (rtac notI 1); -by (dtac er_class_eqE 1); -by Auto_tac; -qed "er_class_neqI"; - -Goal "<[x]>~=<[y]>==>~x===y"; -by (rtac notI 1); -by (etac notE 1); -by (etac per_class_eqI 1); -qed "per_class_neqE"; - -Goal "x:D==><[x]>~=<[y]>=(~x===y)"; -by (rtac iffI 1); -by (etac per_class_neqE 1); -by (etac per_class_neqI 1);by (assume_tac 1); -qed "per_class_not"; - -Goal "<[(x::'a::er)]>~=<[y]>=(~x===y)"; -by (rtac iffI 1); -by (etac per_class_neqE 1); -by (etac er_class_neqI 1); -qed "er_class_not"; - -(* exhaustiveness and induction *) -Goalw [peclass_def] "? s. x=<[s]>"; -by (rtac all_q 1); -by (strip_tac 1); -by (asm_full_simp_tac (HOL_ss addsimps [mem_Collect_eq,quot_def]) 1); -by (etac exE 1); -by (res_inst_tac [("x","r")] exI 1); -by (rtac quot_eq 1); -by (subgoal_tac "s:quot" 1); -by (asm_simp_tac(HOL_ss addsimps [Abs_quot_inverse,per_class_rep_quot])1); -by (rtac set_ext 1); -by (Blast_tac 1); -by (asm_full_simp_tac (HOL_ss addsimps [mem_Collect_eq,quot_def]) 1); -by (Blast_tac 1); -qed "per_class_exh"; - -Goal "!x. P<[x]> ==> P s"; -by (cut_facts_tac [read_instantiate[("x","s::'a::per quot")] per_class_exh] 1); -by (Blast_tac 1); -qed "per_class_all"; - -(* theorems for any_in *) -Goalw [any_in_def,peclass_def] "any_in<[(s::'a::er)]>===s"; -by (rtac selectI2 1); -by (rtac refl 1); -by (fold_goals_tac [peclass_def]); -by (etac er_class_eqE 1); -qed "er_any_in_class"; - -Goalw [any_in_def,peclass_def] "s:D==>any_in<[s]>===s"; -by (rtac selectI2 1); -by (rtac refl 1); -by (fold_goals_tac [peclass_def]); -by (rtac per_sym 1); -by (etac per_class_eqE 1); -by (etac sym 1); -qed "per_any_in_class"; - -Goal "<[any_in (s::'a::er quot)]> = s"; -by (rtac per_class_all 1); -by (rtac allI 1); -by (rtac (er_any_in_class RS per_class_eqI) 1); -qed "er_class_any_in"; - -(* equivalent theorem for per would need !x.x:D *) -Goal "!x::'a::per. x:D==><[any_in (q::'a::per quot)]> = q"; -by (rtac per_class_all 1); -by (rtac allI 1); -by (rtac (per_any_in_class RS per_class_eqI) 1); -by (etac spec 1); -qed "per_class_any_in"; - -(* is like theorem for class er *) diff -r 9506127f6fbb -r d7e354c16dc6 src/HOL/Quot/HQUOT.thy --- a/src/HOL/Quot/HQUOT.thy Sun Jul 30 13:06:20 2000 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,27 +0,0 @@ -(* Title: HOL/Quot/HQUOT.thy - ID: $Id$ - Author: Oscar Slotosch - Copyright 1997 Technische Universitaet Muenchen - -quotient constructor for higher order quotients - -*) - -HQUOT = PER + - -typedef 'a quot = "{s::'a::per set. ? r.!y. y:s=y===r}" (quotNE) - -(* constants for equivalence classes *) -consts - peclass :: "'a::per => 'a quot" - any_in :: "'a::per quot => 'a" - -syntax "@ecl" :: "'a::per => 'a quot" ("<[ _ ]>") - -translations "<[x]>" == "peclass x" - -defs - peclass_def "<[x]> == Abs_quot {y. y===x}" - any_in_def "any_in f == @x.<[x]>=f" -end - diff -r 9506127f6fbb -r d7e354c16dc6 src/HOL/Quot/NPAIR.ML --- a/src/HOL/Quot/NPAIR.ML Sun Jul 30 13:06:20 2000 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,18 +0,0 @@ -(* Title: HOL/Quot/NPAIR.ML - ID: $Id$ - Author: Oscar Slotosch - Copyright 1997 Technische Universitaet Muenchen - -*) -open NPAIR; - -Goalw [rep_NP_def] "rep_NP(abs_NP np) = np"; -by Auto_tac; -qed "rep_abs_NP"; - -Addsimps [rep_abs_NP]; - -Goalw [per_NP_def] "eqv (x::NP) y ==> eqv y x"; -by Auto_tac; -qed "per_sym_NP"; - diff -r 9506127f6fbb -r d7e354c16dc6 src/HOL/Quot/NPAIR.thy --- a/src/HOL/Quot/NPAIR.thy Sun Jul 30 13:06:20 2000 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,24 +0,0 @@ -(* 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 = PER + Main + (* representation for rational numbers *) - -datatype NP = abs_NP "(nat * nat)" - -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 diff -r 9506127f6fbb -r d7e354c16dc6 src/HOL/Quot/PER.ML --- a/src/HOL/Quot/PER.ML Sun Jul 30 13:06:20 2000 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,19 +0,0 @@ -(* Title: HOL/Quot/PER.ML - ID: $Id$ - Author: Oscar Slotosch - Copyright 1997 Technische Universitaet Muenchen - -*) -open PER; - -Goalw [fun_per_def,per_def] "f===g=(!x y. x:D&y:D&x===y-->f x===g y)"; -by (rtac refl 1); -qed "inst_fun_per"; - -(* Witness that quot is not empty *) -Goal "?z:{s.? r.!y. y:s=y===r}"; -by (rtac CollectI 1); -by (res_inst_tac [("x","x")] exI 1); -by (rtac allI 1); -by (rtac mem_Collect_eq 1); -qed "quotNE"; diff -r 9506127f6fbb -r d7e354c16dc6 src/HOL/Quot/PER.thy --- a/src/HOL/Quot/PER.thy Sun Jul 30 13:06:20 2000 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,14 +0,0 @@ -(* 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 *) - -instance fun :: (per,per)per -{| (etac per_trans_fun 1) THEN (atac 1) THEN (etac per_sym_fun 1) |} - -end diff -r 9506127f6fbb -r d7e354c16dc6 src/HOL/Quot/PER0.ML --- a/src/HOL/Quot/PER0.ML Sun Jul 30 13:06:20 2000 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,103 +0,0 @@ -(* Title: HOL/Quot/PER0.ML - ID: $Id$ - Author: Oscar Slotosch - Copyright 1997 Technische Universitaet Muenchen - -*) -open PER0; - -(* derive the characteristic axioms *) -Goalw [per_def] "x === y ==> y === x"; -by (etac ax_per_sym 1); -qed "per_sym"; - -Goalw [per_def] "[| x === y; y === z |] ==> x === z"; -by (etac ax_per_trans 1); -by (assume_tac 1); -qed "per_trans"; - -Goalw [per_def] "(x::'a::er) === x"; -by (rtac ax_er_refl 1); -qed "er_refl"; - -(* now everything works without axclasses *) - -Goal "x===y=y===x"; -by (rtac iffI 1); -by (etac per_sym 1); -by (etac per_sym 1); -qed "per_sym2"; - -Goal "x===y ==> x===x"; -by (rtac per_trans 1);by (assume_tac 1); -by (etac per_sym 1); -qed "sym2refl1"; - -Goal "x===y ==> y===y"; -by (rtac per_trans 1);by (assume_tac 2); -by (etac per_sym 1); -qed "sym2refl2"; - -Goalw [Dom] "x:D ==> x === x"; -by (Blast_tac 1); -qed "DomainD"; - -Goalw [Dom] "x === x ==> x:D"; -by (Blast_tac 1); -qed "DomainI"; - -Goal "x:D = x===x"; -by (rtac iffI 1); -by (etac DomainD 1); -by (etac DomainI 1); -qed "DomainEq"; - -Goal "(~ x === y) = (~ y === x)"; -by (rtac (per_sym2 RS arg_cong) 1); -qed "per_not_sym"; - -(* show that PER work only on D *) -Goal "x===y ==> x:D"; -by (etac (sym2refl1 RS DomainI) 1); -qed "DomainI_left"; - -Goal "x===y ==> y:D"; -by (etac (sym2refl2 RS DomainI) 1); -qed "DomainI_right"; - -Goalw [Dom] "x~:D ==> ~x===y"; -by (res_inst_tac [("Q","x===y")] (excluded_middle RS disjE) 1); -by (assume_tac 1); -by (dtac sym2refl1 1); -by (Blast_tac 1); -qed "notDomainE1"; - -Goalw [Dom] "x~:D ==> ~y===x"; -by (res_inst_tac [("Q","y===x")] (excluded_middle RS disjE) 1); -by (assume_tac 1); -by (dtac sym2refl2 1); -by (Blast_tac 1); -qed "notDomainE2"; - -(* theorems for equivalence relations *) -Goal "(x::'a::er) : D"; -by (rtac DomainI 1); -by (rtac er_refl 1); -qed "er_Domain"; - -(* witnesses for "=>" ::(per,per)per *) -Goalw [fun_per_def]"eqv (x::'a::per => 'b::per) y ==> eqv y x"; -by (auto_tac (claset(), simpset() addsimps [per_sym2])); -qed "per_sym_fun"; - -Goalw [fun_per_def] "[| eqv (f::'a::per=>'b::per) g;eqv g h|] ==> eqv f h"; -by Safe_tac; -by (REPEAT (dtac spec 1)); -by (res_inst_tac [("y","g y")] per_trans 1); -by (rtac mp 1);by (assume_tac 1); -by (Asm_simp_tac 1); -by (rtac mp 1);by (assume_tac 1); -by (asm_simp_tac (simpset() addsimps [sym2refl2]) 1); -qed "per_trans_fun"; - - diff -r 9506127f6fbb -r d7e354c16dc6 src/HOL/Quot/PER0.thy --- a/src/HOL/Quot/PER0.thy Sun Jul 30 13:06:20 2000 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,37 +0,0 @@ -(* 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_trans "[|eqv x y; eqv y z|] ==> eqv x z" - ax_per_sym "eqv x y ==> eqv y x" - -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" - Dom "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 "\\" 50) - -end diff -r 9506127f6fbb -r d7e354c16dc6 src/HOL/Quot/README --- a/src/HOL/Quot/README Sun Jul 30 13:06:20 2000 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,14 +0,0 @@ -This directorty contains the higher order quotients in Isabelle HOL - -higher order quotients use partial equivalence relations/classes (PERs) -instead of euivalence relations/classes -We have two classes er