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 \ lam" where "Var \ rVar" -quotient_def (for lam) +quotient_def App :: "lam \ lam \ lam" where "App \ rApp" -quotient_def (for lam) +quotient_def Lam :: "name \ lam \ lam" where "Lam \ rLam" @@ -56,7 +56,7 @@ thm App_def thm Lam_def -quotient_def (for lam) +quotient_def fv :: "lam \ name set" where "fv \ rfv" @@ -66,10 +66,10 @@ (* definition of overloaded permutation function *) (* for the lifted type lam *) overloading - perm_lam \ "perm :: 'x prm \ lam \ lam" (unchecked) + perm_lam \ "perm :: 'x prm \ lam \ lam" (unchecked) begin -quotient_def (for lam) +quotient_def perm_lam :: "'x prm \ lam \ lam" where "perm_lam \ (perm::'x prm \ rlam \ rlam)" @@ -308,14 +308,11 @@ thm alpha.induct lemma rvar_inject: "rVar a \ rVar b \ (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: