nominal2: comparison QuotMain.thy

equal deleted inserted replaced

-:5f6ee943c697
+:f46eddb570a3
 assumes equiv: "EQUIV R"
 and     rep_prop: "\<And>y. \<exists>x. Rep y = R x"
 and     rep_inverse: "\<And>x. Abs (Rep x) = x"
 and     abs_inverse: "\<And>x. (Rep (Abs (R x))) = (R x)"
 and     rep_inject: "\<And>x y. (Rep x = Rep y) = (x = y)"
 begin
 definition
 "ABS x \<equiv> Abs (R x)"
 definition
 "REP a = Eps (Rep a)"
 lemma lem9:
 shows "R (Eps (R x)) = R x"
 proof -
 have a: "R x x" using equiv by (simp add: EQUIV_REFL_SYM_TRANS REFL_def)
 then have "R x (Eps (R x))" by (rule someI)
 then show "R (Eps (R x)) = R x"
 using equiv unfolding EQUIV_def by simp
 qed
 theorem thm10:
 shows "ABS (REP a) = a"
 unfolding ABS_def REP_def
 proof -
 from rep_prop
 obtain x where eq: "Rep a = R x" by auto
 have "Abs (R (Eps (Rep a))) = Abs (R (Eps (R x)))" using eq by simp
 also have "\<dots> = Abs (R x)" using lem9 by simp
 also have "\<dots> = Abs (Rep a)" using eq by simp
 also have "\<dots> = a" using rep_inverse by simp
 finally
 show "Abs (R (Eps (Rep a))) = a" by simp
 qed
 lemma REP_refl:
 shows "R (REP a) (REP a)"
 unfolding REP_def
 by (simp add: equiv[simplified EQUIV_def])
 lemma lem7:
 apply(rule iffI)
 apply(simp)
 apply(drule rep_inject[THEN iffD2])
 apply(simp add: abs_inverse)
 done
 theorem thm11:
 shows "R r r' = (ABS r = ABS r')"
 unfolding ABS_def
 by (simp only: equiv[simplified EQUIV_def] lem7)
 ML {*
 (* constructs the term \<lambda>(c::ty \<Rightarrow> bool). \<exists>x. c = rel x *)
 fun typedef_term rel ty lthy =
 let
 val [x, c] = [("x", ty), ("c", ty --> @{typ bool})]
 |> Variable.variant_frees lthy [rel]
 |> map Free
 in
 lambda c
 (HOLogic.mk_exists
 ("x", ty, HOLogic.mk_eq (c, (rel $ x))))
 end
 *}
 (*
 |> Syntax.string_of_term @{context}
 |> writeln
 *}*)
 ML {*
 val typedef_tac =
 EVERY1 [rewrite_goal_tac @{thms mem_def},
 rtac @{thm exI}, rtac @{thm exI}, rtac @{thm refl}]
 *}
 ML {*
 (* makes the new type definitions *)
 fun typedef_make (qty_name, rel, ty) lthy =
 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
 *}
 text {* proves the QUOT_TYPE theorem for the new type *}
 ML {*
 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
 val rep_inj = #Rep_inject typedef_info
 val ss = HOL_basic_ss addsimps @{thms mem_def}
 val rep_thm_simpd = Simplifier.asm_full_simplify ss rep_thm
 val abs_inv_simpd = Simplifier.asm_full_simplify ss abs_inv
 in
 EVERY1 [rtac @{thm QUOT_TYPE.intro},
 rtac equiv_thm,
 rtac rep_thm_simpd,
 rtac rep_inv,
 rtac abs_inv_simpd, rtac @{thm exI}, rtac @{thm refl},
 rtac rep_inj]
 end
 *}
 term QUOT_TYPE
 ML {* HOLogic.mk_Trueprop *}
 ML {* Goal.prove *}
 ML {* Syntax.check_term *}
 ML {*
 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
 end
 *}
 ML {*
 fun typedef_quotient_thm_tac defs quot_type_thm =
 EVERY1 [K (rewrite_goals_tac defs),
 rtac @{thm QUOT_TYPE.QUOTIENT},
 rtac quot_type_thm]
 *}
 ML {*
 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
 (fn _ => typedef_quotient_thm_tac [abs_def, rep_def] quot_type_thm)
 end
 *}
 text {* two wrappers for define and note *}
 ML {*
 fun make_def (name, mx, trm) lthy =
 let
 val ((trm, (_ , thm)), lthy') =
 LocalTheory.define Thm.internalK ((name, mx), (Attrib.empty_binding, trm)) lthy
 in
 ((trm, thm), lthy')
 end
 *}
 ML {* make_def (@{binding foo}, NoSyn, @{term "x + x"}) @{context} *}
 *)
 ML {*
 fun reg_thm (name, thm) lthy =
 let
 val ((_,[thm']), lthy') = LocalTheory.note Thm.theoremK ((name, []), [thm]) lthy
 in
 (thm',lthy')
 end
 *}
 ML {* Binding.str_of @{binding foo} *}
 ML {*
 fun typedef_main (qty_name, rel, ty, equiv_thm) lthy =
 let
 (* generates typedef *)
 val ((_,typedef_info), lthy') = typedef_make (qty_name, rel, ty) lthy
 (* abs and rep functions *)
 val abs_ty = #abs_type typedef_info
 val rep = Const (rep_name, abs_ty --> rep_ty)
 (* ABS and REP definitions *)
 val ABS_const = Const (@{const_name "QUOT_TYPE.ABS"}, dummyT )
 val REP_const = Const (@{const_name "QUOT_TYPE.REP"}, dummyT )
 val ABS_trm = Syntax.check_term lthy' (ABS_const $ rel $ abs)
 val REP_trm = Syntax.check_term lthy' (REP_const $ rep)
 val ABS_name = Binding.prefix_name "ABS_" qty_name
 val REP_name = Binding.prefix_name "REP_" qty_name
 val (((ABS, ABS_def), (REP, REP_def)), lthy'') =
 lthy' |> make_def (ABS_name, NoSyn, ABS_trm)
 ||>> make_def (REP_name, NoSyn, REP_trm)
 (* REMOVE VARIFY *)
 val _ = tracing (Syntax.string_of_typ lthy' (type_of ABS_trm))
 *}
 section {* various tests for quotient types*}
 datatype trm =
 var  "nat"
 | app  "trm" "trm"
 | lam  "nat" "trm"
 axiomatization RR :: "trm \<Rightarrow> trm \<Rightarrow> bool" where
 r_eq: "EQUIV RR"
 ML {*
 typedef_main
 *}
 (*ML {*
 val lthy = @{context};
 val qty_name = @{binding "qtrm"}
 axioms rmy_eq: "EQUIV Rmy"
 term "\<lambda>(c::'a my\<Rightarrow>bool). \<exists>x. c = Rmy x"
 datatype 'a trm' =
 var'  "'a"
 | app'  "'a trm'" "'a trm'"
 | lam'  "'a" "'a trm'"
 consts R' :: "'a trm' \<Rightarrow> 'a trm' \<Rightarrow> bool"
 axioms r_eq': "EQUIV R'"
 local_setup {*
 val empty = Symtab.empty
 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))
 end
 *}
 (* mapfuns for some standard types *)
 setup {*
 ML {* lookup (Context.Proof @{context}) @{type_name list} *}
 ML {*
 datatype abs_or_rep = abs | rep
 fun get_fun abs_or_rep rty qty lthy ty =
 let
 val qty_name = Long_Name.base_name (fst (dest_Type qty))
 fun get_fun_aux s fs_tys =
 let
 val (fs, tys) = split_list fs_tys
 val (otys, ntys) = split_list tys
 val oty = Type (s, otys)
 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))
 end
 fun get_const abs = (Const ("QuotMain.ABS_" ^ qty_name, rty --> qty), (rty, qty))
 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))
 | Type (s, tys) => get_fun_aux s (map (get_fun abs_or_rep rty qty lthy) tys)
 | _ => raise ERROR ("no variables")
 )
 end
 *}
 let
 val ty = fastype_of nconst
 val (arg_tys, res_ty) = strip_type ty
 val fresh_args = arg_tys |> map (pair "x")
 |> 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
 |> fold_rev lambda fresh_args
 end
 *}
 ML {*
 fun exchange_ty rty qty ty =
 if ty = rty then qty
 else
 (case ty of
 Type (s, tys) => Type (s, map (exchange_ty rty qty) tys)
 | _ => ty)
 *}
 ML {*
 fun make_const_def nconst_name oconst mx rty qty lthy =
 let
 val oconst_ty = fastype_of oconst
 val nconst_ty = exchange_ty rty qty oconst_ty
 val nconst = Const (nconst_name, nconst_ty)
 val def_trm = get_const_def nconst oconst rty qty lthy
 in
 make_def (Binding.name nconst_name, mx, def_trm) lthy
 end
 *}
 local_setup {*
 make_const_def "VR" @{term "vr"} NoSyn @{typ "t"} @{typ "qt"} #> snd
 *}
 local_setup {*
 make_const_def "UNION" @{term "op @"} NoSyn @{typ "'a list"} @{typ "'a fset"} #> snd
 *}
 term append
 term UNION
 thm UNION_def
 local_setup {*
 make_const_def "CARD" @{term "length"} NoSyn @{typ "'a list"} @{typ "'a fset"} #> snd

changeset 15	f46eddb570a3
parent 14	5f6ee943c697
child 16	06b158ee1545