# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1267714618 -3600
# Node ID 3727e234fe6b9175ddb9e331ffcd1d030aa538d0
# Parent  cad5f385156937801b51f471dbd9d441d404994d# Parent  c25f797c7e6ec9db7ed98729256bf900514db490
merged

diff -r c25f797c7e6e -r 3727e234fe6b Nominal/Abs.thy
--- a/Nominal/Abs.thy	Thu Mar 04 15:55:53 2010 +0100
+++ b/Nominal/Abs.thy	Thu Mar 04 15:56:58 2010 +0100
@@ -415,48 +415,146 @@
 apply(simp add: supp_swap)
 done
 
+lemma perm_zero:
+  assumes a: "\<forall>x::atom. p \<bullet> x = x"
+  shows "p = 0"
+using a
+by (simp add: expand_perm_eq)
 
-thm supp_perm
+fun
+  add_perm 
+where
+  "add_perm [] = 0"
+| "add_perm ((a, b) # xs) = (a \<rightleftharpoons> b) + add_perm xs"
+
+fun
+  elem_perm
+where
+  "elem_perm [] = {}"
+| "elem_perm ((a, b) # xs) = {a, b} \<union> elem_perm xs"
+
+
+lemma add_perm_apend:
+  shows "add_perm (xs @ ys) = add_perm xs + add_perm ys"
+apply(induct xs arbitrary: ys)
+apply(auto simp add: add_assoc)
+done
 
