Mercurial Mercurial > hg > nominal2 / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Fixes
authorCezary Kaliszyk <kaliszyk@in.tum.de>
Wed, 28 Oct 2009 16:05:59 +0100
changeset 221 f219011a5e3c
parent 219 329111e1c4ba
child 222 37b29231265b
Fixes
FSet.thy file | annotate | diff | comparison | revisions
IntEx.thy file | annotate | diff | comparison | revisions
LamEx.thy file | annotate | diff | comparison | revisions
QuotMain.thy file | annotate | diff | comparison | revisions
isar-keywords-prove.el file | annotate | diff | comparison | revisions 
--- a/FSet.thy	Wed Oct 28 15:25:36 2009 +0100
+++ b/FSet.thy	Wed Oct 28 16:05:59 2009 +0100
@@ -306,8 +306,12 @@
   apply (metis)
   done
 
+ML {* (atomize_thm @{thm list_induct_hol4}) *}
+
+ML {* regularise (prop_of (atomize_thm @{thm list_induct_hol4})) @{typ "'a list"} @{term "op \<approx>"} @{context} *}
+
 prove list_induct_r: {*
-   build_regularize_goal (atomize_thm @{thm list_induct_hol4}) @{typ "'a List.list"} @{term "op \<approx>"} @{context} *}
+   build_regularize_goal (atomize_thm @{thm list_induct_hol4}) @{typ "'a list"} @{term "op \<approx>"} @{context} *}
   apply (simp only: equiv_res_forall[OF equiv_list_eq])
   thm RIGHT_RES_FORALL_REGULAR
   apply (rule RIGHT_RES_FORALL_REGULAR)
--- a/IntEx.thy	Wed Oct 28 15:25:36 2009 +0100
+++ b/IntEx.thy	Wed Oct 28 16:05:59 2009 +0100
@@ -156,7 +156,7 @@
 
 text {* Below is the construction site code used if things do now work *}
 
