--- 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)