--- a/Quot/Nominal/Fv.thy Fri Feb 19 12:05:58 2010 +0100
+++ b/Quot/Nominal/Fv.thy Fri Feb 19 16:45:24 2010 +0100
@@ -215,23 +215,39 @@
print_theorems
*)
+
ML {*
-fun build_alpha_inj_gl thms ctxt =
+fun alpha_inj_tac dist_inj intrs elims =
+ SOLVED' (asm_full_simp_tac (HOL_ss addsimps intrs)) ORELSE'
+ rtac @{thm iffI} THEN' RANGE [
+ (eresolve_tac elims THEN_ALL_NEW
+ asm_full_simp_tac (HOL_ss addsimps dist_inj)
+ ),
+ (asm_full_simp_tac (HOL_ss addsimps intrs))]
+*}
+
+ML {*
+fun build_alpha_inj_gl thm =
+ let
+ val prop = prop_of thm;
+ val concl = HOLogic.dest_Trueprop (Logic.strip_imp_concl prop);
+ val hyps = map HOLogic.dest_Trueprop (Logic.strip_imp_prems prop);
+ fun list_conj l = foldr1 HOLogic.mk_conj l;
+ in
+ if hyps = [] then concl
+ else HOLogic.mk_eq (concl, list_conj hyps)
+ end;
+*}
+
+ML {*
+fun build_alpha_inj intrs dist_inj elims ctxt =
let
- (* TODO: use the context for export *)
- val ((_, thms_imp), ctxt') = Variable.import false thms ctxt;
- fun inj_thm thm_imp =
- let
- val prop = prop_of thm_imp;
- val concl = HOLogic.dest_Trueprop (Logic.strip_imp_concl prop);
- val hyps = map HOLogic.dest_Trueprop (Logic.strip_imp_prems prop);
- fun list_conj l = foldr1 HOLogic.mk_conj l;
- in
- if hyps = [] then concl
- else HOLogic.mk_eq (concl, list_conj hyps)
- end;
+ val ((_, thms_imp), ctxt') = Variable.import false intrs ctxt;
+ val gls = map (HOLogic.mk_Trueprop o build_alpha_inj_gl) thms_imp;
+ fun tac _ = alpha_inj_tac dist_inj intrs elims 1;
+ val thms = map (fn gl => Goal.prove ctxt' [] [] gl tac) gls;
in
- Logic.mk_conjunction_list (map (HOLogic.mk_Trueprop o inj_thm) thms_imp)
+ Variable.export ctxt' ctxt thms
end
*}
--- a/Quot/Nominal/Terms.thy Fri Feb 19 12:05:58 2010 +0100
+++ b/Quot/Nominal/Terms.thy Fri Feb 19 16:45:24 2010 +0100
@@ -31,22 +31,10 @@
setup {* snd o define_raw_perms ["rtrm1", "bp"] ["Terms.rtrm1", "Terms.bp"] *}
-ML {*
- val elims_ref = ref (@{thms refl})
- val intrs_ref = ref (@{thms refl})
-*}
-ML elims_ref
local_setup {*
-fn ctxt =>
- let val ((fv, ind), ctxt') =
- define_fv_alpha "Terms.rtrm1"
+ snd o define_fv_alpha "Terms.rtrm1"
[[[[]], [[], []], [[(NONE, 0)], [(NONE, 0)]], [[(SOME @{term bv1}, 0)], [], [(SOME @{term bv1}, 0)]]],
- [[], [[]], [[], []]]] ctxt;
- val elims' = ProofContext.export ctxt' ctxt (#elims ind)
- val intrs' = ProofContext.export ctxt' ctxt (#intrs ind)
- val _ = (elims_ref := elims');
- val _ = (intrs_ref := intrs');
- in ctxt' end *}
+ [[], [[]], [[], []]]] *}
print_theorems
notation
@@ -54,38 +42,8 @@
alpha_bp ("_ \<approx>1b _" [100, 100] 100)
thm alpha_rtrm1_alpha_bp.intros
-prove {* build_alpha_inj_gl @{thms alpha_rtrm1_alpha_bp.intros} @{context} *}
-apply -
-prefer 4
-apply (rule iffI)
-apply (tactic {* eresolve_tac (!elims_ref) 1 *})
-apply (simp only: rtrm1.distinct)
-apply (simp only: rtrm1.distinct)
-apply (simp only: rtrm1.distinct)
-apply (rule conjI) apply (simp only: rtrm1.inject)
-apply (rule conjI) apply (simp only: rtrm1.inject)
-apply (simp only: rtrm1.inject)
-apply (simp only: alpha_rtrm1_alpha_bp.intros)
-sorry
-
-lemma alpha1_inj:
-"(rVr1 a \<approx>1 rVr1 b) = (a = b)"
-"(rAp1 t1 s1 \<approx>1 rAp1 t2 s2) = (t1 \<approx>1 t2 \<and> s1 \<approx>1 s2)"
-"(rLm1 aa t \<approx>1 rLm1 ab s) = (\<exists>pi. (({atom aa}, t) \<approx>gen alpha_rtrm1 fv_rtrm1 pi ({atom ab}, s)))"
-"(rLt1 bp rtrm11 rtrm12 \<approx>1 rLt1 bpa rtrm11a rtrm12a) =
- ((\<exists>pi. (bv1 bp, bp) \<approx>gen alpha_bp fv_bp pi (bv1 bpa, bpa)) \<and> rtrm11 \<approx>1 rtrm11a \<and>
- (\<exists>pi. (bv1 bp, rtrm12) \<approx>gen alpha_rtrm1 fv_rtrm1 pi (bv1 bpa, rtrm12a)))"
-"alpha_bp BUnit BUnit"
-"(alpha_bp (BVr name) (BVr namea)) = (name = namea)"
-"(alpha_bp (BPr bp1 bp2) (BPr bp1a bp2a)) = (alpha_bp bp1 bp1a \<and> alpha_bp bp2 bp2a)"
-apply -
-apply rule apply (erule alpha_rtrm1.cases) apply (simp_all add: alpha_rtrm1_alpha_bp.intros)
-apply rule apply (erule alpha_rtrm1.cases) apply (simp_all add: alpha_rtrm1_alpha_bp.intros)
-apply rule apply (erule alpha_rtrm1.cases) apply (simp_all add: alpha_rtrm1_alpha_bp.intros)
-apply rule apply (erule alpha_rtrm1.cases) apply (simp_all add: alpha_rtrm1_alpha_bp.intros)
-apply rule apply (erule alpha_bp.cases) apply (simp_all add: alpha_rtrm1_alpha_bp.intros)
-apply rule apply (erule alpha_bp.cases) apply (simp_all add: alpha_rtrm1_alpha_bp.intros)
-done
+local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha1_inj}, []), (build_alpha_inj @{thms alpha_rtrm1_alpha_bp.intros} @{thms rtrm1.distinct rtrm1.inject bp.distinct bp.inject} @{thms alpha_rtrm1.cases alpha_bp.cases} ctxt)) ctxt)) *}
+thm alpha1_inj
lemma alpha_bp_refl: "alpha_bp a a"
apply induct
@@ -344,13 +302,16 @@
local_setup {* snd o define_fv_alpha "Terms.rtrm2"
[[[[]], [[], []], [[(NONE, 0)], [(NONE, 0)]], [[(SOME @{term rbv2}, 0)], [(SOME @{term rbv2}, 0)]]],
[[[], []]]] *}
-print_theorems
notation
alpha_rtrm2 ("_ \<approx>2 _" [100, 100] 100) and
alpha_rassign ("_ \<approx>2b _" [100, 100] 100)
thm alpha_rtrm2_alpha_rassign.intros
+local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha2_inj}, []), (build_alpha_inj @{thms alpha_rtrm2_alpha_rassign.intros} @{thms rtrm2.distinct rtrm2.inject rassign.distinct rassign.inject} @{thms alpha_rtrm2.cases alpha_rassign.cases} ctxt)) ctxt)) *}
+thm alpha2_inj
+
+
lemma alpha2_equivp:
"equivp alpha_rtrm2"
"equivp alpha_rassign"
@@ -492,28 +453,8 @@
alpha_rlts ("_ \<approx>l _" [100, 100] 100)
thm alpha_rtrm5_alpha_rlts.intros
-lemma alpha5_inj:
- "((rVr5 a) \<approx>5 (rVr5 b)) = (a = b)"
- "(rAp5 t1 s1 \<approx>5 rAp5 t2 s2) = (t1 \<approx>5 t2 \<and> s1 \<approx>5 s2)"
- "(rLt5 l1 t1 \<approx>5 rLt5 l2 t2) = ((\<exists>pi. ((rbv5 l1, t1) \<approx>gen alpha_rtrm5 fv_rtrm5 pi (rbv5 l2, t2))) \<and>
- (\<exists>pi. ((rbv5 l1, l1) \<approx>gen alpha_rlts fv_rlts pi (rbv5 l2, l2))))"
- "rLnil \<approx>l rLnil"
- "(rLcons n1 t1 ls1 \<approx>l rLcons n2 t2 ls2) = (n1 = n2 \<and> ls1 \<approx>l ls2 \<and> t1 \<approx>5 t2)"
-apply -
-apply (simp_all add: alpha_rtrm5_alpha_rlts.intros)
-apply rule
-apply (erule alpha_rtrm5.cases)
-apply (simp_all add: alpha_rtrm5_alpha_rlts.intros)
-apply rule
-apply (erule alpha_rtrm5.cases)
-apply (simp_all add: alpha_rtrm5_alpha_rlts.intros)
-apply rule
-apply (erule alpha_rtrm5.cases)
-apply (simp_all add: alpha_rtrm5_alpha_rlts.intros)
-apply rule
-apply (erule alpha_rlts.cases)
-apply (simp_all add: alpha_rtrm5_alpha_rlts.intros)
-done
+local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha5_inj}, []), (build_alpha_inj @{thms alpha_rtrm5_alpha_rlts.intros} @{thms rtrm5.distinct rtrm5.inject rlts.distinct rlts.inject} @{thms alpha_rtrm5.cases alpha_rlts.cases} ctxt)) ctxt)) *}
+thm alpha5_inj
lemma alpha5_equivps:
shows "equivp alpha_rtrm5"
@@ -560,6 +501,15 @@
apply(unfold alpha_gen)
apply (erule conjE)+
apply (rule conjI)
+ apply (rule_tac x="x \<bullet> pi" in exI)
+ apply (rule conjI)
+ apply(rule_tac ?p1="- x" in permute_eq_iff[THEN iffD1])
+ apply(simp add: atom_eqvt Diff_eqvt insert_eqvt set_eqvt empty_eqvt rbv5_eqvt fv_rlts_eqvt)
+ apply(rule conjI)
+ apply(rule_tac ?p1="- x" in fresh_star_permute_iff[THEN iffD1])
+ apply(simp add: atom_eqvt Diff_eqvt insert_eqvt set_eqvt empty_eqvt rbv5_eqvt fv_rlts_eqvt)
+ apply (subst permute_eqvt[symmetric])
+ apply (simp)
apply (rule_tac x="x \<bullet> pia" in exI)
apply (rule conjI)
apply(rule_tac ?p1="- x" in permute_eq_iff[THEN iffD1])
@@ -569,15 +519,6 @@
apply(simp add: atom_eqvt Diff_eqvt insert_eqvt set_eqvt empty_eqvt rbv5_eqvt fv_rtrm5_eqvt)
apply (subst permute_eqvt[symmetric])
apply (simp)
- apply (rule_tac x="x \<bullet> pi" in exI)
- apply (rule conjI)
- apply(rule_tac ?p1="- x" in permute_eq_iff[THEN iffD1])
- apply(simp add: atom_eqvt Diff_eqvt insert_eqvt set_eqvt empty_eqvt rbv5_eqvt fv_rlts_eqvt)
- apply(rule conjI)
- apply(rule_tac ?p1="- x" in fresh_star_permute_iff[THEN iffD1])
- apply(simp add: atom_eqvt Diff_eqvt insert_eqvt set_eqvt empty_eqvt rbv5_eqvt fv_rlts_eqvt)
- apply (subst permute_eqvt[symmetric])
- apply (simp)
done
lemma alpha5_rfv:
@@ -678,10 +619,10 @@
(Lt5 (Lcons y (Vr5 y) (Lcons x (Vr5 x) Lnil)) (Ap5 (Vr5 x) (Vr5 y)))"
apply (subst alpha5_INJ)
apply (rule conjI)
-apply (rule_tac x="0 :: perm" in exI)
+apply (rule_tac x="(x \<leftrightarrow> y)" in exI)
apply (simp only: alpha_gen)
apply (simp add: permute_trm5_lts fresh_star_def)
-apply (rule_tac x="(x \<leftrightarrow> y)" in exI)
+apply (rule_tac x="0 :: perm" in exI)
apply (simp only: alpha_gen)
apply (simp add: permute_trm5_lts fresh_star_def)
done
@@ -697,7 +638,7 @@
apply (simp add: alpha5_INJ(5))
apply(clarify)
apply (simp add: alpha5_INJ(2))
-apply (simp only: alpha5_INJ(1))
+apply (simp add: alpha5_INJ(1))
done
lemma distinct_helper:
@@ -1068,7 +1009,7 @@
setup {* snd o define_raw_perms ["tyS"] ["Terms.tyS"] *}
print_theorems
-local_setup {* define_raw_fv "Terms.ty" [[[[]], [[], []]]] *}
+local_setup {* snd o define_fv_alpha "Terms.ty" [[[[]], [[], []]]] *}
print_theorems
(*