all examples for strong exhausts work; recursive binders need to be treated differently; still unclean version with lots of diagnostic code
--- 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 "\<exists>n::nat. Suc n = n"
-sorry
+lemma at_set_avoiding5:
+ assumes "finite xs"
+ and "finite (supp c)"
+ shows "\<exists>p. (p \<bullet> xs) \<sharp>* c \<and> supp p = xs \<union> p \<bullet> 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 \<bullet> (set bs)) \<sharp>* (bs, x)"
+ shows "\<exists>q. [bs]lst. x = [p \<bullet> bs]lst. (q \<bullet> x) \<and> p \<bullet> bs = q \<bullet> bs"
+proof -
+ from a have "p \<bullet> (set bs) \<inter> (set bs) = {}" using at_fresh_star_inter
+ by (simp add: fresh_star_Pair fresh_star_set)
+ with list_renaming_perm
+ obtain q where *: "q \<bullet> bs = p \<bullet> bs" and **: "supp q \<subseteq> set bs \<union> (p \<bullet> set bs)" by metis
+ have "[bs]lst. x = q \<bullet> ([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 "\<dots> = [q \<bullet> bs]lst. (q \<bullet> x)" by simp
+ also have "\<dots> = [p \<bullet> bs]lst. (q \<bullet> x)" using * by simp
+ finally have "[bs]lst. x = [p \<bullet> bs]lst. (q \<bullet> x)" .
+ then show "\<exists>q. [bs]lst. x = [p \<bullet> bs]lst. (q \<bullet> x) \<and> p \<bullet> bs = q \<bullet> bs"
+ using * ** by metis
+qed
+lemma
+ fixes c::"'a::fs"
+ assumes a: "\<And>assg1 trm1 assg2 trm2. \<lbrakk>((set (bn assg1)) \<union> (set (bn assg2))) \<sharp>* c; y = Let1 assg1 trm1 assg2 trm2\<rbrakk> \<Longrightarrow> P"
+ shows "y = Let1 assg1 trm1 assg2 trm2 \<Longrightarrow> P"
+apply -
+apply(subgoal_tac "\<exists>p. (p \<bullet> ((set (bn assg1)) \<union> (set (bn assg2)))) \<sharp>* (c, bn assg1, bn assg2, trm1, trm2) \<and>
+ supp p = (set (bn assg1)) \<union> (set (bn assg2)) \<union> (p \<bullet> ((set (bn assg1)) \<union> (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: "\<And>assg1 trm1 assg2 trm2. \<lbrakk>((set (bn assg1)) \<union> (set (bn assg2))) \<sharp>* c; y = Let1 assg1 trm1 assg2 trm2\<rbrakk> \<Longrightarrow> P"
+ shows "y = Let1 assg1 trm1 assg2 trm2 \<Longrightarrow> P"
+apply -
+apply(subgoal_tac "\<exists>p. (p \<bullet> ((set (bn assg1)) \<union> (set (bn assg2)))) \<sharp>* (c, bn assg1, bn assg2, trm1, trm2) \<and>
+ supp p = (set (bn assg1)) \<union> (set (bn assg2)) \<union> (p \<bullet> ((set (bn assg1)) \<union> (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: "\<And>assg1 trm1 assg2 trm2. \<lbrakk>((set (bn assg1)) \<union> (set (bn assg2))) \<sharp>* c; y = Let1 assg1 trm1 assg2 trm2\<rbrakk> \<Longrightarrow> P"
+ shows "y = Let1 assg1 trm1 assg2 trm2 \<Longrightarrow> P"
+apply -
+apply(subgoal_tac "\<exists>p. (p \<bullet> ((set (bn assg1)) \<union> (set (bn assg2)))) \<sharp>* (c, bn assg1, bn assg2, trm1, trm2) \<and>
+ supp p = (set (bn assg1)) \<union> (set (bn assg2)) \<union> (p \<bullet> ((set (bn assg1)) \<union> (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 "\<exists>p. (p \<bullet> ((set (bn assg1)) \<union> (set (bn assg2)))) \<sharp>* (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)
--- 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
--- 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 \<bullet> cs) \<sharp>* (cs, x)"
- and b: "finite cs"
- shows "\<exists>q. [cs]set. x = [p \<bullet> cs]set. (q \<bullet> x) \<and> q \<bullet> cs = p \<bullet> cs \<and> supp q \<subseteq> cs \<union> (p \<bullet> cs)"
-proof -
- from a b have "p \<bullet> cs \<inter> cs = {}" using at_fresh_star_inter by (auto simp add: fresh_star_Pair)
- with set_renaming_perm
- obtain q where *: "q \<bullet> cs = p \<bullet> cs" and **: "supp q \<subseteq> cs \<union> (p \<bullet> cs)" using b by metis
- have "[cs]set. x = q \<bullet> ([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 "\<dots> = [q \<bullet> cs]set. (q \<bullet> x)" by simp
- also have "\<dots> = [p \<bullet> cs]set. (q \<bullet> x)" using * by simp
- finally have "[cs]set. x = [p \<bullet> cs]set. (q \<bullet> x)" .
- then show "\<exists>q. [cs]set. x = [p \<bullet> cs]set. (q \<bullet> x) \<and> q \<bullet> cs = p \<bullet> cs \<and> supp q \<subseteq> cs \<union> (p \<bullet> cs)"
- using * **
- by (blast)
-qed
-
lemma at_set_avoiding5:
assumes "finite xs"
and "finite (supp c)"
@@ -88,47 +64,36 @@
assumes a: "\<And>lrbs exp. \<lbrakk>bs lrbs \<sharp>* c; y = LetRec lrbs exp\<rbrakk> \<Longrightarrow> P"
shows "y = LetRec lrbs exp \<Longrightarrow> P"
apply -
-apply(subgoal_tac "\<exists>p. ((p \<bullet> (bs lrbs)) \<sharp>* (c, bs lrbs, lrbs, exp)) \<and> supp p = bs lrbs \<union> (p \<bullet> (bs lrbs))")
+apply(subgoal_tac "\<exists>p. ((p \<bullet> (bs lrbs)) \<sharp>* (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
--- 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"
--- 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 \<and>"} $ _ $ _ => (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 \<Longrightarrow> 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
*}
--- 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 \<bullet> bs) \<sharp>* (bs, x)"
and b: "finite bs"
- shows "\<exists>y. [bs]set. x = [p \<bullet> bs]set. y"
+ shows "\<exists>q. [bs]set. x = [p \<bullet> bs]set. (q \<bullet> x) \<and> q \<bullet> bs = p \<bullet> bs"
proof -
from a b have "p \<bullet> bs \<inter> 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 "\<dots> = [q \<bullet> bs]set. (q \<bullet> x)" by simp
- also have "\<dots> = [p \<bullet> bs]set. (q \<bullet> x)" using * by simp
- finally have "[bs]set. x = [p \<bullet> bs]set. (q \<bullet> x)" .
- then show "\<exists>y. [bs]set. x = [p \<bullet> bs]set. y" by blast
+ finally have "[bs]set. x = [p \<bullet> bs]set. (q \<bullet> x)" by (simp add: *)
+ then show "\<exists>q. [bs]set. x = [p \<bullet> bs]set. (q \<bullet> x) \<and> q \<bullet> bs = p \<bullet> bs" using * by metis
qed
lemma Abs_rename_res:
fixes x::"'a::fs"
assumes a: "(p \<bullet> bs) \<sharp>* (bs, x)"
and b: "finite bs"
- shows "\<exists>y. [bs]res. x = [p \<bullet> bs]res. y"
+ shows "\<exists>q. [bs]res. x = [p \<bullet> bs]res. (q \<bullet> x) \<and> q \<bullet> bs = p \<bullet> bs"
proof -
from a b have "p \<bullet> bs \<inter> 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 "\<dots> = [q \<bullet> bs]res. (q \<bullet> x)" by simp
- also have "\<dots> = [p \<bullet> bs]res. (q \<bullet> x)" using * by simp
- finally have "[bs]res. x = [p \<bullet> bs]res. (q \<bullet> x)" .
- then show "\<exists>y. [bs]res. x = [p \<bullet> bs]res. y" by blast
+ finally have "[bs]res. x = [p \<bullet> bs]res. (q \<bullet> x)" by (simp add: *)
+ then show "\<exists>q. [bs]res. x = [p \<bullet> bs]res. (q \<bullet> x) \<and> q \<bullet> bs = p \<bullet> bs" using * by metis
qed
lemma Abs_rename_lst:
fixes x::"'a::fs"
assumes a: "(p \<bullet> (set bs)) \<sharp>* (bs, x)"
- shows "\<exists>y. [bs]lst. x = [p \<bullet> bs]lst. y"
+ shows "\<exists>q. [bs]lst. x = [p \<bullet> bs]lst. (q \<bullet> x) \<and> q \<bullet> bs = p \<bullet> bs"
proof -
from a have "p \<bullet> (set bs) \<inter> (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 "\<dots> = [q \<bullet> bs]lst. (q \<bullet> x)" by simp
- also have "\<dots> = [p \<bullet> bs]lst. (q \<bullet> x)" using * by simp
- finally have "[bs]lst. x = [p \<bullet> bs]lst. (q \<bullet> x)" .
- then show "\<exists>y. [bs]lst. x = [p \<bullet> bs]lst. y" by blast
+ finally have "[bs]lst. x = [p \<bullet> bs]lst. (q \<bullet> x)" by (simp add: *)
+ then show "\<exists>q. [bs]lst. x = [p \<bullet> bs]lst. (q \<bullet> x) \<and> q \<bullet> bs = p \<bullet> bs" using * by metis
qed
+text {* for deep recursive binders *}
+
+lemma Abs_rename_set':
+ fixes x::"'a::fs"
+ assumes a: "(p \<bullet> bs) \<sharp>* (bs, x)"
+ and b: "finite bs"
+ shows "\<exists>q. [bs]set. x = [q \<bullet> bs]set. (q \<bullet> x) \<and> q \<bullet> bs = p \<bullet> bs"
+using Abs_rename_set[OF a b] by metis
+
+lemma Abs_rename_res':
+ fixes x::"'a::fs"
+ assumes a: "(p \<bullet> bs) \<sharp>* (bs, x)"
+ and b: "finite bs"
+ shows "\<exists>q. [bs]res. x = [q \<bullet> bs]res. (q \<bullet> x) \<and> q \<bullet> bs = p \<bullet> bs"
+using Abs_rename_res[OF a b] by metis
+
+lemma Abs_rename_lst':
+ fixes x::"'a::fs"
+ assumes a: "(p \<bullet> (set bs)) \<sharp>* (bs, x)"
+ shows "\<exists>q. [bs]lst. x = [q \<bullet> bs]lst. (q \<bullet> x) \<and> q \<bullet> bs = p \<bullet> bs"
+using Abs_rename_lst[OF a] by metis
section {* Infrastructure for building tuples of relations and functions *}
--- 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)
--- 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