# HG changeset patch # User Cezary Kaliszyk # Date 1269328271 -3600 # Node ID 6542026b95cd6467c3dd082f896f153283e6092c # Parent d804729d6cf4ba9fc45210cf2a9f2670e3b53f00 Move Non-respectful examples to NotRsp diff -r d804729d6cf4 -r 6542026b95cd Nominal/NotRsp.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Nominal/NotRsp.thy Tue Mar 23 08:11:11 2010 +0100 @@ -0,0 +1,48 @@ +theory Test +imports "Parser" "../Attic/Prove" +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 +binder + bv6 +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" +*) + +(* 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 +binder + bv9 +where + "bv9 (Var9 x) = {}" +| "bv9 (Lam9 x b) = {atom x}" + +end + + + diff -r d804729d6cf4 -r 6542026b95cd Nominal/Term6.thy --- a/Nominal/Term6.thy Tue Mar 23 07:04:27 2010 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,155 +0,0 @@ -theory Term6 -imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "Abs" "Perm" "Fv" "Rsp" "../Attic/Prove" -begin - -atom_decl name - -(* example with a bn function defined over the type itself, NOT respectful. *) - -datatype rtrm6 = - rVr6 "name" -| rLm6 "name" "rtrm6" --"bind name in rtrm6" -| rLt6 "rtrm6" "rtrm6" --"bind (bv6 left) in (right)" - -primrec - rbv6 -where - "rbv6 (rVr6 n) = {}" -| "rbv6 (rLm6 n t) = {atom n} \ rbv6 t" -| "rbv6 (rLt6 l r) = rbv6 l \ rbv6 r" - -setup {* snd o define_raw_perms (Datatype.the_info @{theory} "Term6.rtrm6") 1 *} -print_theorems - -local_setup {* snd o define_fv_alpha (Datatype.the_info @{theory} "Term6.rtrm6") [ - [[], [(NONE, 0, 1)], [(SOME @{term rbv6}, 0, 1)]]] *} -notation alpha_rtrm6 ("_ \6 _" [100, 100] 100) -thm alpha_rtrm6.intros - -local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha6_inj}, []), (build_alpha_inj @{thms alpha_rtrm6.intros} @{thms rtrm6.distinct rtrm6.inject} @{thms alpha_rtrm6.cases} ctxt)) ctxt)) *} -thm alpha6_inj - -local_setup {* -snd o (build_eqvts @{binding rbv6_eqvt} [@{term rbv6}] [@{term "permute :: perm \ rtrm6 \ rtrm6"}] (@{thms rbv6.simps permute_rtrm6.simps}) @{thm rtrm6.induct}) -*} - -local_setup {* -snd o build_eqvts @{binding fv_rtrm6_eqvt} [@{term fv_rtrm6}] [@{term "permute :: perm \ rtrm6 \ rtrm6"}] (@{thms fv_rtrm6.simps permute_rtrm6.simps}) @{thm rtrm6.induct} -*} - -local_setup {* -(fn ctxt => snd (Local_Theory.note ((@{binding alpha6_eqvt}, []), - build_alpha_eqvts [@{term alpha_rtrm6}] [@{term "permute :: perm \ rtrm6 \ rtrm6"}] @{thms permute_rtrm6.simps alpha6_inj} @{thm alpha_rtrm6.induct} ctxt) ctxt)) -*} -thm alpha6_eqvt -local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha6_equivp}, []), - (build_equivps [@{term alpha_rtrm6}] @{thm rtrm6.induct} @{thm alpha_rtrm6.induct} @{thms rtrm6.inject} @{thms alpha6_inj} @{thms rtrm6.distinct} @{thms alpha_rtrm6.cases} @{thms alpha6_eqvt} ctxt)) ctxt)) *} -thm alpha6_equivp - -quotient_type - trm6 = rtrm6 / alpha_rtrm6 - by (auto intro: alpha6_equivp) - -local_setup {* -(fn ctxt => ctxt - |> snd o (Quotient_Def.quotient_lift_const ("Vr6", @{term rVr6})) - |> snd o (Quotient_Def.quotient_lift_const ("Lm6", @{term rLm6})) - |> snd o (Quotient_Def.quotient_lift_const ("Lt6", @{term rLt6})) - |> snd o (Quotient_Def.quotient_lift_const ("fv_trm6", @{term fv_rtrm6})) - |> snd o (Quotient_Def.quotient_lift_const ("bv6", @{term rbv6}))) -*} -print_theorems - -lemma [quot_respect]: - "(op = ===> alpha_rtrm6 ===> alpha_rtrm6) permute permute" -by (auto simp add: alpha6_eqvt) - -(* Definitely not true , see lemma below *) -lemma [quot_respect]:"(alpha_rtrm6 ===> op =) rbv6 rbv6" -apply simp apply clarify -apply (erule alpha_rtrm6.induct) -oops - -lemma "(a :: name) \ b \ \ (alpha_rtrm6 ===> op =) rbv6 rbv6" -apply simp -apply (rule_tac x="rLm6 (a::name) (rVr6 (a :: name))" in exI) -apply (rule_tac x="rLm6 (b::name) (rVr6 (b :: name))" in exI) -apply simp -apply (simp add: alpha6_inj) -apply (rule_tac x="(a \ b)" in exI) -apply (simp add: alpha_gen fresh_star_def) -apply (simp add: alpha6_inj) -done - -lemma fv6_rsp: "x \6 y \ fv_rtrm6 x = fv_rtrm6 y" -apply (induct_tac x y rule: alpha_rtrm6.induct) -apply simp_all -apply (erule exE) -apply (simp_all add: alpha_gen) -done - -lemma [quot_respect]:"(alpha_rtrm6 ===> op =) fv_rtrm6 fv_rtrm6" -by (simp add: fv6_rsp) - -lemma [quot_respect]: - "(op = ===> alpha_rtrm6) rVr6 rVr6" - "(op = ===> alpha_rtrm6 ===> alpha_rtrm6) rLm6 rLm6" -apply auto -apply (simp_all add: alpha6_inj) -apply (rule_tac x="0::perm" in exI) -apply (simp add: alpha_gen fv6_rsp fresh_star_def fresh_zero_perm) -done - -lemma [quot_respect]: - "(alpha_rtrm6 ===> alpha_rtrm6 ===> alpha_rtrm6) rLt6 rLt6" -apply auto -apply (simp_all add: alpha6_inj) -apply (rule_tac [!] x="0::perm" in exI) -apply (simp_all add: alpha_gen fresh_star_def fresh_zero_perm) -(* needs rbv6_rsp *) -oops - -instantiation trm6 :: pt begin - -quotient_definition - "permute_trm6 :: perm \ trm6 \ trm6" -is - "permute :: perm \ rtrm6 \ rtrm6" - -instance -apply default -sorry -end - -lemma lifted_induct: -"\x1 = x2; \name namea. name = namea \ P (Vr6 name) (Vr6 namea); - \name rtrm6 namea rtrm6a. - \True; - \pi. fv_trm6 rtrm6 - {atom name} = fv_trm6 rtrm6a - {atom namea} \ - (fv_trm6 rtrm6 - {atom name}) \* pi \ pi \ rtrm6 = rtrm6a \ P (pi \ rtrm6) rtrm6a\ - \ P (Lm6 name rtrm6) (Lm6 namea rtrm6a); - \rtrm61 rtrm61a rtrm62 rtrm62a. - \rtrm61 = rtrm61a; P rtrm61 rtrm61a; - \pi. fv_trm6 rtrm62 - bv6 rtrm61 = fv_trm6 rtrm62a - bv6 rtrm61a \ - (fv_trm6 rtrm62 - bv6 rtrm61) \* pi \ pi \ rtrm62 = rtrm62a \ P (pi \ rtrm62) rtrm62a\ - \ P (Lt6 rtrm61 rtrm62) (Lt6 rtrm61a rtrm62a)\ -\ P x1 x2" -apply (lifting alpha_rtrm6.induct[unfolded alpha_gen]) -apply injection -(* notice unsolvable goals: (alpha_rtrm6 ===> op =) rbv6 rbv6 *) -oops - -lemma lifted_inject_a3: -"(Lt6 rtrm61 rtrm62 = Lt6 rtrm61a rtrm62a) = -(rtrm61 = rtrm61a \ - (\pi. fv_trm6 rtrm62 - bv6 rtrm61 = fv_trm6 rtrm62a - bv6 rtrm61a \ - (fv_trm6 rtrm62 - bv6 rtrm61) \* pi \ pi \ rtrm62 = rtrm62a))" -apply(lifting alpha6_inj(3)[unfolded alpha_gen]) -apply injection -(* notice unsolvable goals: (alpha_rtrm6 ===> op =) rbv6 rbv6 *) -oops - - - - -end diff -r d804729d6cf4 -r 6542026b95cd Nominal/Term7.thy --- a/Nominal/Term7.thy Tue Mar 23 07:04:27 2010 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,50 +0,0 @@ -theory Term7 -imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "Abs" "Perm" "Fv" "Rsp" "../Attic/Prove" -begin - -atom_decl name - -(* example with a respectful bn function defined over the type itself *) - -datatype rtrm7 = - rVr7 "name" -| rLm7 "name" "rtrm7" --"bind left in right" -| rLt7 "rtrm7" "rtrm7" --"bind (bv7 left) in (right)" - -primrec - rbv7 -where - "rbv7 (rVr7 n) = {atom n}" -| "rbv7 (rLm7 n t) = rbv7 t - {atom n}" -| "rbv7 (rLt7 l r) = rbv7 l \ rbv7 r" - -setup {* snd o define_raw_perms (Datatype.the_info @{theory} "Term7.rtrm7") 1 *} -thm permute_rtrm7.simps - -local_setup {* snd o define_fv_alpha (Datatype.the_info @{theory} "Term7.rtrm7") [ - [[[]], [[(NONE, 0)], [(NONE, 0)]], [[], [(SOME @{term rbv7}, 0)]]]] *} -print_theorems -notation - alpha_rtrm7 ("_ \7a _" [100, 100] 100) -thm alpha_rtrm7.intros -thm fv_rtrm7.simps -inductive - alpha7 :: "rtrm7 \ rtrm7 \ bool" ("_ \7 _" [100, 100] 100) -where - a1: "a = b \ (rVr7 a) \7 (rVr7 b)" -| a2: "(\pi. (({atom a}, t) \gen alpha7 fv_rtrm7 pi ({atom b}, s))) \ rLm7 a t \7 rLm7 b s" -| a3: "(\pi. (((rbv7 t1), s1) \gen alpha7 fv_rtrm7 pi ((rbv7 t2), s2))) \ rLt7 t1 s1 \7 rLt7 t2 s2" - -lemma "(x::name) \ y \ \ (alpha7 ===> op =) rbv7 rbv7" - apply simp - apply (rule_tac x="rLt7 (rVr7 x) (rVr7 x)" in exI) - apply (rule_tac x="rLt7 (rVr7 y) (rVr7 y)" in exI) - apply simp - apply (rule a3) - apply (rule_tac x="(x \ y)" in exI) - apply (simp_all add: alpha_gen fresh_star_def) - apply (rule a1) - apply (rule refl) -done - -end diff -r d804729d6cf4 -r 6542026b95cd Nominal/Term9.thy --- a/Nominal/Term9.thy Tue Mar 23 07:04:27 2010 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,78 +0,0 @@ -theory Term9 -imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "Abs" "Perm" "Fv" "Rsp" "../Attic/Prove" -begin - -atom_decl name - -datatype rlam9 = - Var9 "name" -| Lam9 "name" "rlam9" --"bind name in rlam" -and rbla9 = - Bla9 "rlam9" "rlam9" --"bind bv(first) in second" - -primrec - rbv9 -where - "rbv9 (Var9 x) = {}" -| "rbv9 (Lam9 x b) = {atom x}" - -setup {* snd o define_raw_perms (Datatype.the_info @{theory} "Term9.rlam9") 2 *} -print_theorems - -local_setup {* snd o define_fv_alpha (Datatype.the_info @{theory} "Term9.rlam9") [ - [[[]], [[(NONE, 0)], [(NONE, 0)]]], [[[], [(SOME @{term rbv9}, 0)]]]] *} -notation - alpha_rlam9 ("_ \9l' _" [100, 100] 100) and - alpha_rbla9 ("_ \9b' _" [100, 100] 100) -thm alpha_rlam9_alpha_rbla9.intros - - -inductive - alpha9l :: "rlam9 \ rlam9 \ bool" ("_ \9l _" [100, 100] 100) -and - alpha9b :: "rbla9 \ rbla9 \ bool" ("_ \9b _" [100, 100] 100) -where - a1: "a = b \ (Var9 a) \9l (Var9 b)" -| a4: "(\pi. (({atom x1}, t1) \gen alpha9l fv_rlam9 pi ({atom x2}, t2))) \ Lam9 x1 t1 \9l Lam9 x2 t2" -| a3: "b1 \9l b2 \ (\pi. (((rbv9 b1), t1) \gen alpha9l fv_rlam9 pi ((rbv9 b2), t2))) \ Bla9 b1 t1 \9b Bla9 b2 t2" - -quotient_type - lam9 = rlam9 / alpha9l and bla9 = rbla9 / alpha9b -sorry - -local_setup {* -(fn ctxt => ctxt - |> snd o (Quotient_Def.quotient_lift_const ("qVar9", @{term Var9})) - |> snd o (Quotient_Def.quotient_lift_const ("qLam9", @{term Lam9})) - |> snd o (Quotient_Def.quotient_lift_const ("qBla9", @{term Bla9})) - |> snd o (Quotient_Def.quotient_lift_const ("fv_lam9", @{term fv_rlam9})) - |> snd o (Quotient_Def.quotient_lift_const ("fv_bla9", @{term fv_rbla9})) - |> snd o (Quotient_Def.quotient_lift_const ("bv9", @{term rbv9}))) -*} -print_theorems - -instantiation lam9 and bla9 :: pt -begin - -quotient_definition - "permute_lam9 :: perm \ lam9 \ lam9" -is - "permute :: perm \ rlam9 \ rlam9" - -quotient_definition - "permute_bla9 :: perm \ bla9 \ bla9" -is - "permute :: perm \ rbla9 \ rbla9" - -instance -sorry - -end - -lemma "\b1 = b2; \pi. fv_lam9 t1 - bv9 b1 = fv_lam9 t2 - bv9 b2 \ (fv_lam9 t1 - bv9 b1) \* pi \ pi \ t1 = t2\ - \ qBla9 b1 t1 = qBla9 b2 t2" -apply (lifting a3[unfolded alpha_gen]) -apply injection -sorry - -end diff -r d804729d6cf4 -r 6542026b95cd Nominal/Test.thy --- a/Nominal/Test.thy Tue Mar 23 07:04:27 2010 +0100 +++ b/Nominal/Test.thy Tue Mar 23 08:11:11 2010 +0100 @@ -564,37 +564,6 @@ thm alpha_weird_raw.intros[no_vars] thm fv_weird_raw.simps[no_vars] -(* example 6 from Terms.thy *) - -(* BV is not respectful, needs to fail*) -(* -nominal_datatype trm6 = - Vr6 "name" -| Lm6 x::"name" t::"trm6" bind x in t -| Lt6 left::"trm6" right::"trm6" bind "bv6 left" in right -binder - bv6 -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 *) -(* BV is not respectful, needs to fail*) -(* -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" -*) - (* example 8 from Terms.thy *) (* Binding in a term under a bn, needs to fail *) @@ -611,21 +580,6 @@ "bv8 (Bar0 x) = {}" | "bv8 (Bar1 v x b) = {atom v}" *) -(* example 9 from Terms.thy *) - -(* BV is not respectful, needs to fail*) -(* -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 -binder - bv9 -where - "bv9 (Var9 x) = {}" -| "bv9 (Lam9 x b) = {atom x}" -*) (* Type schemes with separate datatypes *) nominal_datatype T =