# HG changeset patch # User Cezary Kaliszyk # Date 1254157827 -7200 # Node ID f078dbf557b725a3faa09f40e2ceff200f65a977 # Parent e51af8bace6506b5f651805086c534f8b83ccf35# Parent 72d63aa8af6853f7f209881e322805268f52b3a0 Merged diff -r 72d63aa8af68 -r f078dbf557b7 QuotMain.thy --- a/QuotMain.thy Mon Sep 28 02:39:44 2009 +0200 +++ b/QuotMain.thy Mon Sep 28 19:10:27 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 @@ -559,7 +559,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) @@ -568,7 +568,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 {* @@ -767,7 +767,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: @@ -776,7 +776,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: @@ -794,17 +794,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 @@ -823,45 +823,83 @@ *} ML {* -fun build_goal ctxt thm constructors qty mk_rep_abs = -let - fun is_const (Const (x, t)) = x mem constructors +fun build_goal ctxt thm constructors lifted_type mk_rep_abs = + let + 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 ctxt t) - in - if type_of t = qty then mk_rep_abs t else t - end - handle TYPE _ => t - - fun build_aux (Abs (s, t, tr)) = (Abs (s, t, build_aux tr)) - | build_aux (f $ a) = + 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 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) + in + Logic.mk_equals (build_aux ctxt 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 = [emptyt, in_t, uniont, cardt, insertt] *} +ML {* val fset_defs_sym = map (fn t => symmetric (unlam_def @{context} t)) fset_defs *} ML {* fun dest_cbinop t = @@ -894,25 +932,46 @@ *} ML {* - fun foo_conv t = + fun split_binop_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 = + 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 foo_tac n thm = + fun split_binop_tac n thm = let val concl = Thm.cprem_of thm n; val (_, cconcl) = Thm.dest_comb concl; - val rewr = foo_conv cconcl; -(* val _ = tracing (Display.string_of_thm @{context} rewr) - val _ = tracing (Display.string_of_thm @{context} thm)*) + 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; in rtac rewr n thm end @@ -925,23 +984,36 @@ 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}, 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})), - foo_tac, + DatatypeAux.cong_tac, + rtac @{thm ext}, + rtac @{thm eq_reflection}, CHANGED o (ObjectLogic.full_atomize_tac) ]) *} ML {* +<<<<<<< variant A + 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 +>>>>>>> variant B 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 +####### Ancestor + val m1_novars = snd(no_vars ((Context.Theory @{theory}), @{thm m1})) + val goal = build_goal m1_novars consts @{typ "'a list"} mk_rep_abs +======= end val cgoal = cterm_of @{theory} goal val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false fset_defs_sym cgoal) *} @@ -949,15 +1021,39 @@ (*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 *) ML {* - 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 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) *} @@ -968,8 +1064,8 @@ thm m2 ML {* - 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 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) *} @@ -980,8 +1076,8 @@ thm list_eq.intros(4) ML {* - 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 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) val cgoal3 = Thm.rhs_of (MetaSimplifier.rewrite true @{thms QUOT_TYPE_I_fset.thm10} cgoal2) @@ -1006,33 +1102,19 @@ 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. +thm list_eq.intros(5) +ML {* + 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 {* - 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 goal = build_goal @{context} 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 false fset_defs_sym cgoal) + val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite true fset_defs_sym cgoal) *} prove {* Thm.term_of cgoal2 *} apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} ) @@ -1040,7 +1122,6 @@ 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})) @@ -1053,18 +1134,94 @@ *} ML {* val cgoal = cterm_of @{theory} goal - val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false fset_defs_sym cgoal) *} -ML fset_defs_sym +ML {* + val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite true fset_defs_sym cgoal) +*} + prove {* (Thm.term_of cgoal2) *} apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} ) - 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) + apply (tactic {* foo_tac' @{context} 1 *}) 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} + ) + ) +*} + +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 {* @@ -1075,11 +1232,13 @@ *} ML {* val cgoal = cterm_of @{theory} goal - val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false fset_defs_sym cgoal) + val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite true fset_defs_sym cgoal) *} +ML {* @{term "\x. P x"} *} +ML {* Thm.bicompose *} prove {* (Thm.term_of cgoal2) *} - apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} ) - + apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} ) + apply (tactic {* foo_tac' @{context} 1 *}) (*