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.
LamEx.thy
changeset 252 e30997c88050
parent 251 c770f36f9459
child 253 e169a99c6ada 
--- a/LamEx.thy	Fri Oct 30 18:31:06 2009 +0100
+++ b/LamEx.thy	Fri Oct 30 19:03:53 2009 +0100
@@ -107,7 +107,7 @@
 
 lemma fv_lam:
   shows "fv (Lam a t) = (fv t) - {a}"
-sorry 
+sorry
 
 lemma real_alpha:
   assumes "t = [(a,b)]\<bullet>s" "a\<sharp>[b].s"
@@ -179,16 +179,20 @@
 ML {* val a2 = lift_thm_lam @{context} @{thm a1} *}
 ML {* val a3 = lift_thm_lam @{context} @{thm a3} *}
 
+ML {* val alpha_cases = lift_thm_lam @{context} @{thm alpha.cases} *}
+
 local_setup {*
   Quotient.note (@{binding "pi_var"}, pi_var) #> snd #>
   Quotient.note (@{binding "pi_app"}, pi_app) #> snd #>
   Quotient.note (@{binding "pi_lam"}, pi_lam) #> snd #>
   Quotient.note (@{binding "a1"}, a1) #> snd #>
   Quotient.note (@{binding "a2"}, a2) #> snd #>
-  Quotient.note (@{binding "a3"}, a3) #> snd
+  Quotient.note (@{binding "a3"}, a3) #> snd #>
+  Quotient.note (@{binding "alpha_cases"}, alpha_cases) #> snd
 *}
 
 thm alpha.cases
+thm alpha_cases
 
 thm rlam.inject
 thm pi_var
@@ -217,114 +221,17 @@
 
 
 
-
-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 abs = findabs rty (prop_of t_a); *}
+ML {* val simp_lam_prs_thms = map (make_simp_lam_prs_thm @{context} quot) abs *}
 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
-
+ML {* val defs_sym = add_lower_defs @{context} defs; *}
+ML {* val t_d = repeat_eqsubst_thm @{context} defs_sym t_a *}
+ML {* val t_r = MetaSimplifier.rewrite_rule [reps_same] t_d *}
+ML {* ObjectLogic.rulify t_r *}
 
 
 
