equal
deleted
inserted
replaced
1100 (Conv.params_conv ~1 (fn ctxt => |
1100 (Conv.params_conv ~1 (fn ctxt => |
1101 (Conv.prems_conv ~1 (lambda_prs_conv ctxt quot) then_conv |
1101 (Conv.prems_conv ~1 (lambda_prs_conv ctxt quot) then_conv |
1102 Conv.concl_conv ~1 (lambda_prs_conv ctxt quot))) ctxt) i) |
1102 Conv.concl_conv ~1 (lambda_prs_conv ctxt quot))) ctxt) i) |
1103 *} |
1103 *} |
1104 |
1104 |
|
1105 (* |
|
1106 Cleaning the theorem consists of 5 kinds of rewrites. |
|
1107 These rewrites can be done independently and in any order. |
|
1108 |
|
1109 - LAMBDA_PRS: |
|
1110 (Rep1 ---> Abs2) (\<lambda>x. Rep2 (?f (Abs1 x))) \<equiv> ?f |
|
1111 - Rewriting with definitions from the argument defs |
|
1112 (Abs) OldConst (Rep Args) \<equiv> NewConst Args |
|
1113 - QUOTIENT_REL_REP: |
|
1114 Rel (Rep x) (Rep y) \<equiv> x = y |
|
1115 - FORALL_PRS (and the same for exists: EXISTS_PRS) |
|
1116 \<forall>x\<in>Respects R. (abs ---> id) ?f \<equiv> \<forall>x. ?f |
|
1117 - applic_prs |
|
1118 Abs1 ((Abs2 --> Rep1) f (Rep2 args)) \<equiv> f args |
|
1119 |
|
1120 The first one is implemented as a conversion (fast). |
|
1121 The second and third one are a simp_tac (fast). |
|
1122 The last two are EqSubst (slow). |
|
1123 *) |
1105 ML {* |
1124 ML {* |
1106 fun clean_tac lthy quot defs aps = |
1125 fun clean_tac lthy quot defs aps = |
1107 let |
1126 let |
1108 val lower = flat (map (add_lower_defs lthy) defs) |
1127 val lower = flat (map (add_lower_defs lthy) defs) |
1109 val meta_lower = map (fn x => @{thm eq_reflection} OF [x]) lower |
1128 val meta_lower = map (fn x => @{thm eq_reflection} OF [x]) lower |