FSet.thy
changeset 459 020e27417b59
parent 458 44a70e69ef92
child 462 0911d3aabf47
equal deleted inserted replaced
458:44a70e69ef92 459:020e27417b59
   503 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
   503 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
   504 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
   504 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
   505 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
   505 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
   506 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
   506 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
   507 apply (tactic {* instantiate_tac @{thm APPLY_RSP2} @{context} 1 *})
   507 apply (tactic {* instantiate_tac @{thm APPLY_RSP2} @{context} 1 *})
   508 apply (tactic {* (instantiate_tac @{thm REP_ABS_RSP(1)} @{context} THEN' (RANGE [quotient_tac [quot]])) 1 *})
   508 apply (tactic {* (instantiate_tac @{thm REP_ABS_RSP} @{context} THEN' (RANGE [quotient_tac [quot]])) 1 *})
   509 apply assumption
   509 apply assumption
   510 apply (rule refl)
   510 apply (rule refl)
   511 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
   511 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
   512 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
   512 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
   513 apply (tactic {* instantiate_tac @{thm APPLY_RSP2} @{context} 1 *})
   513 apply (tactic {* instantiate_tac @{thm APPLY_RSP2} @{context} 1 *})
   514 apply (tactic {* instantiate_tac @{thm APPLY_RSP2} @{context} 1 *})
   514 apply (tactic {* instantiate_tac @{thm APPLY_RSP2} @{context} 1 *})
   515 apply (tactic {* (instantiate_tac @{thm REP_ABS_RSP(1)} @{context} THEN' (RANGE [quotient_tac [quot]])) 1 *})
   515 apply (tactic {* (instantiate_tac @{thm REP_ABS_RSP} @{context} THEN' (RANGE [quotient_tac [quot]])) 1 *})
   516 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
   516 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
   517 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
   517 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
   518 apply (tactic {* REPEAT_ALL_NEW (inj_repabs_tac_fset @{context}) 1 *})
   518 apply (tactic {* REPEAT_ALL_NEW (inj_repabs_tac_fset @{context}) 1 *})
   519 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
   519 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
   520 apply (tactic {* instantiate_tac @{thm APPLY_RSP2} @{context} 1 *})
   520 apply (tactic {* instantiate_tac @{thm APPLY_RSP2} @{context} 1 *})
   521 apply (tactic {* (instantiate_tac @{thm REP_ABS_RSP(1)} @{context} THEN' (RANGE [quotient_tac [quot]])) 1 *})
   521 apply (tactic {* (instantiate_tac @{thm REP_ABS_RSP} @{context} THEN' (RANGE [quotient_tac [quot]])) 1 *})
   522 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
   522 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
   523 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
   523 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
   524 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
   524 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
   525 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
   525 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
   526 apply (tactic {* clean_tac @{context} [quot] defs [(@{typ "('a list \<Rightarrow> 'c list \<Rightarrow> bool)"},@{typ "('a list \<Rightarrow> 'c fset \<Rightarrow> bool)"})] 1 *})
   526 apply (tactic {* clean_tac @{context} [quot] defs [(@{typ "('a list \<Rightarrow> 'c list \<Rightarrow> bool)"},@{typ "('a list \<Rightarrow> 'c fset \<Rightarrow> bool)"})] 1 *})