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 {*

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

*}

term Nil

term EMPTY

thm EMPTY_def

local_setup {*

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

*}

term Cons

term INSERT

thm INSERT_def

local_setup {*

  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 {*

  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 = [])"

  apply (induct a)

   apply (simp)

  apply (simp_all)

   apply meson

  apply (simp_all)

  done

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

  apply (induct xs)

  apply (auto intro: list_eq.intros)

  done

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 {*

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

*}

term membship

term IN

thm IN_def

ML {*

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

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

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

*}

ML {* val fset_defs = @{thms EMPTY_def IN_def UNION_def card_def INSERT_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)"

  apply (simp add: FUN_REL.simps)

  apply (metis memb_rsp)

  done

lemma card1_rsp:

  fixes a b :: "'a list"

  assumes e: "a \<approx> b"

  shows "card1 a = card1 b"

  using e apply induct

  apply (simp_all add:memb_rsp)

  done

lemma ho_card1_rsp: "op \<approx> ===> op = card1 card1"

  apply (simp add: FUN_REL.simps)

  apply (metis card1_rsp)

  done

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:

  "op = ===> op \<approx> ===> op \<approx> op # op #"

  apply (simp add: FUN_REL.simps)

  apply (metis cons_rsp)

  done

lemma append_rsp_fst:

  assumes a : "list_eq l1 l2"

  shows "list_eq (l1 @ s) (l2 @ s)"

  using a

  apply(induct)

  apply(auto intro: list_eq.intros)

  apply(rule list_eq_refl)

done

(* Need stronger induction... *)

lemma "(a @ b) \<approx> (b @ a)"

  apply(induct a)

  sorry

lemma (* ho_append_rsp: *)

  "op \<approx> ===> op \<approx> ===> op \<approx> op @ op @"

sorry

thm list.induct

lemma list_induct_hol4:

  fixes P :: "'a list \<Rightarrow> bool"

  assumes a: "((P []) \<and> (\<forall>t. (P t) \<longrightarrow> (\<forall>h. (P (h # t)))))"

  shows "\<forall>l. (P l)"

  using a

  apply (rule_tac allI)

  apply (induct_tac "l")

  apply (simp)

  apply (metis)

  done

prove list_induct_r: {*

   build_regularize_goal (atomize_thm @{thm list_induct_hol4}) @{typ "'a List.list"} @{term "op \<approx>"} @{context} *}

  apply (simp only: equiv_res_forall[OF equiv_list_eq])

  thm RIGHT_RES_FORALL_REGULAR

  apply (rule RIGHT_RES_FORALL_REGULAR)

  prefer 2

  apply (assumption)

  apply (metis)

  done

(* The all_prs and ex_prs should be proved for the instance... *)

ML {*

fun r_mk_comb_tac_fset ctxt =

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

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

*}

ML {* val thm = @{thm list_induct_r} OF [atomize_thm @{thm list_induct_hol4}] *}

ML {* val trm_r = build_repabs_goal @{context} thm consts @{typ "'a list"} @{typ "'a fset"} *}

ML {* val trm = build_repabs_term @{context} thm consts @{typ "'a list"} @{typ "'a fset"} *}

ML {* trm_r *}

prove list_induct_tr: trm_r

apply (atomize(full))

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

done

prove list_induct_t: trm

apply (simp only: list_induct_tr[symmetric])

apply (tactic {* rtac thm 1 *})

done

thm m2

ML {* atomize_thm @{thm m2} *}

prove m2_r_p: {*

   build_regularize_goal (atomize_thm @{thm m2}) @{typ "'a List.list"} @{term "op \<approx>"} @{context} *}

  apply (simp add: equiv_res_forall[OF equiv_list_eq])

done

ML {* val m2_r = @{thm m2_r_p} OF [atomize_thm @{thm m2}] *}

ML {* val m2_t_g = build_repabs_goal @{context} m2_r consts @{typ "'a list"} @{typ "'a fset"} *}

ML {* val m2_t = build_repabs_term @{context} m2_r consts @{typ "'a list"} @{typ "'a fset"} *}

prove m2_t_p: m2_t_g

apply (atomize(full))

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

done

prove m2_t: m2_t

apply (simp only: m2_t_p[symmetric])

apply (tactic {* rtac m2_r 1 *})

done

lemma id_apply2 [simp]: "id x \<equiv> x"

  by (simp add: id_def)

ML {*

   val lpis = @{thm LAMBDA_PRS} OF [@{thm QUOTIENT_fset}, @{thm IDENTITY_QUOTIENT}];

   val lpist = @{thm "HOL.sym"} OF [lpis];

   val lam_prs = MetaSimplifier.rewrite_rule [@{thm id_apply2}] lpist

*}

text {* the proper way to do it *}

ML {*

  fun findabs rty tm =

    case tm of

      Abs(_, T, b) =>

        let

          val b' = subst_bound ((Free ("x", T)), b);

          val tys = findabs rty b'

          val ty = fastype_of tm

        in if needs_lift rty ty then (ty :: tys) else tys

        end

    | f $ a => (findabs rty f) @ (findabs rty a)

    | _ => []

*}

ML {* findabs @{typ "'a list"} (prop_of (atomize_thm @{thm list_induct_hol4})) *}

ML {*

 val lpi = Drule.instantiate'

   [SOME @{ctyp "'a list"}, NONE, SOME @{ctyp "bool"}, NONE] [] @{thm LAMBDA_PRS};

*}

prove lambda_prs_l_b : {* concl_of lpi *}

apply (tactic {* compose_tac (false, @{thm LAMBDA_PRS}, 2) 1 *})

apply (tactic {* quotient_tac @{thm QUOTIENT_fset} 1 *})

apply (tactic {* quotient_tac @{thm QUOTIENT_fset} 1 *})

done

thm HOL.sym[OF lambda_prs_l_b,simplified]

ML {*

 val lpi = Drule.instantiate'

   [SOME @{ctyp "'a list \<Rightarrow> bool"}, NONE, SOME @{ctyp "bool"}, NONE] [] @{thm LAMBDA_PRS};

*}

prove lambda_prs_lb_b : {* concl_of lpi *}

apply (tactic {* compose_tac (false, @{thm LAMBDA_PRS}, 2) 1 *})

apply (tactic {* quotient_tac @{thm QUOTIENT_fset} 1 *})

apply (tactic {* quotient_tac @{thm QUOTIENT_fset} 1 *})

done

thm HOL.sym[OF lambda_prs_lb_b,simplified]

ML {*

  fun simp_lam_prs lthy thm =

    simp_lam_prs lthy (eqsubst_thm lthy

      @{thms HOL.sym[OF lambda_prs_lb_b,simplified] HOL.sym[OF lambda_prs_l_b,simplified]}

    thm)

    handle _ => thm

*}

ML {* val m2_t' = eqsubst_thm @{context} [lam_prs] @{thm m2_t} *}

ML {*

  fun simp_allex_prs lthy thm =

    let

      val rwf = @{thm FORALL_PRS[OF QUOTIENT_fset]};

      val rwfs = @{thm "HOL.sym"} OF [rwf];

      val rwe = @{thm EXISTS_PRS[OF QUOTIENT_fset]};

      val rwes = @{thm "HOL.sym"} OF [rwe]

    in

      (simp_allex_prs lthy (eqsubst_thm lthy [rwfs, rwes] thm))

    end

    handle _ => thm

*}

ML {* val ithm = simp_allex_prs @{context} m2_t' *}

ML fset_defs_sym

ML {* val rthm = MetaSimplifier.rewrite_rule fset_defs_sym ithm *}

ML {* ObjectLogic.rulify rthm *}

prove card1_suc_r_p: {*

   build_regularize_goal (atomize_thm @{thm card1_suc}) @{typ "'a List.list"} @{term "op \<approx>"} @{context} *}

  apply (simp add: equiv_res_forall[OF equiv_list_eq] equiv_res_exists[OF equiv_list_eq])

done

ML {* val card1_suc_r = @{thm card1_suc_r_p} OF [atomize_thm @{thm card1_suc}] *}

ML {* val card1_suc_t_g = build_repabs_goal @{context} card1_suc_r consts @{typ "'a list"} @{typ "'a fset"} *}

ML {* val card1_suc_t = build_repabs_term @{context} card1_suc_r consts @{typ "'a list"} @{typ "'a fset"} *}

prove card1_suc_t_p: card1_suc_t_g

apply (atomize(full))

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

done

prove card1_suc_t: card1_suc_t

apply (simp only: card1_suc_t_p[symmetric])

apply (tactic {* rtac card1_suc_r 1 *})

done

ML {* val card1_suc_t_n = @{thm card1_suc_t} *}

ML {* val card1_suc_t' = eqsubst_thm @{context} @{thms HOL.sym[OF lambda_prs_l_b,simplified]} @{thm card1_suc_t} *}

ML {* val card1_suc_t'' = eqsubst_thm @{context} @{thms HOL.sym[OF lambda_prs_l_b,simplified]} card1_suc_t' *}

ML {* val ithm = simp_allex_prs @{context} card1_suc_t'' *}

ML {* val rthm = MetaSimplifier.rewrite_rule fset_defs_sym ithm *}

ML {* val qthm = MetaSimplifier.rewrite_rule @{thms QUOT_TYPE_I_fset.REPS_same} rthm *}

ML {* ObjectLogic.rulify qthm *}

thm fold1.simps(2)

thm list.recs(2)

ML {* val ind_r_a = atomize_thm @{thm list_induct_hol4} *}

(*  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 *})*)

ML {* val (g, thm, othm) =

  Toplevel.program (fn () =>

  repabs_eq @{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} @ @{thms ho_all_prs ho_ex_prs})

  )

*}

ML {*

    fun tac2 ctxt =

     (simp_tac ((Simplifier.context ctxt empty_ss) addsimps [symmetric thm]))

     THEN' (rtac othm); *}

(* ML {*    val cthm = Goal.prove @{context} [] [] g (fn x => tac2 (#context x) 1);

*} *)

ML {*

  val ind_r_t2 =

  Toplevel.program (fn () =>

    repabs_eq2 @{context} (g, thm, othm)

  )

*}

ML {* val ind_r_l = simp_lam_prs @{context} ind_r_t2 *}

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} 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 {* hd fset_defs_sym *}

ML {* val ind_r_d = MetaSimplifier.rewrite_rule fset_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 =

let

  val ind_r_a = atomize_thm thm;

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

  val (g, t, ot) =

    repabs_eq @{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} @ @{thms ho_all_prs ho_ex_prs});

  val ind_r_t = repabs_eq2 @{context} (g, t, ot);

  val ind_r_l = simp_lam_prs @{context} ind_r_t;

  val ind_r_a = simp_allex_prs @{context} ind_r_l;

  val ind_r_d = MetaSimplifier.rewrite_rule fset_defs_sym ind_r_a;

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

in

  ObjectLogic.rulify ind_r_s

end

*}

ML fset_defs

ML {* lift @{thm m2} *}

ML {* lift @{thm m1} *}

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

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

ML {* lift @{thm card1_suc} *}

(* ML {* lift @{thm append_assoc} *} *)

(*notation ( output) "prop" ("#_" [1000] 1000) *)

notation ( output) "Trueprop" ("#_" [1000] 1000)

(*

ML {*

  fun lift_theorem_fset_aux thm lthy =

    let

      val ((_, [novars]), lthy2) = Variable.import true [thm] lthy;

      val goal = build_repabs_goal @{context} novars consts @{typ "'a list"} @{typ "'a fset"};

      val cgoal = cterm_of @{theory} goal;

      val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite true fset_defs_sym cgoal);

      val tac = transconv_fset_tac' @{context};

      val cthm = Goal.prove_internal [] cgoal2 (fn _ => tac);

      val nthm = MetaSimplifier.rewrite_rule [symmetric cthm] (snd (no_vars (Context.Theory @{theory}, thm)))

      val nthm2 = MetaSimplifier.rewrite_rule @{thms QUOT_TYPE_I_fset.REPS_same QUOT_TYPE_I_fset.thm10} nthm;

      val [nthm3] = ProofContext.export lthy2 lthy [nthm2]

    in

      nthm3

    end

*}