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"

  apply (induct xs)

   apply (auto intro: list_eq.intros)

  done

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"

ML {* @{term "Abs_fset"} *}

local_setup {*

  old_make_const_def @{binding EMPTY} @{term "[]"} NoSyn @{typ "'a list"} @{typ "'a fset"} #> snd

*}

term Nil

term EMPTY

thm EMPTY_def

local_setup {*

  old_make_const_def @{binding INSERT} @{term "op #"} NoSyn @{typ "'a list"} @{typ "'a fset"} #> snd

*}

term Cons

term INSERT

thm INSERT_def

local_setup {*

  old_make_const_def @{binding UNION} @{term "op @"} NoSyn @{typ "'a list"} @{typ "'a fset"} #> snd

*}

term append

term UNION

thm UNION_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)))"

local_setup {*

  old_make_const_def @{binding card} @{term "card1"} NoSyn @{typ "'a list"} @{typ "'a fset"} #> snd

*}

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) \<Longrightarrow> card1 (x # xs) = Suc (card1 xs)"

  by simp

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

primrec

  fold1

where

  "fold1 f (g :: 'a \<Rightarrow> 'b) (z :: 'b) [] = z"

| "fold1 f g z (a # A) =

     (if ((!u v. (f u v = f v u))

      \<and> (!u v w. ((f u (f v w) = f (f u v) w))))

     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

local_setup {*

  old_make_const_def @{binding IN} @{term "membship"} NoSyn @{typ "'a list"} @{typ "'a fset"} #> snd

*}

term membship

term IN

thm IN_def

local_setup {*

  old_make_const_def @{binding fold} @{term "fold1::('b \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a list \<Rightarrow> 'b"} NoSyn @{typ "'a list"} @{typ "'a fset"} #> snd

*}

term fold1

term fold

thm fold_def

quotient_def (for "'a fset")

  fmap::"('a \<Rightarrow> 'a) \<Rightarrow> 'a fset \<Rightarrow> 'a fset"

where

  "fmap \<equiv> (map::('a \<Rightarrow> 'a) \<Rightarrow> 'a list \<Rightarrow> 'a list)"

term map

term fmap

thm fmap_def

lemma memb_rsp:

  fixes z

  assumes a: "list_eq x y"

  shows "(z memb x) = (z memb y)"

  using a by induct auto

lemma ho_memb_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)

  by (simp add: card1_rsp)

lemma cons_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:

  by (simp add: cons_rsp)

lemma append_rsp_fst:

  assumes a : "list_eq l1 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 : "list_eq l1 r1"

  assumes b : "list_eq l2 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:

  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 fun_rel_id:

  apply (rule eq_reflection)

  apply (rule ext)

  apply (rule ext)

  apply (simp)

  apply (auto)

  apply (rule ext)

  apply (simp)

  done

lemma ho_map_rsp:

  by (simp add: fun_rel_id map_rsp)

lemma map_append :

  "(map f ((a::'a list) @ b)) \<approx>

  ((map f a) ::'a list) @ (map f b)"

 by simp (rule list_eq_refl)

ML {* val rty = @{typ "'a list"} *}

ML {* val qty = @{typ "'a fset"} *}

ML {* val rel = @{term "list_eq"} *}

ML {* val rel_eqv = (#equiv_thm o hd) (quotdata_lookup @{context}) *}

ML {* val rel_refl = @{thm list_eq_refl} *}

ML {* val quot = @{thm QUOTIENT_fset} *}

ML {* val rsp_thms =

  @{thms ho_memb_rsp ho_cons_rsp ho_card1_rsp ho_map_rsp ho_append_rsp}

  @ @{thms ho_all_prs ho_ex_prs} *}

ML {* val trans2 = @{thm QUOT_TYPE_I_fset.R_trans2} *}

ML {* val reps_same = @{thm QUOT_TYPE_I_fset.REPS_same} *}

ML {* val defs = @{thms EMPTY_def IN_def UNION_def card_def INSERT_def fmap_def fold_def} *}

(* ML {* val consts = map (fst o dest_Const o fst o Logic.dest_equals o concl_of) fset_defs *} *)

ML {*

  val consts = [@{const_name "Nil"}, @{const_name "Cons"},

                @{const_name "membship"}, @{const_name "card1"},

                @{const_name "append"}, @{const_name "fold1"},

                @{const_name "map"}];

*}

ML {* fun lift_thm_fset lthy t =

  lift_thm lthy consts rty qty rel rel_eqv rel_refl quot rsp_thms trans2 reps_same defs t

*}

lemma eq_r: "a = b \<Longrightarrow> a \<approx> b"

by (simp add: list_eq_refl)

ML {* lift_thm_fset @{context} @{thm m1} *}

ML {* lift_thm_fset @{context} @{thm m2} *}

ML {* lift_thm_fset @{context} @{thm list_eq.intros(4)} *}

ML {* lift_thm_fset @{context} @{thm list_eq.intros(5)} *}

ML {* lift_thm_fset @{context} @{thm card1_suc} *}

ML {* lift_thm_fset @{context} @{thm map_append} *}

ML {* lift_thm_fset @{context} @{thm eq_r[OF append_assoc]} *}

thm fold1.simps(2)

thm list.recs(2)

ML {* val ind_r_a = atomize_thm @{thm list.induct} *}

(*  prove {* build_regularize_goal ind_r_a @{typ "'a List.list"} @{term "op \<approx>"} @{context} *}

  ML_prf {*  fun tac ctxt =

       (asm_full_simp_tac ((Simplifier.context ctxt HOL_ss) addsimps

        [(@{thm equiv_res_forall} OF [@{thm equiv_list_eq}]),

         (@{thm equiv_res_exists} OF [@{thm equiv_list_eq}])])) THEN_ALL_NEW

         (((rtac @{thm RIGHT_RES_FORALL_REGULAR}) THEN' (RANGE [fn _ => all_tac, atac]) THEN'

         (MetisTools.metis_tac ctxt [])) ORELSE' (MetisTools.metis_tac ctxt [])); *}

  apply (tactic {* tac @{context} 1 *}) *)

ML {* val ind_r_r = regularize ind_r_a @{typ "'a List.list"} @{term "op \<approx>"} @{thm equiv_list_eq} @{context} *}

ML {*

  val rt = build_repabs_term @{context} ind_r_r consts @{typ "'a list"} @{typ "'a fset"}

  val rg = Logic.mk_equals ((Thm.prop_of ind_r_r), rt);

*}

(*prove rg

apply(atomize(full))

apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *})

done*)

ML {* val ind_r_t =

  Toplevel.program (fn () =>

  repabs @{context} ind_r_r consts @{typ "'a list"} @{typ "'a fset"}

   @{thm QUOTIENT_fset} @{thm list_eq_refl} @{thm QUOT_TYPE_I_fset.R_trans2}

   (@{thms ho_memb_rsp ho_cons_rsp ho_card1_rsp ho_map_rsp ho_append_rsp} @ @{thms ho_all_prs ho_ex_prs})

  )

*}

ML {* val abs = findabs rty (prop_of (atomize_thm @{thm list.induct})) *}

ML {* val simp_lam_prs_thms = map (make_simp_lam_prs_thm @{context} quot) abs *}

ML {* val ind_r_l = repeat_eqsubst_thm @{context} simp_lam_prs_thms ind_r_t *}

lemma app_prs_for_induct: "(ABS_fset ---> id) f (REP_fset T1) = f T1"

  apply (simp add: fun_map.simps QUOT_TYPE_I_fset.thm10)

done

ML {* val ind_r_l1 = eqsubst_thm @{context} @{thms app_prs_for_induct} ind_r_l *}

ML {* val ind_r_l2 = eqsubst_thm @{context} @{thms app_prs_for_induct} ind_r_l1 *}

ML {* val ind_r_l3 = eqsubst_thm @{context} @{thms app_prs_for_induct} ind_r_l2 *}

ML {* val ind_r_l4 = eqsubst_thm @{context} @{thms app_prs_for_induct} ind_r_l3 *}

ML {* val ind_r_a = simp_allex_prs @{context} quot ind_r_l4 *}

ML {* val thm = @{thm FORALL_PRS[OF FUN_QUOTIENT[OF QUOTIENT_fset IDENTITY_QUOTIENT], symmetric]} *}

ML {* val ind_r_a1 = eqsubst_thm @{context} [thm] ind_r_a *}

ML {* val defs_sym = add_lower_defs @{context} defs *}

ML {* val ind_r_d = repeat_eqsubst_thm @{context} defs_sym ind_r_a1 *}

ML {* val ind_r_s = MetaSimplifier.rewrite_rule @{thms QUOT_TYPE_I_fset.REPS_same} ind_r_d *}

ML {* ObjectLogic.rulify ind_r_s *}

ML {*

  fun lift_thm_fset_note name thm lthy =

    let

      val lifted_thm = lift_thm_fset lthy thm;

      val (_, lthy2) = note (name, lifted_thm) lthy;

    in

      lthy2

    end;

*}

local_setup {*

  lift_thm_fset_note @{binding "m1l"} @{thm m1} #>

  lift_thm_fset_note @{binding "m2l"} @{thm m2} #>

  lift_thm_fset_note @{binding "leqi4l"} @{thm list_eq.intros(4)} #>

  lift_thm_fset_note @{binding "leqi5l"} @{thm list_eq.intros(5)}

*}

thm m1l

thm m2l

thm leqi4l

thm leqi5l

end