--- a/Nominal-General/Nominal2_Supp.thy Thu Jul 29 10:16:33 2010 +0100
+++ b/Nominal-General/Nominal2_Supp.thy Fri Jul 30 00:40:32 2010 +0100
@@ -58,12 +58,18 @@
shows "(a \<sharp>* (x, y) \<Longrightarrow> PROP C) \<equiv> (a \<sharp>* x \<Longrightarrow> a \<sharp>* y \<Longrightarrow> PROP C)"
by (rule, simp_all add: fresh_star_prod)
+lemma fresh_star_zero:
+ shows "as \<sharp>* (0::perm)"
+ unfolding fresh_star_def
+ by (simp add: fresh_zero_perm)
+
lemma fresh_star_plus:
fixes p q::perm
shows "\<lbrakk>a \<sharp>* p; a \<sharp>* q\<rbrakk> \<Longrightarrow> a \<sharp>* (p + q)"
unfolding fresh_star_def
by (simp add: fresh_plus_perm)
+
lemma fresh_star_permute_iff:
shows "(p \<bullet> a) \<sharp>* (p \<bullet> x) \<longleftrightarrow> a \<sharp>* x"
unfolding fresh_star_def
--- a/Nominal/Ex/SingleLet.thy Thu Jul 29 10:16:33 2010 +0100
+++ b/Nominal/Ex/SingleLet.thy Fri Jul 30 00:40:32 2010 +0100
@@ -4,7 +4,7 @@
atom_decl name
-declare [[STEPS = 16]]
+declare [[STEPS = 17]]
nominal_datatype trm =
Var "name"
@@ -21,6 +21,7 @@
where
"bn (As x y t) = {atom x}"
+thm size_eqvt
thm alpha_bn_imps
thm distinct
thm eq_iff
@@ -28,6 +29,7 @@
thm fv_defs
thm perm_simps
thm perm_laws
+thm funs_rsp
typ trm
@@ -40,61 +42,31 @@
term alpha_bn
-lemma a2:
- shows "alpha_trm_raw x1 y1 \<Longrightarrow> fv_trm_raw x1 = fv_trm_raw y1"
- and "alpha_assg_raw x2 y2 \<Longrightarrow> fv_assg_raw x2 = fv_assg_raw y2 \<and> bn_raw x2 = bn_raw y2"
- and "alpha_bn_raw x3 y3 \<Longrightarrow> fv_bn_raw x3 = fv_bn_raw y3"
-apply(induct rule: alpha_trm_raw_alpha_assg_raw_alpha_bn_raw.inducts)
-apply(simp_all only: fv_trm_raw.simps fv_assg_raw.simps fv_bn_raw.simps bn_raw.simps
- alphas prod_fv.simps prod_alpha_def ex_simps Un_assoc set.simps append.simps Un_insert_left Un_empty_right Un_empty_left simp_thms)
-done
+lemma exi_zero: "P 0 \<Longrightarrow> \<exists>(x::perm). P x" by auto
+
+ML {*
+ val pre_ss = @{thms fun_rel_def}
+ val post_ss = @{thms alphas prod_alpha_def prod_rel.simps
+ prod_fv.simps fresh_star_zero permute_zero funs_rsp prod.cases alpha_bn_imps}
+
+ val tac =
+ asm_full_simp_tac (HOL_ss addsimps pre_ss)
+ THEN' REPEAT o (resolve_tac @{thms allI impI})
+ THEN' resolve_tac @{thms alpha_trm_raw_alpha_assg_raw_alpha_bn_raw.intros}
+ THEN_ALL_NEW (TRY o (rtac @{thm exi_zero}) THEN' asm_full_simp_tac (HOL_ss addsimps post_ss))
+*}
lemma [quot_respect]:
"(op= ===> alpha_trm_raw) Var_raw Var_raw"
"(alpha_trm_raw ===> alpha_trm_raw ===> alpha_trm_raw) App_raw App_raw"
"(op= ===> alpha_trm_raw ===> alpha_trm_raw) Lam_raw Lam_raw"
"(alpha_assg_raw ===> alpha_trm_raw ===> alpha_trm_raw) Let_raw Let_raw"
- "(op= ===> op= ===> alpha_trm_raw ===> alpha_trm_raw ===> alpha_trm_raw ===> alpha_trm_raw)
+ "(op= ===> op= ===> alpha_trm_raw ===> alpha_trm_raw ===> alpha_trm_raw ===> alpha_trm_raw)
Foo_raw Foo_raw"
"(op= ===> op= ===> alpha_trm_raw ===> alpha_trm_raw) Bar_raw Bar_raw"
"(op= ===> alpha_trm_raw ===> alpha_trm_raw ===> alpha_trm_raw) Baz_raw Baz_raw"
"(op = ===> op = ===> alpha_trm_raw ===> alpha_assg_raw) As_raw As_raw"
-apply(simp only: fun_rel_def)
-apply(simp only: eq_iff)
-apply(simp only: simp_thms)
-apply(simp only: fun_rel_def)
-apply(simp only: eq_iff)
-apply(tactic {* asm_full_simp_tac HOL_ss 1*})
-apply(simp only: fun_rel_def)
-apply(simp only: eq_iff alphas fresh_star_def fresh_zero_perm a2)
-apply(rule allI | rule impI)+
-apply(rule_tac x="0" in exI)
-apply(simp only: eq_iff alphas fresh_star_def fresh_zero_perm a2 permute_zero a2)
-apply(simp add: a2)
-apply(simp add: alphas fresh_star_def fresh_zero_perm a2 alpha_bn_imps)
-apply(simp only: fun_rel_def)
-apply(rule allI | rule impI)+
-apply(rule alpha_trm_raw_alpha_assg_raw_alpha_bn_raw.intros)
-apply(rule_tac x="0" in exI)
-apply(simp add: alphas fresh_star_def fresh_zero_perm a2 prod_alpha_def)
-apply(simp only: fun_rel_def)
-apply(rule allI | rule impI)+
-apply(rule alpha_trm_raw_alpha_assg_raw_alpha_bn_raw.intros)
-apply(rule_tac x="0" in exI)
-apply(simp add: alphas fresh_star_def fresh_zero_perm a2 prod_alpha_def)
-apply(simp only: fun_rel_def)
-apply(rule allI | rule impI)+
-apply(rule alpha_trm_raw_alpha_assg_raw_alpha_bn_raw.intros)
-apply(rule_tac x="0" in exI)
-apply(simp add: alphas fresh_star_def fresh_zero_perm a2 prod_alpha_def)
-apply(rule_tac x="0" in exI)
-apply(simp add: alphas fresh_star_def fresh_zero_perm a2 prod_alpha_def)
-apply(simp only: fun_rel_def)
-apply(rule allI | rule impI)+
-apply(rule alpha_trm_raw_alpha_assg_raw_alpha_bn_raw.intros)
-apply(rule_tac x="0" in exI)
-apply(simp add: alphas fresh_star_def fresh_zero_perm a2 prod_alpha_def)
-apply(assumption)
+apply(tactic {* ALLGOALS tac *})
done
lemma [quot_respect]:
@@ -103,7 +75,7 @@
"(alpha_assg_raw ===> op =) bn_raw bn_raw"
"(alpha_assg_raw ===> op =) fv_assg_raw fv_assg_raw"
"(op = ===> alpha_trm_raw ===> alpha_trm_raw) permute permute"
-apply(simp_all add: a2 a1)
+apply(simp_all add: alpha_bn_imps funs_rsp)
sorry
ML {*
--- a/Nominal/NewParser.thy Thu Jul 29 10:16:33 2010 +0100
+++ b/Nominal/NewParser.thy Fri Jul 30 00:40:32 2010 +0100
@@ -305,24 +305,31 @@
val dtinfo = Datatype.the_info (ProofContext.theory_of lthy0) (hd raw_dt_names)
val {descr, sorts, ...} = dtinfo
- val all_raw_tys = map (fn (_, (n, _, _)) => n) descr
+ val all_raw_tys = all_dtyps descr sorts
+ val all_raw_ty_names = map (fn (_, (n, _, _)) => n) descr
val all_raw_constrs =
flat (map (map (fn (c, _, _, _) => c)) (all_dtyp_constrs_types descr sorts))
- val dtinfos = map (Datatype.the_info (ProofContext.theory_of lthy0)) all_raw_tys
+ val dtinfos = map (Datatype.the_info (ProofContext.theory_of lthy0)) all_raw_ty_names
val inject_thms = flat (map #inject dtinfos);
val distinct_thms = flat (map #distinct dtinfos);
val constr_thms = inject_thms @ distinct_thms
val rel_dtinfos = List.take (dtinfos, (length dts));
val raw_constrs_distinct = (map #distinct rel_dtinfos);
- val induct_thm = #induct dtinfo;
+ val raw_induct_thm = #induct dtinfo;
+ val raw_induct_thms = #inducts dtinfo;
val exhaust_thms = map #exhaust dtinfos;
+ val raw_size_trms = map (fn ty => Const (@{const_name size}, ty --> @{typ nat})) all_raw_tys
+ val raw_size_thms = Size.size_thms (ProofContext.theory_of lthy0) (hd raw_dt_names)
+ |> `(fn thms => (length thms) div 2)
+ |> (uncurry drop)
+
(* definitions of raw permutations *)
val _ = warning "Definition of raw permutations";
val ((raw_perm_funs, raw_perm_simps, raw_perm_laws), lthy2) =
if get_STEPS lthy0 > 1
- then Local_Theory.theory_result (define_raw_perms descr sorts induct_thm (length dts)) lthy0
+ then Local_Theory.theory_result (define_raw_perms descr sorts raw_induct_thm (length dts)) lthy0
else raise TEST lthy0
(* noting the raw permutations as eqvt theorems *)
@@ -338,7 +345,7 @@
val (raw_bns, raw_bn_eqs, raw_bn_info, raw_bn_induct, lthy3a) =
if get_STEPS lthy3 > 2
- then raw_bn_decls all_raw_tys raw_dts raw_bn_funs raw_bn_eqs constr_thms lthy3
+ then raw_bn_decls all_raw_ty_names raw_dts raw_bn_funs raw_bn_eqs constr_thms lthy3
else raise TEST lthy3
val (raw_fvs, raw_fv_bns, raw_fv_defs, raw_fv_bns_induct, lthy3b) =
@@ -367,7 +374,7 @@
then mk_alpha_eq_iff lthy4 alpha_intros distinct_thms inject_thms alpha_cases
else raise TEST lthy4
- (* proving equivariance lemmas for bns, fvs and alpha *)
+ (* proving equivariance lemmas for bns, fvs, size and alpha *)
val _ = warning "Proving equivariance";
val bn_eqvt =
if get_STEPS lthy > 6
@@ -381,13 +388,19 @@
val fv_eqvt =
if get_STEPS lthy > 7
then raw_prove_eqvt (raw_fvs @ raw_fv_bns) raw_fv_bns_induct (raw_fv_defs @ raw_perm_simps)
- (Local_Theory.restore lthy_tmp)
+ (Local_Theory.restore lthy_tmp)
+ else raise TEST lthy4
+
+ val size_eqvt =
+ if get_STEPS lthy > 8
+ then raw_prove_eqvt raw_size_trms raw_induct_thms (raw_size_thms @ raw_perm_simps)
+ (Local_Theory.restore lthy_tmp)
else raise TEST lthy4
val lthy5 = snd (Local_Theory.note ((Binding.empty, [add_eqvt]), fv_eqvt) lthy_tmp)
val (alpha_eqvt, lthy6) =
- if get_STEPS lthy > 8
+ if get_STEPS lthy > 9
then Nominal_Eqvt.equivariance true (alpha_trms @ alpha_bn_trms) alpha_induct alpha_intros lthy5
else raise TEST lthy4
@@ -395,23 +408,23 @@
val _ = warning "Proving equivalence"
val alpha_refl_thms =
- if get_STEPS lthy > 9
- then raw_prove_refl alpha_trms alpha_bn_trms alpha_intros induct_thm lthy6
+ if get_STEPS lthy > 10
+ then raw_prove_refl alpha_trms alpha_bn_trms alpha_intros raw_induct_thm lthy6
else raise TEST lthy6
val alpha_sym_thms =
- if get_STEPS lthy > 10
+ if get_STEPS lthy > 11
then raw_prove_sym (alpha_trms @ alpha_bn_trms) alpha_intros alpha_induct lthy6
else raise TEST lthy6
val alpha_trans_thms =
- if get_STEPS lthy > 11
+ if get_STEPS lthy > 12
then raw_prove_trans (alpha_trms @ alpha_bn_trms) (distinct_thms @ inject_thms)
alpha_intros alpha_induct alpha_cases lthy6
else raise TEST lthy6
val alpha_equivp_thms =
- if get_STEPS lthy > 12
+ if get_STEPS lthy > 13
then raw_prove_equivp alpha_trms alpha_refl_thms alpha_sym_thms alpha_trans_thms lthy6
else raise TEST lthy6
@@ -419,16 +432,14 @@
val _ = warning "Proving alpha implies bn"
val alpha_bn_imp_thms =
- if get_STEPS lthy > 13
+ if get_STEPS lthy > 14
then raw_prove_bn_imp alpha_trms alpha_bn_trms alpha_intros alpha_induct lthy6
else raise TEST lthy6
(* auxiliary lemmas for respectfulness proofs *)
- (* HERE *)
-
- val test = raw_fv_bn_rsp_aux alpha_trms alpha_bn_trms raw_fvs raw_bns raw_fv_bns
- alpha_induct (raw_bn_eqs @ raw_fv_defs) lthy6
- val _ = tracing ("goals\n" ^ cat_lines (map (Syntax.string_of_term lthy6 o prop_of) test))
+ val raw_funs_rsp = raw_fv_bn_rsp_aux alpha_trms alpha_bn_trms raw_fvs
+ raw_bns raw_fv_bns alpha_induct (raw_bn_eqs @ raw_fv_defs) lthy6
+
(* defining the quotient type *)
val _ = warning "Declaring the quotient types"
@@ -438,7 +449,7 @@
val qty_full_names = map (Long_Name.qualify thy_name) qty_names (* not used *)
val (qty_infos, lthy7) =
- if get_STEPS lthy > 14
+ if get_STEPS lthy > 15
then qtype_defs qty_descr alpha_tys alpha_trms alpha_equivp_thms lthy6
else raise TEST lthy6
@@ -463,7 +474,7 @@
map2 (fn (b, _, _) => fn t => ("alpha_" ^ Name.of_binding b, t, NoSyn)) bn_funs alpha_bn_trms
val (((((qconstrs_info, qbns_info), qfvs_info), qfv_bns_info), qalpha_bns_info), lthy8) =
- if get_STEPS lthy > 15
+ if get_STEPS lthy > 16
then
lthy7
|> qconst_defs qtys qconstrs_descr
@@ -479,7 +490,7 @@
val qfv_bns = map #qconst qfv_bns_info
val qalpha_bns = map #qconst qalpha_bns_info
- (* HERE *)
+ (* temporary theorem bindings *)
val (_, lthy8') = lthy8
|> Local_Theory.note ((@{binding "distinct"}, []), alpha_distincts)
@@ -489,9 +500,11 @@
||>> Local_Theory.note ((@{binding "perm_simps"}, []), raw_perm_simps)
||>> Local_Theory.note ((@{binding "perm_laws"}, []), raw_perm_laws)
||>> Local_Theory.note ((@{binding "alpha_bn_imps"}, []), alpha_bn_imp_thms)
+ ||>> Local_Theory.note ((@{binding "funs_rsp"}, []), raw_funs_rsp)
+ ||>> Local_Theory.note ((@{binding "size_eqvt"}, []), size_eqvt)
val _ =
- if get_STEPS lthy > 16
+ if get_STEPS lthy > 17
then true else raise TEST lthy8'
(* old stuff *)
@@ -558,7 +571,7 @@
fun suffix_bind s = Binding.qualify true q_name (Binding.name s);
val _ = warning "Lifting induction";
val constr_names = map (Long_Name.base_name o fst o dest_Const) qconstrs;
- val q_induct = Rule_Cases.name constr_names (lift_thm qtys lthy13 induct_thm);
+ val q_induct = Rule_Cases.name constr_names (lift_thm qtys lthy13 raw_induct_thm);
fun note_suffix s th ctxt =
snd (Local_Theory.note ((suffix_bind s, []), th) ctxt);
fun note_simp_suffix s th ctxt =
--- a/Nominal/nominal_dt_rawfuns.ML Thu Jul 29 10:16:33 2010 +0100
+++ b/Nominal/nominal_dt_rawfuns.ML Fri Jul 30 00:40:32 2010 +0100
@@ -258,11 +258,11 @@
val eqvt_apply_sym = @{thm eqvt_apply[symmetric]}
fun subproof_tac const_names simps =
- Subgoal.FOCUS (fn {prems, context, ...} =>
+ SUBPROOF (fn {prems, context, ...} =>
HEADGOAL
(simp_tac (HOL_basic_ss addsimps simps)
THEN' Nominal_Permeq.eqvt_tac context [] const_names
- THEN' simp_tac (HOL_basic_ss addsimps (eqvt_apply_sym :: prems))))
+ THEN' simp_tac (HOL_basic_ss addsimps (prems @ [eqvt_apply_sym]))))
fun prove_eqvt_tac insts ind_thms const_names simps ctxt =
HEADGOAL