-(* 
-lemma perm_induct_test:
-  fixes P :: "perm => bool"
-  assumes zero: "P 0"
-  assumes swap: "\<And>a b. \<lbrakk>sort_of a = sort_of b; a \<noteq> b\<rbrakk> \<Longrightarrow> P (a \<rightleftharpoons> b)"
-  assumes plus: "\<And>p1 p2. \<lbrakk>supp (p1 + p2) = (supp p1 \<union> supp p2); P p1; P p2\<rbrakk> \<Longrightarrow> P (p1 + p2)"
-  shows "P p"
-sorry
-
-lemma tt1:
-  assumes a: "finite (supp p)"
-  shows "(supp x) \<sharp>* p \<Longrightarrow> p \<bullet> x = x"
-using a
-unfolding fresh_star_def fresh_def
-apply(induct F\<equiv>"supp p" arbitrary: p rule: finite.induct)
+lemma perm_list_exists:
+  fixes p::perm
+  shows "\<exists>xs. p = add_perm xs \<and> supp xs \<subseteq> supp p"
+apply(induct p taking: "\<lambda>p::perm. card (supp p)" rule: measure_induct)
+apply(rename_tac p)
+apply(case_tac "supp p = {}")
+apply(simp)
+apply(simp add: supp_perm)
+apply(drule perm_zero)
+apply(simp)
+apply(rule_tac x="[]" in exI)
+apply(simp add: supp_Nil)
+apply(subgoal_tac "\<exists>x. x \<in> supp p")
+defer
+apply(auto)[1]
+apply(erule exE)
+apply(drule_tac x="p + (((- p) \<bullet> x) \<rightleftharpoons> x)" in spec)
+apply(drule mp)
+defer
+apply(erule exE)
+apply(rule_tac x="xs @ [((- p) \<bullet> x, x)]" in exI)
+apply(simp add: add_perm_apend)
+apply(erule conjE)
+apply(drule sym)
+apply(simp)
+apply(simp add: expand_perm_eq)
+apply(simp add: supp_append)
+apply(simp add: supp_perm supp_Cons supp_Nil supp_Pair supp_atom)
+apply(rule conjI)
+prefer 2
+apply(auto)[1]
+apply (metis left_minus minus_unique permute_atom_def_raw permute_minus_cancel(2))
+defer
+apply(rule psubset_card_mono)
+apply(simp add: finite_supp)
+apply(rule psubsetI)
+defer
+apply(subgoal_tac "x \<notin> supp (p + (- p \<bullet> x \<rightleftharpoons> x))")
+apply(blast)
 apply(simp add: supp_perm)
 defer
-apply(case_tac "a \<in> A")
-apply(simp add: insert_absorb)
-apply(subgoal_tac "A = supp p - {a}")
-prefer 2
+apply(auto simp add: supp_perm)[1]
+apply(case_tac "x = xa")
+apply(simp)
+apply(case_tac "((- p) \<bullet> x) = xa")
+apply(simp)
+apply(case_tac "sort_of xa = sort_of x")
+apply(simp)
+apply(auto)[1]
+apply(simp)
+apply(simp)
+apply(subgoal_tac "{a. p \<bullet> (- p \<bullet> x \<rightleftharpoons> x) \<bullet> a \<noteq> a} \<subseteq> {a. p \<bullet> a \<noteq> a}")
 apply(blast)
-apply(case_tac "p \<bullet> a = a")
-apply(simp add: supp_perm)
-apply(drule_tac x="p + (((- p) \<bullet> a) \<rightleftharpoons> a)" in meta_spec)
+apply(auto simp add: supp_perm)[1]
+apply(case_tac "x = xa")
+apply(simp)
+apply(case_tac "((- p) \<bullet> x) = xa")
+apply(simp)
+apply(case_tac "sort_of xa = sort_of x")
+apply(simp)
+apply(auto)[1]
+apply(simp)
+apply(simp)
+done
+
+lemma tt0:
+  fixes p::perm
+  shows "(supp x) \<sharp>* p \<Longrightarrow> \<forall>a \<in> supp p. a \<sharp> x"
+apply(auto simp add: fresh_star_def supp_perm fresh_def)
+done
+
+lemma uu0:
+  shows "(\<forall>a \<in> elem_perm xs. a \<sharp> x) \<Longrightarrow> (add_perm xs \<bullet> x) = x"
+apply(induct xs rule: add_perm.induct)
 apply(simp)
-apply(drule meta_mp)
-apply(rule subset_antisym)
-apply(rule subsetI)
-apply(simp)
+apply(simp add: swap_fresh_fresh)
+done
+
+lemma yy0:
+  fixes xs::"(atom \<times> atom) list"
+  shows "supp xs = elem_perm xs"
+apply(induct xs rule: elem_perm.induct)
+apply(auto simp add: supp_Nil supp_Cons supp_Pair supp_atom)
+done
+
+lemma tt1:
+  shows "(supp x) \<sharp>* p \<Longrightarrow> p \<bullet> x = x"
+apply(drule tt0)
+apply(subgoal_tac "\<exists>xs. p = add_perm xs \<and> supp xs \<subseteq> supp p")
+prefer 2
+apply(rule perm_list_exists)
+apply(erule exE)
+apply(simp only: yy0)
+apply(rule uu0)
+apply(auto)
+done
+
+
+lemma perm_induct_test:
+  fixes P :: "perm => bool"
+  assumes fin: "finite (supp p)" 
+  assumes zero: "P 0"
+  assumes swap: "\<And>a b. \<lbrakk>sort_of a = sort_of b; a \<noteq> b\<rbrakk> \<Longrightarrow> P (a \<rightleftharpoons> b)"
+  assumes plus: "\<And>p1 p2. \<lbrakk>supp p1 \<inter> supp p2 = {}; P p1; P p2\<rbrakk> \<Longrightarrow> P (p1 + p2)"
+  shows "P p"
+using fin
+apply(induct F\<equiv>"supp p" arbitrary: p rule: finite_induct)
 apply(simp add: supp_perm)
-apply(case_tac "xa = p \<bullet> a")
-apply(simp)
-apply(case_tac "p \<bullet> a = (- p) \<bullet> a")
-apply(simp)
-defer
-apply(simp)
-oops
+apply(drule perm_zero)
+apply(simp add: zero)
+apply(rotate_tac 3)
+sorry
 
+
+(*
 lemma tt:
   "(supp x) \<sharp>* p \<Longrightarrow> p \<bullet> x = x"
 apply(induct p rule: perm_induct_test)
@@ -483,7 +581,7 @@
 apply(simp add: fresh_star_def fresh_def)
 apply(simp)
 done
-
+*)
 lemma yy:
   assumes "S1 - {x} = S2 - {x}" "x \<in> S1" "x \<in> S2"
   shows "S1 = S2"
@@ -500,7 +598,6 @@
 apply(simp)
 oops
 
-*)
 
 fun
   distinct_perms 
