# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1266577558 -3600
# Node ID 5523d5713a65650429dc8cf51f299839c890cbe7
# Parent  2f4ce88c2c96830a4d22a8eb1b4751b44fe96bf6
Experiments for the pseudo-injectivity tactic.

diff -r 2f4ce88c2c96 -r 5523d5713a65 Quot/Nominal/Terms.thy
--- a/Quot/Nominal/Terms.thy	Fri Feb 19 10:26:38 2010 +0100
+++ b/Quot/Nominal/Terms.thy	Fri Feb 19 12:05:58 2010 +0100
@@ -18,6 +18,8 @@
 | BVr "name"
 | BPr "bp" "bp"
 
+print_theorems
+
 (* to be given by the user *)
 
 primrec 
@@ -29,16 +31,41 @@
 
 setup {* snd o define_raw_perms ["rtrm1", "bp"] ["Terms.rtrm1", "Terms.bp"] *}
 
-local_setup {* snd o define_fv_alpha "Terms.rtrm1"
+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"
   [[[[]], [[], []], [[(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
   alpha_rtrm1 ("_ \<approx>1 _" [100, 100] 100) and
   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:
@@ -841,7 +868,7 @@
 
 datatype rtrm7 =
   rVr7 "name"
-| rLm7 "name" "rtrm7"
+| rLm7 "name" "rtrm7" --"bind left in right"
 | rLt7 "rtrm7" "rtrm7" --"bind (bv7 left) in (right)"
 
 primrec
@@ -856,11 +883,12 @@
 
 local_setup {* snd o define_fv_alpha "Terms.rtrm7" [
   [[[]], [[(NONE, 0)], [(NONE, 0)]], [[(SOME @{term rbv7}, 0)], [(SOME @{term rbv7}, 0)]]]] *}
+print_theorems
 notation
   alpha_rtrm7 ("_ \<approx>7a _" [100, 100] 100)
 (* HERE THE RULES DIFFER *)
 thm alpha_rtrm7.intros
-
+thm fv_rtrm7.simps
 inductive
   alpha7 :: "rtrm7 \<Rightarrow> rtrm7 \<Rightarrow> bool" ("_ \<approx>7 _" [100, 100] 100)
 where