# HG changeset patch # User Christian Urban # Date 1261513904 -3600 # Node ID d1064fa29424d1cc84dade9b530c0a27474d9451 # Parent 26fefde1d1249c70343a11b7d286f5647f624c30 renamed get_fun to absrep_fun; introduced explicit checked versions of the term functions diff -r 26fefde1d124 -r d1064fa29424 Quot/Examples/FSet.thy --- a/Quot/Examples/FSet.thy Tue Dec 22 21:16:11 2009 +0100 +++ b/Quot/Examples/FSet.thy Tue Dec 22 21:31:44 2009 +0100 @@ -43,7 +43,7 @@ *} ML {* -get_fun absF @{context} (@{typ "'a list"}, +absrep_fun absF @{context} (@{typ "'a list"}, @{typ "'a fset"}) |> Syntax.check_term @{context} |> Syntax.string_of_term @{context} @@ -54,7 +54,7 @@ term "abs_fset o (map id)" ML {* -get_fun absF @{context} (@{typ "(nat * nat) list"}, +absrep_fun absF @{context} (@{typ "(nat * nat) list"}, @{typ "int fset"}) |> Syntax.check_term @{context} |> Syntax.string_of_term @{context} @@ -66,7 +66,7 @@ ML {* -get_fun absF @{context} (@{typ "('a list) list"}, +absrep_fun absF @{context} (@{typ "('a list) list"}, @{typ "('a fset) fset"}) |> Syntax.check_term @{context} |> Syntax.string_of_term @{context} @@ -74,7 +74,7 @@ *} ML {* -get_fun absF @{context} (@{typ "('a list) list \ 'a"}, +absrep_fun absF @{context} (@{typ "('a list) list \ 'a"}, @{typ "('a fset) fset \ 'a"}) |> Syntax.check_term @{context} |> Syntax.string_of_term @{context} diff -r 26fefde1d124 -r d1064fa29424 Quot/quotient_def.ML --- a/Quot/quotient_def.ML Tue Dec 22 21:16:11 2009 +0100 +++ b/Quot/quotient_def.ML Tue Dec 22 21:31:44 2009 +0100 @@ -36,8 +36,7 @@ let val Free (lhs_str, lhs_ty) = lhs; val qconst_bname = Binding.name lhs_str; - val absrep_trm = get_fun absF lthy (fastype_of rhs, lhs_ty) $ rhs - |> Syntax.check_term lthy + val absrep_trm = absrep_fun_chk absF lthy (fastype_of rhs, lhs_ty) $ rhs val prop = Logic.mk_equals (lhs, absrep_trm) val (_, prop') = LocalDefs.cert_def lthy prop val (_, newrhs) = Primitive_Defs.abs_def prop' diff -r 26fefde1d124 -r d1064fa29424 Quot/quotient_tacs.ML --- a/Quot/quotient_tacs.ML Tue Dec 22 21:16:11 2009 +0100 +++ b/Quot/quotient_tacs.ML Tue Dec 22 21:31:44 2009 +0100 @@ -586,11 +586,9 @@ val thy = ProofContext.theory_of ctxt val rtrm' = HOLogic.dest_Trueprop rtrm val qtrm' = HOLogic.dest_Trueprop qtrm - val reg_goal = - Syntax.check_term ctxt (regularize_trm ctxt (rtrm', qtrm')) + val reg_goal = regularize_trm_chk ctxt (rtrm', qtrm') handle (LIFT_MATCH str) => lift_match_error ctxt str rtrm qtrm - val inj_goal = - Syntax.check_term ctxt (inj_repabs_trm ctxt (reg_goal, qtrm')) + val inj_goal = inj_repabs_trm_chk ctxt (reg_goal, qtrm') handle (LIFT_MATCH str) => lift_match_error ctxt str rtrm qtrm in Drule.instantiate' [] diff -r 26fefde1d124 -r d1064fa29424 Quot/quotient_term.ML --- a/Quot/quotient_term.ML Tue Dec 22 21:16:11 2009 +0100 +++ b/Quot/quotient_term.ML Tue Dec 22 21:31:44 2009 +0100 @@ -3,10 +3,15 @@ exception LIFT_MATCH of string datatype flag = absF | repF - val get_fun: flag -> Proof.context -> (typ * typ) -> term + + val absrep_fun: flag -> Proof.context -> (typ * typ) -> term + val absrep_fun_chk: flag -> Proof.context -> (typ * typ) -> term val regularize_trm: Proof.context -> (term * term) -> term + val regularize_trm_chk: Proof.context -> (term * term) -> term + val inj_repabs_trm: Proof.context -> (term * term) -> term + val inj_repabs_trm_chk: Proof.context -> (term * term) -> term end; structure Quotient_Term: QUOTIENT_TERM = @@ -33,10 +38,10 @@ absF => Const (@{const_name "comp"}, dummyT) $ trm1 $ trm2 | repF => Const (@{const_name "comp"}, dummyT) $ trm2 $ trm1 -fun get_fun_aux lthy s fs = +fun absrep_fun_aux lthy s fs = let val thy = ProofContext.theory_of lthy - val exc = LIFT_MATCH (space_implode " " ["get_fun_aux: no map for type", quote s, "."]) + val exc = LIFT_MATCH (space_implode " " ["absrep_fun_aux: no map for type", quote s, "."]) val info = maps_lookup thy s handle NotFound => raise exc in list_comb (Const (#mapfun info, dummyT), fs) @@ -53,15 +58,15 @@ | repF => Const (Sign.full_bname thy ("rep_" ^ qty_name), dummyT) end -fun get_fun flag lthy (rty, qty) = +fun absrep_fun flag lthy (rty, qty) = if rty = qty then mk_identity qty else case (rty, qty) of (Type ("fun", [ty1, ty2]), Type ("fun", [ty1', ty2'])) => let - val fs_ty1 = get_fun (negF flag) lthy (ty1, ty1') - val fs_ty2 = get_fun flag lthy (ty2, ty2') + val fs_ty1 = absrep_fun (negF flag) lthy (ty1, ty1') + val fs_ty2 = absrep_fun flag lthy (ty2, ty2') in - get_fun_aux lthy "fun" [fs_ty1, fs_ty2] + absrep_fun_aux lthy "fun" [fs_ty1, fs_ty2] end | (Type (s, _), Type (s', [])) => if s = s' @@ -69,19 +74,22 @@ else get_const flag lthy rty qty | (Type (s, tys), Type (s', tys')) => let - val args = map (get_fun flag lthy) (tys ~~ tys') + val args = map (absrep_fun flag lthy) (tys ~~ tys') in if s = s' - then get_fun_aux lthy s args - else mk_compose flag (get_const flag lthy rty qty, get_fun_aux lthy s args) + then absrep_fun_aux lthy s args + else mk_compose flag (get_const flag lthy rty qty, absrep_fun_aux lthy s args) end | (TFree x, TFree x') => if x = x' then mk_identity qty - else raise (LIFT_MATCH "get_fun (frees)") - | (TVar _, TVar _) => raise (LIFT_MATCH "get_fun (vars)") - | _ => raise (LIFT_MATCH "get_fun (default)") + else raise (LIFT_MATCH "absrep_fun (frees)") + | (TVar _, TVar _) => raise (LIFT_MATCH "absrep_fun (vars)") + | _ => raise (LIFT_MATCH "absrep_fun (default)") +fun absrep_fun_chk flag lthy (rty, qty) = + absrep_fun flag lthy (rty, qty) + |> Syntax.check_term lthy (* Regularizing an rtrm means: @@ -259,7 +267,9 @@ raise (LIFT_MATCH ("regularize failed (default: " ^ rtrm_str ^ "," ^ qtrm_str ^ ")")) end - +fun regularize_trm_chk lthy (rtrm, qtrm) = + regularize_trm lthy (rtrm, qtrm) + |> Syntax.check_term lthy (* Injection of Rep/Abs means: @@ -290,7 +300,7 @@ *) fun mk_repabs lthy (T, T') trm = - get_fun repF lthy (T, T') $ (get_fun absF lthy (T, T') $ trm) + absrep_fun repF lthy (T, T') $ (absrep_fun absF lthy (T, T') $ trm) (* bound variables need to be treated properly, *) @@ -344,6 +354,10 @@ | _ => raise (LIFT_MATCH "injection (default)") +fun inj_repabs_trm_chk lthy (rtrm, qtrm) = + inj_repabs_trm lthy (rtrm, qtrm) + |> Syntax.check_term lthy + end; (* structure *)