# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1256755012 -3600
# Node ID 13f985a93dbc478ef9a501d98fd3ffeeb511408a
# Parent  9b8e039ae960a7c380a6dbd94c883b91cca9550a
fixed the definition of alpha; this *breaks* some of the experiments

diff -r 9b8e039ae960 -r 13f985a93dbc LamEx.thy
--- a/LamEx.thy	Wed Oct 28 16:48:57 2009 +0100
+++ b/LamEx.thy	Wed Oct 28 19:36:52 2009 +0100
@@ -14,7 +14,7 @@
 where
   a1: "a = b \<Longrightarrow> (rVar a) \<approx> (rVar b)"
 | a2: "\<lbrakk>t1 \<approx> t2; s1 \<approx> s2\<rbrakk> \<Longrightarrow> rApp t1 s1 \<approx> rApp t2 s2"
-| a3: "\<lbrakk>t \<approx> ([(a,b)]\<bullet>s); a\<sharp>s\<rbrakk> \<Longrightarrow> rLam a t \<approx> rLam b s"
+| a3: "\<lbrakk>t \<approx> ([(a,b)]\<bullet>s); a\<sharp>[b].s\<rbrakk> \<Longrightarrow> rLam a t \<approx> rLam b s"
 
 quotient lam = rlam / alpha
 apply -
@@ -22,16 +22,56 @@
 
 print_quotients
 
-local_setup {*
-  old_make_const_def @{binding Var} @{term "rVar"} NoSyn @{typ "rlam"} @{typ "lam"} #> snd #>
-  old_make_const_def @{binding App} @{term "rApp"} NoSyn @{typ "rlam"} @{typ "lam"} #> snd #>
-  old_make_const_def @{binding Lam} @{term "rLam"} NoSyn @{typ "rlam"} @{typ "lam"} #> snd
-*}
+quotient_def (for lam)
+  Var :: "name \<Rightarrow> lam"
+where
+  "Var \<equiv> rVar"
+
+quotient_def (for lam)
+  App :: "lam \<Rightarrow> lam \<Rightarrow> lam"
+where
+  "App \<equiv> rApp"
+
+quotient_def (for lam)
+  Lam :: "name \<Rightarrow> lam \<Rightarrow> lam"
+where
+  "Lam \<equiv> rLam"
 
 thm Var_def
 thm App_def
 thm Lam_def
 
+(* definition of overloaded permutation function *)
+(* for the lifted type lam                       *)
+overloading
+  perm_lam    \<equiv> "perm :: 'x prm \<Rightarrow> lam \<Rightarrow> lam"   (unchecked)
+begin
+
+quotient_def (for lam)
+  perm_lam :: "'x prm \<Rightarrow> lam \<Rightarrow> lam"
+where
+  "perm_lam \<equiv> (perm::'x prm \<Rightarrow> rlam \<Rightarrow> rlam)"
+
+end
+
+thm perm_lam_def
+
+(* lemmas that need to lift *)
+lemma
+  fixes pi::"'x prm"
+  shows "(pi\<bullet>Var a) = Var (pi\<bullet>a)"
+  sorry
+
+lemma
+  fixes pi::"'x prm"
+  shows "(pi\<bullet>App t1 t2) = App (pi\<bullet>t1) (pi\<bullet>t2)"
+  sorry
+
+lemma
+  fixes pi::"'x prm"
+  shows "(pi\<bullet>Lam a t) = Lam (pi\<bullet>a) (pi\<bullet>t)"
+  sorry
+
 lemma real_alpha:
   assumes "t = ([(a,b)]\<bullet>s)" "a\<sharp>s"
   shows "Lam a t = Lam b s"
@@ -43,9 +83,28 @@
 
 (* Construction Site code *)
 
-lemma perm_rsp: "op = ===> alpha ===> alpha op \<bullet> op \<bullet>" sorry
-lemma fresh_rsp: "op = ===> (alpha ===> op =) fresh fresh" sorry
-lemma rLam_rsp: "op = ===> (alpha ===> alpha) rLam rLam" sorry
+lemma perm_rsp: "op = ===> alpha ===> alpha op \<bullet> op \<bullet>"
+  apply(auto)
+  (* this is propably true if some type conditions are imposed ;o) *)
+  sorry
+
+lemma fresh_rsp: "op = ===> (alpha ===> op =) fresh fresh" 
+  apply(auto)
+  (* this is probably only true if some type conditions are imposed *)
+  sorry
+
+lemma rLam_rsp: "op = ===> (alpha ===> alpha) rLam rLam"
+  apply(auto)
+  apply(rule a3)
+  apply(rule_tac t="[(x,x)]\<bullet>y" and s="y" in subst)
+  apply(rule sym)
+  apply(rule trans)
+  apply(rule pt_name3)
+  apply(rule at_ds1[OF at_name_inst])
+  apply(simp add: pt_name1)
+  apply(assumption)
+  apply(simp add: abs_fresh)
+  done
 
 ML {* val defs = @{thms Var_def App_def Lam_def} *}
 ML {* val consts = [@{const_name "rVar"}, @{const_name "rApp"}, @{const_name "rLam"}]; *}