theory QuotMain
imports QuotScript QuotList Prove
begin
locale 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)"
begin
definition
"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 simp
qed
theorem thm10:
shows "ABS (REP a) = a"
unfolding ABS_def REP_def
proof -
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 simp
qed
lemma REP_refl:
shows "R (REP a) (REP a)"
unfolding REP_def
by (simp add: equiv[simplified EQUIV_def])
lemma lem7:
"(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)
done
theorem thm11:
shows "R r r' = (ABS r = ABS r')"
unfolding ABS_def
by (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"
apply(subst thm11)
apply(simp add: thm10 thm11)
apply(subst thm11)
apply(simp add: thm10 thm11)
done
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])
done
end
section {* 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 Free
in
lambda c
(HOLogic.mk_exists
("x", ty, HOLogic.mk_eq (c, (rel $ x))))
end
*}
(*
ML {*
typedef_term @{term R} @{typ "nat"} @{context}
|> Syntax.string_of_term @{context}
|> writeln
*}*)
ML {*
val typedef_tac =
EVERY1 [rewrite_goal_tac @{thms mem_def},
rtac @{thm exI}, rtac @{thm exI}, rtac @{thm refl}]
*}
ML {*
(* makes the new type definitions *)
fun typedef_make (qty_name, rel, ty) lthy =
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) lthy
*}
text {* proves the QUOT_TYPE theorem for the new type *}
ML {*
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_inv
in
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]
end
*}
term QUOT_TYPE
ML {* HOLogic.mk_Trueprop *}
ML {* Goal.prove *}
ML {* Syntax.check_term *}
ML {*
fun 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 lthy
in
Goal.prove lthy [] [] goal
(fn _ => typedef_quot_type_tac equiv_thm typedef_info)
end
*}
ML {*
fun typedef_quotient_thm_tac defs quot_type_thm =
EVERY1 [K (rewrite_goals_tac defs),
rtac @{thm QUOT_TYPE.QUOTIENT},
rtac quot_type_thm]
*}
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
in
Goal.prove lthy [] [] goal
(fn _ => typedef_quotient_thm_tac [abs_def, rep_def] quot_type_thm)
end
*}
text {* two wrappers for define and note *}
ML {*
fun make_def (name, mx, trm) lthy =
let
val ((trm, (_ , thm)), lthy') =
LocalTheory.define Thm.internalK ((name, mx), (Attrib.empty_binding, trm)) lthy
in
((trm, thm), lthy')
end
*}
ML {*
fun reg_thm (name, thm) lthy =
let
val ((_,[thm']), lthy') = LocalTheory.note Thm.theoremK ((name, []), [thm]) lthy
in
(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), lthy') = 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 lthy' (ABS_const $ rel $ abs)
val REP_trm = Syntax.check_term lthy' (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)), lthy'') =
lthy' |> 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) lthy''
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) lthy''
val quotient_thm_name = Binding.prefix_name "QUOTIENT_" qty_name
(* interpretation *)
val bindd = ((Binding.make ("", Position.none)), ([]: Attrib.src list))
val ((_, [eqn1pre]), lthy''') = Variable.import true [ABS_def] lthy'';
val eqn1i = Thm.prop_of (symmetric eqn1pre)
val ((_, [eqn2pre]), lthy'''') = Variable.import true [REP_def] lthy''';
val eqn2i = Thm.prop_of (symmetric eqn2pre)
val exp_morphism = ProofContext.export_morphism lthy'''' (ProofContext.init (ProofContext.theory_of lthy''''));
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
lthy''''
|> reg_thm (quot_thm_name, quot_thm)
||>> reg_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, lthy''''') = Variable.import_terms true global_eqns lthy'''';
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"
ML {*
typedef_main
*}
local_setup {*
typedef_main (@{binding "qtrm"}, @{term "RR"}, @{typ trm}, @{thm r_eq}) #> snd
*}
term Rep_qtrm
term REP_qtrm
term Abs_qtrm
term ABS_qtrm
thm QUOT_TYPE_qtrm
thm QUOTIENT_qtrm
(* Test interpretation *)
thm QUOT_TYPE_I_qtrm.thm11
thm Rep_qtrm
text {* another test *}
datatype 'a my = Foo
consts Rmy :: "'a my \<Rightarrow> 'a my \<Rightarrow> bool"
axioms rmy_eq: "EQUIV Rmy"
term "\<lambda>(c::'a my\<Rightarrow>bool). \<exists>x. c = Rmy x"
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_theorems
term 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 | rep
fun 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_ty
in
map (op $) (rep_fns ~~ fresh_args)
|> curry list_comb oconst
|> curry (op $) abs_fn
|> fold_rev lambda fresh_args
end
*}
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_name oconst mx rty qty lthy =
let
val oconst_ty = fastype_of oconst
val nconst_ty = exchange_ty rty qty oconst_ty
val nconst = Const (nconst_name, nconst_ty)
val def_trm = get_const_def nconst oconst rty qty lthy
in
make_def (Binding.name nconst_name, mx, def_trm) lthy
end
*}
local_setup {*
make_const_def "VR" @{term "vr"} NoSyn @{typ "t"} @{typ "qt"} #> snd
*}
local_setup {*
make_const_def "AP" @{term "ap"} NoSyn @{typ "t"} @{typ "qt"} #> snd
*}
local_setup {*
make_const_def "LM" @{term "lm"} NoSyn @{typ "t"} @{typ "qt"} #> snd
*}
thm VR_def
thm AP_def
thm LM_def
term LM
term VR
term AP
text {* 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_theorems
local_setup {*
make_const_def "VR'" @{term "vr'"} NoSyn @{typ "'a t'"} @{typ "'a qt'"} #> snd
*}
local_setup {*
make_const_def "AP'" @{term "ap'"} NoSyn @{typ "'a t'"} @{typ "'a qt'"} #> snd
*}
local_setup {*
make_const_def "LM'" @{term "lm'"} NoSyn @{typ "'a t'"} @{typ "'a qt'"} #> snd
*}
thm VR'_def
thm AP'_def
thm LM'_def
term LM'
term VR'
term AP'
text {* finite set example *}
print_syntax
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_sym:
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_sym)
done
local_setup {*
typedef_main (@{binding "fset"}, @{term "list_eq"}, @{typ "'a list"}, @{thm "equiv_list_eq"}) #> snd
*}
print_theorems
typ "'a fset"
thm "Rep_fset"
local_setup {*
make_const_def "EMPTY" @{term "[]"} NoSyn @{typ "'a list"} @{typ "'a fset"} #> snd
*}
term Nil
term EMPTY
thm EMPTY_def
local_setup {*
make_const_def "INSERT" @{term "op #"} NoSyn @{typ "'a list"} @{typ "'a fset"} #> snd
*}
term Cons
term INSERT
thm INSERT_def
local_setup {*
make_const_def "UNION" @{term "op @"} NoSyn @{typ "'a list"} @{typ "'a fset"} #> snd
*}
term append
term UNION
thm UNION_def
local_setup {*
make_const_def "CARD" @{term "length"} NoSyn @{typ "'a list"} @{typ "'a fset"} #> snd
*}
term length
term CARD
thm CARD_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))"
lemma mem_respects:
fixes z
assumes a: "list_eq x y"
shows "(z memb x) = (z memb y)"
using a by induct auto
lemma cons_preserves:
fixes z
assumes a: "xs \<approx> ys"
shows "(z # xs) \<approx> (z # ys)"
using a by (rule QuotMain.list_eq.intros(5))
ML {*
fun unlam_def 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 orig_ctxt ctxt tnorm end
| NONE => singleton (ProofContext.export ctxt orig_ctxt) t)
end
*}
local_setup {*
make_const_def "IN" @{term "membship"} NoSyn @{typ "'a list"} @{typ "'a fset"} #> snd
*}
term membship
term IN
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_def
apply(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)
done
lemma
shows "IN (x::nat) EMPTY = False"
using m1
apply -
apply(rule yy[THEN iffD1, symmetric])
apply(simp)
done
lemma
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_def
apply(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)
done
lemma 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)
done
lemma 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)
done
lemma
shows "
(UNION EMPTY s = s) &
((UNION (INSERT e s1) s2) = (INSERT e (UNION s1 s2)))"
apply (simp add: yyy)
apply (rule QUOT_TYPE_I_fset.thm10)
done
ML {*
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 concl = HOLogic.dest_Trueprop (Thm.concl_of thm)
in
HOLogic.mk_eq ((build_aux concl), concl)
end *}
ML {* val emptyt = (symmetric (unlam_def @{context} @{context} @{thm EMPTY_def})) *}
ML {* val in_t = (symmetric (unlam_def @{context} @{context} @{thm IN_def})) *}
ML {* val uniont = symmetric (unlam_def @{context} @{context} @{thm UNION_def}) *}
ML {* val cardt = symmetric (unlam_def @{context} @{context} @{thm CARD_def}) *}
ML {* val insertt = symmetric (unlam_def @{context} @{context} @{thm INSERT_def}) *}
ML {*
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 [emptyt, in_t] cgoal)
*}
prove {* HOLogic.mk_Trueprop (Thm.term_of cgoal2) *}
apply(rule_tac f="(op =)" in arg_cong2)
unfolding IN_def EMPTY_def
apply (rule_tac mem_respects)
apply (simp only: QUOT_TYPE_I_fset.REP_ABS_rsp)
apply (simp_all)
apply (rule list_eq_sym)
done
thm 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 [emptyt, in_t, cardt, uniont] cgoal)
*}
thm m2
ML {*
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 [emptyt, in_t, cardt, uniont, insertt] cgoal)
*}
prove {* HOLogic.mk_Trueprop (Thm.term_of cgoal2) *}
apply(rule_tac f="(op =)" in arg_cong2)
unfolding IN_def
apply (rule_tac mem_respects)
unfolding INSERT_def
apply (simp only: QUOT_TYPE_I_fset.REP_ABS_rsp)
apply (rule cons_preserves)
apply (simp only: QUOT_TYPE_I_fset.REP_ABS_rsp)
apply (rule list_eq_sym)
apply(rule_tac f="(op \<or>)" in arg_cong2)
apply (simp)
apply (rule_tac mem_respects)
apply (simp only: QUOT_TYPE_I_fset.REP_ABS_rsp)
apply (rule list_eq_sym)
done