QuotMain.thy
changeset 254 77ff9624cfd6
parent 252 e30997c88050
child 255 264c7b9d19f4
--- a/QuotMain.thy	Fri Oct 30 19:03:53 2009 +0100
+++ b/QuotMain.thy	Mon Nov 02 09:33:48 2009 +0100
@@ -159,17 +159,13 @@
 section {* lifting of constants *}
 
 ML {*
-(* whether ty1 is an instance of ty2 *)
-fun matches (ty1, ty2) =
-  Type.raw_instance (ty1, Logic.varifyT ty2)
-
 fun lookup_snd _ [] _ = NONE
   | lookup_snd eq ((value, key)::xs) key' =
       if eq (key', key) then SOME value
       else lookup_snd eq xs key';
 
 fun lookup_qenv qenv qty =
-  (case (AList.lookup matches qenv qty) of
+  (case (AList.lookup (op =) qenv qty) of
     SOME rty => SOME (qty, rty)
   | NONE => NONE)
 *}
@@ -225,7 +221,7 @@
   fun mk_identity ty = Abs ("", ty, Bound 0)
 
 in
-  if (AList.defined matches qenv ty)
+  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))
@@ -259,11 +255,10 @@
 end
 *}
 
-ML {* lookup_snd *}
 
 ML {*
 fun exchange_ty qenv ty =
-  case (lookup_snd matches qenv ty) of
+  case (lookup_snd (op =) qenv ty) of
     SOME qty => qty
   | NONE =>
     (case ty of
@@ -272,6 +267,18 @@
     )
 *}
 
