--- a/FSet.thy	Sat Oct 24 08:34:14 2009 +0200
+++ b/FSet.thy	Sat Oct 24 10:16:53 2009 +0200
@@ -235,6 +235,11 @@
   apply (simp_all add:memb_rsp)
   done
 
+lemma ho_card1_rsp: "op \<approx> ===> op = card1 card1"
+  apply (simp add: FUN_REL.simps)
+  apply (metis card1_rsp)
+  done
+
 lemma cons_rsp:
   fixes z
   assumes a: "xs \<approx> ys"
@@ -259,11 +264,32 @@
 thm list.induct
 lemma list_induct_hol4:
   fixes P :: "'a list \<Rightarrow> bool"
-  assumes "((P []) \<and> (\<forall>t. (P t) \<longrightarrow> (\<forall>h. (P (h # t)))))"
-  shows "(\<forall>l. (P l))"
-  sorry
+  assumes a: "((P []) \<and> (\<forall>t. (P t) \<longrightarrow> (\<forall>h. (P (h # t)))))"
+  shows "\<forall>l. (P l)"
+  using a
+  apply (rule_tac allI)
+  apply (induct_tac "l")
+  apply (simp)
+  apply (metis)
+  done
 
-ML {* atomize_thm @{thm list_induct_hol4} *}
+ML {*
+fun regularize thm rty rel rel_eqv lthy =
+  let
+    val g = build_regularize_goal thm rty rel lthy;
+    val tac =
+       (simp_tac ((Simplifier.context lthy HOL_ss) addsimps
+        [(@{thm equiv_res_forall} OF [rel_eqv]),
+         (@{thm equiv_res_exists} OF [rel_eqv])])) THEN'
+         (rtac @{thm RIGHT_RES_FORALL_REGULAR}) THEN'
+         (RANGE [fn _ => all_tac, atac]) THEN' (MetisTools.metis_tac lthy []);
+    val cgoal = cterm_of (ProofContext.theory_of lthy) g;
+    val cthm = Goal.prove_internal [] cgoal (fn _ => tac 1);
+  in
+    cthm OF [thm]
+  end
+*}
+
 
 prove list_induct_r: {*
    build_regularize_goal (atomize_thm @{thm list_induct_hol4}) @{typ "'a List.list"} @{term "op \<approx>"} @{context} *}
@@ -295,6 +321,14 @@
   (simp_tac ((Simplifier.context ctxt HOL_ss) addsimps @{thms FUN_REL.simps}))
 *}
 
+ML {*
+fun res_exists_rsp_tac ctxt =
+  (simp_tac ((Simplifier.context ctxt HOL_ss) addsimps @{thms FUN_REL.simps}))
+  THEN' rtac @{thm allI} THEN' rtac @{thm allI} THEN' rtac @{thm impI}
+  THEN' instantiate_tac @{thm RES_EXISTS_RSP} ctxt THEN'
+  (simp_tac ((Simplifier.context ctxt HOL_ss) addsimps @{thms FUN_REL.simps}))
+*}
+
 
 ML {*
 fun quotient_tac quot_thm =
@@ -314,9 +348,21 @@
   | _ => fn _ => no_tac) i st
 *}
 
+ML {*
+fun WEAK_LAMBDA_RES_TAC ctxt i st =
+  (case (term_of o #concl o fst) (Subgoal.focus ctxt i st) of
+    (_ $ (_ $ _$(Abs(_,_,_)))) =>
+      (EqSubst.eqsubst_tac ctxt [0] @{thms FUN_REL.simps}) THEN'
+      (rtac @{thm allI}) THEN' (rtac @{thm allI}) THEN' (rtac @{thm impI})
+  | (_ $ (_ $ (Abs(_,_,_))$_)) =>
+      (EqSubst.eqsubst_tac ctxt [0] @{thms FUN_REL.simps}) THEN'
+      (rtac @{thm allI}) THEN' (rtac @{thm allI}) THEN' (rtac @{thm impI})
+  | _ => fn _ => no_tac) i st
+*}
+
 
 ML {*
-fun r_mk_comb_tac ctxt quot_thm reflex_thm trans_thm res_thms =
+fun r_mk_comb_tac ctxt quot_thm reflex_thm trans_thm rsp_thms =
   (FIRST' [
     rtac @{thm FUN_QUOTIENT},
     rtac quot_thm,
@@ -325,8 +371,9 @@
     rtac trans_thm,
     LAMBDA_RES_TAC ctxt,
     res_forall_rsp_tac ctxt,
+    res_exists_rsp_tac ctxt,
     (
-     (simp_tac ((Simplifier.context @{context} HOL_ss) addsimps (res_thms @ @{thms ho_all_prs})))
+     (simp_tac ((Simplifier.context ctxt HOL_ss) addsimps (rsp_thms @ @{thms ho_all_prs ho_ex_prs})))
      THEN_ALL_NEW (fn _ => no_tac)
     ),
     (instantiate_tac @{thm REP_ABS_RSP(1)} ctxt THEN' (RANGE [quotient_tac quot_thm])),
@@ -337,13 +384,34 @@
     (
      (simp_tac ((Simplifier.context @{context} HOL_ss) addsimps @{thms FUN_REL.simps}))
      THEN_ALL_NEW (fn _ => no_tac)
-    )
+    ),
+    WEAK_LAMBDA_RES_TAC ctxt
     ])
 *}
 
