# HG changeset patch
# User berghofe
# Date 1176993539 -7200
# Node ID 8bcc8809ed3b55b15fc1cd6705991b892b2343bd
# Parent  69ef734825c57e54d572baaa7bb0bf87f7c3d490
nominal_inductive no longer proves equivariance.

diff -r 69ef734825c5 -r 8bcc8809ed3b src/HOL/Nominal/Examples/CR.thy
--- a/src/HOL/Nominal/Examples/CR.thy	Thu Apr 19 16:27:53 2007 +0200
+++ b/src/HOL/Nominal/Examples/CR.thy	Thu Apr 19 16:38:59 2007 +0200
@@ -155,6 +155,8 @@
   | b3[intro]: "s1\<longrightarrow>\<^isub>\<beta>s2 \<Longrightarrow> (Lam [a].s1)\<longrightarrow>\<^isub>\<beta> (Lam [a].s2)"
   | b4[intro]: "a\<sharp>s2 \<Longrightarrow> (App (Lam [a].s1) s2)\<longrightarrow>\<^isub>\<beta>(s1[a::=s2])"
 
+equivariance Beta
+
 nominal_inductive Beta
   by (simp_all add: abs_fresh fresh_fact')
 
@@ -183,6 +185,8 @@
   | o3[simp,intro!]: "s1\<longrightarrow>\<^isub>1s2 \<Longrightarrow> (Lam [a].s1)\<longrightarrow>\<^isub>1(Lam [a].s2)"
   | o4[simp,intro!]: "\<lbrakk>a\<sharp>(s1,s2); s1\<longrightarrow>\<^isub>1s2;t1\<longrightarrow>\<^isub>1t2\<rbrakk> \<Longrightarrow> (App (Lam [a].t1) s1)\<longrightarrow>\<^isub>1(t2[a::=s2])"
 
+equivariance One
+
 nominal_inductive One
   by (simp_all add: abs_fresh fresh_fact')
 
diff -r 69ef734825c5 -r 8bcc8809ed3b src/HOL/Nominal/Examples/Crary.thy
--- a/src/HOL/Nominal/Examples/Crary.thy	Thu Apr 19 16:27:53 2007 +0200
+++ b/src/HOL/Nominal/Examples/Crary.thy	Thu Apr 19 16:38:59 2007 +0200
@@ -304,6 +304,8 @@
 | t_Const[intro]: "valid \<Gamma> \<Longrightarrow> \<Gamma> \<turnstile> Const n : TBase"
 | t_Unit[intro]:  "valid \<Gamma> \<Longrightarrow> \<Gamma> \<turnstile> Unit : TUnit"
 
+equivariance typing
+
 nominal_inductive typing
   by (simp_all add: abs_fresh)
 
@@ -340,6 +342,8 @@
 | Q_Ext[intro]:   "\<lbrakk>x\<sharp>(\<Gamma>,s,t); (x,T\<^isub>1)#\<Gamma> \<turnstile> App s (Var x) \<equiv> App t (Var x) : T\<^isub>2\<rbrakk> 
                    \<Longrightarrow> \<Gamma> \<turnstile> s \<equiv> t : T\<^isub>1 \<rightarrow> T\<^isub>2"
 
+equivariance def_equiv
+
 nominal_inductive def_equiv
   by (simp_all add: abs_fresh fresh_subst'')
 
@@ -452,6 +456,8 @@
 | QAP_App[intro]:   "\<lbrakk>\<Gamma> \<turnstile> p \<leftrightarrow> q : T\<^isub>1 \<rightarrow> T\<^isub>2; \<Gamma> \<turnstile> s \<Leftrightarrow> t : T\<^isub>1\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> App p s \<leftrightarrow> App q t : T\<^isub>2"
 | QAP_Const[intro]: "valid \<Gamma> \<Longrightarrow> \<Gamma> \<turnstile> Const n \<leftrightarrow> Const n : TBase"
 
+equivariance alg_equiv
+
 nominal_inductive alg_equiv
   avoids QAT_Arrow: x
   by simp_all
diff -r 69ef734825c5 -r 8bcc8809ed3b src/HOL/Nominal/Examples/Fsub.thy
--- a/src/HOL/Nominal/Examples/Fsub.thy	Thu Apr 19 16:27:53 2007 +0200
+++ b/src/HOL/Nominal/Examples/Fsub.thy	Thu Apr 19 16:38:59 2007 +0200
@@ -330,6 +330,8 @@
   ultimately show "X\<sharp>S \<and> X\<sharp>T" by (force simp add: supp_prod fresh_def)
 qed
 
+equivariance subtype_of
+
 nominal_inductive subtype_of  
   by (simp_all add: abs_fresh subtype_implies_fresh)
 
diff -r 69ef734825c5 -r 8bcc8809ed3b src/HOL/Nominal/Examples/SN.thy
--- a/src/HOL/Nominal/Examples/SN.thy	Thu Apr 19 16:27:53 2007 +0200
+++ b/src/HOL/Nominal/Examples/SN.thy	Thu Apr 19 16:38:59 2007 +0200
@@ -66,6 +66,8 @@
 | b3[intro!]: "s1\<longrightarrow>\<^isub>\<beta>s2 \<Longrightarrow> (Lam [a].s1)\<longrightarrow>\<^isub>\<beta> (Lam [a].s2)"
 | b4[intro!]: "a\<sharp>s2 \<Longrightarrow>(App (Lam [a].s1) s2)\<longrightarrow>\<^isub>\<beta>(s1[a::=s2])"
 
+equivariance Beta
+
 nominal_inductive Beta
   by (simp_all add: abs_fresh fresh_fact')
 
@@ -166,6 +168,8 @@
 | t2[intro]: "\<lbrakk>\<Gamma> \<turnstile> t1 : \<tau>\<rightarrow>\<sigma>; \<Gamma> \<turnstile> t2 : \<tau>\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> App t1 t2 : \<sigma>"
 | t3[intro]: "\<lbrakk>a\<sharp>\<Gamma>;((a,\<tau>)#\<Gamma>) \<turnstile> t : \<sigma>\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> Lam [a].t : \<tau>\<rightarrow>\<sigma>"
 
+equivariance typing
+
 nominal_inductive typing
   by (simp_all add: abs_fresh fresh_ty)
 
diff -r 69ef734825c5 -r 8bcc8809ed3b src/HOL/Nominal/Examples/SOS.thy
--- a/src/HOL/Nominal/Examples/SOS.thy	Thu Apr 19 16:27:53 2007 +0200
+++ b/src/HOL/Nominal/Examples/SOS.thy	Thu Apr 19 16:38:59 2007 +0200
@@ -269,6 +269,8 @@
                    (x\<^isub>1,Data(S\<^isub>1))#\<Gamma> \<turnstile> e\<^isub>1 : T; (x\<^isub>2,Data(S\<^isub>2))#\<Gamma> \<turnstile> e\<^isub>2 : T\<rbrakk> 
                    \<Longrightarrow> \<Gamma> \<turnstile> (Case e of inl x\<^isub>1 \<rightarrow> e\<^isub>1 | inr x\<^isub>2 \<rightarrow> e\<^isub>2) : T"
 
+equivariance typing
+
 nominal_inductive typing
   by (simp_all add: abs_fresh fresh_prod fresh_atm)
 
@@ -499,6 +501,8 @@
 | b_CaseR[intro]: "\<lbrakk>x\<^isub>1\<sharp>(e,e\<^isub>2,e'',x\<^isub>2); x\<^isub>2\<sharp>(e,e\<^isub>1,e'',x\<^isub>1) ; e\<Down>InR e'; e\<^isub>2[x\<^isub>2::=e']\<Down>e''\<rbrakk> 
                    \<Longrightarrow> Case e of inl x\<^isub>1 \<rightarrow> e\<^isub>1 | inr x\<^isub>2 \<rightarrow> e\<^isub>2 \<Down> e''"
 
+equivariance big
+
 nominal_inductive big
   by (simp_all add: abs_fresh fresh_prod fresh_atm)
 
diff -r 69ef734825c5 -r 8bcc8809ed3b src/HOL/Nominal/Examples/Weakening.thy
--- a/src/HOL/Nominal/Examples/Weakening.thy	Thu Apr 19 16:27:53 2007 +0200
+++ b/src/HOL/Nominal/Examples/Weakening.thy	Thu Apr 19 16:38:59 2007 +0200
@@ -43,6 +43,8 @@
   | t_App[intro]: "\<lbrakk>\<Gamma> \<turnstile> t1 : T1\<rightarrow>T2; \<Gamma> \<turnstile> t2 : T1\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> App t1 t2 : T2"
   | t_Lam[intro]: "\<lbrakk>x\<sharp>\<Gamma>;((x,T1)#\<Gamma>) \<turnstile> t : T2\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> Lam [x].t : T1\<rightarrow>T2"
 
+equivariance typing
+
 (* automatically deriving the strong induction principle *)
 nominal_inductive typing
   by (simp_all add: abs_fresh ty_fresh)
diff -r 69ef734825c5 -r 8bcc8809ed3b src/HOL/Nominal/nominal_inductive.ML
--- a/src/HOL/Nominal/nominal_inductive.ML	Thu Apr 19 16:27:53 2007 +0200
+++ b/src/HOL/Nominal/nominal_inductive.ML	Thu Apr 19 16:38:59 2007 +0200
@@ -8,8 +8,8 @@
 
 signature NOMINAL_INDUCTIVE =
 sig
-  val nominal_inductive: string -> (string * string list) list -> theory -> Proof.state
-  val equivariance: string -> theory -> theory
+  val prove_strong_ind: string -> (string * string list) list -> theory -> Proof.state
+  val prove_eqvt: string -> string list -> theory -> theory
 end
 
 structure NominalInductive : NOMINAL_INDUCTIVE =
@@ -49,9 +49,11 @@
   | add_binders thy i (Abs (_, _, t)) bs = add_binders thy (i + 1) t bs
   | add_binders thy i _ bs = bs;
 
-fun prove_strong_ind raw_induct names avoids thy =
+fun prove_strong_ind s avoids thy =
   let
     val ctxt = ProofContext.init thy;
+    val ({names, ...}, {raw_induct, ...}) =
+      InductivePackage.the_inductive ctxt (Sign.intern_const thy s);
     val induct_cases = map fst (fst (RuleCases.get (the
       (InductAttrib.lookup_inductS ctxt (hd names)))));
     val raw_induct' = Logic.unvarify (prop_of raw_induct);
@@ -314,10 +316,24 @@
       (map (map (rpair [])) vc_compat)
   end;
 
-fun prove_eqvt names raw_induct intrs thy =
+fun prove_eqvt s xatoms thy =
   let
     val ctxt = ProofContext.init thy;
-    val atoms = NominalAtoms.atoms_of thy;
+    val ({names, ...}, {raw_induct, intrs, ...}) =
+      InductivePackage.the_inductive ctxt (Sign.intern_const thy s);
+    val atoms' = NominalAtoms.atoms_of thy;
+    val atoms =
+      if null xatoms then atoms' else
+      let val atoms = map (Sign.intern_type thy) xatoms
+      in
+        (case duplicates op = atoms of
+             [] => ()
+           | xs => error ("Duplicate atoms: " ^ commas xs);
+         case atoms \\ atoms' of
+             [] => ()
+           | xs => error ("No such atoms: " ^ commas xs);
+         atoms)
+      end;
     val eqvt_ss = HOL_basic_ss addsimps NominalThmDecls.get_eqvt_thms thy;
     val t = Logic.unvarify (concl_of raw_induct);
     val pi = Name.variant (add_term_names (t, [])) "pi";
@@ -363,20 +379,6 @@
       Theory.parent_path) (names ~~ transp thss) thy
   end;
 
-fun gen_nominal_inductive f s avoids thy =
-  let
-    val ctxt = ProofContext.init thy;
-    val ({names, ...}, {raw_induct, intrs, ...}) =
-      InductivePackage.the_inductive ctxt (Sign.intern_const thy s);
-  in
-    thy |>
-    prove_eqvt names raw_induct intrs |>
-    f raw_induct names avoids
-  end;
-
-val nominal_inductive = gen_nominal_inductive prove_strong_ind;
-fun equivariance s = gen_nominal_inductive (K (K (K I))) s [];
-
 
 (* outer syntax *)
 
@@ -387,12 +389,13 @@
     "prove equivariance and strong induction theorem for inductive predicate involving nominal datatypes" K.thy_goal
     (P.name -- Scan.optional (P.$$$ "avoids" |-- P.and_list1 (P.name --
       (P.$$$ ":" |-- Scan.repeat1 P.name))) [] >> (fn (name, avoids) =>
-        Toplevel.print o Toplevel.theory_to_proof (nominal_inductive name avoids)));
+        Toplevel.print o Toplevel.theory_to_proof (prove_strong_ind name avoids)));
 
 val equivarianceP =
   OuterSyntax.command "equivariance"
     "prove equivariance for inductive predicate involving nominal datatypes" K.thy_decl
-    (P.name >> (Toplevel.theory o equivariance));
+    (P.name -- Scan.optional (P.$$$ "[" |-- P.list1 P.name --| P.$$$ "]") [] >>
+      (fn (name, atoms) => Toplevel.theory (prove_eqvt name atoms)));
 
 val _ = OuterSyntax.add_keywords ["avoids"];
 val _ = OuterSyntax.add_parsers [nominal_inductiveP, equivarianceP];