# HG changeset patch # User Christian Urban # Date 1273404370 -3600 # Node ID 0854af516f14bc6e6fe626e6db9c6420fb8de188 # Parent 9e7cf0a996d3b6fc8023c223a4e1eba24116e399 cleaned up a bit the examples; added equivariance to all examples diff -r 9e7cf0a996d3 -r 0854af516f14 Nominal/Ex/Ex1rec.thy --- a/Nominal/Ex/Ex1rec.thy Sun May 09 11:43:24 2010 +0100 +++ b/Nominal/Ex/Ex1rec.thy Sun May 09 12:26:10 2010 +0100 @@ -29,10 +29,11 @@ ML {* Sign.of_sort @{theory} (@{typ lam}, @{sort fs}) *} thm lam_bp.fv[simplified lam_bp.supp(1-2)] -(*declare permute_lam_raw_permute_bp_raw.simps[eqvt] +declare permute_lam_raw_permute_bp_raw.simps[eqvt] declare alpha_gen_eqvt[eqvt] + equivariance alpha_lam_raw -*) + end diff -r 9e7cf0a996d3 -r 0854af516f14 Nominal/Ex/Ex2.thy --- a/Nominal/Ex/Ex2.thy Sun May 09 11:43:24 2010 +0100 +++ b/Nominal/Ex/Ex2.thy Sun May 09 12:26:10 2010 +0100 @@ -27,6 +27,12 @@ thm trm_pat.distinct thm trm_pat.fv[simplified trm_pat.supp(1-2)] +declare permute_trm_raw_permute_pat_raw.simps[eqvt] +declare alpha_gen_eqvt[eqvt] + +equivariance alpha_trm_raw + + end diff -r 9e7cf0a996d3 -r 0854af516f14 Nominal/Ex/Ex3.thy --- a/Nominal/Ex/Ex3.thy Sun May 09 11:43:24 2010 +0100 +++ b/Nominal/Ex/Ex3.thy Sun May 09 12:26:10 2010 +0100 @@ -30,6 +30,13 @@ thm trm_pat.distinct thm trm_pat.fv[simplified trm_pat.supp(1-2)] + +declare permute_trm_raw_permute_pat_raw.simps[eqvt] +declare alpha_gen_eqvt[eqvt] + +equivariance alpha_trm_raw + + end diff -r 9e7cf0a996d3 -r 0854af516f14 Nominal/Ex/ExLF.thy --- a/Nominal/Ex/ExLF.thy Sun May 09 11:43:24 2010 +0100 +++ b/Nominal/Ex/ExLF.thy Sun May 09 12:26:10 2010 +0100 @@ -20,6 +20,14 @@ thm kind_ty_trm.supp +declare permute_kind_raw_permute_ty_raw_permute_trm_raw.simps[eqvt] +declare alpha_gen_eqvt[eqvt] + +equivariance alpha_trm_raw + + + + end diff -r 9e7cf0a996d3 -r 0854af516f14 Nominal/Ex/ExLeroy.thy --- a/Nominal/Ex/ExLeroy.thy Sun May 09 11:43:24 2010 +0100 +++ b/Nominal/Ex/ExLeroy.thy Sun May 09 12:26:10 2010 +0100 @@ -16,10 +16,10 @@ Empty | Seq c::defn d::"body" bind_set "cbinders c" in d and defn = - Type "name" "tyty" + Type "name" "ty" | Dty "name" | DStru "name" "mexp" -| Val "name" "trmtrm" +| Val "name" "trm" and sexp = Sig sbody | SFunc "name" "sexp" "sexp" @@ -28,22 +28,22 @@ | SSeq C::spec D::sbody bind_set "Cbinders C" in D and spec = Type1 "name" -| Type2 "name" "tyty" +| Type2 "name" "ty" | SStru "name" "sexp" -| SVal "name" "tyty" -and tyty = +| SVal "name" "ty" +and ty = Tyref1 "name" -| Tyref2 "path" "tyty" -| Fun "tyty" "tyty" +| Tyref2 "path" "ty" +| Fun "ty" "ty" and path = Sref1 "name" | Sref2 "path" "name" -and trmtrm = +and trm = Tref1 "name" | Tref2 "path" "name" -| Lam' v::"name" "tyty" M::"trmtrm" bind_set v in M -| App' "trmtrm" "trmtrm" -| Let' "body" "trmtrm" +| Lam' v::"name" "ty" M::"trm" bind_set v in M +| App' "trm" "trm" +| Let' "body" "trm" binder cbinders :: "defn \ atom set" and Cbinders :: "spec \ atom set" @@ -57,15 +57,21 @@ | "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(1-3,5-7,9-10) -thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm.fv[simplified mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm.supp(1-3,5-7,9-10)] +thm mexp_body_defn_sexp_sbody_spec_ty_path_trm.fv +thm mexp_body_defn_sexp_sbody_spec_ty_path_trm.eq_iff +thm mexp_body_defn_sexp_sbody_spec_ty_path_trm.bn +thm mexp_body_defn_sexp_sbody_spec_ty_path_trm.perm +thm mexp_body_defn_sexp_sbody_spec_ty_path_trm.induct +thm mexp_body_defn_sexp_sbody_spec_ty_path_trm.inducts +thm mexp_body_defn_sexp_sbody_spec_ty_path_trm.distinct +thm mexp_body_defn_sexp_sbody_spec_ty_path_trm.supp(1-3,5-7,9-10) +thm mexp_body_defn_sexp_sbody_spec_ty_path_trm.fv[simplified mexp_body_defn_sexp_sbody_spec_ty_path_trm.supp(1-3,5-7,9-10)] + +declare permute_mexp_raw_permute_body_raw_permute_defn_raw_permute_sexp_raw_permute_sbody_raw_permute_spec_raw_permute_ty_raw_permute_path_raw_permute_trm_raw.simps[eqvt] +declare alpha_gen_eqvt[eqvt] + +equivariance alpha_trm_raw + end diff -r 9e7cf0a996d3 -r 0854af516f14 Nominal/Ex/ExLet.thy --- a/Nominal/Ex/ExLet.thy Sun May 09 11:43:24 2010 +0100 +++ b/Nominal/Ex/ExLet.thy Sun May 09 12:26:10 2010 +0100 @@ -35,6 +35,13 @@ thm trm_lts.fv[simplified trm_lts.supp(1-2)] +declare permute_trm_raw_permute_lts_raw.simps[eqvt] +declare alpha_gen_eqvt[eqvt] + +equivariance alpha_trm_raw + + + primrec permute_bn_raw where @@ -95,14 +102,14 @@ apply (rule_tac x="q" in exI) apply (simp add: alphas) apply (simp add: perm_bn[symmetric]) - apply (simp add: eqvts[symmetric]) - apply (simp add: supp_abs) + apply(rule conjI) + apply(drule supp_perm_eq) + apply(simp add: abs_eq_iff) + apply(simp add: alphas_abs alphas) + apply(drule conjunct1) apply (simp add: trm_lts.supp) - apply (rule supp_perm_eq[symmetric]) - apply (subst supp_finite_atom_set) - apply (rule finite_Diff) - apply (simp add: finite_supp) - apply (assumption) + apply(simp add: supp_abs) + apply (simp add: trm_lts.supp) done diff -r 9e7cf0a996d3 -r 0854af516f14 Nominal/Ex/ExLetMult.thy --- a/Nominal/Ex/ExLetMult.thy Sun May 09 11:43:24 2010 +0100 +++ b/Nominal/Ex/ExLetMult.thy Sun May 09 12:26:10 2010 +0100 @@ -22,6 +22,12 @@ thm trm_lts.induct thm trm_lts.fv[simplified trm_lts.supp] +declare permute_trm_raw_permute_lts_raw.simps[eqvt] +declare alpha_gen_eqvt[eqvt] + +equivariance alpha_trm_raw + + end diff -r 9e7cf0a996d3 -r 0854af516f14 Nominal/Ex/ExLetRec.thy --- a/Nominal/Ex/ExLetRec.thy Sun May 09 11:43:24 2010 +0100 +++ b/Nominal/Ex/ExLetRec.thy Sun May 09 12:26:10 2010 +0100 @@ -30,6 +30,11 @@ thm trm_lts.supp thm trm_lts.fv[simplified trm_lts.supp] +declare permute_trm_raw_permute_lts_raw.simps[eqvt] +declare alpha_gen_eqvt[eqvt] + +equivariance alpha_trm_raw + (* why is this not in HOL simpset? *) lemma set_sub: "{a, b} - {b} = {a} - {b}" by auto diff -r 9e7cf0a996d3 -r 0854af516f14 Nominal/Ex/ExNotRsp.thy --- a/Nominal/Ex/ExNotRsp.thy Sun May 09 11:43:24 2010 +0100 +++ b/Nominal/Ex/ExNotRsp.thy Sun May 09 12:26:10 2010 +0100 @@ -1,46 +1,52 @@ theory ExNotRsp -imports "../Parser" +imports "../NewParser" begin atom_decl name -(* example 6 from Terms.thy *) - -nominal_datatype trm6 = - Vr6 "name" -| Lm6 x::"name" t::"trm6" bind x in t -| Lt6 left::"trm6" right::"trm6" bind "bv6 left" in right +(* this example binds bound names and + so is not respectful *) +(* +nominal_datatype trm = + Vr "name" +| Lm x::"name" t::"trm" bind x in t +| Lt left::"trm" right::"trm" bind "bv left" in right binder - bv6 + bv where - "bv6 (Vr6 n) = {}" -| "bv6 (Lm6 n t) = {atom n} \ bv6 t" -| "bv6 (Lt6 l r) = bv6 l \ bv6 r" - -(* example 7 from Terms.thy *) -nominal_datatype trm7 = - Vr7 "name" -| Lm7 l::"name" r::"trm7" bind l in r -| Lt7 l::"trm7" r::"trm7" bind "bv7 l" in r -binder - bv7 -where - "bv7 (Vr7 n) = {atom n}" -| "bv7 (Lm7 n t) = bv7 t - {atom n}" -| "bv7 (Lt7 l r) = bv7 l \ bv7 r" + "bv (Vr n) = {}" +| "bv (Lm n t) = {atom n} \ bv t" +| "bv (Lt l r) = bv l \ bv r" *) -(* example 9 from Terms.thy *) -nominal_datatype lam9 = - Var9 "name" -| Lam9 n::"name" l::"lam9" bind n in l -and bla9 = - Bla9 f::"lam9" s::"lam9" bind "bv9 f" in s +(* this example uses "-" in the binding function; + at the moment this is unsupported *) +(* +nominal_datatype trm' = + Vr' "name" +| Lm' l::"name" r::"trm'" bind l in r +| Lt' l::"trm'" r::"trm'" bind "bv' l" in r binder - bv9 + bv' where - "bv9 (Var9 x) = {}" -| "bv9 (Lam9 x b) = {atom x}" + "bv' (Vr' n) = {atom n}" +| "bv' (Lm' n t) = bv' t - {atom n}" +| "bv' (Lt' l r) = bv' l \ bv' r" +*) + +(* this example again binds bound names *) +(* +nominal_datatype trm'' = + Va'' "name" +| Lm'' n::"name" l::"trm''" bind n in l +and bla'' = + Bla'' f::"trm''" s::"trm''" bind "bv'' f" in s +binder + bv'' +where + "bv'' (Vm'' x) = {}" +| "bv'' (Lm'' x b) = {atom x}" +*) end diff -r 9e7cf0a996d3 -r 0854af516f14 Nominal/Ex/ExPS3.thy --- a/Nominal/Ex/ExPS3.thy Sun May 09 11:43:24 2010 +0100 +++ b/Nominal/Ex/ExPS3.thy Sun May 09 12:26:10 2010 +0100 @@ -11,29 +11,35 @@ ML {* val _ = cheat_alpha_bn_rsp := true *} nominal_datatype exp = - VarP "name" -| AppP "exp" "exp" -| LamP x::"name" e::"exp" bind_set x in e -| LetP x::"name" p::"pat3" e1::"exp" e2::"exp" bind_set x in e2, bind_set "bp p" in e1 -and pat3 = + Var "name" +| App "exp" "exp" +| Lam x::"name" e::"exp" bind_set x in e +| Let x::"name" p::"pat" e1::"exp" e2::"exp" bind_set x in e2, bind_set "bp p" in e1 +and pat = PVar "name" | PUnit -| PPair "pat3" "pat3" +| PPair "pat" "pat" binder - bp :: "pat3 \ atom set" + bp :: "pat \ atom set" where "bp (PVar x) = {atom x}" | "bp (PUnit) = {}" | "bp (PPair p1 p2) = bp p1 \ bp p2" -thm exp_pat3.fv -thm exp_pat3.eq_iff -thm exp_pat3.bn -thm exp_pat3.perm -thm exp_pat3.induct -thm exp_pat3.distinct -thm exp_pat3.fv -thm exp_pat3.supp(1-2) +thm exp_pat.fv +thm exp_pat.eq_iff +thm exp_pat.bn +thm exp_pat.perm +thm exp_pat.induct +thm exp_pat.distinct +thm exp_pat.fv +thm exp_pat.supp(1-2) + +declare permute_exp_raw_permute_pat_raw.simps[eqvt] +declare alpha_gen_eqvt[eqvt] + +equivariance alpha_exp_raw + end diff -r 9e7cf0a996d3 -r 0854af516f14 Nominal/Ex/ExPS6.thy --- a/Nominal/Ex/ExPS6.thy Sun May 09 11:43:24 2010 +0100 +++ b/Nominal/Ex/ExPS6.thy Sun May 09 12:26:10 2010 +0100 @@ -1,37 +1,42 @@ theory ExPS6 -imports "../Parser" +imports "../NewParser" begin (* example 6 from Peter Sewell's bestiary *) atom_decl name -(* The binding structure is too complicated, so equivalence the - way we define it is not true *) +(* Is this binding structure supported - I think not + because e1 occurs twice as body *) -ML {* val _ = recursive := false *} -nominal_datatype exp6 = - EVar name -| EPair exp6 exp6 -| ELetRec x::name p::pat6 e1::exp6 e2::exp6 bind x in e1, bind x in e2, bind "bp6 p" in e1 -and pat6 = - PVar' name -| PUnit' -| PPair' pat6 pat6 +nominal_datatype exp = + Var name +| Pair exp exp +| LetRec x::name p::pat e1::exp e2::exp bind x in e1 e2, bind "bp p" in e1 +and pat = + PVar name +| PUnit +| PPair pat pat binder - bp6 :: "pat6 \ atom set" + bp :: "pat \ atom list" where - "bp6 (PVar' x) = {atom x}" -| "bp6 (PUnit') = {}" -| "bp6 (PPair' p1 p2) = bp6 p1 \ bp6 p2" + "bp (PVar x) = [atom x]" +| "bp (PUnit) = []" +| "bp (PPair p1 p2) = bp p1 @ bp p2" -thm exp6_pat6.fv -thm exp6_pat6.eq_iff -thm exp6_pat6.bn -thm exp6_pat6.perm -thm exp6_pat6.induct -thm exp6_pat6.distinct -thm exp6_pat6.supp +thm exp_pat.fv +thm exp_pat.eq_iff +thm exp_pat.bn +thm exp_pat.perm +thm exp_pat.induct +thm exp_pat.distinct +thm exp_pat.supp + +declare permute_exp_raw_permute_pat_raw.simps[eqvt] +declare alpha_gen_eqvt[eqvt] + +equivariance alpha_exp_raw + end diff -r 9e7cf0a996d3 -r 0854af516f14 Nominal/Ex/ExPS7.thy --- a/Nominal/Ex/ExPS7.thy Sun May 09 11:43:24 2010 +0100 +++ b/Nominal/Ex/ExPS7.thy Sun May 09 12:26:10 2010 +0100 @@ -1,3 +1,4 @@ + theory ExPS7 imports "../NewParser" begin @@ -6,25 +7,31 @@ atom_decl name -nominal_datatype exp7 = - EVar name -| EUnit -| EPair exp7 exp7 -| ELetRec l::"lrbs" e::"exp7" bind_set "b7s l" in l e +nominal_datatype exp = + Var name +| Unit +| Pair exp exp +| LetRec l::"lrbs" e::"exp" bind_set "bs l" in l e and lrb = - Assign name exp7 + Assign name exp and lrbs = Single lrb | More lrb lrbs binder - b7 :: "lrb \ atom set" and - b7s :: "lrbs \ atom set" + b :: "lrb \ atom set" and + bs :: "lrbs \ atom set" where - "b7 (Assign x e) = {atom x}" -| "b7s (Single a) = b7 a" -| "b7s (More a as) = (b7 a) \ (b7s as)" -thm exp7_lrb_lrbs.eq_iff -thm exp7_lrb_lrbs.supp + "b (Assign x e) = {atom x}" +| "bs (Single a) = b a" +| "bs (More a as) = (b a) \ (bs as)" + +thm exp_lrb_lrbs.eq_iff +thm exp_lrb_lrbs.supp + +declare permute_exp_raw_permute_lrb_raw_permute_lrbs_raw.simps[eqvt] +declare alpha_gen_eqvt[eqvt] + +equivariance alpha_exp_raw end diff -r 9e7cf0a996d3 -r 0854af516f14 Nominal/Ex/ExPS8.thy --- a/Nominal/Ex/ExPS8.thy Sun May 09 11:43:24 2010 +0100 +++ b/Nominal/Ex/ExPS8.thy Sun May 09 12:26:10 2010 +0100 @@ -48,6 +48,11 @@ thm exp_fnclause_fnclauses_lrb_lrbs_pat.fv thm exp_fnclause_fnclauses_lrb_lrbs_pat.eq_iff + +declare permute_exp_raw_permute_fnclause_raw_permute_fnclauses_raw_permute_lrb_raw_permute_lrbs_raw_permute_pat_raw.simps[eqvt] +declare alpha_gen_eqvt[eqvt] + +equivariance alpha_exp_raw end diff -r 9e7cf0a996d3 -r 0854af516f14 Nominal/Ex/Lambda.thy --- a/Nominal/Ex/Lambda.thy Sun May 09 11:43:24 2010 +0100 +++ b/Nominal/Ex/Lambda.thy Sun May 09 12:26:10 2010 +0100 @@ -15,6 +15,10 @@ declare lam.perm[eqvt] +declare permute_lam_raw.simps[eqvt] +declare alpha_gen_eqvt[eqvt] +equivariance alpha_lam_raw + section {* Strong Induction Principles*} (* diff -r 9e7cf0a996d3 -r 0854af516f14 Nominal/Ex/Term8.thy --- a/Nominal/Ex/Term8.thy Sun May 09 11:43:24 2010 +0100 +++ b/Nominal/Ex/Term8.thy Sun May 09 12:26:10 2010 +0100 @@ -2,22 +2,27 @@ imports "../NewParser" begin -(* example 8 from Terms.thy *) +(* example 8 *) atom_decl name +(* this should work but gives an error at the moment: + seems like in the symmetry proof +*) + nominal_datatype foo = Foo0 "name" | Foo1 b::"bar" f::"foo" bind_set "bv b" in f and bar = Bar0 "name" -| Bar1 "name" s::"name" b::"bar" bind_set s in b +| Bar1 "name" s::"name" b::"bar" bind s in b binder bv where "bv (Bar0 x) = {}" | "bv (Bar1 v x b) = {atom v}" + end diff -r 9e7cf0a996d3 -r 0854af516f14 Nominal/Ex/TestMorePerm.thy --- a/Nominal/Ex/TestMorePerm.thy Sun May 09 11:43:24 2010 +0100 +++ b/Nominal/Ex/TestMorePerm.thy Sun May 09 12:26:10 2010 +0100 @@ -1,35 +1,35 @@ theory TestMorePerm -imports "../Parser" +imports "../NewParser" begin text {* "Weirdo" example from Peter Sewell's bestiary. - In case of deep binders, it is not coverd by our - approach of defining alpha-equivalence with a - single permutation. - - Check whether it works with shallow binders as - defined below. + This example is not covered by our binding + specification. *} ML {* val _ = cheat_equivp := true *} atom_decl name -nominal_datatype foo = +nominal_datatype weird = Foo_var "name" -| Foo_pair "foo" "foo" -| Foo x::"name" y::"name" p1::"foo" p2::"foo" p3::"foo" - bind x in p1, bind x in p2, - bind y in p2, bind y in p3 +| Foo_pair "weird" "weird" +| Foo x::"name" y::"name" p1::"weird" p2::"weird" p3::"weird" + bind x in p1 p2, + bind y in p2 p3 -thm alpha_foo_raw.intros[no_vars] +thm alpha_weird_raw.intros[no_vars] thm permute_weird_raw.simps[no_vars] thm alpha_weird_raw.intros[no_vars] thm fv_weird_raw.simps[no_vars] +declare permute_weird_raw.simps[eqvt] +declare alpha_gen_eqvt[eqvt] +equivariance alpha_weird_raw + end diff -r 9e7cf0a996d3 -r 0854af516f14 Nominal/Ex/TypeSchemes.thy --- a/Nominal/Ex/TypeSchemes.thy Sun May 09 11:43:24 2010 +0100 +++ b/Nominal/Ex/TypeSchemes.thy Sun May 09 12:26:10 2010 +0100 @@ -14,6 +14,11 @@ lemmas ty_tys_supp = ty_tys.fv[simplified ty_tys.supp] +declare permute_ty_raw_permute_tys_raw.simps[eqvt] +declare alpha_gen_eqvt[eqvt] +equivariance alpha_ty_raw + + (* below we define manually the function for size *) lemma size_eqvt_raw: