# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1260157302 -3600
# Node ID 66f39908df953ba55e7c556b0c33a1841218b924
# Parent  01a0da807f50b505957d110f0599a860d0663c8f# Parent  951681538e3f37644cfef9155beaefabfd432dfd
merge

diff -r 951681538e3f -r 66f39908df95 IntEx.thy
--- a/IntEx.thy	Mon Dec 07 02:34:24 2009 +0100
+++ b/IntEx.thy	Mon Dec 07 04:41:42 2009 +0100
@@ -228,3 +228,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
+