--- a/FSet.thy	Sat Oct 24 14:00:18 2009 +0200
+++ b/FSet.thy	Sat Oct 24 16:15:58 2009 +0200
@@ -252,15 +252,22 @@
   apply (metis cons_rsp)
   done
 
-lemma append_respects_fst:
+lemma append_rsp_fst:
   assumes a : "list_eq l1 l2"
   shows "list_eq (l1 @ s) (l2 @ s)"
   using a
   apply(induct)
   apply(auto intro: list_eq.intros)
-  apply(simp add: list_eq_refl)
+  apply(rule list_eq_refl)
 done
 
+lemma "(a @ b) \<approx> (b @ a)"
+sorry
+
+lemma (* ho_append_rsp: *)
+  "op \<approx> ===> op \<approx> ===> op \<approx> op @ op @"
+sorry
+
 thm list.induct
 lemma list_induct_hol4:
   fixes P :: "'a list \<Rightarrow> bool"
@@ -281,8 +288,8 @@
        (asm_full_simp_tac ((Simplifier.context ctxt HOL_ss) addsimps
         [(@{thm equiv_res_forall} OF [rel_eqv]),
          (@{thm equiv_res_exists} OF [rel_eqv])])) THEN_ALL_NEW
-         (((rtac @{thm RIGHT_RES_FORALL_REGULAR}) THEN' (RANGE [fn _ => all_tac, atac])) ORELSE'
-         (MetisTools.metis_tac ctxt []));
+         (((rtac @{thm RIGHT_RES_FORALL_REGULAR}) THEN' (RANGE [fn _ => all_tac, atac]) THEN'
+         (MetisTools.metis_tac ctxt [])) ORELSE' (MetisTools.metis_tac ctxt []));
     val cthm = Goal.prove lthy [] [] g (fn x => tac (#context x) 1);
   in
     cthm OF [thm]
@@ -388,8 +395,6 @@
     ])
 *}
 
-ML Goal.prove
-
 ML {*
 fun repabs_eq lthy thm constructors rty qty quot_thm reflex_thm trans_thm rsp_thms =
   let
@@ -469,15 +474,41 @@
 
 text {* the proper way to do it *}
 ML {*
+  fun findabs rty tm =
+    case tm of
+      Abs(_, T, b) =>
+        let
+          val b' = subst_bound ((Free ("x", T)), b);
+          val tys = findabs rty b'
+          val ty = fastype_of tm
+        in if needs_lift rty ty then (ty :: tys) else tys
+        end
+    | f $ a => (findabs rty f) @ (findabs rty a)
+    | _ => []
+*}
+
+ML {* findabs @{typ "'a list"} (prop_of (atomize_thm @{thm list_induct_hol4})) *}
+
+ML {*
  val lpi = Drule.instantiate'
-   [SOME @{ctyp "'a list"}, SOME @{ctyp "'a fset"}, SOME @{ctyp "bool"}, SOME @{ctyp "bool"}] [] @{thm LAMBDA_PRS};
+   [SOME @{ctyp "'a list"}, NONE, SOME @{ctyp "bool"}, NONE] [] @{thm LAMBDA_PRS};
 *}
-prove asdfasdf : {* concl_of lpi *}
+prove lambda_prs_l_b : {* concl_of lpi *}
 apply (tactic {* compose_tac (false, @{thm LAMBDA_PRS}, 2) 1 *})
 apply (tactic {* quotient_tac @{thm QUOTIENT_fset} 1 *})
 apply (tactic {* quotient_tac @{thm QUOTIENT_fset} 1 *})
 done
-thm HOL.sym[OF asdfasdf,simplified]
+thm HOL.sym[OF lambda_prs_l_b,simplified]
+ML {*
+ val lpi = Drule.instantiate'
+   [SOME @{ctyp "'a list \<Rightarrow> bool"}, NONE, SOME @{ctyp "bool"}, NONE] [] @{thm LAMBDA_PRS};
+*}
+prove lambda_prs_lb_b : {* concl_of lpi *}
+apply (tactic {* compose_tac (false, @{thm LAMBDA_PRS}, 2) 1 *})
+apply (tactic {* quotient_tac @{thm QUOTIENT_fset} 1 *})
+apply (tactic {* quotient_tac @{thm QUOTIENT_fset} 1 *})
+done
+thm HOL.sym[OF lambda_prs_lb_b,simplified]
 
 ML {*
 fun eqsubst_thm ctxt thms thm =
@@ -494,11 +525,12 @@
   end
 *}
 
-(* @{thms HOL.sym[OF asdfasdf,simplified]} *)
 
 ML {*
-  fun simp_lam_prs lthy thm = 
-    simp_lam_prs lthy (eqsubst_thm lthy [lam_prs] thm)
+  fun simp_lam_prs lthy thm =
+    simp_lam_prs lthy (eqsubst_thm lthy
+      @{thms HOL.sym[OF lambda_prs_lb_b,simplified] HOL.sym[OF lambda_prs_l_b,simplified]}
+    thm)
     handle _ => thm
 *}
 
@@ -544,8 +576,8 @@
 
 
 ML {* val card1_suc_t_n = @{thm card1_suc_t} *}
-ML {* val card1_suc_t' = eqsubst_thm @{context} @{thms HOL.sym[OF asdfasdf,simplified]} @{thm card1_suc_t} *}
-ML {* val card1_suc_t'' = eqsubst_thm @{context} @{thms HOL.sym[OF asdfasdf,simplified]} card1_suc_t' *}
+ML {* val card1_suc_t' = eqsubst_thm @{context} @{thms HOL.sym[OF lambda_prs_l_b,simplified]} @{thm card1_suc_t} *}
+ML {* val card1_suc_t'' = eqsubst_thm @{context} @{thms HOL.sym[OF lambda_prs_l_b,simplified]} card1_suc_t' *}
 ML {* val ithm = simp_allex_prs @{context} card1_suc_t'' *}
 ML {* val rthm = MetaSimplifier.rewrite_rule fset_defs_sym ithm *}
 ML {* val qthm = MetaSimplifier.rewrite_rule @{thms QUOT_TYPE_I_fset.REPS_same} rthm *}
@@ -554,10 +586,15 @@
 thm fold1.simps(2)
 thm list.recs(2)
 
-ML {* val ind_r_a = atomize_thm @{thm m2} *}
-  (* prove {* build_regularize_goal ind_r_a @{typ "'a List.list"} @{term "op \<approx>"} @{context} *}
-  apply (simp add: equiv_res_forall[OF equiv_list_eq] equiv_res_exists[OF equiv_list_eq]) done *)
-
+ML {* val ind_r_a = atomize_thm @{thm list_induct_hol4} *}
+(*  prove {* build_regularize_goal ind_r_a @{typ "'a List.list"} @{term "op \<approx>"} @{context} *}
+  ML_prf {*  fun tac ctxt =
+       (asm_full_simp_tac ((Simplifier.context ctxt HOL_ss) addsimps
+        [(@{thm equiv_res_forall} OF [@{thm equiv_list_eq}]),
+         (@{thm equiv_res_exists} OF [@{thm equiv_list_eq}])])) THEN_ALL_NEW
+         (((rtac @{thm RIGHT_RES_FORALL_REGULAR}) THEN' (RANGE [fn _ => all_tac, atac]) THEN'
+         (MetisTools.metis_tac ctxt [])) ORELSE' (MetisTools.metis_tac ctxt [])); *}
+  apply (tactic {* tac @{context} 1 *}) *)
 ML {* val ind_r_r = regularize ind_r_a @{typ "'a List.list"} @{term "op \<approx>"} @{thm equiv_list_eq} @{context} *}
 ML {*
   val rt = build_repabs_term @{context} ind_r_r consts @{typ "'a list"} @{typ "'a fset"}
@@ -590,6 +627,9 @@
 ML {* val ind_r_a = simp_allex_prs @{context} ind_r_l *}
 ML {* val ind_r_d = MetaSimplifier.rewrite_rule fset_defs_sym ind_r_a *}
 ML {* val ind_r_s = MetaSimplifier.rewrite_rule @{thms QUOT_TYPE_I_fset.REPS_same} ind_r_d *}
+lemma app_prs_for_induct: "(ABS_fset ---> id) f (REP_fset T1) = f T1"
+  apply (simp add: fun_map.simps QUOT_TYPE_I_fset.thm10)
+done
 
 ML {*
 fun lift thm =
@@ -614,7 +654,8 @@
 ML {* lift @{thm m1} *}
 ML {* lift @{thm list_eq.intros(4)} *}
 ML {* lift @{thm list_eq.intros(5)} *}
-(* ML {* lift @{thm length_append} *} *)
+ML {* lift @{thm card1_suc} *}
+(* ML {* lift @{thm append_assoc} *} *)
 
 (*notation ( output) "prop" ("#_" [1000] 1000) *)
 notation ( output) "Trueprop" ("#_" [1000] 1000)