-ML {* val t_a = atomize_thm @{thm plus_assoc_pre} *}
+ML {* val t_a = atomize_thm @{thm plus_sym_pre} *}
 ML {* val t_r = regularize t_a rty rel rel_eqv @{context} *}
 
 ML {* val t_t =
@@ -170,19 +170,13 @@
 ML {* val abs = findabs rty (prop_of (atomize_thm @{thm plus_sym_pre})) *}
 
 ML {* val simp_lam_prs_thms = map (make_simp_lam_prs_thm @{context} quot) abs *}
-
-ML {*
-  fun simp_lam_prs lthy thm =
-    simp_lam_prs lthy (eqsubst_thm lthy simp_lam_prs_thms thm)
-    handle _ => thm
-*}
 ML {* t_t *}
-ML {* val t_l = simp_lam_prs @{context} t_t *}
+ML {* val t_l = repeat_eqsubst_thm @{context} simp_lam_prs_thms t_t *}
 
 ML {* val t_a = simp_allex_prs @{context} quot t_l *}
 
 ML {* val t_defs_sym = add_lower_defs @{context} t_defs *}
-ML {* val t_d = MetaSimplifier.rewrite_rule t_defs_sym t_a *}
+ML {* val t_d = repeat_eqsubst_thm @{context} t_defs_sym t_a *}
 ML {* val t_r = MetaSimplifier.rewrite_rule [reps_same] t_d *}
 ML {* ObjectLogic.rulify t_r *}
 
--- a/LamEx.thy	Wed Oct 28 15:25:36 2009 +0100
+++ b/LamEx.thy	Wed Oct 28 16:05:59 2009 +0100
@@ -73,14 +73,88 @@
 ML {* val t_b = MetaSimplifier.rewrite_rule [reps_same] t_d *}
 ML {* ObjectLogic.rulify t_b *}
 
+thm fresh_def
+thm supp_def
+
 local_setup {*
-  make_const_def @{binding lfresh} @{term "fresh :: 'a \<Rightarrow> rlam \<Rightarrow> bool"} NoSyn @{typ "rlam"} @{typ "lam"} #> snd #>
   make_const_def @{binding lperm} @{term "perm :: ('a \<times> 'a) list \<Rightarrow> rlam \<Rightarrow> rlam"} NoSyn @{typ "rlam"} @{typ "lam"} #> snd
 *}
 
-ML {* val consts = @{const_name fresh} :: @{const_name perm} :: consts *}
-ML {* val defs = @{thms lfresh_def lperm_def} @ defs *}
+ML {* val consts = @{const_name perm} :: consts *}
+ML {* val defs = @{thms lperm_def} @ defs *}
+ML {* val t_u = MetaSimplifier.rewrite_rule @{thms fresh_def supp_def} @{thm a3} *}
+ML {* val t_a = atomize_thm t_u *}
+ML {* val t_r = regularize t_a rty rel rel_eqv @{context} *}
+
+ML {*
+fun r_mk_comb_tac_lam ctxt = r_mk_comb_tac ctxt rty quot rel_refl trans2 rsp_thms
+*}
+
+prove {* build_repabs_goal @{context} t_r consts rty qty *}
+apply (atomize(full))
+apply (tactic {* (r_mk_comb_tac_lam @{context}) 1 *})
+apply (tactic {* (r_mk_comb_tac_lam @{context}) 1 *})
+apply (tactic {* (r_mk_comb_tac_lam @{context}) 1 *})
+apply (tactic {* (r_mk_comb_tac_lam @{context}) 1 *})
+apply (tactic {* (r_mk_comb_tac_lam @{context}) 1 *})
+apply (tactic {* (r_mk_comb_tac_lam @{context}) 1 *})
+apply (tactic {* (r_mk_comb_tac_lam @{context}) 1 *})
+apply (tactic {* (r_mk_comb_tac_lam @{context}) 1 *})
+apply (tactic {* (r_mk_comb_tac_lam @{context}) 1 *})
+apply (tactic {* (r_mk_comb_tac_lam @{context}) 1 *})
+apply (tactic {* (r_mk_comb_tac_lam @{context}) 1 *})
+apply (tactic {* (r_mk_comb_tac_lam @{context}) 1 *})
+apply (tactic {* (r_mk_comb_tac_lam @{context}) 1 *})
+apply (tactic {* (r_mk_comb_tac_lam @{context}) 1 *})
+apply (tactic {* (r_mk_comb_tac_lam @{context}) 1 *})
+apply (tactic {* (r_mk_comb_tac_lam @{context}) 1 *})
+apply (tactic {* (r_mk_comb_tac_lam @{context}) 1 *})
+apply (tactic {* (r_mk_comb_tac_lam @{context}) 1 *})
+apply (tactic {* (r_mk_comb_tac_lam @{context}) 1 *})
+apply (tactic {* (r_mk_comb_tac_lam @{context}) 1 *})
+apply (tactic {* (r_mk_comb_tac_lam @{context}) 1 *})
+apply (tactic {* (r_mk_comb_tac_lam @{context}) 1 *})
+apply (tactic {* (r_mk_comb_tac_lam @{context}) 1 *})
+apply (tactic {* (r_mk_comb_tac_lam @{context}) 1 *})
+apply (tactic {* (r_mk_comb_tac_lam @{context}) 1 *})
+apply (tactic {* (r_mk_comb_tac_lam @{context}) 1 *})
+apply (tactic {* (r_mk_comb_tac_lam @{context}) 1 *})
+apply (tactic {* (r_mk_comb_tac_lam @{context}) 1 *})
+prefer 2
+apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_lam @{context}) 1 *})
+apply (tactic {* (r_mk_comb_tac_lam @{context}) 1 *})
+apply (tactic {* (r_mk_comb_tac_lam @{context}) 1 *})
+apply (tactic {* (r_mk_comb_tac_lam @{context}) 1 *})
+apply (tactic {* (r_mk_comb_tac_lam @{context}) 1 *})
+apply (tactic {* (r_mk_comb_tac_lam @{context}) 1 *})
+apply (tactic {* (r_mk_comb_tac_lam @{context}) 1 *})
+apply (tactic {* (r_mk_comb_tac_lam @{context}) 1 *})
+apply (tactic {* (r_mk_comb_tac_lam @{context}) 1 *})
+apply (tactic {* (r_mk_comb_tac_lam @{context}) 1 *})
+apply (tactic {* (r_mk_comb_tac_lam @{context}) 1 *})
+apply (tactic {* (r_mk_comb_tac_lam @{context}) 1 *})
+apply (tactic {* (r_mk_comb_tac_lam @{context}) 1 *})
+apply (tactic {* (r_mk_comb_tac_lam @{context}) 1 *})
+apply (tactic {* (r_mk_comb_tac_lam @{context}) 1 *})
+apply (tactic {* (r_mk_comb_tac_lam @{context}) 1 *})
+apply (tactic {* (r_mk_comb_tac_lam @{context}) 1 *})
+apply (tactic {* (r_mk_comb_tac_lam @{context}) 1 *})
+apply (tactic {* (r_mk_comb_tac_lam @{context}) 1 *})
+nitpick
+apply (tactic {* (r_mk_comb_tac_lam @{context}) 1 *})
+apply (tactic {* (r_mk_comb_tac_lam @{context}) 1 *})
+apply (tactic {* (r_mk_comb_tac_lam @{context}) 1 *})
+
+
+
+
+
+
+
 ML {* val t_t = Toplevel.program (fn () => repabs @{context} t_r consts rty qty quot rel_refl trans2 rsp_thms) *}
