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 lemma bv1_eqvt[eqvt]:

    66   shows "(pi \<bullet> bv1 x) = bv1 (pi \<bullet> x)"

    67   apply (induct x)

    68   apply (simp_all add: atom_eqvt eqvts)

    69   done

    70 

    71 lemma fv_rtrm1_eqvt[eqvt]:

    72     "(pi\<bullet>fv_rtrm1 t) = fv_rtrm1 (pi\<bullet>t)"

    73     "(pi\<bullet>fv_bp b) = fv_bp (pi\<bullet>b)"

    74   apply (induct t and b)

    75   apply (simp_all add: insert_eqvt atom_eqvt empty_eqvt union_eqvt Diff_eqvt bv1_eqvt)

    76   done

    77 

    78 lemma alpha1_eqvt:

    79   "t \<approx>1 s \<Longrightarrow> (pi \<bullet> t) \<approx>1 (pi \<bullet> s)"

    80   "alpha_bp a b \<Longrightarrow> alpha_bp (pi \<bullet> a) (pi \<bullet> b)"

    81   apply (induct t s and a b rule: alpha_rtrm1_alpha_bp.inducts)

    82   apply (simp_all add:eqvts alpha1_inj)

    83   apply (erule exE)

    84   apply (rule_tac x="pi \<bullet> pia" in exI)

    85   apply (simp add: alpha_gen)

    86   apply(erule conjE)+

    87   apply(rule conjI)

    88   apply(rule_tac ?p1="- pi" in permute_eq_iff[THEN iffD1])

    89   apply(simp add: atom_eqvt Diff_eqvt insert_eqvt empty_eqvt fv_rtrm1_eqvt)

    90   apply(rule conjI)

    91   apply(rule_tac ?p1="- pi" in fresh_star_permute_iff[THEN iffD1])

    92   apply(simp add: atom_eqvt Diff_eqvt fv_rtrm1_eqvt insert_eqvt empty_eqvt)

    93   apply(simp add: permute_eqvt[symmetric])

    94   apply (erule exE)

    95   apply (erule exE)

    96   apply (rule conjI)

    97   apply (rule_tac x="pi \<bullet> pia" in exI)

    98   apply (simp add: alpha_gen)

    99   apply(erule conjE)+

   100   apply(rule conjI)

   101   apply(rule_tac ?p1="- pi" in permute_eq_iff[THEN iffD1])

   102   apply(simp add: fv_rtrm1_eqvt Diff_eqvt bv1_eqvt)

   103   apply(rule conjI)

   104   apply(rule_tac ?p1="- pi" in fresh_star_permute_iff[THEN iffD1])

   105   apply(simp add: atom_eqvt fv_rtrm1_eqvt Diff_eqvt bv1_eqvt)

   106   apply(simp add: permute_eqvt[symmetric])

   107   apply (rule_tac x="pi \<bullet> piaa" in exI)

   108   apply (simp add: alpha_gen)

   109   apply(erule conjE)+

   110   apply(rule conjI)

   111   apply(rule_tac ?p1="- pi" in permute_eq_iff[THEN iffD1])

   112   apply(simp add: fv_rtrm1_eqvt Diff_eqvt bv1_eqvt)

   113   apply(rule conjI)

   114   apply(rule_tac ?p1="- pi" in fresh_star_permute_iff[THEN iffD1])

   115   apply(simp add: atom_eqvt fv_rtrm1_eqvt Diff_eqvt bv1_eqvt)

   116   apply(simp add: permute_eqvt[symmetric])

   117   done

   118 

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

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

   121 thm alpha1_equivp

   122 

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

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

   125 

   126 local_setup {*

   127 (fn ctxt => ctxt

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

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

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

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

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

   133 *}

   134 print_theorems

   135 

   136 thm alpha_rtrm1_alpha_bp.induct

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

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

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

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

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

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

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

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

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

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

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

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

   149 

   150 lemmas trm1_bp_induct = rtrm1_bp.induct[quot_lifted]

   151 lemmas trm1_bp_inducts = rtrm1_bp.inducts[quot_lifted]

   152 

   153 instantiation trm1 and bp :: pt

   154 begin

   155 

   156 quotient_definition

   157   "permute_trm1 :: perm \<Rightarrow> trm1 \<Rightarrow> trm1"

   158 is

   159   "permute :: perm \<Rightarrow> rtrm1 \<Rightarrow> rtrm1"

   160 

   161 instance by default 

   162   (simp_all add: permute_rtrm1_permute_bp_zero[quot_lifted] permute_rtrm1_permute_bp_append[quot_lifted])

   163 

   164 end

   165 

   166 lemmas

   167     permute_trm1 = permute_rtrm1_permute_bp.simps[quot_lifted]

   168 and fv_trm1 = fv_rtrm1_fv_bp.simps[quot_lifted]

   169 and fv_trm1_eqvt = fv_rtrm1_eqvt[quot_lifted]

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

   171 

   172 lemma supports:

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

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

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

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

   177   "{} supports BUnit"

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

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

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

   181 apply(rule_tac [!] allI)+

   182 apply(rule_tac [!] impI)

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

   184 apply(simp_all add: fresh_atom)

   185 done

   186 

   187 lemma rtrm1_bp_fs:

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

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

   190   apply (induct x and b rule: trm1_bp_inducts)

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

   192   apply(simp_all add: supp_atom)

   193   done

   194 

   195 instance trm1 :: fs

   196 apply default

   197 apply (rule rtrm1_bp_fs(1))

   198 done

   199 

   200 lemma fv_eq_bv: "fv_bp bp = bv1 bp"

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

   202 apply(simp_all)

   203 done

   204 

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

   206 apply auto

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

   208 apply auto

   209 done

   210 

   211 lemma supp_fv:

   212   "supp t = fv_trm1 t"

   213   "supp b = fv_bp b"

   214 apply(induct t and b rule: trm1_bp_inducts)

   215 apply(simp_all)

   216 apply(simp add: supp_def permute_trm1 alpha1_INJ fv_trm1)

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

   218 apply(simp add: supp_def permute_trm1 alpha1_INJ fv_trm1)

   219 apply(simp add: Collect_imp_eq Collect_neg_eq)

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

   221 apply(simp add: supp_Abs fv_trm1)

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

   223 apply(simp add: alpha1_INJ)

   224 apply(simp add: Abs_eq_iff)

   225 apply(simp add: alpha_gen.simps)

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

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

   228 apply(simp add: supp_Abs fv_trm1 fv_eq_bv)

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

   230 apply(simp add: alpha1_INJ alpha_bp_eq)

   231 apply(simp add: Abs_eq_iff)

   232 apply(simp add: alpha_gen)

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

   234 apply(simp add: Collect_imp_eq Collect_neg_eq fresh_star_def helper2)

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

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

   237 apply(fold supp_def)

   238 apply(simp add: supp_at_base)

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

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

   241 done

   242 

   243 lemma trm1_supp:

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

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

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

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

   248 by (simp_all add: supp_fv fv_trm1 fv_eq_bv)

   249 

   250 lemma trm1_induct_strong:

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

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

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

   254   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)"

   255   shows   "P a rtrma"

   256 sorry

   257 

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

   259 

   260 datatype rtrm2 =

   261   rVr2 "name"

   262 | rAp2 "rtrm2" "rtrm2"

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

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

   265 and rassign =

   266   rAs "name" "rtrm2"

   267 

   268 (* to be given by the user *)

   269 primrec 

   270   rbv2

   271 where

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

   273 

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

   275 

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

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

   278    [[[], []]]] *}

   279 

   280 notation

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

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

   283 thm alpha_rtrm2_alpha_rassign.intros

   284 

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

   286 thm alpha2_inj

   287 

   288 lemma alpha2_eqvt:

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

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

   291 sorry

   292 

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

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

   295 thm alpha2_equivp

   296 

   297 local_setup  {* define_quotient_type 

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

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

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

   301 

   302 local_setup {*

   303 (fn ctxt => ctxt

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

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

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

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

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

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

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

   311 *}

   312 print_theorems

   313 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

   328 

   329 

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

   331 

   332 datatype rtrm3 =

   333   rVr3 "name"

   334 | rAp3 "rtrm3" "rtrm3"

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

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

   337 and rassigns =

   338   rANil

   339 | rACons "name" "rtrm3" "rassigns"

   340 

   341 (* to be given by the user *)

   342 primrec 

   343   bv3

   344 where

   345   "bv3 rANil = {}"

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

   347 

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

   349 

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

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

   352    [[], [[], [], []]]] *}

   353 print_theorems

   354 

   355 notation

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

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

   358 thm alpha_rtrm3_alpha_rassigns.intros

   359 

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

   361 thm alpha3_inj

   362 

   363 lemma alpha3_eqvt:

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

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

   366 sorry

   367 

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

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

   370 thm alpha3_equivp

   371 

   372 quotient_type

   373   trm3 = rtrm3 / alpha_rtrm3

   374 and

   375   assigns = rassigns / alpha_rassigns

   376   by (rule alpha3_equivp(1)) (rule alpha3_equivp(2))

   377 

   378 

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

   380 

   381 datatype rtrm4 =

   382   rVr4 "name"

   383 | rAp4 "rtrm4" "rtrm4 list"

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

   385 print_theorems

   386 

   387 thm rtrm4.recs

   388 

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

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

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

   392 

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

   394 lemma repaired:

   395   fixes ts::"rtrm4 list"

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

   397   apply(induct ts)

   398   apply(simp_all)

   399   done

   400 

   401 thm permute_rtrm4_permute_rtrm4_list.simps

   402 thm permute_rtrm4_permute_rtrm4_list.simps[simplified repaired]

   403 

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

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

   406 print_theorems

   407 

   408 notation

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

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

   411 thm alpha_rtrm4_alpha_rtrm4_list.intros

   412 

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

   414 thm alpha4_inj

   415 

   416 lemma alpha4_eqvt:

   417   "t \<approx>4 s \<Longrightarrow> (pi \<bullet> t) \<approx>4 (pi \<bullet> s)"

   418   "a \<approx>4l b \<Longrightarrow> (pi \<bullet> a) \<approx>4l (pi \<bullet> b)"

   419 sorry

   420 

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

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

   423 thm alpha4_equivp

   424 

   425 quotient_type 

   426   qrtrm4 = rtrm4 / alpha_rtrm4 and

   427   qrtrm4list = "rtrm4 list" / alpha_rtrm4_list

   428   by (simp_all add: alpha4_equivp)

   429 

   430 

   431 datatype rtrm5 =

   432   rVr5 "name"

   433 | rAp5 "rtrm5" "rtrm5"

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

   435 and rlts =

   436   rLnil

   437 | rLcons "name" "rtrm5" "rlts"

   438 

   439 primrec

   440   rbv5

   441 where

   442   "rbv5 rLnil = {}"

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

   444 

   445 

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

   447 print_theorems

   448 

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

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

   451 print_theorems

   452 

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

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

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

   456 print_theorems*)

   457 

   458 notation

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

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

   461 thm alpha_rtrm5_alpha_rlts.intros

   462 

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

   464 thm alpha5_inj

   465 

   466 lemma rbv5_eqvt:

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

   468 sorry

   469 

   470 lemma fv_rtrm5_eqvt:

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

   472 sorry

   473 

   474 lemma fv_rlts_eqvt:

   475   "pi \<bullet> (fv_rlts x) = fv_rlts (pi \<bullet> x)"

   476 sorry

   477 

   478 lemma alpha5_eqvt:

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

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

   481   apply(induct rule: alpha_rtrm5_alpha_rlts.inducts)

   482   apply (simp_all add: alpha5_inj)

   483   apply (erule exE)+

   484   apply(unfold alpha_gen)

   485   apply (erule conjE)+

   486   apply (rule conjI)

   487   apply (rule_tac x="x \<bullet> pi" in exI)

   488   apply (rule conjI)

   489   apply(rule_tac ?p1="- x" in permute_eq_iff[THEN iffD1])

   490   apply(simp add: atom_eqvt Diff_eqvt insert_eqvt set_eqvt empty_eqvt rbv5_eqvt fv_rlts_eqvt)

   491   apply(rule conjI)

   492   apply(rule_tac ?p1="- x" in fresh_star_permute_iff[THEN iffD1])

   493   apply(simp add: atom_eqvt Diff_eqvt insert_eqvt set_eqvt empty_eqvt rbv5_eqvt fv_rlts_eqvt)

   494   apply (subst permute_eqvt[symmetric])

   495   apply (simp)

   496   apply (rule_tac x="x \<bullet> pia" in exI)

   497   apply (rule conjI)

   498   apply(rule_tac ?p1="- x" in permute_eq_iff[THEN iffD1])

   499   apply(simp add: atom_eqvt Diff_eqvt insert_eqvt set_eqvt empty_eqvt rbv5_eqvt fv_rtrm5_eqvt)

   500   apply(rule conjI)

   501   apply(rule_tac ?p1="- x" in fresh_star_permute_iff[THEN iffD1])

   502   apply(simp add: atom_eqvt Diff_eqvt insert_eqvt set_eqvt empty_eqvt rbv5_eqvt fv_rtrm5_eqvt)

   503   apply (subst permute_eqvt[symmetric])

   504   apply (simp)

   505   done

   506 

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

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

   509 thm alpha5_equivp

   510 

   511 quotient_type

   512   trm5 = rtrm5 / alpha_rtrm5

   513 and

   514   lts = rlts / alpha_rlts

   515   by (auto intro: alpha5_equivp)

   516 

   517 local_setup {*

   518 (fn ctxt => ctxt

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

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

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

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

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

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

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

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

   527 *}

   528 print_theorems

   529 

   530 lemma alpha5_rfv:

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

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

   533   apply(induct rule: alpha_rtrm5_alpha_rlts.inducts)

   534   apply(simp_all add: alpha_gen)

   535   done

   536 

   537 lemma bv_list_rsp:

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

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

   540   apply(simp_all)

   541   done

   542 

   543 lemma [quot_respect]:

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

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

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

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

   548   "(alpha_rtrm5 ===> alpha_rtrm5 ===> alpha_rtrm5) rAp5 rAp5"

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

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

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

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

   553   apply (simp_all add: alpha5_inj alpha5_rfv alpha5_eqvt bv_list_rsp)

   554   apply (clarify) apply (rule conjI)

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

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

   557   done

   558 

   559 lemma

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

   561   by (simp add: bv_list_rsp)

   562 

   563 lemmas trm5_lts_inducts = rtrm5_rlts.inducts[quot_lifted]

   564 

   565 instantiation trm5 and lts :: pt

   566 begin

   567 

   568 quotient_definition

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

   570 is

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

   572 

   573 quotient_definition

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

   575 is

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

   577 

   578 instance by default

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

   580 

   581 end

   582 

   583 lemmas

   584     permute_trm5_lts = permute_rtrm5_permute_rlts.simps[quot_lifted]

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

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

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

   588 

   589 lemma lets_ok:

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

   591 apply (subst alpha5_INJ)

   592 apply (rule conjI)

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

   594 apply (simp only: alpha_gen)

   595 apply (simp add: permute_trm5_lts fresh_star_def)

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

   597 apply (simp only: alpha_gen)

   598 apply (simp add: permute_trm5_lts fresh_star_def)

   599 done

   600 

   601 lemma lets_ok2:

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

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

   604 apply (subst alpha5_INJ)

   605 apply (rule conjI)

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

   607 apply (simp only: alpha_gen)

   608 apply (simp add: permute_trm5_lts fresh_star_def)

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

   610 apply (simp only: alpha_gen)

   611 apply (simp add: permute_trm5_lts fresh_star_def)

   612 done

   613 

   614 

   615 lemma lets_not_ok1:

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

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

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

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

   620 done

   621 

   622 lemma distinct_helper:

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

   624   apply auto

   625   apply (erule alpha_rtrm5.cases)

   626   apply (simp_all only: rtrm5.distinct)

   627   done

   628 

   629 lemma distinct_helper2:

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

   631   by (lifting distinct_helper)

   632 

   633 lemma lets_nok:

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

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

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

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

   638 apply (simp add: distinct_helper2)

   639 done

   640 

   641 

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

   643 datatype rtrm6 =

   644   rVr6 "name"

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

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

   647 

   648 primrec

   649   rbv6

   650 where

   651   "rbv6 (rVr6 n) = {}"

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

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

   654 

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

   656 print_theorems

   657 

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

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

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

   661 (* HERE THE RULES DIFFER *)

   662 thm alpha_rtrm6.intros

   663 

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

   665 thm alpha6_inj

   666 

   667 lemma alpha6_eqvt:

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

   669 sorry

   670 

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

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

   673 thm alpha6_equivp

   674 

   675 quotient_type

   676   trm6 = rtrm6 / alpha_rtrm6

   677   by (auto intro: alpha6_equivp)

   678 

   679 local_setup {*

   680 (fn ctxt => ctxt

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

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

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

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

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

   686 *}

   687 print_theorems

   688 

   689 lemma [quot_respect]:

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

   691 by (auto simp add: alpha6_eqvt)

   692 

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

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

   695 apply simp apply clarify

   696 apply (erule alpha_rtrm6.induct)

   697 oops

   698 

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

   700 apply simp

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

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

   703 apply simp

   704 apply (simp add: alpha6_inj)

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

   706 apply (simp add: alpha_gen fresh_star_def)

   707 apply (simp add: alpha6_inj)

   708 done

   709 

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

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

   712 apply simp_all

   713 apply (erule exE)

   714 apply (simp_all add: alpha_gen)

   715 done

   716 

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

   718 by (simp add: fv6_rsp)

   719 

   720 lemma [quot_respect]:

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

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

   723 apply auto

   724 apply (simp_all add: alpha6_inj)

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

   726 apply (simp add: alpha_gen fv6_rsp fresh_star_def fresh_zero_perm)

   727 done

   728 

   729 lemma [quot_respect]:

   730  "(alpha_rtrm6 ===> alpha_rtrm6 ===> alpha_rtrm6) rLt6 rLt6"

   731 apply auto

   732 apply (simp_all add: alpha6_inj)

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

   734 apply (simp_all add: alpha_gen fresh_star_def fresh_zero_perm)

   735 (* needs rbv6_rsp *)

   736 oops

   737 

   738 instantiation trm6 :: pt begin

   739 

   740 quotient_definition

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

   742 is

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

   744 

   745 instance

   746 apply default

   747 sorry

   748 end

   749 

   750 lemma lifted_induct:

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

   752  \<And>name rtrm6 namea rtrm6a.

   753     \<lbrakk>True;

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

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

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

   757  \<And>rtrm61 rtrm61a rtrm62 rtrm62a.

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

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

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

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

   762 \<Longrightarrow> P x1 x2"

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

   764 apply injection

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

   766 oops

   767 

   768 lemma lifted_inject_a3:

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

   770 (rtrm61 = rtrm61a \<and>

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

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

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

   774 apply injection

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

   776 oops

   777 

   778 

   779 

   780 

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

   782 

   783 datatype rtrm7 =

   784   rVr7 "name"

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

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

   787 

   788 primrec

   789   rbv7

   790 where

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

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

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

   794 

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

   796 thm permute_rtrm7.simps

   797 

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

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

   800 print_theorems

   801 notation

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

   803 (* HERE THE RULES DIFFER *)

   804 thm alpha_rtrm7.intros

   805 thm fv_rtrm7.simps

   806 inductive

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

   808 where

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

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

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

   812 

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

   814   apply simp

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

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

   817   apply simp

   818   apply (rule a3)

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

   820   apply (simp_all add: alpha_gen fresh_star_def)

   821   apply (rule a1)

   822   apply (rule refl)

   823 done

   824 

   825 

   826 

   827 

   828 

   829 datatype rfoo8 =

   830   Foo0 "name"

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

   832 and rbar8 =

   833   Bar0 "name"

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

   835 

   836 primrec

   837   rbv8

   838 where

   839   "rbv8 (Bar0 x) = {}"

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

   841 

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

   843 print_theorems

   844 

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

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

   847 notation

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

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

   850 (* HERE THE RULE DIFFERS *)

   851 thm alpha_rfoo8_alpha_rbar8.intros

   852 

   853 

   854 inductive

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

   856 and

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

   858 where

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

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

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

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

   863 

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

   865   apply simp apply clarify

   866   apply (erule alpha8f_alpha8b.inducts(2))

   867   apply (simp_all)

   868 done

   869 

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

   871   apply (erule alpha8f_alpha8b.inducts(2))

   872   apply (simp_all add: alpha_gen)

   873 done

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

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

   876 done

   877 

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

   879   apply simp apply clarify

   880   apply (erule alpha8f_alpha8b.inducts(1))

   881   apply (simp_all add: alpha_gen fv_rbar8_rsp_hlp)

   882 done

   883 

   884 

   885 

   886 

   887 

   888 

   889 datatype rlam9 =

   890   Var9 "name"

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

   892 and rbla9 =

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

   894 

   895 primrec

   896   rbv9

   897 where

   898   "rbv9 (Var9 x) = {}"

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

   900 

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

   902 print_theorems

   903 

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

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

   906 notation

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

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

   909 (* HERE THE RULES DIFFER *)

   910 thm alpha_rlam9_alpha_rbla9.intros

   911 

   912 

   913 inductive

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

   915 and

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

   917 where

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

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

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

   921 

   922 quotient_type

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

   924 sorry

   925 

   926 local_setup {*

   927 (fn ctxt => ctxt

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

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

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

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

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

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

   934 *}

   935 print_theorems

   936 

   937 instantiation lam9 and bla9 :: pt

   938 begin

   939 

   940 quotient_definition

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

   942 is

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

   944 

   945 quotient_definition

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

   947 is

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

   949 

   950 instance

   951 sorry

   952 

   953 end

   954 

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

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

   957 apply (lifting a3[unfolded alpha_gen])

   958 apply injection

   959 sorry

   960 

   961 

   962 

   963 

   964 

   965 

   966 

   967 

   968 text {* type schemes *} 

   969 datatype ty = 

   970   Var "name" 

   971 | Fun "ty" "ty"

   972 

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

   974 print_theorems

   975 

   976 datatype tyS = 

   977   All "name set" "ty" 

   978 

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

   980 print_theorems

   981 

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

   983 print_theorems 

   984 

   985 (*

   986 Doesnot work yet since we do not refer to fv_ty

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

   988 print_theorems

   989 *)

   990 

   991 primrec

   992   fv_tyS

   993 where 

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

   995 

   996 inductive

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

   998 where

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

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

  1001 

  1002 lemma

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

  1004   apply(rule a1)

  1005   apply(simp add: alpha_gen)

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

  1007   apply(simp add: fresh_star_def)

  1008   done

  1009 

  1010 lemma

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

  1012   apply(rule a1)

  1013   apply(simp add: alpha_gen)

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

  1015   apply(simp add: fresh_star_def)

  1016   done

  1017 

  1018 lemma

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

  1020   apply(rule a1)

  1021   apply(simp add: alpha_gen)

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

  1023   apply(simp add: fresh_star_def)

  1024   done

  1025 

  1026 lemma

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

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

  1029   using a

  1030   apply(clarify)

  1031   apply(erule alpha_tyS.cases)

  1032   apply(simp add: alpha_gen)

  1033   apply(erule conjE)+

  1034   apply(erule exE)

  1035   apply(erule conjE)+

  1036   apply(clarify)

  1037   apply(simp)

  1038   apply(simp add: fresh_star_def)

  1039   apply(auto)

  1040   done

  1041 

  1042 

  1043 end