--- /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} \<union> bv6 t"
+| "bv6 (Lt6 l r) = bv6 l \<union> 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 \<union> 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
+
+
+
--- 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} \<union> rbv6 t"
-| "rbv6 (rLt6 l r) = rbv6 l \<union> 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 ("_ \<approx>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 \<Rightarrow> rtrm6 \<Rightarrow> 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 \<Rightarrow> rtrm6 \<Rightarrow> 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 \<Rightarrow> rtrm6 \<Rightarrow> 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) \<noteq> b \<Longrightarrow> \<not> (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 \<leftrightarrow> b)" in exI)
-apply (simp add: alpha_gen fresh_star_def)
-apply (simp add: alpha6_inj)
-done
-
-lemma fv6_rsp: "x \<approx>6 y \<Longrightarrow> 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 \<Rightarrow> trm6 \<Rightarrow> trm6"
-is
- "permute :: perm \<Rightarrow> rtrm6 \<Rightarrow> rtrm6"
-
-instance
-apply default
-sorry
-end
-
-lemma lifted_induct:
-"\<lbrakk>x1 = x2; \<And>name namea. name = namea \<Longrightarrow> P (Vr6 name) (Vr6 namea);
- \<And>name rtrm6 namea rtrm6a.
- \<lbrakk>True;
- \<exists>pi. fv_trm6 rtrm6 - {atom name} = fv_trm6 rtrm6a - {atom namea} \<and>
- (fv_trm6 rtrm6 - {atom name}) \<sharp>* pi \<and> pi \<bullet> rtrm6 = rtrm6a \<and> P (pi \<bullet> rtrm6) rtrm6a\<rbrakk>
- \<Longrightarrow> P (Lm6 name rtrm6) (Lm6 namea rtrm6a);
- \<And>rtrm61 rtrm61a rtrm62 rtrm62a.
- \<lbrakk>rtrm61 = rtrm61a; P rtrm61 rtrm61a;
- \<exists>pi. fv_trm6 rtrm62 - bv6 rtrm61 = fv_trm6 rtrm62a - bv6 rtrm61a \<and>
- (fv_trm6 rtrm62 - bv6 rtrm61) \<sharp>* pi \<and> pi \<bullet> rtrm62 = rtrm62a \<and> P (pi \<bullet> rtrm62) rtrm62a\<rbrakk>
- \<Longrightarrow> P (Lt6 rtrm61 rtrm62) (Lt6 rtrm61a rtrm62a)\<rbrakk>
-\<Longrightarrow> 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 \<and>
- (\<exists>pi. fv_trm6 rtrm62 - bv6 rtrm61 = fv_trm6 rtrm62a - bv6 rtrm61a \<and>
- (fv_trm6 rtrm62 - bv6 rtrm61) \<sharp>* pi \<and> pi \<bullet> rtrm62 = rtrm62a))"
-apply(lifting alpha6_inj(3)[unfolded alpha_gen])
-apply injection
-(* notice unsolvable goals: (alpha_rtrm6 ===> op =) rbv6 rbv6 *)
-oops
-
-
-
-
-end
--- 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 \<union> 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 ("_ \<approx>7a _" [100, 100] 100)
-thm alpha_rtrm7.intros
-thm fv_rtrm7.simps
-inductive
- alpha7 :: "rtrm7 \<Rightarrow> rtrm7 \<Rightarrow> bool" ("_ \<approx>7 _" [100, 100] 100)
-where
- a1: "a = b \<Longrightarrow> (rVr7 a) \<approx>7 (rVr7 b)"
-| a2: "(\<exists>pi. (({atom a}, t) \<approx>gen alpha7 fv_rtrm7 pi ({atom b}, s))) \<Longrightarrow> rLm7 a t \<approx>7 rLm7 b s"
-| a3: "(\<exists>pi. (((rbv7 t1), s1) \<approx>gen alpha7 fv_rtrm7 pi ((rbv7 t2), s2))) \<Longrightarrow> rLt7 t1 s1 \<approx>7 rLt7 t2 s2"
-
-lemma "(x::name) \<noteq> y \<Longrightarrow> \<not> (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 \<leftrightarrow> y)" in exI)
- apply (simp_all add: alpha_gen fresh_star_def)
- apply (rule a1)
- apply (rule refl)
-done
-
-end
--- 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 ("_ \<approx>9l' _" [100, 100] 100) and
- alpha_rbla9 ("_ \<approx>9b' _" [100, 100] 100)
-thm alpha_rlam9_alpha_rbla9.intros
-
-
-inductive
- alpha9l :: "rlam9 \<Rightarrow> rlam9 \<Rightarrow> bool" ("_ \<approx>9l _" [100, 100] 100)
-and
- alpha9b :: "rbla9 \<Rightarrow> rbla9 \<Rightarrow> bool" ("_ \<approx>9b _" [100, 100] 100)
-where
- a1: "a = b \<Longrightarrow> (Var9 a) \<approx>9l (Var9 b)"
-| a4: "(\<exists>pi. (({atom x1}, t1) \<approx>gen alpha9l fv_rlam9 pi ({atom x2}, t2))) \<Longrightarrow> Lam9 x1 t1 \<approx>9l Lam9 x2 t2"
-| a3: "b1 \<approx>9l b2 \<Longrightarrow> (\<exists>pi. (((rbv9 b1), t1) \<approx>gen alpha9l fv_rlam9 pi ((rbv9 b2), t2))) \<Longrightarrow> Bla9 b1 t1 \<approx>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 \<Rightarrow> lam9 \<Rightarrow> lam9"
-is
- "permute :: perm \<Rightarrow> rlam9 \<Rightarrow> rlam9"
-
-quotient_definition
- "permute_bla9 :: perm \<Rightarrow> bla9 \<Rightarrow> bla9"
-is
- "permute :: perm \<Rightarrow> rbla9 \<Rightarrow> rbla9"
-
-instance
-sorry
-
-end
-
-lemma "\<lbrakk>b1 = b2; \<exists>pi. fv_lam9 t1 - bv9 b1 = fv_lam9 t2 - bv9 b2 \<and> (fv_lam9 t1 - bv9 b1) \<sharp>* pi \<and> pi \<bullet> t1 = t2\<rbrakk>
- \<Longrightarrow> qBla9 b1 t1 = qBla9 b2 t2"
-apply (lifting a3[unfolded alpha_gen])
-apply injection
-sorry
-
-end
--- 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} \<union> bv6 t"
-| "bv6 (Lt6 l r) = bv6 l \<union> 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 \<union> 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 =