--- a/LamEx.thy	Thu Oct 29 13:29:03 2009 +0100
+++ b/LamEx.thy	Thu Oct 29 13:30:11 2009 +0100
@@ -133,25 +133,104 @@
 
 ML {* add_lower_defs @{context} @{thms perm_lam_def} *}
 ML {* val rr = @{thm eq_reflection} OF [hd (rev (add_lower_defs @{context} @{thms perm_lam_def}))] *}
-lemma prod_fun_id: "prod_fun id id = id"
-  apply (simp add: prod_fun_def)
-done
-lemma map_id: "map id x = x"
-  apply (induct x)
-  apply (simp_all add: map.simps)
-done
+
 ML {* val rrr = repeat_eqsubst_thm @{context} @{thms prod_fun_id map_id} rr *}
 ML {*
 fun lift_thm_lam lthy t =
   lift_thm lthy consts rty qty rel rel_eqv rel_refl quot rsp_thms trans2 reps_same defs t
 *}
-ML {* val t1 = Toplevel.program (fn () => lift_thm_lam @{context} @{thm pi_var_com}) *}
-ML {* val t2 = eqsubst_thm @{context} [rrr] (atomize_thm t1) *}
-ML {* ObjectLogic.rulify t2 *}
-ML {* val t1 = Toplevel.program (fn () => lift_thm_lam @{context} @{thm pi_app_com}) *}
-ML {* val t2 = repeat_eqsubst_thm @{context} [rrr] (atomize_thm t1) *}
-ML {* ObjectLogic.rulify t2 *}
-ML {* val t1 = Toplevel.program (fn () => lift_thm_lam @{context} @{thm pi_lam_com}) *}
-ML {* val t2 = repeat_eqsubst_thm @{context} [rrr] (atomize_thm t1) *}
-ML {* ObjectLogic.rulify t2 *}
+
+ML {* lift_thm_lam @{context} @{thm pi_var_com} *}
+ML {* lift_thm_lam @{context} @{thm pi_app_com} *}
+ML {* lift_thm_lam @{context} @{thm pi_lam_com} *}
+
+fun
+  option_map::"('a \<Rightarrow> 'b) \<Rightarrow> ('a noption) \<Rightarrow> ('b noption)"
+where
+  "option_map f (nSome x) = nSome (f x)"
+| "option_map f nNone = nNone"
+
+fun
+  option_rel
+where
+  "option_rel r (nSome x) (nSome y) = r x y"
+| "option_rel r _ _ = False"
+
+declare [[map noption = (option_map, option_rel)]]
+
+lemma OPT_QUOTIENT:
+  assumes q: "QUOTIENT R Abs Rep"
+  shows "QUOTIENT (option_rel R) (option_map Abs) (option_map Rep)"
+  apply (unfold QUOTIENT_def)
+  apply (auto)
+  using q
+  apply (unfold QUOTIENT_def)
+  apply (case_tac "a :: 'b noption")
+  apply (simp)
+  apply (simp)
+  apply (case_tac "a :: 'b noption")
+  apply (simp only: option_map.simps)
+  apply (subst option_rel.simps)
+  (* Simp starts hanging so don't know how to continue *)
+  sorry
+
+(* Christian: Does it make sense? *)
+lemma abs_fun_rsp: "(op = ===> alpha ===> op = ===> op =) abs_fun abs_fun"
+sorry
+
+(* Should not be needed *)
+lemma eq_rsp2: "((op = ===> op =) ===> (op = ===> op =) ===> op =) op = op ="
+apply auto
+apply (rule ext)
+apply auto
+apply (rule ext)
+apply auto
+done
 
+(* Should not be needed *)
+lemma perm_rsp_eq: "(op = ===> (op = ===> op =) ===> op = ===> op =) op \<bullet> op \<bullet>"
+apply auto
+thm arg_cong2
+apply (rule_tac f="perm x" in arg_cong2)
+apply (auto)
+apply (rule ext)
+apply (auto)
+done
+
+(* Should not be needed *)
+lemma fresh_rsp_eq: "(op = ===> (op = ===> op =) ===> op =) fresh fresh"
+apply (simp add: FUN_REL.simps)
+apply (metis ext)
+done
+
+(* It is just a test, it doesn't seem true... *)
+lemma quotient_cheat: "QUOTIENT op = (option_map ABS_lam) (option_map REP_lam)"
+sorry
+
+
+ML {* val rsp_thms = @{thms abs_fun_rsp OPT_QUOTIENT eq_rsp2 quotient_cheat perm_rsp_eq fresh_rsp_eq} @ rsp_thms *}
+ML {*
+fun lift_thm_lam lthy t =
+  lift_thm lthy consts rty qty rel rel_eqv rel_refl quot rsp_thms trans2 reps_same defs t
+*}
+
+thm a3
+ML {* Toplevel.program (fn () => lift_thm_lam @{context} @{thm a3}) *}
+ML {* val t_u = MetaSimplifier.rewrite_rule @{thms fresh_def supp_def} @{thm a3} *}
+ML {* Toplevel.program (fn () => lift_thm_lam @{context} t_u) *}
+
+ML t_u
+ML {* val t_a = atomize_thm t_u *}
+ML {* val t_r = regularize t_a rty rel rel_eqv @{context} *}
+ML {* val t = (fst o Thm.dest_comb o snd o Thm.dest_comb) (cprop_of t_u) *}
+ML {* val t = (snd o Thm.dest_comb o snd o Thm.dest_comb) t *}
+ML {* val t = (snd o Thm.dest_comb o snd o Thm.dest_comb) t *}
+ML {* val t = (snd o (Thm.dest_abs NONE) o snd o Thm.dest_comb) t *}
+ML {* val t = (snd o Thm.dest_comb o snd o Thm.dest_comb) t *}
+ML {* val t = (snd o (Thm.dest_abs NONE) o snd o Thm.dest_comb) t *}
+ML {* val t = (fst o Thm.dest_comb o snd o Thm.dest_comb) t *}
+ML {* term_of t *}
+term "[b].(s::rlam)"
+thm abs_fun_def
+ML {* val t_t = repabs @{context} t_r consts rty qty quot rel_refl trans2 rsp_thms *}
+