# HG changeset patch # User Christian Urban # Date 1292927288 0 # Node ID dd7490fdd998222dd02c9fbf60808f032ef57876 # Parent d5713db7e146d01df1b7dc4d16c64b64a0119e53 all examples for strong exhausts work; recursive binders need to be treated differently; still unclean version with lots of diagnostic code diff -r d5713db7e146 -r dd7490fdd998 Nominal/Ex/Foo2.thy --- a/Nominal/Ex/Foo2.thy Sun Dec 19 07:50:37 2010 +0000 +++ b/Nominal/Ex/Foo2.thy Tue Dec 21 10:28:08 2010 +0000 @@ -27,6 +27,7 @@ + thm foo.bn_defs thm foo.permute_bn thm foo.perm_bn_alpha @@ -49,28 +50,167 @@ thm foo.supp thm foo.fresh -(* -lemma ex_prop: - shows "\n::nat. Suc n = n" -sorry +lemma at_set_avoiding5: + assumes "finite xs" + and "finite (supp c)" + shows "\p. (p \ xs) \* c \ supp p = xs \ p \ xs" +using assms +apply(erule_tac c="c" in at_set_avoiding) +apply(auto) +done + -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 -*} -*) +lemma Abs_rename_lst3: + fixes x::"'a::fs" + assumes a: "(p \ (set bs)) \* (bs, x)" + shows "\q. [bs]lst. x = [p \ bs]lst. (q \ x) \ p \ bs = q \ bs" +proof - + from a have "p \ (set bs) \ (set bs) = {}" using at_fresh_star_inter + by (simp add: fresh_star_Pair fresh_star_set) + with list_renaming_perm + obtain q where *: "q \ bs = p \ bs" and **: "supp q \ set bs \ (p \ set bs)" by metis + have "[bs]lst. x = q \ ([bs]lst. x)" + apply(rule perm_supp_eq[symmetric]) + using a ** + unfolding fresh_star_Pair + unfolding Abs_fresh_star_iff + unfolding fresh_star_def + by auto + also have "\ = [q \ bs]lst. (q \ x)" by simp + also have "\ = [p \ bs]lst. (q \ x)" using * by simp + finally have "[bs]lst. x = [p \ bs]lst. (q \ x)" . + then show "\q. [bs]lst. x = [p \ bs]lst. (q \ x) \ p \ bs = q \ bs" + using * ** by metis +qed +lemma + fixes c::"'a::fs" + assumes a: "\assg1 trm1 assg2 trm2. \((set (bn assg1)) \ (set (bn assg2))) \* c; y = Let1 assg1 trm1 assg2 trm2\ \ P" + shows "y = Let1 assg1 trm1 assg2 trm2 \ P" +apply - +apply(subgoal_tac "\p. (p \ ((set (bn assg1)) \ (set (bn assg2)))) \* (c, bn assg1, bn assg2, trm1, trm2) \ + supp p = (set (bn assg1)) \ (set (bn assg2)) \ (p \ ((set (bn assg1)) \ (set (bn assg2))))") +defer +apply(rule at_set_avoiding5) +apply(simp add: foo.bn_finite) +apply(simp add: supp_Pair finite_supp) +apply(erule exE) +apply(perm_simp add: foo.permute_bn) +apply(simp add: fresh_star_Pair) +apply(erule conjE)+ +thm Abs_rename_lst +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_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) +apply(drule meta_mp) +apply(perm_simp add: foo.permute_bn) +apply(simp add: fresh_star_Pair fresh_star_Un) +apply(drule meta_mp) +apply(perm_simp add: foo.permute_bn) +apply(simp add: fresh_star_Pair fresh_star_Un) +apply(erule exE)+ +apply(rule a) +apply(assumption) +apply(simp only: foo.eq_iff) +apply(perm_simp add: foo.permute_bn) +apply(rule conjI) +apply(rule refl) +apply(rule conjI) +apply(rule foo.perm_bn_alpha) +apply(rule conjI) +apply(perm_simp add: foo.permute_bn) +apply(rule refl) +apply(rule foo.perm_bn_alpha) +done + +lemma + fixes c::"'a::fs" + assumes a: "\assg1 trm1 assg2 trm2. \((set (bn assg1)) \ (set (bn assg2))) \* c; y = Let1 assg1 trm1 assg2 trm2\ \ P" + shows "y = Let1 assg1 trm1 assg2 trm2 \ P" +apply - +apply(subgoal_tac "\p. (p \ ((set (bn assg1)) \ (set (bn assg2)))) \* (c, bn assg1, bn assg2, trm1, trm2) \ + supp p = (set (bn assg1)) \ (set (bn assg2)) \ (p \ ((set (bn assg1)) \ (set (bn assg2))))") +defer +apply(rule at_set_avoiding5) +apply(simp add: foo.bn_finite) +apply(simp add: supp_Pair finite_supp) +apply(erule exE) +apply(perm_simp add: foo.permute_bn) +apply(simp add: fresh_star_Pair) +apply(erule conjE)+ +apply(insert Abs_rename_lst3)[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_lst3)[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) +apply(drule meta_mp) +apply(perm_simp add: foo.permute_bn) +apply(simp add: fresh_star_Pair fresh_star_Un) +apply(drule meta_mp) +apply(perm_simp add: foo.permute_bn) +apply(simp add: fresh_star_Pair fresh_star_Un) +apply(erule exE)+ +apply(erule conjE)+ +apply(simp add: foo.permute_bn) +apply(rule a) +apply(assumption) +apply(clarify) +apply(simp (no_asm) only: foo.eq_iff) +apply(rule conjI) +apply(assumption) +apply(rule conjI) +apply(rule foo.perm_bn_alpha) +apply(rule conjI) +apply(assumption) +apply(rule foo.perm_bn_alpha) +done + + +lemma + fixes c::"'a::fs" + assumes a: "\assg1 trm1 assg2 trm2. \((set (bn assg1)) \ (set (bn assg2))) \* c; y = Let1 assg1 trm1 assg2 trm2\ \ P" + shows "y = Let1 assg1 trm1 assg2 trm2 \ P" +apply - +apply(subgoal_tac "\p. (p \ ((set (bn assg1)) \ (set (bn assg2)))) \* (c, bn assg1, bn assg2, trm1, trm2) \ + supp p = (set (bn assg1)) \ (set (bn assg2)) \ (p \ ((set (bn assg1)) \ (set (bn assg2))))") +defer +apply(rule at_set_avoiding5) +apply(simp add: foo.bn_finite) +apply(simp add: supp_Pair finite_supp) +apply(erule exE) +apply(simp add: fresh_star_Pair) +apply(erule conjE)+ +apply(simp (no_asm_use) only: foo.permute_bn set_eqvt union_eqvt) +apply(rule a) +apply(assumption) +apply(clarify) +apply(simp (no_asm) only: foo.eq_iff) +apply(rule conjI) +apply(rule trans) +apply(rule_tac p="p" in supp_perm_eq[symmetric]) +apply(rule fresh_star_supp_conv) +apply(simp (no_asm_use) add: fresh_star_def) +apply(simp (no_asm_use) add: Abs_fresh_iff)[1] +apply(rule ballI) +apply(auto simp add: fresh_Pair)[1] +apply(simp (no_asm_use) only: permute_Abs) +apply(simp (no_asm_use) only: multi_recs.fv_bn_eqvt) +apply(simp) +apply(rule at_set_avoiding5) +apply(simp add: multi_recs.bn_finite) +apply(simp add: supp_Pair finite_supp) +apply(rule finite_sets_supp) +apply(simp add: multi_recs.bn_finite) +done @@ -112,14 +252,9 @@ (* let1 case *) 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_lst)[1] apply(drule_tac x="p" in meta_spec) apply(drule_tac x="bn assg1" in meta_spec) @@ -129,21 +264,22 @@ apply(drule_tac x="bn assg2" in meta_spec) apply(drule_tac x="trm2" in meta_spec) apply(drule meta_mp) -apply(simp only: union_eqvt fresh_star_Pair set.simps fresh_star_Un, simp) +apply(perm_simp add: foo.permute_bn) +apply(simp add: fresh_star_Pair fresh_star_Un) apply(drule meta_mp) -apply(simp only: union_eqvt fresh_star_Pair set.simps fresh_star_Un, simp) +apply(perm_simp add: foo.permute_bn) +apply(simp add: fresh_star_Pair fresh_star_Un) apply(erule exE)+ -apply(perm_simp add: foo.permute_bn) -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(perm_simp add: foo.permute_bn) apply(rule refl) apply(rule conjI) apply(rule foo.perm_bn_alpha) apply(rule conjI) +apply(perm_simp add: foo.permute_bn) apply(rule refl) apply(rule foo.perm_bn_alpha) apply(rule at_set_avoiding1) diff -r d5713db7e146 -r dd7490fdd998 Nominal/Ex/LetFun.thy --- a/Nominal/Ex/LetFun.thy Sun Dec 19 07:50:37 2010 +0000 +++ b/Nominal/Ex/LetFun.thy Tue Dec 21 10:28:08 2010 +0000 @@ -8,7 +8,6 @@ bp-names in p are bound only in e1 *) -declare [[STEPS = 100]] nominal_datatype exp = Var name diff -r d5713db7e146 -r dd7490fdd998 Nominal/Ex/Multi_Recs.thy --- a/Nominal/Ex/Multi_Recs.thy Sun Dec 19 07:50:37 2010 +0000 +++ b/Nominal/Ex/Multi_Recs.thy Tue Dec 21 10:28:08 2010 +0000 @@ -50,30 +50,6 @@ thm multi_recs.bn_finite -lemma Abs_rename_set2: - fixes x::"'a::fs" - assumes a: "(p \ cs) \* (cs, x)" - and b: "finite cs" - shows "\q. [cs]set. x = [p \ cs]set. (q \ x) \ q \ cs = p \ cs \ supp q \ cs \ (p \ cs)" -proof - - from a b have "p \ cs \ cs = {}" using at_fresh_star_inter by (auto simp add: fresh_star_Pair) - with set_renaming_perm - obtain q where *: "q \ cs = p \ cs" and **: "supp q \ cs \ (p \ cs)" using b by metis - have "[cs]set. x = q \ ([cs]set. x)" - apply(rule perm_supp_eq[symmetric]) - using a ** - unfolding fresh_star_Pair - unfolding Abs_fresh_star_iff - unfolding fresh_star_def - by auto - also have "\ = [q \ cs]set. (q \ x)" by simp - also have "\ = [p \ cs]set. (q \ x)" using * by simp - finally have "[cs]set. x = [p \ cs]set. (q \ x)" . - then show "\q. [cs]set. x = [p \ cs]set. (q \ x) \ q \ cs = p \ cs \ supp q \ cs \ (p \ cs)" - using * ** - by (blast) -qed - lemma at_set_avoiding5: assumes "finite xs" and "finite (supp c)" @@ -88,47 +64,36 @@ assumes a: "\lrbs exp. \bs lrbs \* c; y = LetRec lrbs exp\ \ P" shows "y = LetRec lrbs exp \ P" apply - -apply(subgoal_tac "\p. ((p \ (bs lrbs)) \* (c, bs lrbs, lrbs, exp)) \ supp p = bs lrbs \ (p \ (bs lrbs))") +apply(subgoal_tac "\p. ((p \ (bs lrbs)) \* (c, bs lrbs, lrbs, exp))") apply(erule exE) apply(simp add: fresh_star_Pair) apply(erule conjE)+ apply(simp add: multi_recs.fv_bn_eqvt) -(* -using Abs_rename_set2 +using Abs_rename_set' apply - apply(drule_tac x="p" in meta_spec) apply(drule_tac x="bs lrbs" in meta_spec) -apply(drule_tac x="lrbs" in meta_spec) +apply(drule_tac x="(lrbs, exp)" in meta_spec) apply(drule meta_mp) apply(simp add: multi_recs.fv_bn_eqvt fresh_star_Pair) apply(drule meta_mp) apply(simp add: multi_recs.bn_finite) apply(erule exE) +apply(erule conjE) +apply(rotate_tac 6) +apply(drule sym) apply(simp add: multi_recs.fv_bn_eqvt) -*) apply(rule a) apply(assumption) apply(clarify) apply(simp (no_asm) only: multi_recs.eq_iff) -apply(rule trans) -apply(rule_tac p="p" in supp_perm_eq[symmetric]) -apply(rule fresh_star_supp_conv) -apply(simp (no_asm_use) add: fresh_star_def) -apply(simp (no_asm_use) add: Abs_fresh_iff)[1] -apply(rule ballI) -apply(auto simp add: fresh_Pair)[1] -apply(simp (no_asm_use) only: permute_Abs) -apply(simp (no_asm_use) only: multi_recs.fv_bn_eqvt) -apply(simp) -apply(rule at_set_avoiding5) +apply(rule at_set_avoiding1) apply(simp add: multi_recs.bn_finite) apply(simp add: supp_Pair finite_supp) apply(rule finite_sets_supp) apply(simp add: multi_recs.bn_finite) done - - end diff -r d5713db7e146 -r dd7490fdd998 Nominal/Ex/SingleLet.thy --- a/Nominal/Ex/SingleLet.thy Sun Dec 19 07:50:37 2010 +0000 +++ b/Nominal/Ex/SingleLet.thy Tue Dec 21 10:28:08 2010 +0000 @@ -4,8 +4,6 @@ atom_decl name -declare [[STEPS = 100]] - nominal_datatype single_let: trm = Var "name" | App "trm" "trm" diff -r d5713db7e146 -r dd7490fdd998 Nominal/Nominal2.thy --- a/Nominal/Nominal2.thy Sun Dec 19 07:50:37 2010 +0000 +++ b/Nominal/Nominal2.thy Tue Dec 21 10:28:08 2010 +0000 @@ -116,7 +116,8 @@ ML {* (* derives abs_eq theorems of the form Exists s. [as].t = [p o as].s *) -fun abs_eq_thm ctxt fprops p parms bn_finite_thms (BC (bmode, binders, bodies)) = +fun abs_eq_thm ctxt fprops p parms bn_finite_thms bn_eqvt permute_bns + (bclause as (BC (bmode, binders, bodies))) = case binders of [] => [] | _ => @@ -133,37 +134,85 @@ 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)) + val abs_rhs = abs $ mk_perm p binder_trm $ mk_perm (Bound 0) body_trm + val abs_rhs' = abs $ mk_perm (Bound 0) binder_trm $ mk_perm (Bound 0) body_trm + val abs_eq = HOLogic.mk_eq (abs_lhs, abs_rhs) + val abs_eq' = HOLogic.mk_eq (abs_lhs, abs_rhs') + val eq = HOLogic.mk_eq (mk_perm (Bound 0) binder_trm, mk_perm p binder_trm) + + val goal = HOLogic.mk_conj (abs_eq, eq) + |> (fn t => HOLogic.mk_exists ("q", @{typ "perm"}, t)) |> HOLogic.mk_Trueprop + + val goal' = HOLogic.mk_conj (abs_eq', eq) + |> (fn t => HOLogic.mk_exists ("q", @{typ "perm"}, 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} + 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))))] + if is_recursive_binder bclause + then + (tracing "recursive"; + [ 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)))) + |> Nominal_Permeq.eqvt_strict_rule ctxt bn_eqvt [] + ]) + else + (tracing "non-recursive"; + [ 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)))) + |> Nominal_Permeq.eqvt_strict_rule ctxt permute_bns [] + ]) end *} - -(* FIXME: use pure cterm functions *) ML {* -fun mk_cperm ctxt p ctrm = - mk_perm (term_of p) (term_of ctrm) - |> cterm_of (ProofContext.theory_of ctxt) +fun conj_tac tac i = + let + fun select (t, i) = + case t of + @{term "Trueprop"} $ t' => select (t', i) + | @{term "op \"} $ _ $ _ => (rtac @{thm conjI} THEN' RANGE [conj_tac tac, conj_tac tac]) i + | _ => tac i + in + SUBGOAL select i + end *} +ML {* +fun is_abs_eq thm = + let + fun is_abs trm = + case (head_of trm) of + Const (@{const_name "Abs_set"}, _) => true + | Const (@{const_name "Abs_lst"}, _) => true + | Const (@{const_name "Abs_res"}, _) => true + | _ => false + in + thm |> prop_of + |> HOLogic.dest_Trueprop + |> HOLogic.dest_eq + |> fst + |> is_abs + end +*} + +lemma setify: + shows "xs = ys \ set xs = set ys" + by simp ML {* -fun case_tac ctxt c bn_finite_thms (prems, bclausess) thm = +fun case_tac ctxt c bn_finite_thms eq_iff_thms bn_eqvt permute_bns perm_bn_alphas + (prems, bclausess) qexhaust_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, ...} => + | binders => Subgoal.SUBPROOF (fn {params, prems, concl, context = ctxt, ...} => let val parms = map (term_of o snd) params val fthm = fresh_thm ctxt c parms binders bn_finite_thms @@ -172,36 +221,76 @@ val (([(_, fperm)], fprops), ctxt') = Obtain.result (K (EVERY1 [etac exE, full_simp_tac (HOL_basic_ss addsimps ss), - REPEAT o (etac conjE)])) [fthm] ctxt + REPEAT o (etac @{thm conjE})])) [fthm] ctxt - val abs_eqs = flat (map (abs_eq_thm ctxt fprops (term_of fperm) parms bn_finite_thms) bclauses) + val abs_eq_thms = flat + (map (abs_eq_thm ctxt fprops (term_of fperm) parms bn_finite_thms bn_eqvt permute_bns) bclauses) + + val ((_, eqs), ctxt'') = Obtain.result + (K (EVERY1 + [ REPEAT o (etac @{thm exE}), + REPEAT o (etac @{thm conjE}), + REPEAT o (dtac @{thm setify}), + full_simp_tac (HOL_basic_ss addsimps @{thms set_append set.simps})])) abs_eq_thms ctxt' + + val (abs_eqs, peqs) = split_filter is_abs_eq eqs + + val fprops' = map (Nominal_Permeq.eqvt_strict_rule ctxt permute_bns []) fprops + val fprops'' = map (Nominal_Permeq.eqvt_strict_rule ctxt bn_eqvt []) fprops - val _ = tracing ("test") - (* - val _ = tracing ("fprop:\n" ^ cat_lines (map (Syntax.string_of_term ctxt' o prop_of) fprops)) - *) - (* - val _ = tracing ("abs_eqs:\n" ^ cat_lines (map (Syntax.string_of_term ctxt' o prop_of) abs_eqs)) - *) + val _ = tracing ("prem:\n" ^ (Syntax.string_of_term ctxt'' o prop_of) prem) + val _ = tracing ("prems:\n" ^ cat_lines (map (Syntax.string_of_term ctxt'' o prop_of) prems)) + val _ = tracing ("fprop':\n" ^ cat_lines (map (Syntax.string_of_term ctxt'' o prop_of) fprops')) + val _ = tracing ("fprop'':\n" ^ cat_lines (map (Syntax.string_of_term ctxt'' o prop_of) fprops'')) + val _ = tracing ("abseq:\n" ^ cat_lines (map (Syntax.string_of_term ctxt'' o prop_of) abs_eqs)) + val _ = tracing ("peqs:\n" ^ cat_lines (map (Syntax.string_of_term ctxt'' o prop_of) peqs)) + + + val tac1 = EVERY' + [ simp_tac (HOL_basic_ss addsimps peqs), + rewrite_goal_tac (@{thms fresh_star_Un[THEN eq_reflection]}), + K (print_tac "before solving freshness"), + conj_tac (TRY o DETERM o resolve_tac (fprops' @ fprops'')) ] + + val tac2 = EVERY' + [ rtac (@{thm ssubst} OF prems), + rewrite_goal_tac (map safe_mk_equiv eq_iff_thms), + K (print_tac "before substituting"), + rewrite_goal_tac (map safe_mk_equiv abs_eqs), + K (print_tac "after substituting"), + conj_tac (TRY o DETERM o resolve_tac (@{thms refl} @ perm_bn_alphas)), + K (print_tac "end") + ] + + val side_thm = Goal.prove ctxt'' [] [] (term_of concl) + (fn _ => (* Skip_Proof.cheat_tac (ProofContext.theory_of ctxt'') *) + EVERY + [ rtac prem 1, + print_tac "after applying prem", + RANGE [SOLVED' tac1, SOLVED' tac2] 1, + print_tac "final" ] ) + |> singleton (ProofContext.export ctxt'' ctxt) + + val _ = tracing ("side_thm:\n" ^ (Syntax.string_of_term ctxt o prop_of) side_thm) in - (*HEADGOAL (rtac prem THEN' RANGE [K all_tac, simp_tac (HOL_basic_ss addsimps prems)])*) - Skip_Proof.cheat_tac (ProofContext.theory_of ctxt') + rtac side_thm 1 end) ctxt in - rtac thm THEN' RANGE (map2 aux_tac prems bclausess) + rtac qexhaust_thm THEN' RANGE (map2 aux_tac prems bclausess) end *} ML {* -fun prove_strong_exhausts lthy qexhausts qtrms bclausesss bn_finite_thms = +fun prove_strong_exhausts lthy exhausts qtrms bclausesss bn_finite_thms eq_iff_thms bn_eqvt permute_bns + perm_bn_alphas = let - val ((_, qexhausts'), lthy') = Variable.import true qexhausts lthy + val ((_, exhausts'), lthy') = Variable.import true exhausts lthy val ([c, a], lthy'') = Variable.variant_fixes ["c", "'a"] lthy' val c = Free (c, TFree (a, @{sort fs})) - val (ecases, main_concls) = qexhausts' (* ecases or of the form (params, prems, concl) *) + val (ecases, main_concls) = exhausts' (* ecases or of the form (params, prems, concl) *) |> map prop_of |> map Logic.strip_horn |> split_list @@ -215,7 +304,8 @@ val prems' = partitions prems (map length bclausesss) in EVERY1 [Goal.conjunction_tac, - RANGE (map2 (case_tac context c bn_finite_thms) (prems' ~~ bclausesss) qexhausts')] + RANGE (map2 (case_tac context c bn_finite_thms eq_iff_thms bn_eqvt permute_bns perm_bn_alphas) + (prems' ~~ bclausesss) exhausts')] end) end *} @@ -582,7 +672,7 @@ (* defining of quotient term-constructors, binding functions, free vars functions *) val _ = warning "Defining the quotient constants" val qconstrs_descrs = - map2 (map2 (fn (b, _, mx) => fn t => (Name.of_binding b, t, mx))) (get_cnstrs dts) raw_constrs + (map2 o map2) (fn (b, _, mx) => fn t => (Name.of_binding b, t, mx)) (get_cnstrs dts) raw_constrs val qbns_descr = map2 (fn (b, _, mx) => fn t => (Name.of_binding b, t, mx)) bn_funs raw_bns @@ -734,7 +824,9 @@ 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 qbn_finite_thms + val qstrong_exhaust_thms = prove_strong_exhausts lthyC qexhausts qtrms bclauses qbn_finite_thms qeq_iffs' + qfv_qbn_eqvts qpermute_bn_thms qperm_bn_alpha_thms + (* noting the theorems *) @@ -917,7 +1009,7 @@ bcs @ (flat (map_range (add bcs) n)) end in - map2 (map2 complt) args bclauses + (map2 o map2) complt args bclauses end *} diff -r d5713db7e146 -r dd7490fdd998 Nominal/Nominal2_Abs.thy --- a/Nominal/Nominal2_Abs.thy Sun Dec 19 07:50:37 2010 +0000 +++ b/Nominal/Nominal2_Abs.thy Tue Dec 21 10:28:08 2010 +0000 @@ -547,7 +547,7 @@ fixes x::"'a::fs" assumes a: "(p \ bs) \* (bs, x)" and b: "finite bs" - shows "\y. [bs]set. x = [p \ bs]set. y" + shows "\q. [bs]set. x = [p \ bs]set. (q \ x) \ q \ bs = p \ bs" proof - from a b have "p \ bs \ bs = {}" using at_fresh_star_inter by (auto simp add: fresh_star_Pair) with set_renaming_perm @@ -560,16 +560,15 @@ unfolding fresh_star_def by auto also have "\ = [q \ bs]set. (q \ x)" by simp - also have "\ = [p \ bs]set. (q \ x)" using * by simp - finally have "[bs]set. x = [p \ bs]set. (q \ x)" . - then show "\y. [bs]set. x = [p \ bs]set. y" by blast + finally have "[bs]set. x = [p \ bs]set. (q \ x)" by (simp add: *) + then show "\q. [bs]set. x = [p \ bs]set. (q \ x) \ q \ bs = p \ bs" using * by metis qed lemma Abs_rename_res: fixes x::"'a::fs" assumes a: "(p \ bs) \* (bs, x)" and b: "finite bs" - shows "\y. [bs]res. x = [p \ bs]res. y" + shows "\q. [bs]res. x = [p \ bs]res. (q \ x) \ q \ bs = p \ bs" proof - from a b have "p \ bs \ bs = {}" using at_fresh_star_inter by (simp add: fresh_star_Pair) with set_renaming_perm @@ -582,15 +581,14 @@ unfolding fresh_star_def by auto also have "\ = [q \ bs]res. (q \ x)" by simp - also have "\ = [p \ bs]res. (q \ x)" using * by simp - finally have "[bs]res. x = [p \ bs]res. (q \ x)" . - then show "\y. [bs]res. x = [p \ bs]res. y" by blast + finally have "[bs]res. x = [p \ bs]res. (q \ x)" by (simp add: *) + then show "\q. [bs]res. x = [p \ bs]res. (q \ x) \ q \ bs = p \ bs" using * by metis qed lemma Abs_rename_lst: fixes x::"'a::fs" assumes a: "(p \ (set bs)) \* (bs, x)" - shows "\y. [bs]lst. x = [p \ bs]lst. y" + shows "\q. [bs]lst. x = [p \ bs]lst. (q \ x) \ q \ bs = p \ bs" proof - from a have "p \ (set bs) \ (set bs) = {}" using at_fresh_star_inter by (simp add: fresh_star_Pair fresh_star_set) @@ -604,12 +602,32 @@ unfolding fresh_star_def by auto also have "\ = [q \ bs]lst. (q \ x)" by simp - also have "\ = [p \ bs]lst. (q \ x)" using * by simp - finally have "[bs]lst. x = [p \ bs]lst. (q \ x)" . - then show "\y. [bs]lst. x = [p \ bs]lst. y" by blast + finally have "[bs]lst. x = [p \ bs]lst. (q \ x)" by (simp add: *) + then show "\q. [bs]lst. x = [p \ bs]lst. (q \ x) \ q \ bs = p \ bs" using * by metis qed +text {* for deep recursive binders *} + +lemma Abs_rename_set': + fixes x::"'a::fs" + assumes a: "(p \ bs) \* (bs, x)" + and b: "finite bs" + shows "\q. [bs]set. x = [q \ bs]set. (q \ x) \ q \ bs = p \ bs" +using Abs_rename_set[OF a b] by metis + +lemma Abs_rename_res': + fixes x::"'a::fs" + assumes a: "(p \ bs) \* (bs, x)" + and b: "finite bs" + shows "\q. [bs]res. x = [q \ bs]res. (q \ x) \ q \ bs = p \ bs" +using Abs_rename_res[OF a b] by metis + +lemma Abs_rename_lst': + fixes x::"'a::fs" + assumes a: "(p \ (set bs)) \* (bs, x)" + shows "\q. [bs]lst. x = [q \ bs]lst. (q \ x) \ q \ bs = p \ bs" +using Abs_rename_lst[OF a] by metis section {* Infrastructure for building tuples of relations and functions *} diff -r d5713db7e146 -r dd7490fdd998 Nominal/nominal_dt_rawfuns.ML --- a/Nominal/nominal_dt_rawfuns.ML Sun Dec 19 07:50:37 2010 +0000 +++ b/Nominal/nominal_dt_rawfuns.ML Tue Dec 21 10:28:08 2010 +0000 @@ -18,6 +18,7 @@ datatype bclause = BC of bmode * (term option * int) list * int list val get_all_binders: bclause list -> (term option * int) list + val is_recursive_binder: bclause -> bool val define_raw_bns: string list -> dt_info -> (binding * typ option * mixfix) list -> (Attrib.binding * term) list -> thm list -> thm list -> local_theory -> @@ -64,6 +65,12 @@ |> flat |> remove_dups (op =) +fun is_recursive_binder (BC (_, binders, bodies)) = + case (inter (op =) (map snd binders) bodies) of + nil => false + | _ => true + + fun lookup xs x = the (AList.lookup (op=) xs x) diff -r d5713db7e146 -r dd7490fdd998 Nominal/nominal_library.ML --- a/Nominal/nominal_library.ML Sun Dec 19 07:50:37 2010 +0000 +++ b/Nominal/nominal_library.ML Tue Dec 21 10:28:08 2010 +0000 @@ -10,6 +10,7 @@ val order: ('a * 'a -> bool) -> 'a list -> ('a * 'b) list -> 'b list val remove_dups: ('a * 'a -> bool) -> 'a list -> 'a list val partitions: 'a list -> int list -> 'a list list + val split_filter: ('a -> bool) -> 'a list -> 'a list * 'a list val is_true: term -> bool @@ -146,6 +147,15 @@ head :: partitions tail js end +fun split_filter f [] = ([], []) + | split_filter f (x :: xs) = + let + val (r, l) = split_filter f xs + in + if f x + then (x :: r, l) + else (r, x :: l) + end fun is_true @{term "Trueprop True"} = true