147 |
147 |
148 lemmas [quotient_thm] = |
148 lemmas [quotient_thm] = |
149 fun_quotient list_quotient |
149 fun_quotient list_quotient |
150 |
150 |
151 lemmas [quotient_rsp] = |
151 lemmas [quotient_rsp] = |
152 quot_rel_rsp |
152 quot_rel_rsp nil_rsp cons_rsp |
153 |
153 |
154 ML {* maps_lookup @{theory} "List.list" *} |
154 ML {* maps_lookup @{theory} "List.list" *} |
155 ML {* maps_lookup @{theory} "*" *} |
155 ML {* maps_lookup @{theory} "*" *} |
156 ML {* maps_lookup @{theory} "fun" *} |
156 ML {* maps_lookup @{theory} "fun" *} |
157 |
157 |
982 | (Const (@{const_name fun_rel}, _) $ _ $ _) $ |
982 | (Const (@{const_name fun_rel}, _) $ _ $ _) $ |
983 (Const(@{const_name Ball},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $ |
983 (Const(@{const_name Ball},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $ |
984 (Const(@{const_name Ball},_) $ (Const (@{const_name Respects}, _) $ _) $ _) |
984 (Const(@{const_name Ball},_) $ (Const (@{const_name Respects}, _) $ _) $ _) |
985 => rtac @{thm fun_rel_id} THEN' quot_true_tac ctxt unlam |
985 => rtac @{thm fun_rel_id} THEN' quot_true_tac ctxt unlam |
986 (* (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 |
|
994 | Const (@{const_name "op ="},_) $ |
987 | Const (@{const_name "op ="},_) $ |
995 (Const(@{const_name Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $ |
988 (Const(@{const_name Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $ |
996 (Const(@{const_name Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _) |
989 (Const(@{const_name Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _) |
997 => rtac @{thm bex_rsp} THEN' dtac @{thm QT_ex} |
990 => rtac @{thm bex_rsp} THEN' dtac @{thm QT_ex} |
998 (* (R1 ===> op =) (Bex\<dots>) (Bex\<dots>) ----> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> (Bex\<dots>x) = (Bex\<dots>y) *) |
991 (* (R1 ===> op =) (Bex\<dots>) (Bex\<dots>) ----> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> (Bex\<dots>x) = (Bex\<dots>y) *) |
1003 | Const (@{const_name "op ="},_) $ _ $ _ => |
996 | Const (@{const_name "op ="},_) $ _ $ _ => |
1004 (* reflexivity of operators arising from Cong_tac *) |
997 (* reflexivity of operators arising from Cong_tac *) |
1005 rtac @{thm refl} ORELSE' |
998 rtac @{thm refl} ORELSE' |
1006 (resolve_tac trans2 THEN' RANGE [ |
999 (resolve_tac trans2 THEN' RANGE [ |
1007 quot_true_tac ctxt (fst o dest_bcomb), quot_true_tac ctxt (snd o dest_bcomb)]) |
1000 quot_true_tac ctxt (fst o dest_bcomb), quot_true_tac ctxt (snd o dest_bcomb)]) |
|
1001 | (Const (@{const_name fun_rel}, _) $ _ $ _) $ |
|
1002 (Const (@{const_name fun_rel}, _) $ _ $ _) $ |
|
1003 (Const (@{const_name fun_rel}, _) $ _ $ _) |
|
1004 => rtac @{thm quot_rel_rsp} THEN_ALL_NEW quotient_tac ctxt |
|
1005 | _ $ (Const _) $ (Const _) => (* fun_rel, list_rel, etc but not equality *) |
|
1006 (* respectfulness of constants; in particular of a simple relation *) |
|
1007 resolve_tac (rsp_rules_get ctxt) THEN_ALL_NEW quotient_tac ctxt |
1008 | _ $ _ $ _ => |
1008 | _ $ _ $ _ => |
1009 (* R (\<dots>) (Rep (Abs \<dots>)) ----> R (\<dots>) (\<dots>) *) |
1009 (* R (\<dots>) (Rep (Abs \<dots>)) ----> R (\<dots>) (\<dots>) *) |
1010 (* observe ---> *) |
1010 (* observe ---> *) |
1011 rep_abs_rsp_tac ctxt |
1011 rep_abs_rsp_tac ctxt |
1012 | _ => error "inj_repabs_tac not a relation" |
1012 | _ => error "inj_repabs_tac not a relation" |