# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1263921462 -3600
# Node ID 3bd2847cfda73e209b143c74a4af09db21c8d9aa
# Parent  2468c0f2b2762c76ae8eff1a9d97458adb480ede
A version of hom with quantifiers.

diff -r 2468c0f2b276 -r 3bd2847cfda7 Quot/Examples/LamEx.thy
--- a/Quot/Examples/LamEx.thy	Sun Jan 17 02:24:15 2010 +0100
+++ b/Quot/Examples/LamEx.thy	Tue Jan 19 18:17:42 2010 +0100
@@ -32,23 +32,23 @@
 declare perm_rlam.simps[eqvt]
 
 instance rlam::pt_name
-apply(default)
-apply(induct_tac [!] x rule: rlam.induct)
-apply(simp_all add: pt_name2 pt_name3)
-done
+  apply(default)
+  apply(induct_tac [!] x rule: rlam.induct)
+  apply(simp_all add: pt_name2 pt_name3)
+  done
 
 instance rlam::fs_name
-apply(default)
-apply(induct_tac [!] x rule: rlam.induct)
-apply(simp add: supp_def)
-apply(fold supp_def)
-apply(simp add: supp_atm)
-apply(simp add: supp_def Collect_imp_eq Collect_neg_eq)
-apply(simp add: supp_def)
-apply(simp add: supp_def Collect_imp_eq Collect_neg_eq[symmetric])
-apply(fold supp_def)
-apply(simp add: supp_atm)
-done
+  apply(default)
+  apply(induct_tac [!] x rule: rlam.induct)
+  apply(simp add: supp_def)
+  apply(fold supp_def)
+  apply(simp add: supp_atm)
+  apply(simp add: supp_def Collect_imp_eq Collect_neg_eq)
+  apply(simp add: supp_def)
+  apply(simp add: supp_def Collect_imp_eq Collect_neg_eq[symmetric])
+  apply(fold supp_def)
+  apply(simp add: supp_atm)
+  done
 
 declare set_diff_eqvt[eqvt]
 
@@ -480,33 +480,29 @@
 apply(simp)
 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)
-
-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_res: "
+\<forall>f_var. \<forall>f_app \<in> Respects(alpha ===> alpha ===> op =).
+\<forall>f_lam \<in> Respects((op = ===> 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))))"
+apply(rule allI)
+apply(rule ballI)+
+apply(rule_tac x="rlam_rec f_var f_app XX" in bexI)
+apply(rule conjI)
+apply(simp)
+apply(rule conjI)
+apply(simp)
+apply(simp_all only: in_respects)
+sorry
 
 lemma 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)
+apply (lifting hom_res)
 done
 
 (* test test