diff -r 76d4d66309bd -r 8c3cf9f4f5f2 Nominal/Term9.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Nominal/Term9.thy Thu Feb 25 14:14:08 2010 +0100 @@ -0,0 +1,78 @@ +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 ["rlam9", "rbla9"] ["Term9.rlam9", "Term9.rbla9"] *} +print_theorems + +local_setup {* snd o define_fv_alpha "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