# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1267557116 -3600
# Node ID bfd9af005e23b9e136ab2a7bfc01ff04e744c0af
# Parent  447666754176256ef3f91a26f93fe1223f3086df
preliinary test about alpha-weirdo

diff -r 447666754176 -r bfd9af005e23 Nominal/Test.thy
--- a/Nominal/Test.thy	Tue Mar 02 18:57:26 2010 +0100
+++ b/Nominal/Test.thy	Tue Mar 02 20:11:56 2010 +0100
@@ -7,15 +7,68 @@
 nominal_datatype weird =
   WBind x::"name" y::"name" p1::"weird" p2::"weird" p3::"weird"
     bind x in p1, bind x in p2, bind y in p2, bind y in p3
-| WVar "name"
-| WPair "weird" "weird"
+| WV "name"
+| WP "weird" "weird"
 
+thm permute_weird_raw.simps[no_vars]
 thm alpha_weird_raw.intros[no_vars]
 thm fv_weird_raw.simps[no_vars]
 (* Potential problem: Is it correct that in the fv-function 
 the first two terms are created? Should be ommitted. Also
 something wrong with the permutations. *)
 
+primrec 
+  fv_weird
+where
+  "fv_weird (WBind_raw x y p1 p2 p3) = 
+    (fv_weird p1 - {atom x}) \<union> (fv_weird p2 - ({atom x} \<union> {atom y})) \<union> (fv_weird p3 - {atom y})"
+| "fv_weird (WV_raw x) = {atom x}"
+| "fv_weird (WP_raw p1 p2) = (fv_weird p1 \<union> fv_weird p2)"
+
+inductive
+  alpha_weird
+where
+  "\<exists>p1 p2.  
+  ({atom y}, w3) \<approx>gen alpha_weird fv_weird p2 ({atom ya}, w3a) \<and>
+  ({atom x} \<union> {atom y}, w2) \<approx>gen alpha_weird fv_weird (p1 + p2) ({atom xa} \<union> {atom ya}, w2a) \<and>
+  ({atom x}, w1) \<approx>gen alpha_weird fv_weird p1 ({atom xa}, w1a) \<and>
+  supp p1 \<inter> supp p2 = {} \<Longrightarrow>
+  alpha_weird (WBind_raw x y w1 w2 w3) (WBind_raw xa ya w1a w2a w3a)"
+| "x = xa \<Longrightarrow> alpha_weird (WV_raw x) (WV_raw xa)"
+| "alpha_weird w2 w2a \<and> alpha_weird w1 w1a \<Longrightarrow> alpha_weird (WP_raw w1 w2) (WP_raw w1a w2a)"
+
+(*
+abbreviation "WBind \<equiv> WBind_raw"
+abbreviation "WP \<equiv> WP_raw"
+abbreviation "WV \<equiv> WV_raw"
+
+lemma test:
+  assumes a: "distinct [x, y, z]"
+  shows "alpha_weird (WBind x y (WP (WV x) (WV z)) (WP (WV x) (WV y)) (WP (WV z) (WV y)))  
+                     (WBind y x (WP (WV y) (WV z)) (WP (WV y) (WV x)) (WP (WV z) (WV x)))"
+apply(rule_tac alpha_weird.intros)
+unfolding alpha_gen
+using a
+apply(simp)
+apply(rule_tac x="(x \<leftrightarrow> y)" in exI)
+apply(rule_tac x="(x \<leftrightarrow> y)" in exI)
+apply(simp add: fresh_star_def)
+apply(simp add: flip_def)
+apply(auto)
+prefer 2
+apply(rule alpha_weird.intros)
+apply(simp add: alpha_weird.intros(2))
+prefer 2
+apply(rule alpha_weird.intros)
+apply(simp add: alpha_weird.intros(2))
+apply(simp)
+apply(rule alpha_weird.intros)
+apply(simp)
+apply(simp add: alpha_gen)
+using a
+apply(simp)
+*)
+
 text {* example 1 *}
 
 nominal_datatype lam =