77 (typedef_term rel rty lthy) |
77 (typedef_term rel rty lthy) |
78 NONE typedef_tac) lthy |
78 NONE typedef_tac) lthy |
79 end |
79 end |
80 |
80 |
81 |
81 |
82 (* tactic to prove the Quot_Type theorem for the new type *) |
82 (* tactic to prove the quot_type theorem for the new type *) |
83 fun typedef_quot_type_tac equiv_thm (typedef_info: Typedef.info) = |
83 fun typedef_quot_type_tac equiv_thm (typedef_info: Typedef.info) = |
84 let |
84 let |
85 val rep_thm = #Rep typedef_info RS mem_def1 |
85 val rep_thm = #Rep typedef_info RS mem_def1 |
86 val rep_inv = #Rep_inverse typedef_info |
86 val rep_inv = #Rep_inverse typedef_info |
87 val abs_inv = mem_def2 RS #Abs_inverse typedef_info |
87 val abs_inv = mem_def2 RS #Abs_inverse typedef_info |
88 val rep_inj = #Rep_inject typedef_info |
88 val rep_inj = #Rep_inject typedef_info |
89 in |
89 in |
90 (rtac @{thm Quot_Type.intro} THEN' RANGE [ |
90 (rtac @{thm quot_type.intro} THEN' RANGE [ |
91 rtac equiv_thm, |
91 rtac equiv_thm, |
92 rtac rep_thm, |
92 rtac rep_thm, |
93 rtac rep_inv, |
93 rtac rep_inv, |
94 EVERY' (map rtac [abs_inv, @{thm exI}, @{thm refl}]), |
94 EVERY' (map rtac [abs_inv, @{thm exI}, @{thm refl}]), |
95 rtac rep_inj]) 1 |
95 rtac rep_inj]) 1 |
96 end |
96 end |
97 |
97 |
98 |
98 |
99 (* proves the Quot_Type theorem for the new type *) |
99 (* proves the quot_type theorem for the new type *) |
100 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 = |
101 let |
101 let |
102 val quot_type_const = Const (@{const_name "Quot_Type"}, dummyT) |
102 val quot_type_const = Const (@{const_name "quot_type"}, dummyT) |
103 val goal = |
103 val goal = |
104 HOLogic.mk_Trueprop (quot_type_const $ rel $ abs $ rep) |
104 HOLogic.mk_Trueprop (quot_type_const $ rel $ abs $ rep) |
105 |> Syntax.check_term lthy |
105 |> Syntax.check_term lthy |
106 in |
106 in |
107 Goal.prove lthy [] [] goal |
107 Goal.prove lthy [] [] goal |
117 |> Syntax.check_term lthy |
117 |> Syntax.check_term lthy |
118 |
118 |
119 val typedef_quotient_thm_tac = |
119 val typedef_quotient_thm_tac = |
120 EVERY1 [ |
120 EVERY1 [ |
121 K (rewrite_goals_tac [abs_def, rep_def]), |
121 K (rewrite_goals_tac [abs_def, rep_def]), |
122 rtac @{thm Quot_Type.Quotient}, |
122 rtac @{thm quot_type.Quotient}, |
123 rtac quot_type_thm] |
123 rtac quot_type_thm] |
124 in |
124 in |
125 Goal.prove lthy [] [] goal |
125 Goal.prove lthy [] [] goal |
126 (K typedef_quotient_thm_tac) |
126 (K typedef_quotient_thm_tac) |
127 end |
127 end |
140 val Rep_name = #Rep_name typedef_info |
140 val Rep_name = #Rep_name typedef_info |
141 val Abs_const = Const (Abs_name, Rep_ty --> Abs_ty) |
141 val Abs_const = Const (Abs_name, Rep_ty --> Abs_ty) |
142 val Rep_const = Const (Rep_name, Abs_ty --> Rep_ty) |
142 val Rep_const = Const (Rep_name, Abs_ty --> Rep_ty) |
143 |
143 |
144 (* more useful abs and rep definitions *) |
144 (* more useful abs and rep definitions *) |
145 val abs_const = Const (@{const_name "Quot_Type.abs"}, dummyT ) |
145 val abs_const = Const (@{const_name "quot_type.abs"}, dummyT ) |
146 val rep_const = Const (@{const_name "Quot_Type.rep"}, dummyT ) |
146 val rep_const = Const (@{const_name "quot_type.rep"}, dummyT ) |
147 val abs_trm = Syntax.check_term lthy1 (abs_const $ rel $ Abs_const) |
147 val abs_trm = Syntax.check_term lthy1 (abs_const $ rel $ Abs_const) |
148 val rep_trm = Syntax.check_term lthy1 (rep_const $ Rep_const) |
148 val rep_trm = Syntax.check_term lthy1 (rep_const $ Rep_const) |
149 val abs_name = Binding.prefix_name "abs_" qty_name |
149 val abs_name = Binding.prefix_name "abs_" qty_name |
150 val rep_name = Binding.prefix_name "rep_" qty_name |
150 val rep_name = Binding.prefix_name "rep_" qty_name |
151 |
151 |