equal
deleted
inserted
replaced
358 ML_prf {* val qtm = #concl (fst (Subgoal.focus @{context} 1 (#goal (Isar.goal ())))) *} |
358 ML_prf {* val qtm = #concl (fst (Subgoal.focus @{context} 1 (#goal (Isar.goal ())))) *} |
359 apply(tactic {* procedure_tac @{context} @{thm list.induct} 1 *}) |
359 apply(tactic {* procedure_tac @{context} @{thm list.induct} 1 *}) |
360 apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *}) |
360 apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *}) |
361 prefer 2 |
361 prefer 2 |
362 apply(tactic {* clean_tac @{context} [quot] defs 1 *}) |
362 apply(tactic {* clean_tac @{context} [quot] defs 1 *}) |
|
363 apply(rule_tac a="\<forall>(P\<Colon>'a fset \<Rightarrow> bool) l\<Colon>'a fset. P EMPTY \<longrightarrow> (\<forall>(a\<Colon>'a) x\<Colon>'a fset. P x \<longrightarrow> P (INSERT a x)) \<longrightarrow> P l" in QUOT_TRUE_i) |
|
364 |
|
365 apply (drule QT_all) |
|
366 apply (drule_tac x = "x" in QT_lam) |
|
367 apply (drule QT_all) |
|
368 apply (drule_tac x = "y" in QT_lam) |
|
369 apply (tactic {* quot_true_tac @{context} (fst o strip_comb) 1 *}) |
363 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 3 *) (* Ball-Ball *) |
370 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 3 *) (* Ball-Ball *) |
364 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *) |
371 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *) |
365 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 2 *) (* lam-lam-elim for R = (===>) *) |
372 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 2 *) (* lam-lam-elim for R = (===>) *) |
366 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 3 *) (* Ball-Ball *) |
373 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 3 *) (* Ball-Ball *) |
367 apply(tactic {* inj_repabs_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 *) |