--- a/QuotMain.thy Mon Sep 28 19:15:19 2009 +0200
+++ b/QuotMain.thy Mon Sep 28 19:22:28 2009 +0200
@@ -77,8 +77,8 @@
done
lemma R_trans:
- assumes ab: "R a b"
- and bc: "R b c"
+ 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
@@ -88,15 +88,15 @@
qed
lemma R_sym:
- assumes ab: "R a b"
+ 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"
+lemma R_trans2:
+ assumes ac: "R a c"
and bd: "R b d"
shows "R a b = R c d"
proof
@@ -151,18 +151,18 @@
|> map Free
in
lambda c
- (HOLogic.exists_const ty $
+ (HOLogic.exists_const ty $
lambda x (HOLogic.mk_eq (c, (rel $ x))))
end
(* makes the new type definitions and proves non-emptyness*)
fun typedef_make (qty_name, rel, ty) lthy =
-let
+let
val typedef_tac =
EVERY1 [rewrite_goal_tac @{thms mem_def},
- rtac @{thm exI},
- rtac @{thm exI},
+ rtac @{thm exI},
+ rtac @{thm exI},
rtac @{thm refl}]
in
LocalTheory.theory_result
@@ -217,7 +217,7 @@
rtac @{thm QUOT_TYPE.QUOTIENT},
rtac quot_type_thm]
in
- Goal.prove lthy [] [] goal
+ Goal.prove lthy [] [] goal
(K typedef_quotient_thm_tac)
end
*}
@@ -324,8 +324,8 @@
| app "trm" "trm"
| lam "nat" "trm"
-axiomatization
- RR :: "trm \<Rightarrow> trm \<Rightarrow> bool"
+axiomatization
+ RR :: "trm \<Rightarrow> trm \<Rightarrow> bool"
where
r_eq: "EQUIV RR"
@@ -397,8 +397,8 @@
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))
+ val lookup = Symtab.lookup o Data.get
+ fun update k v = Data.map (Symtab.update (k, v))
end
*}
@@ -412,9 +412,9 @@
ML {* lookup (Context.Proof @{context}) @{type_name list} *}
ML {*
-datatype abs_or_rep = abs | rep
+datatype flag = absF | repF
-fun get_fun abs_or_rep rty qty lthy ty =
+fun get_fun flag rty qty lthy ty =
let
val qty_name = Long_Name.base_name (fst (dest_Type qty))
@@ -431,30 +431,36 @@
| 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))
+ 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 ("x", ty, Bound 0)
in
if ty = qty
- then (get_const abs_or_rep)
+ then (get_const flag)
else (case ty of
TFree _ => (mk_identity ty, (ty, ty))
| Type (_, []) => (mk_identity ty, (ty, ty))
- | Type (s, tys) => get_fun_aux s (map (get_fun abs_or_rep rty qty lthy) tys)
+ | Type (s, tys) => get_fun_aux s (map (get_fun flag rty qty lthy) tys)
| _ => raise ERROR ("no type variables")
)
end
*}
ML {*
- get_fun rep @{typ t} @{typ qt} @{context} @{typ "t * nat"}
+ get_fun repF @{typ t} @{typ qt} @{context} @{typ "t * nat"}
|> fst
|> Syntax.string_of_term @{context}
|> writeln
*}
+ML {*
+ get_fun absF @{typ t} @{typ qt} @{context} @{typ "t * nat"}
+ |> fst
+ |> Syntax.string_of_term @{context}
+ |> writeln
+*}
text {* produces the definition for a lifted constant *}
ML {*
@@ -467,8 +473,8 @@
|> 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
+ 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)
@@ -480,7 +486,7 @@
ML {*
fun exchange_ty rty qty ty =
- if ty = rty
+ if ty = rty
then qty
else
(case ty of
@@ -559,7 +565,7 @@
| "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:
+lemma list_eq_sym:
shows "xs \<approx> xs"
apply (induct xs)
apply (auto intro: list_eq.intros)
@@ -568,7 +574,7 @@
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)
+ apply(auto intro: list_eq.intros list_eq_sym)
done
local_setup {*
@@ -674,7 +680,7 @@
fixes xs :: "'a list"
assumes a : "x memb xs"
shows "x # xs \<approx> xs"
- using a
+ using a
apply (induct xs)
apply (auto intro: list_eq.intros)
done
@@ -684,10 +690,10 @@
fixes n :: "nat"
assumes c: "card1 xs = Suc n"
shows "\<exists>a ys. ~(a memb ys) \<and> xs \<approx> (a # ys)"
- using c
+ 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)
+apply (metis QUOT_TYPE_I_fset.R_trans QuotMain.card1_cons list_eq_sym mem_cons)
done
lemma cons_preserves:
@@ -698,13 +704,13 @@
text {*
- Unlam_def converts a definition given as
+ Unlam_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
+ 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.
@@ -767,7 +773,7 @@
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)
+apply(rule list_eq_sym)
done
lemma append_respects_fst:
@@ -776,7 +782,7 @@
using a
apply(induct)
apply(auto intro: list_eq.intros)
- apply(simp add: list_eq_refl)
+ apply(simp add: list_eq_sym)
done
lemma yyy:
@@ -794,17 +800,17 @@
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(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_refl)
+ 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_refl)
+ apply(rule list_eq_sym)
done
lemma
@@ -817,89 +823,51 @@
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"},
+ val consts = [@{const_name "Nil"}, @{const_name "append"},
+ @{const_name "Cons"}, @{const_name "membship"},
@{const_name "card1"}]
*}
ML {*
-fun build_goal ctxt thm constructors lifted_type mk_rep_abs =
- let
- fun is_constructor (Const (x, _)) = member (op =) constructors x
- | is_constructor _ = false;
-
+fun build_goal ctxt thm constructors qty 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 ctxt t)
- in
- if type_of t = lifted_type then mk_rep_abs t else t
- end;
-
- 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) =>
- 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
- | _ =>
- if is_constructor head then
- maybe_mk_rep_abs (list_comb (head, map maybe_mk_rep_abs args'))
- else list_comb (head, args'))
- end;
-
- val concl2 = Thm.prop_of thm;
- in
- Logic.mk_equals (build_aux ctxt concl2, concl2)
- end
-*}
-
-ML {*
-fun build_goal' ctxt thm constructors lifted_type mk_rep_abs =
- let
- fun is_const (Const (x, t)) = member (op =) constructors x
- | is_const _ = false
-
- fun maybe_mk_rep_abs t =
- let
- val _ = writeln ("Maybe: " ^ Syntax.string_of_term ctxt t)
- in
- if type_of t = lifted_type then mk_rep_abs t else t
- end
-(* handle TYPE _ => t*)
- fun build_aux ctxt1 (Abs (x, T, t)) =
- 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
- | build_aux ctxt1 (f $ a) =
+ let
+ val _ = writeln ("Maybe: " ^ Syntax.string_of_term ctxt t)
+ in
+ if type_of t = qty then mk_rep_abs t else t
+ end
+ handle TYPE _ => t
+
+ 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 ctxt f)
in
- if is_const f then
- maybe_mk_rep_abs
- (list_comb (f, map maybe_mk_rep_abs (map (build_aux ctxt1) args)))
- else list_comb (build_aux ctxt1 f, map (build_aux ctxt1) args)
+ (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 =
+ | build_aux x =
if is_const x then maybe_mk_rep_abs x else x
-
- val concl2 = term_of (#prop (crep_thm thm))
- in
- Logic.mk_equals (build_aux ctxt concl2, concl2)
+
+ val concl2 = prop_of thm
+in
+ Logic.mk_equals ((build_aux concl2), concl2)
end *}
+thm EMPTY_def IN_def UNION_def
+
+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 = map (fn t => symmetric (unlam_def @{context} t)) fset_defs *}
+ML {* val fset_defs_sym = [emptyt, in_t, uniont, cardt, insertt] *}
ML {*
fun dest_cbinop t =
@@ -915,7 +883,7 @@
fun dest_ceq t =
let
val (bop, pair) = dest_cbinop t;
- val (bop_s, _) = Term.dest_Const (Thm.term_of bop);
+ 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
@@ -932,46 +900,25 @@
*}
ML {*
- fun split_binop_conv t =
+ 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 split_arg_conv t =
- let
- val (lhs, rhs) = dest_ceq t;
- val (lop, larg) = Thm.dest_comb lhs;
- val [caT, crT] = lop |> Thm.ctyp_of_term |> Thm.dest_ctyp;
- in
- Drule.instantiate' [SOME caT, SOME crT] [NONE, NONE, SOME lop] @{thm arg_cong}
+ Drule.instantiate' [SOME clT,SOME cmT,SOME crT] [NONE,NONE,NONE,NONE,SOME bop] @{thm arg_cong2}
end
*}
ML {*
- fun split_binop_tac n thm =
+ fun foo_tac n thm =
let
val concl = Thm.cprem_of thm n;
val (_, cconcl) = Thm.dest_comb concl;
- val rewr = split_binop_conv cconcl;
- in
- rtac rewr n thm
- end
- handle CTERM _ => Seq.empty
-*}
-
-ML {*
- fun split_arg_tac n thm =
- let
- val concl = Thm.cprem_of thm n;
- val (_, cconcl) = Thm.dest_comb concl;
- val rewr = split_arg_conv cconcl;
+ 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
@@ -984,27 +931,22 @@
shows "(a \<equiv> b) \<Longrightarrow> (Trueprop a \<equiv> Trueprop b)"
by auto
-
-thm QUOT_TYPE_I_fset.R_trans2
ML {*
fun foo_tac' ctxt =
REPEAT_ALL_NEW (FIRST' [
-(* rtac @{thm trueprop_cong},*)
- rtac @{thm list_eq_refl},
+ rtac @{thm trueprop_cong},
+ rtac @{thm list_eq_sym},
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})),
- DatatypeAux.cong_tac,
- rtac @{thm ext},
- rtac @{thm eq_reflection},
+ foo_tac,
CHANGED o (ObjectLogic.full_atomize_tac)
])
*}
ML {*
- val m1_novars = snd(no_vars ((Context.Theory @{theory}), @{thm m1}))
+ val m1_novars = snd(no_vars ((Context.Theory @{theory}),@{thm m1}))
val goal = build_goal @{context} 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)
@@ -1013,26 +955,6 @@
(*notation ( output) "prop" ("#_" [1000] 1000) *)
notation ( output) "Trueprop" ("#_" [1000] 1000)
-lemma atomize_eqv [atomize]: "(Trueprop A \<equiv> Trueprop B) \<equiv> (A \<equiv> B)"
- (is "?rhs \<equiv> ?lhs")
-proof
- assume "PROP ?lhs" then show "PROP ?rhs" by unfold
-next
- assume *: "PROP ?rhs"
- have "A = B"
- proof (cases A)
- case True
- with * have B by unfold
- with `A` show ?thesis by simp
- next
- case False
- with * have "~ B" by auto
- with `~ A` show ?thesis by simp
- qed
- then show "PROP ?lhs" by (rule eq_reflection)
-qed
-
-
prove {* (Thm.term_of cgoal2) *}
apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} )
apply (tactic {* foo_tac' @{context} 1 *})
@@ -1040,7 +962,7 @@
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 m1_novars = snd(no_vars ((Context.Theory @{theory}),@{thm length_append}))
val goal = build_goal @{context} 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)
@@ -1052,7 +974,7 @@
thm m2
ML {*
- val m1_novars = snd(no_vars ((Context.Theory @{theory}), @{thm m2}))
+ val m1_novars = snd(no_vars ((Context.Theory @{theory}),@{thm m2}))
val goal = build_goal @{context} 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)
@@ -1064,7 +986,7 @@
thm list_eq.intros(4)
ML {*
- val m1_novars = snd(no_vars ((Context.Theory @{theory}), @{thm list_eq.intros(4)}))
+ 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"} mk_rep_abs
val cgoal = cterm_of @{theory} goal
val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false fset_defs_sym cgoal)
@@ -1090,19 +1012,33 @@
thm QUOT_TYPE_I_fset.REPS_same
ML {* 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 list_eq.intros(5)
ML {*
- val m1_novars = snd(no_vars ((Context.Theory @{theory}), @{thm list_eq.intros(5)}))
+ 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"} mk_rep_abs
*}
ML {*
- val cgoal =
+ val cgoal =
Toplevel.program (fn () =>
cterm_of @{theory} goal
)
*}
ML {*
- val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite true fset_defs_sym cgoal)
+ val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false fset_defs_sym cgoal)
*}
prove {* Thm.term_of cgoal2 *}
apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} )
@@ -1110,6 +1046,7 @@
done
thm list.induct
+ML {* 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}))
@@ -1122,94 +1059,18 @@
*}
ML {*
val cgoal = cterm_of @{theory} goal
+ val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false fset_defs_sym cgoal)
*}
-ML {*
- val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite true fset_defs_sym cgoal)
-*}
-
+ML fset_defs_sym
prove {* (Thm.term_of cgoal2) *}
apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} )
- apply (tactic {* foo_tac' @{context} 1 *})
+ apply (atomize(full))
+ apply (rule_tac trueprop_cong)
+ apply (atomize(full))
+ apply (tactic {* foo_tac' @{context} 1 *})
+ apply (rule_tac f = "P" in arg_cong)
sorry
-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"} mk_rep_abs;
- val cgoal = cterm_of @{theory} goal;
- val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite true fset_defs_sym cgoal);
- val tac = (LocalDefs.unfold_tac @{context} fset_defs) THEN (foo_tac' @{context}) 1;
- 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_thm (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 Drule.instantiate'
-text {*
- We lost the schematic variable again :(.
- Another variable export will still be necessary...
-*}
-ML {*
- Toplevel.program (fn () =>
- MetaSimplifier.rewrite_rule @{thms QUOT_TYPE_I_fset.thm10} (
- Drule.instantiate' [] [NONE, NONE, SOME (@{cpat "REP_fset x"})] @{thm m2_lift}
- )
- )
-*}
-
-thm leqi4_lift
-ML {*
- val (nam, typ) = (hd (Term.add_vars (term_of (#prop (crep_thm @{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 {*
-term_of (#prop (crep_thm @{thm sym}))
-*}
-
-ML {*
- Toplevel.program (fn () =>
- MetaSimplifier.rewrite_rule @{thms QUOT_TYPE_I_fset.thm10} (
- Drule.instantiate' [] [NONE, SOME (cv)] @{thm leqi4_lift}
- )
- )
-*}
-
-
-
-
-
-ML {* MRS *}
thm card1_suc
ML {*
@@ -1220,13 +1081,11 @@
*}
ML {*
val cgoal = cterm_of @{theory} goal
- val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite true fset_defs_sym cgoal)
+ val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false fset_defs_sym cgoal)
*}
-ML {* @{term "\<exists>x. P x"} *}
-ML {* Thm.bicompose *}
prove {* (Thm.term_of cgoal2) *}
apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} )
- apply (tactic {* foo_tac' @{context} 1 *})
+
(*