# HG changeset patch # User Cezary Kaliszyk # Date 1254209182 -7200 # Node ID 50f72361d0958fc94344657130c89f9b8d8fe2a2 # Parent 5d32a81cfe49752fcfca5e8ebdbd9d1693b01e86 Merged diff -r 5d32a81cfe49 -r 50f72361d095 QuotMain.thy --- a/QuotMain.thy Mon Sep 28 23:17:29 2009 +0200 +++ b/QuotMain.thy Tue Sep 29 09:26:22 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 @@ -151,18 +151,18 @@ |> map Free in lambda c - (HOLogic.exists_const ty $ + (HOLogic.exists_const ty $ lambda x (HOLogic.mk_eq (c, (rel $ x)))) end (* 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 @@ -217,7 +217,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 *} @@ -324,8 +324,8 @@ | app "trm" "trm" | lam "nat" "trm" -axiomatization - RR :: "trm \ trm \ bool" +axiomatization + RR :: "trm \ trm \ bool" where r_eq: "EQUIV RR" @@ -486,7 +486,7 @@ ML {* fun exchange_ty rty qty ty = - if ty = rty + if ty = rty then qty else (case ty of @@ -680,7 +680,7 @@ fixes xs :: "'a list" assumes a : "x memb xs" shows "x # xs \ xs" - using a + using a apply (induct xs) apply (auto intro: list_eq.intros) done @@ -690,7 +690,7 @@ fixes n :: "nat" assumes c: "card1 xs = Suc n" shows "\a ys. ~(a memb ys) \ xs \ (a # ys)" - using c + 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_refl mem_cons) @@ -704,13 +704,13 @@ text {* - Unlam_def converts a definition given as + Unlam_def converts a definition given as c \ %x. %y. f x y - to a theorem of the form - - c x y \ f x y + to a theorem of the form + + c x y \ f x y This function is needed to rewrite the right-hand side to the left-hand side. @@ -823,51 +823,89 @@ ML {* fun mk_rep_abs x = @{term REP_fset} $ (@{term ABS_fset} $ x) - val consts = [@{const_name "Nil"}, @{const_name "append"}, - @{const_name "Cons"}, @{const_name "membship"}, + val consts = [@{const_name "Nil"}, @{const_name "append"}, + @{const_name "Cons"}, @{const_name "membship"}, @{const_name "card1"}] *} ML {* fun build_goal ctxt thm constructors qty mk_rep_abs = -let - fun is_const (Const (x, t)) = x mem constructors - | is_const _ = false - + 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 = 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 = qty 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 qty 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 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 = prop_of thm -in - Logic.mk_equals ((build_aux concl2), concl2) + + val concl2 = term_of (#prop (crep_thm thm)) + 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 = @@ -883,7 +921,7 @@ fun dest_ceq t = let val (bop, pair) = dest_cbinop t; - val (bop_s, _) = Term.dest_Const (Thm.term_of bop); + val (bop_s, _) = Term.dest_Const (Thm.term_of bop); in if bop_s = "op =" then pair else (raise CTERM ("Not an equality", [t])) end @@ -900,25 +938,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 @@ -931,22 +990,27 @@ 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 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 {* - 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 @{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) @@ -955,6 +1019,26 @@ (*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 (tactic {* foo_tac' @{context} 1 *}) @@ -962,7 +1046,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 @{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) @@ -974,7 +1058,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 @{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) @@ -986,7 +1070,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 @{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) @@ -1028,17 +1112,17 @@ 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 @{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 *} ) @@ -1046,7 +1130,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})) @@ -1059,18 +1142,92 @@ *} 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 fset_defs_sym 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 @{context} 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 {* @@ -1081,11 +1238,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 {* foo_tac' @{context} 1 *}) (* @@ -1097,4 +1256,4 @@ *) -yyes \ No newline at end of file +yyes