diff -r fe6eb116b341 -r c55883442514 LamEx.thy --- a/LamEx.thy Tue Nov 03 17:30:27 2009 +0100 +++ b/LamEx.thy Tue Nov 03 17:30:43 2009 +0100 @@ -37,17 +37,17 @@ print_quotients -quotient_def (for lam) +quotient_def Var :: "name \<Rightarrow> lam" where "Var \<equiv> rVar" -quotient_def (for lam) +quotient_def App :: "lam \<Rightarrow> lam \<Rightarrow> lam" where "App \<equiv> rApp" -quotient_def (for lam) +quotient_def Lam :: "name \<Rightarrow> lam \<Rightarrow> lam" where "Lam \<equiv> rLam" @@ -56,7 +56,7 @@ thm App_def thm Lam_def -quotient_def (for lam) +quotient_def fv :: "lam \<Rightarrow> name set" where "fv \<equiv> rfv" @@ -66,10 +66,10 @@ (* definition of overloaded permutation function *) (* for the lifted type lam *) overloading - perm_lam \<equiv> "perm :: 'x prm \<Rightarrow> lam \<Rightarrow> lam" (unchecked) + perm_lam \<equiv> "perm :: 'x prm \<Rightarrow> lam \<Rightarrow> lam" (unchecked) begin -quotient_def (for lam) +quotient_def perm_lam :: "'x prm \<Rightarrow> lam \<Rightarrow> lam" where "perm_lam \<equiv> (perm::'x prm \<Rightarrow> rlam \<Rightarrow> rlam)" @@ -308,14 +308,11 @@ thm alpha.induct lemma rvar_inject: "rVar a \<approx> rVar b \<Longrightarrow> (a = b)" -apply (rule alpha.cases) -apply (assumption) -apply (assumption) -apply (simp_all) -apply (cases "a = b") -apply (simp_all) -apply (cases "ba = b") -apply (simp_all) +apply (erule alpha.cases) +apply (simp add: rlam.inject) +apply (simp) +apply (simp) +done lemma var_inject_test: