--- a/LamEx.thy Tue Nov 03 14:04:45 2009 +0100
+++ b/LamEx.thy Tue Nov 03 16:17:19 2009 +0100
@@ -282,81 +282,17 @@
ML {* val t_t = repabs @{context} t_r consts rty qty quot rel_refl trans2 rsp_thms *}
ML {* val abs = findabs rty (prop_of (atomize_thm @{thm alpha.induct})) *}
ML {* val aps = findaps rty (prop_of (atomize_thm @{thm alpha.induct})) *}
-ML {* prop_of (atomize_thm @{thm alpha.induct}) *}
-ML {*
- fun findall_all rty qty tm =
- case tm of
- Const (@{const_name All}, T) $ (s as (Abs(_, _, b))) =>
- let
- val tys = findall_all rty qty s
- in if needs_lift rty T then
- (( T) :: tys)
- else tys end
- | Abs(_, T, b) =>
- findall_all rty qty (subst_bound ((Free ("x", T)), b))
- | f $ a => (findall_all rty qty f) @ (findall_all rty qty a)
- | _ => [];
- fun findall rty qty tm =
- map domain_type (
- map (old_exchange_ty rty qty)
- (distinct (op =) (findall_all rty qty tm))
- )
-*}
-ML {* val alls = findall rty qty (prop_of (atomize_thm @{thm alpha.induct})) *}
-
-ML {*
-fun make_simp_all_prs_thm lthy quot_thm thm typ =
- let
- val (_, [lty, rty]) = dest_Type typ;
- val thy = ProofContext.theory_of lthy;
- val (lcty, rcty) = (ctyp_of thy lty, ctyp_of thy rty)
- val inst = [NONE, SOME lcty];
- val lpi = Drule.instantiate' inst [] thm;
- val tac =
- (compose_tac (false, lpi, 1)) THEN_ALL_NEW
- (quotient_tac quot_thm);
- val gc = Drule.strip_imp_concl (cprop_of lpi);
- val t = Goal.prove_internal [] gc (fn _ => tac 1)
- in
- MetaSimplifier.rewrite_rule [@{thm eq_reflection} OF @{thms id_apply}] t
- end
-*}
+ML {* val (alls, exs) = findallex rty qty (prop_of (atomize_thm @{thm alpha.induct})) *}
+ML {* val allthms = map (make_allex_prs_thm @{context} quot @{thm FORALL_PRS} ) alls *}
+ML {* val exthms = map (make_allex_prs_thm @{context} quot @{thm EXISTS_PRS} ) exs *}
+ML {* val t_a = MetaSimplifier.rewrite_rule allthms t_t *}
ML {* val simp_app_prs_thms = map (make_simp_prs_thm @{context} quot @{thm APP_PRS}) aps *}
-ML {* val aps = @{typ "LamEx.rlam \<Rightarrow> bool"} :: aps; *}
ML {* val simp_lam_prs_thms = map (make_simp_prs_thm @{context} quot @{thm LAMBDA_PRS}) abs *}
-ML {* val t_l = repeat_eqsubst_thm @{context} (simp_app_prs_thms @ simp_lam_prs_thms) t_a *}
-ML {* val typ = hd (alls) *}
-
-
-ML {*
- val (_, [lty, rty]) = dest_Type typ;
- val thy = @{theory};
- val (lcty, rcty) = (ctyp_of thy lty, ctyp_of thy rty)
- val inst = [NONE, SOME lcty];
- val lpi = Drule.instantiate' inst [] @{thm FORALL_PRS};
- val tac =
- (compose_tac (false, lpi, 1)) THEN_ALL_NEW
- (quotient_tac quot);
- val gc = Drule.strip_imp_concl (cprop_of lpi);
-*}
-prove tst: {*term_of gc*}
-apply (tactic {*compose_tac (false, lpi, 1) 1 *})
-apply (tactic {*quotient_tac quot 1 *})
-done
-thm tst
-
-
-
-
-
-ML {* val thms = (make_simp_all_prs_thm @{context} quot @{thm FORALL_PRS} o domain_type) (hd (rev alls)) *}
-ML {* val thm =
- @{thm FORALL_PRS[OF FUN_QUOTIENT[OF QUOTIENT_lam FUN_QUOTIENT[OF QUOTIENT_lam IDENTITY_QUOTIENT]]]} *}
-ML {* val t_a = simp_allex_prs quot [thm] t_t *}
+ML {* val t_l = repeat_eqsubst_thm @{context} (simp_lam_prs_thms) t_a *}
+ML {* val t_l1 = repeat_eqsubst_thm @{context} simp_app_prs_thms t_l *}
ML {* val defs_sym = add_lower_defs @{context} defs; *}
ML {* val defs_sym_eq = map (fn x => eq_reflection OF [x]) defs_sym *}
-ML t_l
-ML {* val t_d0 = MetaSimplifier.rewrite_rule defs_sym_eq t_l *}
+ML {* val t_d0 = MetaSimplifier.rewrite_rule defs_sym_eq t_l1 *}
ML {* val t_d = repeat_eqsubst_thm @{context} defs_sym t_d0 *}
ML {* val t_r = MetaSimplifier.rewrite_rule [reps_same] t_d *}
ML {* val t_r1 = repeat_eqsubst_thm @{context} @{thms fun_map.simps} t_r *}