
diff -r f7dee6e808eb -r e99c0334d8bf FSet.thy
--- a/FSet.thy	Wed Nov 25 03:47:07 2009 +0100
+++ b/FSet.thy	Wed Nov 25 10:34:03 2009 +0100
@@ -337,155 +337,21 @@
 apply (tactic {* lift_tac_fset @{context} @{thm fold1.simps(2)} 1 *})
 done
 
-ML {*
-
-fun lambda_prs_conv ctxt quot ctrm =
-  case (Thm.term_of ctrm) of
-    (Const (@{const_name "fun_map"}, _) $ y $ z) $ (Abs (_, T, x)) =>
-      let
-        val _ = tracing "AAA";
-        val lty = T;
-        val rty = fastype_of x;
-        val thy = ProofContext.theory_of ctxt;
-        val (lcty, rcty) = (ctyp_of thy lty, ctyp_of thy rty)
-        val inst = [SOME lcty, NONE, SOME rcty];
-        val lpi = Drule.instantiate' inst [] @{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 ts = MetaSimplifier.rewrite_rule [@{thm eq_reflection} OF @{thms id_apply}] t
-        val te = @{thm eq_reflection} OF [ts]
-        val _ = tracing (Syntax.string_of_term @{context} (term_of ctrm));
-        val _ = tracing (Syntax.string_of_term @{context} (term_of (Thm.lhs_of te)));
-        val insts = matching_prs (ProofContext.theory_of ctxt) (term_of ctrm) (term_of (Thm.lhs_of te));
-        val ti = Drule.instantiate insts te;
-        val _ = tracing (Syntax.string_of_term @{context} (term_of (cprop_of ti)));
-      in
-        Conv.rewr_conv (eq_reflection OF [ti]) ctrm
-      end
-  | _ $ _ => 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)
-*}
-
-ML {*
-val ctrm = @{cterm "((ABS_fset ---> id) ---> id) (\<lambda>x. id ((REP_fset ---> id) x))"}
-val pat =  @{cpat  "((ABS_fset ---> id) ---> id) (\<lambda>x. ?f ((REP_fset ---> id) x))"}
-*}
-
-ML {* matching_prs @{theory} (term_of pat) (term_of ctrm); *}
-
-ML {*
-  lambda_prs_conv @{context} quot ctrm
-*}
-
-
-ML {* 
-val t = @{thm LAMBDA_PRS[OF FUN_QUOTIENT[OF QUOTIENT_fset IDENTITY_QUOTIENT] IDENTITY_QUOTIENT]}
-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
- *}
-
-ML {* val inst = matching_prs @{theory} (term_of tl) (term_of ctrm); *}
-
-ML {* val trm = @{cterm "(((ABS_fset ---> id) ---> id) (\<lambda>(P\<Colon>('a list \<Rightarrow> bool)).
-              All ((REP_fset ---> id) (\<lambda>(list\<Colon>('a list)).
-                        (ABS_fset ---> id) ((REP_fset ---> id) P) (REP_fset (ABS_fset [])) \<longrightarrow>
-               True \<longrightarrow> (ABS_fset ---> id) ((REP_fset ---> id) P) (REP_fset (ABS_fset list))))))"} *}
-
-ML {*
-  lambda_prs_conv @{context} quot trm
-*}
-
-
-
-(*ML {* val trm = @{cterm "(((ABS_fset ---> id) ---> id) (\<lambda>(?P\<Colon>('a list \<Rightarrow> bool)). (g (id P)"} *} *)
-
-
-
-lemma "\<lbrakk>P EMPTY; \<And>a x. P x \<Longrightarrow> P (INSERT a x)\<rbrakk> \<Longrightarrow> P l"
-apply(tactic {* procedure_tac @{thm list.induct} @{context} 1 *})
-apply(tactic {* regularize_tac @{context} rel_eqv rel_refl 1 *})
-apply(tactic {* REPEAT_ALL_NEW (r_mk_comb_tac @{context} rty quot rel_refl trans2 rsp_thms) 1 *})
-apply(tactic {* REPEAT_ALL_NEW (allex_prs_tac @{context} quot) 1 *})
-apply(tactic {* lambda_prs_tac @{context} quot 1 *})
-
-
-ML_prf {* Subgoal.focus @{context} 1 (#goal (Isar.goal ())) *}
-
-apply (tactic {* lift_tac_fset @{context} @{thm list.induct} 1 *})
-
-
-thm LAMBDA_PRS
-apply(tactic {* EqSubst.eqsubst_tac @{context} [0] @{thms LAMBDA_PRS} 1 *})
-
-apply(tactic {*  (lambda_prs_tac @{context} quot) 1 *})
-
-apply(tactic {* REPEAT_ALL_NEW (lambda_prs_tac @{context} quot) 1 *})
-
-apply(tactic {* clean_tac @{context} quot defs reps_same 1 *})
-apply (tactic {* lift_tac_fset @{context} @{thm list.induct} 1 *})
-ML {* lift_thm_fset @{context} @{thm list.induct} *}
-ML {* lift_thm_g_fset @{context} @{thm list.induct} @{term "\<lbrakk>P EMPTY; \<And>a x. P x \<Longrightarrow> P (INSERT a x)\<rbrakk> \<Longrightarrow> P l"} *}
-
-
-
-
-thm map_append
 lemma "fmap f (FUNION (x::'b fset) (xa::'b fset)) = FUNION (fmap f x) (fmap f xa)"
-apply(tactic {* procedure_tac @{thm map_append} @{context} 1 *})
-apply(tactic {* prepare_tac 1 *})
-thm map_append
 apply (tactic {* lift_tac_fset @{context} @{thm map_append} 1 *})
 done
 
-
-
 lemma "FUNION (FUNION x xa) xb = FUNION x (FUNION xa xb)"
 apply (tactic {* lift_tac_fset @{context} @{thm append_assoc} 1 *})
 done
 
-ML {* atomize_thm @{thm fold1.simps(2)} *}
-(*ML {* lift_thm_g_fset @{context} @{thm fold1.simps(2)} @{term "FOLD f g (z::'b) (INSERT a x) =
-    (if rsp_fold f then if IN a x then FOLD f g z x else f (g a) (FOLD f g z x) else z)"} *}*)
-
-
-*)
-ML {* lift_thm_g_fset @{context} @{thm map_append} @{term "fmap f (FUNION (x::'b fset) (xa::'b fset)) = FUNION (fmap f x) (fmap f xa)"} *}
-
-
-ML {* cterm_of @{theory} (atomize_goal @{theory} @{term "\<forall>x xa a. x = xa \<Longrightarrow> INSERT a x = INSERT a xa"}) *}
-
-
-ML {* lift_thm_fset @{context} @{thm map_append} *}
-
-
-(*
-apply(tactic {* procedure_tac @{thm m1} @{context} 1 *})
-apply(tactic {* regularize_tac @{context} rel_eqv rel_refl 1 *})
-apply(tactic {* REPEAT_ALL_NEW (r_mk_comb_tac @{context} rty quot rel_refl trans2 rsp_thms) 1 *})
-apply(tactic {* clean_tac @{context} quot defs reps_same 1 *})
-apply(tactic {* TRY' (REPEAT_ALL_NEW (allex_prs_tac @{context} quot)) 1 *})
-apply(tactic {* TRY' (REPEAT_ALL_NEW (lambda_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 {* simp_tac (HOL_ss addsimps [reps_same]) 1 *})
-*)
-
-
-
-(*ML {* lift_thm_fset @{context} @{thm neq_Nil_conv} *}*)
+ML {* val aps = findaps rty (prop_of (atomize_thm @{thm list.induct})) *}
+ML {* val app_prs_thms = map (applic_prs @{context} rty qty absrep) aps *}
+lemma "\<lbrakk>P EMPTY; \<And>a x. P x \<Longrightarrow> P (INSERT a x)\<rbrakk> \<Longrightarrow> P l"
+apply (tactic {* lift_tac_fset @{context} @{thm list.induct} 1 *})
+apply (tactic {* REPEAT_ALL_NEW (EqSubst.eqsubst_tac @{context} [0] app_prs_thms) 1 *})
+apply (tactic {* simp_tac (HOL_ss addsimps [reps_same]) 1 *})
+done
 
 quotient_def
   fset_rec::"'a \<Rightarrow> ('b \<Rightarrow> 'b fset \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'b fset \<Rightarrow> 'a"
@@ -510,67 +376,35 @@
   apply (auto simp add: FUN_REL_EQ)
   sorry
 
-
 ML {* val rsp_thms = @{thms list_rec_rsp list_case_rsp} @ rsp_thms *}
 ML {* val defs = @{thms fset_rec_def fset_case_def} @ defs *}
 
 ML {* fun lift_thm_fset lthy t = lift_thm lthy qty "fset" rsp_thms defs t *}
 ML {* fun lift_thm_g_fset lthy t g = lift_thm_goal lthy qty "fset" rsp_thms defs t g *}
+ML {* fun lift_tac_fset lthy t = lift_tac lthy t rel_eqv rel_refl rty quot trans2 rsp_thms reps_same defs *}
 
-thm list.recs(2)
-ML {* lift_thm_fset @{context} @{thm list.recs(2)} *}
-ML {* lift_thm_g_fset @{context} @{thm list.recs(2)} @{term "fset_rec (f1::'t) x (INSERT a xa) = x a xa (fset_rec f1 x xa)"} *}
+ML {* val aps = findaps rty (prop_of (atomize_thm @{thm list.recs(2)})) *}
+ML {* val app_prs_thms = map (applic_prs @{context} rty qty absrep) aps *}
+lemma "fset_rec (f1::'t) x (INSERT a xa) = x a xa (fset_rec f1 x xa)"
+apply (tactic {* lift_tac_fset @{context} @{thm list.recs(2)} 1 *})
+apply (tactic {* REPEAT_ALL_NEW (EqSubst.eqsubst_tac @{context} [0] app_prs_thms) 1 *})
+apply (tactic {* (simp_tac (HOL_ss addsimps
+  @{thms eq_reflection[OF FUN_MAP_I] eq_reflection[OF id_apply] id_def_sym prod_fun_id map_id})) 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 {* simp_tac (HOL_ss addsimps [reps_same]) 1 *})
+done
+
+ML {* val aps = findaps rty (prop_of (atomize_thm @{thm list.cases(2)})) *}
+ML {* val app_prs_thms = map (applic_prs @{context} rty qty absrep) aps *}
 
 
-ML {* val gl = @{term "fset_rec (f1::'t) x (INSERT a xa) = x a xa (fset_rec f1 x xa)"} *}
-ML {* val t_a = atomize_thm @{thm list.recs(2)} *}
-ML {* val qtrm = atomize_goal @{theory} gl *}
-ML {* val rg = cterm_of @{theory}(Syntax.check_term @{context} (REGULARIZE_trm @{context} (prop_of t_a) qtrm)) *}
-ML {* val rg2 = cterm_of @{theory}(my_reg @{context} rel rty (prop_of t_a)) *}
-
-ML {* val t_r = regularize_goal @{context} t_a rel_eqv rel_refl qtrm *}
-ML {* val t_r = regularize t_a rty rel rel_eqv rel_refl @{context} *}
-
-ML {* val rg = cterm_of @{theory}(Syntax.check_term @{context} (inj_REPABS @{context} ((prop_of t_r), qtrm))) *}
-ML {* val rg2 = cterm_of @{theory} (build_repabs_term @{context} t_r consts rty qty) *}
-ML {* val t_t = repabs_goal @{context} t_r rty quot rel_refl trans2 rsp_thms qtrm *}
-ML {* val t_t = repabs @{context} t_r consts rty qty quot rel_refl trans2 rsp_thms *}
-ML {*
-  val lthy = @{context}
-  val (alls, exs) = findallex lthy rty qty (prop_of t_a);
-  val allthms = map (make_allex_prs_thm lthy quot @{thm FORALL_PRS}) alls
-  val exthms = map (make_allex_prs_thm lthy quot @{thm EXISTS_PRS}) exs
-  val t_a = MetaSimplifier.rewrite_rule (allthms @ exthms) t_t
-  val abs = findabs rty (prop_of t_a);
-  val aps = findaps rty (prop_of t_a);
-  val app_prs_thms = map (applic_prs lthy rty qty absrep) aps;
-  val lam_prs_thms = map (make_simp_prs_thm lthy quot @{thm LAMBDA_PRS}) abs;
-  val t_l = repeat_eqsubst_thm lthy (lam_prs_thms @ app_prs_thms) t_a;
-  val defs_sym = flat (map (add_lower_defs lthy) defs);
-  val defs_sym_eq = map (fn x => eq_reflection OF [x]) defs_sym;
-  val t_id = simp_ids lthy t_l;
-  val t_d0 = MetaSimplifier.rewrite_rule defs_sym_eq t_id;
-  val t_d = repeat_eqsubst_thm lthy defs_sym t_d0;
-  val t_r = MetaSimplifier.rewrite_rule [reps_same] t_d;
-  val t_rv = ObjectLogic.rulify t_r
-
-*}
-
-
-
-
-
-
-ML {* map (lift_thm_fset @{context}) @{thms list.cases} *}
-
-
-
-
-ML {* atomize_thm @{thm m1} *}
-ML {* cterm_of @{theory} (atomize_goal @{theory} @{term "IN x EMPTY = False"}) *}
-ML {* lift_thm_fset @{context} @{thm m1} *}
-(* ML {* lift_thm_g_fset @{context} @{thm m1} @{term "IN x EMPTY = False"}) *} *)
-
+ML {* map (lift_thm_fset @{context}) @{thms list.cases(2)} *}
+lemma "fset_case (f1::'t) f2 (INSERT a xa) = f2 a xa"
+apply (tactic {* lift_tac_fset @{context} @{thm list.cases(2)} 1 *})
+apply (tactic {* REPEAT_ALL_NEW (EqSubst.eqsubst_tac @{context} [0] app_prs_thms) 1 *})
+apply (tactic {* simp_tac (HOL_ss addsimps [reps_same]) 1 *})
+done
 
 lemma list_induct_part:
   assumes a: "P (x :: 'a list) ([] :: 'a list)"
@@ -583,6 +417,7 @@
   done
 
 
+
 (* Construction site starts here *)
 
 
@@ -590,7 +425,6 @@
 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_induct_part} *}
 
 
@@ -754,26 +588,4 @@
 ML {* val t_al = MetaSimplifier.rewrite_rule (allthms) t_d *}
 ML {* val t_s = MetaSimplifier.rewrite_rule @{thms QUOT_TYPE_I_fset.REPS_same} t_al *}
 
-
-ML {*
-  fun lift_thm_fset_note name thm lthy =
-    let
-      val lifted_thm = lift_thm_fset lthy thm;
-      val (_, lthy2) = note (name, lifted_thm) lthy;
-    in
-      lthy2
-    end;
-*}
-
-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




