# HG changeset patch # User Christian Urban # Date 1292488968 0 # Node ID 3d101f2f817c43627a6d0d2d0496277bb3a6356d # Parent f5c7375ab4655177801dfb79ebe65c1a0ec6baba simple cases for strong inducts done; infrastructure for the difficult ones is there diff -r f5c7375ab465 -r 3d101f2f817c Nominal/Ex/Ex1.thy --- a/Nominal/Ex/Ex1.thy Thu Dec 16 02:25:35 2010 +0000 +++ b/Nominal/Ex/Ex1.thy Thu Dec 16 08:42:48 2010 +0000 @@ -6,7 +6,7 @@ atom_decl name -declare [[STEPS = 100]] +thm finite_sets_supp nominal_datatype foo = Foo0 "name" diff -r f5c7375ab465 -r 3d101f2f817c Nominal/Ex/Foo2.thy --- a/Nominal/Ex/Foo2.thy Thu Dec 16 02:25:35 2010 +0000 +++ b/Nominal/Ex/Foo2.thy Thu Dec 16 08:42:48 2010 +0000 @@ -21,10 +21,12 @@ binder bn::"assg \ atom list" where - "bn (As x y t a) = [atom x] @ bn a" + "bn (As x y t a) = [atom x] @ bn a" | "bn (As_Nil) = []" + + thm foo.bn_defs thm foo.permute_bn thm foo.perm_bn_alpha @@ -69,65 +71,26 @@ *) -text {* *} -(* -thm at_set_avoiding1[THEN exE] - - -lemma Let1_rename: - fixes c::"'a::fs" - shows "\name' trm'. {atom name'} \* c \ Lam name trm = Lam name' trm'" -apply(simp only: foo.eq_iff) -apply(rule at_set_avoiding1[where c="(c, atom name, trm)" and xs="set [atom name]", THEN exE]) -apply(simp) -apply(simp add: finite_supp) -apply(perm_simp) -apply(rule Abs_rename_list[THEN exE]) -apply(simp only: set_eqvt) -apply -sorry -*) - -thm foo.exhaust - -ML {* -fun strip_prems_concl trm = - (Logic.strip_imp_prems trm, Logic.strip_imp_concl trm) -*} - -ML {* - @{thms foo.exhaust} - |> map prop_of - |> map strip_prems_concl - |> map fst - |> map (map (Syntax.string_of_term @{context})) - |> map cat_lines - |> cat_lines - |> writeln -*} - lemma test6: fixes c::"'a::fs" - assumes "\name. y = Var name \ P" - and "\trm1 trm2. y = App trm1 trm2 \ P" + assumes "\name. y = Var name \ P" + and "\trm1 trm2. y = App trm1 trm2 \ P" and "\name trm. \{atom name} \* c; y = Lam name trm\ \ P" - and "\a1 trm1 a2 trm2. ((set (bn a1)) \ (set (bn a2))) \* c \ y = Let1 a1 trm1 a2 trm2 \ P" + and "\a1 trm1 a2 trm2. \((set (bn a1)) \ (set (bn a2))) \* c; y = Let1 a1 trm1 a2 trm2\ \ P" and "\x1 x2 trm1 trm2. {atom x1, atom x2} \* c \ y = Let2 x1 x2 trm1 trm2 \ P" shows "P" -apply(rule_tac foo.exhaust(1)) +apply(rule_tac y="y" in foo.exhaust(1)) apply(rule assms(1)) -apply(rule exI)+ apply(assumption) apply(rule assms(2)) -apply(rule exI)+ apply(assumption) (* lam case *) apply(subgoal_tac "\p. (p \ {atom name}) \* (c, name, trm)") apply(erule exE) -apply(insert Abs_rename_list)[1] +apply(insert Abs_rename_lst)[1] apply(drule_tac x="p" in meta_spec) apply(drule_tac x="[atom name]" in meta_spec) apply(drule_tac x="trm" in meta_spec) @@ -150,12 +113,18 @@ apply(subgoal_tac "\p. (p \ ((set (bn assg1)) \ (set (bn assg2)))) \* (c, bn assg1, bn assg2, trm1, trm2)") apply(erule exE) apply(rule assms(4)) +apply(perm_simp add: foo.permute_bn) +apply(simp add: fresh_star_Pair) +apply(erule conjE)+ +apply(assumption) +apply(simp only:) apply(simp only: foo.eq_iff) -apply(insert Abs_rename_list)[1] +(* *) +apply(insert Abs_rename_lst)[1] apply(drule_tac x="p" in meta_spec) apply(drule_tac x="bn assg1" in meta_spec) apply(drule_tac x="trm1" in meta_spec) -apply(insert Abs_rename_list)[1] +apply(insert Abs_rename_lst)[1] apply(drule_tac x="p" in meta_spec) apply(drule_tac x="bn assg2" in meta_spec) apply(drule_tac x="trm2" in meta_spec) @@ -164,21 +133,18 @@ apply(drule meta_mp) apply(simp only: union_eqvt fresh_star_Pair set.simps fresh_star_Un, simp) apply(erule exE)+ -apply(rule exI)+ apply(perm_simp add: foo.permute_bn) -apply(rule conjI) -apply(simp add: fresh_star_Pair fresh_star_Un) +apply(simp add: fresh_star_Pair) apply(erule conjE)+ +apply(rule assms(4)) +apply(assumption) +apply(simp add: foo.eq_iff refl) apply(rule conjI) -apply(assumption) -apply(rotate_tac 4) -apply(assumption) -apply(rule conjI) -apply(assumption) +apply(rule refl) apply(rule conjI) apply(rule foo.perm_bn_alpha) apply(rule conjI) -apply(assumption) +apply(rule refl) apply(rule foo.perm_bn_alpha) apply(rule at_set_avoiding1) apply(simp) diff -r f5c7375ab465 -r 3d101f2f817c Nominal/Ex/TypeSchemes.thy --- a/Nominal/Ex/TypeSchemes.thy Thu Dec 16 02:25:35 2010 +0000 +++ b/Nominal/Ex/TypeSchemes.thy Thu Dec 16 08:42:48 2010 +0000 @@ -9,6 +9,8 @@ (* defined as a single nominal datatype *) +thm finite_set + nominal_datatype ty = Var "name" | Fun "ty" "ty" diff -r f5c7375ab465 -r 3d101f2f817c Nominal/Nominal2.thy --- a/Nominal/Nominal2.thy Thu Dec 16 02:25:35 2010 +0000 +++ b/Nominal/Nominal2.thy Thu Dec 16 08:42:48 2010 +0000 @@ -6,6 +6,7 @@ ("nominal_dt_quot.ML") begin + use "nominal_dt_rawfuns.ML" ML {* open Nominal_Dt_RawFuns *} @@ -50,9 +51,10 @@ ML {* -fun process_ecase lthy c (params, prems, concl) binders = +fun process_ecase lthy c (params, prems, concl) bclauses = let val tys = map snd params + val binders = get_all_binders bclauses fun prep_binder (opt, i) = let @@ -77,15 +79,21 @@ end *} + ML {* -fun fresh_thm ctxt c params binders bn_finite_thms = +fun fresh_thm ctxt c parms binders bn_finite_thms = let fun prep_binder (opt, i) = case opt of - NONE => setify ctxt (nth params i) - | SOME bn => to_set (bn $ (nth params i)) + NONE => setify ctxt (nth parms i) + | SOME bn => to_set (bn $ (nth parms i)) - val rhs = HOLogic.mk_tuple (c :: params) + fun prep_binder2 (opt, i) = + case opt of + NONE => atomify ctxt (nth parms i) + | SOME bn => bn $ (nth parms i) + + val rhs = HOLogic.mk_tuple ([c] @ parms @ (map prep_binder2 binders)) val lhs = binders |> map prep_binder |> fold_union @@ -94,33 +102,99 @@ val goal = mk_fresh_star lhs rhs |> (fn t => HOLogic.mk_exists ("p", @{typ perm}, t)) |> HOLogic.mk_Trueprop - val ss = @{thms finite.emptyI finite.insertI finite_supp supp_Pair finite_Un finite_fset finite_set} - @ bn_finite_thms + + val ss = bn_finite_thms @ @{thms supp_Pair finite_supp finite_sets_supp} + @ @{thms finite.intros finite_Un finite_set finite_fset} in Goal.prove ctxt [] [] goal (K (HEADGOAL (rtac @{thm at_set_avoiding1} THEN_ALL_NEW (simp_tac (HOL_ss addsimps ss))))) end + +fun abs_eq_thm ctxt fprops p parms bn_finite_thms (BC (bmode, binders, bodies)) = + case binders of + [] => [] + | binders => + let + val binder_trm = Nominal_Dt_Alpha.comb_binders ctxt bmode parms binders + val body_trm = foldl1 HOLogic.mk_prod (map (nth parms) bodies) + val body_ty = fastype_of body_trm + + val (abs_name, binder_ty, abs_ty) = + case bmode of + Lst => (@{const_name "Abs_lst"}, @{typ "atom list"}, @{type_name abs_lst}) + | Set => (@{const_name "Abs_set"}, @{typ "atom set"}, @{type_name abs_set}) + | Res => (@{const_name "Abs_res"}, @{typ "atom set"}, @{type_name abs_res}) + + val abs = Const (abs_name, [binder_ty, body_ty] ---> Type (abs_ty, [body_ty])) + val abs_lhs = abs $ binder_trm $ body_trm + val abs_rhs = abs $ mk_perm p binder_trm $ Bound 0 + val goal = HOLogic.mk_eq (abs_lhs, abs_rhs) + |> (fn t => HOLogic.mk_exists ("y", body_ty, t)) + |> HOLogic.mk_Trueprop + + val ss = fprops @ bn_finite_thms @ @{thms set.simps set_append union_eqvt} + @ @{thms fresh_star_Un fresh_star_Pair fresh_star_list fresh_star_singleton fresh_star_fset + fresh_star_set} @ @{thms finite.intros finite_fset} + in + [Goal.prove ctxt [] [] goal + (K (HEADGOAL (resolve_tac @{thms Abs_rename_set Abs_rename_res Abs_rename_lst} + THEN_ALL_NEW (simp_tac (HOL_basic_ss addsimps ss) THEN' TRY o simp_tac HOL_ss))))] + end +*} + +ML {* +fun partitions [] [] = [] + | partitions xs (i :: js) = + let + val (head, tail) = chop i xs + in + head :: partitions tail js + end +*} + + +ML {* +fun mk_cperm ctxt p ctrm = + mk_perm (term_of p) (term_of ctrm) + |> cterm_of (ProofContext.theory_of ctxt) +*} + + +ML {* +fun case_tac ctxt c bn_finite_thms (prems, bclausess) thm = + let + fun aux_tac prem bclauses = + case (get_all_binders bclauses) of + [] => EVERY' [rtac prem, atac] + | binders => Subgoal.FOCUS (fn {params, prems, context = ctxt, ...} => + let + val parms = map (term_of o snd) params + val fthm = fresh_thm ctxt c parms binders bn_finite_thms + + val ss = @{thms fresh_star_Pair union_eqvt fresh_star_Un} + val (([(_, fperm)], fprops), ctxt') = Obtain.result + (K (EVERY1 [etac exE, + full_simp_tac (HOL_basic_ss addsimps ss), + REPEAT o (etac conjE)])) [fthm] ctxt + (* + val _ = tracing ("fprop:\n" ^ cat_lines (map (Syntax.string_of_term ctxt' o prop_of) fprops)) + *) + val abs_eqs = flat (map (abs_eq_thm ctxt fprops (term_of fperm) parms bn_finite_thms) bclauses) + (* + val _ = tracing ("abs_eqs:\n" ^ cat_lines (map (Syntax.string_of_term ctxt' o prop_of) abs_eqs)) + *) + in + (*HEADGOAL (rtac prem THEN' RANGE [K all_tac, simp_tac (HOL_basic_ss addsimps prems)])*) + Skip_Proof.cheat_tac (ProofContext.theory_of ctxt') + end) ctxt + in + rtac thm THEN' RANGE (map2 aux_tac prems bclausess) + end *} ML {* -fun case_tac ctxt c bn_finite_thms binderss thm = - let - fun aux_tac (binders : (term option * int) list)= - Subgoal.FOCUS (fn {params, context, ...} => - let - val prms = map (term_of o snd) params - val fthm = fresh_thm ctxt c prms binders bn_finite_thms - val _ = tracing ("params" ^ @{make_string} params) - val _ = tracing ("binders" ^ @{make_string} binders) - in - Skip_Proof.cheat_tac (ProofContext.theory_of ctxt) - end) ctxt - in - rtac thm THEN' RANGE (map aux_tac binderss) - end - fun prove_strong_exhausts lthy qexhausts qtrms bclausesss bn_finite_thms = let val ((_, qexhausts'), lthy') = Variable.import true qexhausts lthy @@ -128,22 +202,22 @@ val ([c, a], lthy'') = Variable.variant_fixes ["c", "'a"] lthy' val c = Free (c, TFree (a, @{sort fs})) - val binderss = map (map get_all_binders) bclausesss - val (ecases, main_concls) = qexhausts' (* ecases or of the form (params, prems, concl) *) |> map prop_of |> map Logic.strip_horn |> split_list |>> map (map strip_params_prems_concl) - val prems = map2 (process_ecase lthy'' c) (flat ecases) (flat binderss) - - val _ = tracing ("binderss: " ^ @{make_string} binderss) + val prems = map2 (process_ecase lthy'' c) (flat ecases) (flat bclausesss) in Goal.prove_multi lthy'' [] prems main_concls - (fn {prems, context} => - EVERY1 [Goal.conjunction_tac, - RANGE (map2 (case_tac context c bn_finite_thms) binderss qexhausts')]) + (fn {prems:thm list, context} => + let + val prems' = partitions prems (map length bclausesss) + in + EVERY1 [Goal.conjunction_tac, + RANGE (map2 (case_tac context c bn_finite_thms) (prems' ~~ bclausesss) qexhausts')] + end) end *} @@ -323,7 +397,7 @@ val raw_induct_thm = #induct dtinfo val raw_induct_thms = #inducts dtinfo val raw_exhaust_thms = map #exhaust dtinfos - val raw_size_trms = map size_const raw_tys + val raw_size_trms = map HOLogic.size_const raw_tys val raw_size_thms = Size.size_thms (ProofContext.theory_of lthy0) (hd raw_dt_names) |> `(fn thms => (length thms) div 2) |> uncurry drop diff -r f5c7375ab465 -r 3d101f2f817c Nominal/Nominal2_Abs.thy --- a/Nominal/Nominal2_Abs.thy Thu Dec 16 02:25:35 2010 +0000 +++ b/Nominal/Nominal2_Abs.thy Thu Dec 16 08:42:48 2010 +0000 @@ -587,7 +587,7 @@ then show "\y. [bs]res. x = [p \ bs]res. y" by blast qed -lemma Abs_rename_list: +lemma Abs_rename_lst: fixes x::"'a::fs" assumes a: "(p \ (set bs)) \* (bs, x)" shows "\y. [bs]lst. x = [p \ bs]lst. y" diff -r f5c7375ab465 -r 3d101f2f817c Nominal/Nominal2_Base.thy --- a/Nominal/Nominal2_Base.thy Thu Dec 16 02:25:35 2010 +0000 +++ b/Nominal/Nominal2_Base.thy Thu Dec 16 08:42:48 2010 +0000 @@ -1411,6 +1411,16 @@ unfolding fresh_star_def by (simp add: fresh_set) +lemma fresh_star_singleton: + fixes a::"atom" + shows "as \* {a} \ as \* a" + by (simp add: fresh_star_def fresh_finite_insert fresh_set_empty) + +lemma fresh_star_fset: + fixes xs::"('a::fs) list" + shows "as \* fset S \ as \* S" +by (simp add: fresh_star_def fresh_def) + lemma fresh_star_Un: shows "(as \ bs) \* x = (as \* x \ bs \* x)" by (auto simp add: fresh_star_def) @@ -1701,7 +1711,6 @@ section {* Renaming permutations *} - lemma set_renaming_perm: assumes a: "p \ bs \ bs = {}" and b: "finite bs" @@ -1840,6 +1849,10 @@ shows "a \ atom b \ a \ b" by (simp add: fresh_def supp_at_base supp_atom) +lemma fresh_star_atom_at_base: + fixes b::"'a::at_base" + shows "as \* atom b \ as \* b" + by (simp add: fresh_star_def fresh_atom_at_base) instance at_base < fs proof qed (simp add: supp_at_base) diff -r f5c7375ab465 -r 3d101f2f817c Nominal/nominal_dt_alpha.ML --- a/Nominal/nominal_dt_alpha.ML Thu Dec 16 02:25:35 2010 +0000 +++ b/Nominal/nominal_dt_alpha.ML Thu Dec 16 08:42:48 2010 +0000 @@ -7,6 +7,8 @@ signature NOMINAL_DT_ALPHA = sig + val comb_binders: Proof.context -> bmode -> term list -> (term option * int) list -> term + val define_raw_alpha: string list -> typ list -> cns_info list -> bn_info list -> bclause list list list -> term list -> Proof.context -> term list * term list * thm list * thm list * thm * local_theory @@ -71,7 +73,7 @@ end (* generates the compound binder terms *) -fun mk_binders lthy bmode args binders = +fun comb_binders lthy bmode args binders = let fun bind_set lthy args (NONE, i) = setify lthy (nth args i) | bind_set _ args (SOME bn, i) = bn $ (nth args i) @@ -150,8 +152,8 @@ val comp_alpha = foldl1 mk_prod_alpha alphas val comp_args = foldl1 HOLogic.mk_prod (map (nth args) bodies) val comp_args' = foldl1 HOLogic.mk_prod (map (nth args') bodies) - val comp_binders = mk_binders lthy bmode args binders - val comp_binders' = mk_binders lthy bmode args' binders + val comp_binders = comb_binders lthy bmode args binders + val comp_binders' = comb_binders lthy bmode args' binders val alpha_prem = mk_alpha_term bmode comp_fv comp_alpha comp_args comp_args' comp_binders comp_binders' val alpha_bn_prems = flat (map (mk_alpha_bn_prem alpha_bn_map args args' bodies) binders) diff -r f5c7375ab465 -r 3d101f2f817c Nominal/nominal_dt_rawfuns.ML --- a/Nominal/nominal_dt_rawfuns.ML Thu Dec 16 02:25:35 2010 +0000 +++ b/Nominal/nominal_dt_rawfuns.ML Thu Dec 16 08:42:48 2010 +0000 @@ -60,7 +60,7 @@ fun get_all_binders bclauses = bclauses - |> map (fn (BC (_, x, _)) => x) + |> map (fn (BC (_, binders, _)) => binders) |> flat |> remove_dups (op =) diff -r f5c7375ab465 -r 3d101f2f817c Nominal/nominal_library.ML --- a/Nominal/nominal_library.ML Thu Dec 16 02:25:35 2010 +0000 +++ b/Nominal/nominal_library.ML Thu Dec 16 08:42:48 2010 +0000 @@ -18,8 +18,6 @@ val mk_id: term -> term val mk_all: (string * typ) -> term -> term - val size_const: typ -> term - val sum_case_const: typ -> typ -> typ -> term val mk_sum_case: term -> term -> term @@ -49,10 +47,11 @@ val is_atom_fset: Proof.context -> typ -> bool val is_atom_list: Proof.context -> typ -> bool - val to_atom_set: term -> term val to_set_ty: typ -> term -> term val to_set: term -> term + val atomify_ty: Proof.context -> typ -> term -> term + val atomify: Proof.context -> term -> term val setify_ty: Proof.context -> typ -> term -> term val setify: Proof.context -> term -> term val listify_ty: Proof.context -> typ -> term -> term @@ -125,19 +124,18 @@ fun order eq keys list = map (the o AList.lookup eq list) keys +(* remove duplicates *) fun remove_dups eq [] = [] - | remove_dups eq (x::xs) = - if (member eq xs x) + | remove_dups eq (x :: xs) = + if member eq xs x then remove_dups eq xs - else x::(remove_dups eq xs) - + else x :: remove_dups eq xs fun last2 [] = raise Empty | last2 [_] = raise Empty | last2 [x, y] = (x, y) | last2 (_ :: xs) = last2 xs - fun is_true @{term "Trueprop True"} = true | is_true _ = false @@ -148,6 +146,7 @@ | dest_fsetT T = raise TYPE ("dest_fsetT: fset type expected", [T], []); + fun mk_id trm = let val ty = fastype_of trm @@ -157,11 +156,9 @@ fun mk_all (a, T) t = Term.all T $ Abs (a, T, t) - -fun size_const ty = Const (@{const_name size}, ty --> @{typ nat}) - fun sum_case_const ty1 ty2 ty3 = Const (@{const_name sum_case}, [ty1 --> ty3, ty2 --> ty3, Type (@{type_name sum}, [ty1, ty2])] ---> ty3) + fun mk_sum_case trm1 trm2 = let val ([ty1], ty3) = strip_type (fastype_of trm1) @@ -192,19 +189,18 @@ fun mk_atom_set_ty ty t = let - val atom_ty = HOLogic.dest_setT ty --> @{typ "atom"}; - val img_ty = atom_ty --> ty --> @{typ "atom set"}; + val atom_ty = HOLogic.dest_setT ty + val img_ty = (atom_ty --> @{typ atom}) --> ty --> @{typ "atom set"}; in - Const (@{const_name image}, img_ty) $ mk_atom_ty atom_ty t + Const (@{const_name image}, img_ty) $ atom_const atom_ty $ t end fun mk_atom_fset_ty ty t = let val atom_ty = dest_fsetT ty val fmap_ty = (atom_ty --> @{typ atom}) --> ty --> @{typ "atom fset"}; - val fset = @{term "fset :: atom fset => atom set"} in - fset $ (Const (@{const_name map_fset}, fmap_ty) $ (atom_const atom_ty) $ t) + Const (@{const_name map_fset}, fmap_ty) $ atom_const atom_ty $ t end fun mk_atom_list_ty ty t = @@ -212,7 +208,7 @@ val atom_ty = dest_listT ty val map_ty = (atom_ty --> @{typ atom}) --> ty --> @{typ "atom list"} in - Const (@{const_name map}, map_ty) $ (atom_const atom_ty) $ t + Const (@{const_name map}, map_ty) $ atom_const atom_ty $ t end fun mk_atom_set t = mk_atom_set_ty (fastype_of t) t @@ -220,11 +216,12 @@ fun mk_atom_list t = mk_atom_list_ty (fastype_of t) t (* coerces a list into a set *) -fun to_atom_set t = @{term "set :: atom list => atom set"} $ t fun to_set_ty ty t = - if ty = @{typ "atom list"} - then to_atom_set t else t + case ty of + @{typ "atom list"} => @{term "set :: atom list => atom set"} $ t + | @{typ "atom fset"} => @{term "fset :: atom fset => atom set"} $ t + | _ => t fun to_set t = to_set_ty (fastype_of t) t @@ -243,22 +240,30 @@ | is_atom_list _ _ = false -(* functions that coerces singletons, sets and fsets of concrete atoms - into sets of general atoms *) +(* functions that coerce singletons, sets, fsets and lists of concrete + atoms into general atoms sets / lists *) +fun atomify_ty ctxt ty t = + if is_atom ctxt ty + then mk_atom_ty ty t + else if is_atom_set ctxt ty + then mk_atom_set_ty ty t + else if is_atom_fset ctxt ty + then mk_atom_fset_ty ty t + else if is_atom_list ctxt ty + then mk_atom_list_ty ty t + else raise TERM ("atomify", [t]) + fun setify_ty ctxt ty t = if is_atom ctxt ty then HOLogic.mk_set @{typ atom} [mk_atom_ty ty t] else if is_atom_set ctxt ty then mk_atom_set_ty ty t else if is_atom_fset ctxt ty - then mk_atom_fset_ty ty t + then @{term "fset :: atom fset => atom set"} $ mk_atom_fset_ty ty t else if is_atom_list ctxt ty - then to_atom_set (mk_atom_list_ty ty t) + then @{term "set :: atom list => atom set"} $ mk_atom_list_ty ty t else raise TERM ("setify", [t]) - -(* functions that coerces singletons and lists of concrete atoms - into lists of general atoms *) fun listify_ty ctxt ty t = if is_atom ctxt ty then HOLogic.mk_list @{typ atom} [mk_atom_ty ty t] @@ -266,7 +271,8 @@ then mk_atom_list_ty ty t else raise TERM ("listify", [t]) -fun setify ctxt t = setify_ty ctxt (fastype_of t) t +fun atomify ctxt t = atomify_ty ctxt (fastype_of t) t +fun setify ctxt t = setify_ty ctxt (fastype_of t) t fun listify ctxt t = listify_ty ctxt (fastype_of t) t fun fresh_star_ty ty = [@{typ "atom set"}, ty] ---> @{typ bool} @@ -422,7 +428,7 @@ SumTree.mk_sumcase fT sT natT (mk_size_measure fT) (mk_size_measure sT) | (Type (@{type_name Product_Type.prod}, [fT, sT])) => prod_size_const fT sT $ (mk_size_measure fT) $ (mk_size_measure sT) - | _ => size_const T + | _ => HOLogic.size_const T fun mk_measure_trm T = HOLogic.dest_setT T