# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1271405896 -7200
# Node ID 226b797868dca5a6aff1011d8ef553900ba1c902
# Parent  d3fe17786640075f6b075f7f5939e1b0728e9bbd
some tuning of eqvt-infrastructure

diff -r d3fe17786640 -r 226b797868dc Nominal-General/Nominal2_Supp.thy
--- a/Nominal-General/Nominal2_Supp.thy	Thu Apr 15 21:56:03 2010 +0200
+++ b/Nominal-General/Nominal2_Supp.thy	Fri Apr 16 10:18:16 2010 +0200
@@ -68,7 +68,7 @@
   unfolding fresh_star_def
   by (metis mem_permute_iff permute_minus_cancel fresh_permute_iff)
 
-lemma fresh_star_eqvt:
+lemma fresh_star_eqvt[eqvt]:
   shows "(p \<bullet> (as \<sharp>* x)) = (p \<bullet> as) \<sharp>* (p \<bullet> x)"
 unfolding fresh_star_def
 unfolding Ball_def
diff -r d3fe17786640 -r 226b797868dc Nominal-General/nominal_eqvt.ML
--- a/Nominal-General/nominal_eqvt.ML	Thu Apr 15 21:56:03 2010 +0200
+++ b/Nominal-General/nominal_eqvt.ML	Fri Apr 16 10:18:16 2010 +0200
@@ -146,7 +146,7 @@
   val params_no = length (Inductive.params_of raw_induct)
   val (([raw_concl], [raw_pi]), ctxt') = ctxt 
          |> Variable.import_terms false [concl_of raw_induct] 
-         ||>> Variable.variant_fixes ["pi"]
+         ||>> Variable.variant_fixes ["p"]
   val pi = Free (raw_pi, @{typ perm})
   val preds = map (fst o HOLogic.dest_imp)
     (HOLogic.dest_conj (HOLogic.dest_Trueprop raw_concl));
diff -r d3fe17786640 -r 226b797868dc Nominal/Ex/Lambda.thy
--- a/Nominal/Ex/Lambda.thy	Thu Apr 15 21:56:03 2010 +0200
+++ b/Nominal/Ex/Lambda.thy	Fri Apr 16 10:18:16 2010 +0200
@@ -180,21 +180,35 @@
 inductive
  alpha_lam_raw'
 where
-  "name = namea \<Longrightarrow> alpha_lam_raw' (Var_raw name) (Var_raw namea)"
-| "\<lbrakk>alpha_lam_raw' lam_raw1 lam_raw1a; alpha_lam_raw' lam_raw2 lam_raw2a\<rbrakk> \<Longrightarrow>
+  a1: "name = namea \<Longrightarrow> alpha_lam_raw' (Var_raw name) (Var_raw namea)"
+| a2: "\<lbrakk>alpha_lam_raw' lam_raw1 lam_raw1a; alpha_lam_raw' lam_raw2 lam_raw2a\<rbrakk> \<Longrightarrow>
    alpha_lam_raw' (App_raw lam_raw1 lam_raw2) (App_raw lam_raw1a lam_raw2a)"
-| "\<exists>pi. ({atom name}, lam_raw) \<approx>gen alpha_lam_raw fv_lam_raw pi ({atom namea}, lam_rawa) \<Longrightarrow>
+| a3: "\<exists>pi. ({atom name}, lam_raw) \<approx>gen alpha_lam_raw fv_lam_raw pi ({atom namea}, lam_rawa) \<Longrightarrow>
    alpha_lam_raw' (Lam_raw name lam_raw) (Lam_raw namea lam_rawa)"
 
 declare permute_lam_raw.simps[eqvt]
-(*declare alpha_gen_real_eqvt[eqvt]*)
+declare alpha_gen_eqvt[eqvt]
 (*equivariance alpha_lam_raw'*)
+thm eqvts_raw
+
+lemma
+  assumes a: "alpha_lam_raw' t1 t2"
+  shows "alpha_lam_raw' (p \<bullet> t1) (p \<bullet> t2)"
+oops
 
 lemma
   assumes a: "alpha_lam_raw' t1 t2"
   shows "alpha_lam_raw' (p \<bullet> t1) (p \<bullet> t2)"
 using a
 apply(induct)
+ML_prf {*
+val ({names, ...}, {raw_induct, intrs, ...}) =
+    Inductive.the_inductive @{context} (Sign.intern_const @{theory} "alpha_lam_raw")
+*}
+apply(tactic {* Nominal_Eqvt.eqvt_rel_case_tac 
+  @{context} ["Lambda.alpha_lam_raw"] @{term "p::perm"} @{thm a1} 1*})
+apply(tactic {* Nominal_Eqvt.eqvt_rel_case_tac 
+  @{context} ["Lambda.alpha_lam_raw"] @{term "p::perm"} @{thm a2} 1*})
 oops