nominal2: comparison QuotMain.thy

equal deleted inserted replaced

-:d98224cafb86
+:e801b929216b
 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
 val [x, c] = [("x", ty), ("c", ty --> @{typ bool})]
 |> Variable.variant_frees lthy [rel]
 |> map Free
 in
 lambda c
 (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
 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)
 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 *}
 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
 (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 {*
 *}
 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))
 fun get_fun_aux s fs_tys =
 let
 (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))
+fun get_const absF = (Const ("QuotMain.ABS_" ^ qty_name, rty --> qty), (rty, qty))
-| get_const rep = (Const ("QuotMain.REP_" ^ qty_name, qty --> rty), (qty, rty))
+| 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 {*
 fun get_const_def nconst oconst rty qty lthy =
 let
 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 rep_fns = map (fst o get_fun repF rty qty lthy) arg_tys
-val abs_fn  = (fst o get_fun abs rty qty lthy) res_ty
+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
 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
 | "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:
+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_refl)
+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
 *}
 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)
+apply (metis QUOT_TYPE_I_fset.R_trans QuotMain.card1_cons list_eq_sym mem_cons)
 done
 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))
 text {*
 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
 This function is needed to rewrite the right-hand
 side to the left-hand side.
 *}
 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)
+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_refl)
+apply(simp add: list_eq_sym)
 done
 lemma yyy:
 shows "
 (
 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(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
 shows "
 (UNION EMPTY s = s) &
 apply (simp add: 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"},
 @{const_name "card1"}]
 *}
 ML {*
-fun build_goal ctxt thm constructors lifted_type mk_rep_abs =
+fun build_goal ctxt thm constructors qty mk_rep_abs =
 let
-fun is_constructor (Const (x, _)) = member (op =) constructors x
+fun is_const (Const (x, t)) = x mem constructors
-| is_constructor _ = false;
+| 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
+if type_of t = qty then mk_rep_abs t else t
-end;
+end
+handle TYPE _ => t
-fun build_aux ctxt1 tm =
-let
+fun build_aux (Abs (s, t, tr)) = (Abs (s, t, build_aux tr))
-val (head, args) = Term.strip_comb tm;
+| build_aux (f $ a) =
-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 (f, args) = strip_comb (f $ a)
 val _ = writeln (Syntax.string_of_term ctxt f)
 in
-if is_const f then
+(if is_const f then maybe_mk_rep_abs (list_comb (f, (map maybe_mk_rep_abs (map build_aux args))))
-maybe_mk_rep_abs
+else list_comb ((build_aux f), (map build_aux args)))
-(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)
 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))
+val concl2 = prop_of thm
 in
-Logic.mk_equals (build_aux ctxt concl2, concl2)
+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 =
 let
 val (t2, rhs) = Thm.dest_comb t;
 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
 *}
 Drule.instantiate' [SOME cT,SOME cT,SOME @{ctyp bool}] [NONE,NONE,NONE,NONE,SOME (@{cpat "op ="})] @{thm arg_cong2}
 )
 *}
 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}
+Drule.instantiate' [SOME clT,SOME cmT,SOME crT] [NONE,NONE,NONE,NONE,SOME bop] @{thm arg_cong2}
 end
 *}
 ML {*
-fun split_arg_conv t =
+fun foo_tac n thm =
-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}
-end
-*}
-ML {*
-fun split_binop_tac n thm =
 let
 val concl = Thm.cprem_of thm n;
 val (_, cconcl) = Thm.dest_comb concl;
-val rewr = split_binop_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
 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;
-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 *)
 lemma trueprop_cong:
 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 trueprop_cong},
-rtac @{thm list_eq_refl},
+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,
+foo_tac,
-rtac @{thm ext},
-rtac @{thm eq_reflection},
 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)
 *}
 (*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 *})
 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 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)
 *}
 prove {* Thm.term_of cgoal2 *}
 apply (tactic {* foo_tac' @{context} 1 *})
 sorry
 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)
 *}
 prove {* Thm.term_of cgoal2 *}
 apply (tactic {* foo_tac' @{context} 1 *})
 done
 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)
 val cgoal3 = Thm.rhs_of (MetaSimplifier.rewrite true @{thms QUOT_TYPE_I_fset.thm10} cgoal2)
 *}
 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'} *}
+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 =
 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 *} )
 apply (tactic {* foo_tac' @{context} 1 *})
 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}))
 *}
 ML {*
 build_goal @{context} 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)
-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 {*
 val m1_novars = snd(no_vars ((Context.Theory @{theory}),@{thm card1_suc}))
 *}
 ML {*
 val goal = build_goal @{context} m1_novars consts @{typ "'a list"} mk_rep_abs
 *}
 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 *})
 (*
 datatype obj1 =
 OVAR1 "string"

changeset 46	e801b929216b
parent 45	d98224cafb86
child 47	6a51704204e5