144 |
144 |
145 declare [[map list = (map, list_rel)]] |
145 declare [[map list = (map, list_rel)]] |
146 declare [[map * = (prod_fun, prod_rel)]] |
146 declare [[map * = (prod_fun, prod_rel)]] |
147 declare [[map "fun" = (fun_map, fun_rel)]] |
147 declare [[map "fun" = (fun_map, fun_rel)]] |
148 |
148 |
|
149 (* identity quotient is not here as it has to be applied first *) |
149 lemmas [quotient_thm] = |
150 lemmas [quotient_thm] = |
150 fun_quotient list_quotient |
151 fun_quotient list_quotient prod_quotient |
151 |
152 |
152 lemmas [quotient_rsp] = |
153 lemmas [quotient_rsp] = |
153 quot_rel_rsp nil_rsp cons_rsp foldl_rsp |
154 quot_rel_rsp nil_rsp cons_rsp foldl_rsp pair_rsp |
154 |
155 |
155 (* OPTION, PRODUCTS *) |
156 (* fun_map is not here since equivp is not true *) |
|
157 (* TODO: option, ... *) |
156 lemmas [quotient_equiv] = |
158 lemmas [quotient_equiv] = |
157 identity_equivp list_equivp |
159 identity_equivp list_equivp prod_equivp |
158 |
160 |
159 |
161 |
160 ML {* maps_lookup @{theory} "List.list" *} |
162 ML {* maps_lookup @{theory} "List.list" *} |
161 ML {* maps_lookup @{theory} "*" *} |
163 ML {* maps_lookup @{theory} "*" *} |
162 ML {* maps_lookup @{theory} "fun" *} |
164 ML {* maps_lookup @{theory} "fun" *} |
706 ML {* |
708 ML {* |
707 fun solve_quotient_assums ctxt thm = |
709 fun solve_quotient_assums ctxt thm = |
708 let val gl = hd (Drule.strip_imp_prems (cprop_of thm)) in |
710 let val gl = hd (Drule.strip_imp_prems (cprop_of thm)) in |
709 thm OF [Goal.prove_internal [] gl (fn _ => quotient_tac ctxt 1)] |
711 thm OF [Goal.prove_internal [] gl (fn _ => quotient_tac ctxt 1)] |
710 end |
712 end |
711 handle _ => error "solve_quotient_assums" |
713 handle _ => error "solve_quotient_assums failed. Maybe a quotient_thm is missing" |
712 *} |
714 *} |
713 |
715 |
|
716 (* Not used *) |
714 (* It proves the Quotient assumptions by calling quotient_tac *) |
717 (* It proves the Quotient assumptions by calling quotient_tac *) |
715 ML {* |
718 ML {* |
716 fun solve_quotient_assum i ctxt thm = |
719 fun solve_quotient_assum i ctxt thm = |
717 let |
720 let |
718 val tac = |
721 val tac = |
915 | Const (@{const_name "op ="},_) $ _ $ _ |
918 | Const (@{const_name "op ="},_) $ _ $ _ |
916 => rtac @{thm refl} ORELSE' |
919 => rtac @{thm refl} ORELSE' |
917 (resolve_tac trans2 THEN' RANGE [ |
920 (resolve_tac trans2 THEN' RANGE [ |
918 quot_true_tac ctxt (fst o dest_bcomb), quot_true_tac ctxt (snd o dest_bcomb)]) |
921 quot_true_tac ctxt (fst o dest_bcomb), quot_true_tac ctxt (snd o dest_bcomb)]) |
919 |
922 |
|
923 (* TODO: These patterns should should be somehow combined and generalized... *) |
920 | (Const (@{const_name fun_rel}, _) $ _ $ _) $ |
924 | (Const (@{const_name fun_rel}, _) $ _ $ _) $ |
921 (Const (@{const_name fun_rel}, _) $ _ $ _) $ |
925 (Const (@{const_name fun_rel}, _) $ _ $ _) $ |
922 (Const (@{const_name fun_rel}, _) $ _ $ _) |
926 (Const (@{const_name fun_rel}, _) $ _ $ _) |
|
927 => rtac @{thm quot_rel_rsp} THEN_ALL_NEW quotient_tac ctxt |
|
928 |
|
929 | (Const (@{const_name fun_rel}, _) $ _ $ _) $ |
|
930 (Const (@{const_name prod_rel}, _) $ _ $ _) $ |
|
931 (Const (@{const_name prod_rel}, _) $ _ $ _) |
923 => rtac @{thm quot_rel_rsp} THEN_ALL_NEW quotient_tac ctxt |
932 => rtac @{thm quot_rel_rsp} THEN_ALL_NEW quotient_tac ctxt |
924 |
933 |
925 (* respectfulness of constants; in particular of a simple relation *) |
934 (* respectfulness of constants; in particular of a simple relation *) |
926 | _ $ (Const _) $ (Const _) (* fun_rel, list_rel, etc but not equality *) |
935 | _ $ (Const _) $ (Const _) (* fun_rel, list_rel, etc but not equality *) |
927 => resolve_tac (rsp_rules_get ctxt) THEN_ALL_NEW quotient_tac ctxt |
936 => resolve_tac (rsp_rules_get ctxt) THEN_ALL_NEW quotient_tac ctxt |