author | paulson |
Fri, 13 Nov 1998 13:41:53 +0100 | |
changeset 5858 | beddc19c107a |
parent 5069 | 3ea049f7979d |
child 6162 | 484adda70b65 |
permissions | -rw-r--r-- |
2905
9a4f353107da
(higher-order) quotient constructor quot, based on PER
slotosch
parents:
diff
changeset
|
1 |
(* Title: HOL/Quot/HQUOT.ML |
9a4f353107da
(higher-order) quotient constructor quot, based on PER
slotosch
parents:
diff
changeset
|
2 |
ID: $Id$ |
9a4f353107da
(higher-order) quotient constructor quot, based on PER
slotosch
parents:
diff
changeset
|
3 |
Author: Oscar Slotosch |
9a4f353107da
(higher-order) quotient constructor quot, based on PER
slotosch
parents:
diff
changeset
|
4 |
Copyright 1997 Technische Universitaet Muenchen |
9a4f353107da
(higher-order) quotient constructor quot, based on PER
slotosch
parents:
diff
changeset
|
5 |
|
9a4f353107da
(higher-order) quotient constructor quot, based on PER
slotosch
parents:
diff
changeset
|
6 |
*) |
9a4f353107da
(higher-order) quotient constructor quot, based on PER
slotosch
parents:
diff
changeset
|
7 |
|
9a4f353107da
(higher-order) quotient constructor quot, based on PER
slotosch
parents:
diff
changeset
|
8 |
(* first prove some helpful lemmas *) |
5069 | 9 |
Goalw [quot_def] "{y. y===x}:quot"; |
2905
9a4f353107da
(higher-order) quotient constructor quot, based on PER
slotosch
parents:
diff
changeset
|
10 |
by (Asm_simp_tac 1); |
5858 | 11 |
by (blast_tac (claset() addIs [per_sym]) 1); |
2905
9a4f353107da
(higher-order) quotient constructor quot, based on PER
slotosch
parents:
diff
changeset
|
12 |
qed "per_class_rep_quot"; |
9a4f353107da
(higher-order) quotient constructor quot, based on PER
slotosch
parents:
diff
changeset
|
13 |
|
5858 | 14 |
Goal "Rep_quot a = Rep_quot b ==> a=b"; |
3457 | 15 |
by (rtac (Rep_quot_inverse RS subst) 1); |
2905
9a4f353107da
(higher-order) quotient constructor quot, based on PER
slotosch
parents:
diff
changeset
|
16 |
by (res_inst_tac [("t","a")] (Rep_quot_inverse RS subst) 1); |
9a4f353107da
(higher-order) quotient constructor quot, based on PER
slotosch
parents:
diff
changeset
|
17 |
by (Asm_simp_tac 1); |
9a4f353107da
(higher-order) quotient constructor quot, based on PER
slotosch
parents:
diff
changeset
|
18 |
qed "quot_eq"; |
9a4f353107da
(higher-order) quotient constructor quot, based on PER
slotosch
parents:
diff
changeset
|
19 |
|
9a4f353107da
(higher-order) quotient constructor quot, based on PER
slotosch
parents:
diff
changeset
|
20 |
(* prepare induction and exhaustiveness *) |
5858 | 21 |
Goal "!s. s:quot --> P (Abs_quot s) ==> P x"; |
3457 | 22 |
by (rtac (Abs_quot_inverse RS subst) 1); |
23 |
by (rtac Rep_quot 1); |
|
2905
9a4f353107da
(higher-order) quotient constructor quot, based on PER
slotosch
parents:
diff
changeset
|
24 |
by (dres_inst_tac [("x","Rep_quot x")] spec 1); |
9a4f353107da
(higher-order) quotient constructor quot, based on PER
slotosch
parents:
diff
changeset
|
25 |
by (asm_full_simp_tac (HOL_ss addsimps [Rep_quot,Rep_quot_inverse]) 1); |
9a4f353107da
(higher-order) quotient constructor quot, based on PER
slotosch
parents:
diff
changeset
|
26 |
qed "all_q"; |
9a4f353107da
(higher-order) quotient constructor quot, based on PER
slotosch
parents:
diff
changeset
|
27 |
|
5069 | 28 |
Goal "? s. s:quot & x=Abs_quot s"; |
2905
9a4f353107da
(higher-order) quotient constructor quot, based on PER
slotosch
parents:
diff
changeset
|
29 |
by (res_inst_tac [("x","Rep_quot x")] exI 1); |
9a4f353107da
(higher-order) quotient constructor quot, based on PER
slotosch
parents:
diff
changeset
|
30 |
by (asm_full_simp_tac (HOL_ss addsimps [Rep_quot,Rep_quot_inverse]) 1); |
9a4f353107da
(higher-order) quotient constructor quot, based on PER
slotosch
parents:
diff
changeset
|
31 |
qed "exh_q"; |
9a4f353107da
(higher-order) quotient constructor quot, based on PER
slotosch
parents:
diff
changeset
|
32 |
|
9a4f353107da
(higher-order) quotient constructor quot, based on PER
slotosch
parents:
diff
changeset
|
33 |
(* some lemmas for the equivalence classes *) |
9a4f353107da
(higher-order) quotient constructor quot, based on PER
slotosch
parents:
diff
changeset
|
34 |
|
9a4f353107da
(higher-order) quotient constructor quot, based on PER
slotosch
parents:
diff
changeset
|
35 |
(* equality and symmetry for equivalence classes *) |
5858 | 36 |
Goalw [peclass_def] "x===y==><[x]>=<[y]>"; |
2905
9a4f353107da
(higher-order) quotient constructor quot, based on PER
slotosch
parents:
diff
changeset
|
37 |
by (res_inst_tac [("f","Abs_quot")] arg_cong 1); |
3457 | 38 |
by (rtac Collect_cong 1); |
39 |
by (rtac iffI 1); |
|
40 |
by (etac per_trans 1);by (assume_tac 1); |
|
41 |
by (etac per_trans 1); |
|
42 |
by (etac per_sym 1); |
|
2905
9a4f353107da
(higher-order) quotient constructor quot, based on PER
slotosch
parents:
diff
changeset
|
43 |
qed "per_class_eqI"; |
9a4f353107da
(higher-order) quotient constructor quot, based on PER
slotosch
parents:
diff
changeset
|
44 |
|
5858 | 45 |
Goalw [peclass_def] "<[(x::'a::er)]>=<[y]>==>x===y"; |
2905
9a4f353107da
(higher-order) quotient constructor quot, based on PER
slotosch
parents:
diff
changeset
|
46 |
by (dres_inst_tac [("f","Rep_quot")] arg_cong 1); |
9a4f353107da
(higher-order) quotient constructor quot, based on PER
slotosch
parents:
diff
changeset
|
47 |
by (asm_full_simp_tac(HOL_ss addsimps [Abs_quot_inverse,per_class_rep_quot])1); |
3457 | 48 |
by (dres_inst_tac [("c","x")] equalityCE 1);by (assume_tac 3); |
5858 | 49 |
by Safe_tac; |
50 |
by (blast_tac (claset() addIs [er_refl]) 1); |
|
2905
9a4f353107da
(higher-order) quotient constructor quot, based on PER
slotosch
parents:
diff
changeset
|
51 |
qed "er_class_eqE"; |
9a4f353107da
(higher-order) quotient constructor quot, based on PER
slotosch
parents:
diff
changeset
|
52 |
|
5858 | 53 |
Goalw [peclass_def] "[|x:D;<[x]>=<[y]>|]==>x===y"; |
3457 | 54 |
by (dtac DomainD 1); |
2905
9a4f353107da
(higher-order) quotient constructor quot, based on PER
slotosch
parents:
diff
changeset
|
55 |
by (dres_inst_tac [("f","Rep_quot")] arg_cong 1); |
9a4f353107da
(higher-order) quotient constructor quot, based on PER
slotosch
parents:
diff
changeset
|
56 |
by (asm_full_simp_tac(HOL_ss addsimps [Abs_quot_inverse,per_class_rep_quot])1); |
3457 | 57 |
by (dres_inst_tac [("c","x")] equalityCE 1);by (assume_tac 3); |
5858 | 58 |
by Auto_tac; |
2905
9a4f353107da
(higher-order) quotient constructor quot, based on PER
slotosch
parents:
diff
changeset
|
59 |
qed "per_class_eqE"; |
9a4f353107da
(higher-order) quotient constructor quot, based on PER
slotosch
parents:
diff
changeset
|
60 |
|
5069 | 61 |
Goal "<[(x::'a::er)]>=<[y]>=x===y"; |
3457 | 62 |
by (rtac iffI 1); |
63 |
by (etac er_class_eqE 1); |
|
64 |
by (etac per_class_eqI 1); |
|
2905
9a4f353107da
(higher-order) quotient constructor quot, based on PER
slotosch
parents:
diff
changeset
|
65 |
qed "er_class_eq"; |
9a4f353107da
(higher-order) quotient constructor quot, based on PER
slotosch
parents:
diff
changeset
|
66 |
|
5858 | 67 |
Goal "x:D==><[x]>=<[y]>=x===y"; |
3457 | 68 |
by (rtac iffI 1); |
69 |
by (etac per_class_eqE 1);by (assume_tac 1); |
|
70 |
by (etac per_class_eqI 1); |
|
2905
9a4f353107da
(higher-order) quotient constructor quot, based on PER
slotosch
parents:
diff
changeset
|
71 |
qed "per_class_eq"; |
9a4f353107da
(higher-order) quotient constructor quot, based on PER
slotosch
parents:
diff
changeset
|
72 |
|
9a4f353107da
(higher-order) quotient constructor quot, based on PER
slotosch
parents:
diff
changeset
|
73 |
(* inequality *) |
5858 | 74 |
Goal "[|x:D;~x===y|]==><[x]>~=<[y]>"; |
3457 | 75 |
by (rtac notI 1); |
76 |
by (dtac per_class_eqE 1); |
|
4477
b3e5857d8d99
New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
paulson
parents:
3842
diff
changeset
|
77 |
by Auto_tac; |
2905
9a4f353107da
(higher-order) quotient constructor quot, based on PER
slotosch
parents:
diff
changeset
|
78 |
qed "per_class_neqI"; |
9a4f353107da
(higher-order) quotient constructor quot, based on PER
slotosch
parents:
diff
changeset
|
79 |
|
5858 | 80 |
Goal "~(x::'a::er)===y==><[x]>~=<[y]>"; |
3457 | 81 |
by (rtac notI 1); |
82 |
by (dtac er_class_eqE 1); |
|
4477
b3e5857d8d99
New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
paulson
parents:
3842
diff
changeset
|
83 |
by Auto_tac; |
2905
9a4f353107da
(higher-order) quotient constructor quot, based on PER
slotosch
parents:
diff
changeset
|
84 |
qed "er_class_neqI"; |
9a4f353107da
(higher-order) quotient constructor quot, based on PER
slotosch
parents:
diff
changeset
|
85 |
|
5858 | 86 |
Goal "<[x]>~=<[y]>==>~x===y"; |
3457 | 87 |
by (rtac notI 1); |
88 |
by (etac notE 1); |
|
89 |
by (etac per_class_eqI 1); |
|
2905
9a4f353107da
(higher-order) quotient constructor quot, based on PER
slotosch
parents:
diff
changeset
|
90 |
qed "per_class_neqE"; |
9a4f353107da
(higher-order) quotient constructor quot, based on PER
slotosch
parents:
diff
changeset
|
91 |
|
5858 | 92 |
Goal "x:D==><[x]>~=<[y]>=(~x===y)"; |
3457 | 93 |
by (rtac iffI 1); |
94 |
by (etac per_class_neqE 1); |
|
95 |
by (etac per_class_neqI 1);by (assume_tac 1); |
|
2905
9a4f353107da
(higher-order) quotient constructor quot, based on PER
slotosch
parents:
diff
changeset
|
96 |
qed "per_class_not"; |
9a4f353107da
(higher-order) quotient constructor quot, based on PER
slotosch
parents:
diff
changeset
|
97 |
|
5069 | 98 |
Goal "<[(x::'a::er)]>~=<[y]>=(~x===y)"; |
3457 | 99 |
by (rtac iffI 1); |
100 |
by (etac per_class_neqE 1); |
|
101 |
by (etac er_class_neqI 1); |
|
2905
9a4f353107da
(higher-order) quotient constructor quot, based on PER
slotosch
parents:
diff
changeset
|
102 |
qed "er_class_not"; |
9a4f353107da
(higher-order) quotient constructor quot, based on PER
slotosch
parents:
diff
changeset
|
103 |
|
9a4f353107da
(higher-order) quotient constructor quot, based on PER
slotosch
parents:
diff
changeset
|
104 |
(* exhaustiveness and induction *) |
5069 | 105 |
Goalw [peclass_def] "? s. x=<[s]>"; |
3457 | 106 |
by (rtac all_q 1); |
2905
9a4f353107da
(higher-order) quotient constructor quot, based on PER
slotosch
parents:
diff
changeset
|
107 |
by (strip_tac 1); |
9a4f353107da
(higher-order) quotient constructor quot, based on PER
slotosch
parents:
diff
changeset
|
108 |
by (asm_full_simp_tac (HOL_ss addsimps [mem_Collect_eq,quot_def]) 1); |
3457 | 109 |
by (etac exE 1); |
2905
9a4f353107da
(higher-order) quotient constructor quot, based on PER
slotosch
parents:
diff
changeset
|
110 |
by (res_inst_tac [("x","r")] exI 1); |
3457 | 111 |
by (rtac quot_eq 1); |
2905
9a4f353107da
(higher-order) quotient constructor quot, based on PER
slotosch
parents:
diff
changeset
|
112 |
by (subgoal_tac "s:quot" 1); |
9a4f353107da
(higher-order) quotient constructor quot, based on PER
slotosch
parents:
diff
changeset
|
113 |
by (asm_simp_tac(HOL_ss addsimps [Abs_quot_inverse,per_class_rep_quot])1); |
3457 | 114 |
by (rtac set_ext 1); |
5858 | 115 |
by (Blast_tac 1); |
2905
9a4f353107da
(higher-order) quotient constructor quot, based on PER
slotosch
parents:
diff
changeset
|
116 |
by (asm_full_simp_tac (HOL_ss addsimps [mem_Collect_eq,quot_def]) 1); |
5858 | 117 |
by (Blast_tac 1); |
2905
9a4f353107da
(higher-order) quotient constructor quot, based on PER
slotosch
parents:
diff
changeset
|
118 |
qed "per_class_exh"; |
9a4f353107da
(higher-order) quotient constructor quot, based on PER
slotosch
parents:
diff
changeset
|
119 |
|
5858 | 120 |
Goal "!x. P<[x]> ==> P s"; |
121 |
by (cut_facts_tac [read_instantiate[("x","s::'a::per quot")] per_class_exh] 1); |
|
122 |
by (Blast_tac 1); |
|
2905
9a4f353107da
(higher-order) quotient constructor quot, based on PER
slotosch
parents:
diff
changeset
|
123 |
qed "per_class_all"; |
9a4f353107da
(higher-order) quotient constructor quot, based on PER
slotosch
parents:
diff
changeset
|
124 |
|
9a4f353107da
(higher-order) quotient constructor quot, based on PER
slotosch
parents:
diff
changeset
|
125 |
(* theorems for any_in *) |
5069 | 126 |
Goalw [any_in_def,peclass_def] "any_in<[(s::'a::er)]>===s"; |
5858 | 127 |
br selectI2 1; |
128 |
br refl 1; |
|
2905
9a4f353107da
(higher-order) quotient constructor quot, based on PER
slotosch
parents:
diff
changeset
|
129 |
by (fold_goals_tac [peclass_def]); |
5858 | 130 |
be er_class_eqE 1; |
2905
9a4f353107da
(higher-order) quotient constructor quot, based on PER
slotosch
parents:
diff
changeset
|
131 |
qed "er_any_in_class"; |
9a4f353107da
(higher-order) quotient constructor quot, based on PER
slotosch
parents:
diff
changeset
|
132 |
|
5858 | 133 |
Goalw [any_in_def,peclass_def] "s:D==>any_in<[s]>===s"; |
134 |
br selectI2 1; |
|
135 |
br refl 1; |
|
2905
9a4f353107da
(higher-order) quotient constructor quot, based on PER
slotosch
parents:
diff
changeset
|
136 |
by (fold_goals_tac [peclass_def]); |
5858 | 137 |
br per_sym 1; |
138 |
be per_class_eqE 1; |
|
139 |
be sym 1; |
|
2905
9a4f353107da
(higher-order) quotient constructor quot, based on PER
slotosch
parents:
diff
changeset
|
140 |
qed "per_any_in_class"; |
9a4f353107da
(higher-order) quotient constructor quot, based on PER
slotosch
parents:
diff
changeset
|
141 |
|
5858 | 142 |
Goal "<[any_in (s::'a::er quot)]> = s"; |
143 |
br per_class_all 1; |
|
144 |
br allI 1; |
|
145 |
br (er_any_in_class RS per_class_eqI) 1; |
|
2905
9a4f353107da
(higher-order) quotient constructor quot, based on PER
slotosch
parents:
diff
changeset
|
146 |
qed "er_class_any_in"; |
9a4f353107da
(higher-order) quotient constructor quot, based on PER
slotosch
parents:
diff
changeset
|
147 |
|
9a4f353107da
(higher-order) quotient constructor quot, based on PER
slotosch
parents:
diff
changeset
|
148 |
(* equivalent theorem for per would need !x.x:D *) |
5858 | 149 |
Goal "!x::'a::per. x:D==><[any_in (q::'a::per quot)]> = q"; |
150 |
br per_class_all 1; |
|
151 |
br allI 1; |
|
152 |
br (per_any_in_class RS per_class_eqI) 1; |
|
153 |
be spec 1; |
|
2905
9a4f353107da
(higher-order) quotient constructor quot, based on PER
slotosch
parents:
diff
changeset
|
154 |
qed "per_class_any_in"; |
9a4f353107da
(higher-order) quotient constructor quot, based on PER
slotosch
parents:
diff
changeset
|
155 |
|
5858 | 156 |
(* is like theorem for class er *) |