# HG changeset patch # User Christian Urban # Date 1292336620 0 # Node ID 666ffc8a92a9bd763ffb57cbf051fc68c51b93a2 # Parent 86e3b39c2a6061984aa0c1c3179f3644cba629cd freshness theorem in strong exhausts; (temporarily includes a cheat_tac to make all tests go through) diff -r 86e3b39c2a60 -r 666ffc8a92a9 Nominal/Ex/Foo2.thy --- a/Nominal/Ex/Foo2.thy Sun Dec 12 22:09:11 2010 +0000 +++ b/Nominal/Ex/Foo2.thy Tue Dec 14 14:23:40 2010 +0000 @@ -24,12 +24,6 @@ "bn (As x y t a) = [atom x] @ bn a" | "bn (As_Nil) = []" -thm foo.exhaust - -ML {* - Variable.import; - Variable.import true @{thms foo.exhaust} @{context} -*} thm foo.bn_defs thm foo.permute_bn @@ -53,6 +47,26 @@ thm foo.supp thm foo.fresh +(* +lemma ex_prop: + shows "\n::nat. Suc n = n" +sorry + +lemma test: + shows "True" +apply - +ML_prf {* + val (x, ctxt') = Obtain.result (K ( + EVERY [print_tac "test", + etac exE 1, + print_tac "end"])) + @{thms ex_prop} @{context}; + ProofContext.verbose := true; + ProofContext.pretty_context ctxt' + |> Pretty.block + |> Pretty.writeln +*} +*) text {* *} @@ -103,7 +117,7 @@ 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 y="y" in foo.exhaust(1)) +apply(rule_tac foo.exhaust(1)) apply(rule assms(1)) apply(rule exI)+ apply(assumption) @@ -111,14 +125,7 @@ apply(rule exI)+ apply(assumption) (* lam case *) -(* -apply(rule Let1_rename) -apply(rule assms(3)) -apply(assumption) -apply(simp) -*) - -apply(subgoal_tac "\p. (p \ {atom name}) \* (c, [atom name], trm)") +apply(subgoal_tac "\p. (p \ {atom name}) \* (c, name, trm)") apply(erule exE) apply(insert Abs_rename_list)[1] apply(drule_tac x="p" in meta_spec) @@ -126,7 +133,7 @@ apply(drule_tac x="trm" in meta_spec) apply(simp only: fresh_star_Pair set.simps) apply(drule meta_mp) -apply(simp) +apply(simp add: fresh_star_def fresh_Nil fresh_Cons fresh_atom_at_base) apply(erule exE) apply(rule assms(3)) apply(perm_simp) diff -r 86e3b39c2a60 -r 666ffc8a92a9 Nominal/Nominal2.thy --- a/Nominal/Nominal2.thy Sun Dec 12 22:09:11 2010 +0000 +++ b/Nominal/Nominal2.thy Tue Dec 14 14:23:40 2010 +0000 @@ -18,20 +18,13 @@ text {* TEST *} ML {* -fun list_implies_rev concl trms = Logic.list_implies (trms, concl) - -fun mk_all (a, T) t = Const ("all", (T --> propT) --> propT) $ Abs (a, T, t) - -fun strip_prems_concl (Const("==>", _) $ A $ B) = strip_prems_concl B |>> cons A - | strip_prems_concl B = ([], B) - fun strip_outer_params (Const("all", _) $ Abs (a, T, t)) = strip_outer_params t |>> cons (a, T) | strip_outer_params B = ([], B) fun strip_params_prems_concl trm = let val (params, body) = strip_outer_params trm - val (prems, concl) = strip_prems_concl body + val (prems, concl) = Logic.strip_horn body in (params, prems, concl) end @@ -40,7 +33,6 @@ Logic.list_implies (prems, concl) |> fold_rev mk_all params - fun mk_binop_env tys c (t, u) = let val ty = fastype_of1 (tys, t) in Const (c, [ty, ty] ---> ty) $ t $ u @@ -58,9 +50,11 @@ ML {* -fun process_ecase lthy c (params, prems, concl) bclauses = +fun process_ecase lthy c (params, prems, concl) binders = let - fun binder tys (opt, i) = + val tys = map snd params + + fun prep_binder (opt, i) = let val t = Bound (length tys - i - 1) in @@ -69,14 +63,12 @@ | SOME bn => to_set_ty (fastype_of1 (tys, bn $ t)) (bn $ t) end - val param_tys = map snd params - val fresh_prem = - case (get_all_binders bclauses) of + case binders of [] => [] (* case: no binders *) | binders => binders (* case: binders *) - |> map (binder param_tys) - |> fold_union_env param_tys + |> map prep_binder + |> fold_union_env tys |> (fn t => mk_fresh_star t c) |> HOLogic.mk_Trueprop |> single @@ -85,40 +77,78 @@ end *} +ML {* +fun fresh_thm ctxt c params 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)) + + val rhs = HOLogic.mk_tuple (c :: params) + val lhs = binders + |> map prep_binder + |> fold_union + |> mk_perm (Bound 0) + + 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 + in + Goal.prove ctxt [] [] goal + (K (HEADGOAL (rtac @{thm at_set_avoiding1} + THEN_ALL_NEW (simp_tac (HOL_ss addsimps ss))))) + end +*} + ML {* -fun mk_strong_exhausts_goal lthy qexhausts bclausesss = +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 val ([c, a], lthy'') = Variable.variant_fixes ["c", "'a"] lthy' val c = Free (c, TFree (a, @{sort fs})) - val (ecases, main_concls) = qexhausts' + 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 strip_prems_concl + |> map Logic.strip_horn |> split_list - |>> map (map strip_params_prems_concl) - in - map2 (map2 (process_ecase lthy'' c)) ecases bclausesss - |> map2 list_implies_rev main_concls - |> rpair lthy'' - end + |>> map (map strip_params_prems_concl) -fun prove_strong_exhausts lthy qexhausts qtrms bclausesss = - let - val (goal, lthy') = mk_strong_exhausts_goal lthy qexhausts bclausesss + val prems = map2 (process_ecase lthy'' c) (flat ecases) (flat binderss) - val _ = goal - |> map (Syntax.check_term lthy') - |> map (Syntax.string_of_term lthy') - |> cat_lines - |> tracing + val _ = tracing ("binderss: " ^ @{make_string} binderss) in - @{thms TrueI} + 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')]) end *} + + ML {* val eqvt_attr = Attrib.internal (K Nominal_ThmDecls.eqvt_add) val rsp_attr = Attrib.internal (K Quotient_Info.rsp_rules_add) @@ -631,7 +661,7 @@ then prove_permute_bn_thms qtys qbns qperm_bns qinduct qperm_bn_simps qbn_defs qfv_qbn_eqvts lthyC else [] - val qstrong_exhaust_thms = prove_strong_exhausts lthyC qexhausts qtrms bclauses + val qstrong_exhaust_thms = prove_strong_exhausts lthyC qexhausts qtrms bclauses qbn_finite_thms (* noting the theorems *) diff -r 86e3b39c2a60 -r 666ffc8a92a9 Nominal/Nominal2_Base.thy --- a/Nominal/Nominal2_Base.thy Sun Dec 12 22:09:11 2010 +0000 +++ b/Nominal/Nominal2_Base.thy Tue Dec 14 14:23:40 2010 +0000 @@ -1835,6 +1835,12 @@ shows "a \ b \ a \ atom b" unfolding fresh_def by (simp add: supp_at_base) +lemma fresh_atom_at_base: + fixes b::"'a::at_base" + shows "a \ atom b \ a \ b" + by (simp add: fresh_def supp_at_base supp_atom) + + instance at_base < fs proof qed (simp add: supp_at_base) diff -r 86e3b39c2a60 -r 666ffc8a92a9 Nominal/nominal_library.ML --- a/Nominal/nominal_library.ML Sun Dec 12 22:09:11 2010 +0000 +++ b/Nominal/nominal_library.ML Tue Dec 14 14:23:40 2010 +0000 @@ -16,6 +16,7 @@ val dest_fsetT: typ -> typ val mk_id: term -> term + val mk_all: (string * typ) -> term -> term val size_const: typ -> term @@ -154,6 +155,8 @@ Const (@{const_name id}, ty --> ty) $ trm end +fun mk_all (a, T) t = Term.all T $ Abs (a, T, t) + fun size_const ty = Const (@{const_name size}, ty --> @{typ nat})