# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1257253461 -3600
# Node ID 5f3b364d476554f9fa1dfd6821608db932d87d34
# Parent  59578f428bbe6b3f825af5c994f7044699cadf9e
Preparing infrastructure for general FORALL_PRS

diff -r 59578f428bbe -r 5f3b364d4765 LamEx.thy
--- a/LamEx.thy	Mon Nov 02 15:38:03 2009 +0100
+++ b/LamEx.thy	Tue Nov 03 14:04:21 2009 +0100
@@ -280,17 +280,79 @@
 *)
 
 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 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 thm = 
+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 simp_app_prs_thms = map (make_simp_prs_thm @{context} quot @{thm APP_PRS}) 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 defs_sym = add_lower_defs @{context} defs; *}
 ML {* val defs_sym_eq = map (fn x => eq_reflection OF [x]) defs_sym *}
 ML t_l