Automatic production and proving of pseudo-injectivity.
authorCezary Kaliszyk <kaliszyk@in.tum.de>
Fri, 19 Feb 2010 16:45:24 +0100
changeset 1199 5770c73f2415
parent 1198 5523d5713a65
child 1200 a94c04c4a720
Automatic production and proving of pseudo-injectivity.
Quot/Nominal/Fv.thy
Quot/Nominal/Terms.thy
--- 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 
 
 (*