theory FSet+
−
imports QuotMain+
−
begin+
−
+
−
inductive+
−
  list_eq (infix "\<approx>" 50)+
−
where+
−
  "a#b#xs \<approx> b#a#xs"+
−
| "[] \<approx> []"+
−
| "xs \<approx> ys \<Longrightarrow> ys \<approx> xs"+
−
| "a#a#xs \<approx> a#xs"+
−
| "xs \<approx> ys \<Longrightarrow> a#xs \<approx> a#ys"+
−
| "\<lbrakk>xs1 \<approx> xs2; xs2 \<approx> xs3\<rbrakk> \<Longrightarrow> xs1 \<approx> xs3"+
−
+
−
lemma list_eq_refl:+
−
  shows "xs \<approx> xs"+
−
  by (induct xs) (auto intro: list_eq.intros)+
−
+
−
lemma equiv_list_eq:+
−
  shows "EQUIV list_eq"+
−
  unfolding EQUIV_REFL_SYM_TRANS REFL_def SYM_def TRANS_def+
−
  apply(auto intro: list_eq.intros list_eq_refl)+
−
  done+
−
+
−
quotient fset = "'a list" / "list_eq"+
−
  apply(rule equiv_list_eq)+
−
  done+
−
+
−
print_theorems+
−
+
−
typ "'a fset"+
−
thm "Rep_fset"+
−
thm "ABS_fset_def"+
−
+
−
quotient_def +
−
  EMPTY :: "'a fset"+
−
where+
−
  "EMPTY \<equiv> ([]::'a list)"+
−
+
−
term Nil+
−
term EMPTY+
−
thm EMPTY_def+
−
+
−
quotient_def +
−
  INSERT :: "'a \<Rightarrow> 'a fset \<Rightarrow> 'a fset"+
−
where+
−
  "INSERT \<equiv> op #"+
−
+
−
term Cons+
−
term INSERT+
−
thm INSERT_def+
−
+
−
quotient_def +
−
  FUNION :: "'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset"+
−
where+
−
  "FUNION \<equiv> (op @)"+
−
+
−
term append+
−
term FUNION+
−
thm FUNION_def+
−
+
−
thm QUOTIENT_fset+
−
+
−
thm QUOT_TYPE_I_fset.thm11+
−
+
−
+
−
fun+
−
  membship :: "'a \<Rightarrow> 'a list \<Rightarrow> bool" (infix "memb" 100)+
−
where+
−
  m1: "(x memb []) = False"+
−
| m2: "(x memb (y#xs)) = ((x=y) \<or> (x memb xs))"+
−
+
−
fun+
−
  card1 :: "'a list \<Rightarrow> nat"+
−
where+
−
  card1_nil: "(card1 []) = 0"+
−
| card1_cons: "(card1 (x # xs)) = (if (x memb xs) then (card1 xs) else (Suc (card1 xs)))"+
−
+
−
quotient_def +
−
  CARD :: "'a fset \<Rightarrow> nat"+
−
where+
−
  "CARD \<equiv> card1"+
−
+
−
term card1+
−
term CARD+
−
thm CARD_def+
−
+
−
(* text {*+
−
 Maybe make_const_def should require a theorem that says that the particular lifted function+
−
 respects the relation. With it such a definition would be impossible:+
−
 make_const_def @{binding CARD} @{term "length"} NoSyn @{typ "'a list"} @{typ "'a fset"} #> snd+
−
*}*)+
−
+
−
lemma card1_0:+
−
  fixes a :: "'a list"+
−
  shows "(card1 a = 0) = (a = [])"+
−
  by (induct a) auto+
−
+
−
lemma not_mem_card1:+
−
  fixes x :: "'a"+
−
  fixes xs :: "'a list"+
−
  shows "(~(x memb xs)) = (card1 (x # xs) = Suc (card1 xs))"+
−
  by auto+
−
+
−
lemma mem_cons:+
−
  fixes x :: "'a"+
−
  fixes xs :: "'a list"+
−
  assumes a : "x memb xs"+
−
  shows "x # xs \<approx> xs"+
−
  using a by (induct xs) (auto intro: list_eq.intros )+
−
+
−
lemma card1_suc:+
−
  fixes xs :: "'a list"+
−
  fixes n :: "nat"+
−
  assumes c: "card1 xs = Suc n"+
−
  shows "\<exists>a ys. ~(a memb ys) \<and> xs \<approx> (a # ys)"+
−
  using c+
−
apply(induct xs)+
−
apply (metis Suc_neq_Zero card1_0)+
−
apply (metis QUOT_TYPE_I_fset.R_trans card1_cons list_eq_refl mem_cons)+
−
done+
−
+
−
definition+
−
  rsp_fold+
