145 declare [[map * = (prod_fun, prod_rel)]] |
145 declare [[map * = (prod_fun, prod_rel)]] |
146 declare [[map "fun" = (fun_map, fun_rel)]] |
146 declare [[map "fun" = (fun_map, fun_rel)]] |
147 |
147 |
148 lemmas [quotient_thm] = |
148 lemmas [quotient_thm] = |
149 fun_quotient list_quotient |
149 fun_quotient list_quotient |
|
150 |
|
151 lemmas [quotient_rsp] = |
|
152 quot_rel_rsp |
150 |
153 |
151 ML {* maps_lookup @{theory} "List.list" *} |
154 ML {* maps_lookup @{theory} "List.list" *} |
152 ML {* maps_lookup @{theory} "*" *} |
155 ML {* maps_lookup @{theory} "*" *} |
153 ML {* maps_lookup @{theory} "fun" *} |
156 ML {* maps_lookup @{theory} "fun" *} |
154 |
157 |
979 | (Const (@{const_name fun_rel}, _) $ _ $ _) $ |
982 | (Const (@{const_name fun_rel}, _) $ _ $ _) $ |
980 (Const(@{const_name Ball},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $ |
983 (Const(@{const_name Ball},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $ |
981 (Const(@{const_name Ball},_) $ (Const (@{const_name Respects}, _) $ _) $ _) |
984 (Const(@{const_name Ball},_) $ (Const (@{const_name Respects}, _) $ _) $ _) |
982 => rtac @{thm fun_rel_id} THEN' quot_true_tac ctxt unlam |
985 => rtac @{thm fun_rel_id} THEN' quot_true_tac ctxt unlam |
983 (* (op =) (Bex\<dots>) (Bex\<dots>) ----> (op =) (\<dots>) (\<dots>) *) |
986 (* (op =) (Bex\<dots>) (Bex\<dots>) ----> (op =) (\<dots>) (\<dots>) *) |
|
987 | (Const (@{const_name fun_rel}, _) $ _ $ _) $ |
|
988 (Const (@{const_name fun_rel}, _) $ _ $ _) $ |
|
989 (Const (@{const_name fun_rel}, _) $ _ $ _) |
|
990 => rtac @{thm quot_rel_rsp} THEN_ALL_NEW quotient_tac ctxt |
|
991 | (Const (@{const_name fun_rel}, _) $ _ $ _) $ (Const _) $ (Const _) => |
|
992 (* respectfulness of constants; in particular of a simple relation *) |
|
993 resolve_tac (rsp_rules_get ctxt) THEN_ALL_NEW quotient_tac ctxt |
984 | Const (@{const_name "op ="},_) $ |
994 | Const (@{const_name "op ="},_) $ |
985 (Const(@{const_name Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $ |
995 (Const(@{const_name Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $ |
986 (Const(@{const_name Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _) |
996 (Const(@{const_name Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _) |
987 => rtac @{thm bex_rsp} THEN' dtac @{thm QT_ex} |
997 => rtac @{thm bex_rsp} THEN' dtac @{thm QT_ex} |
988 (* (R1 ===> op =) (Bex\<dots>) (Bex\<dots>) ----> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> (Bex\<dots>x) = (Bex\<dots>y) *) |
998 (* (R1 ===> op =) (Bex\<dots>) (Bex\<dots>) ----> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> (Bex\<dots>x) = (Bex\<dots>y) *) |
1018 NDT ctxt "C" (rtac @{thm ext} THEN' quot_true_tac ctxt unlam), |
1028 NDT ctxt "C" (rtac @{thm ext} THEN' quot_true_tac ctxt unlam), |
1019 (* resolving with R x y assumptions *) |
1029 (* resolving with R x y assumptions *) |
1020 NDT ctxt "E" (atac), |
1030 NDT ctxt "E" (atac), |
1021 (* reflexivity of the basic relations *) |
1031 (* reflexivity of the basic relations *) |
1022 (* R \<dots> \<dots> *) |
1032 (* R \<dots> \<dots> *) |
1023 NDT ctxt "D" (resolve_tac rel_refl), |
1033 NDT ctxt "D" (resolve_tac rel_refl) |
1024 (* respectfulness of constants *) |
|
1025 NDT ctxt "7" (resolve_tac (rsp_rules_get ctxt)) |
|
1026 ]) |
1034 ]) |
1027 *} |
1035 *} |
1028 |
1036 |
1029 ML {* |
1037 ML {* |
1030 fun all_inj_repabs_tac ctxt rel_refl trans2 = |
1038 fun all_inj_repabs_tac ctxt rel_refl trans2 = |