# HG changeset patch # User Christian Urban # Date 1297094377 0 # Node ID ba34f893539a4ebd5451fc0c7ea3f42c9e056544 # Parent af5bbc257f7f36b381c2666dc0d9e45f7b82c4f9 cleaned up the experiments so that the tests go through diff -r af5bbc257f7f -r ba34f893539a Nominal/Ex/Let.thy --- a/Nominal/Ex/Let.thy Sat Feb 05 07:39:00 2011 +0900 +++ b/Nominal/Ex/Let.thy Mon Feb 07 15:59:37 2011 +0000 @@ -100,6 +100,7 @@ | "set (bn as) \* (s, t) \ subst s t (Let as b) = Let (substa s t as) (subst s t b)" | "substa s t ANil = ANil" | "substa s t (ACons v t' as) = ACons v (subst v t t') as" +oops (*apply (subgoal_tac "\l. \!r. subst_substa_graph l r") defer @@ -113,6 +114,7 @@ apply rule apply (rule subst_substa_graph.intros)*) +(* defer apply (case_tac x) apply (case_tac a) @@ -163,7 +165,7 @@ (Acons s (subst a t t') a2) ACons v (subst v t t') as" - +*) end diff -r af5bbc257f7f -r ba34f893539a Nominal/Ex/TypeSchemes.thy --- a/Nominal/Ex/TypeSchemes.thy Sat Feb 05 07:39:00 2011 +0900 +++ b/Nominal/Ex/TypeSchemes.thy Mon Feb 07 15:59:37 2011 +0000 @@ -4,40 +4,6 @@ section {*** Type Schemes ***} -nominal_datatype - A = Aa bool | Ab B -and - B = Ba bool | Bb A - -lemma - "(p \ (Sum_Type.Projl (f (Inl x)))) = Sum_Type.Projl ((p \ f) (Inl (p \ x)))" -apply(perm_simp) -apply(subst permute_fun_def) -sorry - -nominal_primrec - even :: "nat \ A" -and odd :: "nat \ B" -where - "even 0 = Aa True" -| "even (Suc n) = Ab (odd n)" -| "odd 0 = Ba False" -| "odd (Suc n) = Bb (even n)" -thm even_odd_graph.intros even_odd_sumC_def -thm sum.cases Product_Type.split -thm even_odd_graph_def -term Inr -term Sum_Type.Projr -term even_odd_sumC -thm even_odd_sumC_def -unfolding even_odd_sumC_def -sorry - -ML {* the *} - -thm even.psimps odd.psimps - - atom_decl name