# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1268692976 -3600
# Node ID 104bdc0757e9241780f41909f3a6f12dc8c1ce8a
# Parent  1ae5afcddcd4bf028fca445334aad560e91fcf76# Parent  f2c50884dfb9efcba6cfa725d2c059196eb01bb0
merged (confirmed to work with Isabelle from 6th March)

diff -r 1ae5afcddcd4 -r 104bdc0757e9 Nominal/Abs.thy
--- a/Nominal/Abs.thy	Mon Mar 15 17:52:31 2010 +0100
+++ b/Nominal/Abs.thy	Mon Mar 15 23:42:56 2010 +0100
@@ -1,5 +1,5 @@
 theory Abs
-imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "../Quotient" "../Quotient_Product"
+imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "Quotient" "Quotient_Product"
 begin
 
 lemma permute_boolI:
@@ -272,8 +272,6 @@
   apply(simp)
   done
 
-term "alpha_abs_tst"
-
 quotient_type ('a,'b) abs_tst = "(('a \<Rightarrow>atom set) \<times> 'a::pt \<times> 'b::pt)" / "alpha_abs_tst"
   apply(rule equivpI)
   unfolding reflp_def symp_def transp_def
@@ -299,7 +297,6 @@
   apply(simp)
   done
 
-
 quotient_definition
   "Abs::atom set \<Rightarrow> ('a::pt) \<Rightarrow> 'a abs"
 is
diff -r 1ae5afcddcd4 -r 104bdc0757e9 Nominal/LFex.thy
--- a/Nominal/LFex.thy	Mon Mar 15 17:52:31 2010 +0100
+++ b/Nominal/LFex.thy	Mon Mar 15 23:42:56 2010 +0100
@@ -5,6 +5,12 @@
 atom_decl name
 atom_decl ident
 
+ML {* val cheat_fv_rsp = ref false *}
+ML {* val cheat_const_rsp = ref false *}
+ML {* val cheat_equivp = ref false *}
+ML {* val cheat_fv_eqvt = ref false *}
+ML {* val cheat_alpha_eqvt = ref false *}
+
 nominal_datatype kind =
     Type
   | KPi "ty" n::"name" k::"kind" bind n in k
diff -r 1ae5afcddcd4 -r 104bdc0757e9 Nominal/Parser.thy
--- a/Nominal/Parser.thy	Mon Mar 15 17:52:31 2010 +0100
+++ b/Nominal/Parser.thy	Mon Mar 15 23:42:56 2010 +0100
@@ -279,6 +279,8 @@
 ML {* val cheat_fv_rsp = ref true *}
 ML {* val cheat_const_rsp = ref true *} (* For alpha_bn 0 and alpha_bn_rsp *)
 
+ML {* val cheat_equivp = ref true *}
+
 (* Fixes for these 2 are known *)
 ML {* val cheat_fv_eqvt = ref true *} (* The tactic works, building the goal needs fixing *)
 ML {* val cheat_alpha_eqvt = ref true *} (* The tactic works, building the goal needs fixing *)
@@ -317,8 +319,8 @@
   val alpha_ts_loc_nobn = List.take (alpha_ts_loc, length perms)
   val morphism_4_3 = ProofContext.export_morphism lthy4 lthy3;
   val fv_ts = map (Morphism.term morphism_4_3) fv_ts_loc;
-  val fv_ts_loc_nobn = List.take (fv_ts_loc, length perms)
-  val fv_ts_nobn = List.take (fv_ts, length perms)
+  val (fv_ts_loc_nobn, fv_ts_loc_bn) = chop (length perms) fv_ts_loc;
+  val (fv_ts_nobn, fv_ts_bn) = chop (length perms) fv_ts;
   val alpha_ts = map (Morphism.term morphism_4_3) alpha_ts_loc;
   val (alpha_ts_nobn, alpha_ts_bn) = chop (length perms) alpha_ts
   val alpha_induct_loc = #induct alpha
@@ -337,18 +339,22 @@
   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) lthy4 1
-  val alpha_eqvt_loc = build_alpha_eqvts alpha_ts_loc_nobn perms alpha_eqvt_tac' lthy4;
+  val alpha_eqvt_loc = build_alpha_eqvts alpha_ts_loc alpha_eqvt_tac' lthy4;
   val alpha_eqvt = ProofContext.export lthy4 lthy2 alpha_eqvt_loc;
+  val _ = map tracing (map PolyML.makestring alpha_eqvt)
   val (bv_eqvts, lthy5) = fold_map (build_bv_eqvt (raw_bn_eqs @ raw_perm_def) inducts) bns lthy4;
   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 (fv_eqvts, lthy6) = build_eqvts Binding.empty fv_ts_loc fv_eqvt_tac lthy5;
