(higher-order) quotient constructor quot, based on PER
authorslotosch
Fri Apr 04 16:02:12 1997 +0200 (1997-04-04)
changeset 29059a4f353107da
parent 2904 fc10751254aa
child 2906 171dedbc9bdb
(higher-order) quotient constructor quot, based on PER
src/HOL/Quot/HQUOT.ML
src/HOL/Quot/HQUOT.thy
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Quot/HQUOT.ML	Fri Apr 04 16:02:12 1997 +0200
     1.3 @@ -0,0 +1,171 @@
     1.4 +(*  Title:      HOL/Quot/HQUOT.ML
     1.5 +    ID:         $Id$
     1.6 +    Author:     Oscar Slotosch
     1.7 +    Copyright   1997 Technische Universitaet Muenchen
     1.8 +
     1.9 +*)
    1.10 +open HQUOT;
    1.11 +
    1.12 +(* first prove some helpful lemmas *)
    1.13 +goalw thy [quot_def] "{y.y===x}:quot";
    1.14 +by (Asm_simp_tac 1);
    1.15 +by (fast_tac (set_cs addIs [per_sym]) 1);
    1.16 +qed "per_class_rep_quot";
    1.17 +
    1.18 +val prems = goal thy "Rep_quot a = Rep_quot b ==> a=b";
    1.19 +by (cut_facts_tac prems 1);
    1.20 +br (Rep_quot_inverse RS subst) 1;
    1.21 +by (res_inst_tac [("t","a")] (Rep_quot_inverse RS subst) 1);
    1.22 +by (Asm_simp_tac 1);
    1.23 +qed "quot_eq";
    1.24 +
    1.25 +(* prepare induction and exhaustiveness *)
    1.26 +val prems = goal thy "!s.s:quot --> P (Abs_quot s) ==> P x";
    1.27 +by (cut_facts_tac prems 1);
    1.28 +br (Abs_quot_inverse RS subst) 1;
    1.29 +br Rep_quot 1;
    1.30 +by (dres_inst_tac [("x","Rep_quot x")] spec 1);
    1.31 +by (asm_full_simp_tac (HOL_ss addsimps [Rep_quot,Rep_quot_inverse]) 1);
    1.32 +qed "all_q";
    1.33 +
    1.34 +goal thy "? s.s:quot & x=Abs_quot s";
    1.35 +by (res_inst_tac [("x","Rep_quot x")] exI 1);
    1.36 +by (asm_full_simp_tac (HOL_ss addsimps [Rep_quot,Rep_quot_inverse]) 1);
    1.37 +qed "exh_q";
    1.38 +
    1.39 +(* some lemmas for the equivalence classes *)
    1.40 +
    1.41 +(* equality and symmetry for equivalence classes *)
    1.42 +val prems = goalw thy [peclass_def] "x===y==><[x]>=<[y]>";
    1.43 +by (cut_facts_tac prems 1);
    1.44 +by (res_inst_tac [("f","Abs_quot")] arg_cong 1);
    1.45 +br Collect_cong 1;
    1.46 +br iffI 1;
    1.47 +be per_trans 1;ba 1;
    1.48 +be per_trans 1;
    1.49 +be per_sym 1;
    1.50 +qed "per_class_eqI";
    1.51 +
    1.52 +val prems = goalw thy [peclass_def] "<[(x::'a::er)]>=<[y]>==>x===y";
    1.53 +by (cut_facts_tac prems 1);
    1.54 +by (dres_inst_tac [("f","Rep_quot")] arg_cong 1);
    1.55 +by (asm_full_simp_tac(HOL_ss addsimps [Abs_quot_inverse,per_class_rep_quot])1);
    1.56 +by (dres_inst_tac [("c","x")] equalityCE 1);ba 3;
    1.57 +by (safe_tac set_cs);
    1.58 +by (fast_tac (set_cs addIs [er_refl]) 1);
    1.59 +qed "er_class_eqE";
    1.60 +
    1.61 +val prems = goalw thy [peclass_def] "[|x:D;<[x]>=<[y]>|]==>x===y";
    1.62 +by (cut_facts_tac prems 1);
    1.63 +bd DomainD 1;
    1.64 +by (dres_inst_tac [("f","Rep_quot")] arg_cong 1);
    1.65 +by (asm_full_simp_tac(HOL_ss addsimps [Abs_quot_inverse,per_class_rep_quot])1);
    1.66 +by (dres_inst_tac [("c","x")] equalityCE 1);ba 3;
    1.67 +by (safe_tac set_cs);
    1.68 +qed "per_class_eqE";
    1.69 +
    1.70 +goal thy "<[(x::'a::er)]>=<[y]>=x===y";
    1.71 +br iffI 1;
    1.72 +be er_class_eqE 1;
    1.73 +be per_class_eqI 1;
    1.74 +qed "er_class_eq";
    1.75 +
    1.76 +val prems = goal thy "x:D==><[x]>=<[y]>=x===y";
    1.77 +by (cut_facts_tac prems 1);
    1.78 +br iffI 1;
    1.79 +be per_class_eqE 1;ba 1;
    1.80 +be per_class_eqI 1;
    1.81 +qed "per_class_eq";
    1.82 +
    1.83 +(* inequality *)
    1.84 +val prems = goal thy "[|x:D;~x===y|]==><[x]>~=<[y]>";
    1.85 +by (cut_facts_tac prems 1);
    1.86 +br notI 1;
    1.87 +bd per_class_eqE 1;
    1.88 +auto();
    1.89 +qed "per_class_neqI";
    1.90 +
    1.91 +val prems = goal thy "~(x::'a::er)===y==><[x]>~=<[y]>";
    1.92 +by (cut_facts_tac prems 1);
    1.93 +br notI 1;
    1.94 +bd er_class_eqE 1;
    1.95 +auto();
    1.96 +qed "er_class_neqI";
    1.97 +
    1.98 +val prems = goal thy "<[x]>~=<[y]>==>~x===y";
    1.99 +by (cut_facts_tac prems 1);
   1.100 +br notI 1;
   1.101 +be notE 1;
   1.102 +be per_class_eqI 1;
   1.103 +qed "per_class_neqE";
   1.104 +
   1.105 +val prems = goal thy "x:D==><[x]>~=<[y]>=(~x===y)";
   1.106 +by (cut_facts_tac prems 1);
   1.107 +br iffI 1;
   1.108 +be per_class_neqE 1;
   1.109 +be per_class_neqI 1;ba 1;
   1.110 +qed "per_class_not";
   1.111 +
   1.112 +goal thy "<[(x::'a::er)]>~=<[y]>=(~x===y)";
   1.113 +br iffI 1;
   1.114 +be per_class_neqE 1;
   1.115 +be er_class_neqI 1;
   1.116 +qed "er_class_not";
   1.117 +
   1.118 +(* exhaustiveness and induction *)
   1.119 +goalw thy [peclass_def] "? s.x=<[s]>";
   1.120 +br all_q 1;
   1.121 +by (strip_tac 1);
   1.122 +by (asm_full_simp_tac (HOL_ss addsimps [mem_Collect_eq,quot_def]) 1);
   1.123 +be exE 1;
   1.124 +by (res_inst_tac [("x","r")] exI 1);
   1.125 +br quot_eq 1;
   1.126 +by (subgoal_tac "s:quot" 1);
   1.127 +by (asm_simp_tac(HOL_ss addsimps [Abs_quot_inverse,per_class_rep_quot])1);
   1.128 +br set_ext 1;
   1.129 +by (fast_tac set_cs 1);
   1.130 +by (asm_full_simp_tac (HOL_ss addsimps [mem_Collect_eq,quot_def]) 1);
   1.131 +by (fast_tac set_cs 1);
   1.132 +qed "per_class_exh";
   1.133 +
   1.134 +val prems = goal thy "!x.P<[x]> ==> P s";
   1.135 +by (cut_facts_tac (prems@[
   1.136 +	read_instantiate[("x","s::'a::per quot")] per_class_exh]) 1);
   1.137 +by (fast_tac set_cs 1);
   1.138 +qed "per_class_all";
   1.139 +
   1.140 +(* theorems for any_in *)
   1.141 +goalw thy [any_in_def,peclass_def] "any_in<[(s::'a::er)]>===s";
   1.142 +fr selectI2;
   1.143 +fr refl;
   1.144 +by (fold_goals_tac [peclass_def]);
   1.145 +fe er_class_eqE;
   1.146 +qed "er_any_in_class";
   1.147 +
   1.148 +val prems = goalw thy [any_in_def,peclass_def] "s:D==>any_in<[s]>===s";
   1.149 +by (cut_facts_tac prems 1);
   1.150 +fr selectI2;
   1.151 +fr refl;
   1.152 +by (fold_goals_tac [peclass_def]);
   1.153 +fr per_sym;
   1.154 +fe per_class_eqE;
   1.155 +fe sym;
   1.156 +qed "per_any_in_class";
   1.157 +
   1.158 +val prems = goal thy "<[any_in (s::'a::er quot)]> = s";
   1.159 +by (cut_facts_tac prems 1);
   1.160 +fr per_class_all;
   1.161 +fr allI;
   1.162 +fr (er_any_in_class RS per_class_eqI);
   1.163 +qed "er_class_any_in";
   1.164 +
   1.165 +(* equivalent theorem for per would need !x.x:D *)
   1.166 +val prems = goal thy "!x::'a::per.x:D==><[any_in (q::'a::per quot)]> = q";
   1.167 +by (cut_facts_tac prems 1);
   1.168 +fr per_class_all;
   1.169 +fr allI;
   1.170 +fr (per_any_in_class RS per_class_eqI);
   1.171 +fe spec;
   1.172 +qed "per_class_any_in";
   1.173 +
   1.174 +(* is like theorem for class er *)
   1.175 \ No newline at end of file
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/HOL/Quot/HQUOT.thy	Fri Apr 04 16:02:12 1997 +0200
     2.3 @@ -0,0 +1,27 @@
     2.4 +(*  Title:      HOL/Quot/HQUOT.thy
     2.5 +    ID:         $Id$
     2.6 +    Author:     Oscar Slotosch
     2.7 +    Copyright   1997 Technische Universitaet Muenchen
     2.8 +
     2.9 +quotient constructor for higher order quotients
    2.10 +
    2.11 +*)
    2.12 +
    2.13 +HQUOT = PER +      
    2.14 +
    2.15 +typedef 'a quot = "{s::'a::per set. ? r.!y.y:s=y===r}" (quotNE)
    2.16 +
    2.17 +(* constants for equivalence classes *)
    2.18 +consts
    2.19 +        peclass         :: "'a::per => 'a quot"
    2.20 +        any_in          :: "'a::per quot => 'a"
    2.21 +
    2.22 +syntax          "@ecl"  :: "'a::per => 'a quot" ("<[ _ ]>")
    2.23 +
    2.24 +translations    "<[x]>" == "peclass x"
    2.25 +
    2.26 +defs
    2.27 +        peclass_def     "<[x]> == Abs_quot {y.y===x}"
    2.28 +        any_in_def      "any_in f == @x.<[x]>=f"
    2.29 +end
    2.30 +