--- a/FSet.thy	Wed Oct 28 16:48:57 2009 +0100
+++ b/FSet.thy	Wed Oct 28 17:17:21 2009 +0100
@@ -167,18 +167,6 @@
 term fmap
 thm fmap_def
 
-ML {* val fset_defs = @{thms EMPTY_def IN_def UNION_def card_def INSERT_def fmap_def fold_def} *}
-(* ML {* val consts = map (fst o dest_Const o fst o Logic.dest_equals o concl_of) fset_defs *} *)
-
-ML {*
-  val consts = [@{const_name "Nil"}, @{const_name "Cons"},
-                @{const_name "membship"}, @{const_name "card1"},
-                @{const_name "append"}, @{const_name "fold1"},
-                @{const_name "map"}];
-*}
-
-ML {* val fset_defs_sym = add_lower_defs @{context} fset_defs *}
-
 lemma memb_rsp:
   fixes z
   assumes a: "list_eq x y"
@@ -293,136 +281,43 @@
   ((map f a) ::'a list) @ (map f b)"
  by simp (rule list_eq_refl)
 
-thm list.induct
-lemma list_induct_hol4:
-  fixes P :: "'a list \<Rightarrow> bool"
-  assumes a: "((P []) \<and> (\<forall>t. (P t) \<longrightarrow> (\<forall>h. (P (h # t)))))"
-  shows "\<forall>l. (P l)"
-  using a
-  apply (rule_tac allI)
-  apply (induct_tac "l")
-  apply (simp)
-  apply (metis)
-  done
-
-ML {* (atomize_thm @{thm list_induct_hol4}) *}
-
-ML {* regularise (prop_of (atomize_thm @{thm list_induct_hol4})) @{typ "'a list"} @{term "op \<approx>"} @{context} *}
-
-prove list_induct_r: {*
-   build_regularize_goal (atomize_thm @{thm list_induct_hol4}) @{typ "'a list"} @{term "op \<approx>"} @{context} *}
-  apply (simp only: equiv_res_forall[OF equiv_list_eq])
-  thm RIGHT_RES_FORALL_REGULAR
-  apply (rule RIGHT_RES_FORALL_REGULAR)
-  prefer 2
-  apply (assumption)
-  apply (metis)
-  done
-
-(* The all_prs and ex_prs should be proved for the instance... *)
+ML {* val rty = @{typ "'a list"} *}
+ML {* val qty = @{typ "'a fset"} *}
+ML {* val rel = @{term "list_eq"} *}
+ML {* val rel_eqv = (#equiv_thm o hd) (quotdata_lookup @{context}) *}
+ML {* val rel_refl = @{thm list_eq_refl} *}
+ML {* val quot = @{thm QUOTIENT_fset} *}
+ML {* val rsp_thms =
+  @{thms ho_memb_rsp ho_cons_rsp ho_card1_rsp ho_map_rsp ho_append_rsp}
+  @ @{thms ho_all_prs ho_ex_prs} *}
+ML {* val trans2 = @{thm QUOT_TYPE_I_fset.R_trans2} *}
+ML {* val reps_same = @{thm QUOT_TYPE_I_fset.REPS_same} *}
+ML {* val defs = @{thms EMPTY_def IN_def UNION_def card_def INSERT_def fmap_def fold_def} *}
+(* ML {* val consts = map (fst o dest_Const o fst o Logic.dest_equals o concl_of) fset_defs *} *)
 ML {*
-fun r_mk_comb_tac_fset ctxt =
-  r_mk_comb_tac ctxt @{typ "'a list"} @{thm QUOTIENT_fset} @{thm list_eq_refl} @{thm QUOT_TYPE_I_fset.R_trans2}
-  (@{thms ho_memb_rsp ho_cons_rsp ho_card1_rsp ho_map_rsp ho_append_rsp} @ @{thms ho_all_prs ho_ex_prs})
-*}
-
-
-ML {* val thm = @{thm list_induct_r} OF [atomize_thm @{thm list_induct_hol4}] *}
-ML {* val trm_r = build_repabs_goal @{context} thm consts @{typ "'a list"} @{typ "'a fset"} *}
-ML {* val trm = build_repabs_term @{context} thm consts @{typ "'a list"} @{typ "'a fset"} *}
-
-ML {* val rty = @{typ "'a list"} *}
-
-ML {*
-fun r_mk_comb_tac_fset ctxt =
-  r_mk_comb_tac ctxt rty @{thm QUOTIENT_fset} @{thm list_eq_refl} @{thm QUOT_TYPE_I_fset.R_trans2}
-  (@{thms ho_memb_rsp ho_cons_rsp ho_card1_rsp ho_map_rsp ho_append_rsp} @ @{thms ho_all_prs ho_ex_prs})
+  val consts = [@{const_name "Nil"}, @{const_name "Cons"},
+                @{const_name "membship"}, @{const_name "card1"},
+                @{const_name "append"}, @{const_name "fold1"},
+                @{const_name "map"}];
 *}
 
-
-ML {* trm_r *}
-prove list_induct_tr: trm_r
-apply (atomize(full))
-apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *})
-done
-
-prove list_induct_t: trm
-apply (simp only: list_induct_tr[symmetric])
-apply (tactic {* rtac thm 1 *})
-done
-
-thm m2
-ML {* atomize_thm @{thm m2} *}
-
-prove m2_r_p: {*
-   build_regularize_goal (atomize_thm @{thm m2}) @{typ "'a List.list"} @{term "op \<approx>"} @{context} *}
-  apply (simp add: equiv_res_forall[OF equiv_list_eq])
-done
-
-ML {* val m2_r = @{thm m2_r_p} OF [atomize_thm @{thm m2}] *}
-ML {* val m2_t_g = build_repabs_goal @{context} m2_r consts @{typ "'a list"} @{typ "'a fset"} *}
-ML {* val m2_t = build_repabs_term @{context} m2_r consts @{typ "'a list"} @{typ "'a fset"} *}
-prove m2_t_p: m2_t_g
-apply (atomize(full))
-apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *})
-done
-
-prove m2_t: m2_t
-apply (simp only: m2_t_p[symmetric])
-apply (tactic {* rtac m2_r 1 *})
-done
-
-lemma id_apply2 [simp]: "id x \<equiv> x"
-  by (simp add: id_def)
-
-ML {* val quot = @{thm QUOTIENT_fset} *}
-ML {* val abs = findabs @{typ "'a list"} (prop_of (atomize_thm @{thm list_induct_hol4})) *}
-ML {* val simp_lam_prs_thms = map (make_simp_lam_prs_thm @{context} quot) abs *}
-
-ML {*
-  fun simp_lam_prs lthy thm =
-    simp_lam_prs lthy (eqsubst_thm lthy simp_lam_prs_thms thm)
-    handle _ => thm
+ML {* fun lift_thm_fset lthy t =
+  lift_thm lthy consts rty qty rel rel_eqv rel_refl quot rsp_thms trans2 reps_same defs t
 *}
 
-ML {* val m2_t' = simp_lam_prs @{context} @{thm m2_t} *}
-
-ML {* val ithm = simp_allex_prs @{context} quot m2_t' *}
-
-ML {* val rthm = MetaSimplifier.rewrite_rule fset_defs_sym ithm *}
-ML {* ObjectLogic.rulify rthm *}
-
-
-ML {* val card1_suc_a = atomize_thm @{thm card1_suc} *}
-
-prove card1_suc_r_p: {*
-   build_regularize_goal (atomize_thm @{thm card1_suc}) @{typ "'a List.list"} @{term "op \<approx>"} @{context} *}
-  apply (simp add: equiv_res_forall[OF equiv_list_eq] equiv_res_exists[OF equiv_list_eq])
-done
+lemma eq_r: "a = b \<Longrightarrow> a \<approx> b"
+by (simp add: list_eq_refl)
 
-ML {* val card1_suc_r = @{thm card1_suc_r_p} OF [atomize_thm @{thm card1_suc}] *}
-ML {* val card1_suc_t_g = build_repabs_goal @{context} card1_suc_r consts @{typ "'a list"} @{typ "'a fset"} *}
-ML {* val card1_suc_t = build_repabs_term @{context} card1_suc_r consts @{typ "'a list"} @{typ "'a fset"} *}
-prove card1_suc_t_p: card1_suc_t_g
-apply (atomize(full))
-apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *})
-done
-
-prove card1_suc_t: card1_suc_t
-apply (simp only: card1_suc_t_p[symmetric])
-apply (tactic {* rtac card1_suc_r 1 *})
-done
-
-ML {* val card1_suc_t_n = @{thm card1_suc_t} *}
-ML {* val card1_suc_t' = simp_lam_prs @{context} @{thm card1_suc_t} *}
-ML {* val ithm = simp_allex_prs @{context} quot card1_suc_t' *}
-ML {* val rthm = MetaSimplifier.rewrite_rule fset_defs_sym ithm *}
-ML {* val qthm = MetaSimplifier.rewrite_rule @{thms QUOT_TYPE_I_fset.REPS_same} rthm *}
-ML {* ObjectLogic.rulify qthm *}
+ML {* lift_thm_fset @{context} @{thm m1} *}
+ML {* lift_thm_fset @{context} @{thm m2} *}
+ML {* lift_thm_fset @{context} @{thm list_eq.intros(4)} *}
+ML {* lift_thm_fset @{context} @{thm list_eq.intros(5)} *}
+ML {* lift_thm_fset @{context} @{thm card1_suc} *}
+ML {* lift_thm_fset @{context} @{thm map_append} *}
+ML {* lift_thm_fset @{context} @{thm eq_r[OF append_assoc]} *}
 
 thm fold1.simps(2)
 thm list.recs(2)
-thm map_append
 
 ML {* val ind_r_a = atomize_thm @{thm list.induct} *}
 (*  prove {* build_regularize_goal ind_r_a @{typ "'a List.list"} @{term "op \<approx>"} @{context} *}
@@ -438,12 +333,10 @@
   val rt = build_repabs_term @{context} ind_r_r consts @{typ "'a list"} @{typ "'a fset"}
   val rg = Logic.mk_equals ((Thm.prop_of ind_r_r), rt);
 *}
-
-prove rg
+(*prove rg
 apply(atomize(full))
 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *})
-done
-
+done*)
 ML {* val ind_r_t =
   Toplevel.program (fn () =>
   repabs @{context} ind_r_r consts @{typ "'a list"} @{typ "'a fset"}
@@ -451,7 +344,9 @@
    (@{thms ho_memb_rsp ho_cons_rsp ho_card1_rsp ho_map_rsp ho_append_rsp} @ @{thms ho_all_prs ho_ex_prs})
   )
 *}
-ML {* val ind_r_l = simp_lam_prs @{context} ind_r_t *}
+ML {* val abs = findabs rty (prop_of (atomize_thm @{thm list.induct})) *}
+ML {* val simp_lam_prs_thms = map (make_simp_lam_prs_thm @{context} quot) abs *}
+ML {* val ind_r_l = repeat_eqsubst_thm @{context} simp_lam_prs_thms ind_r_t *}
 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
@@ -463,100 +358,30 @@
 ML {* val ind_r_a = simp_allex_prs @{context} quot ind_r_l4 *}
 ML {* val thm = @{thm 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 = repeat_eqsubst_thm @{context} fset_defs_sym ind_r_a1 *}
+ML {* val defs_sym = add_lower_defs @{context} defs *}
+ML {* val ind_r_d = repeat_eqsubst_thm @{context} 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
-  val ind_r_a = atomize_thm thm;
-  val ind_r_r = regularize ind_r_a @{typ "'a List.list"} @{term "op \<approx>"} @{thm equiv_list_eq} @{context};
-  val ind_r_t =
-    repabs @{context} ind_r_r consts @{typ "'a list"} @{typ "'a fset"}
-     @{thm QUOTIENT_fset} @{thm list_eq_refl} @{thm QUOT_TYPE_I_fset.R_trans2}
-     (@{thms ho_memb_rsp ho_cons_rsp  ho_card1_rsp ho_map_rsp ho_append_rsp} @ @{thms ho_all_prs ho_ex_prs});
-  val ind_r_l = simp_lam_prs @{context} ind_r_t;
-  val ind_r_a = simp_allex_prs @{context} quot ind_r_l;
-  val ind_r_d = repeat_eqsubst_thm @{context} fset_defs_sym ind_r_a;
-  val ind_r_s = MetaSimplifier.rewrite_rule @{thms QUOT_TYPE_I_fset.REPS_same} ind_r_d
-in
-  ObjectLogic.rulify ind_r_s
-end
-*}
-ML fset_defs
-
-lemma eq_r: "a = b \<Longrightarrow> a \<approx> b"
-by (simp add: list_eq_refl)
-
-
-ML {* lift @{thm m2} *}
-ML {* lift @{thm m1} *}
-ML {* lift @{thm list_eq.intros(4)} *}
-ML {* lift @{thm list_eq.intros(5)} *}
-ML {* lift @{thm card1_suc} *}
-ML {* lift @{thm map_append} *}
-ML {* lift @{thm eq_r[OF append_assoc]} *}
-
-thm
-
-
-(*notation ( output) "prop" ("#_" [1000] 1000) *)
-notation ( output) "Trueprop" ("#_" [1000] 1000)
-
-(*
-ML {*
-  fun lift_theorem_fset_aux thm lthy =
+  fun lift_thm_fset_note name thm lthy =
     let
-      val ((_, [novars]), lthy2) = Variable.import true [thm] lthy;
-      val goal = build_repabs_goal @{context} novars consts @{typ "'a list"} @{typ "'a fset"};
-      val cgoal = cterm_of @{theory} goal;
-      val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite true fset_defs_sym cgoal);
-      val tac = transconv_fset_tac' @{context};
-      val cthm = Goal.prove_internal [] cgoal2 (fn _ => tac);
-      val nthm = MetaSimplifier.rewrite_rule [symmetric cthm] (snd (no_vars (Context.Theory @{theory}, thm)))
-      val nthm2 = MetaSimplifier.rewrite_rule @{thms QUOT_TYPE_I_fset.REPS_same QUOT_TYPE_I_fset.thm10} nthm;
-      val [nthm3] = ProofContext.export lthy2 lthy [nthm2]
-    in
-      nthm3
-    end
-*}
-*)
-
-(*
-ML {* lift_theorem_fset_aux @{thm m1} @{context} *}
-ML {*
-  fun lift_theorem_fset name thm lthy =
-    let
-      val lifted_thm = lift_theorem_fset_aux thm lthy;
+      val lifted_thm = lift_thm_fset lthy thm;
       val (_, lthy2) = note (name, lifted_thm) lthy;
     in
       lthy2
     end;
 *}
-*)
 
-local_setup {* lift_theorem_fset @{binding "m1_lift"} @{thm m1} *}
-local_setup {* lift_theorem_fset @{binding "leqi4_lift"} @{thm list_eq.intros(4)} *}
-local_setup {* lift_theorem_fset @{binding "leqi5_lift"} @{thm list_eq.intros(5)} *}
-local_setup {* lift_theorem_fset @{binding "m2_lift"} @{thm m2} *}
-thm m1_lift
-thm leqi4_lift
-thm leqi5_lift
-thm m2_lift
-ML {* @{thm card1_suc_r} OF [card1_suc_f] *}
-(*ML {* Toplevel.program (fn () => lift_theorem_fset @{binding "card_suc"}
-     (@{thm card1_suc_r} OF [card1_suc_f]) @{context}) *}*)
-(*local_setup {* lift_theorem_fset @{binding "card_suc"} @{thm card1_suc} *}*)
-
-thm leqi4_lift
-ML {*
-  val (nam, typ) = hd (Term.add_vars (prop_of @{thm leqi4_lift}) [])
-  val (_, l) = dest_Type typ
-  val t = Type ("FSet.fset", l)
-  val v = Var (nam, t)
-  val cv = cterm_of @{theory} ((term_of @{cpat "REP_fset"}) $ v)
+local_setup {*
+  lift_thm_fset_note @{binding "m1l"} @{thm m1} #>
+  lift_thm_fset_note @{binding "m2l"} @{thm m2} #>
+  lift_thm_fset_note @{binding "leqi4l"} @{thm list_eq.intros(4)} #>
+  lift_thm_fset_note @{binding "leqi5l"} @{thm list_eq.intros(5)}
 *}
-
+thm m1l
+thm m2l
+thm leqi4l
+thm leqi5l
 
 end

--- a/Unused.thy	Wed Oct 28 16:48:57 2009 +0100
+++ b/Unused.thy	Wed Oct 28 17:17:21 2009 +0100
@@ -1,3 +1,5 @@
+(*notation ( output) "prop" ("#_" [1000] 1000) *)
+notation ( output) "Trueprop" ("#_" [1000] 1000)
 
 ML {*
   fun dest_cbinop t =
@@ -72,3 +74,15 @@
 lemma trueprop_cong:
   shows "(a ≡ b) ⟹ (Trueprop a ≡ Trueprop b)"
   by auto
+
+lemma list_induct_hol4:
+  fixes P :: "'a list ⇒ bool"
+  assumes a: "((P []) ∧ (∀t. (P t) ⟶ (∀h. (P (h # t)))))"
+  shows "∀l. (P l)"
+  using a
+  apply (rule_tac allI)
+  apply (induct_tac "l")
+  apply (simp)
+  apply (metis)
+  done
+