199 end |
199 end |
200 *} |
200 *} |
201 |
201 |
202 section {* infrastructure about id *} |
202 section {* infrastructure about id *} |
203 |
203 |
204 (* Need to have a meta-equality *) |
|
205 |
|
206 lemma id_def_sym: "(\<lambda>x. x) \<equiv> id" |
|
207 by (simp add: id_def) |
|
208 |
|
209 (* TODO: can be also obtained with: *) |
|
210 ML {* symmetric (eq_reflection OF @{thms id_def}) *} |
|
211 |
|
212 lemma prod_fun_id: "prod_fun id id \<equiv> id" |
204 lemma prod_fun_id: "prod_fun id id \<equiv> id" |
213 by (rule eq_reflection) (simp add: prod_fun_def) |
205 by (rule eq_reflection) (simp add: prod_fun_def) |
214 |
206 |
215 lemma map_id: "map id \<equiv> id" |
207 lemma map_id: "map id \<equiv> id" |
216 apply (rule eq_reflection) |
208 apply (rule eq_reflection) |
217 apply (rule ext) |
209 apply (rule ext) |
218 apply (rule_tac list="x" in list.induct) |
210 apply (rule_tac list="x" in list.induct) |
219 apply (simp_all) |
211 apply (simp_all) |
220 done |
212 done |
221 |
213 |
222 lemmas id_simps = |
214 lemmas id_simps = |
223 FUN_MAP_I[THEN eq_reflection] |
215 FUN_MAP_I[THEN eq_reflection] |
224 id_apply[THEN eq_reflection] |
216 id_apply[THEN eq_reflection] |
225 id_def_sym prod_fun_id map_id |
217 id_def[THEN eq_reflection,symmetric] |
|
218 prod_fun_id map_id |
226 |
219 |
227 ML {* |
220 ML {* |
228 fun simp_ids thm = |
221 fun simp_ids thm = |
229 MetaSimplifier.rewrite_rule @{thms id_simps} thm |
222 MetaSimplifier.rewrite_rule @{thms id_simps} thm |
230 *} |
223 *} |
903 val largs = map2 mk_rep (raty ~~ qaty) args; |
896 val largs = map2 mk_rep (raty ~~ qaty) args; |
904 val lhs = mk_abs (rgty, qgty) (list_comb((mk_rep (raty ---> rgty, qaty ---> qgty) f), largs)); |
897 val lhs = mk_abs (rgty, qgty) (list_comb((mk_rep (raty ---> rgty, qaty ---> qgty) f), largs)); |
905 val llhs = Syntax.check_term lthy lhs; |
898 val llhs = Syntax.check_term lthy lhs; |
906 val eq = Logic.mk_equals (llhs, rhs); |
899 val eq = Logic.mk_equals (llhs, rhs); |
907 val ceq = cterm_of (ProofContext.theory_of lthy') eq; |
900 val ceq = cterm_of (ProofContext.theory_of lthy') eq; |
908 val sctxt = HOL_ss addsimps (absrep :: @{thms fun_map.simps map_id id_apply}); |
901 val sctxt = HOL_ss addsimps (absrep :: @{thms fun_map.simps id_simps}); |
909 val t = Goal.prove_internal [] ceq (fn _ => simp_tac sctxt 1) |
902 val t = Goal.prove_internal [] ceq (fn _ => simp_tac sctxt 1) |
910 val t_id = MetaSimplifier.rewrite_rule @{thms eq_reflection[OF id_apply] id_def_sym} t; |
903 val t_id = MetaSimplifier.rewrite_rule @{thms id_simps} t; |
911 (* FIXME/TODO: should that be id_simps? *) |
|
912 in |
904 in |
913 singleton (ProofContext.export lthy' lthy) t_id |
905 singleton (ProofContext.export lthy' lthy) t_id |
914 end |
906 end |
915 *} |
907 *} |
916 |
|
917 ML {* |
|
918 fun findaps_all rty tm = |
|
919 case tm of |
|
920 Abs(_, T, b) => |
|
921 findaps_all rty (subst_bound ((Free ("x", T)), b)) |
|
922 | (f $ a) => (findaps_all rty f @ findaps_all rty a) |
|
923 | Free (_, (T as (Type ("fun", (_ :: _))))) => |
|
924 (if needs_lift rty T then [T] else []) |
|
925 | _ => []; |
|
926 fun findaps rty tm = distinct (op =) (findaps_all rty tm) |
|
927 *} |
|
928 |
|
929 |
908 |
930 ML {* |
909 ML {* |
931 fun find_aps_all rtm qtm = |
910 fun find_aps_all rtm qtm = |
932 case (rtm, qtm) of |
911 case (rtm, qtm) of |
933 (Abs(_, T1, s1), Abs(_, T2, s2)) => |
912 (Abs(_, T1, s1), Abs(_, T2, s2)) => |
943 |
922 |
944 fun find_aps rtm qtm = distinct (op =) (find_aps_all rtm qtm) |
923 fun find_aps rtm qtm = distinct (op =) (find_aps_all rtm qtm) |
945 *} |
924 *} |
946 |
925 |
947 ML {* |
926 ML {* |
948 (* FIXME: allex_prs and lambda_prs can be one function *) |
|
949 fun allex_prs_tac lthy quot = |
927 fun allex_prs_tac lthy quot = |
950 (EqSubst.eqsubst_tac lthy [0] @{thms FORALL_PRS[symmetric] EXISTS_PRS[symmetric]}) |
928 (EqSubst.eqsubst_tac lthy [0] @{thms FORALL_PRS[symmetric] EXISTS_PRS[symmetric]}) |
951 THEN' (quotient_tac quot); |
929 THEN' (quotient_tac quot); |
952 *} |
930 *} |
953 |
931 |
986 (compose_tac (false, lpi, 2)) THEN_ALL_NEW |
964 (compose_tac (false, lpi, 2)) THEN_ALL_NEW |
987 (quotient_tac quot); |
965 (quotient_tac quot); |
988 val gc = Drule.strip_imp_concl (cprop_of lpi); |
966 val gc = Drule.strip_imp_concl (cprop_of lpi); |
989 val t = Goal.prove_internal [] gc (fn _ => tac 1) |
967 val t = Goal.prove_internal [] gc (fn _ => tac 1) |
990 val te = @{thm eq_reflection} OF [t] |
968 val te = @{thm eq_reflection} OF [t] |
991 val ts = MetaSimplifier.rewrite_rule [@{thm eq_reflection} OF @{thms id_apply}] te |
969 val ts = MetaSimplifier.rewrite_rule @{thms id_simps} te |
992 val tl = Thm.lhs_of ts |
970 val tl = Thm.lhs_of ts |
993 (* val _ = tracing (Syntax.string_of_term @{context} (term_of ctrm));*) |
971 (* val _ = tracing (Syntax.string_of_term @{context} (term_of ctrm));*) |
994 (* val _ = tracing (Syntax.string_of_term @{context} (term_of tl));*) |
972 (* val _ = tracing (Syntax.string_of_term @{context} (term_of tl));*) |
995 val insts = matching_prs (ProofContext.theory_of ctxt) (term_of tl) (term_of ctrm); |
973 val insts = matching_prs (ProofContext.theory_of ctxt) (term_of tl) (term_of ctrm); |
996 val ti = Drule.eta_contraction_rule (Drule.instantiate insts ts); |
974 val ti = Drule.eta_contraction_rule (Drule.instantiate insts ts); |