# HG changeset patch # User Christian Urban # Date 1253890211 -7200 # Node ID cac00e8b972b9149cd45b963202c7a36f759c3dc # Parent 3767a6f3d9ee83378c37dcd5ed887233d3ba5dd5 tuned slightly one proof diff -r 3767a6f3d9ee -r cac00e8b972b QuotMain.thy --- a/QuotMain.thy Fri Sep 25 14:50:35 2009 +0200 +++ b/QuotMain.thy Fri Sep 25 16:50:11 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 @@ -115,24 +115,27 @@ lemma REPS_same: shows "R (REP a) (REP b) \ (a = b)" - apply (rule eq_reflection) -proof - assume as: "R (REP a) (REP b)" - from rep_prop - obtain x y - where eqs: "Rep a = R x" "Rep b = R y" by blast - from eqs have "R (Eps (R x)) (Eps (R y))" using as unfolding REP_def by simp - then have "R x (Eps (R y))" using lem9 by simp - then have "R (Eps (R y)) x" using R_sym by blast - then have "R y x" using lem9 by simp - then have "R x y" using R_sym by blast - then have "ABS x = ABS y" using thm11 by simp - then have "Abs (Rep a) = Abs (Rep b)" using eqs unfolding ABS_def by simp - then show "a = b" using rep_inverse by simp -next - assume ab: "a = b" - have "REFL R" using equiv EQUIV_REFL_SYM_TRANS[of R] by simp - then show "R (REP a) (REP b)" unfolding REFL_def using ab by auto +proof - + have "R (REP a) (REP b) = (a = b)" + proof + assume as: "R (REP a) (REP b)" + from rep_prop + obtain x y + where eqs: "Rep a = R x" "Rep b = R y" by blast + from eqs have "R (Eps (R x)) (Eps (R y))" using as unfolding REP_def by simp + then have "R x (Eps (R y))" using lem9 by simp + then have "R (Eps (R y)) x" using R_sym by blast + then have "R y x" using lem9 by simp + then have "R x y" using R_sym by blast + then have "ABS x = ABS y" using thm11 by simp + then have "Abs (Rep a) = Abs (Rep b)" using eqs unfolding ABS_def by simp + then show "a = b" using rep_inverse by simp + next + assume ab: "a = b" + have "REFL R" using equiv EQUIV_REFL_SYM_TRANS[of R] by simp + then show "R (REP a) (REP b)" unfolding REFL_def using ab by auto + qed + then show "R (REP a) (REP b) \ (a = b)" by simp qed end @@ -156,11 +159,11 @@ ML {* (* 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 @@ -215,7 +218,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 *} @@ -322,8 +325,8 @@ | app "trm" "trm" | lam "nat" "trm" -axiomatization - RR :: "trm \ trm \ bool" +axiomatization + RR :: "trm \ trm \ bool" where r_eq: "EQUIV RR" @@ -676,66 +679,21 @@ fixes xs :: "'a list" assumes a : "x memb xs" shows "x # xs \ xs" - using a apply (induct xs) - apply (simp_all) - apply (meson) - apply (simp_all add: list_eq.intros(4)) - proof - - fix a :: "'a" - fix xs :: "'a list" - assume a1 : "x # xs \ xs" - assume a2 : "x memb xs" - have a3 : "x # a # xs \ a # x # xs" using list_eq.intros(1)[of "x"] by blast - have a4 : "a # x # xs \ a # xs" using a1 list_eq.intros(5)[of "x # xs" "xs"] by simp - then show "x # a # xs \ a # xs" using a3 list_eq.intros(6) by blast - qed + 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 "\a ys. ~(a memb ys) \ xs \ (a # ys)" - using c apply (induct xs) - apply (simp) -(* apply (rule allI)*) - proof - - fix a :: "'a" - fix xs :: "'a list" - fix n :: "nat" - assume a1: "card1 xs = Suc n \ \a ys. \ a memb ys \ xs \ a # ys" - assume a2: "card1 (a # xs) = Suc n" - from a1 a2 show "\aa ys. \ aa memb ys \ a # xs \ aa # ys" - apply - - apply (rule True_or_False [of "a memb xs", THEN disjE]) - apply (simp_all add: card1_cons if_True simp_thms) - proof - - assume a1: "\a ys. \ a memb ys \ xs \ a # ys" - assume a2: "card1 xs = Suc n" - assume a3: "a memb xs" - from a1 obtain b ys where a5: "\ b memb ys \ xs \ b # ys" by blast - from a2 a3 a5 show "\aa ys. \ aa memb ys \ a # xs \ aa # ys" - apply - - apply (rule_tac x = "b" in exI) - apply (rule_tac x = "ys" in exI) - apply (simp_all) - proof - - assume a1: "a memb xs" - assume a2: "\ b memb ys \ xs \ b # ys" - then have a3: "xs \ b # ys" by simp - have "a # xs \ xs" using a1 mem_cons[of "a" "xs"] by simp - then show "a # xs \ b # ys" using a3 list_eq.intros(6) by blast - qed -next - assume a2: "\ a memb xs" - from a2 show "\aa ys. \ aa memb ys \ a # xs \ aa # ys" - apply - - apply (rule_tac x = "a" in exI) - apply (rule_tac x = "xs" in exI) - apply (simp) - apply (rule list_eq_sym) - done - qed -qed + 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_sym mem_cons) +done lemma cons_preserves: fixes z @@ -859,8 +817,6 @@ val consts = [@{const_name "Nil"}, @{const_name "append"}, @{const_name "Cons"}, @{const_name "membship"}, @{const_name "card1"}] *} -ML lambda - ML {* fun build_goal thm constructors lifted_type mk_rep_abs = let @@ -872,17 +828,8 @@ 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 + 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) @@ -898,8 +845,13 @@ Logic.mk_equals ((build_aux concl2), concl2) end *} +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 = @@ -910,6 +862,7 @@ (bop, (lhs, rhs)) end *} + ML {* fun dest_ceq t = let @@ -919,58 +872,37 @@ if bop_s = "op =" then pair else (raise CTERM ("Not an equality", [t])) end *} + ML Thm.instantiate ML {*@{thm arg_cong2}*} ML {*@{thm arg_cong2[of _ _ _ _ "op ="]} *} ML {* val cT = @{cpat "op ="} |> Thm.ctyp_of_term |> Thm.dest_ctyp |> hd *} ML {* Toplevel.program (fn () => - Drule.instantiate' [SOME cT, SOME cT, SOME @{ctyp bool}] [NONE, NONE, NONE, NONE, SOME (@{cpat "op ="})] @{thm arg_cong2} + 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 _ = tracing (Syntax.string_of_term @{context} (term_of t)) 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 @@ -990,18 +922,15 @@ 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 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) @@ -1017,7 +946,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 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) @@ -1029,7 +958,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 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) @@ -1041,7 +970,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 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) @@ -1067,19 +996,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 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 *} ) @@ -1087,9 +1030,10 @@ 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})) + val m1_novars = snd(no_vars ((Context.Theory @{theory}),@{thm list.induct})) *} ML {* val goal = @@ -1099,89 +1043,33 @@ *} 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 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} - ) - ) -*} - - - - -ML {* MRS *} thm card1_suc ML {* - val m1_novars = snd(no_vars ((Context.Theory @{theory}), @{thm card1_suc})) + val m1_novars = snd(no_vars ((Context.Theory @{theory}),@{thm card1_suc})) *} ML {* val goal = build_goal 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 "\x. P x"} *} prove {* (Thm.term_of cgoal2) *} apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} ) - apply (tactic {* foo_tac' @{context} 1 *}) - done + (*