--- a/Nominal/Ex/CoreHaskell.thy Tue Dec 07 14:27:21 2010 +0000
+++ b/Nominal/Ex/CoreHaskell.thy Tue Dec 07 14:27:39 2010 +0000
@@ -86,6 +86,7 @@
(* generated theorems *)
+thm core_haskell.permute_bn
thm core_haskell.perm_bn_alpha
thm core_haskell.perm_bn_simps
thm core_haskell.bn_finite
--- a/Nominal/Ex/Foo1.thy Tue Dec 07 14:27:21 2010 +0000
+++ b/Nominal/Ex/Foo1.thy Tue Dec 07 14:27:39 2010 +0000
@@ -35,6 +35,7 @@
| "bn4 (BNil) = {}"
| "bn4 (BAs a as) = {atom a} \<union> bn4 as"
+thm foo.permute_bn
thm foo.perm_bn_alpha
thm foo.perm_bn_simps
thm foo.bn_finite
@@ -55,43 +56,6 @@
thm foo.fresh
thm foo.bn_finite
-
-lemma tt1:
- shows "(p \<bullet> bn1 as) = bn1 (permute_bn1 p as)"
-apply(induct as rule: foo.inducts(2))
-apply(auto)[7]
-apply(simp add: foo.perm_bn_simps foo.bn_defs)
-apply(simp add: atom_eqvt)
-apply(auto)
-done
-
-lemma tt2:
- shows "(p \<bullet> bn2 as) = bn2 (permute_bn2 p as)"
-apply(induct as rule: foo.inducts(2))
-apply(auto)[7]
-apply(simp add: foo.perm_bn_simps foo.bn_defs)
-apply(simp add: atom_eqvt)
-apply(auto)
-done
-
-lemma tt3:
- shows "(p \<bullet> bn3 as) = bn3 (permute_bn3 p as)"
-apply(induct as rule: foo.inducts(2))
-apply(auto)[7]
-apply(simp add: foo.perm_bn_simps foo.bn_defs)
-apply(simp add: atom_eqvt)
-apply(auto)
-done
-
-lemma tt4:
- shows "(p \<bullet> bn4 as) = bn4 (permute_bn4 p as)"
-apply(induct as rule: foo.inducts(3))
-apply(auto)[8]
-apply(simp add: foo.perm_bn_simps foo.bn_defs permute_set_eq)
-apply(simp add: foo.perm_bn_simps foo.bn_defs)
-apply(simp add: atom_eqvt insert_eqvt)
-done
-
lemma strong_exhaust1:
fixes c::"'a::fs"
assumes "\<exists>name. y = Var name \<Longrightarrow> P"
--- a/Nominal/Ex/Foo2.thy Tue Dec 07 14:27:21 2010 +0000
+++ b/Nominal/Ex/Foo2.thy Tue Dec 07 14:27:39 2010 +0000
@@ -24,6 +24,8 @@
"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
thm foo.perm_bn_simps
thm foo.bn_finite
@@ -43,57 +45,61 @@
thm foo.supp
thm foo.fresh
-lemma tt1:
- shows "(p \<bullet> bn as) = bn (permute_bn p as)"
-apply(induct as rule: foo.inducts(2))
-apply(auto)[5]
-apply(simp only: foo.perm_bn_simps foo.bn_defs)
-apply(perm_simp)
-apply(simp only:)
-apply(simp only: foo.perm_bn_simps foo.bn_defs)
-apply(perm_simp add: foo.fv_bn_eqvt)
-apply(simp only:)
-done
-
text {*
tests by cu
*}
-lemma yy:
+lemma set_renaming_perm:
assumes a: "p \<bullet> bs \<inter> bs = {}"
and b: "finite bs"
shows "\<exists>q. q \<bullet> bs = p \<bullet> bs \<and> supp q \<subseteq> bs \<union> (p \<bullet> bs)"
using b a
-apply(induct)
-apply(simp add: permute_set_eq)
-apply(rule_tac x="0" in exI)
-apply(simp add: supp_perm)
-apply(perm_simp)
-apply(drule meta_mp)
-apply(auto simp add: fresh_star_def fresh_finite_insert)[1]
-apply(erule exE)
-apply(simp)
-apply(case_tac "q \<bullet> x = p \<bullet> x")
-apply(rule_tac x="q" in exI)
-apply(auto)[1]
-apply(rule_tac x="((q \<bullet> x) \<rightleftharpoons> (p \<bullet> x)) + q" in exI)
-apply(subgoal_tac "p \<bullet> x \<notin> p \<bullet> F")
-apply(subgoal_tac "q \<bullet> x \<notin> p \<bullet> F")
-apply(simp add: swap_set_not_in)
-apply(rule subset_trans)
-apply(rule supp_plus_perm)
-apply(simp)
-apply(rule conjI)
-apply(simp add: supp_swap)
-apply(simp add: supp_perm)
-apply(auto)[1]
-apply(auto)[1]
-apply(erule conjE)+
-apply(drule sym)
-apply(simp add: mem_permute_iff)
-apply(simp add: mem_permute_iff)
-done
-
+proof (induct)
+ case empty
+ have "0 \<bullet> {} = p \<bullet> {} \<and> supp (0::perm) \<subseteq> {} \<union> p \<bullet> {}"
+ by (simp add: permute_set_eq supp_perm)
+ then show "\<exists>q. q \<bullet> {} = p \<bullet> {} \<and> supp q \<subseteq> {} \<union> p \<bullet> {}" by blast
+next
+ case (insert a bs)
+ then have " \<exists>q. q \<bullet> bs = p \<bullet> bs \<and> supp q \<subseteq> bs \<union> p \<bullet> bs"
+ by (perm_simp) (auto)
+ then obtain q where *: "q \<bullet> bs = p \<bullet> bs" and **: "supp q \<subseteq> bs \<union> p \<bullet> bs" by blast
+ { assume 1: "q \<bullet> a = p \<bullet> a"
+ have "q \<bullet> insert a bs = p \<bullet> insert a bs" using 1 * by (simp add: insert_eqvt)
+ moreover
+ have "supp q \<subseteq> insert a bs \<union> p \<bullet> insert a bs"
+ using ** by (auto simp add: insert_eqvt)
+ ultimately
+ have "\<exists>q. q \<bullet> insert a bs = p \<bullet> insert a bs \<and> supp q \<subseteq> insert a bs \<union> p \<bullet> insert a bs" by blast
+ }
+ moreover
+ { assume 2: "q \<bullet> a \<noteq> p \<bullet> a"
+ def q' \<equiv> "((q \<bullet> a) \<rightleftharpoons> (p \<bullet> a)) + q"
+ { have "(q \<bullet> a) \<notin> (p \<bullet> bs)" using `a \<notin> bs` *[symmetric] by (simp add: mem_permute_iff)
+ moreover
+ have "(p \<bullet> a) \<notin> (p \<bullet> bs)" using `a \<notin> bs` by (simp add: mem_permute_iff)
+ ultimately
+ have "q' \<bullet> insert a bs = p \<bullet> insert a bs" using 2 * unfolding q'_def
+ by (simp add: insert_eqvt swap_set_not_in)
+ }
+ moreover
+ { have "{q \<bullet> a, p \<bullet> a} \<subseteq> insert a bs \<union> p \<bullet> insert a bs"
+ using ** `a \<notin> bs` `p \<bullet> insert a bs \<inter> insert a bs = {}`
+ by (auto simp add: supp_perm insert_eqvt)
+ then have "supp (q \<bullet> a \<rightleftharpoons> p \<bullet> a) \<subseteq> insert a bs \<union> p \<bullet> insert a bs" by (simp add: supp_swap)
+ moreover
+ have "supp q \<subseteq> insert a bs \<union> p \<bullet> insert a bs"
+ using ** by (auto simp add: insert_eqvt)
+ ultimately
+ have "supp q' \<subseteq> insert a bs \<union> p \<bullet> insert a bs"
+ unfolding q'_def using supp_plus_perm by blast
+ }
+ ultimately
+ have "\<exists>q. q \<bullet> insert a bs = p \<bullet> insert a bs \<and> supp q \<subseteq> insert a bs \<union> p \<bullet> insert a bs" by blast
+ }
+ ultimately show "\<exists>q. q \<bullet> insert a bs = p \<bullet> insert a bs \<and> supp q \<subseteq> insert a bs \<union> p \<bullet> insert a bs"
+ by blast
+qed
lemma Abs_rename_set:
@@ -103,7 +109,8 @@
shows "\<exists>y. [bs]set. x = [p \<bullet> bs]set. y"
proof -
from a b have "p \<bullet> bs \<inter> bs = {}" using at_fresh_star_inter by (auto simp add: fresh_star_Pair)
- with yy obtain q where *: "q \<bullet> bs = p \<bullet> bs" and **: "supp q \<subseteq> bs \<union> (p \<bullet> bs)" using b by metis
+ with set_renaming_perm
+ obtain q where *: "q \<bullet> bs = p \<bullet> bs" and **: "supp q \<subseteq> bs \<union> (p \<bullet> bs)" using b by metis
have "[bs]set. x = q \<bullet> ([bs]set. x)"
apply(rule perm_supp_eq[symmetric])
using a **
@@ -124,7 +131,8 @@
shows "\<exists>y. [bs]res. x = [p \<bullet> bs]res. y"
proof -
from a b have "p \<bullet> bs \<inter> bs = {}" using at_fresh_star_inter by (simp add: fresh_star_Pair)
- with yy obtain q where *: "q \<bullet> bs = p \<bullet> bs" and **: "supp q \<subseteq> bs \<union> (p \<bullet> bs)" using b by metis
+ with set_renaming_perm
+ obtain q where *: "q \<bullet> bs = p \<bullet> bs" and **: "supp q \<subseteq> bs \<union> (p \<bullet> bs)" using b by metis
have "[bs]res. x = q \<bullet> ([bs]res. x)"
apply(rule perm_supp_eq[symmetric])
using a **
@@ -138,54 +146,60 @@
then show "\<exists>y. [bs]res. x = [p \<bullet> bs]res. y" by blast
qed
-lemma zz0:
- assumes "p \<bullet> bs = q \<bullet> bs"
- and a: "a \<in> set bs"
- shows "p \<bullet> a = q \<bullet> a"
-using assms
-by (induct bs) (auto)
-
-lemma zz:
+lemma list_renaming_perm:
fixes bs::"atom list"
- assumes "(p \<bullet> (set bs)) \<inter> (set bs) = {}"
+ assumes a: "(p \<bullet> (set bs)) \<inter> (set bs) = {}"
shows "\<exists>q. q \<bullet> bs = p \<bullet> bs \<and> supp q \<subseteq> (set bs) \<union> (p \<bullet> (set bs))"
-using assms
-apply(induct bs)
-apply(simp add: permute_set_eq)
-apply(rule_tac x="0" in exI)
-apply(simp add: supp_perm)
-apply(drule meta_mp)
-apply(perm_simp)
-apply(auto)[1]
-apply(erule exE)
-apply(simp)
-apply(case_tac "a \<in> set bs")
-apply(rule_tac x="q" in exI)
-apply(perm_simp)
-apply(auto dest: zz0)[1]
-apply(subgoal_tac "q \<bullet> a \<sharp> p \<bullet> bs")
-apply(subgoal_tac "p \<bullet> a \<sharp> p \<bullet> bs")
-apply(rule_tac x="((q \<bullet> a) \<rightleftharpoons> (p \<bullet> a)) + q" in exI)
-apply(simp add: swap_fresh_fresh)
-apply(rule subset_trans)
-apply(rule supp_plus_perm)
-apply(simp)
-apply(rule conjI)
-apply(simp add: supp_swap)
-apply(simp add: supp_perm)
-apply(perm_simp)
-apply(auto simp add: fresh_def supp_of_atom_list)[1]
-apply(perm_simp)
-apply(auto)[1]
-apply(simp add: fresh_permute_iff)
-apply(simp add: fresh_def supp_of_atom_list)
-apply(erule conjE)+
-apply(drule sym)
-apply(drule sym)
-apply(simp)
-apply(simp add: fresh_permute_iff)
-apply(auto simp add: fresh_def supp_of_atom_list)[1]
-done
+using a
+proof (induct bs)
+ case Nil
+ have "0 \<bullet> [] = p \<bullet> [] \<and> supp (0::perm) \<subseteq> set [] \<union> p \<bullet> set []"
+ by (simp add: permute_set_eq supp_perm)
+ then show "\<exists>q. q \<bullet> [] = p \<bullet> [] \<and> supp q \<subseteq> set [] \<union> p \<bullet> (set [])" by blast
+next
+ case (Cons a bs)
+ then have " \<exists>q. q \<bullet> bs = p \<bullet> bs \<and> supp q \<subseteq> set bs \<union> p \<bullet> (set bs)"
+ by (perm_simp) (auto)
+ then obtain q where *: "q \<bullet> bs = p \<bullet> bs" and **: "supp q \<subseteq> set bs \<union> p \<bullet> (set bs)" by blast
+ { assume 1: "a \<in> set bs"
+ have "q \<bullet> a = p \<bullet> a" using * 1 by (induct bs) (auto)
+ then have "q \<bullet> (a # bs) = p \<bullet> (a # bs)" using * by simp
+ moreover
+ have "supp q \<subseteq> set (a # bs) \<union> p \<bullet> (set (a # bs))" using ** by (auto simp add: insert_eqvt)
+ ultimately
+ have "\<exists>q. q \<bullet> (a # bs) = p \<bullet> (a # bs) \<and> supp q \<subseteq> set (a # bs) \<union> p \<bullet> (set (a # bs))" by blast
+ }
+ moreover
+ { assume 2: "a \<notin> set bs"
+ def q' \<equiv> "((q \<bullet> a) \<rightleftharpoons> (p \<bullet> a)) + q"
+ { have "(q \<bullet> a) \<sharp> (p \<bullet> bs)" using `a \<notin> set bs` *[symmetric]
+ by (simp add: fresh_permute_iff) (simp add: fresh_def supp_of_atom_list)
+ moreover
+ have "(p \<bullet> a) \<sharp> (p \<bullet> bs)" using `a \<notin> set bs`
+ by (simp add: fresh_permute_iff) (simp add: fresh_def supp_of_atom_list)
+ ultimately
+ have "q' \<bullet> (a # bs) = p \<bullet> (a # bs)" using 2 * unfolding q'_def
+ by (simp add: swap_fresh_fresh)
+ }
+ moreover
+ { have "{q \<bullet> a, p \<bullet> a} \<subseteq> set (a # bs) \<union> p \<bullet> (set (a # bs))"
+ using ** `a \<notin> set bs` `p \<bullet> (set (a # bs)) \<inter> set (a # bs) = {}`
+ by (auto simp add: supp_perm insert_eqvt)
+ then have "supp (q \<bullet> a \<rightleftharpoons> p \<bullet> a) \<subseteq> set (a # bs) \<union> p \<bullet> set (a # bs)" by (simp add: supp_swap)
+ moreover
+ have "supp q \<subseteq> set (a # bs) \<union> p \<bullet> (set (a # bs))"
+ using ** by (auto simp add: insert_eqvt)
+ ultimately
+ have "supp q' \<subseteq> set (a # bs) \<union> p \<bullet> (set (a # bs))"
+ unfolding q'_def using supp_plus_perm by blast
+ }
+ ultimately
+ have "\<exists>q. q \<bullet> (a # bs) = p \<bullet> (a # bs) \<and> supp q \<subseteq> set (a # bs) \<union> p \<bullet> (set (a # bs))" by blast
+ }
+ ultimately show "\<exists>q. q \<bullet> (a # bs) = p \<bullet> (a # bs) \<and> supp q \<subseteq> set (a # bs) \<union> p \<bullet> (set (a # bs))"
+ by blast
+qed
+
lemma Abs_rename_list:
fixes x::"'a::fs"
@@ -194,7 +208,8 @@
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 zz obtain q where *: "q \<bullet> bs = p \<bullet> bs" and **: "supp q \<subseteq> set bs \<union> (p \<bullet> set bs)" by metis
+ 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 **
@@ -208,6 +223,23 @@
then show "\<exists>y. [bs]lst. x = [p \<bullet> bs]lst. y" by blast
qed
+(*
+thm at_set_avoiding1[THEN exE]
+
+
+lemma Let1_rename:
+ fixes c::"'a::fs"
+ shows "\<exists>name' trm'. {atom name'} \<sharp>* c \<and> 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
+*)
lemma test6:
fixes c::"'a::fs"
@@ -224,6 +256,14 @@
apply(rule assms(2))
apply(rule exI)+
apply(assumption)
+(* lam case *)
+(*
+apply(rule Let1_rename)
+apply(rule assms(3))
+apply(assumption)
+apply(simp)
+*)
+
apply(subgoal_tac "\<exists>p. (p \<bullet> {atom name}) \<sharp>* (c, [atom name], trm)")
apply(erule exE)
apply(insert Abs_rename_list)[1]
@@ -245,10 +285,10 @@
apply(rule at_set_avoiding1)
apply(simp)
apply(simp add: finite_supp)
+(* 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(simp only:)
apply(simp only: foo.eq_iff)
apply(insert Abs_rename_list)[1]
apply(drule_tac x="p" in meta_spec)
@@ -264,7 +304,7 @@
apply(simp only: union_eqvt fresh_star_Pair set.simps fresh_star_Un, simp)
apply(erule exE)+
apply(rule exI)+
-apply(perm_simp add: tt1)
+apply(perm_simp add: foo.permute_bn)
apply(rule conjI)
apply(simp add: fresh_star_Pair fresh_star_Un)
apply(erule conjE)+
@@ -282,6 +322,7 @@
apply(rule at_set_avoiding1)
apply(simp)
apply(simp add: finite_supp)
+(* let2 case *)
apply(subgoal_tac "\<exists>p. (p \<bullet> ({atom name1} \<union> {atom name2})) \<sharp>* (c, atom name1, atom name2, trm1, trm2)")
apply(erule exE)
apply(rule assms(5))
@@ -309,7 +350,7 @@
apply(auto simp add: fresh_star_def fresh_Pair fresh_Nil fresh_Cons)[1]
apply(erule exE)+
apply(rule exI)+
-apply(perm_simp add: tt1)
+apply(perm_simp add: foo.permute_bn)
apply(rule conjI)
prefer 2
apply(rule conjI)
--- a/Nominal/Ex/Multi_Recs2.thy Tue Dec 07 14:27:21 2010 +0000
+++ b/Nominal/Ex/Multi_Recs2.thy Tue Dec 07 14:27:39 2010 +0000
@@ -50,7 +50,7 @@
| "b_fnclause (K x pat exp) = {atom x}"
-
+thm fun_recs.permute_bn
thm fun_recs.perm_bn_alpha
thm fun_recs.perm_bn_simps
thm fun_recs.bn_finite
--- a/Nominal/Nominal2.thy Tue Dec 07 14:27:21 2010 +0000
+++ b/Nominal/Nominal2.thy Tue Dec 07 14:27:39 2010 +0000
@@ -1,15 +1,11 @@
theory Nominal2
imports
Nominal2_Base Nominal2_Eqvt Nominal2_Abs
-uses ("nominal_dt_rawperm.ML")
- ("nominal_dt_rawfuns.ML")
+uses ("nominal_dt_rawfuns.ML")
("nominal_dt_alpha.ML")
("nominal_dt_quot.ML")
begin
-use "nominal_dt_rawperm.ML"
-ML {* open Nominal_Dt_RawPerm *}
-
use "nominal_dt_rawfuns.ML"
ML {* open Nominal_Dt_RawFuns *}
@@ -614,6 +610,12 @@
qalpha_refl_thms lthyC
else []
+ (* proving the relationship of bn and permute_bn *)
+ val qpermute_bn_thms =
+ if get_STEPS lthy > 33
+ then prove_permute_bn_thms qtys qbns qperm_bns qinduct qperm_bn_simps qbn_defs qfv_qbn_eqvts lthyC
+ else []
+
(* noting the theorems *)
(* generating the prefix for the theorem names *)
@@ -641,6 +643,7 @@
||>> Local_Theory.note ((thms_suffix "perm_bn_simps", []), qperm_bn_simps)
||>> Local_Theory.note ((thms_suffix "bn_finite", []), qbn_finite_thms)
||>> Local_Theory.note ((thms_suffix "perm_bn_alpha", []), qperm_bn_alpha_thms)
+ ||>> Local_Theory.note ((thms_suffix "permute_bn", []), qpermute_bn_thms)
in
(0, lthy9')
end handle TEST ctxt => (0, ctxt)
--- a/Nominal/nominal_dt_quot.ML Tue Dec 07 14:27:21 2010 +0000
+++ b/Nominal/nominal_dt_quot.ML Tue Dec 07 14:27:39 2010 +0000
@@ -35,7 +35,9 @@
val prove_perm_bn_alpha_thms: typ list -> term list -> term list -> thm -> thm list -> thm list ->
thm list -> Proof.context -> thm list
-
+
+ val prove_permute_bn_thms: typ list -> term list -> term list -> thm -> thm list -> thm list ->
+ thm list -> Proof.context -> thm list
end
structure Nominal_Dt_Quot: NOMINAL_DT_QUOT =
@@ -323,6 +325,7 @@
induct_prove qtys props qinduct (K ss_tac) ctxt
end
+
fun prove_perm_bn_alpha_thms qtys qperm_bns alpha_bns qinduct qperm_bn_simps qeq_iffs qalpha_refls ctxt =
let
val ([p], ctxt') = Variable.variant_fixes ["p"] ctxt
@@ -344,7 +347,31 @@
|> map (simplify (HOL_basic_ss addsimps @{thms id_def}))
end
+fun prove_permute_bn_thms qtys qbns qperm_bns qinduct qperm_bn_simps qbn_defs qbn_eqvts ctxt =
+ let
+ val ([p], ctxt') = Variable.variant_fixes ["p"] ctxt
+ val p = Free (p, @{typ perm})
+ fun mk_goal qbn qperm_bn =
+ let
+ val arg_ty = domain_type (fastype_of qbn)
+ in
+ (arg_ty, fn x =>
+ (mk_id (Abs ("", arg_ty,
+ HOLogic.mk_eq (mk_perm p (qbn $ Bound 0), qbn $ (qperm_bn $ p $ Bound 0)))) $ x))
+ end
+
+ val props = map2 mk_goal qbns qperm_bns
+ val ss = @{thm id_def}::qperm_bn_simps @ qbn_defs
+ val ss_tac =
+ EVERY' [asm_full_simp_tac (HOL_basic_ss addsimps ss),
+ TRY o Nominal_Permeq.eqvt_strict_tac ctxt' qbn_eqvts [],
+ TRY o asm_full_simp_tac HOL_basic_ss]
+ in
+ induct_prove qtys props qinduct (K ss_tac) ctxt'
+ |> ProofContext.export ctxt' ctxt
+ |> map (simplify (HOL_basic_ss addsimps @{thms id_def}))
+ end
end (* structure *)
--- a/Nominal/nominal_dt_rawfuns.ML Tue Dec 07 14:27:21 2010 +0000
+++ b/Nominal/nominal_dt_rawfuns.ML Tue Dec 07 14:27:39 2010 +0000
@@ -2,7 +2,7 @@
Author: Cezary Kaliszyk
Author: Christian Urban
- Definitions of the raw fv and fv_bn functions
+ Definitions of the raw fv, fv_bn and permute functions.
*)
signature NOMINAL_DT_RAWFUNS =
@@ -41,6 +41,9 @@
local_theory -> (term list * thm list * local_theory)
val raw_prove_eqvt: term list -> thm list -> thm list -> Proof.context -> thm list
+
+ val define_raw_perms: string list -> typ list -> (string * sort) list -> term list -> thm ->
+ local_theory -> (term list * thm list * thm list) * local_theory
end
@@ -368,6 +371,7 @@
HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs))
end
+
fun raw_prove_eqvt consts ind_thms simps ctxt =
if null consts then []
else
@@ -390,5 +394,117 @@
|> ProofContext.export ctxt'' ctxt
end
+
+
+(*** raw permutation functions ***)
+
+(** proves the two pt-type class properties **)
+
+fun prove_permute_zero induct perm_defs perm_fns lthy =
+ let
+ val perm_types = map (body_type o fastype_of) perm_fns
+ val perm_indnames = Datatype_Prop.make_tnames perm_types
+
+ fun single_goal ((perm_fn, T), x) =
+ HOLogic.mk_eq (perm_fn $ @{term "0::perm"} $ Free (x, T), Free (x, T))
+
+ val goals =
+ HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj
+ (map single_goal (perm_fns ~~ perm_types ~~ perm_indnames)))
+
+ val simps = HOL_basic_ss addsimps (@{thm permute_zero} :: perm_defs)
+
+ val tac = (Datatype_Aux.indtac induct perm_indnames
+ THEN_ALL_NEW asm_simp_tac simps) 1
+ in
+ Goal.prove lthy perm_indnames [] goals (K tac)
+ |> Datatype_Aux.split_conj_thm
+ end
+
+
+fun prove_permute_plus induct perm_defs perm_fns lthy =
+ let
+ val p = Free ("p", @{typ perm})
+ val q = Free ("q", @{typ perm})
+ val perm_types = map (body_type o fastype_of) perm_fns
+ val perm_indnames = Datatype_Prop.make_tnames perm_types
+
+ fun single_goal ((perm_fn, T), x) = HOLogic.mk_eq
+ (perm_fn $ (mk_plus p q) $ Free (x, T), perm_fn $ p $ (perm_fn $ q $ Free (x, T)))
+
+ val goals =
+ HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj
+ (map single_goal (perm_fns ~~ perm_types ~~ perm_indnames)))
+
+ val simps = HOL_basic_ss addsimps (@{thm permute_plus} :: perm_defs)
+
+ val tac = (Datatype_Aux.indtac induct perm_indnames
+ THEN_ALL_NEW asm_simp_tac simps) 1
+ in
+ Goal.prove lthy ("p" :: "q" :: perm_indnames) [] goals (K tac)
+ |> Datatype_Aux.split_conj_thm
+ end
+
+
+fun mk_perm_eq ty_perm_assoc cnstr =
+ let
+ fun lookup_perm p (ty, arg) =
+ case (AList.lookup (op=) ty_perm_assoc ty) of
+ SOME perm => perm $ p $ arg
+ | NONE => Const (@{const_name permute}, perm_ty ty) $ p $ arg
+
+ val p = Free ("p", @{typ perm})
+ val (arg_tys, ty) =
+ fastype_of cnstr
+ |> strip_type
+
+ val arg_names = Name.variant_list ["p"] (Datatype_Prop.make_tnames arg_tys)
+ val args = map Free (arg_names ~~ arg_tys)
+
+ val lhs = lookup_perm p (ty, list_comb (cnstr, args))
+ val rhs = list_comb (cnstr, map (lookup_perm p) (arg_tys ~~ args))
+
+ val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs))
+ in
+ (Attrib.empty_binding, eq)
+ end
+
+
+fun define_raw_perms full_ty_names tys tvs constrs induct_thm lthy =
+ let
+ val perm_fn_names = full_ty_names
+ |> map Long_Name.base_name
+ |> map (prefix "permute_")
+
+ val perm_fn_types = map perm_ty tys
+ val perm_fn_frees = map Free (perm_fn_names ~~ perm_fn_types)
+ val perm_fn_binds = map (fn s => (Binding.name s, NONE, NoSyn)) perm_fn_names
+
+ val perm_eqs = map (mk_perm_eq (tys ~~ perm_fn_frees)) constrs
+
+ fun tac _ (_, _, simps) =
+ Class.intro_classes_tac [] THEN ALLGOALS (resolve_tac simps)
+
+ fun morphism phi (fvs, dfs, simps) =
+ (map (Morphism.term phi) fvs,
+ map (Morphism.thm phi) dfs,
+ map (Morphism.thm phi) simps);
+
+ val ((perm_funs, perm_eq_thms), lthy') =
+ lthy
+ |> Local_Theory.exit_global
+ |> Class.instantiation (full_ty_names, tvs, @{sort pt})
+ |> Primrec.add_primrec perm_fn_binds perm_eqs
+
+ val perm_zero_thms = prove_permute_zero induct_thm perm_eq_thms perm_funs lthy'
+ val perm_plus_thms = prove_permute_plus induct_thm perm_eq_thms perm_funs lthy'
+ in
+ lthy'
+ |> Class.prove_instantiation_exit_result morphism tac
+ (perm_funs, perm_eq_thms, perm_zero_thms @ perm_plus_thms)
+ ||> Named_Target.theory_init
+ end
+
+
end (* structure *)
--- a/Nominal/nominal_dt_rawperm.ML Tue Dec 07 14:27:21 2010 +0000
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,130 +0,0 @@
-(* Title: nominal_dt_rawperm.ML
- Author: Cezary Kaliszyk
- Author: Christian Urban
-
- Definitions of the raw permutations and
- proof that the raw datatypes are in the
- pt-class.
-*)
-
-signature NOMINAL_DT_RAWPERM =
-sig
- val define_raw_perms: string list -> typ list -> (string * sort) list -> term list -> thm ->
- local_theory -> (term list * thm list * thm list) * local_theory
-end
-
-
-structure Nominal_Dt_RawPerm: NOMINAL_DT_RAWPERM =
-struct
-
-
-(** proves the two pt-type class properties **)
-
-fun prove_permute_zero induct perm_defs perm_fns lthy =
- let
- val perm_types = map (body_type o fastype_of) perm_fns
- val perm_indnames = Datatype_Prop.make_tnames perm_types
-
- fun single_goal ((perm_fn, T), x) =
- HOLogic.mk_eq (perm_fn $ @{term "0::perm"} $ Free (x, T), Free (x, T))
-
- val goals =
- HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj
- (map single_goal (perm_fns ~~ perm_types ~~ perm_indnames)))
-
- val simps = HOL_basic_ss addsimps (@{thm permute_zero} :: perm_defs)
-
- val tac = (Datatype_Aux.indtac induct perm_indnames
- THEN_ALL_NEW asm_simp_tac simps) 1
- in
- Goal.prove lthy perm_indnames [] goals (K tac)
- |> Datatype_Aux.split_conj_thm
- end
-
-
-fun prove_permute_plus induct perm_defs perm_fns lthy =
- let
- val p = Free ("p", @{typ perm})
- val q = Free ("q", @{typ perm})
- val perm_types = map (body_type o fastype_of) perm_fns
- val perm_indnames = Datatype_Prop.make_tnames perm_types
-
- fun single_goal ((perm_fn, T), x) = HOLogic.mk_eq
- (perm_fn $ (mk_plus p q) $ Free (x, T), perm_fn $ p $ (perm_fn $ q $ Free (x, T)))
-
- val goals =
- HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj
- (map single_goal (perm_fns ~~ perm_types ~~ perm_indnames)))
-
- val simps = HOL_basic_ss addsimps (@{thm permute_plus} :: perm_defs)
-
- val tac = (Datatype_Aux.indtac induct perm_indnames
- THEN_ALL_NEW asm_simp_tac simps) 1
- in
- Goal.prove lthy ("p" :: "q" :: perm_indnames) [] goals (K tac)
- |> Datatype_Aux.split_conj_thm
- end
-
-
-fun mk_perm_eq ty_perm_assoc cnstr =
- let
- fun lookup_perm p (ty, arg) =
- case (AList.lookup (op=) ty_perm_assoc ty) of
- SOME perm => perm $ p $ arg
- | NONE => Const (@{const_name permute}, perm_ty ty) $ p $ arg
-
- val p = Free ("p", @{typ perm})
- val (arg_tys, ty) =
- fastype_of cnstr
- |> strip_type
-
- val arg_names = Name.variant_list ["p"] (Datatype_Prop.make_tnames arg_tys)
- val args = map Free (arg_names ~~ arg_tys)
-
- val lhs = lookup_perm p (ty, list_comb (cnstr, args))
- val rhs = list_comb (cnstr, map (lookup_perm p) (arg_tys ~~ args))
-
- val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs))
- in
- (Attrib.empty_binding, eq)
- end
-
-
-fun define_raw_perms full_ty_names tys tvs constrs induct_thm lthy =
- let
- val perm_fn_names = full_ty_names
- |> map Long_Name.base_name
- |> map (prefix "permute_")
-
- val perm_fn_types = map perm_ty tys
- val perm_fn_frees = map Free (perm_fn_names ~~ perm_fn_types)
- val perm_fn_binds = map (fn s => (Binding.name s, NONE, NoSyn)) perm_fn_names
-
- val perm_eqs = map (mk_perm_eq (tys ~~ perm_fn_frees)) constrs
-
- fun tac _ (_, _, simps) =
- Class.intro_classes_tac [] THEN ALLGOALS (resolve_tac simps)
-
- fun morphism phi (fvs, dfs, simps) =
- (map (Morphism.term phi) fvs,
- map (Morphism.thm phi) dfs,
- map (Morphism.thm phi) simps);
-
- val ((perm_funs, perm_eq_thms), lthy') =
- lthy
- |> Local_Theory.exit_global
- |> Class.instantiation (full_ty_names, tvs, @{sort pt})
- |> Primrec.add_primrec perm_fn_binds perm_eqs
-
- val perm_zero_thms = prove_permute_zero induct_thm perm_eq_thms perm_funs lthy'
- val perm_plus_thms = prove_permute_plus induct_thm perm_eq_thms perm_funs lthy'
- in
- lthy'
- |> Class.prove_instantiation_exit_result morphism tac
- (perm_funs, perm_eq_thms, perm_zero_thms @ perm_plus_thms)
- ||> Named_Target.theory_init
- end
-
-
-end (* structure *)
-