+ML Goal.prove
+
+ML {*
+fun repabs lthy thm constructors rty qty quot_thm reflex_thm trans_thm rsp_thms =
+  let
+    val rt = build_repabs_term lthy thm constructors rty qty;
+    val rg = Logic.mk_equals ((Thm.prop_of thm), rt);
+    fun tac ctxt = (ObjectLogic.full_atomize_tac) THEN'
+      (REPEAT_ALL_NEW (r_mk_comb_tac ctxt quot_thm reflex_thm trans_thm rsp_thms));
+    val cthm = Goal.prove lthy [] [] rg (fn x => tac (#context x) 1);
+(*    val tac2 =
+     (simp_tac ((Simplifier.context lthy HOL_ss) addsimps [cthm]))
+     THEN' (rtac thm);
+    val cgoal = cterm_of (ProofContext.theory_of lthy) rt;
+    val cthm = Goal.prove_internal [] cgoal (fn _ => tac2); *)
+  in
+    cthm
+  end
+*}
+
 ML {*
 fun r_mk_comb_tac_fset ctxt =
-  r_mk_comb_tac ctxt @{thm QUOTIENT_fset} @{thm list_eq_refl} @{thm QUOT_TYPE_I_fset.R_trans2} @{thms ho_memb_rsp ho_cons_rsp}
+  r_mk_comb_tac ctxt @{thm QUOTIENT_fset} @{thm list_eq_refl} @{thm QUOT_TYPE_I_fset.R_trans2} @{thms ho_memb_rsp ho_cons_rsp ho_card1_rsp}
 *}
 
 
@@ -354,14 +422,6 @@
 ML {* trm_r *}
 prove list_induct_tr: trm_r
 apply (atomize(full))
-(* APPLY_RSP_TAC *)
-ML_prf {* val ctxt = @{context} *}
-apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *})
-(* LAMBDA_RES_TAC *)
-apply (subst FUN_REL.simps)
-apply (rule allI)
-apply (rule allI)
-apply (rule impI)
 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *})
 done
 
@@ -370,9 +430,16 @@
 apply (tactic {* rtac thm 1 *})
 done
 
-ML {* val nthm = MetaSimplifier.rewrite_rule fset_defs_sym (snd (no_vars (Context.Theory @{theory}, @{thm list_induct_t}))) *}
+ML {* val ind_r_a = atomize_thm @{thm list_induct_hol4} *}
+ML {* val ind_r_r = regularize ind_r_a @{typ "'a List.list"} @{term "op \<approx>"} @{thm equiv_list_eq} @{context} *}
+ML {* val ind_r_t =
+  repabs @{context} ind_r_r consts @{typ "'a list"} @{typ "'a fset"}
+   @{thm QUOTIENT_fset} @{thm list_eq_refl} @{thm QUOT_TYPE_I_fset.R_trans2}
+   @{thms ho_memb_rsp ho_cons_rsp ho_card1_rsp}
+*}
 
 thm list.recs(2)
+
 thm m2
 ML {* atomize_thm @{thm m2} *}
 
@@ -397,10 +464,9 @@
 lemma id_apply2 [simp]: "id x \<equiv> x"
   by (simp add: id_def)
 
-thm LAMBDA_PRS
 ML {*
  val t = prop_of @{thm LAMBDA_PRS}
- val tt = Drule.instantiate' [SOME @{ctyp "'a list"}, SOME @{ctyp "'a fset"}] [] @{thm LAMBDA_PRS}
+ val tt = Drule.instantiate' [SOME @{ctyp "'a list"}, SOME @{ctyp "'a fset"}, SOME @{ctyp "bool"}, SOME @{ctyp "bool"}] [] @{thm LAMBDA_PRS}
  val ttt = @{thm LAMBDA_PRS} OF [@{thm QUOTIENT_fset}, @{thm IDENTITY_QUOTIENT}]
  val tttt = @{thm "HOL.sym"} OF [ttt]
 *}
@@ -408,6 +474,13 @@
  val ttttt = MetaSimplifier.rewrite_rule [@{thm id_apply2}] tttt
  val zzz = @{thm m2_t}
 *}