−
where+
−
  "rsp_fold f = ((!u v. (f u v = f v u)) \<and> (!u v w. ((f u (f v w) = f (f u v) w))))"+
−
+
−
primrec+
−
  fold1+
−
where+
−
  "fold1 f (g :: 'a \<Rightarrow> 'b) (z :: 'b) [] = z"+
−
| "fold1 f g z (a # A) =+
−
     (if rsp_fold f+
−
     then (+
−
       if (a memb A) then (fold1 f g z A) else (f (g a) (fold1 f g z A))+
−
     ) else z)"+
−
+
−
(* fold1_def is not usable, but: *)+
−
thm fold1.simps+
−
+
−
lemma fs1_strong_cases:+
−
  fixes X :: "'a list"+
−
  shows "(X = []) \<or> (\<exists>a. \<exists> Y. (~(a memb Y) \<and> (X \<approx> a # Y)))"+
−
  apply (induct X)+
−
  apply (simp)+
−
  apply (metis QUOT_TYPE_I_fset.thm11 list_eq_refl mem_cons m1)+
−
  done+
−
+
−
quotient_def+
−
  IN :: "'a \<Rightarrow> 'a fset \<Rightarrow> bool"+
−
where+
−
  "IN \<equiv> membship"+
−
+
−
term membship+
−
term IN+
−
thm IN_def+
−
+
−
term fold1+
−
quotient_def +
−
  FOLD :: "('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'b fset \<Rightarrow> 'a"+
−
where+
−
  "FOLD \<equiv> fold1"+
−
+
−
term fold1+
−
term fold+
−
thm fold_def+
−
+
−
quotient_def +
−
  fmap::"('a \<Rightarrow> 'b) \<Rightarrow> 'a fset \<Rightarrow> 'b fset"+
−
where+
−
  "fmap \<equiv> map"+
−
+
−
term map+
−
term fmap+
−
thm fmap_def+
−
+
−
ML {* val defs = @{thms EMPTY_def IN_def FUNION_def CARD_def INSERT_def fmap_def FOLD_def} *}+
−
+
−
lemma memb_rsp:+
−
  fixes z+
−
  assumes a: "x \<approx> y"+
−
  shows "(z memb x) = (z memb y)"+
−
  using a by induct auto+
−
+
−
lemma ho_memb_rsp[quot_rsp]:+
−
  "(op = ===> (op \<approx> ===> op =)) (op memb) (op memb)"+
−
  by (simp add: memb_rsp)+
−
+
−
lemma card1_rsp:+
−
  fixes a b :: "'a list"+
−
  assumes e: "a \<approx> b"+
−
  shows "card1 a = card1 b"+
−
  using e by induct (simp_all add:memb_rsp)+
−
+
−
lemma ho_card1_rsp[quot_rsp]: +
−
  "(op \<approx> ===> op =) card1 card1"+
−
  by (simp add: card1_rsp)+
−
+
−
lemma cons_rsp[quot_rsp]:+
−
  fixes z+
−
  assumes a: "xs \<approx> ys"+
−
  shows "(z # xs) \<approx> (z # ys)"+
−
  using a by (rule list_eq.intros(5))+
−
+
−
lemma ho_cons_rsp[quot_rsp]:+
−
  "(op = ===> op \<approx> ===> op \<approx>) op # op #"+
−
  by (simp add: cons_rsp)+
−
+
−
lemma append_rsp_fst:+
−
  assumes a : "l1 \<approx> l2"+
−
  shows "(l1 @ s) \<approx> (l2 @ s)"+
−
  using a+
−
  by (induct) (auto intro: list_eq.intros list_eq_refl)+
−
+
−
lemma append_end:+
−
  shows "(e # l) \<approx> (l @ [e])"+
−
  apply (induct l)+
−
  apply (auto intro: list_eq.intros list_eq_refl)+
−
  done+
−
+
−
lemma rev_rsp:+
−
  shows "a \<approx> rev a"+
−
  apply (induct a)+
−
  apply simp+
−
  apply (rule list_eq_refl)+
−
  apply simp_all+
−
  apply (rule list_eq.intros(6))+
−
  prefer 2+
−
  apply (rule append_rsp_fst)+
−
  apply assumption+
−
  apply (rule append_end)+
−
  done+
−
+
−
lemma append_sym_rsp:+
−
  shows "(a @ b) \<approx> (b @ a)"+
−
  apply (rule list_eq.intros(6))+
−
  apply (rule append_rsp_fst)+
−
  apply (rule rev_rsp)+
−
  apply (rule list_eq.intros(6))+
