--- a/Nominal/Abs.thy Wed Mar 17 17:10:19 2010 +0100
+++ b/Nominal/Abs.thy Wed Mar 17 17:11:23 2010 +0100
@@ -74,7 +74,7 @@
and a: "\<And>pi t s. (R t s \<Longrightarrow> R (pi \<bullet> t) (pi \<bullet> s))"
shows "(ab, s) \<approx>gen R f (- pi) (aa, t)"
using b apply -
- apply(simp add: alpha_gen.simps)
+ apply(simp add: alpha_gen)
apply(erule conjE)+
apply(rule conjI)
apply(simp add: fresh_star_def fresh_minus_perm)
@@ -86,6 +86,35 @@
apply assumption
done
+lemma alpha_gen_compose_sym2:
+ assumes a: "(aa, (t1, t2)) \<approx>gen (\<lambda>(x11, x12) (x21, x22). R1 x11 x21 \<and> R1 x21 x11 \<and> R2 x12 x22 \<and> R2 x22 x12)
+ (\<lambda>(b, a). fb b \<union> fa a) pi (ab, (s1, s2))"
+ and r1: "\<And>pi t s. R1 t s \<Longrightarrow> R1 (pi \<bullet> t) (pi \<bullet> s)"
+ and r2: "\<And>pi t s. R2 t s \<Longrightarrow> R2 (pi \<bullet> t) (pi \<bullet> s)"
+ shows "(ab, (s1, s2)) \<approx>gen
+ (\<lambda>x1 x2. (\<lambda>(a, b) (d, c). R1 a d \<and> R2 b c) x1 x2 \<and> (\<lambda>(a, b) (d, c). R1 a d \<and> R2 b c) x2 x1)
+ (\<lambda>(b, a). fb b \<union> fa a) (- pi) (aa, (t1, t2))"
+ using a
+apply(simp add: alpha_gen)
+apply clarify
+apply (rule conjI)
+ apply(simp add: fresh_star_def fresh_minus_perm)
+apply (rule conjI)
+apply (rotate_tac 3)
+apply (drule_tac pi="- pi" in r1)
+apply simp
+apply (rule conjI)
+apply (rotate_tac -1)
+apply (drule_tac pi="- pi" in r2)
+apply simp
+apply (rule conjI)
+apply (drule_tac pi="- pi" in r1)
+apply simp
+apply (rule conjI)
+apply (drule_tac pi="- pi" in r2)
+apply simp_all
+done
+
lemma alpha_gen_compose_trans:
fixes pi pia
assumes b: "(aa, t) \<approx>gen (\<lambda>x1 x2. R x1 x2 \<and> (\<forall>x. R x2 x \<longrightarrow> R x1 x)) f pi (ab, ta)"
--- a/Nominal/Fv.thy Wed Mar 17 17:10:19 2010 +0100
+++ b/Nominal/Fv.thy Wed Mar 17 17:11:23 2010 +0100
@@ -389,16 +389,12 @@
val rhs_binds = fv_binds args2 rbinds;
val rhs_arg = foldr1 HOLogic.mk_prod bound_args2;
val rhs = mk_pair (rhs_binds, rhs_arg);
- val _ = tracing (PolyML.makestring bound_in_ty_nos);
val fvs = map (nth fv_frees) ((body_index dt) :: bound_in_ty_nos);
- val _ = tracing (PolyML.makestring fvs);
val fv = mk_compound_fv fvs;
val alphas = map (nth alpha_frees) ((body_index dt) :: bound_in_ty_nos);
- val _ = tracing (PolyML.makestring alphas);
val alpha = mk_compound_alpha alphas;
val pi = foldr1 add_perm (distinct (op =) rpis);
val alpha_gen_pre = Const (@{const_name alpha_gen}, dummyT) $ lhs $ alpha $ fv $ pi $ rhs;
- val _ = tracing (PolyML.makestring alpha_gen_pre);
val alpha_gen = Syntax.check_term lthy alpha_gen_pre
in
alpha_gen
@@ -449,7 +445,6 @@
val fv_names_all = fv_names_fst @ fv_bn_names;
val add_binds = map (fn x => (Attrib.empty_binding, x))
(* Function_Fun.add_fun Function_Common.default_config ... true *)
-(* val _ = map tracing (map (Syntax.string_of_term @{context}) fv_eqs_all)*)
val (fvs, lthy') = (Primrec.add_primrec
(map (fn s => (Binding.name s, NONE, NoSyn)) fv_names_all) (add_binds fv_eqs_all) lthy)
val (fvs2, lthy'') =
@@ -596,7 +591,7 @@
split_conjs THEN_ALL_NEW REPEAT o rtac @{thm exI[of _ "0 :: perm"]}
THEN_ALL_NEW split_conjs THEN_ALL_NEW asm_full_simp_tac (HOL_ss addsimps
@{thms alpha_gen fresh_star_def fresh_zero_perm permute_zero ball_triv
- add_0_left supp_zero_perm Int_empty_left})
+ add_0_left supp_zero_perm Int_empty_left split_conv})
*}
--- a/Nominal/Parser.thy Wed Mar 17 17:10:19 2010 +0100
+++ b/Nominal/Parser.thy Wed Mar 17 17:11:23 2010 +0100
@@ -243,7 +243,7 @@
val raw_bns = prep_bn dt_full_names' raw_dts (map snd raw_bn_eqs)
- val _ = tracing (cat_lines (map PolyML.makestring raw_bns))
+(*val _ = tracing (cat_lines (map PolyML.makestring raw_bns))*)
in
lthy
|> add_datatype_wrapper raw_dt_names raw_dts
@@ -289,6 +289,7 @@
ML {*
fun nominal_datatype2 dts bn_funs bn_eqs binds lthy =
let
+ val _ = tracing "Raw declarations";
val thy = ProofContext.theory_of lthy
val thy_name = Context.theory_name thy
val ((((raw_dt_names, (raw_bn_funs_loc, raw_bn_eqs_loc)), raw_binds), raw_bns), lthy2) =
@@ -311,6 +312,7 @@
val rel_distinct = map #distinct rel_dtinfos;
val induct = #induct dtinfo;
val inducts = #inducts dtinfo;
+ val _ = tracing "Defining permutations, fv and alpha";
val ((raw_perm_def, raw_perm_simps, perms), lthy3) =
Local_Theory.theory_result (define_raw_perms dtinfo (length dts)) lthy2;
val raw_binds_flat = map (map flat) raw_binds;
@@ -336,29 +338,25 @@
val alpha_cases = ProofContext.export lthy4 lthy3 alpha_cases_loc
val alpha_inj_loc = build_alpha_inj alpha_intros (inject @ distincts) alpha_cases_loc lthy4
val alpha_inj = ProofContext.export lthy4 lthy3 alpha_inj_loc
+ val _ = tracing "Proving equivariance";
val (bv_eqvts, lthy5) = fold_map (build_bv_eqvt (raw_bn_eqs @ raw_perm_def) inducts) bns lthy4;
- val _ = tracing "3";
val fv_eqvt_tac =
if !cheat_fv_eqvt then (fn _ => fn _ => Skip_Proof.cheat_tac thy)
else build_eqvts_tac induct ((flat (map snd bv_eqvts)) @ fv_def_loc @ raw_perm_def) lthy5
- val _ = tracing "4";
val (fv_eqvts, lthy6) = build_eqvts Binding.empty fv_ts_loc_nobn fv_eqvt_tac lthy5;
- val _ = tracing "4a";
val (fv_bn_eqvts, lthy6a) =
if fv_ts_loc_bn = [] then ([], lthy6) else
fold_map (build_bv_eqvt ((flat (map snd bv_eqvts)) @ fv_def_loc @ raw_perm_def) inducts)
(fv_ts_loc_bn ~~ (map snd bns)) lthy6;
- val _ = tracing "4b";
val lthy6 = lthy6a;
val raw_fv_bv_eqvt_loc = flat (map snd bv_eqvts) @ (snd fv_eqvts)
val raw_fv_bv_eqvt = ProofContext.export lthy6 lthy3 raw_fv_bv_eqvt_loc;
- val _ = tracing "5";
fun alpha_eqvt_tac' _ =
if !cheat_alpha_eqvt then Skip_Proof.cheat_tac thy
else alpha_eqvt_tac alpha_induct_loc (raw_perm_def @ alpha_inj_loc @ raw_fv_bv_eqvt_loc) lthy6 1
val alpha_eqvt_loc = build_alpha_eqvts alpha_ts_loc alpha_eqvt_tac' lthy6;
val alpha_eqvt = ProofContext.export lthy6 lthy2 alpha_eqvt_loc;
- val _ = map tracing (map PolyML.makestring alpha_eqvt)
+ val _ = tracing "Proving equivalence";
val alpha_equivp_loc =
if !cheat_equivp then map (equivp_hack lthy6) alpha_ts_loc_nobn
else build_equivps alpha_ts_loc induct alpha_induct_loc
@@ -382,6 +380,7 @@
val consts = map (Morphism.term morphism_8_7) consts_loc;
(* Could be done nicer *)
val q_tys = distinct (op =) (map (snd o strip_type o fastype_of) consts);
+ val _ = tracing "Proving respects";
val (bns_rsp_pre, lthy9) = fold_map (
fn (bn_t, i) => prove_const_rsp Binding.empty [bn_t]
(fn _ => fvbv_rsp_tac (nth alpha_inducts i) raw_bn_eqs 1)) bns lthy8;
@@ -400,12 +399,14 @@
val qbn_names = map (fn (b, _ , _) => Name.of_binding b) bn_funs
val (qbn_defs, lthy12b) = fold_map Quotient_Def.quotient_lift_const (qbn_names ~~ raw_bn_funs) lthy12a;
val qalpha_bn_names = map (unsuffix "_raw" o Long_Name.base_name o fst o dest_Const) alpha_ts_bn
+ val _ = tracing "Lifting permutations";
val (qbn_defs, lthy12c) = fold_map Quotient_Def.quotient_lift_const (qalpha_bn_names ~~ alpha_ts_bn) lthy12b;
val thy = Local_Theory.exit_global lthy12c;
val perm_names = map (fn x => "permute_" ^ x) qty_names
val thy' = define_lifted_perms qty_full_names (perm_names ~~ perms) raw_perm_simps thy;
val lthy13 = Theory_Target.init NONE thy';
val q_name = space_implode "_" qty_names;
+ val _ = tracing "Lifting induction";
val q_induct = lift_thm lthy13 induct;
val (_, lthy14) = Local_Theory.note ((Binding.name (q_name ^ "_induct"), []), [q_induct]) lthy13;
val q_inducts = Project_Rule.projects lthy13 (1 upto (length alpha_inducts)) q_induct
@@ -416,6 +417,7 @@
val (_, lthy16) = Local_Theory.note ((Binding.name (q_name ^ "_fv"), []), q_fv) lthy15;
val q_bn = map (lift_thm lthy16) raw_bn_eqs;
val (_, lthy17) = Local_Theory.note ((Binding.name (q_name ^ "_bn"), []), q_bn) lthy16;
+ val _ = tracing "Lifting pseudo-injectivity";
val inj_unfolded1 = map (Local_Defs.unfold lthy17 @{thms alpha_gen2}) alpha_inj
val inj_unfolded2 = map (Local_Defs.unfold lthy17 @{thms alpha_gen}) inj_unfolded1
val q_inj_pre1 = map (lift_thm lthy17) inj_unfolded2;
@@ -429,8 +431,8 @@
val q_eqvt = map (lift_thm lthy19) raw_fv_bv_eqvt;
val (_, lthy20) = Local_Theory.note ((Binding.empty,
[Attrib.internal (fn _ => Nominal_ThmDecls.eqvt_add)]), q_eqvt) lthy19;
+ val _ = tracing "Finite Support";
val supports = map (prove_supports lthy20 q_perm) consts
- val _ = map tracing (map PolyML.makestring supports);
val fin_supp = HOLogic.conj_elims (prove_fs lthy20 q_induct supports q_tys) handle _ => []
val thy3 = Local_Theory.exit_global lthy20;
val lthy21 = Theory_Target.instantiation (qty_full_names, [], @{sort fs}) thy3;