--- a/FSet.thy Wed Oct 28 20:01:20 2009 +0100
+++ b/FSet.thy Thu Oct 29 07:29:12 2009 +0100
@@ -206,7 +206,7 @@
shows "card1 a = card1 b"
using e by induct (simp_all add:memb_rsp)
-lemma ho_card1_rsp: "op \<approx> ===> op = card1 card1"
+lemma ho_card1_rsp: "(op \<approx> ===> op =) card1 card1"
by (simp add: card1_rsp)
lemma cons_rsp:
@@ -216,7 +216,7 @@
using a by (rule list_eq.intros(5))
lemma ho_cons_rsp:
- "op = ===> op \<approx> ===> op \<approx> op # op #"
+ "(op = ===> op \<approx> ===> op \<approx>) op # op #"
by (simp add: cons_rsp)
lemma append_rsp_fst:
@@ -273,7 +273,7 @@
done
lemma ho_append_rsp:
- "op \<approx> ===> op \<approx> ===> op \<approx> op @ op @"
+ "(op \<approx> ===> op \<approx> ===> op \<approx>) op @ op @"
by (simp add: append_rsp)
lemma map_rsp:
@@ -285,7 +285,7 @@
done
lemma fun_rel_id:
- "op = ===> op = \<equiv> op ="
+ "(op = ===> op =) \<equiv> op ="
apply (rule eq_reflection)
apply (rule ext)
apply (rule ext)
@@ -296,7 +296,7 @@
done
lemma ho_map_rsp:
- "op = ===> op = ===> op \<approx> ===> op \<approx> map map"
+ "((op = ===> op =) ===> op \<approx> ===> op \<approx>) map map"
by (simp add: fun_rel_id map_rsp)
lemma map_append :
@@ -304,136 +304,43 @@
((map f a) ::'a list) @ (map f b)"
by simp (rule list_eq_refl)
-thm list.induct
-lemma list_induct_hol4:
- fixes P :: "'a list \<Rightarrow> bool"
- 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 {* regularise (prop_of (atomize_thm @{thm list_induct_hol4})) @{typ "'a list"} @{term "op \<approx>"} @{context} *}
-
-prove list_induct_r: {*
- build_regularize_goal (atomize_thm @{thm list_induct_hol4}) @{typ "'a list"} @{term "op \<approx>"} @{context} *}
- apply (simp only: equiv_res_forall[OF equiv_list_eq])
- thm RIGHT_RES_FORALL_REGULAR
- apply (rule RIGHT_RES_FORALL_REGULAR)
- prefer 2
- apply (assumption)
- apply (metis)
- done
-
-(* The all_prs and ex_prs should be proved for the instance... *)
+ML {* val rty = @{typ "'a list"} *}
+ML {* val qty = @{typ "'a fset"} *}
+ML {* val rel = @{term "list_eq"} *}
+ML {* val rel_eqv = (#equiv_thm o hd) (quotdata_lookup @{context}) *}
+ML {* val rel_refl = @{thm list_eq_refl} *}
+ML {* val quot = @{thm QUOTIENT_fset} *}
+ML {* val rsp_thms =
+ @{thms ho_memb_rsp ho_cons_rsp ho_card1_rsp ho_map_rsp ho_append_rsp}
+ @ @{thms ho_all_prs ho_ex_prs} *}
+ML {* val trans2 = @{thm QUOT_TYPE_I_fset.R_trans2} *}
+ML {* val reps_same = @{thm QUOT_TYPE_I_fset.REPS_same} *}
+ML {* val defs = @{thms EMPTY_def IN_def UNION_def card_def INSERT_def fmap_def fold_def} *}
+(* ML {* val consts = map (fst o dest_Const o fst o Logic.dest_equals o concl_of) fset_defs *} *)
ML {*
-fun r_mk_comb_tac_fset ctxt =
- r_mk_comb_tac ctxt @{typ "'a list"} @{thm QUOTIENT_fset} @{thm list_eq_refl} @{thm QUOT_TYPE_I_fset.R_trans2}
- (@{thms ho_memb_rsp ho_cons_rsp ho_card1_rsp ho_map_rsp ho_append_rsp} @ @{thms ho_all_prs ho_ex_prs})
-*}
-
-
-ML {* val thm = @{thm list_induct_r} OF [atomize_thm @{thm list_induct_hol4}] *}
-ML {* val trm_r = build_repabs_goal @{context} thm consts @{typ "'a list"} @{typ "'a fset"} *}
-ML {* val trm = build_repabs_term @{context} thm consts @{typ "'a list"} @{typ "'a fset"} *}
-
-ML {* val rty = @{typ "'a list"} *}
-
-ML {*
-fun r_mk_comb_tac_fset ctxt =
- r_mk_comb_tac ctxt rty @{thm QUOTIENT_fset} @{thm list_eq_refl} @{thm QUOT_TYPE_I_fset.R_trans2}
- (@{thms ho_memb_rsp ho_cons_rsp ho_card1_rsp ho_map_rsp ho_append_rsp} @ @{thms ho_all_prs ho_ex_prs})
+ val consts = [@{const_name "Nil"}, @{const_name "Cons"},
+ @{const_name "membship"}, @{const_name "card1"},
+ @{const_name "append"}, @{const_name "fold1"},
+ @{const_name "map"}];
*}
-
-ML {* trm_r *}
-prove list_induct_tr: trm_r
-apply (atomize(full))
-apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *})
-done
-
-prove list_induct_t: trm
-apply (simp only: list_induct_tr[symmetric])
-apply (tactic {* rtac thm 1 *})
-done
-
-thm m2
-ML {* atomize_thm @{thm m2} *}
-
-prove m2_r_p: {*
- build_regularize_goal (atomize_thm @{thm m2}) @{typ "'a List.list"} @{term "op \<approx>"} @{context} *}
- apply (simp add: equiv_res_forall[OF equiv_list_eq])
-done
-
-ML {* val m2_r = @{thm m2_r_p} OF [atomize_thm @{thm m2}] *}
-ML {* val m2_t_g = build_repabs_goal @{context} m2_r consts @{typ "'a list"} @{typ "'a fset"} *}
-ML {* val m2_t = build_repabs_term @{context} m2_r consts @{typ "'a list"} @{typ "'a fset"} *}
-prove m2_t_p: m2_t_g
-apply (atomize(full))
-apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *})
-done
-
-prove m2_t: m2_t
-apply (simp only: m2_t_p[symmetric])
-apply (tactic {* rtac m2_r 1 *})
-done
-
-lemma id_apply2 [simp]: "id x \<equiv> x"
- by (simp add: id_def)
-
-ML {* val quot = @{thm QUOTIENT_fset} *}
-ML {* val abs = findabs @{typ "'a list"} (prop_of (atomize_thm @{thm list_induct_hol4})) *}
-ML {* val simp_lam_prs_thms = map (make_simp_lam_prs_thm @{context} quot) abs *}
-
-ML {*
- fun simp_lam_prs lthy thm =
- simp_lam_prs lthy (eqsubst_thm lthy simp_lam_prs_thms thm)
- handle _ => thm
+ML {* fun lift_thm_fset lthy t =
+ lift_thm lthy consts rty qty rel rel_eqv rel_refl quot rsp_thms trans2 reps_same defs t
*}
-ML {* val m2_t' = simp_lam_prs @{context} @{thm m2_t} *}
-
-ML {* val ithm = simp_allex_prs @{context} quot m2_t' *}
-
-ML {* val rthm = MetaSimplifier.rewrite_rule fset_defs_sym ithm *}
-ML {* ObjectLogic.rulify rthm *}
-
-
-ML {* val card1_suc_a = atomize_thm @{thm card1_suc} *}
-
-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
+lemma eq_r: "a = b \<Longrightarrow> a \<approx> b"
+by (simp add: list_eq_refl)
-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
-
-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' = simp_lam_prs @{context} @{thm card1_suc_t} *}
-ML {* val ithm = simp_allex_prs @{context} quot 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 *}
-ML {* ObjectLogic.rulify qthm *}
+ML {* lift_thm_fset @{context} @{thm m1} *}
+ML {* lift_thm_fset @{context} @{thm m2} *}
+ML {* lift_thm_fset @{context} @{thm list_eq.intros(4)} *}
+ML {* lift_thm_fset @{context} @{thm list_eq.intros(5)} *}
+ML {* lift_thm_fset @{context} @{thm card1_suc} *}
+ML {* lift_thm_fset @{context} @{thm map_append} *}
+ML {* lift_thm_fset @{context} @{thm eq_r[OF append_assoc]} *}
thm fold1.simps(2)
thm list.recs(2)
-thm map_append
ML {* val ind_r_a = atomize_thm @{thm list.induct} *}
(* prove {* build_regularize_goal ind_r_a @{typ "'a List.list"} @{term "op \<approx>"} @{context} *}
@@ -449,12 +356,10 @@
val rt = build_repabs_term @{context} ind_r_r consts @{typ "'a list"} @{typ "'a fset"}
val rg = Logic.mk_equals ((Thm.prop_of ind_r_r), rt);
*}
-
-prove rg
+(*prove rg
apply(atomize(full))
apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *})
-done
-
+done*)
ML {* val ind_r_t =
Toplevel.program (fn () =>
repabs @{context} ind_r_r consts @{typ "'a list"} @{typ "'a fset"}
@@ -462,7 +367,9 @@
(@{thms ho_memb_rsp ho_cons_rsp ho_card1_rsp ho_map_rsp ho_append_rsp} @ @{thms ho_all_prs ho_ex_prs})
)
*}
-ML {* val ind_r_l = simp_lam_prs @{context} ind_r_t *}
+ML {* val abs = findabs rty (prop_of (atomize_thm @{thm list.induct})) *}
+ML {* val simp_lam_prs_thms = map (make_simp_lam_prs_thm @{context} quot) abs *}
+ML {* val ind_r_l = repeat_eqsubst_thm @{context} simp_lam_prs_thms ind_r_t *}
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
@@ -474,98 +381,30 @@
ML {* val ind_r_a = simp_allex_prs @{context} quot ind_r_l4 *}
ML {* val thm = @{thm FORALL_PRS[OF FUN_QUOTIENT[OF QUOTIENT_fset IDENTITY_QUOTIENT], symmetric]} *}
ML {* val ind_r_a1 = eqsubst_thm @{context} [thm] ind_r_a *}
-ML {* val ind_r_d = repeat_eqsubst_thm @{context} fset_defs_sym ind_r_a1 *}
+ML {* val defs_sym = add_lower_defs @{context} defs *}
+ML {* val ind_r_d = repeat_eqsubst_thm @{context} defs_sym ind_r_a1 *}
ML {* val ind_r_s = MetaSimplifier.rewrite_rule @{thms QUOT_TYPE_I_fset.REPS_same} ind_r_d *}
ML {* ObjectLogic.rulify ind_r_s *}
ML {*
-fun lift thm =
-let
- val ind_r_a = atomize_thm thm;
- val ind_r_r = regularize ind_r_a @{typ "'a List.list"} @{term "op \<approx>"} @{thm equiv_list_eq} @{context};
- 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 ho_map_rsp ho_append_rsp} @ @{thms ho_all_prs ho_ex_prs});
- val ind_r_l = simp_lam_prs @{context} ind_r_t;
- val ind_r_a = simp_allex_prs @{context} quot ind_r_l;
- val ind_r_d = repeat_eqsubst_thm @{context} fset_defs_sym ind_r_a;
- val ind_r_s = MetaSimplifier.rewrite_rule @{thms QUOT_TYPE_I_fset.REPS_same} ind_r_d
-in
- ObjectLogic.rulify ind_r_s
-end
-*}
-ML fset_defs
-
-lemma eq_r: "a = b \<Longrightarrow> a \<approx> b"
-by (simp add: list_eq_refl)
-
-
-ML {* lift @{thm m2} *}
-ML {* lift @{thm m1} *}
-ML {* lift @{thm list_eq.intros(4)} *}
-ML {* lift @{thm list_eq.intros(5)} *}
-ML {* lift @{thm card1_suc} *}
-ML {* lift @{thm map_append} *}
-ML {* lift @{thm eq_r[OF append_assoc]} *}
-
-
-(*notation ( output) "prop" ("#_" [1000] 1000) *)
-notation ( output) "Trueprop" ("#_" [1000] 1000)
-
-(*
-ML {*
- fun lift_theorem_fset_aux thm lthy =
+ fun lift_thm_fset_note name thm lthy =
let
- val ((_, [novars]), lthy2) = Variable.import true [thm] lthy;
- val goal = build_repabs_goal @{context} novars consts @{typ "'a list"} @{typ "'a fset"};
- val cgoal = cterm_of @{theory} goal;
- val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite true fset_defs_sym cgoal);
- val tac = transconv_fset_tac' @{context};
- val cthm = Goal.prove_internal [] cgoal2 (fn _ => tac);
- val nthm = MetaSimplifier.rewrite_rule [symmetric cthm] (snd (no_vars (Context.Theory @{theory}, thm)))
- val nthm2 = MetaSimplifier.rewrite_rule @{thms QUOT_TYPE_I_fset.REPS_same QUOT_TYPE_I_fset.thm10} nthm;
- val [nthm3] = ProofContext.export lthy2 lthy [nthm2]
- in
- nthm3
- end
-*}
-*)
-
-(*
-ML {* lift_theorem_fset_aux @{thm m1} @{context} *}
-ML {*
- fun lift_theorem_fset name thm lthy =
- let
- val lifted_thm = lift_theorem_fset_aux thm lthy;
+ val lifted_thm = lift_thm_fset lthy thm;
val (_, lthy2) = note (name, lifted_thm) lthy;
in
lthy2
end;
*}
-*)
-local_setup {* lift_theorem_fset @{binding "m1_lift"} @{thm m1} *}
-local_setup {* lift_theorem_fset @{binding "leqi4_lift"} @{thm list_eq.intros(4)} *}
-local_setup {* lift_theorem_fset @{binding "leqi5_lift"} @{thm list_eq.intros(5)} *}
-local_setup {* lift_theorem_fset @{binding "m2_lift"} @{thm m2} *}
-thm m1_lift
-thm leqi4_lift
-thm leqi5_lift
-thm m2_lift
-ML {* @{thm card1_suc_r} OF [card1_suc_f] *}
-(*ML {* Toplevel.program (fn () => lift_theorem_fset @{binding "card_suc"}
- (@{thm card1_suc_r} OF [card1_suc_f]) @{context}) *}*)
-(*local_setup {* lift_theorem_fset @{binding "card_suc"} @{thm card1_suc} *}*)
-
-thm leqi4_lift
-ML {*
- val (nam, typ) = hd (Term.add_vars (prop_of @{thm leqi4_lift}) [])
- val (_, l) = dest_Type typ
- val t = Type ("FSet.fset", l)
- val v = Var (nam, t)
- val cv = cterm_of @{theory} ((term_of @{cpat "REP_fset"}) $ v)
+local_setup {*
+ lift_thm_fset_note @{binding "m1l"} @{thm m1} #>
+ lift_thm_fset_note @{binding "m2l"} @{thm m2} #>
+ lift_thm_fset_note @{binding "leqi4l"} @{thm list_eq.intros(4)} #>
+ lift_thm_fset_note @{binding "leqi5l"} @{thm list_eq.intros(5)}
*}
-
+thm m1l
+thm m2l
+thm leqi4l
+thm leqi5l
end