23 thm alpha_trm_raw_alpha_assg_raw_alpha_bn_raw.intros

    24 thm alpha_trm_raw.cases alpha_assg_raw.cases alpha_bn_raw.cases

    26 

    27 lemma [eqvt]:

    28  "p \<bullet> alpha_trm_raw x1 y1  = alpha_trm_raw (p \<bullet> x1) (p \<bullet> y1)"

    29  "p \<bullet> alpha_assg_raw x2 y2 = alpha_assg_raw (p \<bullet> x2) (p \<bullet> y2)"

    30  "p \<bullet> alpha_bn_raw x3 y3   = alpha_bn_raw (p \<bullet> x3) (p \<bullet> y3)"

    31 sorry

    32 

    33 lemmas ii = alpha_trm_raw_alpha_assg_raw_alpha_bn_raw.intros

    34 lemmas cc = alpha_trm_raw.cases alpha_assg_raw.cases alpha_bn_raw.cases

    35 

    36 ML {*

    37 length @{thms cc}

    38 *}

    39 

    40 ML {*

    41   val pp = ["SingleLet.alpha_trm_raw", "SingleLet.alpha_assg_raw", "SingleLet.alpha_bn_raw"]

    42 *}

    43 

    44 lemma exi_sum: "\<exists>(q :: perm). P q \<Longrightarrow> \<exists>q. Q q \<Longrightarrow> (\<And>p q. P p \<Longrightarrow> Q q \<Longrightarrow> R (p + q)) \<Longrightarrow> \<exists>r. R r"

    45 apply(erule exE)+

    46 apply(rule_tac x="q + qa" in exI)

    47 apply(simp)

    48 done

    49 

    50 lemma alpha_gen_compose_trans:

    51   assumes b: "(as, t) \<approx>gen (\<lambda>x1 x2. R x1 x2 \<and> (\<forall>x. R x2 x \<longrightarrow> R x1 x)) f pi (bs, s)"

    52   shows "(\<forall>x. R s x \<longrightarrow> R (pi \<bullet> t) x)"

    53   using b

    54   by (simp add: alphas)

    55 

    56 lemma test:

    57   assumes b: "(as, t) \<approx>gen R f pi (bs, s)"

    58   shows "R (pi \<bullet> t) s"

    59   using b

    60   by (simp add: alphas)

    61 

    62 lemma alpha_gen_trans_eqvt:

    63   assumes a: "(bs, x) \<approx>gen R f p (cs, y)" and a1: "(cs, y) \<approx>gen R f q (ds, z)"

    64   and b: "\<lbrakk>R (p \<bullet> x) y; R y (- q \<bullet> z)\<rbrakk> \<Longrightarrow> R (p \<bullet> x) (- q \<bullet> z)"

    65   shows "(bs, x) \<approx>gen R f (q + p) (ds, z)"

    66   sorry

    67 

    68 

    69 lemma

    70  "alpha_trm_raw x1 y1  \<Longrightarrow> (\<And>z1. alpha_trm_raw y1 z1 \<Longrightarrow> alpha_trm_raw x1 z1)"

    71  "alpha_assg_raw x2 y2 \<Longrightarrow> (\<And>z2. alpha_assg_raw y2 z2 \<Longrightarrow> alpha_assg_raw x2 z2)"

    72  "alpha_bn_raw x3 y3   \<Longrightarrow> (\<And>z3. alpha_bn_raw y3 z3 \<Longrightarrow> alpha_bn_raw x3 z3)"

    73 apply(induct rule: alpha_trm_raw_alpha_assg_raw_alpha_bn_raw.inducts)

    74 (* 8 *)

    75 prefer 8

    76 thm alpha_bn_raw.cases

    77 apply(rotate_tac -1)

    78 apply(erule alpha_bn_raw.cases)

    79 apply(simp_all)[6]

    80 

    81 

    82 apply(rotate_tac -1)

    83 apply(erule cc)

    84 apply(simp_all)[6]

    85 apply(rule ii) 

    86 apply(simp)

    87 (* 1 *)

    88 apply(rotate_tac -1)

    89 apply(erule cc)

    90 apply(simp_all)[6]

    91 apply(rule ii) 

    92 apply(simp)

    93 apply(simp)

    94 (* 2 *)

    95 apply(rotate_tac -1)

    96 apply(erule cc)

    97 apply(simp_all)[6]

    98 apply(rule ii)

    99 apply(erule exE)+

   100 apply(rule_tac x="pa + p" in exI)

   101 apply(rule alpha_gen_trans_eqvt)

   102 prefer 2

   103 apply(assumption)

   104 apply(simp add: alphas)

   105 apply(metis)

   106 apply(drule test)

   107 apply(simp)

   108 (* 3 *)

   109 apply(rotate_tac -1)

   110 apply(erule cc)

   111 apply(simp_all)[6]

   112 apply(rule ii)

   113 apply(erule exE)+

   114 apply(rule_tac x="pa + p" in exI)

   115 apply(rule alpha_gen_trans_eqvt)

   116 prefer 2

   117 apply(assumption)

   118 apply(simp add: alphas)

   119 apply(metis)

   120 apply(drule alpha_gen_compose_trans)

   121 apply(simp)

   122 apply(simp)

   123 (* 4 *)

   124 apply(rotate_tac -1)

   125 apply(erule cc)

   126 apply(simp_all)[6]

   127 apply(rule ii)

   128 apply(erule exE)+

   129 apply(rule_tac x="pa + p" in exI)

   130 apply(rule alpha_gen_trans_eqvt)

   131 prefer 2

   132 apply(assumption)

   133 prefer 2

   134 apply(drule test)

   135 apply(simp add: prod_alpha_def)

   136 apply(simp add: alphas)

   137 

   138 apply(drule alpha_gen_compose_trans)

   139 apply(drule_tac x="(- pa \<bullet> trm_rawaa)" in spec)

   140 apply(simp)

   141 apply(simp)

   142 (* 4 *)

   143 apply(assumption) 

   144 apply(simp)

   145 apply(simp)

   146 

   147 (* 3 *)

   148 

   149 (* 4 *)

   150 

   151 (* 5 *)

   152 

   153 (* 6 *)

   154 

   155 (* 7 *)

   156 

   157 (* 8 *)

   158 

   159 (* 9 *)

   160 done

   161 

   162 ML {* Inductive.the_inductive *}