# HG changeset patch # User Christian Urban # Date 1267713081 -3600 # Node ID cffc5d78ab7f34e35462988fd827fe7d42db2388 # Parent 5b31e49678fc0b45a39ba13f6a29c143b9a761f3 more proofs in Abs and work on Core Haskell diff -r 5b31e49678fc -r cffc5d78ab7f Nominal/Abs.thy --- a/Nominal/Abs.thy Wed Mar 03 19:10:40 2010 +0100 +++ b/Nominal/Abs.thy Thu Mar 04 15:31:21 2010 +0100 @@ -425,7 +425,14 @@ add_perm where "add_perm [] = 0" -| "add_perm ((a,b) # xs) = (a \ b) + add_perm xs" +| "add_perm ((a, b) # xs) = (a \ b) + add_perm xs" + +fun + elem_perm +where + "elem_perm [] = {}" +| "elem_perm ((a, b) # xs) = {a, b} \ elem_perm xs" + lemma add_perm_apend: shows "add_perm (xs @ ys) = add_perm xs + add_perm ys" @@ -433,9 +440,9 @@ apply(auto simp add: add_assoc) done -lemma +lemma perm_list_exists: fixes p::perm - shows "\xs. p = add_perm xs" + shows "\xs. p = add_perm xs \ supp xs \ supp p" apply(induct p taking: "\p::perm. card (supp p)" rule: measure_induct) apply(rename_tac p) apply(case_tac "supp p = {}") @@ -444,7 +451,7 @@ apply(drule perm_zero) apply(simp) apply(rule_tac x="[]" in exI) -apply(simp) +apply(simp add: supp_Nil) apply(subgoal_tac "\x. x \ supp p") defer apply(auto)[1] @@ -455,9 +462,17 @@ apply(erule exE) apply(rule_tac x="xs @ [((- p) \ 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) @@ -465,7 +480,20 @@ apply(subgoal_tac "x \ supp (p + (- p \ x \ x))") apply(blast) apply(simp add: supp_perm) -apply(auto simp add: supp_perm) +defer +apply(auto simp add: supp_perm)[1] +apply(case_tac "x = xa") +apply(simp) +apply(case_tac "((- p) \ 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 \ (- p \ x \ x) \ a \ a} \ {a. p \ a \ a}") +apply(blast) +apply(auto simp add: supp_perm)[1] apply(case_tac "x = xa") apply(simp) apply(case_tac "((- p) \ x) = xa") @@ -477,23 +505,37 @@ apply(simp) done -lemma tt1: - shows "(supp x) \* add_perm xs \ (add_perm xs) \ x = x" +lemma tt0: + fixes p::perm + shows "(supp x) \* p \ \a \ supp p. a \ x" +apply(auto simp add: fresh_star_def supp_perm fresh_def) +done + +lemma uu0: + shows "(\a \ elem_perm xs. a \ x) \ (add_perm xs \ x) = x" apply(induct xs rule: add_perm.induct) apply(simp) -apply(simp) -apply(case_tac "a = b") -apply(simp) -apply(drule meta_mp) -defer -apply(simp) -apply(rule swap_fresh_fresh) -apply(simp add: fresh_def) -apply(auto)[1] -apply(simp add: fresh_star_def fresh_def supp_perm) -apply(drule_tac x="a" in bspec) -apply(simp) -oops +apply(simp add: swap_fresh_fresh) +done + +lemma yy0: + fixes xs::"(atom \ 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) \* p \ p \ x = x" +apply(drule tt0) +apply(subgoal_tac "\xs. p = add_perm xs \ supp xs \ 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: @@ -512,7 +554,7 @@ sorry - +(* lemma tt: "(supp x) \* p \ p \ x = x" apply(induct p rule: perm_induct_test) @@ -539,7 +581,7 @@ apply(simp add: fresh_star_def fresh_def) apply(simp) done - +*) lemma yy: assumes "S1 - {x} = S2 - {x}" "x \ S1" "x \ S2" shows "S1 = S2" @@ -556,7 +598,6 @@ apply(simp) oops -*) fun distinct_perms diff -r 5b31e49678fc -r cffc5d78ab7f Nominal/Test.thy --- a/Nominal/Test.thy Wed Mar 03 19:10:40 2010 +0100 +++ b/Nominal/Test.thy Thu Mar 04 15:31:21 2010 +0100 @@ -340,57 +340,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 \ 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 \ kind_raw) list" "(var \ ty) list" + K "string" "(tvar \ kind) list" "(var \ ty) list" binder bv :: "pat \ atom set" where "bv (K s ts vs) = (atoms (set (map fst ts))) \ (atoms (set (map fst vs)))" -*) (*thm bv_raw.simps*)