+prove asdfasdf : {* concl_of tt *}
+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]
 
 ML {*
 fun eqsubst_thm ctxt thms thm =
@@ -423,9 +496,10 @@
     Simplifier.rewrite_rule [rt] thm
   end
 *}
-ML {* val m2_t' = eqsubst_thm @{context} [ttttt] @{thm m2_t} *}
+ML ttttt
+ML {* val m2_t' = eqsubst_thm @{context} @{thms HOL.sym[OF asdfasdf,simplified]} @{thm m2_t} *}
 ML {* val rwr = @{thm FORALL_PRS[OF QUOTIENT_fset]} *}
-ML {* val rwrs = @{thm "HOL.sym"} OF [ObjectLogic.rulify rwr] *}
+ML {* val rwrs = @{thm "HOL.sym"} OF [spec OF [rwr]] *}
 ML {* val ithm = eqsubst_thm @{context} [rwrs] m2_t' *}
 ML {* val rthm = MetaSimplifier.rewrite_rule fset_defs_sym ithm *}
 ML {* ObjectLogic.rulify rthm *}
@@ -433,14 +507,36 @@
 
 ML {* val card1_suc_f = Thm.freezeT (atomize_thm @{thm card1_suc}) *}
 
-prove card1_suc_r: {*
- Logic.mk_implies
-   ((prop_of card1_suc_f),
-   (regularise (prop_of card1_suc_f) @{typ "'a List.list"} @{term "op \<approx>"} @{context})) *}
+prove card1_suc_r_p: {*
+   build_regularize_goal (atomize_thm @{thm card1_suc}) @{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
+done
+
+ML {* val card1_suc_r = @{thm card1_suc_r_p} OF [atomize_thm @{thm card1_suc}] *}
+ML {* val card1_suc_t_g = build_repabs_goal @{context} card1_suc_r consts @{typ "'a list"} @{typ "'a fset"} *}
+ML {* val card1_suc_t = build_repabs_term @{context} card1_suc_r consts @{typ "'a list"} @{typ "'a fset"} *}
+prove card1_suc_t_p: card1_suc_t_g
+apply (atomize(full))
+apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *})
+done
 
-ML {* @{thm card1_suc_r} OF [card1_suc_f] *}
+prove card1_suc_t: card1_suc_t
+apply (simp only: card1_suc_t_p[symmetric])
+apply (tactic {* rtac card1_suc_r 1 *})
+done
+
+
+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 ithm = eqsubst_thm @{context} [rwrs] card1_suc_t'' *}
+ML {* val rwr = @{thm EXISTS_PRS[OF QUOTIENT_fset]} *}
+ML {* val rwrs = @{thm "HOL.sym"} OF [spec OF [rwr]] *}
+ML {* val jthm = eqsubst_thm @{context} [rwrs] ithm *}
+ML {* val rthm = MetaSimplifier.rewrite_rule fset_defs_sym jthm *}
+ML {* val qthm = MetaSimplifier.rewrite_rule @{thms QUOT_TYPE_I_fset.REPS_same} rthm *}
+ML {* ObjectLogic.rulify qthm *}
+
 
 ML {* val li = Thm.freezeT (atomize_thm @{thm fold1.simps(2)}) *}
 prove fold1_def_2_r: {*
@@ -635,7 +731,6 @@
 *}
 
 ML {* lift_theorem_fset_aux @{thm m1} @{context} *}
-
 ML {*
   fun lift_theorem_fset name thm lthy =
     let

--- a/QuotScript.thy	Sat Oct 24 08:34:14 2009 +0200
+++ b/QuotScript.thy	Sat Oct 24 10:16:53 2009 +0200
@@ -480,6 +480,12 @@
   apply (simp add: FUN_REL.simps Ball_def IN_RESPECTS)
   done
 
+lemma RES_EXISTS_RSP:
+  shows "\<And>f g. (R ===> (op =)) f g ==>
+        (Bex (Respects R) f = Bex (Respects R) g)"
+  apply (simp add: FUN_REL.simps Bex_def IN_RESPECTS)
+  done
+
 (* TODO: 
 - [FORALL_PRS, EXISTS_PRS, COND_PRS];
 > val it =
@@ -498,9 +504,18 @@
   shows "!f. All f = Ball (Respects R) ((absf ---> id) f)"
   sorry
 
+lemma EXISTS_PRS:
+  assumes a: "QUOTIENT R absf repf"
+  shows "!f. Ex f = Bex (Respects R) ((absf ---> id) f)"
+  sorry
+
 lemma ho_all_prs: "op = ===> op = ===> op = All All"
   apply (auto)
   done
 
+lemma ho_ex_prs: "op = ===> op = ===> op = Ex Ex"
+  apply (auto)
+  done
+
 end