# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1256398167 -7200
# Node ID 945786a68ec6f9419f27ad0c7ae7186abd8282eb
# Parent  3a8978c335f06d963714fb39ac38c152a66ed724
Finally lifted induction, with some manually added simplification lemmas.

diff -r 3a8978c335f0 -r 945786a68ec6 FSet.thy
--- a/FSet.thy	Sat Oct 24 16:15:33 2009 +0200
+++ b/FSet.thy	Sat Oct 24 17:29:27 2009 +0200
@@ -18,7 +18,7 @@
 get_fun repF @{typ t} @{typ qt} @{context} @{typ "((((qt \<Rightarrow> qt) \<Rightarrow> qt) \<Rightarrow> qt) list) * nat"}
  |> fst
  |> Syntax.string_of_term @{context}
- |> writeln*)
+ |> writeln
 *}
 
 ML {*
@@ -617,13 +617,21 @@
   )
 *}
 ML {* val ind_r_l = simp_lam_prs @{context} ind_r_t2 *}
-ML {* val ind_r_a = simp_allex_prs @{context} ind_r_l *}
-ML {* val ind_r_d = MetaSimplifier.rewrite_rule fset_defs_sym ind_r_a *}
-ML {* val ind_r_s = MetaSimplifier.rewrite_rule @{thms QUOT_TYPE_I_fset.REPS_same} ind_r_d *}
 lemma app_prs_for_induct: "(ABS_fset ---> id) f (REP_fset T1) = f T1"
   apply (simp add: fun_map.simps QUOT_TYPE_I_fset.thm10)
 done
 
+ML {* val ind_r_l1 = eqsubst_thm @{context} @{thms app_prs_for_induct} ind_r_l *}
+ML {* val ind_r_l2 = eqsubst_thm @{context} @{thms app_prs_for_induct} ind_r_l1 *}
+ML {* val ind_r_l3 = eqsubst_thm @{context} @{thms app_prs_for_induct} ind_r_l2 *}
+ML {* val ind_r_l4 = eqsubst_thm @{context} @{thms app_prs_for_induct} ind_r_l3 *}
+ML {* val ind_r_a = simp_allex_prs @{context} ind_r_l4 *}
+ML {* val thm = @{thm spec[OF FORALL_PRS[OF FUN_QUOTIENT[OF QUOTIENT_fset IDENTITY_QUOTIENT]],symmetric]} *}
+ML {* val ind_r_a1 = eqsubst_thm @{context} [thm] ind_r_a *}
+ML {* val ind_r_d = MetaSimplifier.rewrite_rule fset_defs_sym ind_r_a1 *}
+ML {* val ind_r_s = MetaSimplifier.rewrite_rule @{thms QUOT_TYPE_I_fset.REPS_same} ind_r_d *}
+ML {* ObjectLogic.rulify ind_r_s *}
+
 ML {*
 fun lift thm =
 let