# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1257871385 -3600
# Node ID e741c735b867991a54efac8a42f1b9bdd7ff6f9e
# Parent  991b0e53f9dc83e6fad1fcd23ce701bb0a28ebd0
Atomizing a "goal" theorems.

diff -r 991b0e53f9dc -r e741c735b867 FSet.thy
--- a/FSet.thy	Tue Nov 10 09:32:16 2009 +0100
+++ b/FSet.thy	Tue Nov 10 17:43:05 2009 +0100
@@ -349,22 +349,26 @@
 ML {* map (lift_thm_fset @{context}) @{thms list.recs} *}
 ML {* map (lift_thm_fset @{context}) @{thms list.cases} *}
 
-
-
-
-
+lemma list_induct_part:
+  assumes a: "P (x :: 'a list) ([] :: 'a list)"
+  assumes b: "\<And>e t. P x t \<Longrightarrow> P x (e # t)"
+  shows "P x l"
+  apply (rule_tac P="P x" in list.induct)
+  apply (rule a)
+  apply (rule b)
+  apply (assumption)
+  done
 
 
 (* Construction site starts here *)
 
 
 ML {* val consts = lookup_quot_consts defs *}
-ML {* val defs_sym = flat (map (add_lower_defs @{context}) defs) *}
 ML {* val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data @{context} qty *}
 ML {* val (trans2, reps_same, absrep, quot) = lookup_quot_thms @{context} "fset" *}
 
 thm list.recs(2)
-ML {* val t_a = atomize_thm @{thm list.recs(2)} *}
+ML {* val t_a = atomize_thm @{thm list_induct_part} *}
 (* prove {* build_regularize_goal t_a rty rel @{context}  *}
  ML_prf {*  fun tac ctxt = FIRST' [
       rtac rel_refl,
@@ -407,22 +411,30 @@
 ML {* t_t *}
 ML {* val (alls, exs) = findallex @{context} rty qty (prop_of t_a); *}
 ML {* val allthms = map (make_allex_prs_thm @{context} quot @{thm FORALL_PRS}) alls *}
-ML {* val t_a = MetaSimplifier.rewrite_rule (allthms) t_t *}
-ML {* val t_l0 = repeat_eqsubst_thm @{context} (app_prs_thms) t_a *}
-ML {* val iitt = Drule.eta_contraction_rule (hd (tl lam_prs_thms)) *}
-ML {* val iitt = (hd (lam_prs_thms)) *}
-
-ML {* val t_l0 = repeat_eqsubst_thm @{context} [iitt] t_a *}
-ML {* val t_l0 = repeat_eqsubst_thm @{context} ([hd (tl lam_prs_thms)]) t_a *}
+ML {* val t_l0 = repeat_eqsubst_thm @{context} (app_prs_thms) t_t *}
+ML app_prs_thms
 ML {* val t_l = repeat_eqsubst_thm @{context} (lam_prs_thms) t_l0 *}
+ML lam_prs_thms
+ML {* val t_id = simp_ids @{context} t_l *}
+thm INSERT_def
 ML {* val defs_sym = flat (map (add_lower_defs @{context}) defs) *}
-ML t_l0
-ML {* val t_id = simp_ids @{context} t_l0 *}
 ML {* val t_d = repeat_eqsubst_thm @{context} defs_sym t_id *}
-ML {* val t_l = repeat_eqsubst_thm @{context} (lam_prs_thms) t_d *}
+ML allthms
+thm FORALL_PRS
+ML {* val t_a = MetaSimplifier.rewrite_rule (allthms) t_d *}
+ML {* val t_s = MetaSimplifier.rewrite_rule @{thms QUOT_TYPE_I_fset.REPS_same} t_a *}
+ML {* ObjectLogic.rulify t_s *}
+
+ML {* Type.freeze *}
 
-ML {* val t_s = MetaSimplifier.rewrite_rule @{thms QUOT_TYPE_I_fset.REPS_same} t_d *}
-ML {* ObjectLogic.rulify t_s *}
+ML {* val gl = @{term "P (x :: 'a list) (EMPTY :: 'a fset) \<Longrightarrow> (\<And>e t. P x t \<Longrightarrow> P x (INSERT e t)) \<Longrightarrow> P x l"} *}
+ML {* val vars = map Free (Term.add_frees gl []) *}
+ML {* fun lambda_all (var as Free(_, T)) trm = (Term.all T) $ lambda var trm *}
+ML {* val gla = fold lambda_all vars gl *}
+ML {* val glf = Type.freeze gla *}
+ML {* val glac = (snd o Thm.dest_equals o cprop_of) (ObjectLogic.atomize (cterm_of @{theory} glf)) *}
+ML {* val allsym = map symmetric allthms *}
+ML {* val t_a = (snd o Thm.dest_equals o cprop_of) (MetaSimplifier.rewrite true allsym glac) *}
 
 ML {*
   fun lift_thm_fset_note name thm lthy =