# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1293809824 0
# Node ID 3ce1089cdbf3551c06419250430ebfb9de34c6e1
# Parent  d1d09177ec8985ce968a2f36fccae06902891790
changed res keyword to set+ for restrictions; comment by a referee

diff -r d1d09177ec89 -r 3ce1089cdbf3 Nominal/Ex/Lambda.thy
--- a/Nominal/Ex/Lambda.thy	Fri Dec 31 13:31:39 2010 +0000
+++ b/Nominal/Ex/Lambda.thy	Fri Dec 31 15:37:04 2010 +0000
@@ -19,6 +19,37 @@
 thm lam.fv_bn_eqvt
 thm lam.size_eqvt
 
+ML {*
+  Outer_Syntax.local_theory_to_proof;
+  Proof.theorem
+*}
+
+ML {*
+fun prove_strong_ind pred_name avoids ctxt =
+  let
+    val _ = ()
+  in
+    Proof.theorem NONE (fn thss => fn ctxt => ctxt) [] ctxt
+  end
+
+(* outer syntax *)
+local
+  structure P = Parse;
+  structure S = Scan
+
+in
+val _ =
+  Outer_Syntax.local_theory_to_proof "nominal_inductive"
+    "prove strong induction theorem for inductive predicate involving nominal datatypes"
+    Keyword.thy_goal
+    (Parse.xname -- 
+     (Scan.optional (Parse.$$$ "avoids" |-- Parse.enum1 "|" (Parse.name --
+      (Parse.$$$ ":" |-- Parse.and_list1 Parse.term))) []) >> (fn (pred_name, avoids) =>
+        prove_strong_ind pred_name avoids))
+
+end
+*}
+
 
 section {* Typing *}
 
@@ -27,9 +58,6 @@
 | TFun ty ty ("_ \<rightarrow> _") 
 
 
-(*
-declare ty.perm[eqvt]
-
 inductive
   valid :: "(name \<times> ty) list \<Rightarrow> bool"
 where
@@ -53,6 +81,7 @@
 
 thm typing.induct[of "\<Gamma>" "t" "T", no_vars]
 
+(*
 lemma
   fixes c::"'a::fs"
   assumes a: "\<Gamma> \<turnstile> t : T" 
diff -r d1d09177ec89 -r 3ce1089cdbf3 Nominal/Ex/Shallow.thy
--- a/Nominal/Ex/Shallow.thy	Fri Dec 31 13:31:39 2010 +0000
+++ b/Nominal/Ex/Shallow.thy	Fri Dec 31 15:37:04 2010 +0000
@@ -32,9 +32,9 @@
 nominal_datatype trm3 =
   Var3 "name"
 | App3 "trm3" "trm3"
-| Lam3 xs::"name fset" t::"trm3" bind (res) xs in t
+| Lam3 xs::"name fset" t::"trm3" bind (set+) xs in t
 
-thm trm3.strong_exhaust
+thm trm3.eq_iff
 
 end
 
diff -r d1d09177ec89 -r 3ce1089cdbf3 Nominal/Ex/SingleLet.thy
--- a/Nominal/Ex/SingleLet.thy	Fri Dec 31 13:31:39 2010 +0000
+++ b/Nominal/Ex/SingleLet.thy	Fri Dec 31 15:37:04 2010 +0000
@@ -11,7 +11,7 @@
 | Let a::"assg" t::"trm"  bind "bn a" in t
 | Foo x::"name" y::"name" t::"trm" t1::"trm" t2::"trm" bind (set) x in y t t1 t2
 | Bar x::"name" y::"name" t::"trm" bind y x in t x y
-| Baz x::"name" t1::"trm" t2::"trm" bind (set) x in t1, bind (res) x in t2 
+| Baz x::"name" t1::"trm" t2::"trm" bind (set) x in t1, bind (set+) x in t2 
 and assg =
   As "name" x::"name" t::"trm" bind x in t
 binder
diff -r d1d09177ec89 -r 3ce1089cdbf3 Nominal/Ex/TypeSchemes.thy
--- a/Nominal/Ex/TypeSchemes.thy	Fri Dec 31 13:31:39 2010 +0000
+++ b/Nominal/Ex/TypeSchemes.thy	Fri Dec 31 15:37:04 2010 +0000
@@ -12,7 +12,7 @@
   Var "name"
 | Fun "ty" "ty"
 and tys =
-  All xs::"name fset" ty::"ty" bind (res) xs in ty
+  All xs::"name fset" ty::"ty" bind (set+) xs in ty
 
 thm ty_tys.distinct
 thm ty_tys.induct
@@ -35,7 +35,7 @@
 | Fun2 "ty2" "ty2"
 
 nominal_datatype tys2 =
-  All2 xs::"name fset" ty::"ty2" bind (res) xs in ty
+  All2 xs::"name fset" ty::"ty2" bind (set+) xs in ty
 
 thm tys2.distinct
 thm tys2.induct tys2.strong_induct
diff -r d1d09177ec89 -r 3ce1089cdbf3 Nominal/Nominal2.thy
--- a/Nominal/Nominal2.thy	Fri Dec 31 13:31:39 2010 +0000
+++ b/Nominal/Nominal2.thy	Fri Dec 31 15:37:04 2010 +0000
@@ -774,7 +774,7 @@
 
 val bind_mode = P.$$$ "bind" |--
   S.optional (Args.parens 
-    (Args.$$$ "list" >> K Lst || Args.$$$ "set" >> K Set || Args.$$$ "res" >> K Res)) Lst
+    (Args.$$$ "list" >> K Lst || (Args.$$$ "set" -- Args.$$$ "+") >> K Res || Args.$$$ "set" >> K Set)) Lst
 
 val bind_clauses = 
   P.enum "," (bind_mode -- S.repeat1 P.term -- (P.$$$ "in" |-- S.repeat1 P.name) >> triple)