
diff -r 34ad627ac5d5 -r 37636f2b1c19 QuotMain.thy
--- 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 *}




