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 \ 'a list"}, @{typ "('a fset) fset \ 'a fset"}) - |> Syntax.string_of_term @{context} - |> writeln -*} - -lemma "(\ (c::'s \ bool). \(x::'s). c = rel x) = {c. \x. c = rel x}" -apply(auto simp add: mem_def) -done - lemma ball_reg_right_unfolded: "(\x. R x \ P x \ Q x) \ (All P \ Ball R Q)" apply rule apply (rule ball_reg_right)