--- 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 \<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)
@@ -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 \<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_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 \<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 *)