53 val mem_def2 = @{lemma "S y ==> y : S" by (simp add: mem_def)} |
53 val mem_def2 = @{lemma "S y ==> y : S" by (simp add: mem_def)} |
54 |
54 |
55 (* constructs the term lambda (c::rty => bool). EX (x::rty). c = rel x *) |
55 (* constructs the term lambda (c::rty => bool). EX (x::rty). c = rel x *) |
56 fun typedef_term rel rty lthy = |
56 fun typedef_term rel rty lthy = |
57 let |
57 let |
58 val [x, c] = [("x", rty), ("c", HOLogic.mk_setT rty)] |
58 val [x, c] = |
59 |> Variable.variant_frees lthy [rel] |
59 [("x", rty), ("c", HOLogic.mk_setT rty)] |
60 |> map Free |
60 |> Variable.variant_frees lthy [rel] |
|
61 |> map Free |
61 in |
62 in |
62 lambda c (HOLogic.exists_const rty $ |
63 lambda c (HOLogic.exists_const rty $ |
63 lambda x (HOLogic.mk_eq (c, (rel $ x)))) |
64 lambda x (HOLogic.mk_eq (c, (rel $ x)))) |
64 end |
65 end |
65 |
66 |
84 val rep_thm = #Rep typedef_info RS mem_def1 |
85 val rep_thm = #Rep typedef_info RS mem_def1 |
85 val rep_inv = #Rep_inverse typedef_info |
86 val rep_inv = #Rep_inverse typedef_info |
86 val abs_inv = mem_def2 RS #Abs_inverse typedef_info |
87 val abs_inv = mem_def2 RS #Abs_inverse typedef_info |
87 val rep_inj = #Rep_inject typedef_info |
88 val rep_inj = #Rep_inject typedef_info |
88 in |
89 in |
89 (rtac @{thm Quot_Type.intro} THEN' |
90 (rtac @{thm Quot_Type.intro} THEN' RANGE [ |
90 RANGE [rtac equiv_thm, |
91 rtac equiv_thm, |
91 rtac rep_thm, |
92 rtac rep_thm, |
92 rtac rep_inv, |
93 rtac rep_inv, |
93 EVERY' (map rtac [abs_inv, @{thm exI}, @{thm refl}]), |
94 EVERY' (map rtac [abs_inv, @{thm exI}, @{thm refl}]), |
94 rtac rep_inj]) 1 |
95 rtac rep_inj]) 1 |
95 end |
96 end |
96 |
97 |
97 |
98 |
98 (* proves the Quot_Type theorem for the new type *) |
99 (* proves the Quot_Type theorem for the new type *) |
99 fun typedef_quot_type_thm (rel, abs, rep, equiv_thm, typedef_info) lthy = |
100 fun typedef_quot_type_thm (rel, abs, rep, equiv_thm, typedef_info) lthy = |
100 let |
101 let |
101 val quot_type_const = Const (@{const_name "Quot_Type"}, dummyT) |
102 val quot_type_const = Const (@{const_name "Quot_Type"}, dummyT) |
102 val goal = HOLogic.mk_Trueprop (quot_type_const $ rel $ abs $ rep) |
103 val goal = |
103 |> Syntax.check_term lthy |
104 HOLogic.mk_Trueprop (quot_type_const $ rel $ abs $ rep) |
|
105 |> Syntax.check_term lthy |
104 in |
106 in |
105 Goal.prove lthy [] [] goal |
107 Goal.prove lthy [] [] goal |
106 (K (typedef_quot_type_tac equiv_thm typedef_info)) |
108 (K (typedef_quot_type_tac equiv_thm typedef_info)) |
107 end |
109 end |
108 |
110 |
109 (* proves the quotient theorem for the new type *) |
111 (* proves the quotient theorem for the new type *) |
110 fun typedef_quotient_thm (rel, abs, rep, abs_def, rep_def, quot_type_thm) lthy = |
112 fun typedef_quotient_thm (rel, abs, rep, abs_def, rep_def, quot_type_thm) lthy = |
111 let |
113 let |
112 val quotient_const = Const (@{const_name "Quotient"}, dummyT) |
114 val quotient_const = Const (@{const_name "Quotient"}, dummyT) |
113 val goal = HOLogic.mk_Trueprop (quotient_const $ rel $ abs $ rep) |
115 val goal = |
114 |> Syntax.check_term lthy |
116 HOLogic.mk_Trueprop (quotient_const $ rel $ abs $ rep) |
|
117 |> Syntax.check_term lthy |
115 |
118 |
116 val typedef_quotient_thm_tac = |
119 val typedef_quotient_thm_tac = |
117 EVERY1 [K (rewrite_goals_tac [abs_def, rep_def]), |
120 EVERY1 [ |
118 rtac @{thm Quot_Type.Quotient}, |
121 K (rewrite_goals_tac [abs_def, rep_def]), |
119 rtac quot_type_thm] |
122 rtac @{thm Quot_Type.Quotient}, |
|
123 rtac quot_type_thm] |
120 in |
124 in |
121 Goal.prove lthy [] [] goal |
125 Goal.prove lthy [] [] goal |
122 (K typedef_quotient_thm_tac) |
126 (K typedef_quotient_thm_tac) |
123 end |
127 end |
124 |
128 |
159 val equiv_thm_name = Binding.suffix_name "_equivp" qty_name |
163 val equiv_thm_name = Binding.suffix_name "_equivp" qty_name |
160 |
164 |
161 (* storing the quot-info *) |
165 (* storing the quot-info *) |
162 (* FIXME: VarifyT should not be used - at the moment it allows matching against the types. *) |
166 (* FIXME: VarifyT should not be used - at the moment it allows matching against the types. *) |
163 fun qinfo phi = transform_quotdata phi |
167 fun qinfo phi = transform_quotdata phi |
164 {qtyp = Logic.varifyT Abs_ty, rtyp = Logic.varifyT rty, |
168 {qtyp = Logic.varifyT Abs_ty, rtyp = Logic.varifyT rty, |
165 equiv_rel = map_types Logic.varifyT rel, equiv_thm = equiv_thm} |
169 equiv_rel = map_types Logic.varifyT rel, equiv_thm = equiv_thm} |
166 val lthy4 = Local_Theory.declaration true |
170 val lthy4 = Local_Theory.declaration true |
167 (fn phi => quotdata_update_gen qty_full_name (qinfo phi)) lthy3 |
171 (fn phi => quotdata_update_gen qty_full_name (qinfo phi)) lthy3 |
168 in |
172 in |
169 lthy4 |
173 lthy4 |
170 |> note (quotient_thm_name, quotient_thm, [intern_attr quotient_rules_add]) |
174 |> note (quotient_thm_name, quotient_thm, [intern_attr quotient_rules_add]) |
171 ||>> note (equiv_thm_name, equiv_thm, [intern_attr equiv_rules_add]) |
175 ||>> note (equiv_thm_name, equiv_thm, [intern_attr equiv_rules_add]) |
172 end |
176 end |