--- 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) \<equiv> (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) \<equiv> (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 \<Rightarrow> trm \<Rightarrow> bool"
+axiomatization
+ RR :: "trm \<Rightarrow> trm \<Rightarrow> 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 \<approx> 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 \<approx> xs"
- assume a2 : "x memb xs"
- have a3 : "x # a # xs \<approx> a # x # xs" using list_eq.intros(1)[of "x"] by blast
- have a4 : "a # x # xs \<approx> a # xs" using a1 list_eq.intros(5)[of "x # xs" "xs"] by simp
- then show "x # a # xs \<approx> 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 "\<exists>a ys. ~(a memb ys) \<and> xs \<approx> (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 \<Longrightarrow> \<exists>a ys. \<not> a memb ys \<and> xs \<approx> a # ys"
- assume a2: "card1 (a # xs) = Suc n"
- from a1 a2 show "\<exists>aa ys. \<not> aa memb ys \<and> a # xs \<approx> 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: "\<exists>a ys. \<not> a memb ys \<and> xs \<approx> a # ys"
- assume a2: "card1 xs = Suc n"
- assume a3: "a memb xs"
- from a1 obtain b ys where a5: "\<not> b memb ys \<and> xs \<approx> b # ys" by blast
- from a2 a3 a5 show "\<exists>aa ys. \<not> aa memb ys \<and> a # xs \<approx> 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: "\<not> b memb ys \<and> xs \<approx> b # ys"
- then have a3: "xs \<approx> b # ys" by simp
- have "a # xs \<approx> xs" using a1 mem_cons[of "a" "xs"] by simp
- then show "a # xs \<approx> b # ys" using a3 list_eq.intros(6) by blast
- qed
-next
- assume a2: "\<not> a memb xs"
- from a2 show "\<exists>aa ys. \<not> aa memb ys \<and> a # xs \<approx> 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 \<equiv> %x. %y. f x y
+
+ to a theorem of the form
+
+ c x y \<equiv> 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