diff -r 1d08221f48c4 -r e51af8bace65 QuotMain.thy --- a/QuotMain.thy Mon Sep 28 15:37:38 2009 +0200 +++ b/QuotMain.thy Mon Sep 28 18:59:04 2009 +0200 @@ -561,7 +561,7 @@ | "xs \ ys \ a#xs \ a#ys" | "\xs1 \ xs2; xs2 \ xs3\ \ xs1 \ xs3" -lemma list_eq_sym: +lemma list_eq_refl: shows "xs \ xs" apply (induct xs) apply (auto intro: list_eq.intros) @@ -570,7 +570,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_sym) + apply(auto intro: list_eq.intros list_eq_refl) done local_setup {* @@ -732,7 +732,7 @@ 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 @@ -806,7 +806,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_sym) +apply(rule list_eq_refl) done lemma append_respects_fst: @@ -815,7 +815,7 @@ 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: @@ -833,17 +833,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_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 @@ -862,40 +862,77 @@ 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)) = - let - val [(fresh_s, _)] = Variable.variant_frees @{context} [] [(s, ())]; - val newv = Free (fresh_s, t); - val str = subst_bound (newv, tr); - val rec_term = build_aux str; - val bound_term = lambda newv rec_term - in - bound_term - end - | build_aux (f $ a) = + 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 @{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)))) - else list_comb ((build_aux f), (map build_aux args))) + 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) 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} *} @@ -984,11 +1021,13 @@ shows "(a \ b) \ (Trueprop a \ 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_sym}, +(* rtac @{thm trueprop_cong},*) + rtac @{thm list_eq_refl}, rtac @{thm cons_preserves}, rtac @{thm mem_respects}, rtac @{thm card1_rsp}, @@ -996,14 +1035,14 @@ 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) *} @@ -1011,9 +1050,33 @@ (*notation ( output) "prop" ("#_" [1000] 1000) *) notation ( output) "Trueprop" ("#_" [1000] 1000) +lemma atomize_eqv [atomize]: "(Trueprop A \ Trueprop B) \ (A \ B)" + (is "?rhs \ ?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 *)