--- a/Quot/Examples/AbsRepTest.thy Fri Dec 25 00:58:06 2009 +0100
+++ b/Quot/Examples/AbsRepTest.thy Sat Dec 26 07:15:30 2009 +0100
@@ -2,21 +2,87 @@
imports "../QuotMain" "../QuotList" "../QuotOption" "../QuotSum" "../QuotProd" List
begin
+ML {* open Quotient_Term *}
+
print_maps
+
quotient_type
'a fset = "'a list" / "\<lambda>xs ys. \<forall>e. e \<in> set xs \<longleftrightarrow> e \<in> set ys"
apply(rule equivpI)
unfolding reflp_def symp_def transp_def
- apply(auto)
- done
+ by auto
quotient_type
'a foo = "('a * 'a) list" / "\<lambda>(xs::('a * 'a) list) ys. \<forall>e. e \<in> set xs \<longleftrightarrow> e \<in> set ys"
apply(rule equivpI)
unfolding reflp_def symp_def transp_def
- apply(auto)
- done
+ by auto
+
+quotient_type
+ 'a bar = "('a * int) list" / "\<lambda>(xs::('a * int) list) ys. \<forall>e. e \<in> set xs \<longleftrightarrow> e \<in> set ys"
+ apply(rule equivpI)
+ unfolding reflp_def symp_def transp_def
+ by auto
+
+fun
+ intrel :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> bool"
+where
+ "intrel (x, y) (u, v) = (x + v = u + y)"
+
+quotient_type int = "nat \<times> nat" / intrel
+ by (auto simp add: equivp_def expand_fun_eq)
+
+print_quotients
+
+ML {*
+absrep_fun_chk absF @{context}
+ (@{typ "('a * 'a) list"},
+ @{typ "'a foo"})
+|> Syntax.string_of_term @{context}
+|> writeln
+*}
+
+(* PROBLEM
+ML {*
+absrep_fun_chk absF @{context}
+ (@{typ "(('a list) * int) list"},
+ @{typ "('a fset) bar"})
+|> Syntax.string_of_term @{context}
+|> writeln
+*}*)
+
+ML {*
+absrep_fun_chk absF @{context}
+ (@{typ "('a list) list"},
+ @{typ "('a fset) fset"})
+|> Syntax.string_of_term @{context}
+|> writeln
+*}
+
+ML {*
+absrep_fun_chk absF @{context}
+ (@{typ "nat \<times> nat"},
+ @{typ "int"})
+|> Syntax.string_of_term @{context}
+|> writeln
+*}
+
+
+term abs_foo
+term rep_foo
+term "abs_foo o map (prod_fun id id)"
+term "map (prod_fun id id) o rep_foo"
+
+ML {*
+absrep_fun_chk absF @{context}
+ (@{typ "('a * 'a) list"},
+ @{typ "'a foo"})
+|> Syntax.string_of_term @{context}
+|> writeln
+*}
+
+typ "('a fset) foo"
print_quotients
@@ -24,12 +90,6 @@
Quotient_Info.quotient_rules_get @{context}
*}
-quotient_type int = "nat \<times> nat" / "\<lambda>(x, y) (u, v). x + v = u + (y::nat)"
- apply(rule equivpI)
- unfolding reflp_def symp_def transp_def
- apply(auto)
- done
-
print_quotients
ML {*
--- a/Quot/Examples/IntEx2.thy Fri Dec 25 00:58:06 2009 +0100
+++ b/Quot/Examples/IntEx2.thy Sat Dec 26 07:15:30 2009 +0100
@@ -1,5 +1,5 @@
theory IntEx2
-imports "../QuotMain" Nat
+imports "../QuotMain" "../QuotProd" Nat
(*uses
("Tools/numeral.ML")
("Tools/numeral_syntax.ML")
@@ -196,7 +196,7 @@
lemma add:
"(abs_int (x,y)) + (abs_int (u,v)) =
(abs_int (x + u, y + v))"
-apply(simp add: plus_int_def)
+apply(simp add: plus_int_def id_simps)
apply(fold plus_raw.simps)
apply(rule Quotient_rel_abs[OF Quotient_int])
apply(rule plus_raw_rsp_aux)
--- a/Quot/Examples/LarryInt.thy Fri Dec 25 00:58:06 2009 +0100
+++ b/Quot/Examples/LarryInt.thy Sat Dec 26 07:15:30 2009 +0100
@@ -2,7 +2,7 @@
header{*The Integers as Equivalence Classes over Pairs of Natural Numbers*}
theory LarryInt
-imports Nat "../QuotMain"
+imports Nat "../QuotMain" "../QuotProd"
begin
fun
@@ -361,22 +361,6 @@
apply(auto iff: nat_raw_def)
done
-ML {*
- let
- val parser = Args.context -- Scan.lift Args.name_source
- fun term_pat (ctxt, str) =
- str |> ProofContext.read_term_pattern ctxt
- |> ML_Syntax.print_term
- |> ML_Syntax.atomic
-in
- ML_Antiquote.inline "term_pat" (parser >> term_pat)
-end
-
-*}
-
-consts test::"'b \<Rightarrow> 'b \<Rightarrow> 'b"
-
-
lemma nat_le_eq_zle: "0 < w \<or> 0 \<le> z \<Longrightarrow> (nat2 w \<le> nat2 z) = (w\<le>z)"
unfolding less_int_def
apply(lifting nat_le_eq_zle_raw)
--- a/Quot/quotient_term.ML Fri Dec 25 00:58:06 2009 +0100
+++ b/Quot/quotient_term.ML Sat Dec 26 07:15:30 2009 +0100
@@ -34,27 +34,59 @@
fun negF absF = repF
| negF repF = absF
+val mk_id = Const (@{const_name "id"}, dummyT)
fun mk_identity ty = Const (@{const_name "id"}, ty --> ty)
+fun mk_Free (TVar ((x, i), _)) = Free (unprefix "'" x ^ string_of_int i, dummyT)
+
fun mk_compose flag (trm1, trm2) =
case flag of
absF => Const (@{const_name "comp"}, dummyT) $ trm1 $ trm2
| repF => Const (@{const_name "comp"}, dummyT) $ trm2 $ trm1
-fun get_map ctxt ty_str =
+fun get_mapfun ctxt s =
let
val thy = ProofContext.theory_of ctxt
- val exc = LIFT_MATCH (space_implode " " ["absrep_fun: no map for type", quote ty_str, "."])
- val mapfun = #mapfun (maps_lookup thy ty_str) handle NotFound => raise exc
+ val exc = LIFT_MATCH ("No map function for type " ^ (quote s) ^ " found.")
+ val mapfun = #mapfun (maps_lookup thy s) handle NotFound => raise exc
in
Const (mapfun, dummyT)
end
-fun get_absrep_const flag ctxt _ qty =
-(* FIXME: check here that the type-constructors of _ and qty are related *)
+fun mk_mapfun ctxt vs ty =
+let
+ val vs' = map (mk_Free) vs
+
+ fun mk_mapfun_aux ty =
+ case ty of
+ TVar _ => mk_Free ty
+ | Type (_, []) => mk_id
+ | Type (s, tys) => list_comb (get_mapfun ctxt s, map mk_mapfun_aux tys)
+ | _ => raise LIFT_MATCH ("mk_mapfun_aux (default)")
+in
+ fold_rev Term.lambda vs' (mk_mapfun_aux ty)
+end
+
+fun get_rty_qty ctxt s =
let
val thy = ProofContext.theory_of ctxt
- val qty_name = Long_Name.base_name (fst (dest_Type qty))
+ val exc = LIFT_MATCH ("No quotient type " ^ (quote s) ^ " found.")
+ val qdata = (quotdata_lookup thy s) handle NotFound => raise exc
+in
+ (#rtyp qdata, #qtyp qdata)
+end
+
+fun double_lookup rtyenv qtyenv v =
+let
+ val v' = fst (dest_TVar v)
+in
+ (snd (the (Vartab.lookup rtyenv v')), snd (the (Vartab.lookup qtyenv v')))
+end
+
+fun absrep_const flag ctxt qty_str =
+let
+ val thy = ProofContext.theory_of ctxt
+ val qty_name = Long_Name.base_name qty_str
in
case flag of
absF => Const (Sign.full_bname thy ("abs_" ^ qty_name), dummyT)
@@ -62,39 +94,62 @@
end
fun absrep_fun flag ctxt (rty, qty) =
- if rty = qty then mk_identity qty else
- case (rty, qty) of
- (Type ("fun", [ty1, ty2]), Type ("fun", [ty1', ty2'])) =>
- let
- val arg1 = absrep_fun (negF flag) ctxt (ty1, ty1')
- val arg2 = absrep_fun flag ctxt (ty2, ty2')
- in
- list_comb (get_map ctxt "fun", [arg1, arg2])
- end
- | (Type (s, _), Type (s', [])) =>
- if s = s'
- then mk_identity qty
- else get_absrep_const flag ctxt rty qty
- | (Type (s, tys), Type (s', tys')) =>
- let
- val args = map (absrep_fun flag ctxt) (tys ~~ tys')
- val result = list_comb (get_map ctxt s, args)
- in
+ if rty = qty
+ then mk_identity qty
+ else
+ case (rty, qty) of
+ (Type ("fun", [ty1, ty2]), Type ("fun", [ty1', ty2'])) =>
+ let
+ val arg1 = absrep_fun (negF flag) ctxt (ty1, ty1')
+ val arg2 = absrep_fun flag ctxt (ty2, ty2')
+ in
+ list_comb (get_mapfun ctxt "fun", [arg1, arg2])
+ end
+ | (Type (s, tys), Type (s', tys')) =>
if s = s'
- then result
- else mk_compose flag (get_absrep_const flag ctxt rty qty, result)
- end
- | (TFree x, TFree x') =>
- if x = x'
- then mk_identity qty
- else raise (LIFT_MATCH "absrep_fun (frees)")
- | (TVar _, TVar _) => raise (LIFT_MATCH "absrep_fun (vars)")
- | _ => raise (LIFT_MATCH "absrep_fun (default)")
+ then
+ let
+ val args = map (absrep_fun flag ctxt) (tys ~~ tys')
+ in
+ list_comb (get_mapfun ctxt s, args)
+ end
+ else
+ let
+ val thy = ProofContext.theory_of ctxt
+ val (rty_pat, qty_pat as Type (_, vs)) = get_rty_qty ctxt s'
+ val rtyenv = Sign.typ_match thy (rty_pat, rty) Vartab.empty
+ val qtyenv = Sign.typ_match thy (qty_pat, qty) Vartab.empty
+ val args_aux = map (double_lookup rtyenv qtyenv) vs
+ val args = map (absrep_fun flag ctxt) args_aux
+ val map_fun = mk_mapfun ctxt vs rty_pat
+ val result = list_comb (map_fun, args)
+ in
+ mk_compose flag (absrep_const flag ctxt s', result)
+ end
+ | (TFree x, TFree x') =>
+ if x = x'
+ then mk_identity qty
+ else raise (LIFT_MATCH "absrep_fun (frees)")
+ | (TVar _, TVar _) => raise (LIFT_MATCH "absrep_fun (vars)")
+ | _ =>
+ let
+ val rty_str = Syntax.string_of_typ ctxt rty
+ val qty_str = Syntax.string_of_typ ctxt qty
+ in
+ raise (LIFT_MATCH ("absrep_fun (default) " ^ rty_str ^ " " ^ qty_str))
+ end
fun absrep_fun_chk flag ctxt (rty, qty) =
+let
+ val rty_str = Syntax.string_of_typ ctxt rty
+ val qty_str = Syntax.string_of_typ ctxt qty
+ val _ = tracing "rty / qty"
+ val _ = tracing rty_str
+ val _ = tracing qty_str
+in
absrep_fun flag ctxt (rty, qty)
|> Syntax.check_term ctxt
-
+end
(* Regularizing an rtrm means:
--- a/Quot/quotient_typ.ML Fri Dec 25 00:58:06 2009 +0100
+++ b/Quot/quotient_typ.ML Sat Dec 26 07:15:30 2009 +0100
@@ -39,6 +39,7 @@
end
+(********************************)
(* definition of quotient types *)
(********************************)
@@ -52,11 +53,11 @@
|> Variable.variant_frees lthy [rel]
|> map Free
in
- lambda c
- (HOLogic.exists_const rty $
- lambda x (HOLogic.mk_eq (c, (rel $ x))))
+ lambda c (HOLogic.exists_const rty $
+ lambda x (HOLogic.mk_eq (c, (rel $ x))))
end
+
(* makes the new type definitions and proves non-emptyness *)
fun typedef_make (vs, qty_name, mx, rel, rty) lthy =
let
@@ -69,10 +70,11 @@
Local_Theory.theory_result
(Typedef.add_typedef false NONE
(qty_name, vs, mx)
- (typedef_term rel rty lthy)
- NONE typedef_tac) lthy
+ (typedef_term rel rty lthy)
+ NONE typedef_tac) lthy
end
+
(* tactic to prove the Quot_Type theorem for the new type *)
fun typedef_quot_type_tac equiv_thm (typedef_info: Typedef.info) =
let
@@ -89,6 +91,7 @@
rtac rep_inj]) 1
end
+
(* proves the Quot_Type theorem *)
fun typedef_quot_type_thm (rel, abs, rep, equiv_thm, typedef_info) lthy =
let
@@ -116,6 +119,7 @@
(K typedef_quotient_thm_tac)
end
+
(* main function for constructing a quotient type *)
fun mk_typedef_main (((vs, qty_name, mx), (rty, rel)), equiv_thm) lthy =
let
@@ -164,6 +168,7 @@
||>> note (equiv_thm_name, equiv_thm, [intern_attr equiv_rules_add])
end
+
(* sanity checks of the quotient type specifications *)
fun sanity_check ((vs, qty_name, _), (rty, rel)) =
let
@@ -203,7 +208,10 @@
if null errs then () else error (cat_lines errs)
end
+
+(******************************)
(* interface and syntax setup *)
+(******************************)
(* the ML-interface takes a list of 5-tuples consisting of *)
(* *)