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 213 7610d2bbca48
parent 212 ca9eae5bd871
parent 211 80859cc80332
child 214 a66f81c264aa 
--- a/FSet.thy	Wed Oct 28 01:48:45 2009 +0100
+++ b/FSet.thy	Wed Oct 28 01:49:31 2009 +0100
@@ -187,8 +187,20 @@
 *}
 
 ML {* val fset_defs = @{thms EMPTY_def IN_def UNION_def card_def INSERT_def fmap_def fold_def} *}
+
+ML {*
+fun add_lower_defs ctxt defs =
+  let
+    val defs_pre_sym = map symmetric defs
+    val defs_atom = map atomize_thm defs_pre_sym
+    val defs_all = flat (map (add_lower_defs_aux ctxt) defs_atom)
+  in
+    map Thm.varifyT defs_all
+  end
+*}
 ML {* val fset_defs_sym = add_lower_defs @{context} fset_defs *}
 
+
 lemma memb_rsp:
   fixes z
   assumes a: "list_eq x y"
@@ -295,7 +307,7 @@
 (* The all_prs and ex_prs should be proved for the instance... *)
 ML {*
 fun r_mk_comb_tac_fset ctxt =
-  r_mk_comb_tac ctxt @{thm QUOTIENT_fset} @{thm list_eq_refl} @{thm QUOT_TYPE_I_fset.R_trans2}
+  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})
 *}
 
@@ -304,6 +316,15 @@
 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})
+*}
+
+
 ML {* trm_r *}
 prove list_induct_tr: trm_r
 apply (atomize(full))
@@ -339,27 +360,6 @@
 lemma id_apply2 [simp]: "id x \<equiv> x"
   by (simp add: id_def)
 
-ML {*
-   val lpis = @{thm LAMBDA_PRS} OF [@{thm QUOTIENT_fset}, @{thm IDENTITY_QUOTIENT}];
-   val lpist = @{thm "HOL.sym"} OF [lpis];
-   val lam_prs = MetaSimplifier.rewrite_rule [@{thm id_apply2}] lpist
-*}
-
-text {* the proper way to do it *}
-ML {*
-  fun findabs rty tm =
-    case tm of
-      Abs(_, T, b) =>
-        let
-          val b' = subst_bound ((Free ("x", T)), b);
-          val tys = findabs rty b'
-          val ty = fastype_of tm
-        in if needs_lift rty ty then (ty :: tys) else tys
-        end
-    | f $ a => (findabs rty f) @ (findabs rty a)
-    | _ => []
-*}
-
 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 *}
@@ -370,10 +370,9 @@
     handle _ => thm
 *}
 
-ML {* val m2_t' = eqsubst_thm @{context} [lam_prs] @{thm m2_t} *}
+ML {* val m2_t' = simp_lam_prs @{context} @{thm m2_t} *}
 
 ML {* val ithm = simp_allex_prs @{context} quot m2_t' *}
-ML fset_defs_sym
 
 ML {* val rthm = MetaSimplifier.rewrite_rule fset_defs_sym ithm *}
 ML {* ObjectLogic.rulify rthm *}
@@ -408,8 +407,9 @@
 
 thm fold1.simps(2)
 thm list.recs(2)
+thm map_append
 
-ML {* val ind_r_a = atomize_thm @{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} *}
   ML_prf {*  fun tac ctxt =
        (asm_full_simp_tac ((Simplifier.context ctxt HOL_ss) addsimps
@@ -423,33 +423,20 @@
   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
 apply(atomize(full))
 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *})
-apply (auto)
 done
 
-ML {* val (g, thm, othm) =
+ML {* val ind_r_t =
   Toplevel.program (fn () =>
-  repabs_eq @{context} ind_r_r consts @{typ "'a list"} @{typ "'a fset"}
+  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})
   )
 *}
-ML {*
-    fun tac2 ctxt =
-     (simp_tac ((Simplifier.context ctxt empty_ss) addsimps [symmetric thm]))
-     THEN' (rtac othm); *}
-(* ML {*    val cthm = Goal.prove @{context} [] [] g (fn x => tac2 (#context x) 1);
-*} *)
-
-ML {*
-  val ind_r_t2 =
-  Toplevel.program (fn () =>
-    repabs_eq2 @{context} (g, thm, othm)
-  )
-*}
-ML {* val ind_r_l = simp_lam_prs @{context} ind_r_t2 *}
+ML {* val ind_r_l = simp_lam_prs @{context} 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
@@ -458,13 +445,10 @@
 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 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 {* hd fset_defs_sym *}
-ML {* val ind_r_d = MetaSimplifier.rewrite_rule fset_defs_sym ind_r_a1 *}
+ML {* val ind_r_d = repeat_eqsubst_thm @{context} 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 *}
 
@@ -473,14 +457,13 @@
 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 (g, t, ot) =
-    repabs_eq @{context} ind_r_r consts @{typ "'a list"} @{typ "'a fset"}
+  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} @ @{thms ho_all_prs ho_ex_prs});
-  val ind_r_t = repabs_eq2 @{context} (g, t, ot);
+     (@{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} ind_r_l;
-  val ind_r_d = MetaSimplifier.rewrite_rule fset_defs_sym ind_r_a;
+  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
@@ -488,15 +471,19 @@
 *}
 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 append_assoc} *} *)
+ML {* lift @{thm map_append} *}
+ML {* lift @{thm eq_r[OF append_assoc]} *}
 
-thm 
+thm
 
 
 (*notation ( output) "prop" ("#_" [1000] 1000) *)
nominal2