diff -r 0f920b62fb7b -r 7bac7dffadeb Quot/Examples/LamEx.thy --- a/Quot/Examples/LamEx.thy Fri Jan 15 12:17:30 2010 +0100 +++ b/Quot/Examples/LamEx.thy Fri Jan 15 15:51:25 2010 +0100 @@ -360,26 +360,49 @@ apply(simp add: var_supp1) done +(* lemma hom_reg: *) lemma hom: " -\<forall>f_lam \<in> Respects((op = ===> alpha) ===> op =). -\<forall>f_app \<in> Respects(alpha ===> alpha ===> op =). - \<exists>hom \<in> Respects(alpha ===> op =). ( + \<exists>hom\<in>Respects (alpha ===> op =). ( (\<forall>x. hom (rVar x) = f_var x) \<and> (\<forall>l r. hom (rApp l r) = f_app l r (hom l) (hom r)) \<and> (\<forall>x a. hom (rLam a x) = f_lam (\<lambda>b. ([(a,b)]\<bullet> x)) (\<lambda>b. hom ([(a,b)] \<bullet> x))) )" sorry +lemma hom_reg:" +(\<exists>hom\<in>Respects (alpha ===> op =). + (\<forall>x. hom (rVar x) = f_var x) \<and> + (\<forall>l r. hom (rApp l r) = f_app l r (hom l) (hom r)) \<and> + (\<forall>xa a. hom (rLam a xa) = f_lam (\<lambda>b. [(a, b)] \<bullet> xa) (\<lambda>b. hom ([(a, b)] \<bullet> xa)))) \<longrightarrow> +(\<exists>hom. + (\<forall>x. hom (rVar x) = f_var x) \<and> + (\<forall>l r. hom (rApp l r) = f_app l r (hom l) (hom r)) \<and> + (\<forall>xa a. hom (rLam a xa) = f_lam (\<lambda>b. [(a, b)] \<bullet> xa) (\<lambda>b. hom ([(a, b)] \<bullet> xa))))" +by(regularize) + +thm impE[OF hom_reg] +lemma hom_pre:" +(\<exists>hom. + (\<forall>x. hom (rVar x) = f_var x) \<and> + (\<forall>l r. hom (rApp l r) = f_app l r (hom l) (hom r)) \<and> + (\<forall>xa a. hom (rLam a xa) = f_lam (\<lambda>b. [(a, b)] \<bullet> xa) (\<lambda>b. hom ([(a, b)] \<bullet> xa))))" +apply (rule impE[OF hom_reg]) +apply (rule hom) +apply (assumption) +done + lemma hom': -"\<forall>f_lam. \<forall>f_app. \<exists>hom. ( +"\<exists>hom. ( (\<forall>x. hom (Var x) = f_var x) \<and> (\<forall>l r. hom (App l r) = f_app l r (hom l) (hom r)) \<and> (\<forall>x a. hom (Lam a x) = f_lam (\<lambda>b. ([(a,b)] \<bullet> x)) (\<lambda>b. hom ([(a,b)] \<bullet> x))) )" -(*apply (lifting hom)*) -sorry +apply (lifting hom) +done -thm rlam.recs +thm bex_reg_eqv_range[OF identity_equivp, of "alpha"] + end +