# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1259154934 -3600
# Node ID 7f8b5ff303f4e52a431ff1a260440e3333af4ecd
# Parent  7ccbf4e2eb18415a684ebebafbea3a8100bbc79a
Finished manual lifting of list_induct_part :)

diff -r 7ccbf4e2eb18 -r 7f8b5ff303f4 FSet.thy
--- a/FSet.thy	Wed Nov 25 11:59:49 2009 +0100
+++ b/FSet.thy	Wed Nov 25 14:15:34 2009 +0100
@@ -411,6 +411,57 @@
 
 
 
+
+ML {*
+fun lambda_prs_conv1 ctxt quot ctrm =
+  case (term_of ctrm) of ((Const (@{const_name "fun_map"}, _) $ r1 $ a2) $ (Abs _)) =>
+  let
+    val (_, [ty_b, ty_a]) = dest_Type (fastype_of r1);
+    val (_, [ty_c, ty_d]) = dest_Type (fastype_of a2);
+    val thy = ProofContext.theory_of ctxt;
+    val [cty_a, cty_b, cty_c, cty_d] = map (ctyp_of thy) [ty_a, ty_b, ty_c, ty_d]
+    val tyinst = [SOME cty_a, SOME cty_b, SOME cty_c, SOME cty_d];
+    val tinst = [NONE, NONE, SOME (cterm_of thy r1), NONE, SOME (cterm_of thy a2)]
+    val lpi = Drule.instantiate' tyinst tinst @{thm LAMBDA_PRS};
+    val tac =
+      (compose_tac (false, lpi, 2)) THEN_ALL_NEW
+      (quotient_tac quot);
+    val gc = Drule.strip_imp_concl (cprop_of lpi);
+    val t = Goal.prove_internal [] gc (fn _ => tac 1)
+    val te = @{thm eq_reflection} OF [t]
+    val ts = MetaSimplifier.rewrite_rule [@{thm eq_reflection} OF @{thms id_apply}] te
+    val tl = Thm.lhs_of ts
+    val _ = tracing (Syntax.string_of_term @{context} (term_of ctrm));
+    val _ = tracing (Syntax.string_of_term @{context} (term_of tl));
+    val insts = matching_prs (ProofContext.theory_of ctxt) (term_of tl) (term_of ctrm);
+    val ti = Drule.eta_contraction_rule (Drule.instantiate insts ts);
+(*    val _ = tracing (Syntax.string_of_term @{context} (term_of (cprop_of ti)));*)
+  in
+    Conv.rewr_conv ti ctrm
+  end
+  handle _ => Conv.all_conv ctrm
+
+*}
+ML {*
+fun lambda_prs_conv ctxt quot ctrm =
+  case (term_of ctrm) of
+    (Const (@{const_name "fun_map"}, _) $ r1 $ a2) $ (Abs (_, _, x)) =>
+      (Conv.arg_conv (Conv.abs_conv (fn (_, ctxt) => lambda_prs_conv ctxt quot) ctxt)
+      then_conv (lambda_prs_conv1 ctxt quot)) ctrm
+  | _ $ _ => Conv.comb_conv (lambda_prs_conv ctxt quot) ctrm
+  | Abs _ => Conv.abs_conv (fn (_, ctxt) => lambda_prs_conv ctxt quot) ctxt ctrm
+  | _ => Conv.all_conv ctrm
+*}
+
+ML {*
+fun lambda_prs_tac ctxt quot = CSUBGOAL (fn (goal, i) =>
+  CONVERSION
+    (Conv.params_conv ~1 (fn ctxt =>
+       (Conv.prems_conv ~1 (lambda_prs_conv ctxt quot) then_conv
+          Conv.concl_conv ~1 (lambda_prs_conv ctxt quot))) ctxt) i)
+*}
+
+
 (* Construction site starts here *)
 lemma "P (x :: 'a list) (EMPTY :: 'a fset) \<Longrightarrow> (\<And>e t. P x t \<Longrightarrow> P x (INSERT e t)) \<Longrightarrow> P x l"
 apply (tactic {* procedure_tac @{thm list_induct_part} @{context} 1 *})
@@ -483,7 +534,14 @@
 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
-apply (tactic {* clean_tac @{context} quot defs reps_same 1 *})
+apply (simp only:map_id)
+apply (tactic {* REPEAT_ALL_NEW (allex_prs_tac @{context} quot) 1 *})
+ML_prf {* val lower = flat (map (add_lower_defs @{context}) defs) *}
+apply (tactic {* REPEAT_ALL_NEW (EqSubst.eqsubst_tac @{context} [0] lower) 1 *})
+apply (tactic {* lambda_prs_tac @{context} quot 1 *})
+ML_prf {* val t = applic_prs @{context} rty qty absrep @{typ "('b \<Rightarrow> 'a list \<Rightarrow> bool)"} *}
+apply (tactic {* REPEAT_ALL_NEW (EqSubst.eqsubst_tac @{context} [0] [t]) 1 *})
+apply (tactic {* simp_tac (HOL_ss addsimps [reps_same]) 1 *})
 done
 
 end