# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1256640182 -3600
# Node ID 1ac36993cc711c309cd8c0211592c1e0c62c71fb
# Parent  d6a24dad5882c846d52f1c959ab16ffefff783ca
added an example about lambda-terms

diff -r d6a24dad5882 -r 1ac36993cc71 LamEx.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/LamEx.thy	Tue Oct 27 11:43:02 2009 +0100
@@ -0,0 +1,31 @@
+theory LamEx
+imports Nominal QuotMain
+begin
+
+atom_decl name
+
+nominal_datatype rlam =
+  rVar "name"
+| rApp "rlam" "rlam"
+| rLam "name" "rlam"
+
+inductive 
+  alpha :: "rlam \<Rightarrow> rlam \<Rightarrow> bool" ("_ \<approx> _" [100, 100] 100)
+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"
+
+quotient lam = rlam / alpha
+sorry
+
+local_setup {*
+  make_const_def @{binding Var} @{term "rVar"} NoSyn @{typ "rlam"} @{typ "lam"} #> snd #>
+  make_const_def @{binding App} @{term "rApp"} NoSyn @{typ "rlam"} @{typ "lam"} #> snd #>
+  make_const_def @{binding Lam} @{term "rLam"} NoSyn @{typ "rlam"} @{typ "lam"} #> snd
+*}
+
+lemma real_alpha:
+  assumes "t = ([(a,b)]\<bullet>s)" "a\<sharp>s"
+  shows "Lam a t = Lam b s"
+sorry
\ No newline at end of file