nominal2: comparison QuotMain.thy

equal deleted inserted replaced

-:e51af8bace65
+:f078dbf557b7
 then show "R a b" using R_sym by blast
 qed
 lemma REPS_same:
 shows "R (REP a) (REP b) \<equiv> (a = b)"
-apply (rule eq_reflection)
+proof -
-proof
+have "R (REP a) (REP b) = (a = b)"
-assume as: "R (REP a) (REP b)"
+proof
-from rep_prop
+assume as: "R (REP a) (REP b)"
-obtain x y
+from rep_prop
-where eqs: "Rep a = R x" "Rep b = R y" by blast
+obtain x y
-from eqs have "R (Eps (R x)) (Eps (R y))" using as unfolding REP_def by simp
+where eqs: "Rep a = R x" "Rep b = R y" by blast
-then have "R x (Eps (R y))" using lem9 by simp
+from eqs have "R (Eps (R x)) (Eps (R y))" using as unfolding REP_def by simp
-then have "R (Eps (R y)) x" using R_sym by blast
+then have "R x (Eps (R y))" using lem9 by simp
-then have "R y x" using lem9 by simp
+then have "R (Eps (R y)) x" using R_sym by blast
-then have "R x y" using R_sym by blast
+then have "R y x" using lem9 by simp
-then have "ABS x = ABS y" using thm11 by simp
+then have "R x y" using R_sym by blast
-then have "Abs (Rep a) = Abs (Rep b)" using eqs unfolding ABS_def by simp
+then have "ABS x = ABS y" using thm11 by simp
-then show "a = b" using rep_inverse by simp
+then have "Abs (Rep a) = Abs (Rep b)" using eqs unfolding ABS_def by simp
-next
+then show "a = b" using rep_inverse by simp
-assume ab: "a = b"
+next
-have "REFL R" using equiv EQUIV_REFL_SYM_TRANS[of R] by simp
+assume ab: "a = b"
-then show "R (REP a) (REP b)" unfolding REFL_def using ab by auto
+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
 section {* type definition for the quotient type *}
 val [x, c] = [("x", ty), ("c", ty --> @{typ bool})]
 |> Variable.variant_frees lthy [rel]
 |> map Free
 in
 lambda c
-(HOLogic.mk_exists
+(HOLogic.exists_const ty $
-("x", ty, HOLogic.mk_eq (c, (rel $ x))))
+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
 val typedef_tac =
 EVERY1 [rewrite_goal_tac @{thms mem_def},
 rtac @{thm exI},
 rtac @{thm exI},
 rtac @{thm refl}]
 in
 LocalTheory.theory_result
 (Typedef.add_typedef false NONE
 (qty_name, map fst (Term.add_tfreesT ty []), NoSyn)
 (typedef_term rel ty lthy)
 NONE typedef_tac) lthy
 end
-*}
-ML {*
+(* tactic to prove the QUOT_TYPE theorem for the new type *)
-(* proves 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
 val rep_inv = #Rep_inverse typedef_info
 val abs_inv = #Abs_inverse typedef_info
 rtac rep_inv,
 rtac abs_inv_simpd, rtac @{thm exI}, rtac @{thm refl},
 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)
 val goal = HOLogic.mk_Trueprop (quot_type_const $ rel $ abs $ rep)
 |> Syntax.check_term lthy
 in
 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)
 val goal = HOLogic.mk_Trueprop (quotient_const $ rel $ abs $ rep)
 |> Syntax.check_term lthy
 val typedef_quotient_thm_tac =
 EVERY1 [K (rewrite_goals_tac [abs_def, rep_def]),
 rtac @{thm QUOT_TYPE.QUOTIENT},
 rtac quot_type_thm]
 in
 Goal.prove lthy [] [] goal
 (K typedef_quotient_thm_tac)
 end
 *}
 text {* two wrappers for define and note *}
 datatype trm =
 var  "nat"
 | app  "trm" "trm"
 | lam  "nat" "trm"
 axiomatization
 RR :: "trm \<Rightarrow> trm \<Rightarrow> bool"
 where
 r_eq: "EQUIV RR"
 local_setup {*
 typedef_main (@{binding "qtrm"}, @{term "RR"}, @{typ trm}, @{thm r_eq}) #> snd
 val nty = Type (s, ntys)
 val ftys = map (op -->) tys
 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))
