merged
authorChristian Urban <urbanc@in.tum.de>
Wed, 17 Mar 2010 17:11:23 +0100
changeset 1486 f86710d35146
parent 1485 c004e7448dca (current diff)
parent 1482 a98c15866300 (diff)
child 1490 9923b2cee778
child 1491 f970ca9b5bec
merged
Nominal/Parser.thy
Nominal/Test.thy
--- 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;