−
  apply (rule rev_rsp)+
−
  apply (simp)+
−
  apply (rule append_rsp_fst)+
−
  apply (rule list_eq.intros(3))+
−
  apply (rule rev_rsp)+
−
  done+
−
+
−
lemma append_rsp:+
−
  assumes a : "l1 \<approx> r1"+
−
  assumes b : "l2 \<approx> r2 "+
−
  shows "(l1 @ l2) \<approx> (r1 @ r2)"+
−
  apply (rule list_eq.intros(6))+
−
  apply (rule append_rsp_fst)+
−
  using a apply (assumption)+
−
  apply (rule list_eq.intros(6))+
−
  apply (rule append_sym_rsp)+
−
  apply (rule list_eq.intros(6))+
−
  apply (rule append_rsp_fst)+
−
  using b apply (assumption)+
−
  apply (rule append_sym_rsp)+
−
  done+
−
+
−
lemma ho_append_rsp[quot_rsp]:+
−
  "(op \<approx> ===> op \<approx> ===> op \<approx>) op @ op @"+
−
  by (simp add: append_rsp)+
−
+
−
lemma map_rsp:+
−
  assumes a: "a \<approx> b"+
−
  shows "map f a \<approx> map f b"+
−
  using a+
−
  apply (induct)+
−
  apply(auto intro: list_eq.intros)+
−
  done+
−
+
−
lemma ho_map_rsp[quot_rsp]:+
−
  "(op = ===> op \<approx> ===> op \<approx>) map map"+
−
  by (simp add: map_rsp)+
−
+
−
lemma map_append:+
−
  "(map f (a @ b)) \<approx> (map f a) @ (map f b)"+
−
 by simp (rule list_eq_refl)+
−
+
−
lemma ho_fold_rsp[quot_rsp]:+
−
  "(op = ===> op = ===> op = ===> op \<approx> ===> op =) fold1 fold1"+
−
  apply (auto simp add: FUN_REL_EQ)+
−
  apply (case_tac "rsp_fold x")+
−
  prefer 2+
−
  apply (erule_tac list_eq.induct)+
−
  apply (simp_all)+
−
  apply (erule_tac list_eq.induct)+
−
  apply (simp_all)+
−
  apply (auto simp add: memb_rsp rsp_fold_def)+
−
done+
−
+
−
print_quotients+
−
+
−
ML {* val qty = @{typ "'a fset"} *}+
−
ML {* val rsp_thms =+
−
  @{thms ho_memb_rsp ho_cons_rsp ho_card1_rsp ho_map_rsp ho_append_rsp ho_fold_rsp}+
−
  @ @{thms ho_all_prs ho_ex_prs} *}+
−
+
−
ML {* val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data @{context} qty *}+
−
ML {* val (trans2, reps_same, absrep, quot) = lookup_quot_thms @{context} "fset"; *}+
−
ML {* val consts = lookup_quot_consts defs *}+
−
ML {* fun lift_tac_fset lthy t = lift_tac lthy t [rel_eqv] rty [quot] defs *}+
−
+
−
lemma "IN x EMPTY = False"+
−
by (tactic {* lift_tac_fset @{context} @{thm m1} 1 *})+
−
+
−
lemma "IN x (INSERT y xa) = (x = y \<or> IN x xa)"+
−
by (tactic {* lift_tac_fset @{context} @{thm m2} 1 *})+
−
+
−
lemma "INSERT a (INSERT a x) = INSERT a x"+
−
apply (tactic {* lift_tac_fset @{context} @{thm list_eq.intros(4)} 1 *})+
−
done+
−
+
−
lemma "x = xa \<Longrightarrow> INSERT a x = INSERT a xa"+
−
apply (tactic {* lift_tac_fset @{context} @{thm list_eq.intros(5)} 1 *})+
−
done+
−
+
−
lemma "CARD x = Suc n \<Longrightarrow> (\<exists>a b. \<not> IN a b & x = INSERT a b)"+
−
apply (tactic {* lift_tac_fset @{context} @{thm card1_suc} 1 *})+
−
done+
−
+
−
lemma "(\<not> IN x xa) = (CARD (INSERT x xa) = Suc (CARD xa))"+
−
apply (tactic {* lift_tac_fset @{context} @{thm not_mem_card1} 1 *})+
−
done+
−
+
−
ML {* fun inj_repabs_tac_fset lthy = inj_repabs_tac lthy rty [quot] [rel_refl] [trans2] *}+
−
+
−
lemma "FOLD f g (z::'b) (INSERT a x) =+
−
  (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)"+
