# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1265108197 -3600
# Node ID b3deb964ad26b11affc4c095d23f32824b29554a
# Parent  7c12f5476d1b1cce1f71fe554b2ab8c7929eff1d
Some equivariance machinery that comes useful in LF.

diff -r 7c12f5476d1b -r b3deb964ad26 Attic/Unused.thy
--- a/Attic/Unused.thy	Tue Feb 02 11:23:17 2010 +0100
+++ b/Attic/Unused.thy	Tue Feb 02 11:56:37 2010 +0100
@@ -1,6 +1,31 @@
 (*notation ( output) "prop" ("#_" [1000] 1000) *)
 notation ( output) "Trueprop" ("#_" [1000] 1000)
 
+function(sequential)
+    akind :: "kind \<Rightarrow> kind \<Rightarrow> bool" ("_ \<approx>ki _" [100, 100] 100)
+and aty   :: "ty \<Rightarrow> ty \<Rightarrow> bool"     ("_ \<approx>ty _" [100, 100] 100)
+and atrm  :: "trm \<Rightarrow> trm \<Rightarrow> bool"   ("_ \<approx>tr _" [100, 100] 100)
+where
+  a1: "(Type) \<approx>ki (Type) = True"
+| a2: "(KPi A x K) \<approx>ki (KPi A' x' K') = (A \<approx>ty A' \<and> (\<exists>pi. (rfv_kind K - {atom x} = rfv_kind K' - {atom x'} \<and> (rfv_kind K - {atom x})\<sharp>* pi \<and> (pi \<bullet> K) \<approx>ki K' \<and> (pi \<bullet> x) = x')))"
+| "_ \<approx>ki _ = False"
+| a3: "(TConst i) \<approx>ty (TConst j) = (i = j)"
+| a4: "(TApp A M) \<approx>ty (TApp A' M') = (A \<approx>ty A' \<and> M \<approx>tr M')"
+| a5: "(TPi A x B) \<approx>ty (TPi A' x' B') = ((A \<approx>ty A') \<and> (\<exists>pi. rfv_ty B - {atom x} = rfv_ty B' - {atom x'} \<and> (rfv_ty B - {atom x})\<sharp>* pi \<and> (pi \<bullet> B) \<approx>ty B' \<and> (pi \<bullet> x) = x'))"
+| "_ \<approx>ty _ = False"
+| a6: "(Const i) \<approx>tr (Const j) = (i = j)"
+| a7: "(Var x) \<approx>tr (Var y) = (x = y)"
+| a8: "(App M N) \<approx>tr (App M' N') = (M \<approx>tr M' \<and> N \<approx>tr N')"
+| a9: "(Lam A x M) \<approx>tr (Lam A' x' M') = (A \<approx>ty A' \<and> (\<exists>pi. rfv_trm M - {atom x} = rfv_trm M' - {atom x'} \<and> (rfv_trm M - {atom x})\<sharp>* pi \<and> (pi \<bullet> M) \<approx>tr M' \<and> (pi \<bullet> x) = x'))"
+| "_ \<approx>tr _ = False"
+apply (pat_completeness)
+apply simp_all
+done
+termination
+by (size_change)
+
+
+
 lemma regularize_to_injection:
   shows "(QUOT_TRUE l \<Longrightarrow> y) \<Longrightarrow> (l = r) \<longrightarrow> y"
   by(auto simp add: QUOT_TRUE_def)
diff -r 7c12f5476d1b -r b3deb964ad26 Quot/Nominal/Abs.thy
--- a/Quot/Nominal/Abs.thy	Tue Feb 02 11:23:17 2010 +0100
+++ b/Quot/Nominal/Abs.thy	Tue Feb 02 11:56:37 2010 +0100
@@ -129,6 +129,26 @@
   apply(clarsimp)
   done
 
+lemma alpha_gen_atom_eqvt:
+  assumes a: "\<And>x. pi \<bullet> (f x) = f (pi \<bullet> x)"
+  and     b: "\<exists>pia. ({atom a}, t) \<approx>gen \<lambda>x1 x2. R x1 x2 \<and> R (pi \<bullet> x1) (pi \<bullet> x2) f pia ({atom b}, s)"
+  shows  "\<exists>pia. ({atom (pi \<bullet> a)}, pi \<bullet> t) \<approx>gen R f pia ({atom (pi \<bullet> b)}, pi \<bullet> s)"
+  using b apply -
+  apply(erule exE)
+  apply(rule_tac x="pi \<bullet> pia" in exI)
+  apply(simp add: alpha_gen.simps)
+  apply(erule conjE)+
+  apply(rule conjI)+
+  apply(rule_tac ?p1="- pi" in permute_eq_iff[THEN iffD1])
+  apply(simp add: a[symmetric] atom_eqvt eqvts)
+  apply(rule conjI)
+  apply(rule_tac ?p1="- pi" in fresh_star_permute_iff[THEN iffD1])
+  apply(simp add: a[symmetric] eqvts atom_eqvt)
+  apply(subst permute_eqvt[symmetric])
+  apply(simp)
+  done
+
+
 fun
   alpha_abs 
 where
diff -r 7c12f5476d1b -r b3deb964ad26 Quot/Nominal/LamEx2.thy
--- a/Quot/Nominal/LamEx2.thy	Tue Feb 02 11:23:17 2010 +0100
+++ b/Quot/Nominal/LamEx2.thy	Tue Feb 02 11:56:37 2010 +0100
@@ -122,23 +122,6 @@
 apply(auto)
 done
 
-lemma alpha_gen_eqvt_atom:
-  assumes a: "\<And>x. pi \<bullet> (f x) = f (pi \<bullet> x)"
-  shows "\<exists>pia. ({atom a}, t) \<approx>gen \<lambda>x1 x2. R x1 x2 \<and> R (pi \<bullet> x1) (pi \<bullet> x2) f pia ({atom b}, s) \<Longrightarrow> \<exists>pia. ({atom (pi \<bullet> a)}, pi \<bullet> t) \<approx>gen R f pia ({atom (pi \<bullet> b)}, pi \<bullet> s)"
-apply(erule exE)
-apply(rule_tac x="pi \<bullet> pia" in exI)
-apply(simp add: alpha_gen.simps)
-apply(erule conjE)+
-apply(rule conjI)+
-apply(rule_tac ?p1="- pi" in permute_eq_iff[THEN iffD1])
-apply(simp add: a[symmetric] atom_eqvt eqvts)
-apply(rule conjI)
-apply(rule_tac ?p1="- pi" in fresh_star_permute_iff[THEN iffD1])
-apply(simp add: a[symmetric] eqvts atom_eqvt)
-apply(subst permute_eqvt[symmetric])
-apply(simp)
-done
-
 text {* should be automatic with new version of eqvt-machinery *}
 lemma alpha_eqvt:
   shows "t \<approx> s \<Longrightarrow> (pi \<bullet> t) \<approx> (pi \<bullet> s)"