1064 (Conv.prems_conv ~1 (lambda_prs_conv ctxt quot) then_conv |
1064 (Conv.prems_conv ~1 (lambda_prs_conv ctxt quot) then_conv |
1065 Conv.concl_conv ~1 (lambda_prs_conv ctxt quot))) ctxt) i) |
1065 Conv.concl_conv ~1 (lambda_prs_conv ctxt quot))) ctxt) i) |
1066 *} |
1066 *} |
1067 |
1067 |
1068 (* |
1068 (* |
1069 TODO: Update |
1069 Cleaning the theorem consists of 6 kinds of rewrites. |
1070 Cleaning the theorem consists of 5 kinds of rewrites. |
1070 The first two need to be done before fun_map is unfolded |
1071 These rewrites can be done independently and in any order. |
|
1072 |
1071 |
1073 - LAMBDA_PRS: |
1072 - LAMBDA_PRS: |
1074 (Rep1 ---> Abs2) (\<lambda>x. Rep2 (f (Abs1 x))) ----> f |
1073 (Rep1 ---> Abs2) (\<lambda>x. Rep2 (f (Abs1 x))) \<Longrightarrow> f |
|
1074 - FORALL_PRS (and the same for exists: EXISTS_PRS) |
|
1075 \<forall>x\<in>Respects R. (abs ---> id) ?f \<Longrightarrow> \<forall>x. ?f |
1075 - Rewriting with definitions from the argument defs |
1076 - Rewriting with definitions from the argument defs |
1076 (Abs) OldConst (Rep Args) ----> NewConst Args |
1077 NewConst \<Longrightarrow> (rep ---> abs) oldConst |
1077 - QUOTIENT_REL_REP: |
1078 - QUOTIENT_REL_REP: |
1078 Rel (Rep x) (Rep y) ----> x = y |
1079 Rel (Rep x) (Rep y) \<Longrightarrow> x = y |
1079 - FORALL_PRS (and the same for exists: EXISTS_PRS) |
1080 - ABS_REP |
1080 \<forall>x\<in>Respects R. (abs ---> id) f ----> \<forall>x. f |
1081 Abs (Rep x) \<Longrightarrow> x |
1081 - applic_prs |
1082 - id_simps; fun_map.simps |
1082 Abs1 ((Abs2 --> Rep1) f (Rep2 args)) ----> f args |
|
1083 |
1083 |
1084 The first one is implemented as a conversion (fast). |
1084 The first one is implemented as a conversion (fast). |
1085 The second and third one are a simp_tac (fast). |
1085 The second one is an EqSubst (slow). |
1086 The last two are EqSubst (slow). |
1086 The rest are a simp_tac and are fast. |
1087 *) |
1087 *) |
1088 ML {* |
1088 ML {* |
1089 fun clean_tac lthy quot defs aps = |
1089 fun clean_tac lthy quot defs aps = |
1090 let |
1090 let |
1091 val absrep = map (fn x => @{thm QUOTIENT_ABS_REP} OF [x]) quot |
1091 val absrep = map (fn x => @{thm QUOTIENT_ABS_REP} OF [x]) quot |