−
apply(tactic {* lift_tac_fset @{context} @{thm fold1.simps(2)} 1 *})+
−
done+
−
+
−
lemma "fmap f (FUNION (x::'b fset) (xa::'b fset)) = FUNION (fmap f x) (fmap f xa)"+
−
apply (tactic {* lift_tac_fset @{context} @{thm map_append} 1 *})+
−
done+
−
+
−
lemma "FUNION (FUNION x xa) xb = FUNION x (FUNION xa xb)"+
−
apply (tactic {* lift_tac_fset @{context} @{thm append_assoc} 1 *})+
−
done+
−
+
−
lemma cheat: "P" sorry+
−
+
−
lemma "\<lbrakk>P EMPTY; \<And>a x. P x \<Longrightarrow> P (INSERT a x)\<rbrakk> \<Longrightarrow> P l"+
−
apply(tactic {* procedure_tac @{context} @{thm list.induct} 1 *})+
−
apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *})+
−
prefer 2+
−
apply(rule cheat)+
−
apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 3 *) (* Ball-Ball *)+
−
apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *)+
−
apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 2 *) (* lam-lam-elim for R = (===>) *) +
−
apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 3 *) (* Ball-Ball *)+
−
apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *)+
−
apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 2 *) (* lam-lam-elim for R = (===>) *) +
−
apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* B *) (* Cong *)+
−
apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* B *) (* Cong *)+
−
apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 8 *) (* = reflexivity arising from cong *)+
−
apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* A *) (* application if type needs lifting *)+
−
apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *)+
−
apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* E *) (* R x y assumptions *)+
−
apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *)+
−
apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* D *) (* reflexivity of basic relations *)+
−
apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* B *) (* Cong *)+
−
apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* B *) (* Cong *)+
−
apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 8 *) (* = reflexivity arising from cong *)+
−
apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* B *) (* Cong *)+
−
apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 8 *) (* = reflexivity arising from cong *)+
−
apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* C *) (* = and extensionality *)+
−
apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 3 *) (* Ball-Ball *)+
−
apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *)+
−
apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 2 *) (* lam-lam-elim for R = (===>) *) +
−
apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* B *) (* Cong *)+
−
apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* B *) (* Cong *)+
−
apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 8 *) (* = reflexivity arising from cong *)+
−
apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* A *) (* application if type needs lifting *)+
−
apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *)+
−
apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* E *) (* R x y assumptions *)+
−
apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *)+
−
apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* E *) (* R x y assumptions *)+
−
apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* A *) (* application if type needs lifting *)+
−
apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *)+
−
apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* E *) (* R x y assumptions *)+
−
apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *)+
−
apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* A *) (* application if type needs lifting *)+
−
apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* A *) (* application if type needs lifting *)+
−
apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 7 *) (* respectfulness *)+
−
apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 8 *) (* = reflexivity arising from cong *)+
−
apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *)+
−
apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* E *) (* R x y assumptions *)+
−
apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* A *) (* application if type needs lifting *)+
−
apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *)+
−
done+
−
+
−
quotient_def+
−
  fset_rec::"'a \<Rightarrow> ('b \<Rightarrow> 'b fset \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'b fset \<Rightarrow> 'a"+
−
where+
−
  "fset_rec \<equiv> list_rec"+
−
+
−
quotient_def+
−
  fset_case::"'a \<Rightarrow> ('b \<Rightarrow> 'b fset \<Rightarrow> 'a) \<Rightarrow> 'b fset \<Rightarrow> 'a"+
−
where+
−
  "fset_case \<equiv> list_case"+
−
+
−
(* Probably not true without additional assumptions about the function *)+
−
lemma list_rec_rsp[quot_rsp]:+
−
  "(op = ===> (op = ===> op \<approx> ===> op =) ===> op \<approx> ===> op =) list_rec list_rec"+
−
  apply (auto simp add: FUN_REL_EQ)+
−
  apply (erule_tac list_eq.induct)+
−
  apply (simp_all)+
−
  sorry+
−
+
−
lemma list_case_rsp[quot_rsp]:+
−
  "(op = ===> (op = ===> op \<approx> ===> op =) ===> op \<approx> ===> op =) list_case list_case"+
−
  apply (auto simp add: FUN_REL_EQ)+
−
  sorry+
