--- 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)
--- a/Nominal/NewParser.thy Tue Jun 22 13:05:00 2010 +0100
+++ b/Nominal/NewParser.thy Tue Jun 22 13:31:42 2010 +0100
@@ -452,6 +452,7 @@
val _ = tracing ("alpha_bn_imp\n" ^
cat_lines (map (Syntax.string_of_term lthy4 o prop_of) alpha_bn_imp_thms))
+ (* old stuff *)
val _ =
if get_STEPS lthy > 13
then true else raise TEST lthy4
@@ -462,6 +463,14 @@
val fv_alpha_all = combine_fv_alpha_bns (raw_fvs, raw_fv_bns) (alpha_trms, alpha_bn_trms) bn_nos
val reflps = build_alpha_refl fv_alpha_all alpha_trms induct_thm alpha_eq_iff lthy4;
+
+ val _ = tracing ("reflps\n" ^
+ cat_lines (map (Syntax.string_of_term lthy4 o prop_of) reflps))
+
+ val _ =
+ if get_STEPS lthy > 13
+ then true else raise TEST lthy4
+
val alpha_equivp =
if !cheat_equivp then map (equivp_hack lthy4) alpha_trms
else build_equivps alpha_trms reflps alpha_induct
--- a/Nominal/nominal_dt_rawfuns.ML Tue Jun 22 13:05:00 2010 +0100
+++ b/Nominal/nominal_dt_rawfuns.ML Tue Jun 22 13:31:42 2010 +0100
@@ -65,6 +65,10 @@
Const (@{const_name image}, img_ty) $ mk_atom_ty atom_ty t
end
+
+fun dest_fsetT (Type (@{type_name fset}, [T])) = T
+ | dest_fsetT T = raise TYPE ("dest_fsetT: fset type expected", [T], []);
+
fun mk_atom_fset t =
let
val ty = fastype_of t;