diff -r c25f797c7e6e -r 3727e234fe6b Nominal/Test.thy
--- a/Nominal/Test.thy	Thu Mar 04 15:55:53 2010 +0100
+++ b/Nominal/Test.thy	Thu Mar 04 15:56:58 2010 +0100
@@ -425,57 +425,60 @@
 
 atom_decl var
 atom_decl tvar
-atom_decl co
 
-datatype sort = 
-  TY tvar
-| CO co
-
-nominal_datatype kind = 
-  KStar
-| KFun kind kind
-| KEq kind kind
 
 (* there are types, coercion types and regular types *)
-(*
-nominal_datatype ty =
-  TVar tvar
-| TFun string "ty list"
-| TAll tvar kind_raw ty --"some binding"
-| TSym ty
-| TCir ty ty
-| TApp ty ty
-| TLeft ty
-| TRight ty
-| TEq ty
-| TRightc ty
-| TLeftc ty
-| TCoe ty ty
-*)
+nominal_datatype tkind = 
+  KStar
+| KFun "tkind" "tkind"
+and ckind =
+  CKEq "ty" "ty" 
+and ty =
+  TVar "tvar"
+| TC "string"
+| TApp "ty" "ty"
+| TFun "string" "ty list"
+| TAll tv::"tvar" "tkind" T::"ty"  bind tv in T
+| TEq "ty" "ty" "ty"
+and co =
+  CC "string"
+| CApp "co" "co"
+| CFun "string" "co list"
+| CAll tv::"tvar" "ckind" C::"co"  bind tv in C
+| CEq "co" "co" "co"
+| CSym "co"
+| CCir "co" "co"
+| CLeft "co"
+| CRight "co"
+| CSim "co"
+| CRightc "co"
+| CLeftc "co"
+| CCoe "co" "co"
+
+
 typedecl ty --"hack since ty is not yet defined"
 
 abbreviation 
   "atoms A \<equiv> atom ` A"
 
-(* does not work yet
 nominal_datatype trm =
-  Var var
-| LAM tv::tvar kind_raw t::trm   bind tv in t 
-| APP trm ty
-| Lam v::var ty t::trm       bind v in t
-| App trm trm
-| Let x::var ty trm t::trm   bind x in t
-| Case trm "assoc list"
-| Cast trm ty   --"ty is supposed to be a coercion type only"
+  Var "var"
+| C "string"
+| LAM tv::"tvar" "kind" t::"trm"   bind tv in t 
+| APP "trm" "ty"
+| Lam v::"var" "ty" t::"trm"       bind v in t
+| App "trm" "trm"
+| Let x::"var" "ty" "trm" t::"trm" bind x in t
+| Case "trm" "assoc list"
+| Cast "trm" "ty"                   --"ty is supposed to be a coercion type only"
 and assoc = 
-  A p::pat t::trm bind "bv p" in t 
+  A p::"pat" t::"trm" bind "bv p" in t 
 and pat = 
-  K string "(tvar \<times> kind_raw) list" "(var \<times> ty) list"
+  K "string" "(tvar \<times> kind) list" "(var \<times> ty) list"
 binder
  bv :: "pat \<Rightarrow> atom set"
 where
  "bv (K s ts vs) = (atoms (set (map fst ts))) \<union> (atoms (set (map fst vs)))"
-*)
 
 (*thm bv_raw.simps*)