# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1271950044 -7200
# Node ID ffca58ce9fbc03baddf0b70c9e8928be41ae46c7
# Parent  99367d481f7859b2fd096894e47b5a97ccc302cd
Update term8

diff -r 99367d481f78 -r ffca58ce9fbc Nominal/Manual/Term8.thy
--- a/Nominal/Manual/Term8.thy	Thu Apr 22 12:42:15 2010 +0200
+++ b/Nominal/Manual/Term8.thy	Thu Apr 22 17:27:24 2010 +0200
@@ -1,5 +1,5 @@
 theory Term8
-imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "Abs" "Perm" "Fv" "Rsp" "../Attic/Prove"
+imports "../../Nominal-General/Nominal2_Atoms" "../../Nominal-General/Nominal2_Eqvt" "../../Nominal-General/Nominal2_Supp" "../Abs" "../Perm" "../Fv" "../Rsp" "../Lift" "../../Attic/Prove"
 begin
 
 atom_decl name
@@ -20,42 +20,55 @@
 setup {* snd o define_raw_perms (Datatype.the_info @{theory} "Term8.rfoo8") 2 *}
 print_theorems
 
-local_setup {* snd o define_fv_alpha (Datatype.the_info @{theory} "Term8.rfoo8") [
-  [[[]], [[], [(SOME @{term rbv8}, 0)]]], [[[]], [[], [(NONE, 1)], [(NONE, 1)]]]] *}
+ML define_fv_alpha_export
+local_setup {* snd o define_fv_alpha_export (Datatype.the_info @{theory} "Term8.rfoo8") [
+  [[], [(SOME (@{term rbv8}, false), 0, 1, AlphaGen)]], [[], [(NONE, 1, 2, AlphaGen)]]]
+  [(@{term "rbv8"}, 1, [[], [(0, NONE), (2, SOME @{term rbv8})]])] *}
 notation
   alpha_rfoo8 ("_ \<approx>f' _" [100, 100] 100) and
   alpha_rbar8 ("_ \<approx>b' _" [100, 100] 100)
-thm alpha_rfoo8_alpha_rbar8.intros
-
+thm alpha_rfoo8_alpha_rbar8_alpha_rbv8.intros[no_vars]
+thm fv_rbar8.simps fv_rfoo8_fv_rbv8.simps
 
 inductive
   alpha8f :: "rfoo8 \<Rightarrow> rfoo8 \<Rightarrow> bool" ("_ \<approx>f _" [100, 100] 100)
 and
   alpha8b :: "rbar8 \<Rightarrow> rbar8 \<Rightarrow> bool" ("_ \<approx>b _" [100, 100] 100)
+and
+  alpha8bv:: "rbar8 \<Rightarrow> rbar8 \<Rightarrow> bool" ("_ \<approx>bv _" [100, 100] 100)
 where
-  a1: "a = b \<Longrightarrow> (Foo0 a) \<approx>f (Foo0 b)"
-| a2: "a = b \<Longrightarrow> (Bar0 a) \<approx>b (Bar0 b)"
-| a3: "b1 \<approx>b b2 \<Longrightarrow> (\<exists>pi. (((rbv8 b1), t1) \<approx>gen alpha8f fv_rfoo8 pi ((rbv8 b2), t2))) \<Longrightarrow> Foo1 b1 t1 \<approx>f Foo1 b2 t2"
-| a4: "v1 = v2 \<Longrightarrow> (\<exists>pi. (({atom x1}, t1) \<approx>gen alpha8b fv_rbar8 pi ({atom x2}, t2))) \<Longrightarrow> Bar1 v1 x1 t1 \<approx>b Bar1 v2 x2 t2"
+  "name = namea \<Longrightarrow> Foo0 name \<approx>f Foo0 namea"
+| "\<exists>pi. rbar8 \<approx>bv rbar8a \<and>
+     (rbv8 rbar8, rfoo8) \<approx>gen alpha8f fv_rfoo8 pi (rbv8 rbar8a, rfoo8a) \<Longrightarrow>
+  Foo1 rbar8 rfoo8 \<approx>f Foo1 rbar8a rfoo8a"
+| "name = namea \<Longrightarrow> Bar0 name \<approx>b Bar0 namea"
+| "\<exists>pi. name1 = name1a \<and> ({atom name2}, rbar8) \<approx>gen alpha8b fv_rbv8 pi ({atom name2a}, rbar8a) \<Longrightarrow>
+  Bar1 name1 name2 rbar8 \<approx>b Bar1 name1a name2a rbar8a"
+| "name = namea \<Longrightarrow> alpha8bv (Bar0 name) (Bar0 namea)"
+| "({atom name2}, rbar8) \<approx>gen alpha8b fv_rbv8 pi ({atom name2a}, rbar8a) \<Longrightarrow>
+   alpha8bv (Bar1 name1 name2 rbar8) (Bar1 name1a name2a rbar8a)"
 
 lemma "(alpha8b ===> op =) rbv8 rbv8"
-  apply simp apply clarify
-  apply (erule alpha8f_alpha8b.inducts(2))
+  apply rule
+  apply (induct_tac a b rule: alpha8f_alpha8b_alpha8bv.inducts(2))
   apply (simp_all)
-done
+  done
 
 lemma fv_rbar8_rsp_hlp: "x \<approx>b y \<Longrightarrow> fv_rbar8 x = fv_rbar8 y"
-  apply (erule alpha8f_alpha8b.inducts(2))
+  apply (erule alpha8f_alpha8b_alpha8bv.inducts(2))
   apply (simp_all add: alpha_gen)
-done
+  apply clarify
+  sorry
+
 lemma "(alpha8b ===> op =) fv_rbar8 fv_rbar8"
   apply simp apply clarify apply (simp add: fv_rbar8_rsp_hlp)
-done
+  done
 
 lemma "(alpha8f ===> op =) fv_rfoo8 fv_rfoo8"
   apply simp apply clarify
-  apply (erule alpha8f_alpha8b.inducts(1))
+  apply (erule alpha8f_alpha8b_alpha8bv.inducts(1))
   apply (simp_all add: alpha_gen fv_rbar8_rsp_hlp)
+
 done
 
 end