--- 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