+  val (fv_eqvts, lthy6) = build_eqvts Binding.empty fv_ts_loc_nobn fv_eqvt_tac lthy5;
+  val (fv_bn_eqvts, lthy6a) = 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 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 alpha_equivp_loc = map (equivp_hack lthy6) alpha_ts_loc_nobn
-(*  val alpha_equivp_loc = build_equivps alpha_ts_loc induct alpha_induct_loc
-    inject alpha_inj_loc distinct alpha_cases_loc alpha_eqvt_loc lthy6;*)
+  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
+      inject alpha_inj_loc distincts alpha_cases_loc alpha_eqvt_loc lthy6;
   val alpha_equivp = ProofContext.export lthy6 lthy2 alpha_equivp_loc;
   val qty_binds = map (fn (_, b, _, _) => b) dts;
   val qty_names = map Name.of_binding qty_binds;
@@ -394,8 +400,10 @@
   val q_name = space_implode "_" qty_names;
   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
+  val (_, lthy14a) = Local_Theory.note ((Binding.name (q_name ^ "_inducts"), []), q_inducts) lthy14;
   val q_perm = map (lift_thm lthy14) raw_perm_def;
-  val (_, lthy15) = Local_Theory.note ((Binding.name (q_name ^ "_perm"), []), q_perm) lthy14;
+  val (_, lthy15) = Local_Theory.note ((Binding.name (q_name ^ "_perm"), []), q_perm) lthy14a;
   val q_fv = map (lift_thm lthy15) fv_def;
   val (_, lthy16) = Local_Theory.note ((Binding.name (q_name ^ "_fv"), []), q_fv) lthy15;
   val q_bn = map (lift_thm lthy16) raw_bn_eqs;
diff -r 1ae5afcddcd4 -r 104bdc0757e9 Nominal/Rsp.thy
--- a/Nominal/Rsp.thy	Mon Mar 15 17:52:31 2010 +0100
+++ b/Nominal/Rsp.thy	Mon Mar 15 23:42:56 2010 +0100
@@ -135,6 +135,16 @@
 *}
 
 ML {*
+fun perm_arg arg =
+let
+  val ty = fastype_of arg
+in
+  Const (@{const_name permute}, @{typ perm} --> ty --> ty)
+end
+*}
+
+
+ML {*
 fun build_eqvts bind funs tac ctxt =
 let
   val pi = Free ("p", @{typ perm});
@@ -142,7 +152,6 @@
   val indnames = Name.variant_list ["p"] (Datatype_Prop.make_tnames types);
   val args = map Free (indnames ~~ types);
   val perm_at = @{term "permute :: perm \<Rightarrow> atom set \<Rightarrow> atom set"}
-  fun perm_arg arg = Const (@{const_name permute}, @{typ perm} --> fastype_of arg --> fastype_of arg)
   fun eqvtc (fnctn, arg) =
     HOLogic.mk_eq ((perm_at $ pi $ (fnctn $ arg)), (fnctn $ (perm_arg arg $ pi $ arg)))
   val gl = HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj (map eqvtc (funs ~~ args)))
@@ -181,19 +190,26 @@
 *}
 
 ML {*
-fun build_alpha_eqvts funs perms tac ctxt =
+fun build_alpha_eqvt alpha names =
 let
   val pi = Free ("p", @{typ perm});
-  val types = map (domain_type o fastype_of) funs;
-  val indnames = Name.variant_list ["p"] (Datatype_Prop.make_tnames (map body_type types));
-  val indnames2 = Name.variant_list ("p" :: indnames) (Datatype_Prop.make_tnames (map body_type types));
-  val args = map Free (indnames ~~ types);
-  val args2 = map Free (indnames2 ~~ types);
-  fun eqvtc ((alpha, perm), (arg, arg2)) =
-    HOLogic.mk_imp (alpha $ arg $ arg2,
-      (alpha $ (perm $ pi $ arg) $ (perm $ pi $ arg2)))
-  val gl = HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj (map eqvtc ((funs ~~ perms) ~~ (args ~~ args2))))
-  val thm = Goal.prove ctxt ("p" :: indnames @ indnames2) [] gl tac
+  val (tys, _) = strip_type (fastype_of alpha)
+  val indnames = Name.variant_list names (Datatype_Prop.make_tnames (map body_type tys));
+  val args = map Free (indnames ~~ tys);
+  val perm_args = map (fn x => perm_arg x $ pi $ x) args
+in
+  (HOLogic.mk_imp (list_comb (alpha, args), list_comb (alpha, perm_args)), indnames @ names)
+end
+*}
+
+ML {* fold_map build_alpha_eqvt *}
+
+ML {*
+fun build_alpha_eqvts funs tac ctxt =
+let
+  val (gls, names) = fold_map build_alpha_eqvt funs ["p"]
+  val gl = HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj gls)
+  val thm = Goal.prove ctxt names [] gl tac
 in
   map (fn x => mp OF [x]) (HOLogic.conj_elims thm)
 end
