the command "quotient" can now define more than one quotient at the same time; quotients need to be separated by and
theory QuotMain
imports QuotScript QuotList Prove
uses ("quotient.ML")
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) \<equiv> a"
apply (rule eq_reflection)
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:
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)
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"
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])
done
lemma 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 blast
qed
lemma 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 blast
qed
lemma 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 blast
next
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 blast
qed
lemma REPS_same:
shows "R (REP a) (REP b) \<equiv> (a = b)"
proof -
have "R (REP a) (REP b) = (a = b)"
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 simp
next
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 auto
qed
then show "R (REP a) (REP b) \<equiv> (a = b)" by simp
qed
end
section {* type definition for the quotient type *}
use "quotient.ML"
term EQUIV
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);
*}
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"
quotient qtrm = trm / "RR"
apply(rule r_eq)
done
typ qtrm
term Rep_qtrm
term REP_qtrm
term Abs_qtrm
term ABS_qtrm
thm QUOT_TYPE_qtrm
thm QUOTIENT_qtrm
thm REP_qtrm_def
(* Test interpretation *)
thm QUOT_TYPE_I_qtrm.thm11
thm QUOT_TYPE.thm11
print_theorems
thm Rep_qtrm
text {* 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'"
quotient qtrm' = "'a trm'" / "R'"
apply(rule r_eq')
done
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"
quotient qt = "t" / "Rt"
by (rule t_eq)
section {* lifting of constants *}
text {* information about map-functions for type-constructor *}
ML {*
type typ_info = {mapfun: string, relfun: string}
local
structure Data = TheoryDataFun
(type T = typ_info Symtab.table
val empty = Symtab.empty
val copy = I
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 {*
update @{type_name "list"} {mapfun = @{const_name "map"}, relfun = @{const_name "LIST_REL"}} #>
update @{type_name "*"} {mapfun = @{const_name "prod_fun"}, relfun = @{const_name "prod_rel"}} #>
update @{type_name "fun"} {mapfun = @{const_name "fun_map"}, relfun = @{const_name "FUN_REL"}}
*}
ML {* lookup @{theory} @{type_name list} *}
ML {*
(* calculates the aggregate abs and rep functions for a given type;
repF is for constants' arguments; absF is for constants;
function types need to be treated specially, since repF and absF
change
*)
datatype flag = absF | repF
fun negF absF = repF
| negF repF = absF
fun get_fun flag 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 (ProofContext.theory_of 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_fun_fun fs_tys =
let
val (fs, tys) = split_list fs_tys
val ([oty1, oty2], [nty1, nty2]) = split_list tys
val oty = Type ("fun", [nty1, oty2])
val nty = Type ("fun", [oty1, nty2])
val ftys = map (op -->) tys
in
(list_comb (Const (@{const_name "fun_map"}, ftys ---> oty --> nty), fs), (oty, nty))
end
fun get_const absF = (Const ("QuotMain.ABS_" ^ qty_name, rty --> qty), (rty, qty))
| get_const repF = (Const ("QuotMain.REP_" ^ qty_name, qty --> rty), (qty, rty))
fun mk_identity ty = Abs ("", ty, Bound 0)
in
if ty = qty
then (get_const flag)
else (case ty of
TFree _ => (mk_identity ty, (ty, ty))
| Type (_, []) => (mk_identity ty, (ty, ty))
| Type ("fun" , [ty1, ty2]) =>
get_fun_fun [get_fun (negF flag) rty qty lthy ty1, get_fun flag rty qty lthy ty2]
| Type (s, tys) => get_fun_aux s (map (get_fun flag rty qty lthy) tys)
| _ => raise ERROR ("no type variables")
)
end
*}
ML {*
get_fun repF @{typ t} @{typ qt} @{context} @{typ "((((qt \<Rightarrow> qt) \<Rightarrow> qt) \<Rightarrow> qt) list) * nat"}
|> fst
|> Syntax.string_of_term @{context}
|> writeln
*}
ML {*
get_fun absF @{typ t} @{typ qt} @{context} @{typ "qt * nat"}
|> fst
|> Syntax.string_of_term @{context}
|> writeln
*}
ML {*
get_fun absF @{typ t} @{typ qt} @{context} @{typ "(qt \<Rightarrow> qt) \<Rightarrow> qt"}
|> fst
|> Syntax.pretty_term @{context}
|> Pretty.string_of
|> writeln
*}
text {* produces the definition for a lifted constant *}
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 repF rty qty lthy) arg_tys
val abs_fn = (fst o get_fun absF 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_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 lthy
in
define (nconst_bname, mx, def_trm) lthy
end
*}
(* A test whether get_fun works properly
consts bla :: "(t \<Rightarrow> t) \<Rightarrow> t"
local_setup {*
fn lthy => (Toplevel.program (fn () =>
make_const_def @{binding bla'} @{term "bla"} NoSyn @{typ "t"} @{typ "qt"} lthy
)) |> snd
*}
*)
local_setup {*
make_const_def @{binding VR} @{term "vr"} NoSyn @{typ "t"} @{typ "qt"} #> snd #>
make_const_def @{binding AP} @{term "ap"} NoSyn @{typ "t"} @{typ "qt"} #> snd #>
make_const_def @{binding LM} @{term "lm"} NoSyn @{typ "t"} @{typ "qt"} #> snd
*}
term vr
term ap
term lm
thm VR_def AP_def 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'"
quotient qt' = "'a t'" / "Rt'"
apply(rule t_eq')
done
print_theorems
local_setup {*
make_const_def @{binding VR'} @{term "vr'"} NoSyn @{typ "'a t'"} @{typ "'a qt'"} #> snd #>
make_const_def @{binding AP'} @{term "ap'"} NoSyn @{typ "'a t'"} @{typ "'a qt'"} #> snd #>
make_const_def @{binding LM'} @{term "lm'"} NoSyn @{typ "'a t'"} @{typ "'a qt'"} #> snd
*}
term vr'
term ap'
term ap'
thm VR'_def AP'_def 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_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"
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))"
lemma mem_respects:
fixes z
assumes a: "list_eq x y"
shows "(z memb x) = (z memb y)"
using a by induct auto
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_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)
done
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 QuotMain.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 cons_preserves:
fixes z
assumes a: "xs \<approx> ys"
shows "(z # xs) \<approx> (z # ys)"
using a by (rule QuotMain.list_eq.intros(5))
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 QuotMain.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
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_refl)
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_refl)
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_refl)
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_refl)
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_refl)
done
lemma
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)
done
ML {*
fun mk_rep x = @{term REP_fset} $ x;
fun mk_abs x = @{term ABS_fset} $ x;
val consts = [@{const_name "Nil"}, @{const_name "Cons"},
@{const_name "membship"}, @{const_name "card1"},
@{const_name "append"}, @{const_name "fold1"}];
*}
ML {* val tm = @{term "x :: 'a list"} *}
ML {* val ty = exchange_ty @{typ "'a list"} @{typ "'a fset"} (fastype_of tm) *}
ML {* (fst (get_fun repF @{typ "'a list"} @{typ "'a fset"} @{context} ty)) $ tm *}
ML {* val qty = @{typ "'a fset"} *}
ML {* val tt = Type ("fun", [Type ("fun", [qty, @{typ "prop"}]), @{typ "prop"}]) *}
ML {* val fall = Const(@{const_name all}, dummyT) *}
ML {*
fun needs_lift (rty as Type (rty_s, _)) ty =
case ty of
Type (s, tys) =>
(s = rty_s) orelse (exists (needs_lift rty) tys)
| _ => false
*}
ML {*
fun build_goal_term lthy thm constructors rty qty =
let
fun mk_rep tm =
let
val ty = exchange_ty rty qty (fastype_of tm)
in fst (get_fun repF rty qty lthy ty) $ tm end
fun mk_abs tm =
let
val _ = tracing (Syntax.string_of_term @{context} tm)
val _ = tracing (Syntax.string_of_typ @{context} (fastype_of tm))
val ty = exchange_ty rty qty (fastype_of tm) in
fst (get_fun absF rty qty lthy ty) $ tm end
fun is_constructor (Const (x, _)) = member (op =) constructors x
| is_constructor _ = false;
fun build_aux lthy tm =
case tm of
Abs (a as (_, vty, _)) =>
let
val (vs, t) = Term.dest_abs a;
val v = Free(vs, vty);
val t' = lambda v (build_aux lthy t)
in
if (not (needs_lift rty (fastype_of tm))) then t'
else mk_rep (mk_abs (
if not (needs_lift rty vty) then t'
else
let
val v' = mk_rep (mk_abs v);
val t1 = Envir.beta_norm (t' $ v')
in
lambda v t1
end
))
end
| x =>
let
val _ = tracing (">>" ^ Syntax.string_of_term @{context} tm)
val (opp, tms0) = Term.strip_comb tm
val tms = map (build_aux lthy) tms0
val ty = fastype_of tm
in
if (((fst (Term.dest_Const opp)) = @{const_name Respects}) handle _ => false)
then (list_comb (opp, (hd tms0) :: (tl tms)))
else if (is_constructor opp andalso needs_lift rty ty) then
mk_rep (mk_abs (list_comb (opp,tms)))
else if ((Term.is_Free opp) andalso (length tms > 0) andalso (needs_lift rty ty)) then
mk_rep(mk_abs(list_comb(opp,tms)))
else if tms = [] then opp
else list_comb(opp, tms)
end
in
build_aux lthy (Thm.prop_of thm)
end
*}
ML {*
fun build_goal_term_old ctxt thm constructors rty qty mk_rep mk_abs =
let
fun mk_rep_abs x = mk_rep (mk_abs x);
fun is_constructor (Const (x, _)) = member (op =) constructors x
| is_constructor _ = false;
fun maybe_mk_rep_abs t =
let
val _ = writeln ("Maybe: " ^ Syntax.string_of_term ctxt t)
in
if fastype_of t = rty then mk_rep_abs t else t
end;
fun is_all (Const ("all", Type("fun", [Type("fun", [ty, _]), _]))) = ty = rty
| is_all _ = false;
fun is_ex (Const ("Ex", Type("fun", [Type("fun", [ty, _]), _]))) = ty = rty
| is_ex _ = false;
fun build_aux ctxt1 tm =
let
val (head, args) = Term.strip_comb tm;
val args' = map (build_aux ctxt1) args;
in
(case head of
Abs (x, T, t) =>
if T = rty then let
val ([x'], ctxt2) = Variable.variant_fixes [x] ctxt1;
val v = Free (x', qty);
val t' = subst_bound (mk_rep v, t);
val rec_term = build_aux ctxt2 t';
val _ = tracing (Syntax.string_of_term ctxt2 t')
val _ = tracing (Syntax.string_of_term ctxt2 (Term.lambda_name (x, v) rec_term))
in
Term.lambda_name (x, v) rec_term
end else let
val ([x'], ctxt2) = Variable.variant_fixes [x] ctxt1;
val v = Free (x', T);
val t' = subst_bound (v, t);
val rec_term = build_aux ctxt2 t';
in Term.lambda_name (x, v) rec_term end
| _ => (* I assume that we never lift 'prop' since it is not of sort type *)
if is_all head then
list_comb (Const(@{const_name all}, dummyT), args') |> Syntax.check_term ctxt1
else if is_ex head then
list_comb (Const(@{const_name Ex}, dummyT), args') |> Syntax.check_term ctxt1
else if is_constructor head then
maybe_mk_rep_abs (list_comb (head, map maybe_mk_rep_abs args'))
else
maybe_mk_rep_abs (list_comb (head, args'))
)
end;
in
build_aux ctxt (Thm.prop_of thm)
end
*}
ML {*
fun build_goal ctxt thm cons rty qty =
Logic.mk_equals ((Thm.prop_of thm), (build_goal_term ctxt thm cons rty qty))
*}
ML {*
val m1_novars = snd(no_vars ((Context.Theory @{theory}), @{thm m2}))
*}
ML {*
cterm_of @{theory} (prop_of m1_novars);
cterm_of @{theory} (build_goal_term @{context} m1_novars consts @{typ "'a list"} @{typ "'a fset"});
cterm_of @{theory} (build_goal_term_old @{context} m1_novars consts @{typ "'a list"} @{typ "'a fset"} mk_rep mk_abs)
*}
text {*
Unabs_def converts a definition given as
c \<equiv> %x. %y. f x y
to a theorem of the form
c x y \<equiv> f x y
This function is needed to rewrite the right-hand
side to the left-hand side.
*}
ML {*
fun unabs_def ctxt def =
let
val (lhs, rhs) = Thm.dest_equals (cprop_of def)
val xs = strip_abs_vars (term_of rhs)
val (_, ctxt') = Variable.add_fixes (map fst xs) ctxt
val thy = ProofContext.theory_of ctxt'
val cxs = map (cterm_of thy o Free) xs
val new_lhs = Drule.list_comb (lhs, cxs)
fun get_conv [] = Conv.rewr_conv def
| get_conv (x::xs) = Conv.fun_conv (get_conv xs)
in
get_conv xs new_lhs |>
singleton (ProofContext.export ctxt' ctxt)
end
*}
ML {* (* Test: *) @{thm IN_def}; unabs_def @{context} @{thm IN_def} *}
ML {* val fset_defs = @{thms EMPTY_def IN_def UNION_def card_def INSERT_def} *}
ML {* val fset_defs_sym = map (fn t => symmetric (unabs_def @{context} t)) fset_defs *}
lemma atomize_eqv[atomize]:
shows "(Trueprop A \<equiv> Trueprop B) \<equiv> (A \<equiv> B)"
proof
assume "A \<equiv> B"
then show "Trueprop A \<equiv> Trueprop B" by unfold
next
assume *: "Trueprop A \<equiv> Trueprop B"
have "A = B"
proof (cases A)
case True
have "A" by fact
then show "A = B" using * by simp
next
case False
have "\<not>A" by fact
then show "A = B" using * by auto
qed
then show "A \<equiv> B" by (rule eq_reflection)
qed
(* Has all the theorems about fset plugged in. These should be parameters to the tactic *)
ML {*
fun transconv_fset_tac' ctxt =
(LocalDefs.unfold_tac @{context} fset_defs) THEN
ObjectLogic.full_atomize_tac 1 THEN
REPEAT_ALL_NEW (FIRST' [
rtac @{thm list_eq_refl},
rtac @{thm cons_preserves},
rtac @{thm mem_respects},
rtac @{thm card1_rsp},
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})),
Cong_Tac.cong_tac @{thm cong},
rtac @{thm ext}
]) 1
*}
ML {*
val m1_novars = snd(no_vars ((Context.Theory @{theory}), @{thm m1}))
val goal = build_goal @{context} m1_novars consts @{typ "'a list"} @{typ "'a fset"}
val cgoal = cterm_of @{theory} goal
val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false fset_defs_sym cgoal)
*}
(*notation ( output) "prop" ("#_" [1000] 1000) *)
notation ( output) "Trueprop" ("#_" [1000] 1000)
prove {* (Thm.term_of cgoal2) *}
apply (tactic {* transconv_fset_tac' @{context} *})
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 @{context} m1_novars consts @{typ "'a list"} @{typ "'a fset"}
val cgoal = cterm_of @{theory} goal
val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false fset_defs_sym cgoal)
*}
prove {* Thm.term_of cgoal2 *}
apply (tactic {* transconv_fset_tac' @{context} *})
sorry
thm m2
ML {*
val m1_novars = snd(no_vars ((Context.Theory @{theory}), @{thm m2}))
val goal = build_goal @{context} m1_novars consts @{typ "'a list"} @{typ "'a fset"}
val cgoal = cterm_of @{theory} goal
val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false fset_defs_sym cgoal)
*}
prove {* Thm.term_of cgoal2 *}
apply (tactic {* transconv_fset_tac' @{context} *})
done
thm list_eq.intros(4)
ML {*
val m1_novars = snd(no_vars ((Context.Theory @{theory}), @{thm list_eq.intros(4)}))
val goal = build_goal @{context} m1_novars consts @{typ "'a list"} @{typ "'a fset"}
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 zzz : {* Thm.term_of cgoal3 *}
apply (tactic {* transconv_fset_tac' @{context} *})
done
(*lemma 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_same
ML {* val zzz'' = MetaSimplifier.rewrite_rule @{thms QUOT_TYPE_I_fset.REPS_same} @{thm zzz'} *}
*)
thm list_eq.intros(5)
ML {*
val m1_novars = snd(no_vars ((Context.Theory @{theory}), @{thm list_eq.intros(5)}))
val goal = build_goal @{context} m1_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)
*}
prove {* Thm.term_of cgoal2 *}
apply (tactic {* transconv_fset_tac' @{context} *})
done
section {* handling quantifiers - regularize *}
text {* tyRel takes a type and builds a relation that a quantifier over this
type needs to respect. *}
ML {*
fun tyRel ty rty rel lthy =
if ty = rty
then rel
else (case ty of
Type (s, tys) =>
let
val tys_rel = map (fn ty => ty --> ty --> @{typ bool}) tys;
val ty_out = ty --> ty --> @{typ bool};
val tys_out = tys_rel ---> ty_out;
in
(case (lookup (ProofContext.theory_of lthy) s) of
SOME (info) => list_comb (Const (#relfun info, tys_out), map (fn ty => tyRel ty rty rel lthy) tys)
| NONE => HOLogic.eq_const ty
)
end
| _ => HOLogic.eq_const ty)
*}
ML {*
cterm_of @{theory} (tyRel @{typ "trm \<Rightarrow> bool"} @{typ "trm"} @{term "RR"} @{context})
*}
definition
Babs :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b"
where
"(x \<in> p) \<Longrightarrow> (Babs p m x = m x)"
(* TODO: Consider defining it with an "if"; sth like:
Babs p m = \<lambda>x. if x \<in> p then m x else undefined
*)
ML {*
(* trm \<Rightarrow> new_trm *)
fun regularise trm rty rel lthy =
case trm of
Abs (x, T, t) =>
if (needs_lift rty T) then let
val ([x'], lthy2) = Variable.variant_fixes [x] lthy;
val v = Free (x', T);
val t' = subst_bound (v, t);
val rec_term = regularise t' rty rel lthy2;
val lam_term = Term.lambda_name (x, v) rec_term;
val sub_res_term = tyRel T rty rel lthy;
val respects = Const (@{const_name Respects}, (fastype_of sub_res_term) --> T --> @{typ bool});
val res_term = respects $ sub_res_term;
val ty = fastype_of trm;
val rabs = Const (@{const_name Babs}, (fastype_of res_term) --> ty --> ty);
val rabs_term = (rabs $ res_term) $ lam_term;
in
rabs_term
end else let
val ([x'], lthy2) = Variable.variant_fixes [x] lthy;
val v = Free (x', T);
val t' = subst_bound (v, t);
val rec_term = regularise t' rty rel lthy2;
in
Term.lambda_name (x, v) rec_term
end
| ((Const (@{const_name "All"}, at)) $ (Abs (x, T, t))) =>
if (needs_lift rty T) then let
val ([x'], lthy2) = Variable.variant_fixes [x] lthy;
val v = Free (x', T);
val t' = subst_bound (v, t);
val rec_term = regularise t' rty rel lthy2;
val lam_term = Term.lambda_name (x, v) rec_term;
val sub_res_term = tyRel T rty rel lthy;
val respects = Const (@{const_name Respects}, (fastype_of sub_res_term) --> T --> @{typ bool});
val res_term = respects $ sub_res_term;
val ty = fastype_of lam_term;
val rall = Const (@{const_name Ball}, (fastype_of res_term) --> ty --> @{typ bool});
val rall_term = (rall $ res_term) $ lam_term;
in
rall_term
end else let
val ([x'], lthy2) = Variable.variant_fixes [x] lthy;
val v = Free (x', T);
val t' = subst_bound (v, t);
val rec_term = regularise t' rty rel lthy2;
val lam_term = Term.lambda_name (x, v) rec_term
in
Const(@{const_name "All"}, at) $ lam_term
end
| ((Const (@{const_name "All"}, at)) $ P) =>
let
val (_, [al, _]) = dest_Type (fastype_of P);
val ([x], lthy2) = Variable.variant_fixes [""] lthy;
val v = (Free (x, al));
val abs = Term.lambda_name (x, v) (P $ v);
in regularise ((Const (@{const_name "All"}, at)) $ abs) rty rel lthy2 end
| ((Const (@{const_name "Ex"}, at)) $ (Abs (x, T, t))) =>
if (needs_lift rty T) then let
val ([x'], lthy2) = Variable.variant_fixes [x] lthy;
val v = Free (x', T);
val t' = subst_bound (v, t);
val rec_term = regularise t' rty rel lthy2;
val lam_term = Term.lambda_name (x, v) rec_term;
val sub_res_term = tyRel T rty rel lthy;
val respects = Const (@{const_name Respects}, (fastype_of sub_res_term) --> T --> @{typ bool});
val res_term = respects $ sub_res_term;
val ty = fastype_of lam_term;
val rall = Const (@{const_name Bex}, (fastype_of res_term) --> ty --> @{typ bool});
val rall_term = (rall $ res_term) $ lam_term;
in
rall_term
end else let
val ([x'], lthy2) = Variable.variant_fixes [x] lthy;
val v = Free (x', T);
val t' = subst_bound (v, t);
val rec_term = regularise t' rty rel lthy2;
val lam_term = Term.lambda_name (x, v) rec_term
in
Const(@{const_name "Ex"}, at) $ lam_term
end
| ((Const (@{const_name "Ex"}, at)) $ P) =>
let
val (_, [al, _]) = dest_Type (fastype_of P);
val ([x], lthy2) = Variable.variant_fixes [""] lthy;
val v = (Free (x, al));
val abs = Term.lambda_name (x, v) (P $ v);
in regularise ((Const (@{const_name "Ex"}, at)) $ abs) rty rel lthy2 end
| a $ b => (regularise a rty rel lthy) $ (regularise b rty rel lthy)
| _ => trm
*}
ML {*
cterm_of @{theory} (regularise @{term "\<lambda>x :: int. x"} @{typ "trm"} @{term "RR"} @{context});
cterm_of @{theory} (regularise @{term "\<lambda>x :: trm. x"} @{typ "trm"} @{term "RR"} @{context});
cterm_of @{theory} (regularise @{term "\<forall>x :: trm. P x"} @{typ "trm"} @{term "RR"} @{context});
cterm_of @{theory} (regularise @{term "\<exists>x :: trm. P x"} @{typ "trm"} @{term "RR"} @{context});
cterm_of @{theory} (regularise @{term "All (P :: trm \<Rightarrow> bool)"} @{typ "trm"} @{term "RR"} @{context});
*}
ML {*
fun atomize_thm thm =
let
val thm' = forall_intr_vars thm
val thm'' = ObjectLogic.atomize (cprop_of thm')
in
Simplifier.rewrite_rule [thm''] thm'
end
*}
thm list.induct
lemma list_induct_hol4:
fixes P :: "'a list \<Rightarrow> bool"
assumes "((P []) \<and> (\<forall>t. (P t) \<longrightarrow> (\<forall>h. (P (h # t)))))"
shows "(\<forall>l. (P l))"
sorry
ML {* atomize_thm @{thm list_induct_hol4} *}
(*fun prove_reg trm \<Rightarrow> thm (we might need some facts to do this)
trm == new_trm
*)
ML {* val li = Thm.freezeT (atomize_thm @{thm list_induct_hol4}) *}
prove list_induct_r: {*
Logic.mk_implies
((prop_of li),
(regularise (prop_of li) @{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
ML {* val thm = @{thm list_induct_r} OF [li] *}
ML {* val trm = build_goal @{context} thm consts @{typ "'a list"} @{typ "'a fset"} *}
lemmas APPLY_RSP_I = APPLY_RSP[of "(op \<approx> ===> op =) ===> op =" "(ABS_fset ---> id) ---> id" "(REP_fset ---> id) ---> id" "op =" "id" "id"]
lemmas REP_ABS_RSP_I = REP_ABS_RSP(1)[of "(op \<approx> ===> op =) ===> op =" "(ABS_fset ---> id) ---> id" "(REP_fset ---> id) ---> id"]
prove trm
apply (atomize(full))
apply (simp only: id_def[symmetric])
(* APPLY_RSP_TAC *)
ML_prf {*
val (_, gc') = Thm.dest_comb (Subgoal.focus @{context} 1 (Isar.goal ()) |> fst |> #concl)
val (_, tc') = Thm.dest_comb (cterm_of @{theory} (concl_of @{thm "APPLY_RSP_I" }))
val m = Thm.match (tc', gc')
val t2 = Drule.instantiate m @{thm "APPLY_RSP_I" }
*}
thm APPLY_RSP_I
apply (tactic {* rtac t2 1 *})
prefer 2
apply (rule IDENTITY_QUOTIENT)
prefer 3
(* ABS_REP_RSP_TAC *)
ML_prf {*
val (_, gc') = Thm.dest_comb (Subgoal.focus @{context} 1 (Isar.goal ()) |> fst |> #concl)
val (_, tc') = Thm.dest_comb (cterm_of @{theory} (concl_of @{thm "REP_ABS_RSP_I" }))
val m = Thm.match (tc', gc')
val t2 = Drule.instantiate m @{thm "REP_ABS_RSP_I" }
*}
apply (tactic {* rtac t2 1 *})
prefer 2
(* LAMBDA_RES_TAC *)
apply (simp only: FUN_REL.simps)
apply (rule allI)
apply (rule allI)
apply (rule impI)
(* MK_COMB_TAC *)
apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1 *})
(* MK_COMB_TAC *)
apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1 *})
(* REFL_TAC *)
apply (simp)
(* MK_COMB_TAC *)
apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1 *})
(* MK_COMB_TAC *)
apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1 *})
(* REFL_TAC *)
apply (simp)
(* APPLY_RSP_TAC *)
apply (rule_tac APPLY_RSP[of "op \<approx>" "ABS_fset" "REP_fset" "op =" "id" "id"])
apply (rule QUOTIENT_fset)
apply (rule IDENTITY_QUOTIENT)
prefer 2
(* ABS_REP_RSP *)
apply (rule REP_ABS_RSP(1)[of "op \<approx>" "ABS_fset" "REP_fset"])
apply (rule QUOTIENT_fset)
(* MINE *)
apply (rule list_eq_refl )
(* ABS_REP_RSP *)
apply (rule REP_ABS_RSP(1)[of "op \<approx> ===> op =" "REP_fset ---> id" "ABS_fset ---> id"])
prefer 2
(* MINE *)
apply (simp only: FUN_REL.simps)
prefer 2
(* APPLY_RSP *)
apply (rule_tac APPLY_RSP[of "op \<approx> ===> op =" "REP_fset ---> id" "ABS_fset ---> id" "op =" "id" "id" "Ball (Respects op \<approx>)" "Ball (Respects op \<approx>)"])
prefer 2
apply (rule IDENTITY_QUOTIENT)
(* 2: ho_respects *)
prefer 3
(* ABS_REP_RSP *)
apply (rule REP_ABS_RSP(1)[of "op \<approx> ===> op =" "REP_fset ---> id" "ABS_fset ---> id"])
prefer 2
(* LAMBDA_RSP *)
apply (simp only: FUN_REL.simps)
apply (rule allI)
apply (rule allI)
apply (rule impI)
(* MK_COMB_TAC *)
apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1 *})
(* MK_COMB_TAC *)
apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1 *})
(* REFL_TAC *)
apply (simp)
(* APPLY_RSP *)
apply (rule APPLY_RSP[of "op \<approx>" "ABS_fset" "REP_fset" "op =" "id" "id"])
apply (rule QUOTIENT_fset)
apply (rule IDENTITY_QUOTIENT)
apply (rule REP_ABS_RSP(1)[of "op \<approx> ===> op =" "REP_fset ---> id" "ABS_fset ---> id"])
prefer 2
(* MINE *)
apply (simp only: FUN_REL.simps)
prefer 2
apply (rule REP_ABS_RSP(1)[of "op \<approx>" "ABS_fset" "REP_fset"])
apply (rule QUOTIENT_fset)
(* FIRST_ASSUM MATCH_ACCEPT_TAC *)
apply (assumption)
prefer 2
(* MK_COMB_TAC *)
apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1 *})
(* REFL_TAC *)
apply (simp)
(* W(C (curry op THEN) (G... *)
apply (rule ext)
(* APPLY_RSP *)
apply (rule APPLY_RSP[of "op \<approx>" "ABS_fset" "REP_fset" "op =" "id" "id"])
apply (rule QUOTIENT_fset)
apply (rule IDENTITY_QUOTIENT)
apply (rule REP_ABS_RSP(1)[of "op \<approx> ===> op =" "REP_fset ---> id" "ABS_fset ---> id"])
prefer 2
apply (simp only: FUN_REL.simps)
prefer 2
apply (rule REP_ABS_RSP(1)[of "op \<approx>" "ABS_fset" "REP_fset"])
apply (rule QUOTIENT_fset)
(* APPLY_RSP *)
apply (rule_tac ?f="\<lambda>x. h # x" and ?g="\<lambda>x. h # x" in APPLY_RSP[of "op \<approx>" "ABS_fset" "REP_fset" "op \<approx>" "ABS_fset" "REP_fset"] )
apply (rule QUOTIENT_fset)
apply (rule QUOTIENT_fset)
apply (rule_tac ?f="op #" and ?g="op #" in APPLY_RSP[of "op =" "id" "id" "op \<approx> ===> op \<approx>" "REP_fset ---> ABS_fset" "ABS_fset ---> REP_fset"])
apply (rule IDENTITY_QUOTIENT)
(* CONS respects *)
prefer 2
apply (simp add: FUN_REL.simps)
apply (rule allI)
apply (rule allI)
apply (rule allI)
apply (rule impI)
apply (rule cons_preserves)
apply (assumption)
prefer 2
apply (simp)
sorry
thm list.recs(2)
ML {* val card1_suc_f = Thm.freezeT (atomize_thm @{thm card1_suc}) *}
prove card1_suc_r: {*
Logic.mk_implies
((prop_of card1_suc_f),
(regularise (prop_of card1_suc_f) @{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 {* @{thm card1_suc_r} OF [card1_suc_f] *}
ML {* val li = Thm.freezeT (atomize_thm @{thm fold1.simps(2)}) *}
prove fold1_def_2_r: {*
Logic.mk_implies
((prop_of li),
(regularise (prop_of li) @{typ "'a List.list"} @{term "op \<approx>"} @{context})) *}
apply (simp add: equiv_res_forall[OF equiv_list_eq])
done
ML {* @{thm fold1_def_2_r} OF [li] *}
ML {*
fun lift_theorem_fset_aux thm lthy =
let
val ((_, [novars]), lthy2) = Variable.import true [thm] lthy;
val goal = build_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
*}
ML {* lift_theorem_fset_aux @{thm m1} @{context} *}
ML {*
fun lift_theorem_fset name thm lthy =
let
val lifted_thm = lift_theorem_fset_aux thm lthy;
val (_, lthy2) = note (name, lifted_thm) lthy;
in
lthy2
end;
*}
local_setup {* lift_theorem_fset @{binding "m1_lift"} @{thm m1} *}
local_setup {* lift_theorem_fset @{binding "leqi4_lift"} @{thm list_eq.intros(4)} *}
local_setup {* lift_theorem_fset @{binding "leqi5_lift"} @{thm list_eq.intros(5)} *}
local_setup {* lift_theorem_fset @{binding "m2_lift"} @{thm m2} *}
thm m1_lift
thm leqi4_lift
thm leqi5_lift
thm m2_lift
ML {* @{thm card1_suc_r} OF [card1_suc_f] *}
(*ML {* Toplevel.program (fn () => lift_theorem_fset @{binding "card_suc"}
(@{thm card1_suc_r} OF [card1_suc_f]) @{context}) *}*)
(*local_setup {* lift_theorem_fset @{binding "card_suc"} @{thm card1_suc} *}*)
thm leqi4_lift
ML {*
val (nam, typ) = hd (Term.add_vars (prop_of @{thm leqi4_lift}) [])
val (_, l) = dest_Type typ
val t = Type ("QuotMain.fset", l)
val v = Var (nam, t)
val cv = cterm_of @{theory} ((term_of @{cpat "REP_fset"}) $ v)
*}
ML {*
Toplevel.program (fn () =>
MetaSimplifier.rewrite_rule @{thms QUOT_TYPE_I_fset.thm10} (
Drule.instantiate' [] [NONE, SOME (cv)] @{thm leqi4_lift}
)
)
*}
lemma "(Ball (Respects ((op \<approx>) ===> (op =)))
(((REP_fset ---> id) ---> id)
(((ABS_fset ---> id) ---> id)
(\<lambda>P.
(ABS_fset ---> id) ((REP_fset ---> id) P)
(REP_fset (ABS_fset [])) \<and>
Ball (Respects (op \<approx>))
((ABS_fset ---> id)
((REP_fset ---> id)
(\<lambda>t.
((ABS_fset ---> id)
((REP_fset ---> id) P)
(REP_fset (ABS_fset t))) \<longrightarrow>
(!h.
(ABS_fset ---> id)
((REP_fset ---> id) P)
(REP_fset
(ABS_fset
(h #
REP_fset
(ABS_fset t)))))))) \<longrightarrow>
Ball (Respects (op \<approx>))
((ABS_fset ---> id)
((REP_fset ---> id)
(\<lambda>l.
(ABS_fset ---> id)
((REP_fset ---> id) P)
(REP_fset (ABS_fset l)))))))))
= Ball (Respects ((op \<approx>) ===> (op =)))
(\<lambda>P. ((P []) \<and> (Ball (Respects (op \<approx>)) (\<lambda>t. P t \<longrightarrow> (\<forall>h. (P (h # t)))))) \<longrightarrow>
(Ball (Respects (op \<approx>)) (\<lambda>l. P l)))"
thm APPLY_RSP[of "op \<approx> ===> (op = ===> op =)" "REP_fset ---> (id ---> id)" "ABS_fset ---> (id ---> id)" "op =" "id" "id"]
proof -
note APPLY_RSP_I = APPLY_RSP[of "op \<approx> ===> (op = ===> op =)" "REP_fset ---> (id ---> id)" "ABS_fset ---> (id ---> id)" "op =" "id" "id"]
show ?thesis apply -
ML_prf {*
val gc = Subgoal.focus @{context} 1 (Isar.goal ())
|> fst
|> #concl
val tc = cterm_of @{theory} (concl_of ( @{thm "APPLY_RSP" }))
val (_, tc') = Thm.dest_comb tc
val (_, gc') = Thm.dest_comb gc
*}
ML_prf {*
(gc', tc')
*}
ML_prf {* Pattern.first_order_match *}
ML_prf {* Thm.match (@{cpat "?P::?'a"}, @{cterm "1::nat"}) *}
ML_prf {* Pattern.match @{theory} (term_of @{cpat "?P::nat"}, term_of @{cterm "1::nat"}) (Vartab.empty, Vartab.empty) *}
ML_prf {* val (op1, (l1, r1)) = dest_cbinop tc' *}
ML_prf {* val (op2, (l2, r2)) = dest_cbinop gc' *}
ML_prf {* val mo = Thm.match (op1, op2) *}
ML_prf {* val t1 = Drule.instantiate mo @{thm "APPLY_RSP" } *}
ML_prf {* val tc = cterm_of @{theory} (concl_of t1) *}
ML_prf {* val (_, tc') = Thm.dest_comb tc *}
ML_prf {* val (op1, (l1, r1)) = dest_cbinop tc' *}
ML_prf {* val (mlty, mlt) = Thm.match (l1, l2) *}
ML_prf {* val t2 = Drule.instantiate (mlty, []) t1 *}
ML_prf {* val tc = cterm_of @{theory} (concl_of t2) *}
ML_prf {* val (_, tc') = Thm.dest_comb tc *}
ML_prf {* val (op1, (l1, r1)) = dest_cbinop tc' *}
ML_prf {* val mr = Thm.match (r1, r2) *}
ML_prf {* val t3 = Drule.instantiate ml t2 *}
ML_prf {* val tc = cterm_of @{theory} (concl_of t3) *}
ML_prf {* val (_, tc') = Thm.dest_comb tc *}
ML_prf {* mtyl; mtyr *}
ML_prf {* val ol1 = Thm.capply op1 l1 *}
ML_prf {* val ol2 = Thm.capply op2 l2 *}
ML_prf {* (ol1, ol2); Thm.match (ol1, ol2) *}
ML_prf {* val w1 = Thm.capply ol1 r1 *}
ML_prf {* val w2 = Thm.capply ol2 r2 *}
.
(*ML_prf {* (w1, w2); Thm.match (w1, w2) *}*)
ML_prf {*
(tc', gc')
*}
thm APPLY_RSP
thm APPLY_RSP[of "op \<approx> ===> (op = ===> op =)"]
term "(op \<approx> ===> op =) ===> op ="
proof -
note APPLY_RSP_I2 = APPLY_RSP[of "(op \<approx> ===> op =) ===> op =" "(ABS_fset ---> id) ---> id" "(REP_fset ---> id) ---> id" "op =" "id" "id" "Ball (Respects op \<approx> ===> op =)" "Ball (Respects op \<approx> ===> op =)"]
show ?thesis apply -
thm APPLY_RSP_I2[of _ "\<lambda>P. (P [] \<and> (\<forall>t\<Colon>'b list\<in>Respects op \<approx>. P t \<longrightarrow> (\<forall>h\<Colon>'b. P (h # t))) \<longrightarrow>
(\<forall>l\<Colon>'b list\<in>Respects op \<approx>. P l))"]
proof -
note APPLY_RSP_I3=APPLY_RSP_I2[of _ "\<lambda>P. (P [] \<and> (\<forall>t\<Colon>'b list\<in>Respects op \<approx>. P t \<longrightarrow> (\<forall>h\<Colon>'b. P (h # t))) \<longrightarrow>
(\<forall>l\<Colon>'b list\<in>Respects op \<approx>. P l))"]
show ?thesis apply -
term "(REP_fset ---> id ---> id
(ABS_fset ---> id ---> id
(\<lambda>P\<Colon>'a list \<Rightarrow> bool.
ABS_fset ---> id (REP_fset ---> id P)
(REP_fset (ABS_fset [])) \<and>
Ball (Respects op \<approx>)
(ABS_fset ---> id
(REP_fset ---> id
(\<lambda>t\<Colon>'a list.
ABS_fset ---> id (REP_fset ---> id P)
(REP_fset (ABS_fset t)) \<longrightarrow>
(\<forall>h\<Colon>'a.
ABS_fset ---> id (REP_fset ---> id P)
(REP_fset
(ABS_fset
(h # REP_fset (ABS_fset t)))))))) \<longrightarrow>
Ball (Respects op \<approx>)
(ABS_fset ---> id
(REP_fset ---> id
(\<lambda>l\<Colon>'a list.
ABS_fset ---> id (REP_fset ---> id P)
(REP_fset (ABS_fset l))))))))"
apply (rule APPLY_RSP_I3)
term "Ball (Respects op \<approx> ===> op =)"
thm APPLY_RSP_I [of _ "Ball (Respects op \<approx> ===> op =)"]
thm APPLY_RSP
.
apply (tactic {* Cong_Tac.cong_tac @{thm APPLY_RSP_I} 1 *} )
apply (tactic {* match_tac @{thms APPLY_RSP_I} 1 *})
.
apply (rule APPLY_RSP[of "op \<approx> ===> (op = ===> op =)" "REP_fset ---> (id ---> id)" "ABS_fset ---> (id ---> id)" "op =" "id" "id"])
apply (rule APPLY_RSP[of "op \<approx> ===> (op = ===> op =)" _ _ "op ="])
term "(\<forall>P. (((P []) \<and> (\<forall>t. (P t \<longrightarrow> (\<forall>h. P (h # t))))) \<longrightarrow> (\<forall>l. (P l))))"
thm LAMBDA_PRS1[symmetric]
(*apply (simp only:LAMBDA_PRS1[symmetric] FUN_QUOTIENT IDENTITY_QUOTIENT QUOT_TYPE_I_fset.QUOTIENT)*)
apply (unfold Ball_def)
apply (simp only: IN_RESPECTS)
apply (simp only:list_eq_refl)
apply (unfold id_def)
(*apply (simp only: FUN_MAP_I)*)
apply (simp)
apply (simp only: QUOT_TYPE_I_fset.thm10)
..
apply (simp add:IN_RESPECTS)
apply (simp add: QUOT_TYPE_I_fset.R_trans2)
apply (rule ext)
apply (simp add:QUOT_TYPE_I_fset.REP_ABS_rsp)
apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1 *} )
apply (simp add:cons_preserves)
(*prove aaa: {* (Thm.term_of cgoal2) *}
apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} )
apply (atomize(full))
apply (tactic {* transconv_fset_tac' @{context} 1 *})
done*)
(*
datatype obj1 =
OVAR1 "string"
| OBJ1 "(string * (string \<Rightarrow> obj1)) list"
| INVOKE1 "obj1 \<Rightarrow> string"
| UPDATE1 "obj1 \<Rightarrow> string \<Rightarrow> (string \<Rightarrow> obj1)"
*)
end