94 |
94 |
95 fun setup_by_quotient no_code quot_thm maybe_reflp_thm lthy = |
95 fun setup_by_quotient no_code quot_thm maybe_reflp_thm lthy = |
96 let |
96 let |
97 val transfer_attr = Attrib.internal (K Transfer.transfer_add) |
97 val transfer_attr = Attrib.internal (K Transfer.transfer_add) |
98 val (_, qty) = Lifting_Term.quot_thm_rty_qty quot_thm |
98 val (_, qty) = Lifting_Term.quot_thm_rty_qty quot_thm |
|
99 val induct_attr = Attrib.internal (K (Induct.induct_type (fst (dest_Type qty)))) |
99 val qty_name = (Binding.name o fst o dest_Type) qty |
100 val qty_name = (Binding.name o fst o dest_Type) qty |
100 fun qualify suffix = Binding.qualified true suffix qty_name |
101 fun qualify suffix = Binding.qualified true suffix qty_name |
101 val lthy' = case maybe_reflp_thm of |
102 val lthy' = case maybe_reflp_thm of |
102 SOME reflp_thm => lthy |
103 SOME reflp_thm => lthy |
103 |> (snd oo Local_Theory.note) ((qualify "bi_total", [transfer_attr]), |
104 |> (snd oo Local_Theory.note) ((qualify "bi_total", [transfer_attr]), |
104 [[quot_thm, reflp_thm] MRSL @{thm Quotient_bi_total}]) |
105 [[quot_thm, reflp_thm] MRSL @{thm Quotient_bi_total}]) |
105 |> (snd oo Local_Theory.note) ((qualify "id_abs_transfer", [transfer_attr]), |
106 |> (snd oo Local_Theory.note) ((qualify "id_abs_transfer", [transfer_attr]), |
106 [[quot_thm, reflp_thm] MRSL @{thm Quotient_id_abs_transfer}]) |
107 [[quot_thm, reflp_thm] MRSL @{thm Quotient_id_abs_transfer}]) |
|
108 |> (snd oo Local_Theory.note) ((qualify "abs_induct", [induct_attr]), |
|
109 [[quot_thm, reflp_thm] MRSL @{thm Quotient_total_abs_induct}]) |
107 | NONE => lthy |
110 | NONE => lthy |
108 |> (snd oo Local_Theory.note) ((qualify "All_transfer", [transfer_attr]), |
111 |> (snd oo Local_Theory.note) ((qualify "All_transfer", [transfer_attr]), |
109 [quot_thm RS @{thm Quotient_All_transfer}]) |
112 [quot_thm RS @{thm Quotient_All_transfer}]) |
110 |> (snd oo Local_Theory.note) ((qualify "Ex_transfer", [transfer_attr]), |
113 |> (snd oo Local_Theory.note) ((qualify "Ex_transfer", [transfer_attr]), |
111 [quot_thm RS @{thm Quotient_Ex_transfer}]) |
114 [quot_thm RS @{thm Quotient_Ex_transfer}]) |
112 |> (snd oo Local_Theory.note) ((qualify "forall_transfer", [transfer_attr]), |
115 |> (snd oo Local_Theory.note) ((qualify "forall_transfer", [transfer_attr]), |
113 [quot_thm RS @{thm Quotient_forall_transfer}]) |
116 [quot_thm RS @{thm Quotient_forall_transfer}]) |
|
117 |> (snd oo Local_Theory.note) ((qualify "abs_induct", [induct_attr]), |
|
118 [quot_thm RS @{thm Quotient_abs_induct}]) |
114 in |
119 in |
115 lthy' |
120 lthy' |
116 |> (snd oo Local_Theory.note) ((qualify "right_unique", [transfer_attr]), |
121 |> (snd oo Local_Theory.note) ((qualify "right_unique", [transfer_attr]), |
117 [quot_thm RS @{thm Quotient_right_unique}]) |
122 [quot_thm RS @{thm Quotient_right_unique}]) |
118 |> (snd oo Local_Theory.note) ((qualify "right_total", [transfer_attr]), |
123 |> (snd oo Local_Theory.note) ((qualify "right_total", [transfer_attr]), |