# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1264257714 -3600
# Node ID a7bf638e9af329b06be9d27c70a0642d622385c0
# Parent  16082d0b8ac1c773d8627e242c9cb9c60e29819c
More experiments with defining the homomorphism directly, lifting of 'distinct' and of 'exhaust'.

diff -r 16082d0b8ac1 -r a7bf638e9af3 Quot/Examples/LamEx.thy
--- a/Quot/Examples/LamEx.thy	Sat Jan 23 07:22:27 2010 +0100
+++ b/Quot/Examples/LamEx.thy	Sat Jan 23 15:41:54 2010 +0100
@@ -318,16 +318,45 @@
 apply(simp_all)
 done
 
+lemma rlam_distinct:
+  shows "\<not>(rVar nam \<approx> rApp rlam1' rlam2')"
+  and   "\<not>(rApp rlam1' rlam2' \<approx> rVar nam)"
+  and   "\<not>(rVar nam \<approx> rLam nam' rlam')"
+  and   "\<not>(rLam nam' rlam' \<approx> rVar nam)"
+  and   "\<not>(rApp rlam1 rlam2 \<approx> rLam nam' rlam')"
+  and   "\<not>(rLam nam' rlam' \<approx> rApp rlam1 rlam2)"
+apply auto
+apply(erule alpha.cases)
+apply simp_all
+apply(erule alpha.cases)
+apply simp_all
+apply(erule alpha.cases)
+apply simp_all
+apply(erule alpha.cases)
+apply simp_all
+apply(erule alpha.cases)
+apply simp_all
+apply(erule alpha.cases)
+apply simp_all
+done
+
+lemma lam_distinct[simp]:
+  shows "Var nam \<noteq> App lam1' lam2'"
+  and   "App lam1' lam2' \<noteq> Var nam"
+  and   "Var nam \<noteq> Lam nam' lam'"
+  and   "Lam nam' lam' \<noteq> Var nam"
+  and   "App lam1 lam2 \<noteq> Lam nam' lam'"
+  and   "Lam nam' lam' \<noteq> App lam1 lam2"
+apply(lifting rlam_distinct(1) rlam_distinct(2) rlam_distinct(3) rlam_distinct(4) rlam_distinct(5) rlam_distinct(6))
+done
+
 lemma var_supp1:
   shows "(supp (Var a)) = ((supp a)::name set)"
-apply(simp add: supp_def)
-done
+  by (simp add: supp_def)
 
 lemma var_supp:
   shows "(supp (Var a)) = {a::name}"
-using var_supp1
-apply(simp add: supp_atm)
-done
+  using var_supp1 by (simp add: supp_atm)
 
 lemma app_supp:
   shows "supp (App t1 t2) = (supp t1) \<union> ((supp t2)::name set)"
@@ -490,12 +519,21 @@
 done
 
 termination term1_hom
-  apply -
   apply(relation "measure (\<lambda>(f1, f2, f3, t). size t)")
 apply(auto simp add: pi_size)
 done
 
-(*
+lemma lam_exhaust:
+  "\<lbrakk>\<And>name. y = Var name \<Longrightarrow> P; \<And>rlam1 rlam2. y = App rlam1 rlam2 \<Longrightarrow> P; \<And>name rlam. y = Lam name rlam \<Longrightarrow> P\<rbrakk>
+    \<Longrightarrow> P"
+apply(lifting rlam.exhaust)
+done
+
+(* THIS IS NOT TRUE, but it lets prove the existence of the hom function *)
+lemma lam_inject':
+  "(Lam a x = Lam b y) = ((\<lambda>c. [(a, c)] \<bullet> x) = (\<lambda>c. [(b, c)] \<bullet> y))"
+sorry
+
 function
   hom :: "(name \<Rightarrow> 'a) \<Rightarrow>
                 (lam \<Rightarrow> lam \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow>
@@ -504,10 +542,33 @@
   "hom f_var f_app f_lam (Var x) = f_var x"
 | "hom f_var f_app f_lam (App l r) = f_app l r (hom f_var f_app f_lam l) (hom f_var f_app f_lam r)"
 | "hom f_var f_app f_lam (Lam a x) = f_lam (\<lambda>b. ([(a,b)] \<bullet> x)) (\<lambda>b. hom f_var f_app f_lam ([(a,b)] \<bullet> x))"
-apply(pat_completeness)
-apply(auto)
+defer
+apply(simp_all add: lam_inject') (* inject, distinct *)
+apply(tactic {* Cong_Tac.cong_tac @{thm cong} 1 *})
+apply(rule refl)
+apply(rule ext)
+apply(tactic {* Cong_Tac.cong_tac @{thm cong} 1 *})
+apply simp_all
+apply(erule conjE)+
+apply(rule_tac x="b" in cong)
+apply simp_all
+apply auto
+apply(rule_tac y="b" in lam_exhaust)
+apply simp_all
+apply auto
+apply meson
+apply(simp_all add: lam_inject')
+apply metis
 done
+
+termination hom
+  apply -
+(*
+ML_prf {* Size.size_thms @{theory} "LamEx.lam" *}
 *)
+sorry
+
+thm hom.simps
 
 lemma term1_hom_rsp:
   "\<lbrakk>(alpha ===> alpha ===> op =) f_app f_app; ((op = ===> alpha) ===> op =) f_lam f_lam\<rbrakk>