
diff -r d835a2771608 -r e9b0728061a8 Nominal/FSet.thy
--- a/Nominal/FSet.thy	Tue Jun 22 13:05:00 2010 +0100
+++ b/Nominal/FSet.thy	Tue Jun 22 13:31:42 2010 +0100
@@ -1410,267 +1410,6 @@
   unfolding fset_to_set_trans
   by (rule card_Diff_subset_Int) (fold inter_set, rule finite_fset)
 
-
-ML {*
-fun dest_fsetT (Type (@{type_name fset}, [T])) = T
-  | dest_fsetT T = raise TYPE ("dest_fsetT: fset type expected", [T], []);
-*}
-
-ML {*
-open Quotient_Info;
-
-exception LIFT_MATCH of string
-
-
-
-(*** Aggregate Rep/Abs Function ***)
-
-
-(* The flag RepF is for types in negative position; AbsF is for types
-   in positive position. Because of this, function types need to be
-   treated specially, since there the polarity changes.
-*)
-
-datatype flag = AbsF | RepF
-
-fun negF AbsF = RepF
-  | negF RepF = AbsF
-
-fun is_identity (Const (@{const_name "id"}, _)) = true
-  | is_identity _ = false
-
-fun mk_identity ty = Const (@{const_name "id"}, ty --> ty)
-
-fun mk_fun_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_mapfun ctxt s =
-let
-  val thy = ProofContext.theory_of ctxt
-  val exn = LIFT_MATCH ("No map function for type " ^ quote s ^ " found.")
-  val mapfun = #mapfun (maps_lookup thy s) handle Quotient_Info.NotFound => raise exn
-in
-  Const (mapfun, dummyT)
-end
-
-(* makes a Free out of a TVar *)
-fun mk_Free (TVar ((x, i), _)) = Free (unprefix "'" x ^ string_of_int i, dummyT)
-
-(* produces an aggregate map function for the
-   rty-part of a quotient definition; abstracts
-   over all variables listed in vs (these variables
-   correspond to the type variables in rty)
-
-   for example for: (?'a list * ?'b)
-   it produces:     %a b. prod_map (map a) b
-*)
-fun mk_mapfun ctxt vs rty =
-let
-  val vs' = map (mk_Free) vs
-
-  fun mk_mapfun_aux rty =
-    case rty of
-      TVar _ => mk_Free rty
-    | Type (_, []) => mk_identity rty
-    | Type (s, tys) => list_comb (get_mapfun ctxt s, map mk_mapfun_aux tys)
-    | _ => raise LIFT_MATCH "mk_mapfun (default)"
-in
-  fold_rev Term.lambda vs' (mk_mapfun_aux rty)
-end
-
-(* looks up the (varified) rty and qty for
-   a quotient definition
-*)
-fun get_rty_qty ctxt s =
-let
-  val thy = ProofContext.theory_of ctxt
-  val exn = LIFT_MATCH ("No quotient type " ^ quote s ^ " found.")
-  val qdata = (quotdata_lookup thy s) handle Quotient_Info.NotFound => raise exn
-in
-  (#rtyp qdata, #qtyp qdata)
-end
-
-(* takes two type-environments and looks
-   up in both of them the variable v, which
-   must be listed in the environment
-*)
-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
-
-(* matches a type pattern with a type *)
-fun match ctxt err ty_pat ty =
-let
-  val thy = ProofContext.theory_of ctxt
-in
-  Sign.typ_match thy (ty_pat, ty) Vartab.empty
-  handle MATCH_TYPE => err ctxt ty_pat ty
-end
-
-(* produces the rep or abs constant for a qty *)
-fun absrep_const flag ctxt qty_str =
-let
-  val qty_name = Long_Name.base_name qty_str
-  val qualifier = Long_Name.qualifier qty_str
-in
-  case flag of
-    AbsF => Const (Long_Name.qualify qualifier ("abs_" ^ qty_name), dummyT)
-  | RepF => Const (Long_Name.qualify qualifier ("rep_" ^ qty_name), dummyT)
-end
-
-(* Lets Nitpick represent elements of quotient types as elements of the raw type *)
-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
-  val ty_str = Syntax.string_of_typ ctxt ty
-in
-  raise LIFT_MATCH (space_implode " "
-    ["absrep_fun (Types ", quote ty_pat_str, "and", quote ty_str, " do not match.)"])
-end
-
-
-(** generation of an aggregate absrep function **)
-
-(* - In case of equal types we just return the identity.
-
-   - In case of TFrees we also return the identity.
-
-   - In case of function types we recurse taking
-     the polarity change into account.
-
-   - If the type constructors are equal, we recurse for the
-     arguments and build the appropriate map function.
-
-   - If the type constructors are unequal, there must be an
-     instance of quotient types:
-
-       - we first look up the corresponding rty_pat and qty_pat
-         from the quotient definition; the arguments of qty_pat
-         must be some distinct TVars
-       - we then match the rty_pat with rty and qty_pat with qty;
-         if matching fails the types do not correspond -> error
-       - the matching produces two environments; we look up the
-         assignments for the qty_pat variables and recurse on the
-         assignments
-       - we prefix the aggregate map function for the rty_pat,
-         which is an abstraction over all type variables
-       - finally we compose the result with the appropriate
-         absrep function in case at least one argument produced
-         a non-identity function /
-         otherwise we just return the appropriate absrep
-         function
-
-     The composition is necessary for types like
-
-        ('a list) list / ('a foo) foo
-
-     The matching is necessary for types like
-
-        ('a * 'a) list / 'a bar
-
-     The test is necessary in order to eliminate superfluous
-     identity maps.
-*)
-
-fun absrep_fun flag ctxt (rty, qty) =
-  if rty = qty
-  then mk_identity rty
-  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
-           let
-             val args = map (absrep_fun flag ctxt) (tys ~~ tys')
-           in
-             list_comb (get_mapfun ctxt s, args)
-           end
-        else
-           let
-             val (rty_pat, qty_pat as Type (_, vs)) = get_rty_qty ctxt s'
-             val rtyenv = match ctxt absrep_match_err rty_pat rty
-             val qtyenv = match ctxt absrep_match_err qty_pat qty
-             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
-             (*if forall is_identity args
-             then absrep_const flag ctxt s'
-             else*) mk_fun_compose flag (absrep_const flag ctxt s', result)
-           end
-    | (TFree x, TFree x') =>
-        if x = x'
-        then mk_identity rty
-        else raise (LIFT_MATCH "absrep_fun (frees)")
-    | (TVar _, TVar _) => raise (LIFT_MATCH "absrep_fun (vars)")
-    | _ => raise (LIFT_MATCH "absrep_fun (default)")
-
-
-*}
-
-ML {*
-let
-val parser = Args.context -- Scan.lift Args.name_source
-fun typ_pat (ctxt, str) =
-str |> Syntax.parse_typ ctxt
-|> ML_Syntax.print_typ
-|> ML_Syntax.atomic
-in
-ML_Antiquote.inline "typ_pat" (parser >> typ_pat)
-end
-*}
-
-ML {*
-  mk_mapfun @{context} [@{typ_pat "?'a"}] @{typ_pat "(?'a list) * nat"}
-  |> Syntax.check_term @{context}
-  |> fastype_of
-  |> Syntax.string_of_typ @{context}
-  |> tracing
-*}
-
-ML {*
-  mk_mapfun @{context} [@{typ_pat "?'a"}] @{typ_pat "(?'a list) * nat"}
-  |> Syntax.check_term @{context}
-  |> Syntax.string_of_term @{context}
-  |> warning
-*}
-
-ML {*
-  mk_mapfun @{context} [@{typ_pat "?'a"}] @{typ_pat "(?'a list) * nat"}
-  |> Syntax.check_term @{context}
-*}
-
-term prod_fun
-term map
-term fun_map
-term "op o"
-
-ML {*
-  absrep_fun AbsF @{context} (@{typ "('a list) list \<Rightarrow> 'a list"}, @{typ "('a fset) fset \<Rightarrow> 'a fset"})
-  |> Syntax.string_of_term @{context}
-  |> writeln
-*}
-
-lemma "(\<lambda> (c::'s \<Rightarrow> bool). \<exists>(x::'s). c = rel x) = {c. \<exists>x. c = rel x}"
-apply(auto simp add: mem_def)
-done
-
 lemma ball_reg_right_unfolded: "(\<forall>x. R x \<longrightarrow> P x \<longrightarrow> Q x) \<longrightarrow> (All P \<longrightarrow> Ball R Q)"
 apply rule
 apply (rule ball_reg_right)