+TFree _ => (mk_identity ty, (ty, ty))
-| Type (_, []) => (Abs ("x", ty, Bound 0), (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
 *}
 ML {*
 |> Syntax.string_of_term @{context}
 |> writeln
 *}
+text {* produces the definition for a lifted constant *}
 ML {*
 fun get_const_def nconst oconst rty qty lthy =
 let
 val ty = fastype_of nconst
 val (arg_tys, res_ty) = strip_type ty
 end
 *}
 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 {*
 fun make_const_def nconst_bname oconst mx rty qty lthy =
 let
 make_def (nconst_bname, mx, def_trm) lthy
 end
 *}
 local_setup {*
-make_const_def @{binding VR} @{term "vr"} NoSyn @{typ "t"} @{typ "qt"} #> snd
+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 #>
-local_setup {*
-make_const_def @{binding AP} @{term "ap"} NoSyn @{typ "t"} @{typ "qt"} #> snd
-*}
-local_setup {*
 make_const_def @{binding LM} @{term "lm"} NoSyn @{typ "t"} @{typ "qt"} #> snd
 *}
-thm VR_def
+term vr
-thm AP_def
+term ap
-thm LM_def
+term lm
+thm VR_def AP_def LM_def
 term LM
 term VR
 term AP
 *}
 print_theorems
 local_setup {*
-make_const_def @{binding VR'} @{term "vr'"} NoSyn @{typ "'a t'"} @{typ "'a qt'"} #> snd
+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 #>
-local_setup {*
-make_const_def @{binding AP'} @{term "ap'"} NoSyn @{typ "'a t'"} @{typ "'a qt'"} #> snd
-*}
-local_setup {*
 make_const_def @{binding LM'} @{term "lm'"} NoSyn @{typ "'a t'"} @{typ "'a qt'"} #> snd
 *}
-thm VR'_def
+term vr'
-thm AP'_def
+term ap'
-thm LM'_def
+term ap'
+thm VR'_def AP'_def LM'_def
 term LM'
 term VR'
 term AP'
 (* text {*
 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"
 assumes e: "a \<approx> b"
 shows "card1 a = card1 b"
 lemma mem_cons:
 fixes x :: "'a"
 fixes xs :: "'a list"
 assumes a : "x memb xs"
 shows "x # xs \<approx> xs"
-using a apply (induct xs)
+using a
-apply (simp_all)
+apply (induct xs)
-apply (meson)
+apply (auto intro: list_eq.intros)
-apply (simp_all add: list_eq.intros(4))
+done
-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
 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)
+using c
-apply (simp)
+apply(induct xs)
-(*  apply (rule allI)*)
+apply (metis Suc_neq_Zero card1_0)
-proof -
+apply (metis QUOT_TYPE_I_fset.R_trans QuotMain.card1_cons list_eq_sym mem_cons)
-fix a :: "'a"
+done
-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
 lemma cons_preserves:
 fixes z
 assumes a: "xs \<approx> ys"
 shows "(z # xs) \<approx> (z # ys)"
 using a by (rule QuotMain.list_eq.intros(5))
 text {*
-unlam_def converts a definition theorem given as 'a = \lambda x. \lambda y. f (x y)'
+Unlam_def converts a definition given as
-to a theorem 'a x y = f (x, y)'. These are needed to rewrite right-to-left.
+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 {*
 fun unlam_def_aux orig_ctxt ctxt t =
 let val rhs = Thm.rhs_of t in
 apply (simp add: QUOT_TYPE_I_fset.thm10)
 done
 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
 fun is_constructor (Const (x, _)) = member (op =) constructors x
 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
 (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 =
 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)
 end *}
 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
 *}
 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;
 val [cmT, crT] = Thm.dest_ctyp cr2;
 in
 CHANGED o (ObjectLogic.full_atomize_tac)
 ])
 *}
 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)
 *}
 (*notation ( output) "prop" ("#_" [1000] 1000) *)
 done
 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 {*
 val cgoal = cterm_of @{theory} goal
 *}
 ML {* MRS *}
 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
 val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite true fset_defs_sym cgoal)
 *}

changeset 44	f078dbf557b7
parent 43	e51af8bace65
parent 41	72d63aa8af68
child 45	d98224cafb86