--- a/QuotMain.thy Wed Nov 04 10:43:33 2009 +0100
+++ b/QuotMain.thy Wed Nov 04 11:59:15 2009 +0100
@@ -2,10 +2,9 @@
imports QuotScript QuotList Prove
uses ("quotient_info.ML")
("quotient.ML")
+ ("quotient_def.ML")
begin
-ML {* Attrib.empty_binding *}
-
locale QUOT_TYPE =
fixes R :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
and Abs :: "('a \<Rightarrow> bool) \<Rightarrow> 'b"
@@ -143,7 +142,6 @@
(* the auxiliary data for the quotient types *)
use "quotient_info.ML"
-
declare [[map list = (map, LIST_REL)]]
declare [[map * = (prod_fun, prod_rel)]]
declare [[map "fun" = (fun_map, FUN_REL)]]
@@ -154,9 +152,14 @@
(* definition of the quotient types *)
+(* FIXME: should be called quotient_typ.ML *)
use "quotient.ML"
+(* lifting of constants *)
+use "quotient_def.ML"
+
+
text {* FIXME: auxiliary function *}
ML {*
val no_vars = Thm.rule_attribute (fn context => fn th =>
@@ -166,182 +169,6 @@
in th' end);
*}
-section {* lifting of constants *}
-
-ML {*
-
-fun lookup_qenv qenv qty =
- (case (AList.lookup (op=) qenv qty) of
- SOME rty => SOME (qty, rty)
- | NONE => NONE)
-*}
-
-ML {*
-(* calculates the aggregate abs and rep functions for a given type;
- repF is for constants' arguments; absF is for constants;
- function types need to be treated specially, since repF and absF
- change
-*)
-datatype flag = absF | repF
-
-fun negF absF = repF
- | negF repF = absF
-
-fun get_fun flag qenv lthy ty =
-let
-
- 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 (maps_lookup (ProofContext.theory_of lthy) s) of
- SOME info => (list_comb (Const (#mapfun info, ftys ---> (oty --> nty)), fs), (oty, nty))
- | NONE => error ("no map association for type " ^ s))
- end
-
- fun get_fun_fun fs_tys =
- let
- val (fs, tys) = split_list fs_tys
- val ([oty1, oty2], [nty1, nty2]) = split_list tys
- val oty = nty1 --> oty2
- val nty = oty1 --> nty2
- val ftys = map (op -->) tys
- in
- (list_comb (Const (@{const_name "fun_map"}, ftys ---> oty --> nty), fs), (oty, nty))
- end
-
- fun get_const flag (qty, rty) =
- let
- val thy = ProofContext.theory_of lthy
- val qty_name = Long_Name.base_name (fst (dest_Type qty))
- in
- case flag of
- absF => (Const (Sign.full_bname thy ("ABS_" ^ qty_name), rty --> qty), (rty, qty))
- | repF => (Const (Sign.full_bname thy ("REP_" ^ qty_name), qty --> rty), (qty, rty))
- end
-
- fun mk_identity ty = Abs ("", ty, Bound 0)
-
-in
- if (AList.defined (op=) qenv ty)
- then (get_const flag (the (lookup_qenv qenv ty)))
- else (case ty of
- TFree _ => (mk_identity ty, (ty, ty))
- | Type (_, []) => (mk_identity ty, (ty, ty))
- | Type ("fun" , [ty1, ty2]) =>
- get_fun_fun [get_fun (negF flag) qenv lthy ty1, get_fun flag qenv lthy ty2]
- | Type (s, tys) => get_fun_aux s (map (get_fun flag qenv lthy) tys)
- | _ => raise ERROR ("no type variables")
- )
-end
-*}
-
-ML {*
-fun make_def nconst_bname rhs qty mx qenv lthy =
-let
- val (arg_tys, res_ty) = strip_type qty
-
- val rep_fns = map (fst o get_fun repF qenv lthy) arg_tys
- val abs_fn = (fst o get_fun absF qenv lthy) res_ty
-
- fun mk_fun_map t s =
- Const (@{const_name "fun_map"}, dummyT) $ t $ s
-
- val absrep_fn = fold_rev mk_fun_map rep_fns abs_fn
- |> Syntax.check_term lthy
-in
- define (nconst_bname, mx, absrep_fn $ rhs) lthy
-end
-*}
-
-ML {*
-(* returns all subterms where two types differ *)
-fun diff (T, S) Ds =
- case (T, S) of
- (TVar v, TVar u) => if v = u then Ds else (T, S)::Ds
- | (TFree x, TFree y) => if x = y then Ds else (T, S)::Ds
- | (Type (a, Ts), Type (b, Us)) =>
- if a = b then diffs (Ts, Us) Ds else (T, S)::Ds
- | _ => (T, S)::Ds
-and diffs (T::Ts, U::Us) Ds = diffs (Ts, Us) (diff (T, U) Ds)
- | diffs ([], []) Ds = Ds
- | diffs _ _ = error "Unequal length of type arguments"
-*}
-
-ML {*
-fun error_msg lthy (qty, rty) =
-let
- val qtystr = quote (Syntax.string_of_typ lthy qty)
- val rtystr = quote (Syntax.string_of_typ lthy rty)
-in
- error (implode ["Quotient type ", qtystr, " does not match with ", rtystr])
-end
-
-
-fun sanity_chk lthy qenv =
-let
- val qenv' = Quotient_Info.mk_qenv lthy
- val thy = ProofContext.theory_of lthy
-
- fun is_inst thy (qty, rty) (qty', rty') =
- if Sign.typ_instance thy (qty, qty')
- then let
- val inst = Sign.typ_match thy (qty', qty) Vartab.empty
- in
- rty = Envir.subst_type inst rty'
- end
- else false
-
- fun chk_inst (qty, rty) =
- if exists (is_inst thy (qty, rty)) qenv' then true
- else error_msg lthy (qty, rty)
-in
- forall chk_inst qenv
-end
-*}
-
-ML {*
-fun quotdef ((bind, qty, mx), (attr, prop)) lthy =
-let
- val (_, prop') = PrimitiveDefs.dest_def lthy (K true) (K false) (K false) prop
- val (_, rhs) = PrimitiveDefs.abs_def prop'
-
- val rty = fastype_of rhs
- val qenv = distinct (op=) (diff (qty, rty) [])
-
-in
- sanity_chk lthy qenv;
- make_def bind rhs qty mx qenv lthy
-end
-*}
-
-ML {*
-val quotdef_parser =
- (OuterParse.binding --
- (OuterParse.$$$ "::" |-- OuterParse.!!! (OuterParse.typ --
- OuterParse.opt_mixfix' --| OuterParse.where_)) >> OuterParse.triple2) --
- (SpecParse.opt_thm_name ":" -- OuterParse.prop)
-*}
-
-ML {*
-fun quotdef_cmd ((bind, qtystr, mx), (attr, propstr)) lthy =
-let
- val qty = (Syntax.check_typ lthy o Syntax.parse_typ lthy) qtystr
- val prop = (Syntax.check_prop lthy o Syntax.parse_prop lthy) propstr
-in
- quotdef ((bind, qty, mx), (attr, prop)) lthy |> snd
-end
-*}
-
-ML {*
-val _ = OuterSyntax.local_theory "quotient_def" "lifted definition of constants"
- OuterKeyword.thy_decl (quotdef_parser >> quotdef_cmd)
-*}
-
section {* ATOMIZE *}
text {*
@@ -522,10 +349,12 @@
(my_reg lthy rel rty (prop_of thm)))
*}
-lemma universal_twice: "(\<And>x. (P x \<longrightarrow> Q x)) \<Longrightarrow> ((\<forall>x. P x) \<longrightarrow> (\<forall>x. Q x))"
+lemma universal_twice:
+ "(\<And>x. (P x \<longrightarrow> Q x)) \<Longrightarrow> ((\<forall>x. P x) \<longrightarrow> (\<forall>x. Q x))"
by auto
-lemma implication_twice: "(c \<longrightarrow> a) \<Longrightarrow> (a \<Longrightarrow> b \<longrightarrow> d) \<Longrightarrow> (a \<longrightarrow> b) \<longrightarrow> (c \<longrightarrow> d)"
+lemma implication_twice:
+ "(c \<longrightarrow> a) \<Longrightarrow> (a \<Longrightarrow> b \<longrightarrow> d) \<Longrightarrow> (a \<longrightarrow> b) \<longrightarrow> (c \<longrightarrow> d)"
by auto
(*lemma equality_twice: "a = c \<Longrightarrow> b = d \<Longrightarrow> (a = b \<longrightarrow> c = d)"
@@ -573,12 +402,13 @@
)
*}
+
ML {*
fun old_get_fun flag rty qty lthy ty =
get_fun flag [(qty, rty)] lthy ty
fun old_make_const_def nconst_bname otrm mx rty qty lthy =
- make_def nconst_bname otrm qty mx [(qty, rty)] lthy
+ make_def nconst_bname otrm qty mx Attrib.empty_binding [(qty, rty)] lthy
*}
text {* Does the same as 'subst' in a given prop or theorem *}