369 apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* B *) (* Cong *) |
369 apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* B *) (* Cong *) |
370 apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* B *) (* Cong *) |
370 apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* B *) (* Cong *) |
371 apply(tactic {* inj_repabs_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 {* inj_repabs_tac_fset' @{context} 1*}) (* B *) (* Cong *) |
372 apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* B *) (* Cong *) |
373 apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* 8 *) (* = reflexivity arising from cong *) |
373 apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* 8 *) (* = reflexivity arising from cong *) |
374 |
|
375 apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* C *) (* = and extensionality *) |
374 apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* C *) (* = and extensionality *) |
376 apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* 3 *) (* Ball-Ball *) |
375 apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* 3 *) (* Ball-Ball *) |
377 apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *) |
376 apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *) |
378 apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* 2 *) (* lam-lam-elim for R = (===>) *) |
377 apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* 2 *) (* lam-lam-elim for R = (===>) *) |
379 apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* B *) (* Cong *) |
378 apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* B *) (* Cong *) |
380 apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* B *) (* Cong *) |
379 apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* B *) (* Cong *) |
381 apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* 8 *) (* = reflexivity arising from cong *) |
380 apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* 8 *) (* = reflexivity arising from cong *) |
382 apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* A *) (* application if type needs lifting *) |
381 apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* A *) (* application if type needs lifting *) |
383 apply(tactic {* inj_repabs_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 *) |
384 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* E *) (* R x y assumptions *) |
383 apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* E *) (* R x y assumptions *) |
385 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *) |
384 apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *) |
386 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* E *) (* R x y assumptions *) |
385 apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* E *) (* R x y assumptions *) |
387 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* A *) (* application if type needs lifting *) |
386 apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* A *) (* application if type needs lifting *) |
388 apply(tactic {* inj_repabs_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 *) |
389 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* E *) (* R x y assumptions *) |
388 apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* E *) (* R x y assumptions *) |
390 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *) |
389 apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *) |
391 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* A *) (* application if type needs lifting *) |
390 apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* A *) (* application if type needs lifting *) |
392 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* A *) (* application if type needs lifting *) |
391 apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* A *) (* application if type needs lifting *) |
393 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 7 *) (* respectfulness *) |
392 apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* 7 *) (* respectfulness *) |
394 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 8 *) (* = reflexivity arising from cong *) |
393 apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* 8 *) (* = reflexivity arising from cong *) |
395 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *) |
394 apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *) |
396 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* E *) (* R x y assumptions *) |
395 apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* E *) (* R x y assumptions *) |
397 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* A *) (* application if type needs lifting *) |
396 apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* A *) (* application if type needs lifting *) |
398 apply(tactic {* inj_repabs_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 *) |
399 done |
398 done |
400 |
399 |
401 quotient_def |
400 quotient_def |
402 fset_rec::"'a \<Rightarrow> ('b \<Rightarrow> 'b fset \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'b fset \<Rightarrow> 'a" |
401 fset_rec::"'a \<Rightarrow> ('b \<Rightarrow> 'b fset \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'b fset \<Rightarrow> 'a" |
403 where |
402 where |