Mercurial Mercurial > hg > nominal2 / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
FSet.thy
changeset 379 57bde65f6eb2
parent 376 e99c0334d8bf
child 384 7f8b5ff303f4 
--- a/FSet.thy	Wed Nov 25 10:52:21 2009 +0100
+++ b/FSet.thy	Wed Nov 25 11:41:42 2009 +0100
@@ -176,8 +176,6 @@
 term fmap
 thm fmap_def
 
-ML {* prop_of @{thm fmap_def} *}
-
 ML {* val defs = @{thms EMPTY_def IN_def FUNION_def CARD_def INSERT_def fmap_def FOLD_def} *}
 
 lemma memb_rsp:
@@ -303,8 +301,6 @@
   @{thms ho_memb_rsp ho_cons_rsp ho_card1_rsp ho_map_rsp ho_append_rsp ho_fold_rsp}
   @ @{thms ho_all_prs ho_ex_prs} *}
 
-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 {* val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data @{context} qty *}
 ML {* val (trans2, reps_same, absrep, quot) = lookup_quot_thms @{context} "fset"; *}
 ML {* val consts = lookup_quot_consts defs *}
@@ -378,9 +374,6 @@
 
 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 *}
 
 ML {* val aps = findaps rty (prop_of (atomize_thm @{thm list.recs(2)})) *}
@@ -397,9 +390,6 @@
 
 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 {* 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 *})
@@ -417,100 +407,14 @@
   done
 
 
-
-(* Construction site starts here *)
-
+ML {* fun r_mk_comb_tac_fset lthy = r_mk_comb_tac lthy rty quot rel_refl trans2 rsp_thms *}
 
-ML {* val consts = lookup_quot_consts 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" *}
-
-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,
-      atac,
-      rtac @{thm universal_twice},
-      (rtac @{thm impI} THEN' atac),
-      rtac @{thm implication_twice},
-      //comented out  rtac @{thm equality_twice}, //
-      EqSubst.eqsubst_tac ctxt [0]
-        [(@{thm equiv_res_forall} OF [rel_eqv]),
-         (@{thm equiv_res_exists} OF [rel_eqv])],
-      (rtac @{thm impI} THEN' (asm_full_simp_tac (Simplifier.context ctxt HOL_ss)) THEN' rtac rel_refl),
-      (rtac @{thm RIGHT_RES_FORALL_REGULAR})
-     ]; *}
-  apply (atomize(full))
-  apply (tactic {* REPEAT_ALL_NEW (tac @{context}) 1 *})
-  done  *)
-ML {* val t_r = regularize t_a rty rel rel_eqv rel_refl @{context} *}
-ML {*
-  val rt = build_repabs_term @{context} t_r consts rty qty
-  val rg = Logic.mk_equals ((Thm.prop_of t_r), rt);
-*}
-prove {* Syntax.check_term @{context} rg *}
-ML_prf {* fun r_mk_comb_tac_fset lthy = r_mk_comb_tac lthy rty quot rel_refl trans2 rsp_thms *}
-apply(atomize(full))
-apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *})
-done
-ML {*
-val t_t = repabs @{context} t_r consts rty qty quot rel_refl trans2 rsp_thms
-*}
-
-ML {* val abs = findabs rty (prop_of (t_a)) *}
-ML {* val aps = findaps rty (prop_of (t_a)) *}
-ML {* val lam_prs_thms = map (make_simp_prs_thm @{context} quot @{thm LAMBDA_PRS}) abs *}
-ML {* val app_prs_thms = map (applic_prs @{context} rty qty absrep) aps *}
-ML {* val lam_prs_thms = map Thm.varifyT lam_prs_thms *}
-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_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 {* val t_d = repeat_eqsubst_thm @{context} defs_sym t_id *}
-ML allthms
-thm FORALL_PRS
-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 {* 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 gla = atomize_goal @{theory} gl *}
-
-prove t_r: {* mk_REGULARIZE_goal @{context} (prop_of t_a) gla *}
-
-ML_prf {*  fun tac ctxt = FIRST' [
-      rtac rel_refl,
-      atac,
-      rtac @{thm universal_twice},
-      (rtac @{thm impI} THEN' atac),
-      rtac @{thm implication_twice},
-      (*rtac @{thm equality_twice},*)
-      EqSubst.eqsubst_tac ctxt [0]
-        [(@{thm equiv_res_forall} OF [rel_eqv]),
-         (@{thm equiv_res_exists} OF [rel_eqv])],
-      (rtac @{thm impI} THEN' (asm_full_simp_tac (Simplifier.context ctxt HOL_ss)) THEN' rtac rel_refl),
-      (rtac @{thm RIGHT_RES_FORALL_REGULAR})
-     ]; *}
-
-  apply (atomize(full))
-  apply (tactic {* REPEAT_ALL_NEW (tac @{context}) 1 *})
-  done
-
-ML {* val t_r = @{thm t_r} OF [t_a] *}
-
-ML {* val ttt = mk_inj_REPABS_goal @{context} (prop_of t_r, gla) *}
-ML {* val si = simp_ids_trm (cterm_of @{theory} ttt) *}
-prove t_t: {* term_of si *}
-ML_prf {* fun r_mk_comb_tac_fset lthy = r_mk_comb_tac lthy rty quot rel_refl trans2 rsp_thms *}
-apply(atomize(full))
+(* Construction site starts here *)
+lemma "P (x :: 'a list) (EMPTY :: 'a fset) \<Longrightarrow> (\<And>e t. P x t \<Longrightarrow> P x (INSERT e t)) \<Longrightarrow> P x l"
+apply (tactic {* procedure_tac @{thm list_induct_part} @{context} 1 *})
+apply (tactic {* regularize_tac @{context} rel_eqv rel_refl 1 *})
 apply (tactic {* (APPLY_RSP_TAC rty @{context}) 1 *})
 apply (rule FUN_QUOTIENT)
 apply (rule FUN_QUOTIENT)
@@ -579,13 +483,7 @@
 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
+apply (tactic {* clean_tac @{context} quot defs reps_same 1 *})
 done
 
-thm t_t
-ML {* val t_t = @{thm Pure.equal_elim_rule1} OF [@{thm t_t}, t_r] *}
-ML {* val t_l = repeat_eqsubst_thm @{context} (lam_prs_thms) t_t *}
-ML {* val t_d = repeat_eqsubst_thm @{context} defs_sym t_l *}
-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 *}
-
 end
nominal2