# HG changeset patch # User Cezary Kaliszyk # Date 1254322629 -7200 # Node ID f2565006dc5afb10f0a0ec65b0edb2809d092016 # Parent 13be92f5b6388c2788d3154592cd228d1ab6253b Just one atomize is enough for the currently lifted theorems. Properly lift 'all' and 'Ex'. diff -r 13be92f5b638 -r f2565006dc5a QuotMain.thy --- a/QuotMain.thy Tue Sep 29 22:35:48 2009 +0200 +++ b/QuotMain.thy Wed Sep 30 16:57:09 2009 +0200 @@ -831,10 +831,12 @@ ML {* val qty = @{typ "'a fset"} *} ML {* val tt = Type ("fun", [Type ("fun", [qty, @{typ "prop"}]), @{typ "prop"}]) *} -ML {* val fall = Const(@{const_name all}, tt) *} +ML {* val fall = Const(@{const_name all}, dummyT) *} + +ML {* Syntax.check_term *} ML {* -fun build_goal ctxt thm constructors rty qty mk_rep mk_abs = +fun build_goal_term ctxt thm constructors rty qty mk_rep mk_abs = let fun mk_rep_abs x = mk_rep (mk_abs x); @@ -851,6 +853,9 @@ fun is_all (Const ("all", Type("fun", [Type("fun", [ty, _]), _]))) = ty = rty | is_all _ = false; + fun is_ex (Const ("Ex", Type("fun", [Type("fun", [ty, _]), _]))) = ty = rty + | is_ex _ = false; + fun build_aux ctxt1 tm = let val (head, args) = Term.strip_comb tm; @@ -873,22 +878,28 @@ val t' = subst_bound (v, t); val rec_term = build_aux ctxt2 t'; in Term.lambda_name (x, v) rec_term end - | _ => - if is_all head then (* I assume that we never lift 'prop' since it is not of sort type *) - list_comb (fall, args') + | _ => (* I assume that we never lift 'prop' since it is not of sort type *) + if is_all head then + list_comb (Const(@{const_name all}, dummyT), args') |> Syntax.check_term ctxt1 + else if is_ex head then + list_comb (Const(@{const_name Ex}, dummyT), args') |> Syntax.check_term ctxt1 else if is_constructor head then maybe_mk_rep_abs (list_comb (head, map maybe_mk_rep_abs args')) else maybe_mk_rep_abs (list_comb (head, args')) ) end; - - val concl2 = Thm.prop_of thm; in - Logic.mk_equals (build_aux ctxt concl2, concl2) + build_aux ctxt (Thm.prop_of thm) end *} +ML {* +fun build_goal ctxt thm cons rty qty mk_rep mk_abs = + Logic.mk_equals ((build_goal_term ctxt thm cons rty qty mk_rep mk_abs), (Thm.prop_of thm)) +*} + + 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 *} @@ -991,9 +1002,9 @@ 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})), Cong_Tac.cong_tac @{thm cong}, - rtac @{thm ext}, + rtac @{thm ext} (* rtac @{thm eq_reflection},*) - CHANGED o (ObjectLogic.full_atomize_tac) +(* CHANGED o (ObjectLogic.full_atomize_tac)*) ]) *} @@ -1029,6 +1040,7 @@ prove {* (Thm.term_of cgoal2) *} apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} ) + apply (atomize(full)) apply (tactic {* foo_tac' @{context} 1 *}) done @@ -1041,6 +1053,7 @@ *} prove {* Thm.term_of cgoal2 *} apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} ) + apply (atomize(full)) apply (tactic {* foo_tac' @{context} 1 *}) sorry @@ -1053,6 +1066,7 @@ *} prove {* Thm.term_of cgoal2 *} apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} ) + apply (atomize(full)) apply (tactic {* foo_tac' @{context} 1 *}) done @@ -1068,6 +1082,7 @@ (* It is the same, but we need a name for it. *) prove zzz : {* Thm.term_of cgoal3 *} apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} ) + apply (atomize(full)) apply (tactic {* foo_tac' @{context} 1 *}) done @@ -1095,6 +1110,7 @@ *} prove {* Thm.term_of cgoal2 *} apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} ) + apply (atomize(full)) apply (tactic {* foo_tac' @{context} 1 *}) done @@ -1103,6 +1119,7 @@ ML {* val m1_novars = snd(no_vars ((Context.Theory @{theory}), @{thm list.induct})) *} + ML {* val goal = Toplevel.program (fn () => @@ -1119,6 +1136,7 @@ prove {* (Thm.term_of cgoal2) *} apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} ) + apply (atomize(full)) apply (tactic {* foo_tac' @{context} 1 *}) sorry @@ -1129,7 +1147,7 @@ val goal = build_goal @{context} novars consts @{typ "'a list"} @{typ "'a fset"} mk_rep mk_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 tac = (LocalDefs.unfold_tac @{context} fset_defs) THEN (ObjectLogic.full_atomize_tac 1) 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; @@ -1155,7 +1173,8 @@ 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} *} -(*local_setup {* lift_theorem_fset @{binding "card_suc"} @{thm card1_suc} *}*) +(*ML {* Toplevel.program (fn () => lift_theorem_fset @{binding "card_suc"} @{thm card1_suc} @{context}) *} +local_setup {* lift_theorem_fset @{binding "card_suc"} @{thm card1_suc} *}*) thm m1_lift thm leqi4_lift @@ -1222,11 +1241,10 @@ ML {* Thm.bicompose *} prove aaa: {* (Thm.term_of cgoal2) *} apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} ) + apply (atomize(full)) apply (tactic {* foo_tac' @{context} 1 *}) done -thm aaa - (* datatype obj1 = OVAR1 "string"