# HG changeset patch # User Christian Urban <urbanc@in.tum.de> # Date 1283015856 -28800 # Node ID 217ef3e4282ed7fe99f14360957ed337bb1f73e2 # Parent 6b51117b89552cd225ad728d585cc5d717d3c38f added proofs for fsupp properties diff -r 6b51117b8955 -r 217ef3e4282e Nominal-General/nominal_library.ML --- a/Nominal-General/nominal_library.ML Sun Aug 29 00:36:47 2010 +0800 +++ b/Nominal-General/nominal_library.ML Sun Aug 29 01:17:36 2010 +0800 @@ -37,6 +37,11 @@ val mk_supports_ty: typ -> term -> term -> term val mk_supports: term -> term -> term + val finite_const: typ -> term + val mk_finite_ty: typ -> term -> term + val mk_finite: term -> term + + val mk_equiv: thm -> thm val safe_mk_equiv: thm -> thm @@ -117,14 +122,19 @@ fun supp_ty ty = ty --> @{typ "atom set"}; -fun supp_const ty = Const (@{const_name "supp"}, supp_ty ty) +fun supp_const ty = Const (@{const_name supp}, supp_ty ty) fun mk_supp_ty ty t = supp_const ty $ t; fun mk_supp t = mk_supp_ty (fastype_of t) t; -fun supports_const ty = Const (@{const_name "supports"}, [@{typ "atom set"}, ty] ---> @{typ bool}); +fun supports_const ty = Const (@{const_name supports}, [@{typ "atom set"}, ty] ---> @{typ bool}); fun mk_supports_ty ty t1 t2 = supports_const ty $ t1 $ t2; fun mk_supports t1 t2 = mk_supports_ty (fastype_of t2) t1 t2; +fun finite_const ty = Const (@{const_name finite}, ty --> @{typ bool}) +fun mk_finite_ty ty t = finite_const ty $ t +fun mk_finite t = mk_finite_ty (fastype_of t) t + + fun mk_equiv r = r RS @{thm eq_reflection}; fun safe_mk_equiv r = mk_equiv r handle Thm.THM _ => r; diff -r 6b51117b8955 -r 217ef3e4282e Nominal/Ex/SingleLet.thy --- a/Nominal/Ex/SingleLet.thy Sun Aug 29 00:36:47 2010 +0800 +++ b/Nominal/Ex/SingleLet.thy Sun Aug 29 01:17:36 2010 +0800 @@ -33,42 +33,16 @@ thm single_let.fv_bn_eqvt thm single_let.size_eqvt thm single_let.supports +thm single_let.fsupp -lemma test: - "finite (supp (t::trm)) \<and> finite (supp (a::assg))" -apply(rule single_let.induct) -apply(rule supports_finite) -apply(rule single_let.supports) -apply(simp only: finite_supp supp_Pair finite_Un, simp) -apply(rule supports_finite) -apply(rule single_let.supports) -apply(simp only: finite_supp supp_Pair finite_Un, simp) -apply(rule supports_finite) -apply(rule single_let.supports) -apply(simp only: finite_supp supp_Pair finite_Un, simp) -apply(rule supports_finite) -apply(rule single_let.supports) -apply(simp only: finite_supp supp_Pair finite_Un, simp) -apply(rule supports_finite) -apply(rule single_let.supports) -apply(simp only: finite_supp supp_Pair finite_Un, simp) -apply(rule supports_finite) -apply(rule single_let.supports) -apply(simp only: finite_supp supp_Pair finite_Un, simp) -apply(rule supports_finite) -apply(rule single_let.supports) -apply(simp only: finite_supp supp_Pair finite_Un, simp) -apply(rule supports_finite) -apply(rule single_let.supports) -apply(simp only: finite_supp supp_Pair finite_Un, simp) -done + instantiation trm and assg :: fs begin instance apply(default) -apply(simp_all add: test) +apply(simp_all add: single_let.fsupp) done end diff -r 6b51117b8955 -r 217ef3e4282e Nominal/Ex/TypeSchemes.thy --- a/Nominal/Ex/TypeSchemes.thy Sun Aug 29 00:36:47 2010 +0800 +++ b/Nominal/Ex/TypeSchemes.thy Sun Aug 29 01:17:36 2010 +0800 @@ -19,6 +19,15 @@ Var2 "name" | Fun2 "ty2" "ty2" +instantiation ty2 :: fs +begin + +instance +sorry + +end + + nominal_datatype tys2 = All2 xs::"name fset" ty::"ty2" bind (res) xs in ty diff -r 6b51117b8955 -r 217ef3e4282e Nominal/NewParser.thy --- a/Nominal/NewParser.thy Sun Aug 29 00:36:47 2010 +0800 +++ b/Nominal/NewParser.thy Sun Aug 29 01:17:36 2010 +0800 @@ -547,6 +547,11 @@ then prove_supports lthyB qperm_simps qtrms else raise TEST lthyB + val qfsupp_thms = + if get_STEPS lthy > 29 + then prove_fsupp lthyB qtys qinduct qsupports_thms + else raise TEST lthyB + (* noting the theorems *) @@ -566,7 +571,7 @@ ||>> Local_Theory.note ((thms_suffix "induct", []), [qinduct]) ||>> Local_Theory.note ((thms_suffix "exhaust", []), qexhausts) ||>> Local_Theory.note ((thms_suffix "supports", []), qsupports_thms) - + ||>> Local_Theory.note ((thms_suffix "fsupp", []), qfsupp_thms) in (0, lthy9') end handle TEST ctxt => (0, ctxt) diff -r 6b51117b8955 -r 217ef3e4282e Nominal/nominal_dt_supp.ML --- a/Nominal/nominal_dt_supp.ML Sun Aug 29 00:36:47 2010 +0800 +++ b/Nominal/nominal_dt_supp.ML Sun Aug 29 01:17:36 2010 +0800 @@ -8,14 +8,14 @@ signature NOMINAL_DT_SUPP = sig val prove_supports: Proof.context -> thm list -> term list -> thm list - + val prove_fsupp: Proof.context -> typ list -> thm -> thm list -> thm list end structure Nominal_Dt_Supp: NOMINAL_DT_SUPP = struct -(* supports lemmas *) +(* supports lemmas for constructors *) fun mk_supports_goal ctxt qtrm = let @@ -52,7 +52,28 @@ map (prove_supports_single ctxt perm_simps) qtrms +(* finite supp lemmas for qtypes *) +fun prove_fsupp ctxt qtys qinduct qsupports_thms = +let + val (vs, ctxt') = Variable.variant_fixes (replicate (length qtys) "x") ctxt + val goals = vs ~~ qtys + |> map Free + |> map (mk_finite o mk_supp) + |> foldr1 (HOLogic.mk_conj) + |> HOLogic.mk_Trueprop + + val tac = + EVERY' [ rtac @{thm supports_finite}, + resolve_tac qsupports_thms, + asm_simp_tac (HOL_ss addsimps @{thms finite_supp supp_Pair finite_Un}) ] +in + Goal.prove ctxt' [] [] goals + (K (HEADGOAL (rtac qinduct THEN_ALL_NEW tac))) + |> singleton (ProofContext.export ctxt' ctxt) + |> Datatype_Aux.split_conj_thm + |> map zero_var_indexes +end end (* structure *)