Quot/Examples/LamEx.thy
changeset 901 28e084a66c7f
parent 900 3bd2847cfda7
child 902 82cdc3755c2c
equal deleted inserted replaced
900:3bd2847cfda7 901:28e084a66c7f
   465 apply(clarify)
   465 apply(clarify)
   466 apply(simp)
   466 apply(simp)
   467 (* probably true *)
   467 (* probably true *)
   468 sorry
   468 sorry
   469 
   469 
       
   470 
       
   471 
   470 lemma hom: 
   472 lemma hom: 
   471   "\<exists>hom\<in>Respects (alpha ===> op =). 
   473   "\<exists>hom\<in>Respects (alpha ===> op =). 
   472     ((\<forall>x. hom (rVar x) = f_var x) \<and>
   474     ((\<forall>x. hom (rVar x) = f_var x) \<and>
   473      (\<forall>l r. hom (rApp l r) = f_app l r (hom l) (hom r)) \<and>
   475      (\<forall>l r. hom (rApp l r) = f_app l r (hom l) (hom r)) \<and>
   474      (\<forall>x a. hom (rLam a x) = f_lam (\<lambda>b. ([(a,b)]\<bullet> x)) (\<lambda>b. hom ([(a,b)] \<bullet> x))))"
   476      (\<forall>x a. hom (rLam a x) = f_lam (\<lambda>b. ([(a,b)]\<bullet> x)) (\<lambda>b. hom ([(a,b)] \<bullet> x))))"
   477 apply(simp)
   479 apply(simp)
   478 apply(rule conjI)
   480 apply(rule conjI)
   479 apply(simp)
   481 apply(simp)
   480 apply(simp)
   482 apply(simp)
   481 sorry
   483 sorry
       
   484 
       
   485 function
       
   486   term1_hom :: "(name \<Rightarrow> 'a) \<Rightarrow> (rlam \<Rightarrow> rlam \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> ((name \<Rightarrow> rlam) \<Rightarrow> (name \<Rightarrow> 'a) \<Rightarrow> 'a) \<Rightarrow> rlam \<Rightarrow> 'a"
       
   487 where
       
   488   "term1_hom var app abs' (rVar x) = (var x)"
       
   489 | "term1_hom var app abs' (rApp t u) =
       
   490      app t u (term1_hom var app abs' t) (term1_hom var app abs' u)"
       
   491 | "term1_hom var app abs' (rLam x u) =
       
   492      abs' (\<lambda>y. [(x, y)] \<bullet> u) (\<lambda>y. term1_hom var app abs' ([(x, y)] \<bullet> u))"
       
   493 sorry
       
   494 
       
   495 print_theorems
   482 
   496 
   483 lemma hom_res: "
   497 lemma hom_res: "
   484 \<forall>f_var. \<forall>f_app \<in> Respects(alpha ===> alpha ===> op =).
   498 \<forall>f_var. \<forall>f_app \<in> Respects(alpha ===> alpha ===> op =).
   485 \<forall>f_lam \<in> Respects((op = ===> alpha) ===> op =).
   499 \<forall>f_lam \<in> Respects((op = ===> alpha) ===> op =).
   486 \<exists>hom\<in>Respects (alpha ===> op =). 
   500 \<exists>hom\<in>Respects (alpha ===> op =). 
   487     ((\<forall>x. hom (rVar x) = f_var x) \<and>
   501     ((\<forall>x. hom (rVar x) = f_var x) \<and>
   488      (\<forall>l r. hom (rApp l r) = f_app l r (hom l) (hom r)) \<and>
   502      (\<forall>l r. hom (rApp l r) = f_app l r (hom l) (hom r)) \<and>
   489      (\<forall>x a. hom (rLam a x) = f_lam (\<lambda>b. ([(a,b)]\<bullet> x)) (\<lambda>b. hom ([(a,b)] \<bullet> x))))"
   503      (\<forall>x a. hom (rLam a x) = f_lam (\<lambda>b. ([(a,b)]\<bullet> x)) (\<lambda>b. hom ([(a,b)] \<bullet> x))))"
   490 apply(rule allI)
   504 apply(rule allI)
   491 apply(rule ballI)+
   505 apply(rule ballI)+
   492 apply(rule_tac x="rlam_rec f_var f_app XX" in bexI)
   506 apply(rule_tac x="term1_hom f_var f_app f_lam" in bexI)
   493 apply(rule conjI)
   507 apply(rule conjI)
   494 apply(simp)
   508 (* apply(simp add: term1_hom.psimps) *)
   495 apply(rule conjI)
   509 prefer 2
   496 apply(simp)
   510 apply(rule conjI)
   497 apply(simp_all only: in_respects)
   511 (* apply(simp add: term1_hom.psimps) *)
   498 sorry
   512 sorry
   499 
   513 
   500 lemma hom':
   514 lemma hom':
   501 "\<exists>hom. 
   515 "\<exists>hom. 
   502   ((\<forall>x. hom (Var x) = f_var x) \<and>
   516   ((\<forall>x. hom (Var x) = f_var x) \<and>