--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/QuotMain.thy Tue Aug 11 12:29:15 2009 +0200
@@ -0,0 +1,559 @@
+theory QuotMain
+imports QuotScript QuotList
+begin
+
+locale QUOT_TYPE =
+ fixes R :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
+ and Abs :: "('a \<Rightarrow> bool) \<Rightarrow> 'b"
+ and Rep :: "'b \<Rightarrow> ('a \<Rightarrow> bool)"
+ 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:
+ "(R x = R y) = (Abs (R x) = Abs (R y))"
+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)
+
+lemma QUOTIENT:
+ "QUOTIENT R ABS REP"
+apply(unfold QUOTIENT_def)
+apply(simp add: thm10)
+apply(simp add: REP_refl)
+apply(subst thm11[symmetric])
+apply(simp add: equiv[simplified EQUIV_def])
+done
+
+end
+
+ML {*
+ Variable.variant_frees
+*}
+
+
+section {* type definition for the quotient type *}
+
+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.exists_const ty) $
+ (lambda x (HOLogic.mk_eq (c, (rel $ x)))))
+end
+*}
+
+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
+ (TypedefPackage.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 QUOTIENT theorem for the new type *}
+ML {*
+fun typedef_quot_type_tac equiv_thm (typedef_info: TypedefPackage.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
+*}
+
+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
+in
+ Goal.prove lthy [] [] goal
+ (fn _ => typedef_quot_type_tac equiv_thm typedef_info)
+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
+in
+ Goal.prove lthy [] [] goal
+ (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 {*
+fun reg_thm (name, thm) lthy =
+let
+ val ((_,[thm']), lthy') = LocalTheory.note Thm.theoremK ((name, []), [thm]) lthy
+in
+ (thm',lthy')
+end
+*}
+
+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_ty = #rep_type typedef_info
+ val abs_name = #Abs_name typedef_info
+ val rep_name = #Rep_name typedef_info
+ val abs = Const (abs_name, rep_ty --> abs_ty)
+ 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)
+
+ (* quot_type theorem *)
+ val quot_thm = typedef_quot_type_thm (rel, abs, rep, equiv_thm, typedef_info) lthy''
+ val quot_thm_name = Binding.prefix_name "QUOT_TYPE_" qty_name
+
+ (* quotient theorem *)
+ val quotient_thm = typedef_quotient_thm (rel, ABS, REP, ABS_def, REP_def, quot_thm) lthy''
+ val quotient_thm_name = Binding.prefix_name "QUOTIENT_" qty_name
+
+in
+ lthy''
+ |> reg_thm (quot_thm_name, quot_thm)
+ ||>> reg_thm (quotient_thm_name, quotient_thm)
+end
+*}
+
+section {* various tests for quotient types*}
+datatype trm =
+ var "nat"
+| app "trm" "trm"
+| lam "nat" "trm"
+
+consts R :: "trm \<Rightarrow> trm \<Rightarrow> bool"
+axioms r_eq: "EQUIV R"
+
+local_setup {*
+ typedef_main (@{binding "qtrm"}, @{term "R"}, @{typ trm}, @{thm r_eq}) #> snd
+*}
+
+term Rep_qtrm
+term Abs_qtrm
+term ABS_qtrm
+term REP_qtrm
+thm QUOT_TYPE_qtrm
+thm QUOTIENT_qtrm
+thm Rep_qtrm
+
+text {* another test *}
+datatype 'a my = foo
+consts Rmy :: "'a my \<Rightarrow> 'a my \<Rightarrow> bool"
+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 {*
+ typedef_main (@{binding "qtrm'"}, @{term "R'"}, @{typ "'a trm'"}, @{thm r_eq'}) #> snd
+*}
+
+term ABS_qtrm'
+term REP_qtrm'
+thm QUOT_TYPE_qtrm'
+thm QUOTIENT_qtrm'
+thm Rep_qtrm'
+
+text {* a test with lists of terms *}
+datatype t =
+ vr "string"
+| ap "t list"
+| lm "string" "t"
+
+consts Rt :: "t \<Rightarrow> t \<Rightarrow> bool"
+axioms t_eq: "EQUIV Rt"
+
+local_setup {*
+ typedef_main (@{binding "qt"}, @{term "Rt"}, @{typ "t"}, @{thm t_eq}) #> snd
+*}
+
+section {* lifting of constants *}
+
+text {* information about map-functions for type-constructor *}
+ML {*
+type typ_info = {mapfun: string}
+
+local
+ structure Data = GenericDataFun
+ (type T = typ_info Symtab.table
+ 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 {*
+ Context.theory_map (update @{type_name "list"} {mapfun = @{const_name "map"}})
+ #> Context.theory_map (update @{type_name "*"} {mapfun = @{const_name "prod_fun"}})
+ #> Context.theory_map (update @{type_name "fun"} {mapfun = @{const_name "fun_map"}})
+*}
+
+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))
+ | get_const rep = (Const ("QuotMain.REP_" ^ qty_name, qty --> rty), (qty, rty))
+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))
+ | Type (s, tys) => get_fun_aux s (map (get_fun abs_or_rep rty qty lthy) tys)
+ | _ => raise ERROR ("no variables")
+ )
+end
+*}
+
+ML {*
+fun get_const_def nconst oconst rty qty lthy =
+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
+
+in
+ map (op $) (rep_fns ~~ fresh_args)
+ |> curry list_comb oconst
+ |> curry (op $) abs_fn
+ |> 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
+*}
+
+text {* a test with functions *}
+datatype 'a t' =
+ vr' "string"
+| ap' "('a t') * ('a t')"
+| lm' "'a" "string \<Rightarrow> ('a t')"
+
+consts Rt' :: "('a t') \<Rightarrow> ('a t') \<Rightarrow> bool"
+axioms t_eq': "EQUIV Rt'"
+
+local_setup {*
+ typedef_main (@{binding "qt'"}, @{term "Rt'"}, @{typ "'a t'"}, @{thm t_eq'}) #> snd
+*}
+
+local_setup {*
+ make_const_def "VR'" @{term "vr'"} NoSyn @{typ "'a t'"} @{typ "'a qt'"} #> snd
+*}
+
+local_setup {*
+ make_const_def "AP'" @{term "ap'"} NoSyn @{typ "'a t'"} @{typ "'a qt'"} #> snd
+*}
+
+local_setup {*
+ make_const_def "LM'" @{term "lm'"} NoSyn @{typ "'a t'"} @{typ "'a qt'"} #> snd
+*}
+
+thm VR'_def
+thm AP'_def
+thm LM'_def
+term LM'
+term VR'
+term AP'
+
+text {* finite set example *}
+
+inductive
+ list_eq ("_ \<approx> _")
+where
+ "a#b#xs \<approx> b#a#xs"
+| "[] \<approx> []"
+| "xs \<approx> ys \<Longrightarrow> ys \<approx> xs"
+| "a#a#xs \<approx> a#xs"
+| "xs \<approx> ys \<Longrightarrow> a#xs \<approx> a#ys"
+| "\<lbrakk>xs1 \<approx> xs2; xs2 \<approx> xs3\<rbrakk> \<Longrightarrow> xs1 \<approx> xs3"
+
+lemma list_eq_sym:
+ shows "xs \<approx> xs"
+apply(induct xs)
+apply(auto intro: list_eq.intros)
+done
+
+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_sym)
+done
+
+local_setup {*
+ typedef_main (@{binding "fset"}, @{term "list_eq"}, @{typ "'a list"}, @{thm "equiv_list_eq"}) #> snd
+*}
+
+typ "'a fset"
+thm "Rep_fset"
+
+local_setup {*
+ make_const_def "EMPTY" @{term "[]"} NoSyn @{typ "'a list"} @{typ "'a fset"} #> snd
+*}
+
+term Nil
+term EMPTY
+
+local_setup {*
+ make_const_def "INSERT" @{term "op #"} NoSyn @{typ "'a list"} @{typ "'a fset"} #> snd
+*}
+
+term Cons
+term INSERT
+
+local_setup {*
+ make_const_def "UNION" @{term "op @"} NoSyn @{typ "'a list"} @{typ "'a fset"} #> snd
+*}
+
+term append
+term UNION
+thm QUOTIENT_fset
+thm Insert_def
+
+fun
+ membship :: "'a \<Rightarrow> 'a list \<Rightarrow> bool" ("_ memb _")
+where
+ m1: "(x memb []) = False"
+| m2: "(x memb (y#xs)) = ((x=y) \<or> (x memb xs))"
+
+
+local_setup {*
+ make_const_def "IN" @{term "membship"} NoSyn @{typ "'a list"} @{typ "'a fset"} #> snd
+*}
+
+term membship
+term IN
+
+lemma
+ shows "IN x EMPTY = False"
+unfolding IN_def EMPTY_def
+apply(auto)
+thm Rep_fset_inverse
+
+
+
+
+
+
+
+
+
+
+text {* old stuff *}
+
+
+lemma QUOT_TYPE_qtrm_old:
+ "QUOT_TYPE R Abs_qtrm Rep_qtrm"
+apply(rule QUOT_TYPE.intro)
+apply(rule r_eq)
+apply(rule Rep_qtrm[simplified mem_def])
+apply(rule Rep_qtrm_inverse)
+apply(rule Abs_qtrm_inverse[simplified mem_def])
+apply(rule exI)
+apply(rule refl)
+apply(rule Rep_qtrm_inject)
+done
+
+definition
+ "ABS_qtrm_old \<equiv> QUOT_TYPE.ABS R Abs_qtrm"
+
+definition
+ "REP_qtrm_old \<equiv> QUOT_TYPE.REP Rep_qtrm"
+
+lemma
+ "QUOTIENT R (ABS_qtrm) (REP_qtrm)"
+apply(simp add: ABS_qtrm_def REP_qtrm_def)
+apply(rule QUOT_TYPE.QUOTIENT)
+apply(rule QUOT_TYPE_qtrm)
+done
+
+term "var"
+term "app"
+term "lam"
+
+definition
+ "VAR x \<equiv> ABS_qtrm (var x)"
+
+definition
+ "APP t1 t2 \<equiv> ABS_qtrm (app (REP_qtrm t1) (REP_qtrm t2))"
+
+definition
+ "LAM x t \<equiv> ABS_qtrm (lam x (REP_qtrm t))"
+
+
+
+
+definition
+ "VR x \<equiv> ABS_qt (vr x)"
+
+definition
+ "AP ts \<equiv> ABS_qt (ap (map REP_qt ts))"
+
+definition
+ "LM x t \<equiv> ABS_qt (lm x (REP_qt t))"
+
+(* for printing types *)
+ML {*
+fun setmp_show_all_types f =
+ setmp show_all_types
+ (! show_types orelse ! show_sorts orelse ! show_all_types) f
+*}
\ No newline at end of file