42 |
42 |
43 |
43 |
44 (* definition of quotient types *) |
44 (* definition of quotient types *) |
45 (********************************) |
45 (********************************) |
46 |
46 |
|
47 val mem_def1 = @{lemma "y : S ==> S y" by (simp add: mem_def)} |
|
48 val mem_def2 = @{lemma "S y ==> y : S" by (simp add: mem_def)} |
|
49 |
47 (* constructs the term lambda (c::rty => bool). EX (x::rty). c = rel x *) |
50 (* constructs the term lambda (c::rty => bool). EX (x::rty). c = rel x *) |
48 fun typedef_term rel rty lthy = |
51 fun typedef_term rel rty lthy = |
49 let |
52 let |
50 val [x, c] = [("x", rty), ("c", HOLogic.mk_setT rty)] |
53 val [x, c] = [("x", rty), ("c", HOLogic.mk_setT rty)] |
51 |> Variable.variant_frees lthy [rel] |
54 |> Variable.variant_frees lthy [rel] |
58 |
61 |
59 (* makes the new type definitions and proves non-emptyness*) |
62 (* makes the new type definitions and proves non-emptyness*) |
60 fun typedef_make (qty_name, mx, rel, rty) lthy = |
63 fun typedef_make (qty_name, mx, rel, rty) lthy = |
61 let |
64 let |
62 val typedef_tac = |
65 val typedef_tac = |
63 EVERY1 [rewrite_goal_tac @{thms mem_def}, |
66 EVERY1 [rtac @{thm exI}, |
64 rtac @{thm exI}, |
67 rtac mem_def2, |
65 rtac @{thm exI}, |
68 rtac @{thm exI}, |
66 rtac @{thm refl}] |
69 rtac @{thm refl}] |
67 val tfrees = map fst (Term.add_tfreesT rty []) |
70 val tfrees = map fst (Term.add_tfreesT rty []) |
68 in |
71 in |
69 Local_Theory.theory_result |
72 Local_Theory.theory_result |
74 end |
77 end |
75 |
78 |
76 (* tactic to prove the QUOT_TYPE theorem for the new type *) |
79 (* tactic to prove the QUOT_TYPE theorem for the new type *) |
77 fun typedef_quot_type_tac equiv_thm (typedef_info: Typedef.info) = |
80 fun typedef_quot_type_tac equiv_thm (typedef_info: Typedef.info) = |
78 let |
81 let |
79 val unfold_mem = MetaSimplifier.rewrite_rule [@{thm mem_def}] |
82 val rep_thm = (#Rep typedef_info) RS mem_def1 |
80 val rep_thm = #Rep typedef_info |> unfold_mem |
|
81 val rep_inv = #Rep_inverse typedef_info |
83 val rep_inv = #Rep_inverse typedef_info |
82 val abs_inv = #Abs_inverse typedef_info |> unfold_mem |
84 val abs_inv = mem_def2 RS (#Abs_inverse typedef_info) |
83 val rep_inj = #Rep_inject typedef_info |
85 val rep_inj = #Rep_inject typedef_info |
84 in |
86 in |
85 EVERY1 [rtac @{thm QUOT_TYPE.intro}, |
87 (rtac @{thm QUOT_TYPE.intro} THEN' |
86 rtac equiv_thm, |
88 RANGE [rtac equiv_thm, |
87 rtac rep_thm, |
89 rtac rep_thm, |
88 rtac rep_inv, |
90 rtac rep_inv, |
89 rtac abs_inv, |
91 EVERY' [rtac abs_inv, rtac @{thm exI}, rtac @{thm refl}], |
90 rtac @{thm exI}, |
92 rtac rep_inj]) 1 |
91 rtac @{thm refl}, |
|
92 rtac rep_inj] |
|
93 end |
93 end |
94 |
94 |
95 (* proves the QUOT_TYPE theorem *) |
95 (* proves the QUOT_TYPE theorem *) |
96 fun typedef_quot_type_thm (rel, abs, rep, equiv_thm, typedef_info) lthy = |
96 fun typedef_quot_type_thm (rel, abs, rep, equiv_thm, typedef_info) lthy = |
97 let |
97 let |
142 val REP_name = Binding.prefix_name "rep_" qty_name |
142 val REP_name = Binding.prefix_name "rep_" qty_name |
143 val (((ABS, ABS_def), (REP, REP_def)), lthy2) = |
143 val (((ABS, ABS_def), (REP, REP_def)), lthy2) = |
144 lthy1 |> define (ABS_name, NoSyn, ABS_trm) |
144 lthy1 |> define (ABS_name, NoSyn, ABS_trm) |
145 ||>> define (REP_name, NoSyn, REP_trm) |
145 ||>> define (REP_name, NoSyn, REP_trm) |
146 |
146 |
147 (* quot_type theorem *) |
147 (* quot_type theorem - needed below *) |
148 val quot_thm = typedef_quot_type_thm (rel, abs, rep, equiv_thm, typedef_info) lthy2 |
148 val quot_thm = typedef_quot_type_thm (rel, abs, rep, equiv_thm, typedef_info) lthy2 |
149 val quot_thm_name = Binding.prefix_name "QUOT_TYPE_" qty_name |
149 |
150 |
150 (* quotient theorem *) |
151 (* quotient theorem *) |
|
152 val quotient_thm = typedef_quotient_thm (rel, ABS, REP, ABS_def, REP_def, quot_thm) lthy2 |
151 val quotient_thm = typedef_quotient_thm (rel, ABS, REP, ABS_def, REP_def, quot_thm) lthy2 |
153 val quotient_thm_name = Binding.prefix_name "Quotient_" qty_name |
152 val quotient_thm_name = Binding.prefix_name "Quotient_" qty_name |
154 |
153 |
155 (* storing the quot-info *) |
154 (* storing the quot-info *) |
156 val qty_str = fst (Term.dest_Type abs_ty) |
155 val qty_str = fst (Term.dest_Type abs_ty) |
160 (* FIXME: the relation can be any term, that later maybe needs to be given *) |
159 (* FIXME: the relation can be any term, that later maybe needs to be given *) |
161 (* FIXME: a different type (in regularize_trm); how should tis be done? *) |
160 (* FIXME: a different type (in regularize_trm); how should tis be done? *) |
162 |
161 |
163 in |
162 in |
164 lthy3 |
163 lthy3 |
165 |> note (quot_thm_name, quot_thm, []) |
164 |> note (quotient_thm_name, quotient_thm, [intern_attr quotient_rules_add]) |
166 ||>> note (quotient_thm_name, quotient_thm, [intern_attr quotient_rules_add]) |
|
167 ||>> note (Binding.suffix_name "_equivp" qty_name, equiv_thm, [intern_attr equiv_rules_add]) |
165 ||>> note (Binding.suffix_name "_equivp" qty_name, equiv_thm, [intern_attr equiv_rules_add]) |
168 end |
166 end |
169 |
167 |
170 |
168 |
171 |
169 |