905 | (Const (@{const_name fun_rel}, _) $ _ $ _) $ |
905 | (Const (@{const_name fun_rel}, _) $ _ $ _) $ |
906 (Const(@{const_name Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $ |
906 (Const(@{const_name Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $ |
907 (Const(@{const_name Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _) |
907 (Const(@{const_name Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _) |
908 => rtac @{thm fun_rel_id} THEN' quot_true_tac ctxt unlam |
908 => rtac @{thm fun_rel_id} THEN' quot_true_tac ctxt unlam |
909 |
909 |
|
910 | (_ $ |
|
911 (Const(@{const_name Babs},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $ |
|
912 (Const(@{const_name Babs},_) $ (Const (@{const_name Respects}, _) $ _) $ _)) |
|
913 => rtac @{thm babs_rsp} THEN' RANGE [quotient_tac ctxt] |
|
914 |
910 (* reflexivity of operators arising from Cong_tac *) |
915 (* reflexivity of operators arising from Cong_tac *) |
911 | Const (@{const_name "op ="},_) $ _ $ _ |
916 | Const (@{const_name "op ="},_) $ _ $ _ |
912 => rtac @{thm refl} ORELSE' |
917 => rtac @{thm refl} ORELSE' |
913 (resolve_tac trans2 THEN' RANGE [ |
918 (resolve_tac trans2 THEN' RANGE [ |
914 quot_true_tac ctxt (fst o dest_bcomb), quot_true_tac ctxt (snd o dest_bcomb)]) |
919 quot_true_tac ctxt (fst o dest_bcomb), quot_true_tac ctxt (snd o dest_bcomb)]) |
991 val tyinst = map (SOME o (ctyp_of thy)) [ty_a, ty_b, ty_c, ty_d] |
996 val tyinst = map (SOME o (ctyp_of thy)) [ty_a, ty_b, ty_c, ty_d] |
992 val tinst = [NONE, NONE, SOME (cterm_of thy r1), NONE, SOME (cterm_of thy a2)] |
997 val tinst = [NONE, NONE, SOME (cterm_of thy r1), NONE, SOME (cterm_of thy a2)] |
993 val lpi = Drule.instantiate' tyinst tinst @{thm lambda_prs} |
998 val lpi = Drule.instantiate' tyinst tinst @{thm lambda_prs} |
994 val te = @{thm eq_reflection} OF [solve_quotient_assums ctxt (solve_quotient_assums ctxt lpi)] |
999 val te = @{thm eq_reflection} OF [solve_quotient_assums ctxt (solve_quotient_assums ctxt lpi)] |
995 val ts = MetaSimplifier.rewrite_rule @{thms id_simps} te |
1000 val ts = MetaSimplifier.rewrite_rule @{thms id_simps} te |
|
1001 val _ = tracing ("te rule:\n" ^ (Syntax.string_of_term ctxt (prop_of te))); |
996 val tl = Thm.lhs_of ts |
1002 val tl = Thm.lhs_of ts |
997 val (insp, inst) = make_inst (term_of tl) (term_of ctrm) |
1003 val (insp, inst) = make_inst (term_of tl) (term_of ctrm) |
998 val ti = Drule.instantiate ([], [(cterm_of thy insp, cterm_of thy inst)]) ts |
1004 val ti = Drule.instantiate ([], [(cterm_of thy insp, cterm_of thy inst)]) ts |
999 val _ = if not (s = @{const_name "id"}) then |
1005 val _ = if not (s = @{const_name "id"}) then |
1000 (tracing "lambda_prs"; |
1006 (tracing "lambda_prs"; |