LamEx.thy
changeset 267 3764566c1151
parent 265 5f3b364d4765
child 268 4d58c02289ca
child 269 fe6eb116b341
--- 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 *}