--- a/FIXME-TODO Wed Jan 27 08:20:31 2010 +0100
+++ b/FIXME-TODO Wed Jan 27 08:41:42 2010 +0100
@@ -1,6 +1,10 @@
Highest Priority
================
+- give examples for the new quantifier translations in regularization
+ (quotient_term.ML)
+
+
Higher Priority
===============
--- a/Quot/quotient_def.ML Wed Jan 27 08:20:31 2010 +0100
+++ b/Quot/quotient_def.ML Wed Jan 27 08:41:42 2010 +0100
@@ -1,3 +1,9 @@
+(* Title: quotient_def.thy
+ Author: Cezary Kaliszyk and Christian Urban
+
+ Definitions for constants on quotient types.
+
+*)
signature QUOTIENT_DEF =
sig
--- a/Quot/quotient_info.ML Wed Jan 27 08:20:31 2010 +0100
+++ b/Quot/quotient_info.ML Wed Jan 27 08:41:42 2010 +0100
@@ -1,3 +1,11 @@
+(* Title: quotient_info.thy
+ Author: Cezary Kaliszyk and Christian Urban
+
+ Data slots for the quotient package.
+
+*)
+
+
signature QUOTIENT_INFO =
sig
exception NotFound
--- a/Quot/quotient_tacs.ML Wed Jan 27 08:20:31 2010 +0100
+++ b/Quot/quotient_tacs.ML Wed Jan 27 08:41:42 2010 +0100
@@ -1,3 +1,10 @@
+(* Title: quotient_tacs.thy
+ Author: Cezary Kaliszyk and Christian Urban
+
+ Tactics for solving goal arising from lifting
+ theorems to quotient types.
+*)
+
signature QUOTIENT_TACS =
sig
val regularize_tac: Proof.context -> int -> tactic
--- a/Quot/quotient_term.ML Wed Jan 27 08:20:31 2010 +0100
+++ b/Quot/quotient_term.ML Wed Jan 27 08:41:42 2010 +0100
@@ -1,11 +1,16 @@
+(* Title: quotient_term.thy
+ Author: Cezary Kaliszyk and Christian Urban
+
+ Constructs terms corresponding to goals from
+ lifting theorems to quotient types.
+*)
+
signature QUOTIENT_TERM =
sig
exception LIFT_MATCH of string
datatype flag = absF | repF
- val absrep_const_chk: flag -> Proof.context -> string -> term
-
val absrep_fun: flag -> Proof.context -> typ * typ -> term
val absrep_fun_chk: flag -> Proof.context -> typ * typ -> term
@@ -128,9 +133,6 @@
| repF => Const (Sign.full_bname thy ("rep_" ^ qty_name), dummyT)
end
-fun absrep_const_chk flag ctxt qty_str =
- Syntax.check_term ctxt (absrep_const flag ctxt qty_str)
-
fun absrep_match_err ctxt ty_pat ty =
let
val ty_pat_str = Syntax.string_of_typ ctxt ty_pat
@@ -434,13 +436,14 @@
else mk_ball $ (mk_resp $ equiv_relation ctxt (qnt_typ ty, qnt_typ ty')) $ subtrm
end
- | (Const (@{const_name "Ball"}, ty) $ (Const (@{const_name "Respects"}, _) $ resrel) $ t, Const (@{const_name "All"}, ty') $ t') =>
+ | (Const (@{const_name "Ball"}, ty) $ (Const (@{const_name "Respects"}, _) $ resrel) $ t,
+ Const (@{const_name "All"}, ty') $ t') =>
let
val subtrm = apply_subt (regularize_trm ctxt) (t, t')
- val needrel = Syntax.check_term ctxt (equiv_relation ctxt (qnt_typ ty, qnt_typ ty'))
+ val needrel = equiv_relation_chk ctxt (qnt_typ ty, qnt_typ ty')
in
if resrel <> needrel
- then term_mismatch "regularize(ball)" ctxt resrel needrel
+ then term_mismatch "regularize (Ball)" ctxt resrel needrel
else mk_ball $ (mk_resp $ resrel) $ subtrm
end
@@ -452,13 +455,14 @@
else mk_bex $ (mk_resp $ equiv_relation ctxt (qnt_typ ty, qnt_typ ty')) $ subtrm
end
- | (Const (@{const_name "Bex"}, ty) $ (Const (@{const_name "Respects"}, _) $ resrel) $ t, Const (@{const_name "Ex"}, ty') $ t') =>
+ | (Const (@{const_name "Bex"}, ty) $ (Const (@{const_name "Respects"}, _) $ resrel) $ t,
+ Const (@{const_name "Ex"}, ty') $ t') =>
let
val subtrm = apply_subt (regularize_trm ctxt) (t, t')
- val needrel = Syntax.check_term ctxt (equiv_relation ctxt (qnt_typ ty, qnt_typ ty'))
+ val needrel = equiv_relation_chk ctxt (qnt_typ ty, qnt_typ ty')
in
if resrel <> needrel
- then term_mismatch "regularize(bex)" ctxt resrel needrel
+ then term_mismatch "regularize (Bex)" ctxt resrel needrel
else mk_bex $ (mk_resp $ resrel) $ subtrm
end
@@ -473,20 +477,21 @@
| (Const (@{const_name "Bexeq"}, ty) $ resrel $ t, Const (@{const_name "Ex1"}, ty') $ t') =>
let
val subtrm = apply_subt (regularize_trm ctxt) (t, t')
- val needrel = Syntax.check_term ctxt (equiv_relation ctxt (qnt_typ ty, qnt_typ ty'))
+ val needrel = equiv_relation_chk ctxt (qnt_typ ty, qnt_typ ty')
in
if resrel <> needrel
- then term_mismatch "regularize(bex1_res)" ctxt resrel needrel
+ then term_mismatch "regularize (Bex1_res)" ctxt resrel needrel
else mk_bexeq $ resrel $ subtrm
end
- | (Const (@{const_name "Bex1"}, ty) $ (Const (@{const_name "Respects"}, _) $ resrel) $ t, Const (@{const_name "Ex1"}, ty') $ t') =>
+ | (Const (@{const_name "Bex1"}, ty) $ (Const (@{const_name "Respects"}, _) $ resrel) $ t,
+ Const (@{const_name "Ex1"}, ty') $ t') =>
let
val subtrm = apply_subt (regularize_trm ctxt) (t, t')
- val needrel = Syntax.check_term ctxt (equiv_relation ctxt (qnt_typ ty, qnt_typ ty'))
+ val needrel = equiv_relation_chk ctxt (qnt_typ ty, qnt_typ ty')
in
if resrel <> needrel
- then term_mismatch "regularize(bex1)" ctxt resrel needrel
+ then term_mismatch "regularize (Bex1)" ctxt resrel needrel
else mk_bexeq $ resrel $ subtrm
end
@@ -501,7 +506,8 @@
val rel_ty = fastype_of rel
val rel' = equiv_relation_chk ctxt (domain_type rel_ty, domain_type ty')
in
- if rel' aconv rel then rtrm else term_mismatch "regularise (relation mismatch)" ctxt rel rel'
+ if rel' aconv rel then rtrm
+ else term_mismatch "regularise (relation mismatch)" ctxt rel rel'
end
| (_, Const _) =>
--- a/Quot/quotient_typ.ML Wed Jan 27 08:20:31 2010 +0100
+++ b/Quot/quotient_typ.ML Wed Jan 27 08:41:42 2010 +0100
@@ -1,3 +1,10 @@
+(* Title: quotient_typ.thy
+ Author: Cezary Kaliszyk and Christian Urban
+
+ Definition of a quotient type.
+
+*)
+
signature QUOTIENT_TYPE =
sig
val quotient_type: ((string list * binding * mixfix) * (typ * term)) list