# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1260157182 -3600
# Node ID 01a0da807f50b505957d110f0599a860d0663c8f
# Parent  b16cac0b7c884a6b68bc2f52e8b9569dc129f5cd
3 new example thms in MyInt; reveal problems with handling of lambdas; regularize fails with "Loose Bound".

diff -r b16cac0b7c88 -r 01a0da807f50 IntEx.thy
--- a/IntEx.thy	Mon Dec 07 00:03:12 2009 +0100
+++ b/IntEx.thy	Mon Dec 07 04:39:42 2009 +0100
@@ -257,3 +257,49 @@
 apply(simp only: foldl_prs[OF Quotient_my_int Quotient_my_int] cons_prs[OF Quotient_my_int])
 done
 
+lemma ho_tst3: "foldl f (s::nat \<times> nat) ([]::(nat \<times> nat) list) = s"
+by simp
+
+lemma "foldl f (x::my_int) ([]::my_int list) = x"
+apply(tactic {* procedure_tac @{context} @{thm ho_tst3} 1 *})
+apply(tactic {* regularize_tac @{context} 1 *})
+apply(tactic {* all_inj_repabs_tac_intex @{context} 1*})
+(* TODO: does not work when this is added *)
+(* apply(tactic {* lambda_prs_tac @{context} 1 *})*)
+apply(tactic {* clean_tac @{context} 1 *})
+apply(simp only: foldl_prs[OF Quotient_my_int Quotient_my_int] nil_prs[OF Quotient_my_int])
+done
+
+lemma lam_tst: "(\<lambda>x. (x, x)) y = (y, (y :: nat \<times> nat))"
+by simp
+
+lemma "(\<lambda>x. (x, x)) (y::my_int) = (y, y)"
+apply(tactic {* procedure_tac @{context} @{thm lam_tst} 1 *})
+defer
+apply(tactic {* inj_repabs_tac_intex @{context} 1*})
+apply(tactic {* inj_repabs_tac_intex @{context} 1*})
+apply(tactic {* inj_repabs_tac_intex @{context} 1*})
+apply(simp only: prod_rel.simps)
+defer
+apply(tactic {* clean_tac @{context} 1 *})
+apply(simp add: prod_rel.simps)
+apply(tactic {* clean_tac @{context} 1 *})
+apply(simp)
+(*apply(tactic {* regularize_tac @{context} 1 *})
+apply(tactic {* inj_repabs_tac_intex @{context} 1*})*)
+sorry
+
+lemma lam_tst2: "(\<lambda>(y :: nat \<times> nat). y) = (\<lambda>(x :: nat \<times> nat). x)"
+by simp
+
+lemma "(\<lambda>(y :: my_int). y) = (\<lambda>(x :: my_int). x)"
+apply(tactic {* ObjectLogic.full_atomize_tac 1 *})
+apply(tactic {* gen_frees_tac @{context} 1 *})
+ML_prf {* procedure_inst @{context} (prop_of @{thm lam_tst2}) @{prop "(\<lambda>(y :: my_int). y) = (\<lambda>(x :: my_int). x)"} *}
+
+apply(tactic {* procedure_tac @{context} @{thm lam_tst2} 1 *})
+apply(tactic {* regularize_tac @{context} 1 *})
+apply(tactic {* all_inj_repabs_tac_intex @{context} 1*})
+apply(tactic {* clean_tac @{context} 1 *})
+done
+