@@ -358,127 +265,3 @@
   (* Simp starts hanging so don't know how to continue *)
   sorry
 
-(* Not sure if it make sense or if it will be needed *)
-lemma abs_fun_rsp: "(op = ===> alpha ===> op = ===> op =) abs_fun abs_fun"
-sorry
-
-(* Should not be needed *)
-lemma eq_rsp2: "((op = ===> op =) ===> (op = ===> op =) ===> op =) op = op ="
-apply auto
-apply (rule ext)
-apply auto
-apply (rule ext)
-apply auto
-done
-
-(* Should not be needed *)
-lemma perm_rsp_eq: "(op = ===> (op = ===> op =) ===> op = ===> op =) op \<bullet> op \<bullet>"
-apply auto
-thm arg_cong2
-apply (rule_tac f="perm x" in arg_cong2)
-apply (auto)
-apply (rule ext)
-apply (auto)
-done
-
-(* Should not be needed *)
-lemma fresh_rsp_eq: "(op = ===> (op = ===> op =) ===> op =) fresh fresh"
-apply (simp add: FUN_REL.simps)
-apply (metis ext)
-done
-
-(* It is just a test, it doesn't seem true... *)
-lemma quotient_cheat: "QUOTIENT op = (option_map ABS_lam) (option_map REP_lam)"
-sorry
-
-ML {* val rsp_thms = @{thms abs_fun_rsp OPT_QUOTIENT eq_rsp2 quotient_cheat perm_rsp_eq fresh_rsp_eq} @ rsp_thms *}
-ML {* fun lift_thm_lam lthy t = lift_thm lthy qty "lam" rsp_thms defs t *}
-
-thm a3
-ML {* Toplevel.program (fn () => lift_thm_lam @{context} @{thm a3}) *}
-thm a3
-ML {* val t_u1 = eqsubst_thm @{context} @{thms abs_fresh(1)} (atomize_thm @{thm a3}) *}
-ML {* val t_u = MetaSimplifier.rewrite_rule @{thms fresh_def supp_def} t_u1 *}
-
-(* T_U *)
-
-ML {* val t_a = atomize_thm @{thm rfv_var} *}
-ML {* val t_r = regularize t_a rty rel rel_eqv @{context} *}
-ML {* val t_t = repabs @{context} t_r consts rty qty quot rel_refl trans2 rsp_thms *}
-
-ML {* fun r_mk_comb_tac_lam ctxt =
-  r_mk_comb_tac ctxt rty quot rel_refl trans2 rsp_thms
-*}
-
-instance lam :: fs_name
-apply(intro_classes)
-sorry
-
-prove asdf: {* Logic.mk_implies (concl_of t_r, (@{term "Trueprop (\<forall>t\<Colon>rlam\<in>Respects
-          alpha.
-         \<forall>(a\<Colon>name) b\<Colon>name.
-            \<forall>s\<Colon>rlam\<in>Respects
-                alpha.
-               t \<approx> ([(a,
-                 b)] \<bullet> s) \<longrightarrow>
-               a = b \<or>
-               a
-               \<notin> {a\<Colon>name.
-                infinite
-                 {b\<Colon>name. Not
-                  (([(a, b)] \<bullet>
-                  s) \<approx>
-                  s)}} \<longrightarrow>
-               rLam a
-                t \<approx> rLam
-                 b s)"})) *}
-apply (tactic {* full_simp_tac ((Simplifier.context @{context} HOL_ss) addsimps
-        [(@{thm equiv_res_forall} OF [rel_eqv]),
-         (@{thm equiv_res_exists} OF [rel_eqv])]) 1 *})
-apply (rule allI)
-apply (drule_tac x="t" in spec)
-apply (rule allI)
-apply (drule_tac x="a" in spec)
-apply (rule allI)
-apply (drule_tac x="b" in spec)
-apply (rule allI)
-apply (drule_tac x="s" in spec)
-apply (rule impI)
-apply (drule_tac mp)
-apply (simp)
-apply (simp)
-apply (rule impI)
-apply (rule a3)
-apply (simp)
-apply (simp add: abs_fresh(1))
-apply (case_tac "a = b")
-apply (simp)
-apply (simp)
-apply (auto)
-apply (unfold fresh_def)
-apply (unfold supp_def)
-apply (simp)
-prefer 2
-apply (simp)
-sorry
-
-ML {* val abs = findabs rty (prop_of t_a) *}
-ML {* val simp_lam_prs_thms = map (make_simp_lam_prs_thm @{context} quot) abs *}
-ML {* val t_defs_sym = add_lower_defs @{context} defs *}
-
-ML {* val t_r' = @{thm asdf} OF [t_r] *}
-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 t_a *}
-ML {* val t_r = MetaSimplifier.rewrite_rule [reps_same] t_d *}
-ML {* val tt = MetaSimplifier.rewrite_rule [symmetric @{thm supp_def}, symmetric @{thm fresh_def}] t_r *}
-ML {* val rr = @{thm sym} OF @{thms abs_fresh(1)} *}
-ML {* val ttt = eqsubst_thm @{context} [rr] tt *}
-ML {* ObjectLogic.rulify ttt *}
-
-lemma
-  assumes a: "a \<notin> {a\<Colon>name. infinite {b\<Colon>name. \<not> ([(a, b)] \<bullet> s) \<approx> s}}"
-  shows "a \<notin> {a\<Colon>name. infinite {b\<Colon>name. [(a, b)] \<bullet> s \<noteq> s}}"
-  using a apply simp
-  sorry (* Not true... *)
nominal2