Mercurial Mercurial > hg > nominal2 / comparison
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
FSet.thy
changeset 309 20fa8dd8fb93
parent 305 d7b60303adb8
child 314 3b3c5feb6b73
equal deleted inserted replaced
308:e39c8793a233 309:20fa8dd8fb93 
    99   by (induct a) auto
 
    99   by (induct a) auto
 
   100 
   100 
   101 lemma not_mem_card1:
 
   101 lemma not_mem_card1:
 
   102   fixes x :: "'a"
 
   102   fixes x :: "'a"
 
   103   fixes xs :: "'a list"
 
   103   fixes xs :: "'a list"
 
   104   shows "~(x memb xs) \<Longrightarrow> card1 (x # xs) = Suc (card1 xs)"
 
   104   shows "(~(x memb xs)) = (card1 (x # xs) = Suc (card1 xs))"
 
   105   by simp
 
   105   by auto
 
   106 
   106 
   107 lemma mem_cons:
 
   107 lemma mem_cons:
 
   108   fixes x :: "'a"
 
   108   fixes x :: "'a"
 
   109   fixes xs :: "'a list"
 
   109   fixes xs :: "'a list"
 
   110   assumes a : "x memb xs"
 
   110   assumes a : "x memb xs"
 
   313 ML {* lift_thm_fset @{context} @{thm card1_suc} *}
 
   313 ML {* lift_thm_fset @{context} @{thm card1_suc} *}
 
   314 ML {* lift_thm_fset @{context} @{thm map_append} *}
 
   314 ML {* lift_thm_fset @{context} @{thm map_append} *}
 
   315 ML {* lift_thm_fset @{context} @{thm append_assoc} *}
 
   315 ML {* lift_thm_fset @{context} @{thm append_assoc} *}
 
   316 ML {* lift_thm_fset @{context} @{thm list.induct} *}
 
   316 ML {* lift_thm_fset @{context} @{thm list.induct} *}
 
   317 ML {* lift_thm_fset @{context} @{thm fold1.simps(2)} *}
 
   317 ML {* lift_thm_fset @{context} @{thm fold1.simps(2)} *}
 
       
   318 ML {* lift_thm_fset @{context} @{thm not_mem_card1} *}
 
   318 
   319 
   319 quotient_def
 
   320 quotient_def
 
   320   fset_rec::"'a \<Rightarrow> ('b \<Rightarrow> 'b fset \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'b fset \<Rightarrow> 'a"
 
   321   fset_rec::"'a \<Rightarrow> ('b \<Rightarrow> 'b fset \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'b fset \<Rightarrow> 'a"
 
   321 where
 
   322 where
 
   322   "fset_rec \<equiv> list_rec"
 
   323   "fset_rec \<equiv> list_rec"
 
   390 ML {*
 
   391 ML {*
 
   391   val rt = build_repabs_term @{context} t_r consts rty qty
 
   392   val rt = build_repabs_term @{context} t_r consts rty qty
 
   392   val rg = Logic.mk_equals ((Thm.prop_of t_r), rt);
 
   393   val rg = Logic.mk_equals ((Thm.prop_of t_r), rt);
 
   393 *}
 
   394 *}
 
   394 prove {* Syntax.check_term @{context} rg *}
 
   395 prove {* Syntax.check_term @{context} rg *}
 
       
   396 ML_prf {* fun r_mk_comb_tac_fset lthy = r_mk_comb_tac lthy rty quot rel_refl trans2 rsp_thms *}
 
   395 apply(atomize(full))
 
   397 apply(atomize(full))
 
   396 ML_prf {* fun r_mk_comb_tac_fset lthy = r_mk_comb_tac lthy rty quot rel_refl trans2 rsp_thms *}
 
   398 apply (tactic {* (APPLY_RSP_TAC rty @{context}) 1 *})
 
       
   399 apply (rule FUN_QUOTIENT)
 
       
   400 apply (rule FUN_QUOTIENT)
 
       
   401 apply (rule QUOTIENT_fset)
 
       
   402 apply (rule FUN_QUOTIENT)
 
       
   403 apply (rule QUOTIENT_fset)
 
       
   404 apply (rule IDENTITY_QUOTIENT)
 
       
   405 apply (rule IDENTITY_QUOTIENT)
 
       
   406 apply (rule IDENTITY_QUOTIENT)
 
       
   407 apply (tactic {*  (r_mk_comb_tac_fset @{context}) 1 *})
 
   397 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *})
 
   408 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *})
 
   398 
       
   399 done
 
   409 done
 
   400 ML {*
 
   410 ML {*
 
   401 val t_t = repabs @{context} t_r consts rty qty quot rel_refl trans2 rsp_thms
 
   411 val t_t = repabs @{context} t_r consts rty qty quot rel_refl trans2 rsp_thms
 
   402 *}
 
   412 *}
 
   403 
   413 
   417 thm INSERT_def
 
   427 thm INSERT_def
 
   418 ML {* val defs_sym = flat (map (add_lower_defs @{context}) defs) *}
 
   428 ML {* val defs_sym = flat (map (add_lower_defs @{context}) defs) *}
 
   419 ML {* val t_d = repeat_eqsubst_thm @{context} defs_sym t_id *}
 
   429 ML {* val t_d = repeat_eqsubst_thm @{context} defs_sym t_id *}
 
   420 ML allthms
 
   430 ML allthms
 
   421 thm FORALL_PRS
 
   431 thm FORALL_PRS
 
   422 ML {* val t_a = MetaSimplifier.rewrite_rule (allthms) t_d *}
 
   432 ML {* val t_al = MetaSimplifier.rewrite_rule (allthms) t_d *}
 
   423 ML {* val t_s = MetaSimplifier.rewrite_rule @{thms QUOT_TYPE_I_fset.REPS_same} t_a *}
 
   433 ML {* val t_s = MetaSimplifier.rewrite_rule @{thms QUOT_TYPE_I_fset.REPS_same} t_al *}
 
   424 ML {* ObjectLogic.rulify t_s *}
 
   434 ML {* ObjectLogic.rulify t_s *}
 
   425 
   435 
   426 ML {* Type.freeze *}
 
   436 ML {* Type.freeze *}
 
   427 
   437 
   428 ML {* val gl = @{term "P (x :: 'a list) (EMPTY :: 'a fset) \<Longrightarrow> (\<And>e t. P x t \<Longrightarrow> P x (INSERT e t)) \<Longrightarrow> P x l"} *}
 
   438 ML {* val gl = @{term "P (x :: 'a list) (EMPTY :: 'a fset) \<Longrightarrow> (\<And>e t. P x t \<Longrightarrow> P x (INSERT e t)) \<Longrightarrow> P x l"} *}
 
   429 ML {* val vars = map Free (Term.add_frees gl []) *}
 
   439 ML {* val vars = map Free (Term.add_frees gl []) *}
 
   430 ML {* fun lambda_all (var as Free(_, T)) trm = (Term.all T) $ lambda var trm *}
 
   440 ML {* fun lambda_all (var as Free(_, T)) trm = (Term.all T) $ lambda var trm *}
 
   431 ML {* val gla = fold lambda_all vars gl *}
 
   441 ML {* val gla = fold lambda_all vars gl *}
 
   432 ML {* val glf = Type.freeze gla *}
 
   442 ML {* val glf = Type.freeze gla *}
 
   433 ML {* val glac = (snd o Thm.dest_equals o cprop_of) (ObjectLogic.atomize (cterm_of @{theory} glf)) *}
 
   443 ML {* val glac = (snd o Thm.dest_equals o cprop_of) (ObjectLogic.atomize (cterm_of @{theory} glf)) *}
 
   434 ML {* val allsym = map symmetric allthms *}
 
   444 
   435 ML {* val t_a = (snd o Thm.dest_equals o cprop_of) (MetaSimplifier.rewrite true allsym glac) *}
 
   445 ML {*
 
       
   446 fun apply_subt2 f trm trm2 =
 
       
   447   case (trm, trm2) of
 
       
   448     (Abs (x, T, t), Abs (x2, T2, t2)) =>
 
       
   449        let
 
       
   450          val (x', t') = Term.dest_abs (x, T, t);
 
       
   451          val (x2', t2') = Term.dest_abs (x2, T2, t2)
 
       
   452          val (s1, s2) = f t' t2';
 
       
   453        in
 
       
   454          (Term.absfree (x', T, s1),
 
       
   455           Term.absfree (x2', T2, s2))
 
       
   456        end
 
       
   457   | _ => f trm trm2
 
       
   458 *}
 
       
   459 
       
   460 ML {*
 
       
   461 fun tyRel2 lthy ty gty =
 
       
   462   if ty = gty then HOLogic.eq_const ty else
 
       
   463 
       
   464   case find_first (fn x => Sign.typ_instance (ProofContext.theory_of lthy) (gty, (#qtyp x))) (quotdata_lookup lthy) of
 
       
   465     SOME quotdata =>
 
       
   466       if Sign.typ_instance (ProofContext.theory_of lthy) (ty, #rtyp quotdata) then
 
       
   467         case #rel quotdata of
 
       
   468           Const(s, _) => Const(s, dummyT)
 
       
   469         | _ => error "tyRel2 fail: relation is not a constant"
 
       
   470       else error "tyRel2 fail: a non-lifted type lifted to a lifted type"
 
       
   471   | NONE => (case (ty, gty) of
 
       
   472       (Type (s, tys), Type (s2, tys2)) =>
 
       
   473       if s = s2 andalso length tys = length tys2 then
 
       
   474         let
 
       
   475           val tys_rel = map (fn ty => ty --> ty --> @{typ bool}) tys;
 
       
   476           val ty_out = ty --> ty --> @{typ bool};
 
       
   477           val tys_out = tys_rel ---> ty_out;
 
       
   478         in
 
       
   479         (case (maps_lookup (ProofContext.theory_of lthy) s) of
 
       
   480           SOME (info) => list_comb (Const (#relfun info, tys_out),
 
       
   481                               map2 (tyRel2 lthy) tys tys2)
 
       
   482         | NONE  => HOLogic.eq_const ty
 
       
   483         )
 
       
   484         end
 
       
   485       else error "tyRel2 fail: different type structures"
 
       
   486     | _ => HOLogic.eq_const ty)
 
       
   487 *}
 
       
   488 
       
   489 ML {*
 
       
   490 fun my_reg2 lthy trm gtrm =
 
       
   491   case (trm, gtrm) of
 
       
   492     (Abs (x, T, t), Abs (x2, T2, t2)) =>
 
       
   493        if not (T = T2) then
 
       
   494          let
 
       
   495            val rrel = tyRel2 lthy T T2;
 
       
   496            val (s1, s2) = apply_subt2 (my_reg2 lthy) trm gtrm
 
       
   497          in
 
       
   498            (((mk_babs (fastype_of trm) T) $ (mk_resp T $ rrel) $ s1),
 
       
   499            ((mk_babs (fastype_of gtrm) T2) $ (mk_resp T2 $ (HOLogic.eq_const dummyT)) $ s2))
 
       
   500          end
 
       
   501        else
 
       
   502          let
 
       
   503            val (s1, s2) = apply_subt2 (my_reg2 lthy) t t2
 
       
   504          in
 
       
   505            (Abs(x, T, s1), Abs(x2, T2, s2))
 
       
   506          end
 
       
   507   | (Const (@{const_name "All"}, ty) $ (t as Abs (_, T, _)),
 
       
   508      Const (@{const_name "All"}, ty') $ (t2 as Abs (_, T2, _))) =>
 
       
   509        if not (T = T2) then
 
       
   510          let
 
       
   511             val ty1 = domain_type ty;
 
       
   512             val ty2 = domain_type ty1;
 
       
   513             val ty'1 = domain_type ty';
 
       
   514             val ty'2 = domain_type ty'1;
 
       
   515             val rrel = tyRel2 lthy T T2;
 
       
   516             val (s1, s2) = apply_subt2 (my_reg2 lthy) t t2;
 
       
   517          in
 
       
   518            (((mk_ball ty1) $ (mk_resp ty2 $ rrel) $ s1),
 
       
   519            ((mk_ball ty'1) $ (mk_resp ty'2 $ (HOLogic.eq_const dummyT)) $ s2))
 
       
   520          end
 
       
   521        else
 
       
   522          let
 
       
   523            val (s1, s2) = apply_subt2 (my_reg2 lthy) t t2
 
       
   524          in
 
       
   525            ((Const (@{const_name "All"}, ty) $ s1),
 
       
   526            (Const (@{const_name "All"}, ty') $ s2))
 
       
   527          end
 
       
   528   | (Const (@{const_name "Ex"}, ty) $ (t as Abs (_, T, _)),
 
       
   529      Const (@{const_name "Ex"}, ty') $ (t2 as Abs (_, T2, _))) =>
 
       
   530        if not (T = T2) then
 
       
   531          let
 
       
   532             val ty1 = domain_type ty
 
       
   533             val ty2 = domain_type ty1
 
       
   534             val ty'1 = domain_type ty'
 
       
   535             val ty'2 = domain_type ty'1
 
       
   536             val rrel = tyRel2 lthy T T2
 
       
   537             val (s1, s2) = apply_subt2 (my_reg2 lthy) t t2
 
       
   538          in
 
       
   539            (((mk_bex ty1) $ (mk_resp ty2 $ rrel) $ s1),
 
       
   540            ((mk_bex ty'1) $ (mk_resp ty'2 $ (HOLogic.eq_const dummyT)) $ s2))
 
       
   541          end
 
       
   542        else
 
       
   543          let
 
       
   544            val (s1, s2) = apply_subt2 (my_reg2 lthy) t t2
 
       
   545          in
 
       
   546            ((Const (@{const_name "Ex"}, ty) $ s1),
 
       
   547            (Const (@{const_name "Ex"}, ty') $ s2))
 
       
   548          end
 
       
   549   | (Const (@{const_name "op ="}, T) $ t, (Const (@{const_name "op ="}, T2) $ t2)) =>
 
       
   550       let
 
       
   551         val (s1, s2) = apply_subt2 (my_reg2 lthy) t t2
 
       
   552         val rhs = Const (@{const_name "op ="}, T2) $ s2
 
       
   553       in
 
       
   554         if not (T = T2) then
 
       
   555           ((tyRel2 lthy T T2) $ s1, rhs)
 
       
   556         else
 
       
   557           (Const (@{const_name "op ="}, T) $ s1, rhs)
 
       
   558       end
 
       
   559   | (t $ t', t2 $ t2') =>
 
       
   560       let
 
       
   561         val (s1, s2) = apply_subt2 (my_reg2 lthy) t t2
 
       
   562         val (s1', s2') = apply_subt2 (my_reg2 lthy) t' t2'
 
       
   563       in
 
       
   564         (s1 $ s1', s2 $ s2')
 
       
   565       end
 
       
   566   | (Const c1, Const c2) => (Const c1, Const c2) (* c2 may be lifted *)
 
       
   567   | (Bound i, Bound j) => (* Bounds are replaced, so should never happen? *)
 
       
   568       if i = j then (Bound i, Bound j) else error "my_reg2: different Bounds"
 
       
   569   | (Free (n, T), Free(n2, T2)) => if n = n2 then (Free (n, T), Free (n2, T2))
 
       
   570       else error ("my_ref2: different variables: " ^ n ^ ", " ^ n2)
 
       
   571   | _ => error "my_reg2: terms don't agree"
 
       
   572 *}
 
       
   573 
       
   574 
       
   575 ML {* prop_of t_a *}
 
       
   576 ML {* term_of glac *}
 
       
   577 ML {* val (tta, ttb) = (my_reg2 @{context} (prop_of t_a) (term_of glac)) *}
 
       
   578 ML {* val tt = Syntax.check_term @{context} tta *}
 
       
   579 
       
   580 prove t_r: {* Logic.mk_implies
 
       
   581        ((prop_of t_a), tt) *}
 
       
   582 ML_prf {*  fun tac ctxt = FIRST' [
 
       
   583       rtac rel_refl,
 
       
   584       atac,
 
       
   585       rtac @{thm universal_twice},
 
       
   586       (rtac @{thm impI} THEN' atac),
 
       
   587       rtac @{thm implication_twice},
 
       
   588       (*rtac @{thm equality_twice},*)
 
       
   589       EqSubst.eqsubst_tac ctxt [0]
 
       
   590         [(@{thm equiv_res_forall} OF [rel_eqv]),
 
       
   591          (@{thm equiv_res_exists} OF [rel_eqv])],
 
       
   592       (rtac @{thm impI} THEN' (asm_full_simp_tac (Simplifier.context ctxt HOL_ss)) THEN' rtac rel_refl),
 
       
   593       (rtac @{thm RIGHT_RES_FORALL_REGULAR})
 
       
   594      ]; *}
 
       
   595 
       
   596   apply (atomize(full))
 
       
   597   apply (tactic {* REPEAT_ALL_NEW (tac @{context}) 1 *})
 
       
   598   done
 
       
   599 
       
   600 ML {* val t_r = @{thm t_r} OF [t_a] *}
 
       
   601 
       
   602 ML {* val ttg = Syntax.check_term @{context} ttb *}
 
       
   603 
       
   604 ML {*
 
       
   605 fun is_lifted_const h gh = is_Const h andalso is_Const gh andalso not (h = gh)
 
       
   606 
       
   607 fun mkrepabs lthy ty gty t =
 
       
   608   let
 
       
   609     val qenv = distinct (op=) (diff (gty, ty) [])
 
       
   610 (*  val _ = sanity_chk qenv lthy *)
 
       
   611     val ty = fastype_of t
 
       
   612     val abs = get_fun absF qenv lthy gty $ t
 
       
   613     val rep = get_fun repF qenv lthy gty $ abs
 
       
   614   in
 
       
   615     Syntax.check_term lthy rep
 
       
   616   end
 
       
   617 *}
 
       
   618 
       
   619 ML {*
 
       
   620   cterm_of @{theory} (mkrepabs @{context} @{typ "'a list \<Rightarrow> bool"} @{typ "'a fset \<Rightarrow> bool"} @{term "f :: ('a list \<Rightarrow> bool)"})
 
       
   621 *}
 
       
   622 
       
   623 
       
   624 
       
   625 ML {*
 
       
   626 fun build_repabs_term lthy trm gtrm =
 
       
   627   case (trm, gtrm) of
 
       
   628     (Abs (a as (_, T, _)), Abs (a2 as (_, T2, _))) =>
 
       
   629       let
 
       
   630         val (vs, t) = Term.dest_abs a;
 
       
   631         val (_,  g) = Term.dest_abs a2;
 
       
   632         val v = Free(vs, T);
 
       
   633         val t' = lambda v (build_repabs_term lthy t g);
 
       
   634         val ty = fastype_of trm;
 
       
   635         val gty = fastype_of gtrm;
 
       
   636       in
 
       
   637         if (ty = gty) then t' else
 
       
   638         mkrepabs lthy ty gty (
 
       
   639           if (T = T2) then t' else
 
       
   640           lambda v (t' $ (mkrepabs lthy T T2 v))
 
       
   641         )
 
       
   642       end
 
       
   643   | _ =>
 
       
   644     case (Term.strip_comb trm, Term.strip_comb gtrm) of
 
       
   645       ((Const(@{const_name Respects}, _), _), _) => trm
 
       
   646     | ((h, tms), (gh, gtms)) =>
 
       
   647       let
 
       
   648         val ty = fastype_of trm;
 
       
   649         val gty = fastype_of gtrm;
 
       
   650         val tms' = map2 (build_repabs_term lthy) tms gtms
 
       
   651         val t' = list_comb(h, tms')
 
       
   652       in
 
       
   653         if ty = gty then t' else
 
       
   654         if is_lifted_const h gh then mkrepabs lthy ty gty t' else
 
       
   655         if (Term.is_Free h) andalso (length tms > 0) then mkrepabs lthy ty gty t' else t'
 
       
   656       end
 
       
   657 *}
 
       
   658 
       
   659 ML {* val ttt = build_repabs_term @{context} tt ttg *}
 
       
   660 ML {* val si = simp_ids_trm (cterm_of @{theory} ttt) *}
 
       
   661 prove t_t: {* Logic.mk_equals ((Thm.prop_of t_r), term_of si) *}
 
       
   662 ML_prf {* fun r_mk_comb_tac_fset lthy = r_mk_comb_tac lthy rty quot rel_refl trans2 rsp_thms *}
 
       
   663 apply(atomize(full))
 
       
   664 apply (tactic {* (APPLY_RSP_TAC rty @{context}) 1 *})
 
       
   665 apply (rule FUN_QUOTIENT)
 
       
   666 apply (rule FUN_QUOTIENT)
 
       
   667 apply (rule IDENTITY_QUOTIENT)
 
       
   668 apply (rule FUN_QUOTIENT)
 
       
   669 apply (rule QUOTIENT_fset)
 
       
   670 apply (rule IDENTITY_QUOTIENT)
 
       
   671 apply (rule IDENTITY_QUOTIENT)
 
       
   672 apply (rule IDENTITY_QUOTIENT)
 
       
   673 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
 
       
   674 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
 
       
   675 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
 
       
   676 apply (tactic {* (APPLY_RSP_TAC rty @{context}) 1 *})
 
       
   677 apply (rule IDENTITY_QUOTIENT)
 
       
   678 apply (rule IDENTITY_QUOTIENT)
 
       
   679 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
 
       
   680 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
 
       
   681 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
 
       
   682 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
 
       
   683 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
 
       
   684 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
 
       
   685 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
 
       
   686 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
 
       
   687 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
 
       
   688 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
 
       
   689 apply (tactic {* (APPLY_RSP_TAC rty @{context}) 1 *})
 
       
   690 apply (rule IDENTITY_QUOTIENT)
 
       
   691 apply (rule FUN_QUOTIENT)
 
       
   692 apply (rule QUOTIENT_fset)
 
       
   693 apply (rule IDENTITY_QUOTIENT)
 
       
   694 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
 
       
   695 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
 
       
   696 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
 
       
   697 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
 
       
   698 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
 
       
   699 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
 
       
   700 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
 
       
   701 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
 
       
   702 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
 
       
   703 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
 
       
   704 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
 
       
   705 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
 
       
   706 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
 
       
   707 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
 
       
   708 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
 
       
   709 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
 
       
   710 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
 
       
   711 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
 
       
   712 apply (tactic {* (APPLY_RSP_TAC rty @{context}) 1 *})
 
       
   713 apply (rule QUOTIENT_fset)
 
       
   714 apply (rule IDENTITY_QUOTIENT)
 
       
   715 apply (tactic {* (APPLY_RSP_TAC rty @{context}) 1 *})
 
       
   716 apply (rule IDENTITY_QUOTIENT)
 
       
   717 apply (rule FUN_QUOTIENT)
 
       
   718 apply (rule QUOTIENT_fset)
 
       
   719 apply (rule IDENTITY_QUOTIENT)
 
       
   720 
       
   721 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
 
       
   722 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
 
       
   723 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
 
       
   724 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
 
       
   725 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
 
       
   726 apply (tactic {* (APPLY_RSP_TAC rty @{context}) 1 *})
 
       
   727 apply (rule QUOTIENT_fset)
 
       
   728 apply (rule IDENTITY_QUOTIENT)
 
       
   729 apply (tactic {* (APPLY_RSP_TAC rty @{context}) 1 *})
 
       
   730 apply (rule IDENTITY_QUOTIENT)
 
       
   731 apply (rule FUN_QUOTIENT)
 
       
   732 apply (rule QUOTIENT_fset)
 
       
   733 apply (rule IDENTITY_QUOTIENT)
 
       
   734 
       
   735 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
 
       
   736 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
 
       
   737 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
 
       
   738 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
 
       
   739 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *})
 
       
   740 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
 
       
   741 apply (tactic {* (APPLY_RSP_TAC rty @{context}) 1 *})
 
       
   742 apply (rule IDENTITY_QUOTIENT)
 
       
   743 apply (rule FUN_QUOTIENT)
 
       
   744 apply (rule QUOTIENT_fset)
 
       
   745 apply (rule IDENTITY_QUOTIENT)
 
       
   746 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
 
       
   747 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
 
       
   748 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
 
       
   749 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
 
       
   750 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
 
       
   751 done
 
       
   752 
       
   753 thm t_t
 
       
   754 ML {* val t_t = @{thm Pure.equal_elim_rule1} OF [@{thm t_t}, t_r] *}
 
       
   755 ML {* val t_l = repeat_eqsubst_thm @{context} (lam_prs_thms) t_t *}
 
       
   756 ML {* val t_d = repeat_eqsubst_thm @{context} defs_sym t_l *}
 
       
   757 ML {* val t_al = MetaSimplifier.rewrite_rule (allthms) t_d *}
 
       
   758 ML {* val t_s = MetaSimplifier.rewrite_rule @{thms QUOT_TYPE_I_fset.REPS_same} t_al *}
 
       
   759 
   436 
   760 
   437 ML {*
 
   761 ML {*
 
   438   fun lift_thm_fset_note name thm lthy =
 
   762   fun lift_thm_fset_note name thm lthy =
 
   439     let
 
   763     let
 
   440       val lifted_thm = lift_thm_fset lthy thm;
 
   764       val lifted_thm = lift_thm_fset lthy thm;
nominal2