1 theory Terms

     2 imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "Abs" "Perm" "Fv" "Rsp" "../Attic/Prove"

     3 begin

     4 

     5 atom_decl name

     6 

     7 text {* primrec seems to be genarally faster than fun *}

     8 

     9 section {*** lets with binding patterns ***}

    10 

    11 datatype rtrm1 =

    12   rVr1 "name"

    13 | rAp1 "rtrm1" "rtrm1"

    14 | rLm1 "name" "rtrm1"        --"name is bound in trm1"

    15 | rLt1 "bp" "rtrm1" "rtrm1"   --"all variables in bp are bound in the 2nd trm1"

    16 and bp =

    17   BUnit

    18 | BVr "name"

    19 | BPr "bp" "bp"

    20 

    21 print_theorems

    22 

    23 (* to be given by the user *)

    24 

    25 primrec 

    26   bv1

    27 where

    28   "bv1 (BUnit) = {}"

    29 | "bv1 (BVr x) = {atom x}"

    30 | "bv1 (BPr bp1 bp2) = (bv1 bp1) \<union> (bv1 bp2)"

    31 

    32 setup {* snd o define_raw_perms ["rtrm1", "bp"] ["Terms.rtrm1", "Terms.bp"] *}

    33 thm permute_rtrm1_permute_bp.simps

    34 

    35 local_setup {*

    36   snd o define_fv_alpha "Terms.rtrm1"

    37   [[[[]], [[], []], [[(NONE, 0)], [(NONE, 0)]], [[(SOME @{term bv1}, 0)], [], [(SOME @{term bv1}, 0)]]],

    38   [[], [[]], [[], []]]] *}

    39 

    40 notation

    41   alpha_rtrm1 ("_ \<approx>1 _" [100, 100] 100) and

    42   alpha_bp ("_ \<approx>1b _" [100, 100] 100)

    43 thm alpha_rtrm1_alpha_bp.intros

    44 thm fv_rtrm1_fv_bp.simps

    45 

    46 local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha1_inj}, []), (build_alpha_inj @{thms alpha_rtrm1_alpha_bp.intros} @{thms rtrm1.distinct rtrm1.inject bp.distinct bp.inject} @{thms alpha_rtrm1.cases alpha_bp.cases} ctxt)) ctxt)) *}

    47 thm alpha1_inj

    48 

    49 lemma alpha_bp_refl: "alpha_bp a a"

    50 apply induct

    51 apply (simp_all  add: alpha1_inj)

    52 done

    53 

    54 lemma alpha_bp_eq_eq: "alpha_bp a b = (a = b)"

    55 apply rule

    56 apply (induct a b rule: alpha_rtrm1_alpha_bp.inducts(2))

    57 apply (simp_all add: alpha_bp_refl)

    58 done

    59 

    60 lemma alpha_bp_eq: "alpha_bp = (op =)"

    61 apply (rule ext)+

    62 apply (rule alpha_bp_eq_eq)

    63 done

    64 

    65 ML {*

    66 fun build_eqvts bind funs perms simps induct ctxt =

    67 let

    68   val pi = Free ("p", @{typ perm});

    69   val types = map (domain_type o fastype_of) funs;

    70   val indnames = Name.variant_list ["pi"] (Datatype_Prop.make_tnames (map body_type types));

    71   val args = map Free (indnames ~~ types);

    72   val perm_at = @{term "permute :: perm \<Rightarrow> atom set \<Rightarrow> atom set"}

    73   fun eqvtc (fnctn, (arg, perm)) =

    74     HOLogic.mk_eq ((perm_at $ pi $ (fnctn $ arg)), (fnctn $ (perm $ pi $ arg)))

    75   val gl = HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj (map eqvtc (funs ~~ (args ~~ perms))))

    76   fun tac _ = (indtac induct indnames THEN_ALL_NEW

    77     (asm_full_simp_tac (HOL_ss addsimps 

    78       (@{thm atom_eqvt} :: (Nominal_ThmDecls.get_eqvts_thms ctxt) @ simps)))) 1

    79   val thm = Goal.prove ctxt ("p" :: indnames) [] gl tac

    80   val thms = HOLogic.conj_elims thm

    81 in

    82   Local_Theory.note ((bind, [Attrib.internal (fn _ => Nominal_ThmDecls.eqvt_add)]), thms) ctxt

    83 end

    84 *}

    85 

    86 local_setup {*

    87 snd o (build_eqvts @{binding bv1_eqvt} [@{term bv1}] [@{term "permute :: perm \<Rightarrow> bp \<Rightarrow> bp"}] (@{thms bv1.simps permute_rtrm1_permute_bp.simps}) @{thm rtrm1_bp.inducts(2)})

    88 *}

    89 

    90 local_setup {*

    91 snd o build_eqvts @{binding fv_rtrm1_fv_bp_eqvt} [@{term fv_rtrm1}, @{term fv_bp}] [@{term "permute :: perm \<Rightarrow> rtrm1 \<Rightarrow> rtrm1"},@{term "permute :: perm \<Rightarrow> bp \<Rightarrow> bp"}] (@{thms fv_rtrm1_fv_bp.simps permute_rtrm1_permute_bp.simps}) @{thm rtrm1_bp.induct}

    92 *}

    93 

    94 ML {*

    95 fun build_alpha_eqvts funs perms simps induct ctxt =

    96 let

    97   val pi = Free ("p", @{typ perm});

    98   val types = map (domain_type o fastype_of) funs;

    99   val indnames = Name.variant_list ["pi"] (Datatype_Prop.make_tnames (map body_type types));

   100   val indnames2 = Name.variant_list ("pi" :: indnames) (Datatype_Prop.make_tnames (map body_type types));

   101   val args = map Free (indnames ~~ types);

   102   val args2 = map Free (indnames2 ~~ types);

   103   fun eqvtc ((alpha, perm), (arg, arg2)) =

   104     HOLogic.mk_imp (alpha $ arg $ arg2,

   105       (alpha $ (perm $ pi $ arg) $ (perm $ pi $ arg2)))

   106   val gl = HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj (map eqvtc ((funs ~~ perms) ~~ (args ~~ args2))))

   107   fun tac _ = (rtac induct THEN_ALL_NEW

   108     (asm_full_simp_tac (HOL_ss addsimps 

   109       (@{thm atom_eqvt} :: (Nominal_ThmDecls.get_eqvts_thms ctxt) @ simps)))

   110     THEN_ALL_NEW (TRY o REPEAT_ALL_NEW (CHANGED o rtac conjI) THEN_ALL_NEW

   111       (etac @{thm alpha_gen_compose_eqvt})) THEN_ALL_NEW

   112     (asm_full_simp_tac (HOL_ss addsimps 

   113       (@{thm atom_eqvt} :: (Nominal_ThmDecls.get_eqvts_thms ctxt) @ simps)))

   114 ) 1

   115   val thm = Goal.prove ctxt ("p" :: indnames @ indnames2) [] gl tac

   116 in

   117   map (fn x => mp OF [x]) (HOLogic.conj_elims thm)

   118 end

   119 *}

   120 

   121 local_setup {*

   122 (fn ctxt => snd (Local_Theory.note ((@{binding alpha1_eqvt}, []),

   123   build_alpha_eqvts [@{term alpha_rtrm1}, @{term alpha_bp}] [@{term "permute :: perm \<Rightarrow> rtrm1 \<Rightarrow> rtrm1"},@{term "permute :: perm \<Rightarrow> bp \<Rightarrow> bp"}] @{thms permute_rtrm1_permute_bp.simps alpha1_inj} @{thm alpha_rtrm1_alpha_bp.induct} ctxt) ctxt))

   124 *}

   125 print_theorems

   126 

   127 lemma alpha1_eqvt_proper[eqvt]:

   128   "pi \<bullet> (t \<approx>1 s) = ((pi \<bullet> t) \<approx>1 (pi \<bullet> s))"

   129   "pi \<bullet> (alpha_bp a b) = (alpha_bp (pi \<bullet> a) (pi \<bullet> b))"

   130   apply (simp_all only: eqvts)

   131   apply rule

   132   apply (simp_all add: alpha1_eqvt)

   133   apply (subst permute_minus_cancel(2)[symmetric,of "t" "pi"])

   134   apply (subst permute_minus_cancel(2)[symmetric,of "s" "pi"])

   135   apply (simp_all only: alpha1_eqvt)

   136   apply rule

   137   apply (simp_all add: alpha1_eqvt)

   138   apply (subst permute_minus_cancel(2)[symmetric,of "a" "pi"])

   139   apply (subst permute_minus_cancel(2)[symmetric,of "b" "pi"])

   140   apply (simp_all only: alpha1_eqvt)

   141 done

   142 

   143 local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha1_equivp}, []),

   144   (build_equivps [@{term alpha_rtrm1}, @{term alpha_bp}] @{thm rtrm1_bp.induct} @{thm alpha_rtrm1_alpha_bp.induct} @{thms rtrm1.inject bp.inject} @{thms alpha1_inj} @{thms rtrm1.distinct bp.distinct} @{thms alpha_rtrm1.cases alpha_bp.cases} @{thms alpha1_eqvt} ctxt)) ctxt)) *}

   145 thm alpha1_equivp

   146 

   147 local_setup  {* define_quotient_type [(([], @{binding trm1}, NoSyn), (@{typ rtrm1}, @{term alpha_rtrm1}))]

   148   (rtac @{thm alpha1_equivp(1)} 1) *}

   149 

   150 local_setup {*

   151 (fn ctxt => ctxt

   152  |> snd o (Quotient_Def.quotient_lift_const ("Vr1", @{term rVr1}))

   153  |> snd o (Quotient_Def.quotient_lift_const ("Ap1", @{term rAp1}))

   154  |> snd o (Quotient_Def.quotient_lift_const ("Lm1", @{term rLm1}))

   155  |> snd o (Quotient_Def.quotient_lift_const ("Lt1", @{term rLt1}))

   156  |> snd o (Quotient_Def.quotient_lift_const ("fv_trm1", @{term fv_rtrm1})))

   157 *}

   158 print_theorems

   159 

   160 thm alpha_rtrm1_alpha_bp.induct

   161 local_setup {* prove_const_rsp @{binding fv_rtrm1_rsp} [@{term fv_rtrm1}]

   162   (fn _ => fvbv_rsp_tac @{thm alpha_rtrm1_alpha_bp.inducts(1)} @{thms fv_rtrm1_fv_bp.simps} 1) *}

   163 local_setup {* prove_const_rsp @{binding rVr1_rsp} [@{term rVr1}]

   164   (fn _ => constr_rsp_tac @{thms alpha1_inj} @{thms fv_rtrm1_rsp} @{thms alpha1_equivp} 1) *}

   165 local_setup {* prove_const_rsp @{binding rAp1_rsp} [@{term rAp1}]

   166   (fn _ => constr_rsp_tac @{thms alpha1_inj} @{thms fv_rtrm1_rsp} @{thms alpha1_equivp} 1) *}

   167 local_setup {* prove_const_rsp @{binding rLm1_rsp} [@{term rLm1}]

   168   (fn _ => constr_rsp_tac @{thms alpha1_inj} @{thms fv_rtrm1_rsp} @{thms alpha1_equivp} 1) *}

   169 local_setup {* prove_const_rsp @{binding rLt1_rsp} [@{term rLt1}]

   170   (fn _ => constr_rsp_tac @{thms alpha1_inj} @{thms fv_rtrm1_rsp} @{thms alpha1_equivp} 1) *}

   171 local_setup {* prove_const_rsp @{binding permute_rtrm1_rsp} [@{term "permute :: perm \<Rightarrow> rtrm1 \<Rightarrow> rtrm1"}]

   172   (fn _ => asm_simp_tac (HOL_ss addsimps @{thms alpha1_eqvt}) 1) *}

   173 

   174 lemmas trm1_bp_induct = rtrm1_bp.induct[quot_lifted]

   175 lemmas trm1_bp_inducts = rtrm1_bp.inducts[quot_lifted]

   176 

   177 setup {* define_lifted_perms ["Terms.trm1"] [("permute_trm1", @{term "permute :: perm \<Rightarrow> rtrm1 \<Rightarrow> rtrm1"})]

   178   @{thms permute_rtrm1_permute_bp_zero permute_rtrm1_permute_bp_append} *}

   179 

   180 lemmas

   181     permute_trm1 = permute_rtrm1_permute_bp.simps[quot_lifted]

   182 and fv_trm1 = fv_rtrm1_fv_bp.simps[quot_lifted]

   183 and fv_trm1_eqvt = fv_rtrm1_fv_bp_eqvt(1)[quot_lifted]

   184 and alpha1_INJ = alpha1_inj[unfolded alpha_gen, quot_lifted, folded alpha_gen]

   185 

   186 lemma supports:

   187   "(supp (atom x)) supports (Vr1 x)"

   188   "(supp t \<union> supp s) supports (Ap1 t s)"

   189   "(supp (atom x) \<union> supp t) supports (Lm1 x t)"

   190   "(supp b \<union> supp t \<union> supp s) supports (Lt1 b t s)"

   191   "{} supports BUnit"

   192   "(supp (atom x)) supports (BVr x)"

   193   "(supp a \<union> supp b) supports (BPr a b)"

   194 apply(simp_all add: supports_def fresh_def[symmetric] swap_fresh_fresh permute_trm1)

   195 apply(rule_tac [!] allI)+

   196 apply(rule_tac [!] impI)

   197 apply(tactic {* ALLGOALS (REPEAT o etac conjE) *})

   198 apply(simp_all add: fresh_atom)

   199 done

   200 

   201 lemma rtrm1_bp_fs:

   202   "finite (supp (x :: trm1))"

   203   "finite (supp (b :: bp))"

   204   apply (induct x and b rule: trm1_bp_inducts)

   205   apply(tactic {* ALLGOALS (rtac @{thm supports_finite} THEN' resolve_tac @{thms supports}) *})

   206   apply(simp_all add: supp_atom)

   207   done

   208 

   209 instance trm1 :: fs

   210 apply default

   211 apply (rule rtrm1_bp_fs(1))

   212 done

   213 

   214 lemma fv_eq_bv: "fv_bp bp = bv1 bp"

   215 apply(induct bp rule: trm1_bp_inducts(2))

   216 apply(simp_all)

   217 done

   218 

   219 lemma helper2: "{b. \<forall>pi. pi \<bullet> (a \<rightleftharpoons> b) \<bullet> bp \<noteq> bp} = {}"

   220 apply auto

   221 apply (rule_tac x="(x \<rightleftharpoons> a)" in exI)

   222 apply auto

   223 done

   224 

   225 lemma supp_fv:

   226   "supp t = fv_trm1 t"

   227   "supp b = fv_bp b"

   228 apply(induct t and b rule: trm1_bp_inducts)

   229 apply(simp_all)

   230 apply(simp add: supp_def permute_trm1 alpha1_INJ fv_trm1)

   231 apply(simp only: supp_at_base[simplified supp_def])

   232 apply(simp add: supp_def permute_trm1 alpha1_INJ fv_trm1)

   233 apply(simp add: Collect_imp_eq Collect_neg_eq)

   234 apply(subgoal_tac "supp (Lm1 name rtrm1) = supp (Abs {atom name} rtrm1)")

   235 apply(simp add: supp_Abs fv_trm1)

   236 apply(simp (no_asm) add: supp_def permute_set_eq atom_eqvt permute_trm1)

   237 apply(simp add: alpha1_INJ)

   238 apply(simp add: Abs_eq_iff)

   239 apply(simp add: alpha_gen.simps)

   240 apply(simp add: supp_eqvt[symmetric] fv_trm1_eqvt[symmetric])

   241 apply(subgoal_tac "supp (Lt1 bp rtrm11 rtrm12) = supp(rtrm11) \<union> supp (Abs (bv1 bp) rtrm12)")

   242 apply(simp add: supp_Abs fv_trm1 fv_eq_bv)

   243 apply(simp (no_asm) add: supp_def permute_trm1)

   244 apply(simp add: alpha1_INJ alpha_bp_eq)

   245 apply(simp add: Abs_eq_iff)

   246 apply(simp add: alpha_gen)

   247 apply(simp add: supp_eqvt[symmetric] fv_trm1_eqvt[symmetric] bv1_eqvt fv_eq_bv)

   248 apply(simp add: Collect_imp_eq Collect_neg_eq fresh_star_def helper2)

   249 apply(simp (no_asm) add: supp_def permute_set_eq atom_eqvt)

   250 apply(simp (no_asm) add: supp_def eqvts)

   251 apply(fold supp_def)

   252 apply(simp add: supp_at_base)

   253 apply(simp (no_asm) add: supp_def Collect_imp_eq Collect_neg_eq)

   254 apply(simp add: Collect_imp_eq[symmetric] Collect_neg_eq[symmetric] supp_def[symmetric])

   255 done

   256 

   257 lemma trm1_supp:

   258   "supp (Vr1 x) = {atom x}"

   259   "supp (Ap1 t1 t2) = supp t1 \<union> supp t2"

   260   "supp (Lm1 x t) = (supp t) - {atom x}"

   261   "supp (Lt1 b t s) = supp t \<union> (supp s - bv1 b)"

   262 by (simp_all add: supp_fv fv_trm1 fv_eq_bv)

   263 

   264 lemma trm1_induct_strong:

   265   assumes "\<And>name b. P b (Vr1 name)"

   266   and     "\<And>rtrm11 rtrm12 b. \<lbrakk>\<And>c. P c rtrm11; \<And>c. P c rtrm12\<rbrakk> \<Longrightarrow> P b (Ap1 rtrm11 rtrm12)"

   267   and     "\<And>name rtrm1 b. \<lbrakk>\<And>c. P c rtrm1; (atom name) \<sharp> b\<rbrakk> \<Longrightarrow> P b (Lm1 name rtrm1)"

   268   and     "\<And>bp rtrm11 rtrm12 b. \<lbrakk>\<And>c. P c rtrm11; \<And>c. P c rtrm12; bv1 bp \<sharp>* b\<rbrakk> \<Longrightarrow> P b (Lt1 bp rtrm11 rtrm12)"

   269   shows   "P a rtrma"

   270 sorry

   271 

   272 section {*** lets with single assignments ***}

   273 

   274 datatype rtrm2 =

   275   rVr2 "name"

   276 | rAp2 "rtrm2" "rtrm2"

   277 | rLm2 "name" "rtrm2" --"bind (name) in (rtrm2)"

   278 | rLt2 "rassign" "rtrm2" --"bind (bv2 rassign) in (rtrm2)"

   279 and rassign =

   280   rAs "name" "rtrm2"

   281 

   282 (* to be given by the user *)

   283 primrec 

   284   rbv2

   285 where

   286   "rbv2 (rAs x t) = {atom x}"

   287 

   288 setup {* snd o define_raw_perms ["rtrm2", "rassign"] ["Terms.rtrm2", "Terms.rassign"] *}

   289 

   290 local_setup {* snd o define_fv_alpha "Terms.rtrm2"

   291   [[[[]], [[], []], [[(NONE, 0)], [(NONE, 0)]], [[], [(SOME @{term rbv2}, 0)]]],

   292    [[[], []]]] *}

   293 

   294 notation

   295   alpha_rtrm2 ("_ \<approx>2 _" [100, 100] 100) and

   296   alpha_rassign ("_ \<approx>2b _" [100, 100] 100)

   297 thm alpha_rtrm2_alpha_rassign.intros

   298 

   299 local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha2_inj}, []), (build_alpha_inj @{thms alpha_rtrm2_alpha_rassign.intros} @{thms rtrm2.distinct rtrm2.inject rassign.distinct rassign.inject} @{thms alpha_rtrm2.cases alpha_rassign.cases} ctxt)) ctxt)) *}

   300 thm alpha2_inj

   301 

   302 lemma alpha2_eqvt:

   303   "t \<approx>2 s \<Longrightarrow> (pi \<bullet> t) \<approx>2 (pi \<bullet> s)"

   304   "a \<approx>2b b \<Longrightarrow> (pi \<bullet> a) \<approx>2b (pi \<bullet> b)"

   305 sorry

   306 

   307 local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha2_equivp}, []),

   308   (build_equivps [@{term alpha_rtrm2}, @{term alpha_rassign}] @{thm rtrm2_rassign.induct} @{thm alpha_rtrm2_alpha_rassign.induct} @{thms rtrm2.inject rassign.inject} @{thms alpha2_inj} @{thms rtrm2.distinct rassign.distinct} @{thms alpha_rtrm2.cases alpha_rassign.cases} @{thms alpha2_eqvt} ctxt)) ctxt)) *}

   309 thm alpha2_equivp

   310 

   311 local_setup  {* define_quotient_type 

   312   [(([], @{binding trm2}, NoSyn), (@{typ rtrm2}, @{term alpha_rtrm2})),

   313    (([], @{binding assign}, NoSyn), (@{typ rassign}, @{term alpha_rassign}))]

   314   ((rtac @{thm alpha2_equivp(1)} 1) THEN (rtac @{thm alpha2_equivp(2)}) 1) *}

   315 

   316 local_setup {*

   317 (fn ctxt => ctxt

   318  |> snd o (Quotient_Def.quotient_lift_const ("Vr2", @{term rVr2}))

   319  |> snd o (Quotient_Def.quotient_lift_const ("Ap2", @{term rAp2}))

   320  |> snd o (Quotient_Def.quotient_lift_const ("Lm2", @{term rLm2}))

   321  |> snd o (Quotient_Def.quotient_lift_const ("Lt2", @{term rLt2}))

   322  |> snd o (Quotient_Def.quotient_lift_const ("As", @{term rAs}))

   323  |> snd o (Quotient_Def.quotient_lift_const ("fv_trm2", @{term fv_rtrm2}))

   324  |> snd o (Quotient_Def.quotient_lift_const ("bv2", @{term rbv2})))

   325 *}

   326 print_theorems

   327 

   328 local_setup {* prove_const_rsp @{binding fv_rtrm2_rsp} [@{term fv_rtrm2}, @{term fv_rassign}]

   329   (fn _ => fvbv_rsp_tac @{thm alpha_rtrm2_alpha_rassign.induct} @{thms fv_rtrm2_fv_rassign.simps} 1) *}

   330 local_setup {* prove_const_rsp @{binding rbv2_rsp} [@{term rbv2}]

   331   (fn _ => fvbv_rsp_tac @{thm alpha_rtrm2_alpha_rassign.inducts(2)} @{thms rbv2.simps} 1) *}

   332 local_setup {* prove_const_rsp @{binding rVr2_rsp} [@{term rVr2}]

   333   (fn _ => constr_rsp_tac @{thms alpha2_inj} @{thms fv_rtrm2_rsp} @{thms alpha2_equivp} 1) *}

   334 local_setup {* prove_const_rsp @{binding rAp2_rsp} [@{term rAp2}]

   335   (fn _ => constr_rsp_tac @{thms alpha2_inj} @{thms fv_rtrm2_rsp} @{thms alpha2_equivp} 1) *}

   336 local_setup {* prove_const_rsp @{binding rLm2_rsp} [@{term rLm2}]

   337   (fn _ => constr_rsp_tac @{thms alpha2_inj} @{thms fv_rtrm2_rsp} @{thms alpha2_equivp} 1) *}

   338 local_setup {* prove_const_rsp @{binding rLt2_rsp} [@{term rLt2}]

   339   (fn _ => constr_rsp_tac @{thms alpha2_inj} @{thms fv_rtrm2_rsp rbv2_rsp} @{thms alpha2_equivp} 1) *}

   340 local_setup {* prove_const_rsp @{binding permute_rtrm2_rsp} [@{term "permute :: perm \<Rightarrow> rtrm2 \<Rightarrow> rtrm2"}]

   341   (fn _ => asm_simp_tac (HOL_ss addsimps @{thms alpha2_eqvt}) 1) *}

   342 

   343 

   344 section {*** lets with many assignments ***}

   345 

   346 datatype rtrm3 =

   347   rVr3 "name"

   348 | rAp3 "rtrm3" "rtrm3"

   349 | rLm3 "name" "rtrm3" --"bind (name) in (trm3)"

   350 | rLt3 "rassigns" "rtrm3" --"bind (bv3 assigns) in (trm3)"

   351 and rassigns =

   352   rANil

   353 | rACons "name" "rtrm3" "rassigns"

   354 

   355 (* to be given by the user *)

   356 primrec 

   357   bv3

   358 where

   359   "bv3 rANil = {}"

   360 | "bv3 (rACons x t as) = {atom x} \<union> (bv3 as)"

   361 

   362 setup {* snd o define_raw_perms ["rtrm3", "rassigns"] ["Terms.rtrm3", "Terms.rassigns"] *}

   363 

   364 local_setup {* snd o define_fv_alpha "Terms.rtrm3"

   365   [[[[]], [[], []], [[(NONE, 0)], [(NONE, 0)]], [[], [(SOME @{term bv3}, 0)]]],

   366    [[], [[], [], []]]] *}

   367 print_theorems

   368 

   369 notation

   370   alpha_rtrm3 ("_ \<approx>3 _" [100, 100] 100) and

   371   alpha_rassigns ("_ \<approx>3a _" [100, 100] 100)

   372 thm alpha_rtrm3_alpha_rassigns.intros

   373 

   374 local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha3_inj}, []), (build_alpha_inj @{thms alpha_rtrm3_alpha_rassigns.intros} @{thms rtrm3.distinct rtrm3.inject rassigns.distinct rassigns.inject} @{thms alpha_rtrm3.cases alpha_rassigns.cases} ctxt)) ctxt)) *}

   375 thm alpha3_inj

   376 

   377 lemma alpha3_eqvt:

   378   "t \<approx>3 s \<Longrightarrow> (pi \<bullet> t) \<approx>3 (pi \<bullet> s)"

   379   "a \<approx>3a b \<Longrightarrow> (pi \<bullet> a) \<approx>3a (pi \<bullet> b)"

   380 sorry

   381 

   382 local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha3_equivp}, []),

   383   (build_equivps [@{term alpha_rtrm3}, @{term alpha_rassigns}] @{thm rtrm3_rassigns.induct} @{thm alpha_rtrm3_alpha_rassigns.induct} @{thms rtrm3.inject rassigns.inject} @{thms alpha3_inj} @{thms rtrm3.distinct rassigns.distinct} @{thms alpha_rtrm3.cases alpha_rassigns.cases} @{thms alpha3_eqvt} ctxt)) ctxt)) *}

   384 thm alpha3_equivp

   385 

   386 quotient_type

   387   trm3 = rtrm3 / alpha_rtrm3

   388 and

   389   assigns = rassigns / alpha_rassigns

   390   by (rule alpha3_equivp(1)) (rule alpha3_equivp(2))

   391 

   392 

   393 section {*** lam with indirect list recursion ***}

   394 

   395 datatype rtrm4 =

   396   rVr4 "name"

   397 | rAp4 "rtrm4" "rtrm4 list"

   398 | rLm4 "name" "rtrm4"  --"bind (name) in (trm)"

   399 print_theorems

   400 

   401 thm rtrm4.recs

   402 

   403 (* there cannot be a clause for lists, as *)

   404 (* permutations are  already defined in Nominal (also functions, options, and so on) *)

   405 setup {* snd o define_raw_perms ["rtrm4"] ["Terms.rtrm4"] *}

   406 

   407 (* "repairing" of the permute function *)

   408 lemma repaired:

   409   fixes ts::"rtrm4 list"

   410   shows "permute_rtrm4_list p ts = p \<bullet> ts"

   411   apply(induct ts)

   412   apply(simp_all)

   413   done

   414 

   415 thm permute_rtrm4_permute_rtrm4_list.simps

   416 thm permute_rtrm4_permute_rtrm4_list.simps[simplified repaired]

   417 

   418 local_setup {* snd o define_fv_alpha "Terms.rtrm4" [

   419   [[[]], [[], []], [[(NONE, 0)], [(NONE, 0)]]], [[], [[], []]]  ] *}

   420 print_theorems

   421 

   422 notation

   423   alpha_rtrm4 ("_ \<approx>4 _" [100, 100] 100) and

   424   alpha_rtrm4_list ("_ \<approx>4l _" [100, 100] 100)

   425 thm alpha_rtrm4_alpha_rtrm4_list.intros

   426 

   427 local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha4_inj}, []), (build_alpha_inj @{thms alpha_rtrm4_alpha_rtrm4_list.intros} @{thms rtrm4.distinct rtrm4.inject list.distinct list.inject} @{thms alpha_rtrm4.cases alpha_rtrm4_list.cases} ctxt)) ctxt)) *}

   428 thm alpha4_inj

   429 thm alpha_rtrm4_alpha_rtrm4_list.induct

   430 

   431 local_setup {*

   432 snd o build_eqvts @{binding fv_rtrm4_fv_rtrm4_list_eqvt} [@{term fv_rtrm4}, @{term fv_rtrm4_list}] [@{term "permute :: perm \<Rightarrow> rtrm4 \<Rightarrow> rtrm4"},@{term "permute :: perm \<Rightarrow> rtrm4 list \<Rightarrow> rtrm4 list"}] (@{thms fv_rtrm4_fv_rtrm4_list.simps permute_rtrm4_permute_rtrm4_list.simps[simplified repaired]}) @{thm rtrm4.induct}

   433 *}

   434 print_theorems

   435 

   436 local_setup {*

   437 (fn ctxt => snd (Local_Theory.note ((@{binding alpha4_eqvt}, []),

   438   build_alpha_eqvts [@{term alpha_rtrm4}, @{term alpha_rtrm4_list}] [@{term "permute :: perm \<Rightarrow> rtrm4 \<Rightarrow> rtrm4"},@{term "permute :: perm \<Rightarrow> rtrm4 list \<Rightarrow> rtrm4 list"}] @{thms permute_rtrm4_permute_rtrm4_list.simps[simplified repaired] alpha4_inj} @{thm alpha_rtrm4_alpha_rtrm4_list.induct} ctxt) ctxt))

   439 *}

   440 print_theorems

   441 

   442 local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha4_equivp}, []),

   443   (build_equivps [@{term alpha_rtrm4}, @{term alpha_rtrm4_list}] @{thm rtrm4.induct} @{thm alpha_rtrm4_alpha_rtrm4_list.induct} @{thms rtrm4.inject list.inject} @{thms alpha4_inj} @{thms rtrm4.distinct list.distinct} @{thms alpha_rtrm4_list.cases alpha_rtrm4.cases} @{thms alpha4_eqvt} ctxt)) ctxt)) *}

   444 thm alpha4_equivp

   445 

   446 quotient_type 

   447   qrtrm4 = rtrm4 / alpha_rtrm4 and

   448   qrtrm4list = "rtrm4 list" / alpha_rtrm4_list

   449   by (simp_all add: alpha4_equivp)

   450 

   451 

   452 datatype rtrm5 =

   453   rVr5 "name"

   454 | rAp5 "rtrm5" "rtrm5"

   455 | rLt5 "rlts" "rtrm5" --"bind (bv5 lts) in (rtrm5)"

   456 and rlts =

   457   rLnil

   458 | rLcons "name" "rtrm5" "rlts"

   459 

   460 primrec

   461   rbv5

   462 where

   463   "rbv5 rLnil = {}"

   464 | "rbv5 (rLcons n t ltl) = {atom n} \<union> (rbv5 ltl)"

   465 

   466 

   467 setup {* snd o define_raw_perms ["rtrm5", "rlts"] ["Terms.rtrm5", "Terms.rlts"] *}

   468 print_theorems

   469 

   470 local_setup {* snd o define_fv_alpha "Terms.rtrm5" [

   471   [[[]], [[], []], [[(SOME @{term rbv5}, 0)], [(SOME @{term rbv5}, 0)]]], [[], [[], [], []]]  ] *}

   472 print_theorems

   473 

   474 (* Alternate version with additional binding of name in rlts in rLcons *)

   475 (*local_setup {* snd o define_fv_alpha "Terms.rtrm5" [

   476   [[[]], [[], []], [[(SOME @{term rbv5}, 0)], [(SOME @{term rbv5}, 0)]]], [[], [[(NONE,0)], [], [(NONE,0)]]]  ] *}

   477 print_theorems*)

   478 

   479 notation

   480   alpha_rtrm5 ("_ \<approx>5 _" [100, 100] 100) and

   481   alpha_rlts ("_ \<approx>l _" [100, 100] 100)

   482 thm alpha_rtrm5_alpha_rlts.intros

   483 

   484 local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha5_inj}, []), (build_alpha_inj @{thms alpha_rtrm5_alpha_rlts.intros} @{thms rtrm5.distinct rtrm5.inject rlts.distinct rlts.inject} @{thms alpha_rtrm5.cases alpha_rlts.cases} ctxt)) ctxt)) *}

   485 thm alpha5_inj

   486 

   487 lemma rbv5_eqvt[eqvt]:

   488   "pi \<bullet> (rbv5 x) = rbv5 (pi \<bullet> x)"

   489   apply (induct x)

   490   apply (simp_all add: eqvts atom_eqvt)

   491   done

   492 

   493 lemma fv_rtrm5_rlts_eqvt[eqvt]:

   494   "pi \<bullet> (fv_rtrm5 x) = fv_rtrm5 (pi \<bullet> x)"

   495   "pi \<bullet> (fv_rlts l) = fv_rlts (pi \<bullet> l)"

   496   apply (induct x and l)

   497   apply (simp_all add: eqvts atom_eqvt)

   498   done

   499 

   500 lemma alpha5_eqvt:

   501   "xa \<approx>5 y \<Longrightarrow> (x \<bullet> xa) \<approx>5 (x \<bullet> y)"

   502   "xb \<approx>l ya \<Longrightarrow> (x \<bullet> xb) \<approx>l (x \<bullet> ya)"

   503   apply (induct rule: alpha_rtrm5_alpha_rlts.inducts)

   504   apply (simp_all add: alpha5_inj)

   505   apply (tactic {* 

   506     ALLGOALS (

   507       TRY o REPEAT_ALL_NEW (CHANGED o rtac conjI) THEN_ALL_NEW

   508       (etac @{thm alpha_gen_compose_eqvt})

   509     ) *})

   510   apply (simp_all only: eqvts atom_eqvt)

   511   done

   512 

   513 local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha5_equivp}, []),

   514   (build_equivps [@{term alpha_rtrm5}, @{term alpha_rlts}] @{thm rtrm5_rlts.induct} @{thm alpha_rtrm5_alpha_rlts.induct} @{thms rtrm5.inject rlts.inject} @{thms alpha5_inj} @{thms rtrm5.distinct rlts.distinct} @{thms alpha_rtrm5.cases alpha_rlts.cases} @{thms alpha5_eqvt} ctxt)) ctxt)) *}

   515 thm alpha5_equivp

   516 

   517 quotient_type

   518   trm5 = rtrm5 / alpha_rtrm5

   519 and

   520   lts = rlts / alpha_rlts

   521   by (auto intro: alpha5_equivp)

   522 

   523 local_setup {*

   524 (fn ctxt => ctxt

   525  |> snd o (Quotient_Def.quotient_lift_const ("Vr5", @{term rVr5}))

   526  |> snd o (Quotient_Def.quotient_lift_const ("Ap5", @{term rAp5}))

   527  |> snd o (Quotient_Def.quotient_lift_const ("Lt5", @{term rLt5}))

   528  |> snd o (Quotient_Def.quotient_lift_const ("Lnil", @{term rLnil}))

   529  |> snd o (Quotient_Def.quotient_lift_const ("Lcons", @{term rLcons}))

   530  |> snd o (Quotient_Def.quotient_lift_const ("fv_trm5", @{term fv_rtrm5}))

   531  |> snd o (Quotient_Def.quotient_lift_const ("fv_lts", @{term fv_rlts}))

   532  |> snd o (Quotient_Def.quotient_lift_const ("bv5", @{term rbv5})))

   533 *}

   534 print_theorems

   535 

   536 lemma alpha5_rfv:

   537   "(t \<approx>5 s \<Longrightarrow> fv_rtrm5 t = fv_rtrm5 s)"

   538   "(l \<approx>l m \<Longrightarrow> fv_rlts l = fv_rlts m)"

   539   apply(induct rule: alpha_rtrm5_alpha_rlts.inducts)

   540   apply(simp_all add: alpha_gen)

   541   done

   542 

   543 lemma bv_list_rsp:

   544   shows "x \<approx>l y \<Longrightarrow> rbv5 x = rbv5 y"

   545   apply(induct rule: alpha_rtrm5_alpha_rlts.inducts(2))

   546   apply(simp_all)

   547   done

   548 

   549 lemma [quot_respect]:

   550   "(alpha_rlts ===> op =) fv_rlts fv_rlts"

   551   "(alpha_rtrm5 ===> op =) fv_rtrm5 fv_rtrm5"

   552   "(alpha_rlts ===> op =) rbv5 rbv5"

   553   "(op = ===> alpha_rtrm5) rVr5 rVr5"

   554   "(alpha_rtrm5 ===> alpha_rtrm5 ===> alpha_rtrm5) rAp5 rAp5"

   555   "(alpha_rlts ===> alpha_rtrm5 ===> alpha_rtrm5) rLt5 rLt5"

   556   "(op = ===> alpha_rtrm5 ===> alpha_rlts ===> alpha_rlts) rLcons rLcons"

   557   "(op = ===> alpha_rtrm5 ===> alpha_rtrm5) permute permute"

   558   "(op = ===> alpha_rlts ===> alpha_rlts) permute permute"

   559   apply (simp_all add: alpha5_inj alpha5_rfv alpha5_eqvt bv_list_rsp)

   560   apply (clarify) apply (rule conjI)

   561   apply (rule_tac x="0" in exI) apply (simp add: fresh_star_def fresh_zero_perm alpha_gen alpha5_rfv)

   562   apply (rule_tac x="0" in exI) apply (simp add: fresh_star_def fresh_zero_perm alpha_gen alpha5_rfv)

   563   done

   564 

   565 lemma

   566   shows "(alpha_rlts ===> op =) rbv5 rbv5"

   567   by (simp add: bv_list_rsp)

   568 

   569 lemmas trm5_lts_inducts = rtrm5_rlts.inducts[quot_lifted]

   570 

   571 instantiation trm5 and lts :: pt

   572 begin

   573 

   574 quotient_definition

   575   "permute_trm5 :: perm \<Rightarrow> trm5 \<Rightarrow> trm5"

   576 is

   577   "permute :: perm \<Rightarrow> rtrm5 \<Rightarrow> rtrm5"

   578 

   579 quotient_definition

   580   "permute_lts :: perm \<Rightarrow> lts \<Rightarrow> lts"

   581 is

   582   "permute :: perm \<Rightarrow> rlts \<Rightarrow> rlts"

   583 

   584 instance by default

   585   (simp_all add: permute_rtrm5_permute_rlts_zero[quot_lifted] permute_rtrm5_permute_rlts_append[quot_lifted])

   586 

   587 end

   588 

   589 lemmas

   590     permute_trm5_lts = permute_rtrm5_permute_rlts.simps[quot_lifted]

   591 and alpha5_INJ = alpha5_inj[unfolded alpha_gen, quot_lifted, folded alpha_gen]

   592 and bv5[simp] = rbv5.simps[quot_lifted]

   593 and fv_trm5_lts[simp] = fv_rtrm5_fv_rlts.simps[quot_lifted]

   594 

   595 lemma lets_ok:

   596   "(Lt5 (Lcons x (Vr5 x) Lnil) (Vr5 x)) = (Lt5 (Lcons y (Vr5 y) Lnil) (Vr5 y))"

   597 apply (subst alpha5_INJ)

   598 apply (rule conjI)

   599 apply (rule_tac x="(x \<leftrightarrow> y)" in exI)

   600 apply (simp only: alpha_gen)

   601 apply (simp add: permute_trm5_lts fresh_star_def)

   602 apply (rule_tac x="(x \<leftrightarrow> y)" in exI)

   603 apply (simp only: alpha_gen)

   604 apply (simp add: permute_trm5_lts fresh_star_def)

   605 done

   606 

   607 lemma lets_ok2:

   608   "(Lt5 (Lcons x (Vr5 x) (Lcons y (Vr5 y) Lnil)) (Ap5 (Vr5 x) (Vr5 y))) =

   609    (Lt5 (Lcons y (Vr5 y) (Lcons x (Vr5 x) Lnil)) (Ap5 (Vr5 x) (Vr5 y)))"

   610 apply (subst alpha5_INJ)

   611 apply (rule conjI)

   612 apply (rule_tac x="(x \<leftrightarrow> y)" in exI)

   613 apply (simp only: alpha_gen)

   614 apply (simp add: permute_trm5_lts fresh_star_def)

   615 apply (rule_tac x="0 :: perm" in exI)

   616 apply (simp only: alpha_gen)

   617 apply (simp add: permute_trm5_lts fresh_star_def)

   618 done

   619 

   620 

   621 lemma lets_not_ok1:

   622   "x \<noteq> y \<Longrightarrow> (Lt5 (Lcons x (Vr5 x) (Lcons y (Vr5 y) Lnil)) (Ap5 (Vr5 x) (Vr5 y))) \<noteq>

   623              (Lt5 (Lcons y (Vr5 x) (Lcons x (Vr5 y) Lnil)) (Ap5 (Vr5 x) (Vr5 y)))"

   624 apply (simp add: alpha5_INJ(3) alpha_gen)

   625 apply (simp add: permute_trm5_lts fresh_star_def alpha5_INJ(5) alpha5_INJ(2) alpha5_INJ(1))

   626 done

   627 

   628 lemma distinct_helper:

   629   shows "\<not>(rVr5 x \<approx>5 rAp5 y z)"

   630   apply auto

   631   apply (erule alpha_rtrm5.cases)

   632   apply (simp_all only: rtrm5.distinct)

   633   done

   634 

   635 lemma distinct_helper2:

   636   shows "(Vr5 x) \<noteq> (Ap5 y z)"

   637   by (lifting distinct_helper)

   638 

   639 lemma lets_nok:

   640   "x \<noteq> y \<Longrightarrow> x \<noteq> z \<Longrightarrow> z \<noteq> y \<Longrightarrow>

   641    (Lt5 (Lcons x (Ap5 (Vr5 z) (Vr5 z)) (Lcons y (Vr5 z) Lnil)) (Ap5 (Vr5 x) (Vr5 y))) \<noteq>

   642    (Lt5 (Lcons y (Vr5 z) (Lcons x (Ap5 (Vr5 z) (Vr5 z)) Lnil)) (Ap5 (Vr5 x) (Vr5 y)))"

   643 apply (simp only: alpha5_INJ(3) alpha5_INJ(5) alpha_gen permute_trm5_lts fresh_star_def)

   644 apply (simp add: distinct_helper2)

   645 done

   646 

   647 

   648 (* example with a bn function defined over the type itself *)

   649 datatype rtrm6 =

   650   rVr6 "name"

   651 | rLm6 "name" "rtrm6" --"bind name in rtrm6"

   652 | rLt6 "rtrm6" "rtrm6" --"bind (bv6 left) in (right)"

   653 

   654 primrec

   655   rbv6

   656 where

   657   "rbv6 (rVr6 n) = {}"

   658 | "rbv6 (rLm6 n t) = {atom n} \<union> rbv6 t"

   659 | "rbv6 (rLt6 l r) = rbv6 l \<union> rbv6 r"

   660 

   661 setup {* snd o define_raw_perms ["rtrm6"] ["Terms.rtrm6"] *}

   662 print_theorems

   663 

   664 local_setup {* snd o define_fv_alpha "Terms.rtrm6" [

   665   [[[]], [[(NONE, 0)], [(NONE, 0)]], [[], [(SOME @{term rbv6}, 0)]]]] *}

   666 notation alpha_rtrm6 ("_ \<approx>6 _" [100, 100] 100)

   667 (* HERE THE RULES DIFFER *)

   668 thm alpha_rtrm6.intros

   669 

   670 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)) *}

   671 thm alpha6_inj

   672 

   673 lemma alpha6_eqvt:

   674   "xa \<approx>6 y \<Longrightarrow> (x \<bullet> xa) \<approx>6 (x \<bullet> y)"

   675 sorry

   676 

   677 local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha6_equivp}, []),

   678   (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)) *}

   679 thm alpha6_equivp

   680 

   681 quotient_type

   682   trm6 = rtrm6 / alpha_rtrm6

   683   by (auto intro: alpha6_equivp)

   684 

   685 local_setup {*

   686 (fn ctxt => ctxt

   687  |> snd o (Quotient_Def.quotient_lift_const ("Vr6", @{term rVr6}))

   688  |> snd o (Quotient_Def.quotient_lift_const ("Lm6", @{term rLm6}))

   689  |> snd o (Quotient_Def.quotient_lift_const ("Lt6", @{term rLt6}))

   690  |> snd o (Quotient_Def.quotient_lift_const ("fv_trm6", @{term fv_rtrm6}))

   691  |> snd o (Quotient_Def.quotient_lift_const ("bv6", @{term rbv6})))

   692 *}

   693 print_theorems

   694 

   695 lemma [quot_respect]:

   696   "(op = ===> alpha_rtrm6 ===> alpha_rtrm6) permute permute"

   697 by (auto simp add: alpha6_eqvt)

   698 

   699 (* Definitely not true , see lemma below *)

   700 lemma [quot_respect]:"(alpha_rtrm6 ===> op =) rbv6 rbv6"

   701 apply simp apply clarify

   702 apply (erule alpha_rtrm6.induct)

   703 oops

   704 

   705 lemma "(a :: name) \<noteq> b \<Longrightarrow> \<not> (alpha_rtrm6 ===> op =) rbv6 rbv6"

   706 apply simp

   707 apply (rule_tac x="rLm6 (a::name) (rVr6 (a :: name))" in  exI)

   708 apply (rule_tac x="rLm6 (b::name) (rVr6 (b :: name))" in  exI)

   709 apply simp

   710 apply (simp add: alpha6_inj)

   711 apply (rule_tac x="(a \<leftrightarrow> b)" in  exI)

   712 apply (simp add: alpha_gen fresh_star_def)

   713 apply (simp add: alpha6_inj)

   714 done

   715 

   716 lemma fv6_rsp: "x \<approx>6 y \<Longrightarrow> fv_rtrm6 x = fv_rtrm6 y"

   717 apply (induct_tac x y rule: alpha_rtrm6.induct)

   718 apply simp_all

   719 apply (erule exE)

   720 apply (simp_all add: alpha_gen)

   721 done

   722 

   723 lemma [quot_respect]:"(alpha_rtrm6 ===> op =) fv_rtrm6 fv_rtrm6"

   724 by (simp add: fv6_rsp)

   725 

   726 lemma [quot_respect]:

   727  "(op = ===> alpha_rtrm6) rVr6 rVr6"

   728  "(op = ===> alpha_rtrm6 ===> alpha_rtrm6) rLm6 rLm6"

   729 apply auto

   730 apply (simp_all add: alpha6_inj)

   731 apply (rule_tac x="0::perm" in exI)

   732 apply (simp add: alpha_gen fv6_rsp fresh_star_def fresh_zero_perm)

   733 done

   734 

   735 lemma [quot_respect]:

   736  "(alpha_rtrm6 ===> alpha_rtrm6 ===> alpha_rtrm6) rLt6 rLt6"

   737 apply auto

   738 apply (simp_all add: alpha6_inj)

   739 apply (rule_tac [!] x="0::perm" in exI)

   740 apply (simp_all add: alpha_gen fresh_star_def fresh_zero_perm)

   741 (* needs rbv6_rsp *)

   742 oops

   743 

   744 instantiation trm6 :: pt begin

   745 

   746 quotient_definition

   747   "permute_trm6 :: perm \<Rightarrow> trm6 \<Rightarrow> trm6"

   748 is

   749   "permute :: perm \<Rightarrow> rtrm6 \<Rightarrow> rtrm6"

   750 

   751 instance

   752 apply default

   753 sorry

   754 end

   755 

   756 lemma lifted_induct:

   757 "\<lbrakk>x1 = x2; \<And>name namea. name = namea \<Longrightarrow> P (Vr6 name) (Vr6 namea);

   758  \<And>name rtrm6 namea rtrm6a.

   759     \<lbrakk>True;

   760      \<exists>pi. fv_trm6 rtrm6 - {atom name} = fv_trm6 rtrm6a - {atom namea} \<and>

   761           (fv_trm6 rtrm6 - {atom name}) \<sharp>* pi \<and> pi \<bullet> rtrm6 = rtrm6a \<and> P (pi \<bullet> rtrm6) rtrm6a\<rbrakk>

   762     \<Longrightarrow> P (Lm6 name rtrm6) (Lm6 namea rtrm6a);

   763  \<And>rtrm61 rtrm61a rtrm62 rtrm62a.

   764     \<lbrakk>rtrm61 = rtrm61a; P rtrm61 rtrm61a;

   765      \<exists>pi. fv_trm6 rtrm62 - bv6 rtrm61 = fv_trm6 rtrm62a - bv6 rtrm61a \<and>

   766           (fv_trm6 rtrm62 - bv6 rtrm61) \<sharp>* pi \<and> pi \<bullet> rtrm62 = rtrm62a \<and> P (pi \<bullet> rtrm62) rtrm62a\<rbrakk>

   767     \<Longrightarrow> P (Lt6 rtrm61 rtrm62) (Lt6 rtrm61a rtrm62a)\<rbrakk>

   768 \<Longrightarrow> P x1 x2"

   769 apply (lifting alpha_rtrm6.induct[unfolded alpha_gen])

   770 apply injection

   771 (* notice unsolvable goals: (alpha_rtrm6 ===> op =) rbv6 rbv6 *)

   772 oops

   773 

   774 lemma lifted_inject_a3:

   775 "(Lt6 rtrm61 rtrm62 = Lt6 rtrm61a rtrm62a) =

   776 (rtrm61 = rtrm61a \<and>

   777  (\<exists>pi. fv_trm6 rtrm62 - bv6 rtrm61 = fv_trm6 rtrm62a - bv6 rtrm61a \<and>

   778        (fv_trm6 rtrm62 - bv6 rtrm61) \<sharp>* pi \<and> pi \<bullet> rtrm62 = rtrm62a))"

   779 apply(lifting alpha6_inj(3)[unfolded alpha_gen])

   780 apply injection

   781 (* notice unsolvable goals: (alpha_rtrm6 ===> op =) rbv6 rbv6 *)

   782 oops

   783 

   784 

   785 

   786 

   787 (* example with a respectful bn function defined over the type itself *)

   788 

   789 datatype rtrm7 =

   790   rVr7 "name"

   791 | rLm7 "name" "rtrm7" --"bind left in right"

   792 | rLt7 "rtrm7" "rtrm7" --"bind (bv7 left) in (right)"

   793 

   794 primrec

   795   rbv7

   796 where

   797   "rbv7 (rVr7 n) = {atom n}"

   798 | "rbv7 (rLm7 n t) = rbv7 t - {atom n}"

   799 | "rbv7 (rLt7 l r) = rbv7 l \<union> rbv7 r"

   800 

   801 setup {* snd o define_raw_perms ["rtrm7"] ["Terms.rtrm7"] *}

   802 thm permute_rtrm7.simps

   803 

   804 local_setup {* snd o define_fv_alpha "Terms.rtrm7" [

   805   [[[]], [[(NONE, 0)], [(NONE, 0)]], [[], [(SOME @{term rbv7}, 0)]]]] *}

   806 print_theorems

   807 notation

   808   alpha_rtrm7 ("_ \<approx>7a _" [100, 100] 100)

   809 (* HERE THE RULES DIFFER *)

   810 thm alpha_rtrm7.intros

   811 thm fv_rtrm7.simps

   812 inductive

   813   alpha7 :: "rtrm7 \<Rightarrow> rtrm7 \<Rightarrow> bool" ("_ \<approx>7 _" [100, 100] 100)

   814 where

   815   a1: "a = b \<Longrightarrow> (rVr7 a) \<approx>7 (rVr7 b)"

   816 | a2: "(\<exists>pi. (({atom a}, t) \<approx>gen alpha7 fv_rtrm7 pi ({atom b}, s))) \<Longrightarrow> rLm7 a t \<approx>7 rLm7 b s"

   817 | a3: "(\<exists>pi. (((rbv7 t1), s1) \<approx>gen alpha7 fv_rtrm7 pi ((rbv7 t2), s2))) \<Longrightarrow> rLt7 t1 s1 \<approx>7 rLt7 t2 s2"

   818 

   819 lemma "(x::name) \<noteq> y \<Longrightarrow> \<not> (alpha7 ===> op =) rbv7 rbv7"

   820   apply simp

   821   apply (rule_tac x="rLt7 (rVr7 x) (rVr7 x)" in exI)

   822   apply (rule_tac x="rLt7 (rVr7 y) (rVr7 y)" in exI)

   823   apply simp

   824   apply (rule a3)

   825   apply (rule_tac x="(x \<leftrightarrow> y)" in exI)

   826   apply (simp_all add: alpha_gen fresh_star_def)

   827   apply (rule a1)

   828   apply (rule refl)

   829 done

   830 

   831 

   832 

   833 

   834 

   835 datatype rfoo8 =

   836   Foo0 "name"

   837 | Foo1 "rbar8" "rfoo8" --"bind bv(bar) in foo"

   838 and rbar8 =

   839   Bar0 "name"

   840 | Bar1 "name" "name" "rbar8" --"bind second name in b"

   841 

   842 primrec

   843   rbv8

   844 where

   845   "rbv8 (Bar0 x) = {}"

   846 | "rbv8 (Bar1 v x b) = {atom v}"

   847 

   848 setup {* snd o define_raw_perms ["rfoo8", "rbar8"] ["Terms.rfoo8", "Terms.rbar8"] *}

   849 print_theorems

   850 

   851 local_setup {* snd o define_fv_alpha "Terms.rfoo8" [

   852   [[[]], [[], [(SOME @{term rbv8}, 0)]]], [[[]], [[], [(NONE, 1)], [(NONE, 1)]]]] *}

   853 notation

   854   alpha_rfoo8 ("_ \<approx>f' _" [100, 100] 100) and

   855   alpha_rbar8 ("_ \<approx>b' _" [100, 100] 100)

   856 (* HERE THE RULE DIFFERS *)

   857 thm alpha_rfoo8_alpha_rbar8.intros

   858 

   859 

   860 inductive

   861   alpha8f :: "rfoo8 \<Rightarrow> rfoo8 \<Rightarrow> bool" ("_ \<approx>f _" [100, 100] 100)

   862 and

   863   alpha8b :: "rbar8 \<Rightarrow> rbar8 \<Rightarrow> bool" ("_ \<approx>b _" [100, 100] 100)

   864 where

   865   a1: "a = b \<Longrightarrow> (Foo0 a) \<approx>f (Foo0 b)"

   866 | a2: "a = b \<Longrightarrow> (Bar0 a) \<approx>b (Bar0 b)"

   867 | a3: "b1 \<approx>b b2 \<Longrightarrow> (\<exists>pi. (((rbv8 b1), t1) \<approx>gen alpha8f fv_rfoo8 pi ((rbv8 b2), t2))) \<Longrightarrow> Foo1 b1 t1 \<approx>f Foo1 b2 t2"

   868 | a4: "v1 = v2 \<Longrightarrow> (\<exists>pi. (({atom x1}, t1) \<approx>gen alpha8b fv_rbar8 pi ({atom x2}, t2))) \<Longrightarrow> Bar1 v1 x1 t1 \<approx>b Bar1 v2 x2 t2"

   869 

   870 lemma "(alpha8b ===> op =) rbv8 rbv8"

   871   apply simp apply clarify

   872   apply (erule alpha8f_alpha8b.inducts(2))

   873   apply (simp_all)

   874 done

   875 

   876 lemma fv_rbar8_rsp_hlp: "x \<approx>b y \<Longrightarrow> fv_rbar8 x = fv_rbar8 y"

   877   apply (erule alpha8f_alpha8b.inducts(2))

   878   apply (simp_all add: alpha_gen)

   879 done

   880 lemma "(alpha8b ===> op =) fv_rbar8 fv_rbar8"

   881   apply simp apply clarify apply (simp add: fv_rbar8_rsp_hlp)

   882 done

   883 

   884 lemma "(alpha8f ===> op =) fv_rfoo8 fv_rfoo8"

   885   apply simp apply clarify

   886   apply (erule alpha8f_alpha8b.inducts(1))

   887   apply (simp_all add: alpha_gen fv_rbar8_rsp_hlp)

   888 done

   889 

   890 

   891 

   892 

   893 

   894 

   895 datatype rlam9 =

   896   Var9 "name"

   897 | Lam9 "name" "rlam9" --"bind name in rlam"

   898 and rbla9 =

   899   Bla9 "rlam9" "rlam9" --"bind bv(first) in second"

   900 

   901 primrec

   902   rbv9

   903 where

   904   "rbv9 (Var9 x) = {}"

   905 | "rbv9 (Lam9 x b) = {atom x}"

   906 

   907 setup {* snd o define_raw_perms ["rlam9", "rbla9"] ["Terms.rlam9", "Terms.rbla9"] *}

   908 print_theorems

   909 

   910 local_setup {* snd o define_fv_alpha "Terms.rlam9" [

   911   [[[]], [[(NONE, 0)], [(NONE, 0)]]], [[[], [(SOME @{term rbv9}, 0)]]]] *}

   912 notation

   913   alpha_rlam9 ("_ \<approx>9l' _" [100, 100] 100) and

   914   alpha_rbla9 ("_ \<approx>9b' _" [100, 100] 100)

   915 (* HERE THE RULES DIFFER *)

   916 thm alpha_rlam9_alpha_rbla9.intros

   917 

   918 

   919 inductive

   920   alpha9l :: "rlam9 \<Rightarrow> rlam9 \<Rightarrow> bool" ("_ \<approx>9l _" [100, 100] 100)

   921 and

   922   alpha9b :: "rbla9 \<Rightarrow> rbla9 \<Rightarrow> bool" ("_ \<approx>9b _" [100, 100] 100)

   923 where

   924   a1: "a = b \<Longrightarrow> (Var9 a) \<approx>9l (Var9 b)"

   925 | a4: "(\<exists>pi. (({atom x1}, t1) \<approx>gen alpha9l fv_rlam9 pi ({atom x2}, t2))) \<Longrightarrow> Lam9 x1 t1 \<approx>9l Lam9 x2 t2"

   926 | 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"

   927 

   928 quotient_type

   929   lam9 = rlam9 / alpha9l and bla9 = rbla9 / alpha9b

   930 sorry

   931 

   932 local_setup {*

   933 (fn ctxt => ctxt

   934  |> snd o (Quotient_Def.quotient_lift_const ("qVar9", @{term Var9}))

   935  |> snd o (Quotient_Def.quotient_lift_const ("qLam9", @{term Lam9}))

   936  |> snd o (Quotient_Def.quotient_lift_const ("qBla9", @{term Bla9}))

   937  |> snd o (Quotient_Def.quotient_lift_const ("fv_lam9", @{term fv_rlam9}))

   938  |> snd o (Quotient_Def.quotient_lift_const ("fv_bla9", @{term fv_rbla9}))

   939  |> snd o (Quotient_Def.quotient_lift_const ("bv9", @{term rbv9})))

   940 *}

   941 print_theorems

   942 

   943 instantiation lam9 and bla9 :: pt

   944 begin

   945 

   946 quotient_definition

   947   "permute_lam9 :: perm \<Rightarrow> lam9 \<Rightarrow> lam9"

   948 is

   949   "permute :: perm \<Rightarrow> rlam9 \<Rightarrow> rlam9"

   950 

   951 quotient_definition

   952   "permute_bla9 :: perm \<Rightarrow> bla9 \<Rightarrow> bla9"

   953 is

   954   "permute :: perm \<Rightarrow> rbla9 \<Rightarrow> rbla9"

   955 

   956 instance

   957 sorry

   958 

   959 end

   960 

   961 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>

   962  \<Longrightarrow> qBla9 b1 t1 = qBla9 b2 t2"

   963 apply (lifting a3[unfolded alpha_gen])

   964 apply injection

   965 sorry

   966 

   967 

   968 

   969 

   970 

   971 

   972 

   973 

   974 text {* type schemes *} 

   975 datatype ty = 

   976   Var "name" 

   977 | Fun "ty" "ty"

   978 

   979 setup {* snd o define_raw_perms ["ty"] ["Terms.ty"] *}

   980 print_theorems

   981 

   982 datatype tyS = 

   983   All "name set" "ty" 

   984 

   985 setup {* snd o define_raw_perms ["tyS"] ["Terms.tyS"] *}

   986 print_theorems

   987 

   988 local_setup {* snd o define_fv_alpha "Terms.ty" [[[[]], [[], []]]] *}

   989 print_theorems 

   990 

   991 (*

   992 Doesnot work yet since we do not refer to fv_ty

   993 local_setup {* define_raw_fv "Terms.tyS" [[[[], []]]] *}

   994 print_theorems

   995 *)

   996 

   997 primrec

   998   fv_tyS

   999 where 

  1000   "fv_tyS (All xs T) = (fv_ty T - atom ` xs)"

  1001 

  1002 inductive

  1003   alpha_tyS :: "tyS \<Rightarrow> tyS \<Rightarrow> bool" ("_ \<approx>tyS _" [100, 100] 100)

  1004 where

  1005   a1: "\<exists>pi. ((atom ` xs1, T1) \<approx>gen (op =) fv_ty pi (atom ` xs2, T2)) 

  1006         \<Longrightarrow> All xs1 T1 \<approx>tyS All xs2 T2"

  1007 

  1008 lemma

  1009   shows "All {a, b} (Fun (Var a) (Var b)) \<approx>tyS All {b, a} (Fun (Var a) (Var b))"

  1010   apply(rule a1)

  1011   apply(simp add: alpha_gen)

  1012   apply(rule_tac x="0::perm" in exI)

  1013   apply(simp add: fresh_star_def)

  1014   done

  1015 

  1016 lemma

  1017   shows "All {a, b} (Fun (Var a) (Var b)) \<approx>tyS All {a, b} (Fun (Var b) (Var a))"

  1018   apply(rule a1)

  1019   apply(simp add: alpha_gen)

  1020   apply(rule_tac x="(atom a \<rightleftharpoons> atom b)" in exI)

  1021   apply(simp add: fresh_star_def)

  1022   done

  1023 

  1024 lemma

  1025   shows "All {a, b, c} (Fun (Var a) (Var b)) \<approx>tyS All {a, b} (Fun (Var a) (Var b))"

  1026   apply(rule a1)

  1027   apply(simp add: alpha_gen)

  1028   apply(rule_tac x="0::perm" in exI)

  1029   apply(simp add: fresh_star_def)

  1030   done

  1031 

  1032 lemma

  1033   assumes a: "a \<noteq> b"

  1034   shows "\<not>(All {a, b} (Fun (Var a) (Var b)) \<approx>tyS All {c} (Fun (Var c) (Var c)))"

  1035   using a

  1036   apply(clarify)

  1037   apply(erule alpha_tyS.cases)

  1038   apply(simp add: alpha_gen)

  1039   apply(erule conjE)+

  1040   apply(erule exE)

  1041   apply(erule conjE)+

  1042   apply(clarify)

  1043   apply(simp)

  1044   apply(simp add: fresh_star_def)

  1045   apply(auto)

  1046   done

  1047 

  1048 

  1049 end