1 header {* Utilities for defining constants and functions *}

     2 

     3 theory Utils imports LambdaTerms begin

     4 

     5 lemma beta_app:

     6   "(\<integral> x. M) \<cdot> Var x \<approx> M"

     7   by (rule b3, rule bI)

     8      (simp add: b1)

     9 

    10 lemma lam1_fast_app:

    11   assumes leq: "\<And>a. (L = \<integral> a. (F (V a)))"

    12       and su: "\<And>x. atom x \<sharp> A \<Longrightarrow> F (V x) [x ::= A] = F A"

    13   shows "L \<cdot> A \<approx> F A"

    14 proof -

    15   obtain x :: name where a: "atom x \<sharp> A" using obtain_fresh by blast

    16   show ?thesis

    17     by (simp add: leq[of x], rule b3, rule bI, simp add: su b1 a)

    18 qed

    19 

    20 lemma lam2_fast_app:

    21   assumes leq: "\<And>a b. a \<noteq> b \<Longrightarrow> L = \<integral> a. \<integral> b. (F (V a) (V b))"

    22      and su: "\<And>x y. atom x \<sharp> A \<Longrightarrow> atom y \<sharp> A \<Longrightarrow> atom x \<sharp> B \<Longrightarrow> atom y \<sharp> B \<Longrightarrow>

    23        x \<noteq> y \<Longrightarrow> F (V x) (V y) [x ::= A] [y ::= B] = F A B"

    24   shows "L \<cdot> A \<cdot> B \<approx> F A B"

    25 proof -

    26   obtain x :: name where a: "atom x \<sharp> (A, B)" using obtain_fresh by blast

    27   obtain y :: name where b: "atom y \<sharp> (x, A, B)" using obtain_fresh by blast

    28   obtain z :: name where c: "atom z \<sharp> (x, y, A, B)" using obtain_fresh by blast

    29   have *: "x \<noteq> y" "x \<noteq> z" "y \<noteq> z"

    30     using a b c by (simp_all add: fresh_Pair fresh_at_base) blast+

    31   have ** : "atom y \<sharp> z" "atom x \<sharp> z" "atom y \<sharp> x"

    32             "atom z \<sharp> y" "atom z \<sharp> x" "atom x \<sharp> y"

    33             "atom x \<sharp> A" "atom y \<sharp> A" "atom z \<sharp> A"

    34             "atom x \<sharp> B" "atom y \<sharp> B" "atom z \<sharp> B"

    35     using a b c by (simp_all add: fresh_Pair fresh_at_base) blast+

    36   show ?thesis

    37     apply (simp add: leq[OF *(1)])

    38     apply (rule b3) apply (rule b5) apply (rule bI)

    39     apply (simp add: ** fresh_Pair)

    40     apply (rule b3) apply (rule bI) apply (simp add: su b1 ** *)

    41     done

    42   qed

    43 

    44 lemma lam3_fast_app:

    45   assumes leq: "\<And>a b c. a \<noteq> b \<Longrightarrow> b \<noteq> c \<Longrightarrow> c \<noteq> a \<Longrightarrow>

    46        L = \<integral> a. \<integral> b. \<integral> c. (F (V a) (V b) (V c))"

    47      and su: "\<And>x y z. atom x \<sharp> A \<Longrightarrow> atom y \<sharp> A \<Longrightarrow> atom z \<sharp> A \<Longrightarrow>

    48                      atom x \<sharp> B \<Longrightarrow> atom y \<sharp> B \<Longrightarrow> atom z \<sharp> B \<Longrightarrow>

    49                      atom y \<sharp> B \<Longrightarrow> atom y \<sharp> B \<Longrightarrow> atom z \<sharp> B \<Longrightarrow>

    50                      x \<noteq> y \<Longrightarrow> y \<noteq> z \<Longrightarrow> z \<noteq> x \<Longrightarrow>

    51       ((F (V x) (V y) (V z))[x ::= A] [y ::= B] [z ::= C] = F A B C)"

    52   shows "L \<cdot> A \<cdot> B \<cdot> C \<approx> F A B C"

    53 proof -

    54   obtain x :: name where a: "atom x \<sharp> (A, B, C)" using obtain_fresh by blast

    55   obtain y :: name where b: "atom y \<sharp> (x, A, B, C)" using obtain_fresh by blast

    56   obtain z :: name where c: "atom z \<sharp> (x, y, A, B, C)" using obtain_fresh by blast

    57   have *: "x \<noteq> y" "y \<noteq> z" "z \<noteq> x"

    58     using a b c by (simp_all add: fresh_Pair fresh_at_base) blast+

    59   have ** : "atom y \<sharp> z" "atom x \<sharp> z" "atom y \<sharp> x"

    60             "atom z \<sharp> y" "atom z \<sharp> x" "atom x \<sharp> y"

    61             "atom x \<sharp> A" "atom y \<sharp> A" "atom z \<sharp> A"

    62             "atom x \<sharp> B" "atom y \<sharp> B" "atom z \<sharp> B"

    63             "atom x \<sharp> C" "atom y \<sharp> C" "atom z \<sharp> C"

    64     using a b c by (simp_all add: fresh_Pair fresh_at_base) blast+

    65   show ?thesis

    66     apply (simp add: leq[OF *(1) *(2) *(3)])

    67     apply (rule b3) apply (rule b5) apply (rule b5) apply (rule bI)

    68     apply (simp add: ** fresh_Pair)

    69     apply (rule b3) apply (rule b5) apply (rule bI)

    70     apply (simp add: ** fresh_Pair)

    71     apply (rule b3) apply (rule bI) apply (simp add: su b1 ** *)

    72     done

    73   qed

    74 

    75 definition cn :: "nat \<Rightarrow> name" where "cn n \<equiv> Abs_name (Atom (Sort ''LambdaTerms.name'' []) n)"

    76 

    77 lemma cnd[simp]: "m \<noteq> n \<Longrightarrow> cn m \<noteq> cn n"

    78   unfolding cn_def using Abs_name_inject by simp

    79 

    80 definition cx :: name where "cx \<equiv> cn 0"

    81 definition cy :: name where "cy \<equiv> cn 1"

    82 definition cz :: name where "cz \<equiv> cn 2"

    83 

    84 lemma cx_cy_cz[simp]:

    85   "cx \<noteq> cy" "cx \<noteq> cz" "cz \<noteq> cy"

    86   unfolding cx_def cy_def cz_def

    87   by simp_all

    88 

    89 lemma noteq_fresh: "atom x \<sharp> y = (x \<noteq> y)"

    90   by (simp add: fresh_at_base(2))

    91 

    92 lemma fresh_fun_eqvt_app2:

    93   assumes a: "eqvt f"

    94   and b: "a \<sharp> x" "a \<sharp> y"

    95   shows "a \<sharp> f x y"

    96   using fresh_fun_eqvt_app[OF a b(1)] a b

    97   by (metis fresh_fun_app)

    98 

    99 end

   100 

   101 

   102