+
+ML {* val t_t = repabs @{context} t_r consts rty qty quot rel_refl trans2 rsp_thms *}
+
 ML {* val t_l = repeat_eqsubst_thm @{context} simp_lam_prs_thms t_t *}
 ML {* val t_c = simp_allex_prs @{context} quot t_l *}
 ML {* val t_defs_sym = add_lower_defs @{context} defs *}
@@ -94,7 +168,11 @@
 
 
 
-
+local_setup {*
+  make_const_def @{binding lfresh} @{term "fresh :: 'a \<Rightarrow> rlam \<Rightarrow> bool"} NoSyn @{typ "rlam"} @{typ "lam"} #> snd #>
+*}
+@{const_name fresh} :: 
+lfresh_def 
 ML {*
 fun lift_thm_lam lthy t =
   lift_thm lthy consts rty qty rel rel_eqv rel_refl quot rsp_thms trans2 reps_same defs t
--- a/QuotMain.thy	Wed Oct 28 15:25:36 2009 +0100
+++ b/QuotMain.thy	Wed Oct 28 16:05:59 2009 +0100
@@ -397,10 +397,10 @@
 ML {*
 fun atomize_thm thm =
 let
-  val thm' = forall_intr_vars thm
+  val thm' = Thm.freezeT (forall_intr_vars thm)
   val thm'' = ObjectLogic.atomize (cprop_of thm')
 in
-  Thm.freezeT @{thm Pure.equal_elim_rule1} OF [thm'', thm']
+  @{thm Pure.equal_elim_rule1} OF [thm'', thm']
 end
 *}
 
--- a/isar-keywords-prove.el	Wed Oct 28 15:25:36 2009 +0100
+++ b/isar-keywords-prove.el	Wed Oct 28 16:05:59 2009 +0100
@@ -127,6 +127,7 @@
     "method_setup"
     "moreover"
     "next"
+    "nitpick"
     "no_notation"
     "no_syntax"
     "no_translations"
@@ -580,6 +581,7 @@
     "apply_end"
     "back"
     "defer"
+    "nitpick"
     "prefer"))
 
 (provide 'isar-keywords)
nominal2