# HG changeset patch # User Christian Urban # Date 1293052424 0 # Node ID e6e6a3da81aaf35c7f073c32e6881da5a3494454 # Parent 02b24877be3efb30e05394962d31e3ffe7be9da5 tuned examples diff -r 02b24877be3e -r e6e6a3da81aa Nominal/Ex/NoneExamples.thy --- a/Nominal/Ex/NoneExamples.thy Wed Dec 22 21:13:32 2010 +0000 +++ b/Nominal/Ex/NoneExamples.thy Wed Dec 22 21:13:44 2010 +0000 @@ -3,7 +3,7 @@ begin text {* - This example is not covered by our binding + These examples are not covered by our binding specification. *} @@ -25,7 +25,7 @@ *) text {* - this example binds bound names and therefore the + This example binds bound names and therefore the fv-function is not respectful - the proof just fails. *} @@ -43,7 +43,7 @@ *) text {* - this example uses "-" in the binding function; + This example uses "-" in the binding function; at the moment this is unsupported *} @@ -61,7 +61,7 @@ *) text {* - again this example binds bound names - so not respectful + Again this example binds bound names - so is not respectful *} (* @@ -73,10 +73,33 @@ binder bv :: "trm \ atom set" where - "bv (Vam x) = {}" + "bv (Var x) = {}" | "bv (Lam x b) = {atom x}" *) +text {* + This example has mal-formed deep recursive binders. + + - Bla1: recursive deep binder used twice + - Bla2: deep binder used recursively and non-recursively + - Bla3: x used in recursive deep binder and somewhere else +*} + +(* +nominal_datatype trm = + Var "name" +and bla = + App "trm" "trm" +| Bla1 f::"trm" s1::"trm" s2::"trm" bind "bv f" in s1 f, bind "bv f" in s2 f +| Bla2 f::"trm" s1::"trm" s2::"trm" bind "bv f" in s1, bind "bv f" in s2 f +| Bla3 f::"trm" s1::"trm" s2::"trm" x::"name" y::"name" bind "bv f" x in s1 f, bind y x in s2 +binder + bv :: "trm \ atom list" +where + "bv (Var a) = [atom a]" +*) + + end diff -r 02b24877be3e -r e6e6a3da81aa Nominal/Ex/Shallow.thy --- a/Nominal/Ex/Shallow.thy Wed Dec 22 21:13:32 2010 +0000 +++ b/Nominal/Ex/Shallow.thy Wed Dec 22 21:13:44 2010 +0000 @@ -15,6 +15,8 @@ | App1 "trm1" "trm1" | Lam1 xs::"name list" t::"trm1" bind xs in t +thm trm1.strong_exhaust + text {* binding a finite set of names *} @@ -23,6 +25,7 @@ | App2 "trm2" "trm2" | Lam2 xs::"name fset" t::"trm2" bind (set) xs in t +thm trm2.strong_exhaust text {* restricting a finite set of names *} @@ -31,6 +34,7 @@ | App3 "trm3" "trm3" | Lam3 xs::"name fset" t::"trm3" bind (res) xs in t +thm trm3.strong_exhaust end diff -r 02b24877be3e -r e6e6a3da81aa Nominal/Ex/SingleLet.thy --- a/Nominal/Ex/SingleLet.thy Wed Dec 22 21:13:32 2010 +0000 +++ b/Nominal/Ex/SingleLet.thy Wed Dec 22 21:13:44 2010 +0000 @@ -22,7 +22,8 @@ thm single_let.distinct thm single_let.induct thm single_let.inducts -thm single_let.exhaust[no_vars] +thm single_let.exhaust +thm single_let.strong_exhaust thm single_let.fv_defs thm single_let.bn_defs thm single_let.perm_simps @@ -34,107 +35,6 @@ thm single_let.supp thm single_let.fresh -lemmas permute_bn = permute_bn_raw.simps[quot_lifted] - -lemma uu: - shows "alpha_bn as (permute_bn p as)" -apply(induct as rule: single_let.inducts(2)) -apply(auto)[7] -apply(simp add: permute_bn) -apply(simp add: single_let.eq_iff) -done - -lemma tt: - shows "(p \ bn as) = bn (permute_bn p as)" -apply(induct as rule: single_let.inducts(2)) -apply(auto)[7] -apply(simp add: permute_bn single_let.bn_defs) -apply(simp add: atom_eqvt) -done - -lemma Abs_fresh_star': - fixes x::"'a::fs" - shows "set bs = as \ as \* Abs_lst bs x" - unfolding fresh_star_def - by(simp_all add: Abs_fresh_iff) - -lemma strong_exhaust: - fixes c::"'a::fs" - assumes "\name. y = Var name \ P" - and "\trm1 trm2. y = App trm1 trm2 \ P" - and "\name trm. \{atom name} \* c; y = Lam name trm\ \ P" - and "\assg trm. \set (bn assg) \* c; y = Let assg trm\ \ P" - and "\name1 name2 trm1 trm2 trm3. \{atom name1} \* c; y = Foo name1 name2 trm1 trm2 trm3\ \ P" - and "\name1 name2 trm. \{atom name1, atom name2} \* c; y = Bar name1 name2 trm\ \ P" - and "\name trm1 trm2. \{atom name} \* c; y = Baz name trm1 trm2\ \ P" - shows "P" - apply(rule_tac y="y" in single_let.exhaust(1)) - apply(rule assms(1)) - apply(assumption) - apply(rule assms(2)) - apply(assumption) - apply(subgoal_tac "\q. (q \ {atom name}) \* c \ supp ([[atom name]]lst.trm) \* q") - apply(erule exE) - apply(erule conjE) - apply(perm_simp) - apply(rule assms(3)) - apply(assumption) - apply(drule supp_perm_eq[symmetric]) - apply(simp add: single_let.eq_iff) - apply(perm_simp) - apply(rule refl) - apply(rule at_set_avoiding2) - apply(simp add: finite_supp) - apply(simp add: finite_supp) - apply(simp add: finite_supp) - apply(simp add: Abs_fresh_star') - apply(subgoal_tac "\q. (q \ (set (bn assg))) \* (c::'a::fs) \ supp ([bn assg]lst.trm) \* q") - apply(erule exE) - apply(erule conjE) - apply(perm_simp add: tt) - apply(rule_tac assms(4)) - apply(assumption) - apply(drule supp_perm_eq[symmetric]) - apply(simp add: single_let.eq_iff) - apply(simp add: tt uu) - apply(rule at_set_avoiding2) - apply(simp add: finite_supp) - apply(simp add: finite_supp) - apply(simp add: finite_supp) - apply(simp add: Abs_fresh_star) - apply(subgoal_tac "\q. (q \ {atom name1}) \* (c::'a::fs) \ - supp ([{atom name1}]set.(((name2, trm1), trm2), trm3)) \* q") - apply(erule exE) - apply(erule conjE) - apply(perm_simp add: tt) - apply(rule_tac assms(5)) - apply(assumption) - apply(drule supp_perm_eq[symmetric]) - apply(simp add: single_let.eq_iff) - apply(perm_simp) - apply(rule refl) - apply(rule at_set_avoiding2) - apply(simp add: finite_supp) - apply(simp add: finite_supp) - apply(simp add: finite_supp) - apply(simp add: Abs_fresh_star) - apply(subgoal_tac "\q. (q \ {atom name1, atom name2}) \* (c::'a::fs) \ - supp ([[atom name2, atom name1]]lst.((trm, name1), name2)) \* q") - apply(erule exE) - apply(erule conjE) - apply(perm_simp add: tt) - apply(rule_tac assms(6)) - apply(assumption) - apply(drule supp_perm_eq[symmetric]) - apply(simp add: single_let.eq_iff) - apply(perm_simp) - apply(rule refl) - apply(rule at_set_avoiding2) - apply(simp add: finite_supp) - apply(simp add: finite_supp) - apply(simp add: finite_supp) - oops - end diff -r 02b24877be3e -r e6e6a3da81aa Nominal/Ex/SystemFOmega.thy --- a/Nominal/Ex/SystemFOmega.thy Wed Dec 22 21:13:32 2010 +0000 +++ b/Nominal/Ex/SystemFOmega.thy Wed Dec 22 21:13:44 2010 +0000 @@ -13,7 +13,8 @@ atom_decl label nominal_datatype kind = - \ | KFun kind kind + \ +| KFun kind kind nominal_datatype ty = TVar tvar @@ -41,7 +42,6 @@ RNil | RCons label trm rec - thm ty_trec.distinct thm ty_trec.induct thm ty_trec.inducts diff -r 02b24877be3e -r e6e6a3da81aa Nominal/Ex/TypeSchemes.thy --- a/Nominal/Ex/TypeSchemes.thy Wed Dec 22 21:13:32 2010 +0000 +++ b/Nominal/Ex/TypeSchemes.thy Wed Dec 22 21:13:44 2010 +0000 @@ -6,7 +6,6 @@ atom_decl name - (* defined as a single nominal datatype *) nominal_datatype ty = diff -r 02b24877be3e -r e6e6a3da81aa Nominal/Ex/TypeVarsTest.thy --- a/Nominal/Ex/TypeVarsTest.thy Wed Dec 22 21:13:32 2010 +0000 +++ b/Nominal/Ex/TypeVarsTest.thy Wed Dec 22 21:13:44 2010 +0000 @@ -7,7 +7,7 @@ (* the sort constraints need to be attached to the *) (* first occurence of the type variables on the *) -(* left-hand side *) +(* right-hand side *) atom_decl name @@ -22,7 +22,7 @@ | App "('a::s1, 'b::s2, 'c::at) lam" "('a, 'b, 'c) lam" | Lam x::"name" l::"('a, 'b, 'c) lam" bind x in l | Foo "'a" "'b" -| Bar x::"'c" l::"('a, 'b, 'c) lam" bind x in l +| Bar x::"'c" l::"('a, 'b, 'c) lam" bind x in l (* Bar binds a polymorphic atom *) term Foo term Bar