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.
Regularization
authorCezary Kaliszyk <kaliszyk@in.tum.de>
Fri, 30 Oct 2009 18:31:06 +0100
changeset 251 c770f36f9459
parent 250 1dd7f7f98040
child 252 e30997c88050
Regularization
FSet.thy file | annotate | diff | comparison | revisions
LamEx.thy file | annotate | diff | comparison | revisions
QuotMain.thy file | annotate | diff | comparison | revisions 
--- a/FSet.thy	Fri Oct 30 16:37:09 2009 +0100
+++ b/FSet.thy	Fri Oct 30 18:31:06 2009 +0100
@@ -316,22 +316,33 @@
 ML {* lift_thm_fset @{context} @{thm list_eq.intros(5)} *}
 ML {* lift_thm_fset @{context} @{thm card1_suc} *}
 ML {* lift_thm_fset @{context} @{thm map_append} *}
-ML {* lift_thm_fset @{context} @{thm eq_r[OF append_assoc]} *}
+ML {* lift_thm_fset @{context} @{thm append_assoc} *}
 
 thm fold1.simps(2)
 thm list.recs(2)
 thm list.cases
 
 
-ML {* val ind_r_a = atomize_thm @{thm list.induct} *}
-(*prove {* build_regularize_goal ind_r_a rty rel @{context}  *}
+ML {* val ind_r_a = atomize_thm @{thm m2} *}
+prove {* build_regularize_goal ind_r_a rty rel @{context}  *}
   ML_prf {*  fun tac ctxt =
-       (asm_full_simp_tac ((Simplifier.context ctxt HOL_ss) addsimps
+     (FIRST' [
+      rtac rel_refl,
+      atac,
+      (rtac @{thm  allI} THEN' dtac @{thm spec}),
+      (fn i => CHANGED (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 [])); *}
-  apply (tactic {* tac @{context} 1 *})*)
+         (@{thm equiv_res_exists} OF [rel_eqv])]) i)),
+      MetisTools.metis_tac ctxt [],
+      rtac (@{thm eq_rr} OF [rel_refl]),
+      ((rtac @{thm RIGHT_RES_FORALL_REGULAR}) THEN' (RANGE [fn _ => all_tac, atac]))
+    ]);
+ *}
+  apply (tactic {* tac @{context} 1 *}) 
+  apply (tactic {* tac @{context} 1 *}) 
+  apply (tactic {* tac @{context} 1 *}) 
+
+
 ML {* val ind_r_r = regularize ind_r_a rty rel rel_eqv @{context} *}
 ML {*
   val rt = build_repabs_term @{context} ind_r_r consts rty qty
--- a/LamEx.thy	Fri Oct 30 16:37:09 2009 +0100
+++ b/LamEx.thy	Fri Oct 30 18:31:06 2009 +0100
@@ -179,7 +179,6 @@
 ML {* val a2 = lift_thm_lam @{context} @{thm a1} *}
 ML {* val a3 = lift_thm_lam @{context} @{thm a3} *}
 
-
 local_setup {*
   Quotient.note (@{binding "pi_var"}, pi_var) #> snd #>
   Quotient.note (@{binding "pi_app"}, pi_app) #> snd #>
@@ -219,6 +218,112 @@
 
 
 
+lemma get_rid: "(\<And>x. (P x \<longrightarrow> Q x)) \<Longrightarrow> ((\<forall>x. P x) \<longrightarrow> (\<forall>x. Q x))"
+apply (auto)
+done
+
+lemma get_rid2: "(c \<longrightarrow> a) \<Longrightarrow> (a \<Longrightarrow> b \<longrightarrow> d) \<Longrightarrow> (a \<longrightarrow> b) \<longrightarrow> (c \<longrightarrow> d)"
+apply (auto)
+done
+
+ML {* val t_a = atomize_thm @{thm alpha.cases} *}
+prove {* build_regularize_goal t_a rty rel @{context}  *}
+  ML_prf {*  fun tac ctxt =
+     (FIRST' [
+      rtac rel_refl,
+      atac,
+      rtac @{thm get_rid},
+      rtac @{thm get_rid2},
+      (fn i => CHANGED (asm_full_simp_tac ((Simplifier.context ctxt HOL_ss) addsimps
+        [(@{thm equiv_res_forall} OF [rel_eqv]),
+         (@{thm equiv_res_exists} OF [rel_eqv])]) i)),
+      (rtac @{thm impI} THEN' (asm_full_simp_tac (Simplifier.context ctxt HOL_ss)) THEN' rtac rel_refl)
+    ]);
+ *}
+  apply (atomize(full))
+  apply (tactic {* tac @{context} 1 *})
+  apply (rule get_rid)
+  apply (rule get_rid)
+  apply (rule get_rid2)
+  apply (simp)
+  apply (rule get_rid)
+  apply (rule get_rid2)
+  apply (rule get_rid)
+  apply (rule get_rid2)
+  apply (rule impI)
+  apply (simp)
+  apply (tactic {* tac @{context} 1 *})
+  apply (rule get_rid2)
+  apply (rule impI)
+  apply (simp)
+  apply (tactic {* tac @{context} 1 *})
+  apply (simp)
+  apply (rule get_rid2)
+  apply (rule get_rid)
+  apply (rule get_rid)
+  apply (rule get_rid)
+  apply (rule get_rid2)
+  apply (rule impI)
+  apply (simp)
+  apply (tactic {* tac @{context} 1 *})
+  apply (rule get_rid)
+  apply (rule get_rid2)
+
+
+  apply (tactic {* compose_tac (false, @{thm get_rid}, 1) 1 *})
+ML_prf {*
+fun focus_compose t = Subgoal.FOCUS (fn {concl, ...} =>
+  rtac t 1)
+*}
+thm spec[of _ "x"]
+  apply (rule allI)
+  apply (drule_tac x="a2" in spec)
+  apply (rule impI)
+  apply (erule impE)
+  apply (assumption)
+  apply (rule allI)
+  apply (drule_tac x="P" in spec)
+  apply (atomize(full))
+  apply (rule allI)
+  apply (rule allI)
+  apply (rule allI)
+  apply (rule impI)
+  apply (rule get_rid2)
+
+  thm get_rid2
+  apply (tactic {* compose_tac (false, @{thm get_rid2}, 0) 1 *})
+
+  thm spec
+
+  ML_prf {* val t = snd (Subgoal.focus @{context} 1 (Isar.goal ())) *}
+ML_prf {* Seq.pull (compose_tac (false, @{thm get_rid}, 2) 1 t) *}
+
+
+  thm get_rid
+  apply (rule allI)
+  apply (drule spec)
+
+  thm spec
+  apply (tactic {* compose_tac (false, @{thm get_rid}, 1) 1 *})
+
+  apply (tactic {* tac @{context} 1 *})
+  apply (tactic {* tac @{context} 1 *})
+  apply (rule impI)
+  apply (erule impE)
+  apply (assumption)
+  apply (tactic {* tac @{context} 1 *})
+  apply (rule impI)
+  apply (erule impE)
+  apply (tactic {* tac @{context} 1 *})
+  apply (tactic {* tac @{context} 1 *})
+  apply (tactic {* tac @{context} 1 *})
+  apply (tactic {* tac @{context} 1 *})
+
+ML {* val t_r = regularize t_a rty rel rel_eqv rel_refl @{context} *}
+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_a = simp_allex_prs @{context} quot t_l *}
+ML {* val t_d = repeat_eqsubst_thm @{context} t_defs_sym
 
 
 
--- a/QuotMain.thy	Fri Oct 30 16:37:09 2009 +0100
+++ b/QuotMain.thy	Fri Oct 30 18:31:06 2009 +0100
@@ -501,6 +501,10 @@
          else
            Const (@{const_name "Ex"}, ty) $ apply_subt (my_reg lthy rel rty) t
        end
+  | Const (@{const_name "op ="}, ty) $ t =>
+      if needs_lift rty (fastype_of t) then
+        (tyRel (fastype_of t) rty rel lthy) $ t
+      else Const (@{const_name "op ="}, ty) $ (my_reg lthy rel rty t)
   | t1 $ t2 => (my_reg lthy rel rty t1) $ (my_reg lthy rel rty t2)
   | _ => trm
 *}