diff -r 1ae5afcddcd4 -r 104bdc0757e9 Nominal/Term1.thy
--- a/Nominal/Term1.thy	Mon Mar 15 17:52:31 2010 +0100
+++ b/Nominal/Term1.thy	Mon Mar 15 23:42:56 2010 +0100
@@ -52,6 +52,18 @@
 snd o build_eqvts @{binding fv_rtrm1_fv_bp_eqvt} [@{term fv_rtrm1}, @{term fv_bp}] (build_eqvts_tac @{thm rtrm1_bp.induct} @{thms fv_rtrm1_fv_bp.simps permute_rtrm1_permute_bp.simps} @{context})
 *}
 
+(*
+local_setup {*
+snd o build_eqvts @{binding fv_rtrm1_fv_bv1_eqvt} [@{term fv_rtrm1}, @{term fv_bv1}] (build_eqvts_tac @{thm rtrm1_bp.induct} @{thms fv_rtrm1_fv_bv1.simps permute_rtrm1_permute_bp.simps} @{context})
+*}
+print_theorems
+
+local_setup {*
+snd o build_eqvts @{binding fv_bp_eqvt} [@{term fv_bp}] (build_eqvts_tac @{thm rtrm1_bp.inducts(2)} @{thms fv_rtrm1_fv_bv1.simps fv_bp.simps permute_rtrm1_permute_bp.simps} @{context})
+*}
+print_theorems
+*)
+
 lemma alpha1_eqvt: 
   "(rtrm1 \<approx>1 rtrm1a \<longrightarrow> (p \<bullet> rtrm1) \<approx>1 (p \<bullet> rtrm1a)) \<and> 
    (bp \<approx>1b bpa \<longrightarrow> (p \<bullet> bp) \<approx>1b (p \<bullet> bpa)) \<and>
diff -r 1ae5afcddcd4 -r 104bdc0757e9 Nominal/Test.thy
--- a/Nominal/Test.thy	Mon Mar 15 17:52:31 2010 +0100
+++ b/Nominal/Test.thy	Mon Mar 15 23:42:56 2010 +0100
@@ -6,6 +6,9 @@
 
 atom_decl name
 
+ML {* val cheat_alpha_eqvt = ref false *}
+ML {* val cheat_fv_eqvt = ref false *}
+
 (*
 nominal_datatype lam =
   VAR "name"
@@ -37,11 +40,11 @@
 thm lam_bp_bn
 thm lam_bp_perm
 thm lam_bp_induct
+thm lam_bp_inducts
 thm lam_bp_distinct
 ML {* Sign.of_sort @{theory} (@{typ lam}, @{sort fs}) *}
 
 term "supp (x :: lam)"
-lemmas lam_bp_inducts = lam_raw_bp_raw.inducts[quot_lifted]
 
 (* maybe should be added to Infinite.thy *)
 lemma infinite_Un:
@@ -50,13 +53,7 @@
 
 lemma bi_eqvt:
   shows "(p \<bullet> (bi b)) = bi (p \<bullet> b)"
-apply(induct b rule: lam_bp_inducts(2))
-apply(simp)
-apply(simp)
-apply(simp)
-apply(simp add: lam_bp_bn lam_bp_perm)
-apply(simp add: eqvts)
-done
+  by (rule eqvts)
 
 term alpha_bi
 
@@ -366,6 +363,7 @@
 thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm_bn
 thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm_perm
 thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm_induct
+thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm_inducts
 thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm_distinct
 
 (* example 3 from Peter Sewell's bestiary *)
diff -r 1ae5afcddcd4 -r 104bdc0757e9 Nominal/nominal_atoms.ML
--- a/Nominal/nominal_atoms.ML	Mon Mar 15 17:52:31 2010 +0100
+++ b/Nominal/nominal_atoms.ML	Mon Mar 15 23:42:56 2010 +0100
@@ -44,7 +44,7 @@
     val set = atom_decl_set str;
     val tac = rtac @{thm exists_eq_simple_sort} 1;
     val ((full_tname, info as {type_definition, Rep_name, Abs_name, ...}), thy) =
-      Typedef.add_typedef_global false NONE (name, [], NoSyn) set NONE tac thy;
+      Typedef.add_typedef false NONE (name, [], NoSyn) set NONE tac thy;
 
     (* definition of atom and permute *)
     val newT = #abs_type info;