equal
deleted
inserted
replaced
11 axiomatization |
11 axiomatization |
12 RR :: "trm \<Rightarrow> trm \<Rightarrow> bool" |
12 RR :: "trm \<Rightarrow> trm \<Rightarrow> bool" |
13 where |
13 where |
14 r_eq: "EQUIV RR" |
14 r_eq: "EQUIV RR" |
15 |
15 |
16 ML {* print_quotdata @{context} *} |
16 print_quotients |
17 |
17 |
18 quotient qtrm = trm / "RR" |
18 quotient qtrm = trm / "RR" |
19 apply(rule r_eq) |
19 apply(rule r_eq) |
20 done |
20 done |
21 |
21 |
22 ML {* print_quotdata @{context} *} |
22 print_quotients |
23 |
23 |
24 typ qtrm |
24 typ qtrm |
25 term Rep_qtrm |
25 term Rep_qtrm |
26 term REP_qtrm |
26 term REP_qtrm |
27 term Abs_qtrm |
27 term Abs_qtrm |
49 |
49 |
50 quotient qtrm' = "'a trm'" / "R'" |
50 quotient qtrm' = "'a trm'" / "R'" |
51 apply(rule r_eq') |
51 apply(rule r_eq') |
52 done |
52 done |
53 |
53 |
|
54 print_quotients |
54 print_theorems |
55 print_theorems |
55 |
56 |
56 term ABS_qtrm' |
57 term ABS_qtrm' |
57 term REP_qtrm' |
58 term REP_qtrm' |
58 thm QUOT_TYPE_qtrm' |
59 thm QUOT_TYPE_qtrm' |
69 consts Rt :: "t \<Rightarrow> t \<Rightarrow> bool" |
70 consts Rt :: "t \<Rightarrow> t \<Rightarrow> bool" |
70 axioms t_eq: "EQUIV Rt" |
71 axioms t_eq: "EQUIV Rt" |
71 |
72 |
72 quotient qt = "t" / "Rt" |
73 quotient qt = "t" / "Rt" |
73 by (rule t_eq) |
74 by (rule t_eq) |
|
75 |
|
76 print_quotients |
|
77 |
|
78 ML {* |
|
79 Toplevel.context_of; |
|
80 Toplevel.keep |
|
81 *} |
74 |
82 |
75 ML {* |
83 ML {* |
76 get_fun repF @{typ t} @{typ qt} @{context} @{typ "((((qt \<Rightarrow> qt) \<Rightarrow> qt) \<Rightarrow> qt) list) * nat"} |
84 get_fun repF @{typ t} @{typ qt} @{context} @{typ "((((qt \<Rightarrow> qt) \<Rightarrow> qt) \<Rightarrow> qt) list) * nat"} |
77 |> fst |
85 |> fst |
78 |> Syntax.string_of_term @{context} |
86 |> Syntax.string_of_term @{context} |
128 |
136 |
129 quotient qt' = "'a t'" / "Rt'" |
137 quotient qt' = "'a t'" / "Rt'" |
130 apply(rule t_eq') |
138 apply(rule t_eq') |
131 done |
139 done |
132 |
140 |
|
141 print_quotients |
133 print_theorems |
142 print_theorems |
134 |
143 |
135 local_setup {* |
144 local_setup {* |
136 make_const_def @{binding VR'} @{term "vr'"} NoSyn @{typ "'a t'"} @{typ "'a qt'"} #> snd #> |
145 make_const_def @{binding VR'} @{term "vr'"} NoSyn @{typ "'a t'"} @{typ "'a qt'"} #> snd #> |
137 make_const_def @{binding AP'} @{term "ap'"} NoSyn @{typ "'a t'"} @{typ "'a qt'"} #> snd #> |
146 make_const_def @{binding AP'} @{term "ap'"} NoSyn @{typ "'a t'"} @{typ "'a qt'"} #> snd #> |