+ML {* 
+fun ppair lthy (ty1, ty2) =
+  "(" ^ (Syntax.string_of_typ lthy ty1) ^ "," ^ (Syntax.string_of_typ lthy ty2) ^ ")"
+*}
+
+ML {*
+fun print_env qenv lthy =
+  map (ppair lthy) qenv
+  |> commas
+  |> tracing
+*}
+
 ML {*
 fun make_const_def nconst_bname otrm mx qenv lthy =
 let
@@ -279,6 +286,11 @@
   val nconst_ty = exchange_ty qenv otrm_ty
   val nconst = Const (Binding.name_of nconst_bname, nconst_ty)
   val def_trm = get_const_def nconst otrm qenv lthy
+
+  val _ = print_env qenv lthy
+  val _ = Syntax.string_of_typ lthy otrm_ty |> tracing
+  val _ = Syntax.string_of_typ lthy nconst_ty |> tracing
+  val _ = Syntax.string_of_term lthy def_trm |> tracing
 in
   define (nconst_bname, mx, def_trm) lthy
 end
@@ -288,46 +300,37 @@
 fun build_qenv lthy qtys = 
 let
   val qenv = map (fn {qtyp, rtyp, ...} => (qtyp, rtyp)) (quotdata_lookup lthy)
-
-  fun find_assoc qty =
-    case (AList.lookup matches qenv qty) of
-      SOME rty => (qty, rty)
-    | NONE => error (implode 
-              ["Quotient type ",     
-               quote (Syntax.string_of_typ lthy qty), 
-               " does not exists"])
+  val tsig = Sign.tsig_of (ProofContext.theory_of lthy)
+  
+  fun find_assoc ((qty', rty')::rest) qty =
+        let 
+          val inst = Type.typ_match tsig (qty', qty) Vartab.empty
+        in
+           (Envir.norm_type inst qty, Envir.norm_type inst rty')
+        end
+    | find_assoc [] qty =
+        let 
+          val qtystr =  quote (Syntax.string_of_typ lthy qty)
+        in
+          error (implode ["Quotient type ", qtystr, " does not exists"])
+        end
 in
-  map find_assoc qtys
+  map (find_assoc qenv) qtys
 end
 *}
 
 ML {*
-(* taken from isar_syn.ML *)
-val constdecl =
-  OuterParse.binding --
-    (OuterParse.where_ >> K (NONE, NoSyn) ||
-      OuterParse.$$$ "::" |-- OuterParse.!!! ((OuterParse.typ >> SOME) -- 
-      OuterParse.opt_mixfix' --| OuterParse.where_) ||
-      Scan.ahead (OuterParse.$$$ "(") |-- 
-      OuterParse.!!! (OuterParse.mixfix' --| OuterParse.where_ >> pair NONE))
-*}
-
-ML {*
 val qd_parser = 
   (Args.parens (OuterParse.$$$ "for" |-- (Scan.repeat OuterParse.typ))) --
-    (constdecl -- (SpecParse.opt_thm_name ":" -- OuterParse.prop))
-*}
-
-ML {* 
-fun pair lthy (ty1, ty2) =
-  "(" ^ (Syntax.string_of_typ lthy ty1) ^ "," ^ (Syntax.string_of_typ lthy ty2) ^ ")"
+    (SpecParse.constdecl -- (SpecParse.opt_thm_name ":" -- OuterParse.prop))
 *}
 
 ML {*
-fun parse_qd_spec (qtystrs, ((bind, (typstr__, mx)), (attr__, propstr))) lthy = 
+fun parse_qd_spec (qtystrs, ((bind, tystr, mx), (attr__, propstr))) lthy = 
 let
   val qtys = map (Syntax.check_typ lthy o Syntax.parse_typ lthy) qtystrs
   val qenv = build_qenv lthy qtys
+  val qty = Syntax.parse_typ lthy (the tystr) |> Syntax.check_typ lthy
   val prop = Syntax.parse_prop lthy propstr |> Syntax.check_prop lthy
   val (lhs, rhs) = Logic.dest_equals prop
 in
@@ -340,6 +343,8 @@
   OuterKeyword.thy_decl (qd_parser >> parse_qd_spec)
 *}
 
+(* ML {* show_all_types := true *} *)
+
 section {* ATOMIZE *}
 
 text {*
@@ -501,10 +506,6 @@
          else
            Const (@{const_name "Ex"}, ty) $ apply_subt (my_reg lthy rel rty) t
        end
-  | Const (@{const_name "op ="}, ty) $ t =>
-      if needs_lift rty (fastype_of t) then
-        (tyRel (fastype_of t) rty rel lthy) $ t
-      else Const (@{const_name "op ="}, ty) $ (my_reg lthy rel rty t)
   | t1 $ t2 => (my_reg lthy rel rty t1) $ (my_reg lthy rel rty t2)
   | _ => trm
 *}
@@ -517,31 +518,16 @@
        (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))"
-apply (auto)
-done
-
-lemma implication_twice: "(c \<longrightarrow> a) \<Longrightarrow> (a \<Longrightarrow> b \<longrightarrow> d) \<Longrightarrow> (a \<longrightarrow> b) \<longrightarrow> (c \<longrightarrow> d)"
-apply (auto)
-done
-
 ML {*
-fun regularize thm rty rel rel_eqv rel_refl lthy =
+fun regularize thm rty rel rel_eqv lthy =
   let
     val g = build_regularize_goal thm rty rel lthy;
     fun tac ctxt =
-      (ObjectLogic.full_atomize_tac) THEN'
-     REPEAT_ALL_NEW (FIRST' [
-      rtac rel_refl,
-      atac,
-      rtac @{thm universal_twice},
-      rtac @{thm implication_twice},
-      (fn i => CHANGED (asm_full_simp_tac ((Simplifier.context ctxt HOL_ss) addsimps
+       (asm_full_simp_tac ((Simplifier.context ctxt HOL_ss) addsimps
         [(@{thm equiv_res_forall} OF [rel_eqv]),
-         (@{thm equiv_res_exists} OF [rel_eqv])]) i)),
-      (rtac @{thm impI} THEN' (asm_full_simp_tac (Simplifier.context ctxt HOL_ss)) THEN' rtac rel_refl),
-      (rtac @{thm RIGHT_RES_FORALL_REGULAR})
-     ]);
+         (@{thm equiv_res_exists} OF [rel_eqv])])) THEN_ALL_NEW
+         (((rtac @{thm RIGHT_RES_FORALL_REGULAR}) THEN' (RANGE [fn _ => all_tac, atac]) THEN'
+         (MetisTools.metis_tac ctxt [])) ORELSE' (MetisTools.metis_tac ctxt []));
     val cthm = Goal.prove lthy [] [] g (fn x => tac (#context x) 1);
   in
     cthm OF [thm]
@@ -565,10 +551,14 @@
      )
 *}
 
+ML {* make_const_def *}
+
 ML {*
 fun old_get_fun flag rty qty lthy ty =
   get_fun flag [(qty, rty)] lthy ty 
+*}
 
+ML {*
 fun old_make_const_def nconst_bname otrm mx rty qty lthy =
   make_const_def nconst_bname otrm mx [(qty, rty)] lthy
 *}
@@ -926,7 +916,7 @@
   val (trans2, reps_same, quot) = lookup_quot_thms lthy qty_name;
   val consts = lookup_quot_consts defs;
   val t_a = atomize_thm t;
-  val t_r = regularize t_a rty rel rel_eqv rel_refl lthy;
+  val t_r = regularize t_a rty rel rel_eqv lthy;
   val t_t = repabs lthy t_r consts rty qty quot rel_refl trans2 rsp_thms;
   val abs = findabs rty (prop_of t_a);
   val simp_lam_prs_thms = map (make_simp_lam_prs_thm lthy quot) abs;