292 

   292 

   293 lemma map_append :

   293 lemma map_append :

   294   "(map f ((a::'a list) @ b)) \<approx>

   294   "(map f ((a::'a list) @ b)) \<approx>

   295   ((map f a) ::'a list) @ (map f b)"

   295   ((map f a) ::'a list) @ (map f b)"

   296  by simp (rule list_eq_refl)

   296  by simp (rule list_eq_refl)

   297 

   298 

   298 ML {* val qty = @{typ "'a fset"} *}

   299 ML {* val qty = @{typ "'a fset"} *}

   299 ML {* val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data @{context} qty *}

   300 ML {* val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data @{context} qty *}

   300 ML {* val (trans2, reps_same, quot) = lookup_quot_thms @{context} "fset" *}

   301 ML {* val (trans2, reps_same, quot) = lookup_quot_thms @{context} "fset" *}

   301 

   302 

   340 ML {* val ind_r_t =

   341 ML {* val ind_r_t =

   341   Toplevel.program (fn () =>

   342   Toplevel.program (fn () =>

   342   repabs @{context} ind_r_r consts rty qty quot rel_refl trans2 rsp_thms

   343   repabs @{context} ind_r_r consts rty qty quot rel_refl trans2 rsp_thms

   343   )

   344   )

   344 *}

   345 *}

   345 ML {* val abs = findabs rty (prop_of (atomize_thm @{thm list.induct})) *}

   347 ML {* val abs = findabs rty (prop_of (atomize_thm @{thm list.induct})) *}

   346 ML {* val simp_lam_prs_thms = map (make_simp_lam_prs_thm @{context} quot) abs *}

   350 ML {* val simp_lam_prs_thms = map (make_simp_lam_prs_thm @{context} quot) abs *}

   347 ML {* val ind_r_l = repeat_eqsubst_thm @{context} simp_lam_prs_thms ind_r_t *}

   351 ML {* val ind_r_l = repeat_eqsubst_thm @{context} simp_lam_prs_thms ind_r_t *}

   348 lemma app_prs_for_induct: "(ABS_fset ---> id) f (REP_fset T1) = f T1"

   352 lemma app_prs_for_induct: "(ABS_fset ---> id) f (REP_fset T1) = f T1"

   349   apply (simp add: fun_map.simps QUOT_TYPE_I_fset.thm10)

   353   apply (simp add: fun_map.simps QUOT_TYPE_I_fset.thm10)

   350 done

   354 done