Proper definition of CARD and some properties of it.
Translation should now support Pure assumptions and Trueprops anywhere,
but a problem needs to be fixed with the tactic.
theory QuotMainimports QuotScript QuotList Provebeginlocale QUOT_TYPE = fixes R :: "'a \<Rightarrow> 'a \<Rightarrow> bool" and Abs :: "('a \<Rightarrow> bool) \<Rightarrow> 'b" and Rep :: "'b \<Rightarrow> ('a \<Rightarrow> bool)" assumes equiv: "EQUIV R" and rep_prop: "\<And>y. \<exists>x. Rep y = R x" and rep_inverse: "\<And>x. Abs (Rep x) = x" and abs_inverse: "\<And>x. (Rep (Abs (R x))) = (R x)" and rep_inject: "\<And>x y. (Rep x = Rep y) = (x = y)"begindefinition "ABS x \<equiv> Abs (R x)"definition "REP a = Eps (Rep a)"lemma lem9: shows "R (Eps (R x)) = R x"proof - have a: "R x x" using equiv by (simp add: EQUIV_REFL_SYM_TRANS REFL_def) then have "R x (Eps (R x))" by (rule someI) then show "R (Eps (R x)) = R x" using equiv unfolding EQUIV_def by simpqedtheorem thm10: shows "ABS (REP a) \<equiv> a" apply (rule eq_reflection) unfolding ABS_def REP_defproof - from rep_prop obtain x where eq: "Rep a = R x" by auto have "Abs (R (Eps (Rep a))) = Abs (R (Eps (R x)))" using eq by simp also have "\<dots> = Abs (R x)" using lem9 by simp also have "\<dots> = Abs (Rep a)" using eq by simp also have "\<dots> = a" using rep_inverse by simp finally show "Abs (R (Eps (Rep a))) = a" by simpqedlemma REP_refl: shows "R (REP a) (REP a)"unfolding REP_defby (simp add: equiv[simplified EQUIV_def])lemma lem7: shows "(R x = R y) = (Abs (R x) = Abs (R y))"apply(rule iffI)apply(simp)apply(drule rep_inject[THEN iffD2])apply(simp add: abs_inverse)donetheorem thm11: shows "R r r' = (ABS r = ABS r')"unfolding ABS_defby (simp only: equiv[simplified EQUIV_def] lem7)lemma REP_ABS_rsp: shows "R f (REP (ABS g)) = R f g" and "R (REP (ABS g)) f = R g f"by (simp_all add: thm10 thm11)lemma QUOTIENT: "QUOTIENT R ABS REP"apply(unfold QUOTIENT_def)apply(simp add: thm10)apply(simp add: REP_refl)apply(subst thm11[symmetric])apply(simp add: equiv[simplified EQUIV_def])donelemma R_trans: assumes ab: "R a b" and bc: "R b c" shows "R a c"proof - have tr: "TRANS R" using equiv EQUIV_REFL_SYM_TRANS[of R] by simp moreover have ab: "R a b" by fact moreover have bc: "R b c" by fact ultimately show "R a c" unfolding TRANS_def by blastqedlemma R_sym: assumes ab: "R a b" shows "R b a"proof - have re: "SYM R" using equiv EQUIV_REFL_SYM_TRANS[of R] by simp then show "R b a" using ab unfolding SYM_def by blastqedlemma R_trans2: assumes ac: "R a c" and bd: "R b d" shows "R a b = R c d"proof assume "R a b" then have "R b a" using R_sym by blast then have "R b c" using ac R_trans by blast then have "R c b" using R_sym by blast then show "R c d" using bd R_trans by blastnext assume "R c d" then have "R a d" using ac R_trans by blast then have "R d a" using R_sym by blast then have "R b a" using bd R_trans by blast then show "R a b" using R_sym by blastqedlemma REPS_same: shows "R (REP a) (REP b) \<equiv> (a = b)" apply (rule eq_reflection)proof assume as: "R (REP a) (REP b)" from rep_prop obtain x y where eqs: "Rep a = R x" "Rep b = R y" by blast from eqs have "R (Eps (R x)) (Eps (R y))" using as unfolding REP_def by simp then have "R x (Eps (R y))" using lem9 by simp then have "R (Eps (R y)) x" using R_sym by blast then have "R y x" using lem9 by simp then have "R x y" using R_sym by blast then have "ABS x = ABS y" using thm11 by simp then have "Abs (Rep a) = Abs (Rep b)" using eqs unfolding ABS_def by simp then show "a = b" using rep_inverse by simpnext assume ab: "a = b" have "REFL R" using equiv EQUIV_REFL_SYM_TRANS[of R] by simp then show "R (REP a) (REP b)" unfolding REFL_def using ab by autoqedendsection {* type definition for the quotient type *}ML {*(* constructs the term \<lambda>(c::ty \<Rightarrow> bool). \<exists>x. c = rel x *)fun typedef_term rel ty lthy =let val [x, c] = [("x", ty), ("c", ty --> @{typ bool})] |> Variable.variant_frees lthy [rel] |> map Freein lambda c (HOLogic.mk_exists ("x", ty, HOLogic.mk_eq (c, (rel $ x))))end*}ML {*(* makes the new type definitions and proves non-emptyness*)fun typedef_make (qty_name, rel, ty) lthy =let val typedef_tac = EVERY1 [rewrite_goal_tac @{thms mem_def}, rtac @{thm exI}, rtac @{thm exI}, rtac @{thm refl}]in LocalTheory.theory_result (Typedef.add_typedef false NONE (qty_name, map fst (Term.add_tfreesT ty []), NoSyn) (typedef_term rel ty lthy) NONE typedef_tac) lthyend*}ML {*(* proves the QUOT_TYPE theorem for the new type *)fun typedef_quot_type_tac equiv_thm (typedef_info: Typedef.info) =let val rep_thm = #Rep typedef_info val rep_inv = #Rep_inverse typedef_info val abs_inv = #Abs_inverse typedef_info val rep_inj = #Rep_inject typedef_info val ss = HOL_basic_ss addsimps @{thms mem_def} val rep_thm_simpd = Simplifier.asm_full_simplify ss rep_thm val abs_inv_simpd = Simplifier.asm_full_simplify ss abs_invin EVERY1 [rtac @{thm QUOT_TYPE.intro}, rtac equiv_thm, rtac rep_thm_simpd, rtac rep_inv, rtac abs_inv_simpd, rtac @{thm exI}, rtac @{thm refl}, rtac rep_inj]endfun typedef_quot_type_thm (rel, abs, rep, equiv_thm, typedef_info) lthy =let val quot_type_const = Const (@{const_name "QUOT_TYPE"}, dummyT) val goal = HOLogic.mk_Trueprop (quot_type_const $ rel $ abs $ rep) |> Syntax.check_term lthyin Goal.prove lthy [] [] goal (K (typedef_quot_type_tac equiv_thm typedef_info))end*}ML {*fun typedef_quotient_thm (rel, abs, rep, abs_def, rep_def, quot_type_thm) lthy =let val quotient_const = Const (@{const_name "QUOTIENT"}, dummyT) val goal = HOLogic.mk_Trueprop (quotient_const $ rel $ abs $ rep) |> Syntax.check_term lthy val typedef_quotient_thm_tac = EVERY1 [K (rewrite_goals_tac [abs_def, rep_def]), rtac @{thm QUOT_TYPE.QUOTIENT}, rtac quot_type_thm]in Goal.prove lthy [] [] goal (K typedef_quotient_thm_tac)end*}text {* two wrappers for define and note *}ML {*fun make_def (name, mx, rhs) lthy =let val ((rhs, (_ , thm)), lthy') = LocalTheory.define Thm.internalK ((name, mx), (Attrib.empty_binding, rhs)) lthyin ((rhs, thm), lthy')end*}ML {*fun note_thm (name, thm) lthy =let val ((_,[thm']), lthy') = LocalTheory.note Thm.theoremK ((name, []), [thm]) lthyin (thm', lthy')end*}ML {*val no_vars = Thm.rule_attribute (fn context => fn th => let val ctxt = Variable.set_body false (Context.proof_of context); val ((_, [th']), _) = Variable.import true [th] ctxt; in th' end);*}ML {*fun typedef_main (qty_name, rel, ty, equiv_thm) lthy =let (* generates typedef *) val ((_, typedef_info), lthy1) = typedef_make (qty_name, rel, ty) lthy (* abs and rep functions *) val abs_ty = #abs_type typedef_info val rep_ty = #rep_type typedef_info val abs_name = #Abs_name typedef_info val rep_name = #Rep_name typedef_info val abs = Const (abs_name, rep_ty --> abs_ty) val rep = Const (rep_name, abs_ty --> rep_ty) (* ABS and REP definitions *) val ABS_const = Const (@{const_name "QUOT_TYPE.ABS"}, dummyT ) val REP_const = Const (@{const_name "QUOT_TYPE.REP"}, dummyT ) val ABS_trm = Syntax.check_term lthy1 (ABS_const $ rel $ abs) val REP_trm = Syntax.check_term lthy1 (REP_const $ rep) val ABS_name = Binding.prefix_name "ABS_" qty_name val REP_name = Binding.prefix_name "REP_" qty_name val (((ABS, ABS_def), (REP, REP_def)), lthy2) = lthy1 |> make_def (ABS_name, NoSyn, ABS_trm) ||>> make_def (REP_name, NoSyn, REP_trm) (* quot_type theorem *) val quot_thm = typedef_quot_type_thm (rel, abs, rep, equiv_thm, typedef_info) lthy2 val quot_thm_name = Binding.prefix_name "QUOT_TYPE_" qty_name (* quotient theorem *) val quotient_thm = typedef_quotient_thm (rel, ABS, REP, ABS_def, REP_def, quot_thm) lthy2 val quotient_thm_name = Binding.prefix_name "QUOTIENT_" qty_name (* interpretation *) val bindd = ((Binding.make ("", Position.none)), ([]: Attrib.src list)) val ((_, [eqn1pre]), lthy3) = Variable.import true [ABS_def] lthy2; val eqn1i = Thm.prop_of (symmetric eqn1pre) val ((_, [eqn2pre]), lthy4) = Variable.import true [REP_def] lthy3; val eqn2i = Thm.prop_of (symmetric eqn2pre) val exp_morphism = ProofContext.export_morphism lthy4 (ProofContext.init (ProofContext.theory_of lthy4)); val exp_term = Morphism.term exp_morphism; val exp = Morphism.thm exp_morphism; val mthd = Method.SIMPLE_METHOD ((rtac quot_thm 1) THEN ALLGOALS (simp_tac (HOL_basic_ss addsimps [(symmetric (exp ABS_def)), (symmetric (exp REP_def))]))) val mthdt = Method.Basic (fn _ => mthd) val bymt = Proof.global_terminal_proof (mthdt, NONE) val exp_i = [(@{const_name QUOT_TYPE}, ((("QUOT_TYPE_I_" ^ (Binding.name_of qty_name)), true), Expression.Named [ ("R", rel), ("Abs", abs), ("Rep", rep) ]))]in lthy4 |> note_thm (quot_thm_name, quot_thm) ||>> note_thm (quotient_thm_name, quotient_thm) ||> LocalTheory.theory (fn thy => let val global_eqns = map exp_term [eqn2i, eqn1i]; (* Not sure if the following context should not be used *) val (global_eqns2, lthy5) = Variable.import_terms true global_eqns lthy4; val global_eqns3 = map (fn t => (bindd, t)) global_eqns2; in ProofContext.theory_of (bymt (Expression.interpretation (exp_i, []) global_eqns3 thy)) end)end*}section {* various tests for quotient types*}datatype trm = var "nat"| app "trm" "trm"| lam "nat" "trm"axiomatization RR :: "trm \<Rightarrow> trm \<Rightarrow> bool" where r_eq: "EQUIV RR"local_setup {* typedef_main (@{binding "qtrm"}, @{term "RR"}, @{typ trm}, @{thm r_eq}) #> snd*}term Rep_qtrmterm REP_qtrmterm Abs_qtrmterm ABS_qtrmthm QUOT_TYPE_qtrmthm QUOTIENT_qtrm(* Test interpretation *)thm QUOT_TYPE_I_qtrm.thm11thm QUOT_TYPE.thm11print_theoremsthm Rep_qtrmtext {* another test *}datatype 'a trm' = var' "'a"| app' "'a trm'" "'a trm'"| lam' "'a" "'a trm'"consts R' :: "'a trm' \<Rightarrow> 'a trm' \<Rightarrow> bool"axioms r_eq': "EQUIV R'"local_setup {* typedef_main (@{binding "qtrm'"}, @{term "R'"}, @{typ "'a trm'"}, @{thm r_eq'}) #> snd*}print_theoremsterm ABS_qtrm'term REP_qtrm'thm QUOT_TYPE_qtrm'thm QUOTIENT_qtrm'thm Rep_qtrm'text {* a test with lists of terms *}datatype t = vr "string"| ap "t list"| lm "string" "t"consts Rt :: "t \<Rightarrow> t \<Rightarrow> bool"axioms t_eq: "EQUIV Rt"local_setup {* typedef_main (@{binding "qt"}, @{term "Rt"}, @{typ "t"}, @{thm t_eq}) #> snd*}section {* lifting of constants *}text {* information about map-functions for type-constructor *}ML {*type typ_info = {mapfun: string}local structure Data = GenericDataFun (type T = typ_info Symtab.table val empty = Symtab.empty val extend = I fun merge _ = Symtab.merge (K true))in val lookup = Symtab.lookup o Data.get fun update k v = Data.map (Symtab.update (k, v))end*}(* mapfuns for some standard types *)setup {* Context.theory_map (update @{type_name "list"} {mapfun = @{const_name "map"}}) #> Context.theory_map (update @{type_name "*"} {mapfun = @{const_name "prod_fun"}}) #> Context.theory_map (update @{type_name "fun"} {mapfun = @{const_name "fun_map"}})*}ML {* lookup (Context.Proof @{context}) @{type_name list} *}ML {*datatype abs_or_rep = abs | repfun get_fun abs_or_rep rty qty lthy ty =let val qty_name = Long_Name.base_name (fst (dest_Type qty)) fun get_fun_aux s fs_tys = let val (fs, tys) = split_list fs_tys val (otys, ntys) = split_list tys val oty = Type (s, otys) val nty = Type (s, ntys) val ftys = map (op -->) tys in (case (lookup (Context.Proof lthy) s) of SOME info => (list_comb (Const (#mapfun info, ftys ---> oty --> nty), fs), (oty, nty)) | NONE => raise ERROR ("no map association for type " ^ s)) end fun get_const abs = (Const ("QuotMain.ABS_" ^ qty_name, rty --> qty), (rty, qty)) | get_const rep = (Const ("QuotMain.REP_" ^ qty_name, qty --> rty), (qty, rty))in if ty = qty then (get_const abs_or_rep) else (case ty of TFree _ => (Abs ("x", ty, Bound 0), (ty, ty)) | Type (_, []) => (Abs ("x", ty, Bound 0), (ty, ty)) | Type (s, tys) => get_fun_aux s (map (get_fun abs_or_rep rty qty lthy) tys) | _ => raise ERROR ("no variables") )end*}ML {* get_fun rep @{typ t} @{typ qt} @{context} @{typ "t * nat"} |> fst |> Syntax.string_of_term @{context} |> writeln*}ML {*fun get_const_def nconst oconst rty qty lthy =let val ty = fastype_of nconst val (arg_tys, res_ty) = strip_type ty val fresh_args = arg_tys |> map (pair "x") |> Variable.variant_frees lthy [nconst, oconst] |> map Free val rep_fns = map (fst o get_fun rep rty qty lthy) arg_tys val abs_fn = (fst o get_fun abs rty qty lthy) res_tyin map (op $) (rep_fns ~~ fresh_args) |> curry list_comb oconst |> curry (op $) abs_fn |> fold_rev lambda fresh_argsend*}ML {*fun exchange_ty rty qty ty = if ty = rty then qty else (case ty of Type (s, tys) => Type (s, map (exchange_ty rty qty) tys) | _ => ty)*}ML {*fun make_const_def nconst_bname oconst mx rty qty lthy =let val oconst_ty = fastype_of oconst val nconst_ty = exchange_ty rty qty oconst_ty val nconst = Const (Binding.name_of nconst_bname, nconst_ty) val def_trm = get_const_def nconst oconst rty qty lthyin make_def (nconst_bname, mx, def_trm) lthyend*}local_setup {* make_const_def @{binding VR} @{term "vr"} NoSyn @{typ "t"} @{typ "qt"} #> snd*}local_setup {* make_const_def @{binding AP} @{term "ap"} NoSyn @{typ "t"} @{typ "qt"} #> snd*}local_setup {* make_const_def @{binding LM} @{term "lm"} NoSyn @{typ "t"} @{typ "qt"} #> snd*}thm VR_defthm AP_defthm LM_defterm LMterm VRterm APtext {* a test with functions *}datatype 'a t' = vr' "string"| ap' "('a t') * ('a t')"| lm' "'a" "string \<Rightarrow> ('a t')"consts Rt' :: "('a t') \<Rightarrow> ('a t') \<Rightarrow> bool"axioms t_eq': "EQUIV Rt'"local_setup {* typedef_main (@{binding "qt'"}, @{term "Rt'"}, @{typ "'a t'"}, @{thm t_eq'}) #> snd*}print_theoremslocal_setup {* make_const_def @{binding VR'} @{term "vr'"} NoSyn @{typ "'a t'"} @{typ "'a qt'"} #> snd*}local_setup {* make_const_def @{binding AP'} @{term "ap'"} NoSyn @{typ "'a t'"} @{typ "'a qt'"} #> snd*}local_setup {* make_const_def @{binding LM'} @{term "lm'"} NoSyn @{typ "'a t'"} @{typ "'a qt'"} #> snd*}thm VR'_defthm AP'_defthm LM'_defterm LM'term VR'term AP'text {* finite set example *}print_syntaxinductive 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_sym: shows "xs \<approx> xs" apply (induct xs) apply (auto intro: list_eq.intros) donelemma 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_sym) donelocal_setup {* typedef_main (@{binding "fset"}, @{term "list_eq"}, @{typ "'a list"}, @{thm "equiv_list_eq"}) #> snd*}print_theoremstyp "'a fset"thm "Rep_fset"local_setup {* make_const_def @{binding EMPTY} @{term "[]"} NoSyn @{typ "'a list"} @{typ "'a fset"} #> snd*}term Nilterm EMPTYthm EMPTY_deflocal_setup {* make_const_def @{binding INSERT} @{term "op #"} NoSyn @{typ "'a list"} @{typ "'a fset"} #> snd*}term Consterm INSERTthm INSERT_deflocal_setup {* make_const_def @{binding UNION} @{term "op @"} NoSyn @{typ "'a list"} @{typ "'a fset"} #> snd*}term appendterm UNIONthm UNION_defthm QUOTIENT_fsetthm QUOT_TYPE_I_fset.thm11fun 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))"lemma mem_respects: fixes z assumes a: "list_eq x y" shows "(z memb x) = (z memb y)" using a by induct autofun 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 card1term cardthm 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_rsp: fixes a b :: "'a list" assumes e: "a \<approx> b" shows "card1 a = card1 b" using e apply induct apply (simp_all add:mem_respects) donelemma card1_0: fixes a :: "'a list" shows "(card1 a = 0) = (a = [])" apply (induct a) apply (simp) apply (simp_all) apply meson apply (simp_all) donelemma not_mem_card1: fixes x :: "'a" fixes xs :: "'a list" shows "~(x memb xs) \<Longrightarrow> card1 (x # xs) = Suc (card1 xs)" by simplemma 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 (simp_all) apply (meson) apply (simp_all add: list_eq.intros(4)) proof - fix a :: "'a" fix xs :: "'a list" assume a1 : "x # xs \<approx> xs" assume a2 : "x memb xs" have a3 : "x # a # xs \<approx> a # x # xs" using list_eq.intros(1)[of "x"] by blast have a4 : "a # x # xs \<approx> a # xs" using a1 list_eq.intros(5)[of "x # xs" "xs"] by simp then show "x # a # xs \<approx> a # xs" using a3 list_eq.intros(6) by blast qedlemma 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 (simp)(* apply (rule allI)*) proof - fix a :: "'a" fix xs :: "'a list" fix n :: "nat" assume a1: "card1 xs = Suc n \<Longrightarrow> \<exists>a ys. \<not> a memb ys \<and> xs \<approx> a # ys" assume a2: "card1 (a # xs) = Suc n" from a1 a2 show "\<exists>aa ys. \<not> aa memb ys \<and> a # xs \<approx> aa # ys" apply - apply (rule True_or_False [of "a memb xs", THEN disjE]) apply (simp_all add: card1_cons if_True simp_thms) proof - assume a1: "\<exists>a ys. \<not> a memb ys \<and> xs \<approx> a # ys" assume a2: "card1 xs = Suc n" assume a3: "a memb xs" from a1 obtain b ys where a5: "\<not> b memb ys \<and> xs \<approx> b # ys" by blast from a2 a3 a5 show "\<exists>aa ys. \<not> aa memb ys \<and> a # xs \<approx> aa # ys" apply - apply (rule_tac x = "b" in exI) apply (rule_tac x = "ys" in exI) apply (simp_all) proof - assume a1: "a memb xs" assume a2: "\<not> b memb ys \<and> xs \<approx> b # ys" then have a3: "xs \<approx> b # ys" by simp have "a # xs \<approx> xs" using a1 mem_cons[of "a" "xs"] by simp then show "a # xs \<approx> b # ys" using a3 list_eq.intros(6) by blast qednext assume a2: "\<not> a memb xs" from a2 show "\<exists>aa ys. \<not> aa memb ys \<and> a # xs \<approx> aa # ys" apply - apply (rule_tac x = "a" in exI) apply (rule_tac x = "xs" in exI) apply (simp) apply (rule list_eq_sym) done qedqedlemma cons_preserves: fixes z assumes a: "xs \<approx> ys" shows "(z # xs) \<approx> (z # ys)" using a by (rule QuotMain.list_eq.intros(5))text {* unlam_def converts a definition theorem given as 'a = \lambda x. \lambda y. f (x y)' to a theorem 'a x y = f (x, y)'. These are needed to rewrite right-to-left.*}ML {*fun unlam_def_aux orig_ctxt ctxt t = let val rhs = Thm.rhs_of t in (case try (Thm.dest_abs NONE) rhs of SOME (v, vt) => let val (vname, vt) = Term.dest_Free (Thm.term_of v) val ([vnname], ctxt) = Variable.variant_fixes [vname] ctxt val nv = Free(vnname, vt) val t2 = Drule.fun_cong_rule t (Thm.cterm_of (ProofContext.theory_of ctxt) nv) val tnorm = equal_elim (Drule.beta_eta_conversion (Thm.cprop_of t2)) t2 in unlam_def_aux orig_ctxt ctxt tnorm end | NONE => singleton (ProofContext.export ctxt orig_ctxt) t) end;fun unlam_def ctxt t = unlam_def_aux ctxt ctxt t*}local_setup {* make_const_def @{binding IN} @{term "membship"} NoSyn @{typ "'a list"} @{typ "'a fset"} #> snd*}term membshipterm INthm IN_defML {* unlam_def @{context} @{thm IN_def} *}lemmas a = QUOT_TYPE.ABS_def[OF QUOT_TYPE_fset]thm QUOT_TYPE.thm11[OF QUOT_TYPE_fset, THEN iffD1, simplified a]lemma yy: shows "(False = x memb []) = (False = IN (x::nat) EMPTY)"unfolding IN_def EMPTY_defapply(rule_tac f="(op =) False" in arg_cong)apply(rule mem_respects)apply(simp only: QUOT_TYPE_I_fset.REP_ABS_rsp)apply(rule list_eq.intros)donelemma shows "IN (x::nat) EMPTY = False"using m1apply -apply(rule yy[THEN iffD1, symmetric])apply(simp)donelemma shows "((x=y) \<or> (IN x xs) = (IN (x::nat) (INSERT y xs))) = ((x=y) \<or> x memb REP_fset xs = x memb (y # REP_fset xs))"unfolding IN_def INSERT_defapply(rule_tac f="(op \<or>) (x=y)" in arg_cong)apply(rule_tac f="(op =) (x memb REP_fset xs)" in arg_cong)apply(rule mem_respects)apply(rule list_eq.intros(3))apply(unfold REP_fset_def ABS_fset_def)apply(simp only: QUOT_TYPE.REP_ABS_rsp[OF QUOT_TYPE_fset])apply(rule list_eq_sym)donelemma append_respects_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(simp add: list_eq_sym)donelemma yyy: shows " ( (UNION EMPTY s = s) & ((UNION (INSERT e s1) s2) = (INSERT e (UNION s1 s2))) ) = ( ((ABS_fset ([] @ REP_fset s)) = s) & ((ABS_fset ((e # (REP_fset s1)) @ REP_fset s2)) = ABS_fset (e # (REP_fset s1 @ REP_fset s2))) )" unfolding UNION_def EMPTY_def INSERT_def apply(rule_tac f="(op &)" in arg_cong2) apply(rule_tac f="(op =)" in arg_cong2) apply(simp only: QUOT_TYPE_I_fset.thm11[symmetric]) apply(rule append_respects_fst) apply(simp only: QUOT_TYPE_I_fset.REP_ABS_rsp) apply(rule list_eq_sym) apply(simp) apply(rule_tac f="(op =)" in arg_cong2) apply(simp only: QUOT_TYPE_I_fset.thm11[symmetric]) apply(rule append_respects_fst) apply(simp only: QUOT_TYPE_I_fset.REP_ABS_rsp) apply(rule list_eq_sym) apply(simp only: QUOT_TYPE_I_fset.thm11[symmetric]) apply(rule list_eq.intros(5)) apply(simp only: QUOT_TYPE_I_fset.REP_ABS_rsp) apply(rule list_eq_sym)donelemma shows " (UNION EMPTY s = s) & ((UNION (INSERT e s1) s2) = (INSERT e (UNION s1 s2)))" apply (simp add: yyy) apply (simp add: QUOT_TYPE_I_fset.thm10) doneML {* fun mk_rep_abs x = @{term REP_fset} $ (@{term ABS_fset} $ x) val consts = [@{const_name "Nil"}, @{const_name "append"}, @{const_name "Cons"}, @{const_name "membship"}]*}ML {*fun build_goal thm constructors lifted_type mk_rep_abs = let fun is_const (Const (x, t)) = x mem constructors | is_const _ = false fun maybe_mk_rep_abs t = let val _ = writeln ("Maybe: " ^ Syntax.string_of_term @{context} t) in if type_of t = lifted_type then mk_rep_abs t else t end fun build_aux (Abs (s, t, tr)) = (Abs (s, t, build_aux tr)) | build_aux (f $ a) = let val (f, args) = strip_comb (f $ a) val _ = writeln (Syntax.string_of_term @{context} f) in (if is_const f then maybe_mk_rep_abs (list_comb (f, (map maybe_mk_rep_abs (map build_aux args)))) else list_comb ((build_aux f), (map build_aux args))) end | build_aux x = if is_const x then maybe_mk_rep_abs x else x val prems = (*map HOLogic.dest_Trueprop*) (Thm.prems_of thm); val concl = (*HOLogic.dest_Trueprop*) (Thm.concl_of thm); val concl2 = Logic.list_implies (prems, concl)(* val concl2 = fold (fn a => fn c => HOLogic.mk_imp (a, c)) prems concl*) in HOLogic.mk_eq ((build_aux concl2), concl2)end *}ML {* val emptyt = (symmetric (unlam_def @{context} @{thm EMPTY_def})) *}ML {* val in_t = (symmetric (unlam_def @{context} @{thm IN_def})) *}ML {* val uniont = symmetric (unlam_def @{context} @{thm UNION_def}) *}ML {* val cardt = symmetric (unlam_def @{context} @{thm card_def}) *}ML {* val insertt = symmetric (unlam_def @{context} @{thm INSERT_def}) *}ML {* val fset_defs = @{thms EMPTY_def IN_def UNION_def card_def INSERT_def} *}ML {* val fset_defs_sym = [emptyt, in_t, uniont, cardt, insertt] *}ML {* fun dest_cbinop t = let val (t2, rhs) = Thm.dest_comb t; val (bop, lhs) = Thm.dest_comb t2; in (bop, (lhs, rhs)) end*}ML {* fun dest_ceq t = let val (bop, pair) = dest_cbinop t; val (bop_s, _) = Term.dest_Const (Thm.term_of bop); in if bop_s = "op =" then pair else (raise CTERM ("Not an equality", [t])) end*}ML Thm.instantiateML {*@{thm arg_cong2}*}ML {*@{thm arg_cong2[of _ _ _ _ "op ="]} *}ML {* val cT = @{cpat "op ="} |> Thm.ctyp_of_term |> Thm.dest_ctyp |> hd *}ML {* Toplevel.program (fn () => Drule.instantiate' [SOME cT,SOME cT,SOME @{ctyp bool}] [NONE,NONE,NONE,NONE,SOME (@{cpat "op ="})] @{thm arg_cong2} )*}ML {* fun foo_conv t = let val (lhs, rhs) = dest_ceq t; val (bop, _) = dest_cbinop lhs; val [clT, cr2] = bop |> Thm.ctyp_of_term |> Thm.dest_ctyp; val [cmT, crT] = Thm.dest_ctyp cr2; in Drule.instantiate' [SOME clT,SOME cmT,SOME crT] [NONE,NONE,NONE,NONE,SOME bop] @{thm arg_cong2} end*}ML {* fun foo_tac n thm = let val concl = Thm.cprem_of thm n; val (_, cconcl) = Thm.dest_comb concl; val rewr = foo_conv cconcl;(* val _ = tracing (Display.string_of_thm @{context} rewr) val _ = tracing (Display.string_of_thm @{context} thm)*) in rtac rewr n thm end handle CTERM _ => Seq.empty*}(* Has all the theorems about fset plugged in. These should be parameters to the tactic *)ML {* fun foo_tac' ctxt = REPEAT_ALL_NEW (FIRST' [ rtac @{thm list_eq_sym}, rtac @{thm cons_preserves}, rtac @{thm mem_respects}, rtac @{thm QUOT_TYPE_I_fset.R_trans2}, CHANGED o (simp_tac ((Simplifier.context ctxt HOL_ss) addsimps @{thms QUOT_TYPE_I_fset.REP_ABS_rsp})), foo_tac ])*}thm m1ML {* val m1_novars = snd(no_vars ((Context.Theory @{theory}),@{thm m1})) val goal = build_goal m1_novars consts @{typ "'a list"} mk_rep_abs val cgoal = cterm_of @{theory} goal val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false fset_defs_sym cgoal)*}notation ( output) "prop" ("#_" [1000] 1000)prove {* HOLogic.mk_Trueprop (Thm.term_of cgoal2) *} apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} ) apply (tactic {* print_tac "" *}) thm arg_cong2 [of "x memb REP_fset (ABS_fset (REP_fset (ABS_fset [])))" "x memb []" False False "op ="](* apply (rule arg_cong2 [of "x memb REP_fset (ABS_fset (REP_fset (ABS_fset [])))" "x memb []" False False "op ="])*) apply (subst arg_cong2 [of "x memb REP_fset (ABS_fset (REP_fset (ABS_fset [])))" "x memb []" False False "op ="]) apply (tactic {* foo_tac' @{context} 1 *}) apply (tactic {* foo_tac' @{context} 1 *}) thm arg_cong2 [of "x memb []" "x memb []" False False "op ="] (*apply (rule arg_cong2 [of "x memb []" "x memb []" False False "op ="]) done *) sorrythm length_append (* Not true but worth checking that the goal is correct *)ML {* val m1_novars = snd(no_vars ((Context.Theory @{theory}),@{thm length_append})) val goal = build_goal m1_novars consts @{typ "'a list"} mk_rep_abs val cgoal = cterm_of @{theory} goal val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false fset_defs_sym cgoal)*}prove {* HOLogic.mk_Trueprop (Thm.term_of cgoal2) *} apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} )(* apply (tactic {* foo_tac' @{context} 1 *})*) sorrythm m2ML {* val m1_novars = snd(no_vars ((Context.Theory @{theory}),@{thm m2})) val goal = build_goal m1_novars consts @{typ "'a list"} mk_rep_abs val cgoal = cterm_of @{theory} goal val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false fset_defs_sym cgoal)*}prove {* HOLogic.mk_Trueprop (Thm.term_of cgoal2) *} apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} )(* apply (tactic {* foo_tac' @{context} 1 *}) done *) sorrythm list_eq.intros(4)ML {* val m1_novars = snd(no_vars ((Context.Theory @{theory}),@{thm list_eq.intros(4)})) val goal = build_goal m1_novars consts @{typ "'a list"} mk_rep_abs val cgoal = cterm_of @{theory} goal val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false fset_defs_sym cgoal) val cgoal3 = Thm.rhs_of (MetaSimplifier.rewrite true @{thms QUOT_TYPE_I_fset.thm10} cgoal2)*}(* It is the same, but we need a name for it. *)prove {* HOLogic.mk_Trueprop (Thm.term_of cgoal3) *} apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} ) apply (tactic {* foo_tac' @{context} 1 *}) sorrylemma zzz : "(REP_fset (INSERT a (INSERT a (ABS_fset xs))) \<approx> REP_fset (INSERT a (ABS_fset xs))) = (a # a # xs \<approx> a # xs)" apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} ) apply (tactic {* foo_tac' @{context} 1 *}) donelemma zzz' : "(REP_fset (INSERT a (INSERT a (ABS_fset xs))) \<approx> REP_fset (INSERT a (ABS_fset xs)))" using list_eq.intros(4) by (simp only: zzz)thm QUOT_TYPE_I_fset.REPS_sameML {* val zzz'' = MetaSimplifier.rewrite_rule @{thms QUOT_TYPE_I_fset.REPS_same} @{thm zzz'} *}ML Drule.instantiate'ML {* zzz'' *}text {* A variable export will still be necessary in the end, but this is already the final theorem.*}ML {* Toplevel.program (fn () => MetaSimplifier.rewrite_rule @{thms QUOT_TYPE_I_fset.thm10} ( Drule.instantiate' [] [NONE,SOME (@{cpat "REP_fset x"})] zzz'' ) )*}thm symML {* val m1_novars = snd(no_vars ((Context.Theory @{theory}),@{thm sym})) val goal = build_goal m1_novars consts @{typ "'a list"} mk_rep_abs*}ML {* val cgoal = Toplevel.program (fn () => cterm_of @{theory} goal )*}thm list_eq.intros(5)ML {* val m1_novars = snd(no_vars ((Context.Theory @{theory}),@{thm list_eq.intros(5)})) val goal = build_goal m1_novars consts @{typ "'a list"} mk_rep_abs*}ML {* val cgoal = Toplevel.program (fn () => cterm_of @{theory} goal )*}ML {* val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false fset_defs_sym cgoal)*}prove {* HOLogic.mk_Trueprop (Thm.term_of cgoal2) *} apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} ) apply (tactic {* foo_tac' @{context} 1 *}) donethm list.inductML {* Logic.list_implies ((Thm.prems_of @{thm list.induct}), (Thm.concl_of @{thm list.induct})) *}ML {* val m1_novars = snd(no_vars ((Context.Theory @{theory}),@{thm list.induct}))*}ML {* val goal = Toplevel.program (fn () => build_goal m1_novars consts @{typ "'a list"} mk_rep_abs )*}ML {* val cgoal = cterm_of @{theory} goal val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false fset_defs_sym cgoal)*}thm card1_sucML {* val m1_novars = snd(no_vars ((Context.Theory @{theory}),@{thm card1_suc}))*}ML {* val goal = build_goal m1_novars consts @{typ "'a list"} mk_rep_abs*}ML {* val cgoal = cterm_of @{theory} goal val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false fset_defs_sym cgoal)*}(*datatype obj1 = OVAR1 "string"| OBJ1 "(string * (string \<Rightarrow> obj1)) list"| INVOKE1 "obj1 \<Rightarrow> string"| UPDATE1 "obj1 \<Rightarrow> string \<Rightarrow> (string \<Rightarrow> obj1)"*)