−
+
−
ML {* val rsp_thms = @{thms list_rec_rsp list_case_rsp} @ rsp_thms *}+
−
ML {* val defs = @{thms fset_rec_def fset_case_def} @ defs *}+
−
ML {* fun lift_tac_fset lthy t = lift_tac lthy t [rel_eqv] rty [quot] defs *}+
−
+
−
lemma "fset_rec (f1::'t) x (INSERT a xa) = x a xa (fset_rec f1 x xa)"+
−
apply (tactic {* lift_tac_fset @{context} @{thm list.recs(2)} 1 *})+
−
done+
−
+
−
lemma "fset_case (f1::'t) f2 (INSERT a xa) = f2 a xa"+
−
apply (tactic {* lift_tac_fset @{context} @{thm list.cases(2)} 1 *})+
−
done+
−
+
−
lemma list_induct_part:+
−
  assumes a: "P (x :: 'a list) ([] :: 'c list)"+
−
  assumes b: "\<And>e t. P x t \<Longrightarrow> P x (e # t)"+
−
  shows "P x l"+
−
  apply (rule_tac P="P x" in list.induct)+
−
  apply (rule a)+
−
  apply (rule b)+
−
  apply (assumption)+
−
  done+
−
+
−
ML {* fun inj_repabs_tac_fset lthy = inj_repabs_tac lthy rty [quot] [rel_refl] [trans2] *}+
−
+
−
(* Construction site starts here *)+
−
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"+
−
apply (tactic {* procedure_tac @{context} @{thm list_induct_part} 1 *})+
−
apply (tactic {* regularize_tac @{context} [rel_eqv] 1 *})+
−
apply (tactic {* (APPLY_RSP_TAC rty @{context}) 1 *})+
−
apply (rule FUN_QUOTIENT)+
−
apply (rule FUN_QUOTIENT)+
−
apply (rule IDENTITY_QUOTIENT)+
−
apply (rule FUN_QUOTIENT)+
−
apply (rule QUOTIENT_fset)+
−
apply (rule IDENTITY_QUOTIENT)+
−
apply (rule IDENTITY_QUOTIENT)+
−
apply (rule IDENTITY_QUOTIENT)+
−
apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})+
−
apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})+
−
apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})+
−
apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})+
−
apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})+
−
apply (tactic {* (APPLY_RSP_TAC rty @{context}) 1 *})+
−
apply (rule IDENTITY_QUOTIENT)+
−
apply (rule IDENTITY_QUOTIENT)+
−
apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})+
−
apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})+
−
apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})+
−
apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})+
−
apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})+
−
apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})+
−
apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})+
−
apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})+
−
apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})+
−
apply (tactic {* (APPLY_RSP_TAC rty @{context}) 1 *})+
−
apply (rule IDENTITY_QUOTIENT)+
−
apply (rule FUN_QUOTIENT)+
−
apply (rule QUOTIENT_fset)+
−
apply (rule IDENTITY_QUOTIENT)+
−
apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})+
−
apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})+
−
apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})+
−
apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})+
−
apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})+
−
apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})+
−
apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})+
−
apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})+
−
apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})+
−
apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})+
−
apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})+
−
apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})+
−
apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})+
−
apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})+
−
apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})+
−
apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})+
−
apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})+
−
apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})+
−
apply (tactic {* instantiate_tac @{thm APPLY_RSP2} @{context} 1 *})+
−
apply (tactic {* (instantiate_tac @{thm REP_ABS_RSP(1)} @{context} THEN' (RANGE [quotient_tac [quot]])) 1 *})+
−
apply assumption+
−
apply (rule refl)+
−
apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})+
−
apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})+
−
apply (tactic {* instantiate_tac @{thm APPLY_RSP2} @{context} 1 *})+
−
apply (tactic {* instantiate_tac @{thm APPLY_RSP2} @{context} 1 *})+
−
apply (tactic {* (instantiate_tac @{thm REP_ABS_RSP(1)} @{context} THEN' (RANGE [quotient_tac [quot]])) 1 *})+
−
apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})+
−
apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})+
−
apply (tactic {* REPEAT_ALL_NEW (inj_repabs_tac_fset @{context}) 1 *})+
−
apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})+
−
apply (tactic {* instantiate_tac @{thm APPLY_RSP2} @{context} 1 *})+
−
apply (tactic {* (instantiate_tac @{thm REP_ABS_RSP(1)} @{context} THEN' (RANGE [quotient_tac [quot]])) 1 *})+
−
apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})+
−
apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})+
−
apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})+
−
apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})+
−
apply (tactic {* clean_tac @{context} [quot] defs [(@{typ "('a list \<Rightarrow> 'c list \<Rightarrow> bool)"},@{typ "('a list \<Rightarrow> 'c fset \<Rightarrow> bool)"})] 1 *})+
−
done+
−
+
−
end+
−