diff -r e51af8bace65 -r f078dbf557b7 QuotMain.thy --- a/QuotMain.thy Mon Sep 28 18:59:04 2009 +0200 +++ b/QuotMain.thy Mon Sep 28 19:10:27 2009 +0200 @@ -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 @@ -148,19 +151,18 @@ |> map Free in lambda c - (HOLogic.mk_exists - ("x", ty, HOLogic.mk_eq (c, (rel $ x)))) + (HOLogic.exists_const ty $ + lambda x (HOLogic.mk_eq (c, (rel $ x)))) end -*} -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 @@ -169,10 +171,9 @@ (typedef_term rel ty lthy) NONE typedef_tac) lthy end -*} + -ML {* -(* proves the QUOT_TYPE theorem for the new type *) +(* tactic to prove the QUOT_TYPE theorem for the new type *) fun typedef_quot_type_tac equiv_thm (typedef_info: Typedef.info) = let val rep_thm = #Rep typedef_info @@ -192,6 +193,7 @@ rtac rep_inj] end + fun typedef_quot_type_thm (rel, abs, rep, equiv_thm, typedef_info) lthy = let val quot_type_const = Const (@{const_name "QUOT_TYPE"}, dummyT) @@ -201,9 +203,9 @@ Goal.prove lthy [] [] goal (K (typedef_quot_type_tac equiv_thm typedef_info)) end -*} + -ML {* +(* proves the quotient theorem *) fun typedef_quotient_thm (rel, abs, rep, abs_def, rep_def, quot_type_thm) lthy = let val quotient_const = Const (@{const_name "QUOTIENT"}, dummyT) @@ -215,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 *} @@ -322,8 +324,8 @@ | app "trm" "trm" | lam "nat" "trm" -axiomatization - RR :: "trm \ trm \ bool" +axiomatization + RR :: "trm \ trm \ bool" where r_eq: "EQUIV RR" @@ -426,19 +428,22 @@ in (case (lookup (Context.Proof lthy) s) of SOME info => (list_comb (Const (#mapfun info, ftys ---> oty --> nty), fs), (oty, nty)) - | NONE => raise ERROR ("no map association for type " ^ s)) + | 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 mk_identity ty = Abs ("x", ty, Bound 0) + in if ty = qty then (get_const abs_or_rep) else (case ty of - TFree _ => (Abs ("x", ty, Bound 0), (ty, ty)) - | Type (_, []) => (Abs ("x", ty, Bound 0), (ty, ty)) + 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) - | _ => raise ERROR ("no variables") + | _ => raise ERROR ("no type variables") ) end *} @@ -451,6 +456,7 @@ *} +text {* produces the definition for a lifted constant *} ML {* fun get_const_def nconst oconst rty qty lthy = let @@ -474,11 +480,13 @@ ML {* fun exchange_ty rty qty ty = - if ty = rty then qty + if ty = rty + then qty else (case ty of Type (s, tys) => Type (s, map (exchange_ty rty qty) tys) - | _ => ty) + | _ => ty + ) *} ML {* @@ -494,20 +502,15 @@ *} local_setup {* - make_const_def @{binding VR} @{term "vr"} NoSyn @{typ "t"} @{typ "qt"} #> snd -*} - -local_setup {* - make_const_def @{binding AP} @{term "ap"} NoSyn @{typ "t"} @{typ "qt"} #> snd -*} - -local_setup {* + make_const_def @{binding VR} @{term "vr"} NoSyn @{typ "t"} @{typ "qt"} #> snd #> + make_const_def @{binding AP} @{term "ap"} NoSyn @{typ "t"} @{typ "qt"} #> snd #> make_const_def @{binding LM} @{term "lm"} NoSyn @{typ "t"} @{typ "qt"} #> snd *} -thm VR_def -thm AP_def -thm LM_def +term vr +term ap +term lm +thm VR_def AP_def LM_def term LM term VR term AP @@ -530,20 +533,15 @@ print_theorems local_setup {* - make_const_def @{binding VR'} @{term "vr'"} NoSyn @{typ "'a t'"} @{typ "'a qt'"} #> snd -*} - -local_setup {* - make_const_def @{binding AP'} @{term "ap'"} NoSyn @{typ "'a t'"} @{typ "'a qt'"} #> snd -*} - -local_setup {* + make_const_def @{binding VR'} @{term "vr'"} NoSyn @{typ "'a t'"} @{typ "'a qt'"} #> snd #> + make_const_def @{binding AP'} @{term "ap'"} NoSyn @{typ "'a t'"} @{typ "'a qt'"} #> snd #> make_const_def @{binding LM'} @{term "lm'"} NoSyn @{typ "'a t'"} @{typ "'a qt'"} #> snd *} -thm VR'_def -thm AP'_def -thm LM'_def +term vr' +term ap' +term ap' +thm VR'_def AP'_def LM'_def term LM' term VR' term AP' @@ -644,7 +642,7 @@ Maybe make_const_def should require a theorem that says that the particular lifted function respects the relation. With it such a definition would be impossible: make_const_def @{binding CARD} @{term "length"} NoSyn @{typ "'a list"} @{typ "'a fset"} #> snd -*} *) +*}*) lemma card1_rsp: fixes a b :: "'a list" @@ -676,66 +674,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_refl) - 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 @@ -745,8 +698,16 @@ text {* - unlam_def converts a definition theorem given as 'a = \lambda x. \lambda y. f (x y)' - to a theorem 'a x y = f (x, y)'. These are needed to rewrite right-to-left. + 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 + + This function is needed to rewrite the right-hand + side to the left-hand side. *} ML {* @@ -856,11 +817,11 @@ 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"}, @{const_name "card1"}] + val consts = [@{const_name "Nil"}, @{const_name "append"}, + @{const_name "Cons"}, @{const_name "membship"}, + @{const_name "card1"}] *} -ML lambda - ML {* fun build_goal ctxt thm constructors lifted_type mk_rep_abs = let @@ -904,6 +865,7 @@ 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) @@ -930,6 +892,7 @@ end | 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) @@ -957,20 +920,20 @@ 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 = 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; @@ -1041,8 +1004,16 @@ *} 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) *} @@ -1153,12 +1124,12 @@ 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 = Toplevel.program (fn () => - build_goal m1_novars consts @{typ "'a list"} mk_rep_abs + build_goal @{context} m1_novars consts @{typ "'a list"} mk_rep_abs ) *} ML {* @@ -1254,10 +1225,10 @@ 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 + val goal = build_goal @{context} m1_novars consts @{typ "'a list"} mk_rep_abs *} ML {* val cgoal = cterm_of @{theory} goal