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 187 f8fc085db38f
parent 183 6acf9e001038
child 189 01151c3853ce 
--- a/FSet.thy	Mon Oct 26 02:06:01 2009 +0100
+++ b/FSet.thy	Mon Oct 26 10:02:50 2009 +0100
@@ -218,8 +218,10 @@
   apply(rule list_eq_refl)
 done
 
+(* Need stronger induction... *)
 lemma "(a @ b) \<approx> (b @ a)"
-sorry
+  apply(induct a)
+  sorry
 
 lemma (* ho_append_rsp: *)
   "op \<approx> ===> op \<approx> ===> op \<approx> op @ op @"
@@ -237,23 +239,6 @@
   apply (metis)
   done
 
-ML {*
-fun regularize thm rty rel rel_eqv lthy =
-  let
-    val g = build_regularize_goal thm rty rel lthy;
-    fun tac ctxt =
-       (asm_full_simp_tac ((Simplifier.context ctxt HOL_ss) addsimps
-        [(@{thm equiv_res_forall} OF [rel_eqv]),
-         (@{thm equiv_res_exists} OF [rel_eqv])])) THEN_ALL_NEW
-         (((rtac @{thm RIGHT_RES_FORALL_REGULAR}) THEN' (RANGE [fn _ => all_tac, atac]) THEN'
-         (MetisTools.metis_tac ctxt [])) ORELSE' (MetisTools.metis_tac ctxt []));
-    val cthm = Goal.prove lthy [] [] g (fn x => tac (#context x) 1);
-  in
-    cthm OF [thm]
-  end
-*}
-
-
 prove list_induct_r: {*
    build_regularize_goal (atomize_thm @{thm list_induct_hol4}) @{typ "'a List.list"} @{term "op \<approx>"} @{context} *}
   apply (simp only: equiv_res_forall[OF equiv_list_eq])
@@ -265,94 +250,6 @@
   done
 
 ML {*
-fun instantiate_tac thm = Subgoal.FOCUS (fn {concl, ...} =>
-let
-  val pat = Drule.strip_imp_concl (cprop_of thm)
-  val insts = Thm.match (pat, concl)
-in
-  rtac (Drule.instantiate insts thm) 1
-end
-handle _ => no_tac
-)
-*}
-
-ML {*
-fun res_forall_rsp_tac ctxt =
-  (simp_tac ((Simplifier.context ctxt HOL_ss) addsimps @{thms FUN_REL.simps}))
-  THEN' rtac @{thm allI} THEN' rtac @{thm allI} THEN' rtac @{thm impI}
-  THEN' instantiate_tac @{thm RES_FORALL_RSP} ctxt THEN'
-  (simp_tac ((Simplifier.context ctxt HOL_ss) addsimps @{thms FUN_REL.simps}))
-*}
-
-ML {*
-fun res_exists_rsp_tac ctxt =
-  (simp_tac ((Simplifier.context ctxt HOL_ss) addsimps @{thms FUN_REL.simps}))
-  THEN' rtac @{thm allI} THEN' rtac @{thm allI} THEN' rtac @{thm impI}
-  THEN' instantiate_tac @{thm RES_EXISTS_RSP} ctxt THEN'
-  (simp_tac ((Simplifier.context ctxt HOL_ss) addsimps @{thms FUN_REL.simps}))
-*}
-
-
-ML {*
-fun quotient_tac quot_thm =
-  REPEAT_ALL_NEW (FIRST' [
-    rtac @{thm FUN_QUOTIENT},
-    rtac quot_thm,
-    rtac @{thm IDENTITY_QUOTIENT}
-  ])
-*}
-
-ML {*
-fun LAMBDA_RES_TAC ctxt i st =
-  (case (term_of o #concl o fst) (Subgoal.focus ctxt i st) of
-    (_ $ (_ $ (Abs(_,_,_))$(Abs(_,_,_)))) =>
-      (EqSubst.eqsubst_tac ctxt [0] @{thms FUN_REL.simps}) THEN'
-      (rtac @{thm allI}) THEN' (rtac @{thm allI}) THEN' (rtac @{thm impI})
-  | _ => fn _ => no_tac) i st
-*}
-
-ML {*
-fun WEAK_LAMBDA_RES_TAC ctxt i st =
-  (case (term_of o #concl o fst) (Subgoal.focus ctxt i st) of
-    (_ $ (_ $ _$(Abs(_,_,_)))) =>
-      (EqSubst.eqsubst_tac ctxt [0] @{thms FUN_REL.simps}) THEN'
-      (rtac @{thm allI}) THEN' (rtac @{thm allI}) THEN' (rtac @{thm impI})
-  | (_ $ (_ $ (Abs(_,_,_))$_)) =>
-      (EqSubst.eqsubst_tac ctxt [0] @{thms FUN_REL.simps}) THEN'
-      (rtac @{thm allI}) THEN' (rtac @{thm allI}) THEN' (rtac @{thm impI})
-  | _ => fn _ => no_tac) i st
-*}
-
-
-ML {*
-fun r_mk_comb_tac ctxt quot_thm reflex_thm trans_thm rsp_thms =
-  (FIRST' [
-    rtac @{thm FUN_QUOTIENT},
-    rtac quot_thm,
-    rtac @{thm IDENTITY_QUOTIENT},
-    rtac @{thm ext},
-    rtac trans_thm,
-    LAMBDA_RES_TAC ctxt,
-    res_forall_rsp_tac ctxt,
-    res_exists_rsp_tac ctxt,
-    (
-     (simp_tac ((Simplifier.context ctxt HOL_ss) addsimps (rsp_thms @ @{thms ho_all_prs ho_ex_prs})))
-     THEN_ALL_NEW (fn _ => no_tac)
-    ),
-    (instantiate_tac @{thm REP_ABS_RSP(1)} ctxt THEN' (RANGE [quotient_tac quot_thm])),
-    rtac refl,
-    (instantiate_tac @{thm APPLY_RSP} ctxt THEN' (RANGE [quotient_tac quot_thm, quotient_tac quot_thm])),
-    rtac reflex_thm, 
-    atac,
-    (
-     (simp_tac ((Simplifier.context @{context} HOL_ss) addsimps @{thms FUN_REL.simps}))
-     THEN_ALL_NEW (fn _ => no_tac)
-    ),
-    WEAK_LAMBDA_RES_TAC ctxt
-    ])
-*}
-
-ML {*
 fun repabs_eq lthy thm constructors rty qty quot_thm reflex_thm trans_thm rsp_thms =
   let
     val rt = build_repabs_term lthy thm constructors rty qty;
@@ -377,10 +274,11 @@
   end
 *}
 
-
+(* 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} @{thms ho_memb_rsp ho_cons_rsp ho_card1_rsp}
+  r_mk_comb_tac ctxt @{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})
 *}
 
 
@@ -467,20 +365,7 @@
 done
 thm HOL.sym[OF lambda_prs_lb_b,simplified]
 
-ML {*
-fun eqsubst_thm ctxt thms thm =
-  let
-    val goalstate = Goal.init (Thm.cprop_of thm)
-    val a' = case (SINGLE (EqSubst.eqsubst_tac ctxt [0] thms 1) goalstate) of
-      NONE => error "eqsubst_thm"
-    | SOME th => cprem_of th 1
-    val tac = (EqSubst.eqsubst_tac ctxt [0] thms 1) THEN simp_tac HOL_ss 1
-    val cgoal = cterm_of (ProofContext.theory_of ctxt) (Logic.mk_equals (term_of (Thm.cprop_of thm), term_of a'))
-    val rt = Toplevel.program (fn () => Goal.prove_internal [] cgoal (fn _ => tac));
-  in
-    Simplifier.rewrite_rule [rt] thm
-  end
-*}
+
 
 
 ML {*
@@ -497,9 +382,9 @@
   fun simp_allex_prs lthy thm =
     let
       val rwf = @{thm FORALL_PRS[OF QUOTIENT_fset]};
-      val rwfs = @{thm "HOL.sym"} OF [spec OF [rwf]];
+      val rwfs = @{thm "HOL.sym"} OF [rwf];
       val rwe = @{thm EXISTS_PRS[OF QUOTIENT_fset]};
-      val rwes = @{thm "HOL.sym"} OF [spec OF [rwe]]
+      val rwes = @{thm "HOL.sym"} OF [rwe]
     in
       (simp_allex_prs lthy (eqsubst_thm lthy [rwfs, rwes] thm))
     end
@@ -564,7 +449,7 @@
   Toplevel.program (fn () =>
   repabs_eq @{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_memb_rsp ho_cons_rsp ho_card1_rsp} @ @{thms ho_all_prs ho_ex_prs})
   )
 *}
 ML {*
@@ -592,6 +477,7 @@
 ML {* val ind_r_a = simp_allex_prs @{context} 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 = MetaSimplifier.rewrite_rule 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 *}
@@ -604,7 +490,7 @@
   val (g, t, ot) =
     repabs_eq @{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_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);
   val ind_r_l = simp_lam_prs @{context} ind_r_t;
   val ind_r_a = simp_allex_prs @{context} ind_r_l;
@@ -614,6 +500,8 @@
   ObjectLogic.rulify ind_r_s
 end
 *}
+ML fset_defs
+
 
 ML {* lift @{thm m2} *}
 ML {* lift @{thm m1} *}
nominal2