# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1269330703 -3600
# Node ID 8b5a1ad6048764e2cc5c589a3a5d253688212e80
# Parent  2406350c358f5cfc369e1816bd3793a9fbd229f9
Move Leroy out of Test, rename accordingly.

diff -r 2406350c358f -r 8b5a1ad60487 Nominal/ExLam.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Nominal/ExLam.thy	Tue Mar 23 08:51:43 2010 +0100
@@ -0,0 +1,91 @@
+theory ExLam
+imports "Parser"
+begin
+
+atom_decl name
+
+nominal_datatype lm =
+  Vr "name"
+| Ap "lm" "lm"
+| Lm x::"name" l::"lm"  bind x in l
+
+lemmas supp_fn' = lm.fv[simplified lm.supp]
+
+lemma
+  fixes c::"'a::fs"
+  assumes a1: "\<And>name c. P c (Vr name)"
+  and     a2: "\<And>lm1 lm2 c. \<lbrakk>\<And>d. P d lm1; \<And>d. P d lm2\<rbrakk> \<Longrightarrow> P c (Ap lm1 lm2)"
+  and     a3: "\<And>name lm c. \<lbrakk>atom name \<sharp> c; \<And>d. P d lm\<rbrakk> \<Longrightarrow> P c (Lm name lm)"
+  shows "P c lm"
+proof -
+  have "\<And>p. P c (p \<bullet> lm)"
+    apply(induct lm arbitrary: c rule: lm.induct)
+    apply(simp only: lm.perm)
+    apply(rule a1)
+    apply(simp only: lm.perm)
+    apply(rule a2)
+    apply(blast)[1]
+    apply(assumption)
+    apply(subgoal_tac "\<exists>new::name. (atom new) \<sharp> (c, Lm (p \<bullet> name) (p \<bullet> lm))")
+    defer
+    apply(simp add: fresh_def)
+    apply(rule_tac X="supp (c, Lm (p \<bullet> name) (p \<bullet> lm))" in obtain_at_base)
+    apply(simp add: supp_Pair finite_supp)
+    apply(blast)
+    apply(erule exE)
+    apply(rule_tac t="p \<bullet> Lm name lm" and 
+                   s="(((p \<bullet> name) \<leftrightarrow> new) + p) \<bullet> Lm name lm" in subst)
+    apply(simp del: lm.perm)
+    apply(subst lm.perm)
+    apply(subst (2) lm.perm)
+    apply(rule flip_fresh_fresh)
+    apply(simp add: fresh_def)
+    apply(simp only: supp_fn')
+    apply(simp)
+    apply(simp add: fresh_Pair)
+    apply(simp)
+    apply(rule a3)
+    apply(simp add: fresh_Pair)
+    apply(drule_tac x="((p \<bullet> name) \<leftrightarrow> new) + p" in meta_spec)
+    apply(simp)
+    done
+  then have "P c (0 \<bullet> lm)" by blast
+  then show "P c lm" by simp
+qed
+
+
+lemma
+  fixes c::"'a::fs"
+  assumes a1: "\<And>name c. P c (Vr name)"
+  and     a2: "\<And>lm1 lm2 c. \<lbrakk>\<And>d. P d lm1; \<And>d. P d lm2\<rbrakk> \<Longrightarrow> P c (Ap lm1 lm2)"
+  and     a3: "\<And>name lm c. \<lbrakk>atom name \<sharp> c; \<And>d. P d lm\<rbrakk> \<Longrightarrow> P c (Lm name lm)"
+  shows "P c lm"
+proof -
+  have "\<And>p. P c (p \<bullet> lm)"
+    apply(induct lm arbitrary: c rule: lm.induct)
+    apply(simp only: lm.perm)
+    apply(rule a1)
+    apply(simp only: lm.perm)
+    apply(rule a2)
+    apply(blast)[1]
+    apply(assumption)
+    thm at_set_avoiding
+    apply(subgoal_tac "\<exists>q. (q \<bullet> {p \<bullet> atom name}) \<sharp>* c \<and> supp (p \<bullet> Lm name lm) \<sharp>* q")
+    apply(erule exE)
+    apply(rule_tac t="p \<bullet> Lm name lm" and 
+                   s="q \<bullet> p \<bullet> Lm name lm" in subst)
+    defer
+    apply(simp add: lm.perm)
+    apply(rule a3)
+    apply(simp add: eqvts fresh_star_def)
+    apply(drule_tac x="q + p" in meta_spec)
+    apply(simp)
+    sorry
+  then have "P c (0 \<bullet> lm)" by blast
+  then show "P c lm" by simp
+qed
+
+end
+
+
+
diff -r 2406350c358f -r 8b5a1ad60487 Nominal/ExLeroy.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Nominal/ExLeroy.thy	Tue Mar 23 08:51:43 2010 +0100
@@ -0,0 +1,74 @@
+theory Test
+imports "Parser"
+begin
+
+(* example form Leroy 96 about modules; OTT *)
+
+atom_decl name
+
+ML {* val _ = recursive := false  *}
+nominal_datatype mexp =
+  Acc "path"
+| Stru "body"
+| Funct x::"name" "sexp" m::"mexp"    bind x in m
+| FApp "mexp" "path"
+| Ascr "mexp" "sexp"
+and body =
+  Empty
+| Seq c::defn d::"body"     bind "cbinders c" in d
+and defn =
+  Type "name" "tyty"
+| Dty "name"
+| DStru "name" "mexp"
+| Val "name" "trmtrm"
+and sexp =
+  Sig sbody
+| SFunc "name" "sexp" "sexp"
+and sbody =
+  SEmpty
+| SSeq C::spec D::sbody    bind "Cbinders C" in D
+and spec =
+  Type1 "name"
+| Type2 "name" "tyty"
+| SStru "name" "sexp"
+| SVal "name" "tyty"
+and tyty =
+  Tyref1 "name"
+| Tyref2 "path" "tyty"
+| Fun "tyty" "tyty"
+and path =
+  Sref1 "name"
+| Sref2 "path" "name"
+and trmtrm =
+  Tref1 "name"
+| Tref2 "path" "name"
+| Lam' v::"name" "tyty" M::"trmtrm"  bind v in M
+| App' "trmtrm" "trmtrm"
+| Let' "body" "trmtrm"
+binder
+    cbinders :: "defn \<Rightarrow> atom set"
+and Cbinders :: "spec \<Rightarrow> atom set"
+where
+  "cbinders (Type t T) = {atom t}"
+| "cbinders (Dty t) = {atom t}"
+| "cbinders (DStru x s) = {atom x}"
+| "cbinders (Val v M) = {atom v}"
+| "Cbinders (Type1 t) = {atom t}"
+| "Cbinders (Type2 t T) = {atom t}"
+| "Cbinders (SStru x S) = {atom x}"
+| "Cbinders (SVal v T) = {atom v}"
+
+thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm.fv
+thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm.eq_iff
+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
+thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm.supp
+thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm.fv[simplified mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm.supp]
+
+end
+
+
+
diff -r 2406350c358f -r 8b5a1ad60487 Nominal/ExTySch.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Nominal/ExTySch.thy	Tue Mar 23 08:51:43 2010 +0100
@@ -0,0 +1,166 @@
+theory ExTySch
+imports "Parser"
+begin
+
+(* Type Schemes *)
+atom_decl name
+
+nominal_datatype t =
+  Var "name"
+| Fun "t" "t"
+and tyS =
+  All xs::"name fset" ty::"t" bind xs in ty
+
+lemma size_eqvt_raw:
+  "size (pi \<bullet> t :: t_raw) = size t"
+  "size (pi \<bullet> ts :: tyS_raw) = size ts"
+  apply (induct rule: t_raw_tyS_raw.inducts)
+  apply simp_all
+  done
+
+instantiation t and tyS :: size begin
+
+quotient_definition
+  "size_t :: t \<Rightarrow> nat"
+is
+  "size :: t_raw \<Rightarrow> nat"
+
+quotient_definition
+  "size_tyS :: tyS \<Rightarrow> nat"
+is
+  "size :: tyS_raw \<Rightarrow> nat"
+
+lemma size_rsp:
+  "alpha_t_raw x y \<Longrightarrow> size x = size y"
+  "alpha_tyS_raw a b \<Longrightarrow> size a = size b"
+  apply (induct rule: alpha_t_raw_alpha_tyS_raw.inducts)
+  apply (simp_all only: t_raw_tyS_raw.size)
+  apply (simp_all only: alpha_gen)
+  apply clarify
+  apply (simp_all only: size_eqvt_raw)
+  done
+
+lemma [quot_respect]:
+  "(alpha_t_raw ===> op =) size size"
+  "(alpha_tyS_raw ===> op =) size size"
+  by (simp_all add: size_rsp)
+
+lemma [quot_preserve]:
+  "(rep_t ---> id) size = size"
+  "(rep_tyS ---> id) size = size"
+  by (simp_all add: size_t_def size_tyS_def)
+
+instance
+  by default
+
+end
+
+thm t_raw_tyS_raw.size(4)[quot_lifted]
+thm t_raw_tyS_raw.size(5)[quot_lifted]
+thm t_raw_tyS_raw.size(6)[quot_lifted]
+
+
+thm t_tyS.fv
+thm t_tyS.eq_iff
+thm t_tyS.bn
+thm t_tyS.perm
+thm t_tyS.inducts
+thm t_tyS.distinct
+ML {* Sign.of_sort @{theory} (@{typ t}, @{sort fs}) *}
+
+lemmas t_tyS_supp = t_tyS.fv[simplified t_tyS.supp]
+
+lemma induct:
+  assumes a1: "\<And>name b. P b (Var name)"
+  and     a2: "\<And>t1 t2 b. \<lbrakk>\<And>c. P c t1; \<And>c. P c t2\<rbrakk> \<Longrightarrow> P b (Fun t1 t2)"
+  and     a3: "\<And>fset t b. \<lbrakk>\<And>c. P c t; fset_to_set (fmap atom fset) \<sharp>* b\<rbrakk> \<Longrightarrow> P' b (All fset t)"
+  shows "P (a :: 'a :: pt) t \<and> P' (d :: 'b :: {fs}) ts "
+proof -
+  have " (\<forall>p a. P a (p \<bullet> t)) \<and> (\<forall>p d. P' d (p \<bullet> ts))"
+    apply (rule t_tyS.induct)
+    apply (simp add: a1)
+    apply (simp)
+    apply (rule allI)+
+    apply (rule a2)
+    apply simp
+    apply simp
+    apply (rule allI)
+    apply (rule allI)
+    apply(subgoal_tac "\<exists>pa. ((pa \<bullet> (fset_to_set (fmap atom (p \<bullet> fset)))) \<sharp>* d \<and> supp (p \<bullet> TySch.All fset t) \<sharp>* pa)")
+    apply clarify
+    apply(rule_tac t="p \<bullet> TySch.All fset t" and 
+                   s="pa \<bullet> (p \<bullet> TySch.All fset t)" in subst)
+    apply (rule supp_perm_eq)
+    apply assumption
+    apply (simp only: t_tyS.perm)
+    apply (rule a3)
+    apply(erule_tac x="(pa + p)" in allE)
+    apply simp
+    apply (simp add: eqvts eqvts_raw)
+    apply (rule at_set_avoiding2)
+    apply (simp add: fin_fset_to_set)
+    apply (simp add: finite_supp)
+    apply (simp add: eqvts finite_supp)
+    apply (subst atom_eqvt_raw[symmetric])
+    apply (subst fmap_eqvt[symmetric])
+    apply (subst fset_to_set_eqvt[symmetric])
+    apply (simp only: fresh_star_permute_iff)
+    apply (simp add: fresh_star_def)
+    apply clarify
+    apply (simp add: fresh_def)
+    apply (simp add: t_tyS_supp)
+    done
+  then have "P a (0 \<bullet> t) \<and> P' d (0 \<bullet> ts)" by blast
+  then show ?thesis by simp
+qed
+
+lemma
+  shows "All {|a, b|} (Fun (Var a) (Var b)) = All {|b, a|} (Fun (Var a) (Var b))"
+  apply(simp add: t_tyS.eq_iff)
+  apply(rule_tac x="0::perm" in exI)
+  apply(simp add: alpha_gen)
+  apply(auto)
+  apply(simp add: fresh_star_def fresh_zero_perm)
+  done
+
+lemma
+  shows "All {|a, b|} (Fun (Var a) (Var b)) = All {|a, b|} (Fun (Var b) (Var a))"
+  apply(simp add: t_tyS.eq_iff)
+  apply(rule_tac x="(atom a \<rightleftharpoons> atom b)" in exI)
+  apply(simp add: alpha_gen fresh_star_def eqvts)
+  apply auto
+  done
+
+lemma
+  shows "All {|a, b, c|} (Fun (Var a) (Var b)) = All {|a, b|} (Fun (Var a) (Var b))"
+  apply(simp add: t_tyS.eq_iff)
+  apply(rule_tac x="0::perm" in exI)
+  apply(simp add: alpha_gen fresh_star_def eqvts t_tyS.eq_iff)
+oops
+
+lemma
+  assumes a: "a \<noteq> b"
+  shows "\<not>(All {|a, b|} (Fun (Var a) (Var b)) = All {|c|} (Fun (Var c) (Var c)))"
+  using a
+  apply(simp add: t_tyS.eq_iff)
+  apply(clarify)
+  apply(simp add: alpha_gen fresh_star_def eqvts t_tyS.eq_iff)
+  apply auto
+  done
+
+(* PROBLEM:
+Type schemes with separate datatypes
+
+nominal_datatype T =
+  TVar "name"
+| TFun "T" "T"
+nominal_datatype TyS =
+  TAll xs::"name list" ty::"T" bind xs in ty
+
+*** exception Datatype raised
+*** (line 218 of "/usr/local/src/Isabelle_16-Mar-2010/src/HOL/Tools/Datatype/datatype_aux.ML")
+*** At command "nominal_datatype".
+*)
+
+
+end
diff -r 2406350c358f -r 8b5a1ad60487 Nominal/LamEx.thy
--- a/Nominal/LamEx.thy	Tue Mar 23 08:46:44 2010 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,91 +0,0 @@
-theory LamEx
-imports "Parser" "../Attic/Prove"
-begin
-
-atom_decl name
-
-nominal_datatype lm =
-  Vr "name"
-| Ap "lm" "lm"
-| Lm x::"name" l::"lm"  bind x in l
-
-lemmas supp_fn' = lm.fv[simplified lm.supp]
-
-lemma
-  fixes c::"'a::fs"
-  assumes a1: "\<And>name c. P c (Vr name)"
-  and     a2: "\<And>lm1 lm2 c. \<lbrakk>\<And>d. P d lm1; \<And>d. P d lm2\<rbrakk> \<Longrightarrow> P c (Ap lm1 lm2)"
-  and     a3: "\<And>name lm c. \<lbrakk>atom name \<sharp> c; \<And>d. P d lm\<rbrakk> \<Longrightarrow> P c (Lm name lm)"
-  shows "P c lm"
-proof -
-  have "\<And>p. P c (p \<bullet> lm)"
-    apply(induct lm arbitrary: c rule: lm.induct)
-    apply(simp only: lm.perm)
-    apply(rule a1)
-    apply(simp only: lm.perm)
-    apply(rule a2)
-    apply(blast)[1]
-    apply(assumption)
-    apply(subgoal_tac "\<exists>new::name. (atom new) \<sharp> (c, Lm (p \<bullet> name) (p \<bullet> lm))")
-    defer
-    apply(simp add: fresh_def)
-    apply(rule_tac X="supp (c, Lm (p \<bullet> name) (p \<bullet> lm))" in obtain_at_base)
-    apply(simp add: supp_Pair finite_supp)
-    apply(blast)
-    apply(erule exE)
-    apply(rule_tac t="p \<bullet> Lm name lm" and 
-                   s="(((p \<bullet> name) \<leftrightarrow> new) + p) \<bullet> Lm name lm" in subst)
-    apply(simp del: lm.perm)
-    apply(subst lm.perm)
-    apply(subst (2) lm.perm)
-    apply(rule flip_fresh_fresh)
-    apply(simp add: fresh_def)
-    apply(simp only: supp_fn')
-    apply(simp)
-    apply(simp add: fresh_Pair)
-    apply(simp)
-    apply(rule a3)
-    apply(simp add: fresh_Pair)
-    apply(drule_tac x="((p \<bullet> name) \<leftrightarrow> new) + p" in meta_spec)
-    apply(simp)
-    done
-  then have "P c (0 \<bullet> lm)" by blast
-  then show "P c lm" by simp
-qed
-
-
-lemma
-  fixes c::"'a::fs"
-  assumes a1: "\<And>name c. P c (Vr name)"
-  and     a2: "\<And>lm1 lm2 c. \<lbrakk>\<And>d. P d lm1; \<And>d. P d lm2\<rbrakk> \<Longrightarrow> P c (Ap lm1 lm2)"
-  and     a3: "\<And>name lm c. \<lbrakk>atom name \<sharp> c; \<And>d. P d lm\<rbrakk> \<Longrightarrow> P c (Lm name lm)"
-  shows "P c lm"
-proof -
-  have "\<And>p. P c (p \<bullet> lm)"
-    apply(induct lm arbitrary: c rule: lm.induct)
-    apply(simp only: lm.perm)
-    apply(rule a1)
-    apply(simp only: lm.perm)
-    apply(rule a2)
-    apply(blast)[1]
-    apply(assumption)
-    thm at_set_avoiding
-    apply(subgoal_tac "\<exists>q. (q \<bullet> {p \<bullet> atom name}) \<sharp>* c \<and> supp (p \<bullet> Lm name lm) \<sharp>* q")
-    apply(erule exE)
-    apply(rule_tac t="p \<bullet> Lm name lm" and 
-                   s="q \<bullet> p \<bullet> Lm name lm" in subst)
-    defer
-    apply(simp add: lm.perm)
-    apply(rule a3)
-    apply(simp add: eqvts fresh_star_def)
-    apply(drule_tac x="q + p" in meta_spec)
-    apply(simp)
-    sorry
-  then have "P c (0 \<bullet> lm)" by blast
-  then show "P c lm" by simp
-qed
-
-end
-
-
-
diff -r 2406350c358f -r 8b5a1ad60487 Nominal/Test.thy
--- a/Nominal/Test.thy	Tue Mar 23 08:46:44 2010 +0100
+++ b/Nominal/Test.thy	Tue Mar 23 08:51:43 2010 +0100
@@ -53,69 +53,6 @@
 thm trm5_lts.distinct
 thm trm5_lts.fv[simplified trm5_lts.supp]
 
-(* example form Leroy 96 about modules; OTT *)
-
-nominal_datatype mexp =
-  Acc "path"
-| Stru "body"
-| Funct x::"name" "sexp" m::"mexp"    bind x in m
-| FApp "mexp" "path"
-| Ascr "mexp" "sexp"
-and body =
-  Empty
-| Seq c::defn d::"body"     bind "cbinders c" in d
-and defn =
-  Type "name" "tyty"
-| Dty "name"
-| DStru "name" "mexp"
-| Val "name" "trmtrm"
-and sexp =
-  Sig sbody
-| SFunc "name" "sexp" "sexp"
-and sbody =
-  SEmpty
-| SSeq C::spec D::sbody    bind "Cbinders C" in D
-and spec =
-  Type1 "name"
-| Type2 "name" "tyty"
-| SStru "name" "sexp"
-| SVal "name" "tyty"
-and tyty =
-  Tyref1 "name"
-| Tyref2 "path" "tyty"
-| Fun "tyty" "tyty"
-and path =
-  Sref1 "name"
-| Sref2 "path" "name"
-and trmtrm =
-  Tref1 "name"
-| Tref2 "path" "name"
-| Lam' v::"name" "tyty" M::"trmtrm"  bind v in M
-| App' "trmtrm" "trmtrm"
-| Let' "body" "trmtrm"
-binder
-    cbinders :: "defn \<Rightarrow> atom set"
-and Cbinders :: "spec \<Rightarrow> atom set"
-where
-  "cbinders (Type t T) = {atom t}"
-| "cbinders (Dty t) = {atom t}"
-| "cbinders (DStru x s) = {atom x}"
-| "cbinders (Val v M) = {atom v}"
-| "Cbinders (Type1 t) = {atom t}"
-| "Cbinders (Type2 t T) = {atom t}"
-| "Cbinders (SStru x S) = {atom x}"
-| "Cbinders (SVal v T) = {atom v}"
-
-thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm.fv
-thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm.eq_iff
-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
-thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm.supp
-thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm.fv[simplified mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm.supp]
-
 (* example 3 from Peter Sewell's bestiary *)
 
 nominal_datatype exp =
diff -r 2406350c358f -r 8b5a1ad60487 Nominal/TySch.thy
--- a/Nominal/TySch.thy	Tue Mar 23 08:46:44 2010 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,165 +0,0 @@
-theory TySch
-imports "Parser" "../Attic/Prove" "FSet"
-begin
-
-atom_decl name
-
-nominal_datatype t =
-  Var "name"
-| Fun "t" "t"
-and tyS =
-  All xs::"name fset" ty::"t" bind xs in ty
-
-lemma size_eqvt_raw:
-  "size (pi \<bullet> t :: t_raw) = size t"
-  "size (pi \<bullet> ts :: tyS_raw) = size ts"
-  apply (induct rule: t_raw_tyS_raw.inducts)
-  apply simp_all
-  done
-
-instantiation t and tyS :: size begin
-
-quotient_definition
-  "size_t :: t \<Rightarrow> nat"
-is
-  "size :: t_raw \<Rightarrow> nat"
-
-quotient_definition
-  "size_tyS :: tyS \<Rightarrow> nat"
-is
-  "size :: tyS_raw \<Rightarrow> nat"
-
-lemma size_rsp:
-  "alpha_t_raw x y \<Longrightarrow> size x = size y"
-  "alpha_tyS_raw a b \<Longrightarrow> size a = size b"
-  apply (induct rule: alpha_t_raw_alpha_tyS_raw.inducts)
-  apply (simp_all only: t_raw_tyS_raw.size)
-  apply (simp_all only: alpha_gen)
-  apply clarify
-  apply (simp_all only: size_eqvt_raw)
-  done
-
-lemma [quot_respect]:
-  "(alpha_t_raw ===> op =) size size"
-  "(alpha_tyS_raw ===> op =) size size"
-  by (simp_all add: size_rsp)
-
-lemma [quot_preserve]:
-  "(rep_t ---> id) size = size"
-  "(rep_tyS ---> id) size = size"
-  by (simp_all add: size_t_def size_tyS_def)
-
-instance
-  by default
-
-end
-
-thm t_raw_tyS_raw.size(4)[quot_lifted]
-thm t_raw_tyS_raw.size(5)[quot_lifted]
-thm t_raw_tyS_raw.size(6)[quot_lifted]
-
-
-thm t_tyS.fv
-thm t_tyS.eq_iff
-thm t_tyS.bn
-thm t_tyS.perm
-thm t_tyS.inducts
-thm t_tyS.distinct
-ML {* Sign.of_sort @{theory} (@{typ t}, @{sort fs}) *}
-
-lemmas t_tyS_supp = t_tyS.fv[simplified t_tyS.supp]
-
-lemma induct:
-  assumes a1: "\<And>name b. P b (Var name)"
-  and     a2: "\<And>t1 t2 b. \<lbrakk>\<And>c. P c t1; \<And>c. P c t2\<rbrakk> \<Longrightarrow> P b (Fun t1 t2)"
-  and     a3: "\<And>fset t b. \<lbrakk>\<And>c. P c t; fset_to_set (fmap atom fset) \<sharp>* b\<rbrakk> \<Longrightarrow> P' b (All fset t)"
-  shows "P (a :: 'a :: pt) t \<and> P' (d :: 'b :: {fs}) ts "
-proof -
-  have " (\<forall>p a. P a (p \<bullet> t)) \<and> (\<forall>p d. P' d (p \<bullet> ts))"
-    apply (rule t_tyS.induct)
-    apply (simp add: a1)
-    apply (simp)
-    apply (rule allI)+
-    apply (rule a2)
-    apply simp
-    apply simp
-    apply (rule allI)
-    apply (rule allI)
-    apply(subgoal_tac "\<exists>pa. ((pa \<bullet> (fset_to_set (fmap atom (p \<bullet> fset)))) \<sharp>* d \<and> supp (p \<bullet> TySch.All fset t) \<sharp>* pa)")
-    apply clarify
-    apply(rule_tac t="p \<bullet> TySch.All fset t" and 
-                   s="pa \<bullet> (p \<bullet> TySch.All fset t)" in subst)
-    apply (rule supp_perm_eq)
-    apply assumption
-    apply (simp only: t_tyS.perm)
-    apply (rule a3)
-    apply(erule_tac x="(pa + p)" in allE)
-    apply simp
-    apply (simp add: eqvts eqvts_raw)
-    apply (rule at_set_avoiding2)
-    apply (simp add: fin_fset_to_set)
-    apply (simp add: finite_supp)
-    apply (simp add: eqvts finite_supp)
-    apply (subst atom_eqvt_raw[symmetric])
-    apply (subst fmap_eqvt[symmetric])
-    apply (subst fset_to_set_eqvt[symmetric])
-    apply (simp only: fresh_star_permute_iff)
-    apply (simp add: fresh_star_def)
-    apply clarify
-    apply (simp add: fresh_def)
-    apply (simp add: t_tyS_supp)
-    done
-  then have "P a (0 \<bullet> t) \<and> P' d (0 \<bullet> ts)" by blast
-  then show ?thesis by simp
-qed
-
-lemma
-  shows "All {|a, b|} (Fun (Var a) (Var b)) = All {|b, a|} (Fun (Var a) (Var b))"
-  apply(simp add: t_tyS.eq_iff)
-  apply(rule_tac x="0::perm" in exI)
-  apply(simp add: alpha_gen)
-  apply(auto)
-  apply(simp add: fresh_star_def fresh_zero_perm)
-  done
-
-lemma
-  shows "All {|a, b|} (Fun (Var a) (Var b)) = All {|a, b|} (Fun (Var b) (Var a))"
-  apply(simp add: t_tyS.eq_iff)
-  apply(rule_tac x="(atom a \<rightleftharpoons> atom b)" in exI)
-  apply(simp add: alpha_gen fresh_star_def eqvts)
-  apply auto
-  done
-
-lemma
-  shows "All {|a, b, c|} (Fun (Var a) (Var b)) = All {|a, b|} (Fun (Var a) (Var b))"
-  apply(simp add: t_tyS.eq_iff)
-  apply(rule_tac x="0::perm" in exI)
-  apply(simp add: alpha_gen fresh_star_def eqvts t_tyS.eq_iff)
-oops
-
-lemma
-  assumes a: "a \<noteq> b"
-  shows "\<not>(All {|a, b|} (Fun (Var a) (Var b)) = All {|c|} (Fun (Var c) (Var c)))"
-  using a
-  apply(simp add: t_tyS.eq_iff)
-  apply(clarify)
-  apply(simp add: alpha_gen fresh_star_def eqvts t_tyS.eq_iff)
-  apply auto
-  done
-
-(* PROBLEM:
-Type schemes with separate datatypes
-
-nominal_datatype T =
-  TVar "name"
-| TFun "T" "T"
-nominal_datatype TyS =
-  TAll xs::"name list" ty::"T" bind xs in ty
-
-*** exception Datatype raised
-*** (line 218 of "/usr/local/src/Isabelle_16-Mar-2010/src/HOL/Tools/Datatype/datatype_aux.ML")
-*** At command "nominal_datatype".
-*)
-
-
-end