nominal2: comparison QuotMain.thy

equal deleted inserted replaced

-:1d08221f48c4
+:e51af8bace65
 | "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:
+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_sym)
+apply(auto intro: list_eq.intros list_eq_refl)
 done
 local_setup {*
 typedef_main (@{binding "fset"}, @{term "list_eq"}, @{typ "'a list"}, @{thm "equiv_list_eq"}) #> snd
 *}
 from a2 show "\<exists>aa ys. \<not> aa memb ys \<and> a # xs \<approx> aa # ys"
 apply -
 apply (rule_tac x = "a" in exI)
 apply (rule_tac x = "xs" in exI)
 apply (simp)
-apply (rule list_eq_sym)
+apply (rule list_eq_refl)
 done
 qed
 qed
 lemma cons_preserves:
 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)
+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_sym)
+apply(simp add: list_eq_refl)
 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_sym)
+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_sym)
+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_sym)
+apply(rule list_eq_refl)
 done
 lemma
 shows "
 (UNION EMPTY s = s) &
 *}
 ML lambda
 ML {*
-fun build_goal thm constructors lifted_type mk_rep_abs =
+fun build_goal ctxt thm constructors lifted_type mk_rep_abs =
 let
-fun is_const (Const (x, t)) = x mem constructors
+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 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 @{context} t)
+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 (Abs (s, t, tr)) =
+fun build_aux ctxt1 (Abs (x, T, t)) =
 let
-val [(fresh_s, _)] = Variable.variant_frees @{context} [] [(s, ())];
+val ([x'], ctxt2) = Variable.variant_fixes [x] ctxt1;
-val newv = Free (fresh_s, t);
+val v = Free (x', T);
-val str = subst_bound (newv, tr);
+val t' = subst_bound (v, t);
-val rec_term = build_aux str;
+val rec_term = build_aux ctxt2 t';
-val bound_term = lambda newv rec_term
+in Term.lambda_name (x, v) rec_term end
-in
+| build_aux ctxt1 (f $ a) =
-bound_term
-end
-| build_aux (f $ a) =
 let
 val (f, args) = strip_comb (f $ a)
-val _ = writeln (Syntax.string_of_term @{context} f)
+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 args))))
+if is_const f then
-else list_comb ((build_aux f), (map build_aux args)))
+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)
 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 concl2), concl2)
+Logic.mk_equals (build_aux ctxt concl2, concl2)
 end *}
 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 *}
 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_sym},
+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})),
 DatatypeAux.cong_tac,
 rtac @{thm ext},
-(*      rtac @{thm eq_reflection}*)
+rtac @{thm eq_reflection},
 CHANGED o (ObjectLogic.full_atomize_tac)
 ])
 *}
 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 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 (atomize (full))
+apply (rule trueprop_cong)
 apply (tactic {* foo_tac' @{context} 1 *})
+thm eq_reflection
 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}))

changeset 43	e51af8bace65
parent 42	1d08221f48c4
child 44	f078dbf557b7