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 445 f1c0a66284d3
parent 442 7beed9b75ea2
child 446 84ee3973f083
equal deleted inserted replaced
444:75af61f32ece 445:f1c0a66284d3 
   326 
   326 
   327 lemma "(\<not> IN x xa) = (CARD (INSERT x xa) = Suc (CARD xa))"
 
   327 lemma "(\<not> IN x xa) = (CARD (INSERT x xa) = Suc (CARD xa))"
 
   328 apply (tactic {* lift_tac_fset @{context} @{thm not_mem_card1} 1 *})
 
   328 apply (tactic {* lift_tac_fset @{context} @{thm not_mem_card1} 1 *})
 
   329 done
 
   329 done
 
   330 
   330 
   331 ML {* fun r_mk_comb_tac_fset lthy = r_mk_comb_tac' lthy rty [quot] [rel_refl] [trans2] rsp_thms *}
 
   331 ML {* fun inj_repabs_tac_fset lthy = inj_repabs_tac' lthy rty [quot] [rel_refl] [trans2] rsp_thms *}
 
   332 
   332 
   333 lemma "FOLD f g (z::'b) (INSERT a x) =
 
   333 lemma "FOLD f g (z::'b) (INSERT a x) =
 
   334   (if rsp_fold f then if IN a x then FOLD f g z x else f (g a) (FOLD f g z x) else z)"
 
   334   (if rsp_fold f then if IN a x then FOLD f g z x else f (g a) (FOLD f g z x) else z)"
 
   335 apply(tactic {* lift_tac_fset @{context} @{thm fold1.simps(2)} 1 *})
 
   335 apply(tactic {* lift_tac_fset @{context} @{thm fold1.simps(2)} 1 *})
 
   336 done
 
   336 done
 
   348 lemma "\<lbrakk>P EMPTY; \<And>a x. P x \<Longrightarrow> P (INSERT a x)\<rbrakk> \<Longrightarrow> P l"
 
   348 lemma "\<lbrakk>P EMPTY; \<And>a x. P x \<Longrightarrow> P (INSERT a x)\<rbrakk> \<Longrightarrow> P l"
 
   349 apply(tactic {* procedure_tac @{context} @{thm list.induct} 1 *})
 
   349 apply(tactic {* procedure_tac @{context} @{thm list.induct} 1 *})
 
   350 apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *})
 
   350 apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *})
 
   351 prefer 2
 
   351 prefer 2
 
   352 apply(rule cheat)
 
   352 apply(rule cheat)
 
   353 apply(tactic {* r_mk_comb_tac_fset @{context} 1*}) (* 3 *) (* Ball-Ball *)
 
   353 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 3 *) (* Ball-Ball *)
 
   354 apply(tactic {* r_mk_comb_tac_fset @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *)
 
   354 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *)
 
   355 apply(tactic {* r_mk_comb_tac_fset @{context} 1*}) (* 2 *) (* lam-lam-elim for R = (===>) *) 
   355 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 2 *) (* lam-lam-elim for R = (===>) *) 
   356 apply(tactic {* r_mk_comb_tac_fset @{context} 1*}) (* 3 *) (* Ball-Ball *)
 
   356 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 3 *) (* Ball-Ball *)
 
   357 apply(tactic {* r_mk_comb_tac_fset @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *)
 
   357 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *)
 
   358 apply(tactic {* r_mk_comb_tac_fset @{context} 1*}) (* 2 *) (* lam-lam-elim for R = (===>) *) 
   358 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 2 *) (* lam-lam-elim for R = (===>) *) 
   359 apply(tactic {* r_mk_comb_tac_fset @{context} 1*}) (* B *) (* Cong *)
 
   359 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* B *) (* Cong *)
 
   360 apply(tactic {* r_mk_comb_tac_fset @{context} 1*}) (* B *) (* Cong *)
 
   360 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* B *) (* Cong *)
 
   361 apply(tactic {* r_mk_comb_tac_fset @{context} 1*}) (* 8 *) (* = reflexivity arising from cong *)
 
   361 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 8 *) (* = reflexivity arising from cong *)
 
   362 apply(tactic {* r_mk_comb_tac_fset @{context} 1*}) (* A *) (* application if type needs lifting *)
 
   362 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* A *) (* application if type needs lifting *)
 
   363 apply(tactic {* r_mk_comb_tac_fset @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *)
 
   363 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *)
 
   364 apply(tactic {* r_mk_comb_tac_fset @{context} 1*}) (* E *) (* R x y assumptions *)
 
   364 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* E *) (* R x y assumptions *)
 
   365 apply(tactic {* r_mk_comb_tac_fset @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *)
 
   365 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *)
 
   366 apply(tactic {* r_mk_comb_tac_fset @{context} 1*}) (* D *) (* reflexivity of basic relations *)
 
   366 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* D *) (* reflexivity of basic relations *)
 
   367 apply(tactic {* r_mk_comb_tac_fset @{context} 1*}) (* B *) (* Cong *)
 
   367 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* B *) (* Cong *)
 
   368 apply(tactic {* r_mk_comb_tac_fset @{context} 1*}) (* B *) (* Cong *)
 
   368 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* B *) (* Cong *)
 
   369 apply(tactic {* r_mk_comb_tac_fset @{context} 1*}) (* 8 *) (* = reflexivity arising from cong *)
 
   369 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 8 *) (* = reflexivity arising from cong *)
 
   370 apply(tactic {* r_mk_comb_tac_fset @{context} 1*}) (* B *) (* Cong *)
 
   370 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* B *) (* Cong *)
 
   371 apply(tactic {* r_mk_comb_tac_fset @{context} 1*}) (* 8 *) (* = reflexivity arising from cong *)
 
   371 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 8 *) (* = reflexivity arising from cong *)
 
   372 apply(tactic {* r_mk_comb_tac_fset @{context} 1*}) (* C *) (* = and extensionality *)
 
   372 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* C *) (* = and extensionality *)
 
   373 apply(tactic {* r_mk_comb_tac_fset @{context} 1*}) (* 3 *) (* Ball-Ball *)
 
   373 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 3 *) (* Ball-Ball *)
 
   374 apply(tactic {* r_mk_comb_tac_fset @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *)
 
   374 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *)
 
   375 apply(tactic {* r_mk_comb_tac_fset @{context} 1*}) (* 2 *) (* lam-lam-elim for R = (===>) *) 
   375 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 2 *) (* lam-lam-elim for R = (===>) *) 
   376 apply(tactic {* r_mk_comb_tac_fset @{context} 1*}) (* B *) (* Cong *)
 
   376 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* B *) (* Cong *)
 
   377 apply(tactic {* r_mk_comb_tac_fset @{context} 1*}) (* B *) (* Cong *)
 
   377 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* B *) (* Cong *)
 
   378 apply(tactic {* r_mk_comb_tac_fset @{context} 1*}) (* 8 *) (* = reflexivity arising from cong *)
 
   378 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 8 *) (* = reflexivity arising from cong *)
 
   379 apply(tactic {* r_mk_comb_tac_fset @{context} 1*}) (* A *) (* application if type needs lifting *)
 
   379 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* A *) (* application if type needs lifting *)
 
   380 apply(tactic {* r_mk_comb_tac_fset @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *)
 
   380 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *)
 
   381 apply(tactic {* r_mk_comb_tac_fset @{context} 1*}) (* E *) (* R x y assumptions *)
 
   381 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* E *) (* R x y assumptions *)
 
   382 apply(tactic {* r_mk_comb_tac_fset @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *)
 
   382 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *)
 
   383 apply(tactic {* r_mk_comb_tac_fset @{context} 1*}) (* E *) (* R x y assumptions *)
 
   383 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* E *) (* R x y assumptions *)
 
   384 apply(tactic {* r_mk_comb_tac_fset @{context} 1*}) (* A *) (* application if type needs lifting *)
 
   384 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* A *) (* application if type needs lifting *)
 
   385 apply(tactic {* r_mk_comb_tac_fset @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *)
 
   385 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *)
 
   386 apply(tactic {* r_mk_comb_tac_fset @{context} 1*}) (* E *) (* R x y assumptions *)
 
   386 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* E *) (* R x y assumptions *)
 
   387 apply(tactic {* r_mk_comb_tac_fset @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *)
 
   387 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *)
 
   388 apply(tactic {* r_mk_comb_tac_fset @{context} 1*}) (* A *) (* application if type needs lifting *)
 
   388 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* A *) (* application if type needs lifting *)
 
   389 apply(tactic {* r_mk_comb_tac_fset @{context} 1*}) (* A *) (* application if type needs lifting *)
 
   389 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* A *) (* application if type needs lifting *)
 
   390 apply(tactic {* r_mk_comb_tac_fset @{context} 1*}) (* 7 *) (* respectfulness *)
 
   390 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 7 *) (* respectfulness *)
 
   391 apply(tactic {* r_mk_comb_tac_fset @{context} 1*}) (* 8 *) (* = reflexivity arising from cong *)
 
   391 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 8 *) (* = reflexivity arising from cong *)
 
   392 apply(tactic {* r_mk_comb_tac_fset @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *)
 
   392 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *)
 
   393 apply(tactic {* r_mk_comb_tac_fset @{context} 1*}) (* E *) (* R x y assumptions *)
 
   393 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* E *) (* R x y assumptions *)
 
   394 apply(tactic {* r_mk_comb_tac_fset @{context} 1*}) (* A *) (* application if type needs lifting *)
 
   394 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* A *) (* application if type needs lifting *)
 
   395 apply(tactic {* r_mk_comb_tac_fset @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *)
 
   395 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *)
 
   396 apply(tactic {* r_mk_comb_tac_fset @{context} 1*}) (* E *) (* R x y assumptions *)
 
   396 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* E *) (* R x y assumptions *)
 
   397 apply(tactic {* r_mk_comb_tac_fset @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *)
 
   397 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *)
 
   398 apply(tactic {* r_mk_comb_tac_fset @{context} 1*}) (* E *) (* R x y assumptions *)
 
   398 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* E *) (* R x y assumptions *)
 
   399 done
 
   399 done
 
   400 
   400 
   401 
   401 
   402 quotient_def
 
   402 quotient_def
 
   403   fset_rec::"'a \<Rightarrow> ('b \<Rightarrow> 'b fset \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'b fset \<Rightarrow> 'a"
 
   403   fset_rec::"'a \<Rightarrow> ('b \<Rightarrow> 'b fset \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'b fset \<Rightarrow> 'a"
 
   442   apply (rule a)
 
   442   apply (rule a)
 
   443   apply (rule b)
 
   443   apply (rule b)
 
   444   apply (assumption)
 
   444   apply (assumption)
 
   445   done
 
   445   done
 
   446 
   446 
   447 ML {* fun r_mk_comb_tac_fset lthy = r_mk_comb_tac lthy rty [quot] [rel_refl] [trans2] rsp_thms *}
 
   447 ML {* fun inj_repabs_tac_fset lthy = inj_repabs_tac lthy rty [quot] [rel_refl] [trans2] rsp_thms *}
 
   448 ML {* fun r_mk_comb_tac_fset' lthy = r_mk_comb_tac' lthy rty [quot] [rel_refl] [trans2] rsp_thms *}
 
   448 ML {* fun inj_repabs_tac_fset' lthy = inj_repabs_tac' lthy rty [quot] [rel_refl] [trans2] rsp_thms *}
 
   449 
   449 
   450 (* Construction site starts here *)
 
   450 (* Construction site starts here *)
 
   451 lemma "P (x :: 'a list) (EMPTY :: 'c fset) \<Longrightarrow> (\<And>e t. P x t \<Longrightarrow> P x (INSERT e t)) \<Longrightarrow> P x l"
 
   451 lemma "P (x :: 'a list) (EMPTY :: 'c fset) \<Longrightarrow> (\<And>e t. P x t \<Longrightarrow> P x (INSERT e t)) \<Longrightarrow> P x l"
 
   452 apply (tactic {* procedure_tac @{context} @{thm list_induct_part} 1 *})
 
   452 apply (tactic {* procedure_tac @{context} @{thm list_induct_part} 1 *})
 
   453 apply (tactic {* regularize_tac @{context} [rel_eqv] 1 *})
 
   453 apply (tactic {* regularize_tac @{context} [rel_eqv] 1 *})
 
   458 apply (rule FUN_QUOTIENT)
 
   458 apply (rule FUN_QUOTIENT)
 
   459 apply (rule QUOTIENT_fset)
 
   459 apply (rule QUOTIENT_fset)
 
   460 apply (rule IDENTITY_QUOTIENT)
 
   460 apply (rule IDENTITY_QUOTIENT)
 
   461 apply (rule IDENTITY_QUOTIENT)
 
   461 apply (rule IDENTITY_QUOTIENT)
 
   462 apply (rule IDENTITY_QUOTIENT)
 
   462 apply (rule IDENTITY_QUOTIENT)
 
   463 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
 
   463 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
 
   464 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
 
   464 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
 
   465 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
 
   465 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
 
   466 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
 
   466 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
 
   467 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
 
   467 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
 
   468 apply (tactic {* (APPLY_RSP_TAC rty @{context}) 1 *})
 
   468 apply (tactic {* (APPLY_RSP_TAC rty @{context}) 1 *})
 
   469 apply (rule IDENTITY_QUOTIENT)
 
   469 apply (rule IDENTITY_QUOTIENT)
 
   470 apply (rule IDENTITY_QUOTIENT)
 
   470 apply (rule IDENTITY_QUOTIENT)
 
   471 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
 
   471 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
 
   472 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
 
   472 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
 
   473 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
 
   473 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
 
   474 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
 
   474 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
 
   475 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
 
   475 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
 
   476 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
 
   476 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
 
   477 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
 
   477 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
 
   478 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
 
   478 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
 
   479 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
 
   479 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
 
   480 apply (tactic {* (APPLY_RSP_TAC rty @{context}) 1 *})
 
   480 apply (tactic {* (APPLY_RSP_TAC rty @{context}) 1 *})
 
   481 apply (rule IDENTITY_QUOTIENT)
 
   481 apply (rule IDENTITY_QUOTIENT)
 
   482 apply (rule FUN_QUOTIENT)
 
   482 apply (rule FUN_QUOTIENT)
 
   483 apply (rule QUOTIENT_fset)
 
   483 apply (rule QUOTIENT_fset)
 
   484 apply (rule IDENTITY_QUOTIENT)
 
   484 apply (rule IDENTITY_QUOTIENT)
 
   485 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
 
   485 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
 
   486 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
 
   486 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
 
   487 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
 
   487 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
 
   488 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
 
   488 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
 
   489 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
 
   489 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
 
   490 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
 
   490 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
 
   491 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
 
   491 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
 
   492 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
 
   492 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
 
   493 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
 
   493 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
 
   494 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
 
   494 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
 
   495 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
 
   495 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
 
   496 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
 
   496 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
 
   497 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
 
   497 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
 
   498 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
 
   498 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
 
   499 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
 
   499 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
 
   500 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
 
   500 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
 
   501 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
 
   501 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
 
   502 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
 
   502 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
 
   503 apply (tactic {* instantiate_tac @{thm APPLY_RSP2} @{context} 1 *})
 
   503 apply (tactic {* instantiate_tac @{thm APPLY_RSP2} @{context} 1 *})
 
   504 apply (tactic {* (instantiate_tac @{thm REP_ABS_RSP(1)} @{context} THEN' (RANGE [quotient_tac [quot]])) 1 *})
 
   504 apply (tactic {* (instantiate_tac @{thm REP_ABS_RSP(1)} @{context} THEN' (RANGE [quotient_tac [quot]])) 1 *})
 
   505 apply assumption
 
   505 apply assumption
 
   506 apply (rule refl)
 
   506 apply (rule refl)
 
   507 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
 
   507 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
 
   508 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
 
   508 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
 
   509 apply (tactic {* instantiate_tac @{thm APPLY_RSP2} @{context} 1 *})
 
   509 apply (tactic {* instantiate_tac @{thm APPLY_RSP2} @{context} 1 *})
 
   510 apply (tactic {* instantiate_tac @{thm APPLY_RSP2} @{context} 1 *})
 
   510 apply (tactic {* instantiate_tac @{thm APPLY_RSP2} @{context} 1 *})
 
   511 apply (tactic {* (instantiate_tac @{thm REP_ABS_RSP(1)} @{context} THEN' (RANGE [quotient_tac [quot]])) 1 *})
 
   511 apply (tactic {* (instantiate_tac @{thm REP_ABS_RSP(1)} @{context} THEN' (RANGE [quotient_tac [quot]])) 1 *})
 
   512 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
 
   512 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
 
   513 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
 
   513 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
 
   514 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *})
 
   514 apply (tactic {* REPEAT_ALL_NEW (inj_repabs_tac_fset @{context}) 1 *})
 
   515 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
 
   515 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
 
   516 apply (tactic {* instantiate_tac @{thm APPLY_RSP2} @{context} 1 *})
 
   516 apply (tactic {* instantiate_tac @{thm APPLY_RSP2} @{context} 1 *})
 
   517 apply (tactic {* (instantiate_tac @{thm REP_ABS_RSP(1)} @{context} THEN' (RANGE [quotient_tac [quot]])) 1 *})
 
   517 apply (tactic {* (instantiate_tac @{thm REP_ABS_RSP(1)} @{context} THEN' (RANGE [quotient_tac [quot]])) 1 *})
 
   518 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
 
   518 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
 
   519 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
 
   519 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
 
   520 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
 
   520 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
 
   521 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
 
   521 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
 
   522 apply (tactic {* clean_tac @{context} [quot] defs [(@{typ "('a list \<Rightarrow> 'c list \<Rightarrow> bool)"},@{typ "('a list \<Rightarrow> 'c fset \<Rightarrow> bool)"})] 1 *})
 
   522 apply (tactic {* clean_tac @{context} [quot] defs [(@{typ "('a list \<Rightarrow> 'c list \<Rightarrow> bool)"},@{typ "('a list \<Rightarrow> 'c fset \<Rightarrow> bool)"})] 1 *})
 
   523 done
 
   523 done
 
   524 
   524 
   525 end
 
   525 end
nominal2