@@ -513,16 +517,25 @@
        (my_reg lthy rel rty (prop_of thm)))
 *}
 
+lemma eq_rr: "(\<And>x. R x x) \<Longrightarrow> a = b \<Longrightarrow> R a b"
+by (auto)
+
 ML {*
-fun regularize thm rty rel rel_eqv lthy =
+fun regularize thm rty rel rel_eqv rel_refl lthy =
   let
     val g = build_regularize_goal thm rty rel lthy;
     fun tac ctxt =
-       (asm_full_simp_tac ((Simplifier.context ctxt HOL_ss) addsimps
+     REPEAT_ALL_NEW (FIRST' [
+      rtac rel_refl,
+      atac,
+      (rtac @{thm  allI} THEN' dtac @{thm spec}),
+      (fn i => CHANGED (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 []));
+         (@{thm equiv_res_exists} OF [rel_eqv])]) i)),
+      MetisTools.metis_tac ctxt [],
+      rtac (@{thm eq_rr} OF [rel_refl]),
+      ((rtac @{thm RIGHT_RES_FORALL_REGULAR}) THEN' (RANGE [fn _ => all_tac, atac]))
+    ]);
     val cthm = Goal.prove lthy [] [] g (fn x => tac (#context x) 1);
   in
     cthm OF [thm]
@@ -907,7 +920,7 @@
   val (trans2, reps_same, quot) = lookup_quot_thms lthy qty_name;
   val consts = lookup_quot_consts defs;
   val t_a = atomize_thm t;
-  val t_r = regularize t_a rty rel rel_eqv lthy;
+  val t_r = regularize t_a rty rel rel_eqv rel_refl lthy;
   val t_t = repabs lthy t_r consts rty qty quot rel_refl trans2 rsp_thms;
   val abs = findabs rty (prop_of t_a);
   val simp_lam_prs_thms = map (make_simp_lam_prs_thm lthy quot) abs;
nominal2