# HG changeset patch # User Cezary Kaliszyk # Date 1269329628 -3600 # Node ID aeed597d20437207847e4ed4f20b56568ba28454 # Parent 892fcdb96c960ef475499b5d45c438a31fe8a689 Move examples which create more permutations out diff -r 892fcdb96c96 -r aeed597d2043 Nominal/LFex.thy --- a/Nominal/LFex.thy Tue Mar 23 08:22:48 2010 +0100 +++ b/Nominal/LFex.thy Tue Mar 23 08:33:48 2010 +0100 @@ -5,8 +5,6 @@ atom_decl name atom_decl ident -ML {* val _ = cheat_equivp := false *} - nominal_datatype kind = Type | KPi "ty" n::"name" k::"kind" bind n in k diff -r 892fcdb96c96 -r aeed597d2043 Nominal/Parser.thy --- a/Nominal/Parser.thy Tue Mar 23 08:22:48 2010 +0100 +++ b/Nominal/Parser.thy Tue Mar 23 08:33:48 2010 +0100 @@ -265,7 +265,8 @@ end *} -ML {* val cheat_equivp = Unsynchronized.ref true *} +(* This one is not needed for the proper examples *) +ML {* val cheat_equivp = Unsynchronized.ref false *} (* These 4 are not needed any more *) ML {* val cheat_fv_rsp = Unsynchronized.ref false *} diff -r 892fcdb96c96 -r aeed597d2043 Nominal/Test.thy --- a/Nominal/Test.thy Tue Mar 23 08:22:48 2010 +0100 +++ b/Nominal/Test.thy Tue Mar 23 08:33:48 2010 +0100 @@ -108,30 +108,8 @@ thm trm0_pat0.distinct thm trm0_pat0.fv[simplified trm0_pat0.supp,no_vars] -text {* example type schemes *} - -nominal_datatype t = - VarTS "name" -| FunTS "t" "t" -and tyS = - All xs::"name fset" ty::"t" bind xs in ty - -thm t_tyS.fv -thm t_tyS.eq_iff -thm t_tyS.bn -thm t_tyS.perm -thm t_tyS.induct -thm t_tyS.distinct -thm t_tyS.fv[simplified t_tyS.supp] - -ML {* Sign.of_sort @{theory} (@{typ t}, @{sort fs}) *} -ML {* Sign.of_sort @{theory} (@{typ tyS}, @{sort fs}) *} - - - (* example 1 from Terms.thy *) - nominal_datatype trm1 = Vr1 "name" | Ap1 "trm1" "trm1" @@ -266,28 +244,6 @@ 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 from my PHD *) - -atom_decl coname - -nominal_datatype phd = - Ax "name" "coname" -| Cut n::"coname" t1::"phd" c::"coname" t2::"phd" bind n in t1, bind c in t2 -| AndR c1::"coname" t1::"phd" c2::"coname" t2::"phd" "coname" bind c1 in t1, bind c2 in t2 -| AndL1 n::"name" t::"phd" "name" bind n in t -| AndL2 n::"name" t::"phd" "name" bind n in t -| ImpL c::"coname" t1::"phd" n::"name" t2::"phd" "name" bind c in t1, bind n in t2 -| ImpR c::"coname" n::"name" t::"phd" "coname" bind n in t, bind c in t - -thm phd.fv -thm phd.eq_iff -thm phd.bn -thm phd.perm -thm phd.induct -thm phd.distinct -thm phd.fv[simplified phd.supp] - (* example 3 from Peter Sewell's bestiary *) nominal_datatype exp = @@ -471,18 +427,6 @@ "bv (K s ts vs) = (atoms (set (map fst ts))) \ (atoms (set (map fst vs)))" *) -text {* weirdo example from Peter Sewell's bestiary *} - -nominal_datatype weird = - WBind x::"name" y::"name" p1::"weird" p2::"weird" p3::"weird" - bind x in p1, bind x in p2, bind y in p2, bind y in p3 -| WV "name" -| WP "weird" "weird" - -thm permute_weird_raw.simps[no_vars] -thm alpha_weird_raw.intros[no_vars] -thm fv_weird_raw.simps[no_vars] - (* example 8 from Terms.thy *) (* Binding in a term under a bn, needs to fail *) diff -r 892fcdb96c96 -r aeed597d2043 Nominal/TestMorePerm.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Nominal/TestMorePerm.thy Tue Mar 23 08:33:48 2010 +0100 @@ -0,0 +1,49 @@ +theory TestMorePerm +imports "Parser" +begin + +(* Since there are more permutations, we do not know how to prove equivalence + (it is probably not true with the way alpha is defined now) so *) +ML {* val _ = cheat_equivp := true *} + + +atom_decl name + +(* example from my PHD *) + +atom_decl coname + +nominal_datatype phd = + Ax "name" "coname" +| Cut n::"coname" t1::"phd" c::"coname" t2::"phd" bind n in t1, bind c in t2 +| AndR c1::"coname" t1::"phd" c2::"coname" t2::"phd" "coname" bind c1 in t1, bind c2 in t2 +| AndL1 n::"name" t::"phd" "name" bind n in t +| AndL2 n::"name" t::"phd" "name" bind n in t +| ImpL c::"coname" t1::"phd" n::"name" t2::"phd" "name" bind c in t1, bind n in t2 +| ImpR c::"coname" n::"name" t::"phd" "coname" bind n in t, bind c in t + +thm phd.fv +thm phd.eq_iff +thm phd.bn +thm phd.perm +thm phd.induct +thm phd.distinct +thm phd.fv[simplified phd.supp] + +text {* weirdo example from Peter Sewell's bestiary *} + +nominal_datatype weird = + WBind x::"name" y::"name" p1::"weird" p2::"weird" p3::"weird" + bind x in p1, bind x in p2, bind y in p2, bind y in p3 +| WV "name" +| WP "weird" "weird" + +thm permute_weird_raw.simps[no_vars] +thm alpha_weird_raw.intros[no_vars] +thm fv_weird_raw.simps[no_vars] + + +end + + + diff -r 892fcdb96c96 -r aeed597d2043 Nominal/TySch.thy --- a/Nominal/TySch.thy Tue Mar 23 08:22:48 2010 +0100 +++ b/Nominal/TySch.thy Tue Mar 23 08:33:48 2010 +0100 @@ -4,8 +4,6 @@ atom_decl name -ML {* val _ = cheat_equivp := false *} - nominal_datatype t = Var "name" | Fun "t" "t"