diff -r d98224cafb86 -r e801b929216b QuotMain.thy --- a/QuotMain.thy Mon Sep 28 19:15:19 2009 +0200 +++ b/QuotMain.thy Mon Sep 28 19:22:28 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" @@ -397,8 +397,8 @@ val extend = I fun merge _ = Symtab.merge (K true)) in - val lookup = Symtab.lookup o Data.get - fun update k v = Data.map (Symtab.update (k, v)) + val lookup = Symtab.lookup o Data.get + fun update k v = Data.map (Symtab.update (k, v)) end *} @@ -412,9 +412,9 @@ ML {* lookup (Context.Proof @{context}) @{type_name list} *} ML {* -datatype abs_or_rep = abs | rep +datatype flag = absF | repF -fun get_fun abs_or_rep rty qty lthy ty = +fun get_fun flag rty qty lthy ty = let val qty_name = Long_Name.base_name (fst (dest_Type qty)) @@ -431,30 +431,36 @@ | NONE => raise ERROR ("no map association for type " ^ s)) end - fun get_const abs = (Const ("QuotMain.ABS_" ^ qty_name, rty --> qty), (rty, qty)) - | get_const rep = (Const ("QuotMain.REP_" ^ qty_name, qty --> rty), (qty, rty)) + fun get_const absF = (Const ("QuotMain.ABS_" ^ qty_name, rty --> qty), (rty, qty)) + | get_const repF = (Const ("QuotMain.REP_" ^ qty_name, qty --> rty), (qty, rty)) fun mk_identity ty = Abs ("x", ty, Bound 0) in if ty = qty - then (get_const abs_or_rep) + then (get_const flag) else (case ty of TFree _ => (mk_identity ty, (ty, ty)) | Type (_, []) => (mk_identity ty, (ty, ty)) - | Type (s, tys) => get_fun_aux s (map (get_fun abs_or_rep rty qty lthy) tys) + | Type (s, tys) => get_fun_aux s (map (get_fun flag rty qty lthy) tys) | _ => raise ERROR ("no type variables") ) end *} ML {* - get_fun rep @{typ t} @{typ qt} @{context} @{typ "t * nat"} + get_fun repF @{typ t} @{typ qt} @{context} @{typ "t * nat"} |> fst |> Syntax.string_of_term @{context} |> writeln *} +ML {* + get_fun absF @{typ t} @{typ qt} @{context} @{typ "t * nat"} + |> fst + |> Syntax.string_of_term @{context} + |> writeln +*} text {* produces the definition for a lifted constant *} ML {* @@ -467,8 +473,8 @@ |> Variable.variant_frees lthy [nconst, oconst] |> map Free - val rep_fns = map (fst o get_fun rep rty qty lthy) arg_tys - val abs_fn = (fst o get_fun abs rty qty lthy) res_ty + val rep_fns = map (fst o get_fun repF rty qty lthy) arg_tys + val abs_fn = (fst o get_fun absF rty qty lthy) res_ty in map (op $) (rep_fns ~~ fresh_args) @@ -480,7 +486,7 @@ ML {* fun exchange_ty rty qty ty = - if ty = rty + if ty = rty then qty else (case ty of @@ -559,7 +565,7 @@ | "xs \ ys \ a#xs \ a#ys" | "\xs1 \ xs2; xs2 \ xs3\ \ xs1 \ xs3" -lemma list_eq_refl: +lemma list_eq_sym: shows "xs \ xs" apply (induct xs) apply (auto intro: list_eq.intros) @@ -568,7 +574,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_refl) + apply(auto intro: list_eq.intros list_eq_sym) done local_setup {* @@ -674,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 @@ -684,10 +690,10 @@ 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) +apply (metis QUOT_TYPE_I_fset.R_trans QuotMain.card1_cons list_eq_sym mem_cons) done lemma cons_preserves: @@ -698,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. @@ -767,7 +773,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_refl) +apply(rule list_eq_sym) done lemma append_respects_fst: @@ -776,7 +782,7 @@ using a apply(induct) apply(auto intro: list_eq.intros) - apply(simp add: list_eq_refl) + apply(simp add: list_eq_sym) done lemma yyy: @@ -794,17 +800,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_refl) + apply(rule list_eq_sym) 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_refl) + apply(rule list_eq_sym) 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_refl) + apply(rule list_eq_sym) done lemma @@ -817,89 +823,51 @@ 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 lifted_type mk_rep_abs = - let - fun is_constructor (Const (x, _)) = member (op =) constructors x - | is_constructor _ = false; - +fun build_goal ctxt thm constructors qty mk_rep_abs = +let + fun is_const (Const (x, t)) = x mem constructors + | is_const _ = 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 = 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 _ = 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 (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 ctxt1) args))) - else list_comb (build_aux ctxt1 f, map (build_aux ctxt1) args) + (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))) 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 ctxt concl2, concl2) + + val concl2 = prop_of thm +in + Logic.mk_equals ((build_aux 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 = 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 = @@ -915,7 +883,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 @@ -932,46 +900,25 @@ *} ML {* - fun split_binop_conv t = + fun foo_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} - 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 @@ -984,27 +931,22 @@ 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_refl}, + rtac @{thm trueprop_cong}, + 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 @{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) @@ -1013,26 +955,6 @@ (*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 *}) @@ -1040,7 +962,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) @@ -1052,7 +974,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) @@ -1064,7 +986,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) @@ -1090,19 +1012,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 @{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 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 *} ) @@ -1110,6 +1046,7 @@ 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})) @@ -1122,94 +1059,18 @@ *} 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 @{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 {* @@ -1220,13 +1081,11 @@ *} 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"} *} -ML {* Thm.bicompose *} prove {* (Thm.term_of cgoal2) *} apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} ) - apply (tactic {* foo_tac' @{context} 1 *}) + (*