equal
deleted
inserted
replaced
1060 \<forall>x\<in>Respects R. (abs ---> id) f ----> \<forall>x. f |
1060 \<forall>x\<in>Respects R. (abs ---> id) f ----> \<forall>x. f |
1061 |
1061 |
1062 - Rewriting with definitions from the argument defs |
1062 - Rewriting with definitions from the argument defs |
1063 NewConst ----> (rep ---> abs) oldConst |
1063 NewConst ----> (rep ---> abs) oldConst |
1064 |
1064 |
1065 - Quotient_REL_REP: |
1065 - Quotient_rel_rep: |
1066 Rel (Rep x) (Rep y) ----> x = y |
1066 Rel (Rep x) (Rep y) ----> x = y |
1067 |
1067 |
1068 - ABS_REP |
1068 - ABS_REP |
1069 Abs (Rep x) ----> x |
1069 Abs (Rep x) ----> x |
1070 |
1070 |
1080 let |
1080 let |
1081 val thy = ProofContext.theory_of lthy; |
1081 val thy = ProofContext.theory_of lthy; |
1082 val quotients = quotient_rules_get lthy |
1082 val quotients = quotient_rules_get lthy |
1083 val defs = map (Thm.varifyT o #def) (qconsts_dest thy); |
1083 val defs = map (Thm.varifyT o #def) (qconsts_dest thy); |
1084 val absrep = map (fn x => @{thm Quotient_abs_rep} OF [x]) quotients |
1084 val absrep = map (fn x => @{thm Quotient_abs_rep} OF [x]) quotients |
1085 val meta_absrep = map (fn x => @{thm eq_reflection} OF [x]) absrep; |
1085 val reps_same = map (fn x => @{thm Quotient_rel_rep} OF [x]) quotients |
1086 val reps_same = map (fn x => @{thm Quotient_REL_REP} OF [x]) quotients |
|
1087 val meta_reps_same = map (fn x => @{thm eq_reflection} OF [x]) reps_same |
|
1088 val simp_ctxt = (Simplifier.context lthy empty_ss) addsimps |
1086 val simp_ctxt = (Simplifier.context lthy empty_ss) addsimps |
1089 (@{thm eq_reflection[OF fun_map.simps]} :: @{thms id_simps} @ meta_absrep @ meta_reps_same @ defs) |
1087 (@{thm eq_reflection[OF fun_map.simps]} :: @{thms id_simps} @ absrep @ reps_same @ defs) |
1090 in |
1088 in |
1091 EVERY' [ |
1089 EVERY' [ |
1092 (* (Rep1 ---> Abs2) (\<lambda>x. Rep2 (f (Abs1 x))) ----> f *) |
1090 (* (Rep1 ---> Abs2) (\<lambda>x. Rep2 (f (Abs1 x))) ----> f *) |
1093 (* \<forall>x\<in>Respects R. (abs ---> id) f ----> \<forall>x. f *) |
1091 (* \<forall>x\<in>Respects R. (abs ---> id) f ----> \<forall>x. f *) |
1094 NDT lthy "a" (TRY o lambda_allex_prs_tac lthy), |
1092 NDT lthy "a" (TRY o lambda_allex_prs_tac lthy), |