src/HOL/Nominal/Examples/Lam_substs.thy
author urbanc
Mon, 23 Jan 2006 15:14:06 +0100
changeset 18758 e8a11e84864c
parent 18659 2ff0ae57431d
child 19166 fd8f152cfc76
permissions -rw-r--r--
made change for ex1
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
18269
3f36e2165e51 some small tuning
urbanc
parents: 18263
diff changeset
     1
(* $Id$ *)
18106
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
     2
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
     3
theory lam_substs
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
     4
imports "../nominal" 
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
     5
begin
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
     6
18269
3f36e2165e51 some small tuning
urbanc
parents: 18263
diff changeset
     7
text {* Contains all the reasoning infrastructure for the
3f36e2165e51 some small tuning
urbanc
parents: 18263
diff changeset
     8
        lambda-calculus that the nominal datatype package
3f36e2165e51 some small tuning
urbanc
parents: 18263
diff changeset
     9
        does not yet provide. *}
3f36e2165e51 some small tuning
urbanc
parents: 18263
diff changeset
    10
18106
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
    11
atom_decl name 
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
    12
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
    13
nominal_datatype lam = Var "name"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
    14
                     | App "lam" "lam"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
    15
                     | Lam "\<guillemotleft>name\<guillemotright>lam" ("Lam [_]._" [100,100] 100)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
    16
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
    17
types 'a f1_ty  = "name\<Rightarrow>('a::pt_name)"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
    18
      'a f2_ty  = "'a\<Rightarrow>'a\<Rightarrow>('a::pt_name)"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
    19
      'a f3_ty  = "name\<Rightarrow>'a\<Rightarrow>('a::pt_name)"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
    20
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
    21
lemma f3_freshness_conditions:
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
    22
  fixes f3::"('a::pt_name) f3_ty"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
    23
  and   y ::"name prm \<Rightarrow> 'a::pt_name"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
    24
  and   a ::"name"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
    25
  and   pi1::"name prm"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
    26
  and   pi2::"name prm"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
    27
  assumes a: "finite ((supp f3)::name set)"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
    28
  and     b: "finite ((supp y)::name set)"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
    29
  and     c: "\<exists>(a::name). a\<sharp>f3 \<and> (\<forall>(y::'a::pt_name). a\<sharp>f3 a y)"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
    30
  shows "\<exists>(a''::name). a''\<sharp>(\<lambda>a'. f3 a' (y (pi1@[(a,pi2\<bullet>a')]))) \<and> 
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
    31
                       a''\<sharp>(\<lambda>a'. f3 a' (y (pi1@[(a,pi2\<bullet>a')]))) a''" 
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
    32
proof -
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
    33
  from c obtain a' where d0: "a'\<sharp>f3" and d1: "\<forall>(y::'a::pt_name). a'\<sharp>f3 a' y" by force
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
    34
  have "\<exists>(a''::name). a''\<sharp>(f3,a,a',pi1,pi2,y)" 
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
    35
    by (rule at_exists_fresh[OF at_name_inst],  simp add: supp_prod fs_name1 a b)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
    36
  then obtain a'' where d2: "a''\<sharp>f3" and d3: "a''\<noteq>a'" and d3b: "a''\<sharp>(f3,a,pi1,pi2,y)" 
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
    37
    by (auto simp add: fresh_prod at_fresh[OF at_name_inst])
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
    38
  have d3c: "a''\<notin>((supp (f3,a,pi1,pi2,y))::name set)" using d3b by (simp add: fresh_def)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
    39
  have d4: "a''\<sharp>f3 a'' (y (pi1@[(a,pi2\<bullet>a'')]))"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
    40
  proof -
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
    41
    have d5: "[(a'',a')]\<bullet>f3 = f3" 
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
    42
      by (rule pt_fresh_fresh[OF pt_name_inst, OF at_name_inst, OF d2, OF d0]) 
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
    43
    from d1 have "\<forall>(y::'a::pt_name). ([(a'',a')]\<bullet>a')\<sharp>([(a'',a')]\<bullet>(f3 a' y))"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
    44
      by (simp add: pt_fresh_bij[OF pt_name_inst, OF at_name_inst])
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
    45
    hence "\<forall>(y::'a::pt_name). a''\<sharp>(f3 a'' ([(a'',a')]\<bullet>y))" using d3 d5 
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
    46
      by (simp add: at_calc[OF at_name_inst] pt_fun_app_eq[OF pt_name_inst, OF at_name_inst])
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
    47
    hence "a''\<sharp>(f3 a'' ([(a'',a')]\<bullet>((rev [(a'',a')])\<bullet>(y (pi1@[(a,pi2\<bullet>a'')])))))" by force
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
    48
    thus ?thesis by (simp only: pt_pi_rev[OF pt_name_inst, OF at_name_inst])
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
    49
  qed
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
    50
  have d6: "a''\<sharp>(\<lambda>a'. f3 a' (y (pi1@[(a,pi2\<bullet>a')])))"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
    51
  proof -
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
    52
    from a b have d7: "finite ((supp (f3,a,pi1,pi2,y))::name set)" by (simp add: supp_prod fs_name1)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
    53
    have e: "((supp (f3,a,pi1,pi2,y))::name set) supports (\<lambda>a'. f3 a' (y (pi1@[(a,pi2\<bullet>a')])))" 
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
    54
      by (supports_simp add: perm_append)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
    55
    from e d7 d3c show ?thesis by (rule supports_fresh)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
    56
  qed
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
    57
  from d6 d4 show ?thesis by force
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
    58
qed
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
    59
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
    60
lemma f3_freshness_conditions_simple:
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
    61
  fixes f3::"('a::pt_name) f3_ty"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
    62
  and   y ::"name prm \<Rightarrow> 'a::pt_name"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
    63
  and   a ::"name"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
    64
  and   pi::"name prm"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
    65
  assumes a: "finite ((supp f3)::name set)"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
    66
  and     b: "finite ((supp y)::name set)"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
    67
  and     c: "\<exists>(a::name). a\<sharp>f3 \<and> (\<forall>(y::'a::pt_name). a\<sharp>f3 a y)"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
    68
  shows "\<exists>(a''::name). a''\<sharp>(\<lambda>a'. f3 a' (y (pi@[(a,a')]))) \<and> a''\<sharp>(\<lambda>a'. f3 a' (y (pi@[(a,a')]))) a''" 
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
    69
proof -
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
    70
  from c obtain a' where d0: "a'\<sharp>f3" and d1: "\<forall>(y::'a::pt_name). a'\<sharp>f3 a' y" by force
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
    71
  have "\<exists>(a''::name). a''\<sharp>(f3,a,a',pi,y)" 
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
    72
    by (rule at_exists_fresh[OF at_name_inst],  simp add: supp_prod fs_name1 a b)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
    73
  then obtain a'' where d2: "a''\<sharp>f3" and d3: "a''\<noteq>a'" and d3b: "a''\<sharp>(f3,a,pi,y)" 
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
    74
    by (auto simp add: fresh_prod at_fresh[OF at_name_inst])
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
    75
  have d3c: "a''\<notin>((supp (f3,a,pi,y))::name set)" using d3b by (simp add: fresh_def)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
    76
  have d4: "a''\<sharp>f3 a'' (y (pi@[(a,a'')]))"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
    77
  proof -
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
    78
    have d5: "[(a'',a')]\<bullet>f3 = f3" 
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
    79
      by (rule pt_fresh_fresh[OF pt_name_inst, OF at_name_inst, OF d2, OF d0]) 
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
    80
    from d1 have "\<forall>(y::'a::pt_name). ([(a'',a')]\<bullet>a')\<sharp>([(a'',a')]\<bullet>(f3 a' y))"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
    81
      by (simp add: pt_fresh_bij[OF pt_name_inst, OF at_name_inst])
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
    82
    hence "\<forall>(y::'a::pt_name). a''\<sharp>(f3 a'' ([(a'',a')]\<bullet>y))" using d3 d5 
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
    83
      by (simp add: at_calc[OF at_name_inst] pt_fun_app_eq[OF pt_name_inst, OF at_name_inst])
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
    84
    hence "a''\<sharp>(f3 a'' ([(a'',a')]\<bullet>((rev [(a'',a')])\<bullet>(y (pi@[(a,a'')])))))" by force
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
    85
    thus ?thesis by (simp only: pt_pi_rev[OF pt_name_inst, OF at_name_inst])
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
    86
  qed
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
    87
  have d6: "a''\<sharp>(\<lambda>a'. f3 a' (y (pi@[(a,a')])))"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
    88
  proof -
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
    89
    from a b have d7: "finite ((supp (f3,a,pi,y))::name set)" by (simp add: supp_prod fs_name1)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
    90
    have "((supp (f3,a,pi,y))::name set) supports (\<lambda>a'. f3 a' (y (pi@[(a,a')])))" 
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
    91
      by (supports_simp add: perm_append)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
    92
    with d7 d3c show ?thesis by (simp add: supports_fresh)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
    93
  qed
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
    94
  from d6 d4 show ?thesis by force
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
    95
qed
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
    96
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
    97
lemma f3_fresh_fun_supports:
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
    98
  fixes f3::"('a::pt_name) f3_ty"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
    99
  and   a ::"name"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   100
  and   pi1::"name prm"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   101
  and   y ::"name prm \<Rightarrow> 'a::pt_name"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   102
  assumes a: "finite ((supp f3)::name set)"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   103
  and     b: "finite ((supp y)::name set)"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   104
  and     c: "\<exists>(a::name). a\<sharp>f3 \<and> (\<forall>(y::'a::pt_name). a\<sharp>f3 a y)"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   105
  shows "((supp (f3,a,y))::name set) supports (\<lambda>pi. fresh_fun (\<lambda>a'. f3 a' (y (pi@[(a,a')]))))"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   106
proof (auto simp add: "op supports_def" perm_fun_def expand_fun_eq fresh_def[symmetric])
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   107
  fix b::"name" and c::"name" and pi::"name prm"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   108
  assume b1: "b\<sharp>(f3,a,y)"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   109
  and    b2: "c\<sharp>(f3,a,y)"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   110
  from b1 b2 have b3: "[(b,c)]\<bullet>f3=f3" and t4: "[(b,c)]\<bullet>a=a" and t5: "[(b,c)]\<bullet>y=y"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   111
    by (simp_all add: pt_fresh_fresh[OF pt_name_inst, OF at_name_inst] fresh_prod)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   112
  let ?g = "\<lambda>a'. f3 a' (y (([(b,c)]\<bullet>pi)@[(a,a')]))"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   113
  and ?h = "\<lambda>a'. f3 a' (y (pi@[(a,a')]))"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   114
  have a0: "finite ((supp (f3,a,[(b,c)]\<bullet>pi,y))::name set)" using a b 
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   115
    by (simp add: supp_prod fs_name1)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   116
  have a1: "((supp (f3,a,[(b,c)]\<bullet>pi,y))::name set) supports ?g" by (supports_simp add: perm_append)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   117
  hence a2: "finite ((supp ?g)::name set)" using a0 by (rule supports_finite)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   118
  have a3: "\<exists>(a''::name). a''\<sharp>?g \<and> a''\<sharp>(?g a'')"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   119
    by (rule f3_freshness_conditions_simple[OF a, OF b, OF c])
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   120
  have "((supp (f3,a,y))::name set) \<subseteq> (supp (f3,a,[(b,c)]\<bullet>pi,y))" by (force simp add: supp_prod)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   121
  have a4: "[(b,c)]\<bullet>?g = ?h" using b1 b2
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   122
    by (simp add: fresh_prod, perm_simp add: perm_append)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   123
  have "[(b,c)]\<bullet>(fresh_fun ?g) = fresh_fun ([(b,c)]\<bullet>?g)" 
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   124
    by (simp add: fresh_fun_equiv[OF pt_name_inst, OF at_name_inst, OF a2, OF a3])
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   125
  also have "\<dots> = fresh_fun ?h" using a4 by simp
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   126
  finally show "[(b,c)]\<bullet>(fresh_fun ?g) = fresh_fun ?h" .
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   127
qed
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   128
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   129
lemma f3_fresh_fun_supp_finite:
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   130
  fixes f3::"('a::pt_name) f3_ty"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   131
  and   a ::"name"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   132
  and   pi1::"name prm"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   133
  and   y ::"name prm \<Rightarrow> 'a::pt_name"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   134
  assumes a: "finite ((supp f3)::name set)"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   135
  and     b: "finite ((supp y)::name set)"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   136
  and     c: "\<exists>(a::name). a\<sharp>f3 \<and> (\<forall>(y::'a::pt_name). a\<sharp>f3 a y)"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   137
  shows "finite ((supp (\<lambda>pi. fresh_fun (\<lambda>a'. f3 a' (y (pi@[(a,a')])))))::name set)"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   138
proof -
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   139
  have "((supp (f3,a,y))::name set) supports (\<lambda>pi. fresh_fun (\<lambda>a'. f3 a' (y (pi@[(a,a')]))))"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   140
    using a b c by (rule f3_fresh_fun_supports)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   141
  moreover
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   142
  have "finite ((supp (f3,a,y))::name set)" using a b by (simp add: supp_prod fs_name1) 
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   143
  ultimately show ?thesis by (rule supports_finite)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   144
qed
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   145
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   146
types 'a recT  = "'a f1_ty \<Rightarrow> 'a f2_ty \<Rightarrow> 'a f3_ty \<Rightarrow> (lam\<times>(name prm \<Rightarrow> ('a::pt_name))) set"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   147
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   148
consts
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   149
  rec :: "('a::pt_name) recT"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   150
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   151
inductive "rec f1 f2 f3"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   152
intros
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   153
r1: "(Var a,\<lambda>pi. f1 (pi\<bullet>a))\<in>rec f1 f2 f3" 
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   154
r2: "\<lbrakk>finite ((supp y1)::name set);(t1,y1)\<in>rec f1 f2 f3; 
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   155
      finite ((supp y2)::name set);(t2,y2)\<in>rec f1 f2 f3\<rbrakk> 
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   156
      \<Longrightarrow> (App t1 t2,\<lambda>pi. f2 (y1 pi) (y2 pi))\<in>rec f1 f2 f3"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   157
r3: "\<lbrakk>finite ((supp y)::name set);(t,y)\<in>rec f1 f2 f3\<rbrakk> 
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   158
      \<Longrightarrow> (Lam [a].t,\<lambda>pi. fresh_fun (\<lambda>a'. f3 a' (y (pi@[(a,a')]))))\<in>rec f1 f2 f3"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   159
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   160
constdefs
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   161
  rfun' :: "'a f1_ty \<Rightarrow> 'a f2_ty \<Rightarrow> 'a f3_ty \<Rightarrow> lam \<Rightarrow> name prm \<Rightarrow> ('a::pt_name)" 
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   162
  "rfun' f1 f2 f3 t \<equiv> (THE y. (t,y)\<in>rec f1 f2 f3)"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   163
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   164
  rfun :: "'a f1_ty \<Rightarrow> 'a f2_ty \<Rightarrow> 'a f3_ty \<Rightarrow> lam \<Rightarrow> ('a::pt_name)" 
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   165
  "rfun f1 f2 f3 t \<equiv> rfun' f1 f2 f3 t ([]::name prm)"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   166
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   167
lemma rec_prm_eq[rule_format]:
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   168
  fixes f1 ::"('a::pt_name) f1_ty"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   169
  and   f2 ::"('a::pt_name) f2_ty"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   170
  and   f3 ::"('a::pt_name) f3_ty"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   171
  and   t  ::"lam"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   172
  and   y  ::"name prm \<Rightarrow> ('a::pt_name)"
18298
f7899cb24c79 changed induction principle and everything to conform with the
urbanc
parents: 18284
diff changeset
   173
  shows "(t,y)\<in>rec f1 f2 f3 \<Longrightarrow> (\<forall>(pi1::name prm) (pi2::name prm). pi1 \<triangleq> pi2 \<longrightarrow> (y pi1 = y pi2))"
18106
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   174
apply(erule rec.induct)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   175
apply(auto simp add: pt3[OF pt_name_inst])
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   176
apply(rule_tac f="fresh_fun" in arg_cong)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   177
apply(auto simp add: expand_fun_eq)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   178
apply(drule_tac x="pi1@[(a,x)]" in spec)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   179
apply(drule_tac x="pi2@[(a,x)]" in spec)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   180
apply(force simp add: prm_eq_def pt2[OF pt_name_inst])
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   181
done
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   182
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   183
(* silly helper lemma *)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   184
lemma rec_trans: 
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   185
  fixes f1 ::"('a::pt_name) f1_ty"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   186
  and   f2 ::"('a::pt_name) f2_ty"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   187
  and   f3 ::"('a::pt_name) f3_ty"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   188
  and   t  ::"lam"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   189
  and   y  ::"name prm \<Rightarrow> ('a::pt_name)"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   190
  assumes a: "(t,y)\<in>rec f1 f2 f3"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   191
  and     b: "y=y'"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   192
  shows   "(t,y')\<in>rec f1 f2 f3"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   193
using a b by simp
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   194
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   195
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   196
lemma rec_prm_equiv:
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   197
  fixes f1 ::"('a::pt_name) f1_ty"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   198
  and   f2 ::"('a::pt_name) f2_ty"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   199
  and   f3 ::"('a::pt_name) f3_ty"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   200
  and   t  ::"lam"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   201
  and   y  ::"name prm \<Rightarrow> ('a::pt_name)"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   202
  and   pi ::"name prm"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   203
  assumes f: "finite ((supp (f1,f2,f3))::name set)"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   204
  and     c: "\<exists>(a::name). a\<sharp>f3 \<and> (\<forall>(y::'a::pt_name). a\<sharp>f3 a y)"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   205
  and     a: "(t,y)\<in>rec f1 f2 f3"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   206
  shows "(pi\<bullet>t,pi\<bullet>y)\<in>rec (pi\<bullet>f1) (pi\<bullet>f2) (pi\<bullet>f3)"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   207
using a
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   208
proof (induct)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   209
  case (r1 c)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   210
  let ?g ="pi\<bullet>(\<lambda>(pi'::name prm). f1 (pi'\<bullet>c))"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   211
  and ?g'="\<lambda>(pi'::name prm). (pi\<bullet>f1) (pi'\<bullet>(pi\<bullet>c))"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   212
  have "?g'=?g" 
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   213
  proof (auto simp only: expand_fun_eq perm_fun_def)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   214
    fix pi'::"name prm"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   215
    let ?h = "((rev pi)\<bullet>(pi'\<bullet>(pi\<bullet>c)))"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   216
    and ?h'= "(((rev pi)\<bullet>pi')\<bullet>c)"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   217
    have "?h' = ((rev pi)\<bullet>pi')\<bullet>((rev pi)\<bullet>(pi\<bullet>c))" 
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   218
      by (simp add: pt_rev_pi[OF pt_name_inst, OF at_name_inst])
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   219
    also have "\<dots> = ?h"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   220
      by (simp add: pt_perm_compose[OF pt_name_inst, OF at_name_inst,symmetric])
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   221
    finally show "pi\<bullet>(f1 ?h) = pi\<bullet>(f1 ?h')" by simp
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   222
  qed
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   223
  thus ?case by (force intro: rec_trans rec.r1)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   224
next
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   225
  case (r2 t1 t2 y1 y2)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   226
  assume a1: "finite ((supp y1)::name set)"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   227
  and    a2: "finite ((supp y2)::name set)"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   228
  and    a3: "(pi\<bullet>t1,pi\<bullet>y1) \<in> rec (pi\<bullet>f1) (pi\<bullet>f2) (pi\<bullet>f3)"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   229
  and    a4: "(pi\<bullet>t2,pi\<bullet>y2) \<in> rec (pi\<bullet>f1) (pi\<bullet>f2) (pi\<bullet>f3)"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   230
  from a1 a2 have a1': "finite ((supp (pi\<bullet>y1))::name set)" and a2': "finite ((supp (pi\<bullet>y2))::name set)"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   231
    by (simp_all add: pt_supp_finite_pi[OF pt_name_inst, OF at_name_inst])
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   232
  let ?g ="pi\<bullet>(\<lambda>(pi'::name prm). f2 (y1 pi') (y2 pi'))"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   233
  and ?g'="\<lambda>(pi'::name prm). (pi\<bullet>f2) ((pi\<bullet>y1) pi') ((pi\<bullet>y2) pi')"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   234
  have "?g'=?g" by  (simp add: expand_fun_eq perm_fun_def pt_rev_pi[OF pt_name_inst, OF at_name_inst])
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   235
  thus ?case using a1' a2' a3 a4 by (force intro: rec.r2 rec_trans)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   236
next
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   237
  case (r3 a t y)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   238
  assume a1: "finite ((supp y)::name set)"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   239
  and    a2: "(pi\<bullet>t,pi\<bullet>y) \<in> rec (pi\<bullet>f1) (pi\<bullet>f2) (pi\<bullet>f3)"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   240
  from a1 have a1': "finite ((supp (pi\<bullet>y))::name set)" 
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   241
    by (simp add: pt_supp_finite_pi[OF pt_name_inst, OF at_name_inst])
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   242
  let ?g ="pi\<bullet>(\<lambda>(pi'::name prm). fresh_fun (\<lambda>a'. f3 a' (y (pi'@[(a,a')]))))"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   243
  and ?g'="(\<lambda>(pi'::name prm). fresh_fun (\<lambda>a'. (pi\<bullet>f3) a' ((pi\<bullet>y) (pi'@[((pi\<bullet>a),a')]))))"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   244
  have "?g'=?g" 
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   245
  proof (auto simp add: expand_fun_eq perm_fun_def pt_rev_pi[OF pt_name_inst, OF at_name_inst] 
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   246
                        perm_append)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   247
    fix pi'::"name prm"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   248
    let ?h  = "\<lambda>a'. pi\<bullet>(f3 ((rev pi)\<bullet>a') (y (((rev pi)\<bullet>pi')@[(a,(rev pi)\<bullet>a')])))"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   249
    and ?h' = "\<lambda>a'. f3 a' (y (((rev pi)\<bullet>pi')@[(a,a')]))"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   250
    have fs_f3: "finite ((supp f3)::name set)" using f by (simp add: supp_prod)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   251
    have fs_h': "finite ((supp ?h')::name set)"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   252
    proof -
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   253
      have "((supp (f3,a,(rev pi)\<bullet>pi',y))::name set) supports ?h'" 
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   254
	by (supports_simp add: perm_append)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   255
      moreover
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   256
      have "finite ((supp (f3,a,(rev pi)\<bullet>pi',y))::name set)" using a1 fs_f3 
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   257
	by (simp add: supp_prod fs_name1)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   258
      ultimately show ?thesis by (rule supports_finite)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   259
    qed
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   260
    have fcond: "\<exists>(a''::name). a''\<sharp>?h' \<and> a''\<sharp>(?h' a'')"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   261
      by (rule f3_freshness_conditions_simple[OF fs_f3, OF a1, OF c])
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   262
    have "fresh_fun ?h = fresh_fun (pi\<bullet>?h')"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   263
      by (simp add: perm_fun_def pt_rev_pi[OF pt_name_inst, OF at_name_inst])
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   264
    also have "\<dots> = pi\<bullet>(fresh_fun ?h')"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   265
      by (simp add: fresh_fun_equiv[OF pt_name_inst, OF at_name_inst, OF fs_h', OF fcond])
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   266
    finally show "fresh_fun ?h = pi\<bullet>(fresh_fun ?h')" .
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   267
  qed
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   268
  thus ?case using a1' a2 by (force intro: rec.r3 rec_trans)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   269
qed
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   270
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   271
lemma rec_perm:
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   272
  fixes f1 ::"('a::pt_name) f1_ty"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   273
  and   f2 ::"('a::pt_name) f2_ty"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   274
  and   f3 ::"('a::pt_name) f3_ty"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   275
  and   pi1::"name prm"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   276
  assumes f: "finite ((supp (f1,f2,f3))::name set)"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   277
  and     c: "\<exists>(a::name). a\<sharp>f3 \<and> (\<forall>(y::'a::pt_name). a\<sharp>f3 a y)"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   278
  and     a: "(t,y)\<in>rec f1 f2 f3"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   279
  shows "(pi1\<bullet>t, \<lambda>pi2. y (pi2@pi1))\<in>rec f1 f2 f3"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   280
proof -
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   281
  have lem: "\<forall>(y::name prm\<Rightarrow>('a::pt_name))(pi::name prm). 
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   282
             finite ((supp y)::name set) \<longrightarrow> finite ((supp (\<lambda>pi'. y (pi'@pi)))::name set)"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   283
  proof (intro strip)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   284
    fix y::"name prm\<Rightarrow>('a::pt_name)" and pi::"name prm"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   285
    assume  "finite ((supp y)::name set)"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   286
    hence "finite ((supp (y,pi))::name set)" by (simp add: supp_prod fs_name1)      
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   287
    moreover
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   288
    have  "((supp (y,pi))::name set) supports (\<lambda>pi'. y (pi'@pi))" 
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   289
      by (supports_simp add: perm_append)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   290
    ultimately show "finite ((supp (\<lambda>pi'. y (pi'@pi)))::name set)" by (simp add: supports_finite)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   291
  qed
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   292
from a
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   293
show ?thesis
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   294
proof (induct)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   295
  case (r1 c)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   296
  show ?case
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   297
    by (auto simp add: pt2[OF pt_name_inst], rule rec.r1)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   298
next
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   299
  case (r2 t1 t2 y1 y2)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   300
  thus ?case using lem by (auto intro!: rec.r2) 
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   301
next
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   302
  case (r3 c t y)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   303
  assume a0: "(t,y)\<in>rec f1 f2 f3"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   304
  and    a1: "finite ((supp y)::name set)"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   305
  and    a2: "(pi1\<bullet>t,\<lambda>pi2. y (pi2@pi1))\<in>rec f1 f2 f3"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   306
  from f have f': "finite ((supp f3)::name set)" by (simp add: supp_prod)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   307
  show ?case
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   308
  proof(simp)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   309
    have a3: "finite ((supp (\<lambda>pi2. y (pi2@pi1)))::name set)" using lem a1 by force
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   310
    let ?g' = "\<lambda>(pi::name prm). fresh_fun (\<lambda>a'. f3 a' ((\<lambda>pi2. y (pi2@pi1)) (pi@[(pi1\<bullet>c,a')])))"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   311
    and ?g  = "\<lambda>(pi::name prm). fresh_fun (\<lambda>a'. f3 a' (y (pi@[(pi1\<bullet>c,a')]@pi1)))"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   312
    and ?h  = "\<lambda>(pi::name prm). fresh_fun (\<lambda>a'. f3 a' (y (pi@pi1@[(c,a')])))"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   313
    have eq1: "?g = ?g'" by simp
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   314
    have eq2: "?g'= ?h" 
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   315
    proof (auto simp only: expand_fun_eq)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   316
      fix pi::"name prm"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   317
      let ?q  = "\<lambda>a'. f3 a' (y ((pi@[(pi1\<bullet>c,a')])@pi1))"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   318
      and ?q' = "\<lambda>a'. f3 a' (y (((pi@pi1)@[(c,(rev pi1)\<bullet>a')])))"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   319
      and ?r  = "\<lambda>a'. f3 a' (y ((pi@pi1)@[(c,a')]))"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   320
      and ?r' = "\<lambda>a'. f3 a' (y (pi@(pi1@[(c,a')])))"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   321
      have eq3a: "?r = ?r'" by simp
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   322
      have eq3: "?q = ?q'"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   323
      proof (auto simp only: expand_fun_eq)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   324
	fix a'::"name"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   325
	have "(y ((pi@[(pi1\<bullet>c,a')])@pi1)) =  (y (((pi@pi1)@[(c,(rev pi1)\<bullet>a')])))" 
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   326
	  proof -
18298
f7899cb24c79 changed induction principle and everything to conform with the
urbanc
parents: 18284
diff changeset
   327
	    have "((pi@[(pi1\<bullet>c,a')])@pi1) \<triangleq> ((pi@pi1)@[(c,(rev pi1)\<bullet>a')])"
18106
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   328
	    by (force simp add: prm_eq_def at_append[OF at_name_inst] 
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   329
                   at_calc[OF at_name_inst] at_bij[OF at_name_inst] 
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   330
                   at_pi_rev[OF at_name_inst] at_rev_pi[OF at_name_inst])
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   331
	    with a0 show ?thesis by (rule rec_prm_eq)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   332
	  qed
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   333
	thus "f3 a' (y ((pi@[(pi1\<bullet>c,a')])@pi1)) = f3 a' (y (((pi@pi1)@[(c,(rev pi1)\<bullet>a')])))" by simp
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   334
      qed
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   335
      have fs_a: "finite ((supp ?q')::name set)"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   336
      proof -
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   337
	have "((supp (f3,c,(pi@pi1),(rev pi1),y))::name set) supports ?q'" 
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   338
	  by (supports_simp add: perm_append fresh_list_append fresh_list_rev)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   339
	moreover
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   340
	have "finite ((supp (f3,c,(pi@pi1),(rev pi1),y))::name set)" using f' a1
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   341
	  by (simp add: supp_prod fs_name1)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   342
	ultimately show ?thesis by (rule supports_finite)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   343
      qed
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   344
      have fs_b: "finite ((supp ?r)::name set)"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   345
      proof -
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   346
	have "((supp (f3,c,(pi@pi1),y))::name set) supports ?r" 
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   347
	  by (supports_simp add: perm_append fresh_list_append)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   348
	moreover
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   349
	have "finite ((supp (f3,c,(pi@pi1),y))::name set)" using f' a1
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   350
	  by (simp add: supp_prod fs_name1)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   351
	ultimately show ?thesis by (rule supports_finite)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   352
      qed
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   353
      have c1: "\<exists>(a''::name). a''\<sharp>?q' \<and> a''\<sharp>(?q' a'')"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   354
	by (rule f3_freshness_conditions[OF f', OF a1, OF c])
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   355
      have c2: "\<exists>(a''::name). a''\<sharp>?r \<and> a''\<sharp>(?r a'')"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   356
	by (rule f3_freshness_conditions_simple[OF f', OF a1, OF c])
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   357
      have c3: "\<exists>(d::name). d\<sharp>(?q',?r,(rev pi1))" 
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   358
	by (rule at_exists_fresh[OF at_name_inst], 
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   359
            simp only: finite_Un supp_prod fs_a fs_b fs_name1, simp)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   360
      then obtain d::"name" where d1: "d\<sharp>?q'" and d2: "d\<sharp>?r" and d3: "d\<sharp>(rev pi1)" 
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   361
	by (auto simp only: fresh_prod)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   362
      have eq4: "(rev pi1)\<bullet>d = d" using d3 by (simp add: at_prm_fresh[OF at_name_inst])
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   363
      have "fresh_fun ?q = fresh_fun ?q'" using eq3 by simp
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   364
      also have "\<dots> = ?q' d" using fs_a c1 d1 
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   365
	by (simp add: fresh_fun_app[OF pt_name_inst, OF at_name_inst])
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   366
      also have "\<dots> = ?r d" using fs_b c2 d2 eq4
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   367
	by (simp add: fresh_fun_app[OF pt_name_inst, OF at_name_inst])
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   368
      also have "\<dots> = fresh_fun ?r" using fs_b c2 d2 
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   369
	by (simp add: fresh_fun_app[OF pt_name_inst, OF at_name_inst])
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   370
      finally show "fresh_fun ?q = fresh_fun ?r'" by simp
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   371
    qed
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   372
    from a3 a2 have "(Lam [(pi1\<bullet>c)].(pi1\<bullet>t), ?g')\<in>rec f1 f2 f3" by (rule rec.r3)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   373
    thus "(Lam [(pi1\<bullet>c)].(pi1\<bullet>t), ?h)\<in>rec f1 f2 f3" using eq2 by simp
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   374
  qed
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   375
qed
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   376
qed    
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   377
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   378
lemma rec_perm_rev:
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   379
  fixes f1::"('a::pt_name) f1_ty"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   380
  and   f2::"('a::pt_name) f2_ty"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   381
  and   f3::"('a::pt_name) f3_ty"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   382
  assumes f: "finite ((supp (f1,f2,f3))::name set)"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   383
  and     c: "\<exists>(a::name). a\<sharp>f3 \<and> (\<forall>(y::'a::pt_name). a\<sharp>f3 a y)"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   384
  and     a: "(pi\<bullet>t,y)\<in>rec f1 f2 f3"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   385
  shows "(t, \<lambda>pi2. y (pi2@(rev pi)))\<in>rec f1 f2 f3"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   386
proof - 
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   387
  from a have "((rev pi)\<bullet>(pi\<bullet>t),\<lambda>pi2. y (pi2@(rev pi)))\<in>rec f1 f2 f3"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   388
    by (rule rec_perm[OF f, OF c])
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   389
  thus ?thesis by (simp add: pt_rev_pi[OF pt_name_inst, OF at_name_inst])
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   390
qed
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   391
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   392
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   393
lemma rec_unique:
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   394
  fixes f1::"('a::pt_name) f1_ty"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   395
  and   f2::"('a::pt_name) f2_ty"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   396
  and   f3::"('a::pt_name) f3_ty"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   397
  assumes f: "finite ((supp (f1,f2,f3))::name set)"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   398
  and     c: "\<exists>(a::name). a\<sharp>f3 \<and> (\<forall>(y::'a::pt_name). a\<sharp>f3 a y)"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   399
  and     a: "(t,y)\<in>rec f1 f2 f3"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   400
  shows "\<forall>(y'::name prm\<Rightarrow>('a::pt_name))(pi::name prm).
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   401
         (t,y')\<in>rec f1 f2 f3 \<longrightarrow> y pi = y' pi"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   402
using a
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   403
proof (induct)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   404
  case (r1 c)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   405
  show ?case 
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   406
   apply(auto)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   407
   apply(ind_cases "(Var c, y') \<in> rec f1 f2 f3")
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   408
   apply(simp_all add: lam.distinct lam.inject)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   409
   done
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   410
next
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   411
  case (r2 t1 t2 y1 y2)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   412
  thus ?case 
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   413
    apply(clarify)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   414
    apply(ind_cases "(App t1 t2, y') \<in> rec f1 f2 f3") 
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   415
    apply(simp_all (no_asm_use) only: lam.distinct lam.inject) 
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   416
    apply(clarify)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   417
    apply(drule_tac x="y1" in spec)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   418
    apply(drule_tac x="y2" in spec)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   419
    apply(auto)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   420
    done
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   421
next
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   422
  case (r3 c t y)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   423
  assume i1: "finite ((supp y)::name set)"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   424
  and    i2: "(t,y)\<in>rec f1 f2 f3"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   425
  and    i3: "\<forall>(y'::name prm\<Rightarrow>('a::pt_name))(pi::name prm).
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   426
              (t,y')\<in>rec f1 f2 f3 \<longrightarrow> y pi = y' pi"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   427
  from f have f': "finite ((supp f3)::name set)" by (simp add: supp_prod)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   428
  show ?case 
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   429
  proof (auto)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   430
    fix y'::"name prm\<Rightarrow>('a::pt_name)" and pi::"name prm"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   431
    assume i4: "(Lam [c].t, y') \<in> rec f1 f2 f3"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   432
    from i4 show "fresh_fun (\<lambda>a'. f3 a' (y (pi@[(c,a')]))) = y' pi"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   433
    proof (cases, simp_all add: lam.distinct lam.inject, auto)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   434
      fix a::"name" and t'::"lam" and y''::"name prm\<Rightarrow>('a::pt_name)"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   435
      assume i5: "[c].t = [a].t'"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   436
      and    i6: "(t',y'')\<in>rec f1 f2 f3"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   437
      and    i6':"finite ((supp y'')::name set)"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   438
      let ?g = "\<lambda>a'. f3 a' (y  (pi@[(c,a')]))"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   439
      and ?h = "\<lambda>a'. f3 a' (y'' (pi@[(a,a')]))"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   440
      show "fresh_fun ?g = fresh_fun ?h" using i5
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   441
      proof (cases "a=c")
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   442
	case True
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   443
	assume i7: "a=c"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   444
	with i5 have i8: "t=t'" by (simp add: alpha)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   445
	show "fresh_fun ?g = fresh_fun ?h" using i3 i6 i7 i8 by simp
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   446
      next
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   447
	case False
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   448
	assume i9: "a\<noteq>c"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   449
	with i5[symmetric] have i10: "t'=[(a,c)]\<bullet>t" and i11: "a\<sharp>t" by (simp_all add: alpha)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   450
	have r1: "finite ((supp ?g)::name set)" 
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   451
	proof -
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   452
	  have "((supp (f3,c,pi,y))::name set) supports ?g" 
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   453
	    by (supports_simp add: perm_append)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   454
	  moreover
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   455
	  have "finite ((supp (f3,c,pi,y))::name set)" using f' i1
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   456
	    by (simp add: supp_prod fs_name1)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   457
	  ultimately show ?thesis by (rule supports_finite)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   458
	qed
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   459
	have r2: "finite ((supp ?h)::name set)" 
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   460
	proof -
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   461
	  have "((supp (f3,a,pi,y''))::name set) supports ?h" 
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   462
	    by (supports_simp add: perm_append)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   463
	  moreover
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   464
	  have "finite ((supp (f3,a,pi,y''))::name set)" using f' i6'
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   465
	    by (simp add: supp_prod fs_name1)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   466
	  ultimately show ?thesis by (rule supports_finite)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   467
	qed
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   468
	have c1: "\<exists>(a''::name). a''\<sharp>?g \<and> a''\<sharp>(?g a'')"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   469
	  by (rule f3_freshness_conditions_simple[OF f', OF i1, OF c])
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   470
	have c2: "\<exists>(a''::name). a''\<sharp>?h \<and> a''\<sharp>(?h a'')"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   471
	  by (rule f3_freshness_conditions_simple[OF f', OF i6', OF c])
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   472
	have "\<exists>(d::name). d\<sharp>(?g,?h,t,a,c)" 
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   473
	  by (rule at_exists_fresh[OF at_name_inst], 
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   474
              simp only: finite_Un supp_prod r1 r2 fs_name1, simp)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   475
	then obtain d::"name" 
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   476
	  where f1: "d\<sharp>?g" and f2: "d\<sharp>?h" and f3: "d\<sharp>t" and f4: "d\<noteq>a" and f5: "d\<noteq>c" 
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   477
	  by (force simp add: fresh_prod at_fresh[OF at_name_inst] at_fresh[OF at_name_inst])
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   478
	have g1: "[(a,d)]\<bullet>t = t" 
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   479
	  by (rule pt_fresh_fresh[OF pt_name_inst, OF at_name_inst, OF i11, OF f3]) 
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   480
	from i6 have "(([(a,c)]@[(a,d)])\<bullet>t,y'')\<in>rec f1 f2 f3" using g1 i10 by (simp only: pt_name2)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   481
	hence "(t, \<lambda>pi2. y'' (pi2@(rev ([(a,c)]@[(a,d)]))))\<in>rec f1 f2 f3"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   482
	  by (simp only: rec_perm_rev[OF f, OF c])
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   483
	hence g2: "(t, \<lambda>pi2. y'' (pi2@([(a,d)]@[(a,c)])))\<in>rec f1 f2 f3" by simp
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   484
	have "distinct [a,c,d]" using i9 f4 f5 by force
18298
f7899cb24c79 changed induction principle and everything to conform with the
urbanc
parents: 18284
diff changeset
   485
	hence g3: "(pi@[(c,d)]@[(a,d)]@[(a,c)]) \<triangleq> (pi@[(a,d)])"
18106
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   486
	  by (force simp add: prm_eq_def at_calc[OF at_name_inst] at_append[OF at_name_inst])
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   487
	have "fresh_fun ?g = ?g d" using r1 c1 f1
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   488
	  by (simp add: fresh_fun_app[OF pt_name_inst, OF at_name_inst])
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   489
	also have "\<dots> = f3 d ((\<lambda>pi2. y'' (pi2@([(a,d)]@[(a,c)]))) (pi@[(c,d)]))" using i3 g2 by simp 
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   490
	also have "\<dots> = f3 d (y'' (pi@[(c,d)]@[(a,d)]@[(a,c)]))" by simp
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   491
	also have "\<dots> = f3 d (y'' (pi@[(a,d)]))" using i6 g3 by (simp add: rec_prm_eq)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   492
	also have "\<dots> = fresh_fun ?h" using r2 c2 f2
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   493
	  by (simp add: fresh_fun_app[OF pt_name_inst, OF at_name_inst])
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   494
	finally show "fresh_fun ?g = fresh_fun ?h" .
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   495
      qed
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   496
    qed
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   497
  qed
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   498
qed
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   499
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   500
lemma rec_total_aux:
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   501
  fixes f1::"('a::pt_name) f1_ty"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   502
  and   f2::"('a::pt_name) f2_ty"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   503
  and   f3::"('a::pt_name) f3_ty"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   504
  assumes f: "finite ((supp (f1,f2,f3))::name set)"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   505
  and     c: "\<exists>(a::name). a\<sharp>f3 \<and> (\<forall>(y::'a::pt_name). a\<sharp>f3 a y)"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   506
  shows "\<exists>(y::name prm\<Rightarrow>('a::pt_name)). ((t,y)\<in>rec f1 f2 f3) \<and> (finite ((supp y)::name set))"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   507
proof (induct t rule: lam.induct_weak)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   508
  case (Var c)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   509
  have a1: "(Var c,\<lambda>(pi::name prm). f1 (pi\<bullet>c))\<in>rec f1 f2 f3" by (rule rec.r1)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   510
  have a2: "finite ((supp (\<lambda>(pi::name prm). f1 (pi\<bullet>c)))::name set)"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   511
  proof -
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   512
    have "((supp (f1,c))::name set) supports (\<lambda>(pi::name prm). f1 (pi\<bullet>c))" by (supports_simp)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   513
    moreover have "finite ((supp (f1,c))::name set)" using f by (simp add: supp_prod fs_name1)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   514
    ultimately show ?thesis by (rule supports_finite)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   515
  qed
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   516
  from a1 a2 show ?case by force
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   517
next
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   518
  case (App t1 t2)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   519
  assume "\<exists>y1. (t1,y1)\<in>rec f1 f2 f3 \<and> finite ((supp y1)::name set)"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   520
  then obtain y1::"name prm \<Rightarrow> ('a::pt_name)"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   521
    where a11: "(t1,y1)\<in>rec f1 f2 f3" and a12: "finite ((supp y1)::name set)" by force
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   522
  assume "\<exists>y2. (t2,y2)\<in>rec f1 f2 f3 \<and> finite ((supp y2)::name set)"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   523
  then obtain y2::"name prm \<Rightarrow> ('a::pt_name)"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   524
    where a21: "(t2,y2)\<in>rec f1 f2 f3" and a22: "finite ((supp y2)::name set)" by force
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   525
  
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   526
  have a1: "(App t1 t2,\<lambda>(pi::name prm). f2 (y1 pi) (y2 pi))\<in>rec f1 f2 f3"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   527
    using a12 a11 a22 a21 by (rule rec.r2)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   528
  have a2: "finite ((supp (\<lambda>(pi::name prm). f2 (y1 pi) (y2 pi)))::name set)"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   529
  proof -
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   530
    have "((supp (f2,y1,y2))::name set) supports (\<lambda>(pi::name prm). f2 (y1 pi) (y2 pi))" 
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   531
      by (supports_simp)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   532
    moreover have "finite ((supp (f2,y1,y2))::name set)" using f a21 a22 
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   533
      by (simp add: supp_prod fs_name1)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   534
    ultimately show ?thesis by (rule supports_finite)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   535
  qed
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   536
  from a1 a2 show ?case by force
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   537
next
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   538
  case (Lam a t)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   539
  assume "\<exists>y. (t,y)\<in>rec f1 f2 f3 \<and> finite ((supp y)::name set)"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   540
  then obtain y::"name prm \<Rightarrow> ('a::pt_name)"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   541
    where a11: "(t,y)\<in>rec f1 f2 f3" and a12: "finite ((supp y)::name set)" by force
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   542
  from f have f': "finite ((supp f3)::name set)" by (simp add: supp_prod)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   543
  have a1: "(Lam [a].t,\<lambda>(pi::name prm). fresh_fun (\<lambda>a'. f3 a' (y (pi@[(a,a')]))))\<in>rec f1 f2 f3"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   544
    using a12 a11 by (rule rec.r3)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   545
  have a2: "finite ((supp (\<lambda>pi. fresh_fun (\<lambda>a'. f3 a' (y (pi@[(a,a')])))))::name set)" 
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   546
    using f' a12 c by (rule f3_fresh_fun_supp_finite)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   547
  from a1 a2 show ?case by force
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   548
qed
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   549
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   550
lemma rec_total:
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   551
  fixes f1::"('a::pt_name) f1_ty"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   552
  and   f2::"('a::pt_name) f2_ty"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   553
  and   f3::"('a::pt_name) f3_ty"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   554
  assumes f: "finite ((supp (f1,f2,f3))::name set)"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   555
  and     c: "\<exists>(a::name). a\<sharp>f3 \<and> (\<forall>(y::'a::pt_name). a\<sharp>f3 a y)"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   556
  shows "\<exists>(y::name prm\<Rightarrow>('a::pt_name)). ((t,y)\<in>rec f1 f2 f3)"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   557
proof -
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   558
  have "\<exists>y. ((t,y)\<in>rec f1 f2 f3) \<and> (finite ((supp y)::name set))"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   559
    by (rule rec_total_aux[OF f, OF c])
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   560
  thus ?thesis by force
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   561
qed
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   562
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   563
lemma rec_function:
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   564
  fixes f1::"('a::pt_name) f1_ty"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   565
  and   f2::"('a::pt_name) f2_ty"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   566
  and   f3::"('a::pt_name) f3_ty"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   567
  assumes f: "finite ((supp (f1,f2,f3))::name set)"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   568
  and     c: "\<exists>(a::name). a\<sharp>f3 \<and> (\<forall>(y::'a::pt_name). a\<sharp>f3 a y)"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   569
  shows "\<exists>!y. (t,y)\<in>rec f1 f2 f3"
18758
e8a11e84864c made change for ex1
urbanc
parents: 18659
diff changeset
   570
proof (rule ex_ex1I)
18106
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   571
  case goal1
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   572
  show ?case by (rule rec_total[OF f, OF c])
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   573
next
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   574
  case (goal2 y1 y2)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   575
  assume a1: "(t,y1)\<in>rec f1 f2 f3" and a2: "(t,y2)\<in>rec f1 f2 f3"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   576
  hence "\<forall>pi. y1 pi = y2 pi" using rec_unique[OF f, OF c] by force
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   577
  thus ?case by (force simp add: expand_fun_eq) 
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   578
qed
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   579
  
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   580
lemma theI2':
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   581
  assumes a1: "P a" 
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   582
  and     a2: "\<exists>!x. P x" 
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   583
  and     a3: "P a \<Longrightarrow> Q a"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   584
  shows "Q (THE x. P x)"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   585
apply(rule theI2)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   586
apply(rule a1)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   587
apply(subgoal_tac "\<exists>!x. P x")
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   588
apply(auto intro: a1 simp add: Ex1_def)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   589
apply(fold Ex1_def)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   590
apply(rule a2)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   591
apply(subgoal_tac "x=a")
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   592
apply(simp)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   593
apply(rule a3)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   594
apply(assumption)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   595
apply(subgoal_tac "\<exists>!x. P x")
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   596
apply(auto intro: a1 simp add: Ex1_def)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   597
apply(fold Ex1_def)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   598
apply(rule a2)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   599
done
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   600
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   601
lemma rfun'_equiv:
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   602
  fixes f1::"('a::pt_name) f1_ty"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   603
  and   f2::"('a::pt_name) f2_ty"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   604
  and   f3::"('a::pt_name) f3_ty"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   605
  and   pi::"name prm"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   606
  and   t ::"lam"  
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   607
  assumes f: "finite ((supp (f1,f2,f3))::name set)"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   608
  and     c: "\<exists>(a::name). a\<sharp>f3 \<and> (\<forall>(y::'a::pt_name). a\<sharp>f3 a y)"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   609
  shows "pi\<bullet>(rfun' f1 f2 f3 t) = rfun' (pi\<bullet>f1) (pi\<bullet>f2) (pi\<bullet>f3) (pi\<bullet>t)"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   610
apply(auto simp add: rfun'_def)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   611
apply(subgoal_tac "\<exists>y. (t,y)\<in>rec f1 f2 f3 \<and> finite ((supp y)::name set)")
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   612
apply(auto)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   613
apply(rule sym)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   614
apply(rule_tac a="y" in theI2')
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   615
apply(assumption)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   616
apply(rule rec_function[OF f, OF c])
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   617
apply(rule the1_equality)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   618
apply(rule rec_function)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   619
apply(subgoal_tac "finite ((supp (f1,f2,f3))::name set)")
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   620
apply(simp add: supp_prod)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   621
apply(simp add: pt_supp_finite_pi[OF pt_name_inst, OF at_name_inst])
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   622
apply(rule f)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   623
apply(subgoal_tac "\<exists>(a::name). a\<sharp>f3 \<and> (\<forall>(y::'a::pt_name). a\<sharp>f3 a y)")
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   624
apply(auto)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   625
apply(rule_tac x="pi\<bullet>a" in exI)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   626
apply(auto)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   627
apply(simp add: pt_fresh_bij[OF pt_name_inst, OF at_name_inst])
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   628
apply(drule_tac x="(rev pi)\<bullet>x" in spec)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   629
apply(subgoal_tac "(pi\<bullet>f3) (pi\<bullet>a) x  = pi\<bullet>(f3 a ((rev pi)\<bullet>x))")
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   630
apply(simp add: pt_fresh_bij[OF pt_name_inst, OF at_name_inst])
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   631
apply(subgoal_tac "pi\<bullet>(f3 a ((rev pi)\<bullet>x)) = (pi\<bullet>f3) (pi\<bullet>a) (pi\<bullet>((rev pi)\<bullet>x))")
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   632
apply(simp)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   633
apply(simp add: pt_pi_rev[OF pt_name_inst, OF at_name_inst])
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   634
apply(simp add: pt_fun_app_eq[OF pt_name_inst, OF at_name_inst])
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   635
apply(rule c)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   636
apply(rule rec_prm_equiv)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   637
apply(rule f, rule c, assumption)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   638
apply(rule rec_total_aux)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   639
apply(rule f)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   640
apply(rule c)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   641
done
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   642
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   643
lemma rfun'_supports:
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   644
  fixes f1::"('a::pt_name) f1_ty"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   645
  and   f2::"('a::pt_name) f2_ty"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   646
  and   f3::"('a::pt_name) f3_ty"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   647
  assumes f: "finite ((supp (f1,f2,f3))::name set)"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   648
  and     c: "\<exists>(a::name). a\<sharp>f3 \<and> (\<forall>(y::'a::pt_name). a\<sharp>f3 a y)"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   649
  shows "((supp (f1,f2,f3,t))::name set) supports (rfun' f1 f2 f3 t)"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   650
proof (auto simp add: "op supports_def" fresh_def[symmetric])
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   651
  fix a::"name" and b::"name"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   652
  assume a1: "a\<sharp>(f1,f2,f3,t)"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   653
  and    a2: "b\<sharp>(f1,f2,f3,t)"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   654
  from a1 a2 have "[(a,b)]\<bullet>f1=f1" and "[(a,b)]\<bullet>f2=f2" and "[(a,b)]\<bullet>f3=f3" and "[(a,b)]\<bullet>t=t"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   655
    by (simp_all add: pt_fresh_fresh[OF pt_name_inst, OF at_name_inst] fresh_prod)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   656
  thus "[(a,b)]\<bullet>(rfun' f1 f2 f3 t) = rfun' f1 f2 f3 t"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   657
    by (simp add: rfun'_equiv[OF f, OF c])
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   658
qed
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   659
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   660
lemma rfun'_finite_supp:
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   661
  fixes f1::"('a::pt_name) f1_ty"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   662
  and   f2::"('a::pt_name) f2_ty"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   663
  and   f3::"('a::pt_name) f3_ty"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   664
  assumes f: "finite ((supp (f1,f2,f3))::name set)"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   665
  and     c: "\<exists>(a::name). a\<sharp>f3 \<and> (\<forall>(y::'a::pt_name). a\<sharp>f3 a y)"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   666
  shows "finite ((supp (rfun' f1 f2 f3 t))::name set)"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   667
apply(rule supports_finite)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   668
apply(rule rfun'_supports[OF f, OF c])
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   669
apply(subgoal_tac "finite ((supp (f1,f2,f3))::name set)")
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   670
apply(simp add: supp_prod fs_name1)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   671
apply(rule f)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   672
done
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   673
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   674
lemma rfun'_prm:
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   675
  fixes f1::"('a::pt_name) f1_ty"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   676
  and   f2::"('a::pt_name) f2_ty"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   677
  and   f3::"('a::pt_name) f3_ty"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   678
  and   pi1::"name prm"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   679
  and   pi2::"name prm"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   680
  and   t ::"lam"  
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   681
  assumes f: "finite ((supp (f1,f2,f3))::name set)"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   682
  and     c: "\<exists>(a::name). a\<sharp>f3 \<and> (\<forall>(y::'a::pt_name). a\<sharp>f3 a y)"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   683
  shows "rfun' f1 f2 f3 (pi1\<bullet>t) pi2 = rfun' f1 f2 f3 t (pi2@pi1)"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   684
apply(auto simp add: rfun'_def)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   685
apply(subgoal_tac "\<exists>y. (t,y)\<in>rec f1 f2 f3 \<and> finite ((supp y)::name set)")
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   686
apply(auto)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   687
apply(rule_tac a="y" in theI2')
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   688
apply(assumption)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   689
apply(rule rec_function[OF f, OF c])
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   690
apply(rule_tac a="\<lambda>pi2. y (pi2@pi1)" in theI2')
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   691
apply(rule rec_perm)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   692
apply(rule f, rule c)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   693
apply(assumption)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   694
apply(rule rec_function)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   695
apply(rule f)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   696
apply(rule c)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   697
apply(simp)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   698
apply(rule rec_total_aux)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   699
apply(rule f)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   700
apply(rule c)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   701
done
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   702
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   703
lemma rfun_Var:
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   704
  fixes f1::"('a::pt_name) f1_ty"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   705
  and   f2::"('a::pt_name) f2_ty"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   706
  and   f3::"('a::pt_name) f3_ty"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   707
  assumes f: "finite ((supp (f1,f2,f3))::name set)"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   708
  and     c: "\<exists>(a::name). a\<sharp>f3 \<and> (\<forall>(y::'a::pt_name). a\<sharp>f3 a y)"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   709
  shows "rfun f1 f2 f3 (Var c) = (f1 c)"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   710
apply(auto simp add: rfun_def rfun'_def)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   711
apply(subgoal_tac "(THE y. (Var c, y) \<in> rec f1 f2 f3) = (\<lambda>(pi::name prm). f1 (pi\<bullet>c))")(*A*)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   712
apply(simp)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   713
apply(rule the1_equality)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   714
apply(rule rec_function)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   715
apply(rule f)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   716
apply(rule c)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   717
apply(rule rec.r1)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   718
done
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   719
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   720
lemma rfun_App:
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   721
  fixes f1::"('a::pt_name) f1_ty"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   722
  and   f2::"('a::pt_name) f2_ty"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   723
  and   f3::"('a::pt_name) f3_ty"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   724
  assumes f: "finite ((supp (f1,f2,f3))::name set)"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   725
  and     c: "\<exists>(a::name). a\<sharp>f3 \<and> (\<forall>(y::'a::pt_name). a\<sharp>f3 a y)"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   726
  shows "rfun f1 f2 f3 (App t1 t2) = (f2 (rfun f1 f2 f3 t1) (rfun f1 f2 f3 t2))"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   727
apply(auto simp add: rfun_def rfun'_def)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   728
apply(subgoal_tac "(THE y. (App t1 t2, y)\<in>rec f1 f2 f3) = 
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   729
      (\<lambda>(pi::name prm). f2 ((rfun' f1 f2 f3 t1) pi) ((rfun' f1 f2 f3 t2) pi))")(*A*)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   730
apply(simp add: rfun'_def)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   731
apply(rule the1_equality)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   732
apply(rule rec_function[OF f, OF c])
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   733
apply(rule rec.r2)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   734
apply(rule rfun'_finite_supp[OF f, OF c])
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   735
apply(subgoal_tac "\<exists>y. (t1,y)\<in>rec f1 f2 f3")
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   736
apply(erule exE, simp add: rfun'_def)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   737
apply(rule_tac a="y" in theI2')
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   738
apply(assumption)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   739
apply(rule rec_function[OF f, OF c])
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   740
apply(assumption)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   741
apply(rule rec_total[OF f, OF c])
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   742
apply(rule rfun'_finite_supp[OF f, OF c])
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   743
apply(subgoal_tac "\<exists>y. (t2,y)\<in>rec f1 f2 f3")
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   744
apply(auto simp add: rfun'_def)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   745
apply(rule_tac a="y" in theI2')
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   746
apply(assumption)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   747
apply(rule rec_function[OF f, OF c])
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   748
apply(assumption)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   749
apply(rule rec_total[OF f, OF c])
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   750
done 
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   751
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   752
lemma rfun_Lam_aux1:
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   753
  fixes f1::"('a::pt_name) f1_ty"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   754
  and   f2::"('a::pt_name) f2_ty"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   755
  and   f3::"('a::pt_name) f3_ty"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   756
  assumes f: "finite ((supp (f1,f2,f3))::name set)"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   757
  and     c: "\<exists>(a::name). a\<sharp>f3 \<and> (\<forall>(y::'a::pt_name). a\<sharp>f3 a y)"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   758
  shows "rfun f1 f2 f3 (Lam [a].t) = fresh_fun (\<lambda>a'. f3 a' (rfun' f1 f2 f3 t ([]@[(a,a')])))"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   759
apply(simp add: rfun_def rfun'_def)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   760
apply(subgoal_tac "(THE y. (Lam [a].t, y)\<in>rec f1 f2 f3) = 
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   761
        (\<lambda>(pi::name prm). fresh_fun(\<lambda>a'. f3 a' ((rfun' f1 f2 f3 t) (pi@[(a,a')]))))")(*A*)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   762
apply(simp add: rfun'_def[symmetric])
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   763
apply(rule the1_equality)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   764
apply(rule rec_function[OF f, OF c])
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   765
apply(rule rec.r3)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   766
apply(rule rfun'_finite_supp[OF f, OF c])
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   767
apply(subgoal_tac "\<exists>y. (t,y)\<in>rec f1 f2 f3")
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   768
apply(erule exE, simp add: rfun'_def)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   769
apply(rule_tac a="y" in theI2')
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   770
apply(assumption)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   771
apply(rule rec_function[OF f, OF c])
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   772
apply(assumption)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   773
apply(rule rec_total[OF f, OF c])
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   774
done
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   775
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   776
lemma rfun_Lam_aux2:
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   777
  fixes f1::"('a::pt_name) f1_ty"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   778
  and   f2::"('a::pt_name) f2_ty"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   779
  and   f3::"('a::pt_name) f3_ty"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   780
  assumes f: "finite ((supp (f1,f2,f3))::name set)"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   781
  and     c: "\<exists>(a::name). a\<sharp>f3 \<and> (\<forall>(y::'a::pt_name). a\<sharp>f3 a y)"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   782
  and     a: "b\<sharp>(a,t,f1,f2,f3)"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   783
  shows "rfun f1 f2 f3 (Lam [b].([(a,b)]\<bullet>t)) = f3 b (rfun f1 f2 f3 ([(a,b)]\<bullet>t))"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   784
proof -
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   785
  from f have f': "finite ((supp f3)::name set)" by (simp add: supp_prod)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   786
  have eq1: "rfun f1 f2 f3 (Lam [b].([(a,b)]\<bullet>t)) = rfun f1 f2 f3 (Lam [a].t)"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   787
  proof -
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   788
    have "Lam [a].t = Lam [b].([(a,b)]\<bullet>t)" using a
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   789
      by (force simp add: lam.inject alpha fresh_prod at_fresh[OF at_name_inst]
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   790
             pt_swap_bij[OF pt_name_inst, OF at_name_inst] 
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   791
             pt_fresh_left[OF pt_name_inst, OF at_name_inst] at_calc[OF at_name_inst])
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   792
    thus ?thesis by simp
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   793
  qed
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   794
  let ?g = "(\<lambda>a'. f3 a' (rfun' f1 f2 f3 t ([]@[(a,a')])))"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   795
  have a0: "((supp (f3,a,([]::name prm),rfun' f1 f2 f3 t))::name set) supports ?g"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   796
    by (supports_simp add: perm_append)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   797
  have a1: "finite ((supp (f3,a,([]::name prm),rfun' f1 f2 f3 t))::name set)"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   798
    using f' by (simp add: supp_prod fs_name1 rfun'_finite_supp[OF f, OF c])
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   799
  from a0 a1 have a2: "finite ((supp ?g)::name set)"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   800
    by (rule supports_finite)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   801
  have c0: "finite ((supp (rfun' f1 f2 f3 t))::name set)"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   802
    by (rule rfun'_finite_supp[OF f, OF c])
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   803
  have c1: "\<exists>(a''::name). a''\<sharp>?g \<and> a''\<sharp>(?g a'')"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   804
    by (rule f3_freshness_conditions_simple[OF f', OF c0, OF c])
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   805
  have c2: "b\<sharp>?g"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   806
  proof -
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   807
    have fs_g: "finite ((supp (f1,f2,f3,t))::name set)" using f
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   808
      by (simp add: supp_prod fs_name1)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   809
    have "((supp (f1,f2,f3,t))::name set) supports (rfun' f1 f2 f3 t)"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   810
      by (simp add: rfun'_supports[OF f, OF c])
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   811
    hence c3: "b\<sharp>(rfun' f1 f2 f3 t)" using fs_g 
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   812
    proof(rule supports_fresh, simp add: fresh_def[symmetric])
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   813
      show "b\<sharp>(f1,f2,f3,t)" using a by (simp add: fresh_prod)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   814
    qed
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   815
    show ?thesis 
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   816
    proof(rule supports_fresh[OF a0, OF a1], simp add: fresh_def[symmetric])
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   817
      show "b\<sharp>(f3,a,([]::name prm),rfun' f1 f2 f3 t)" using a c3
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   818
	by (simp add: fresh_prod fresh_list_nil)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   819
    qed
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   820
  qed
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   821
  (* main proof *)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   822
  have "rfun f1 f2 f3 (Lam [b].([(a,b)]\<bullet>t)) = rfun f1 f2 f3 (Lam [a].t)" by (simp add: eq1)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   823
  also have "\<dots> = fresh_fun ?g" by (rule rfun_Lam_aux1[OF f, OF c])
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   824
  also have "\<dots> = ?g b" using c2
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   825
    by (rule fresh_fun_app[OF pt_name_inst, OF at_name_inst, OF a2, OF c1])
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   826
  also have "\<dots> = f3 b (rfun f1 f2 f3 ([(a,b)]\<bullet>t))"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   827
    by (simp add: rfun_def rfun'_prm[OF f, OF c])
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   828
  finally show "rfun f1 f2 f3 (Lam [b].([(a,b)]\<bullet>t)) = f3 b (rfun f1 f2 f3 ([(a,b)]\<bullet>t))" .
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   829
qed
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   830
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   831
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   832
lemma rfun_Lam:
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   833
  fixes f1::"('a::pt_name) f1_ty"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   834
  and   f2::"('a::pt_name) f2_ty"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   835
  and   f3::"('a::pt_name) f3_ty"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   836
  assumes f: "finite ((supp (f1,f2,f3))::name set)"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   837
  and     c: "\<exists>(a::name). a\<sharp>f3 \<and> (\<forall>(y::'a::pt_name). a\<sharp>f3 a y)"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   838
  and     a: "b\<sharp>(f1,f2,f3)"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   839
  shows "rfun f1 f2 f3 (Lam [b].t) = f3 b (rfun f1 f2 f3 t)"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   840
proof -
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   841
  have "\<exists>(a::name). a\<sharp>(b,t)"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   842
    by (rule at_exists_fresh[OF at_name_inst], simp add: supp_prod fs_name1)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   843
  then obtain a::"name" where a1: "a\<sharp>b" and a2: "a\<sharp>t" by (force simp add: fresh_prod)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   844
  have "rfun f1 f2 f3 (Lam [b].t) = rfun f1 f2 f3 (Lam [b].(([(a,b)])\<bullet>([(a,b)]\<bullet>t)))"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   845
    by (simp add: pt_swap_bij[OF pt_name_inst, OF at_name_inst])
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   846
  also have "\<dots> = f3 b (rfun f1 f2 f3 (([(a,b)])\<bullet>([(a,b)]\<bullet>t)))" 
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   847
  proof(rule rfun_Lam_aux2[OF f, OF c])
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   848
    have "b\<sharp>([(a,b)]\<bullet>t)" using a1 a2
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   849
      by (simp add: pt_fresh_left[OF pt_name_inst, OF at_name_inst] at_calc[OF at_name_inst] 
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   850
        at_fresh[OF at_name_inst])
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   851
    thus "b\<sharp>(a,[(a,b)]\<bullet>t,f1,f2,f3)" using a a1 by (force simp add: fresh_prod at_fresh[OF at_name_inst])
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   852
  qed
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   853
  also have "\<dots> = f3 b (rfun f1 f2 f3 t)" by (simp add: pt_swap_bij[OF pt_name_inst, OF at_name_inst])
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   854
  finally show ?thesis .
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   855
qed
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   856
  
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   857
lemma rec_unique:
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   858
  fixes fun::"lam \<Rightarrow> ('a::pt_name)"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   859
  and   f1::"('a::pt_name) f1_ty"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   860
  and   f2::"('a::pt_name) f2_ty"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   861
  and   f3::"('a::pt_name) f3_ty"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   862
  assumes f: "finite ((supp (f1,f2,f3))::name set)"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   863
  and     c: "\<exists>(a::name). a\<sharp>f3 \<and> (\<forall>(y::'a::pt_name). a\<sharp>f3 a y)"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   864
  and     a1: "\<forall>c. fun (Var c) = f1 c" 
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   865
  and     a2: "\<forall>t1 t2. fun (App t1 t2) = f2 (fun t1) (fun t2)" 
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   866
  and     a3: "\<forall>a t. a\<sharp>(f1,f2,f3) \<longrightarrow> fun (Lam [a].t) = f3 a (fun t)"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   867
  shows "fun t = rfun f1 f2 f3 t"
18659
2ff0ae57431d changes to make use of the new induction principle proved by
urbanc
parents: 18363
diff changeset
   868
apply (rule lam.induct'[of "\<lambda>_. ((supp (f1,f2,f3))::name set)" "\<lambda>_ t. fun t = rfun f1 f2 f3 t"])
2ff0ae57431d changes to make use of the new induction principle proved by
urbanc
parents: 18363
diff changeset
   869
apply(fold fresh_def)
18106
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   870
(* finite support *)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   871
apply(rule f)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   872
(* VAR *)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   873
apply(simp add: a1 rfun_Var[OF f, OF c, symmetric])
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   874
(* APP *)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   875
apply(simp add: a2 rfun_App[OF f, OF c, symmetric])
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   876
(* LAM *)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   877
apply(simp add: a3 rfun_Lam[OF f, OF c, symmetric])
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   878
done
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   879
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   880
lemma rec_function:
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   881
  fixes f1::"('a::pt_name) f1_ty"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   882
  and   f2::"('a::pt_name) f2_ty"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   883
  and   f3::"('a::pt_name) f3_ty"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   884
  assumes f: "finite ((supp (f1,f2,f3))::name set)"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   885
  and     c: "\<exists>(a::name). a\<sharp>f3 \<and> (\<forall>(y::'a::pt_name). a\<sharp>f3 a y)"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   886
  shows "(\<exists>!(fun::lam \<Rightarrow> ('a::pt_name)).
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   887
              (\<forall>c.     fun (Var c)     = f1 c) \<and> 
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   888
              (\<forall>t1 t2. fun (App t1 t2) = f2 (fun t1) (fun t2)) \<and> 
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   889
              (\<forall>a t.   a\<sharp>(f1,f2,f3) \<longrightarrow> fun (Lam [a].t) = f3 a (fun t)))"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   890
apply(rule_tac a="\<lambda>t. rfun f1 f2 f3 t" in ex1I)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   891
(* existence *)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   892
apply(simp add: rfun_Var[OF f, OF c])
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   893
apply(simp add: rfun_App[OF f, OF c])
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   894
apply(simp add: rfun_Lam[OF f, OF c])
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   895
(* uniqueness *)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   896
apply(auto simp add: expand_fun_eq)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   897
apply(rule rec_unique[OF f, OF c])
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   898
apply(force)+
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   899
done
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   900
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   901
(* "real" recursion *)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   902
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   903
types 'a f1_ty' = "name\<Rightarrow>('a::pt_name)"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   904
      'a f2_ty' = "lam\<Rightarrow>lam\<Rightarrow>'a\<Rightarrow>'a\<Rightarrow>('a::pt_name)"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   905
      'a f3_ty' = "lam\<Rightarrow>name\<Rightarrow>'a\<Rightarrow>('a::pt_name)"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   906
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   907
constdefs
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   908
  rfun_gen' :: "'a f1_ty' \<Rightarrow> 'a f2_ty' \<Rightarrow> 'a f3_ty' \<Rightarrow> lam \<Rightarrow> (lam\<times>'a::pt_name)" 
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   909
  "rfun_gen' f1 f2 f3 t \<equiv> (rfun 
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   910
                             (\<lambda>(a::name). (Var a,f1 a)) 
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   911
                             (\<lambda>r1 r2. (App (fst r1) (fst r2), f2 (fst r1) (fst r2) (snd r1) (snd r2))) 
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   912
                             (\<lambda>(a::name) r. (Lam [a].(fst r),f3 (fst r) a (snd r)))
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   913
                           t)"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   914
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   915
  rfun_gen :: "'a f1_ty' \<Rightarrow> 'a f2_ty' \<Rightarrow> 'a f3_ty' \<Rightarrow> lam \<Rightarrow> 'a::pt_name" 
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   916
  "rfun_gen f1 f2 f3 t \<equiv> snd(rfun_gen' f1 f2 f3 t)"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   917
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   918
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   919
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   920
lemma f1'_supports:
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   921
  fixes f1::"('a::pt_name) f1_ty'"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   922
  shows "((supp f1)::name set) supports (\<lambda>(a::name). (Var a,f1 a))"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   923
  by (supports_simp)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   924
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   925
lemma f2'_supports:
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   926
  fixes f2::"('a::pt_name) f2_ty'"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   927
  shows "((supp f2)::name set) supports 
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   928
                         (\<lambda>r1 r2. (App (fst r1) (fst r2), f2 (fst r1) (fst r2) (snd r1) (snd r2)))"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   929
  by (supports_simp add: perm_fst perm_snd)  
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   930
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   931
lemma f3'_supports:
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   932
  fixes f3::"('a::pt_name) f3_ty'"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   933
  shows "((supp f3)::name set) supports (\<lambda>(a::name) r. (Lam [a].(fst r),f3 (fst r) a (snd r)))"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   934
by (supports_simp add: perm_fst perm_snd)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   935
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   936
lemma fcb': 
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   937
  fixes f3::"('a::pt_name) f3_ty'"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   938
  assumes f: "finite ((supp (f1,f2,f3))::name set)"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   939
  and     c: "\<exists>(a::name). a\<sharp>f3 \<and> (\<forall>(y::'a::pt_name) t. a\<sharp>f3 t a y)"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   940
  shows  "\<exists>a.  a \<sharp> (\<lambda>a r. (Lam [a].fst r, f3 (fst r) a (snd r))) \<and>
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   941
                (\<forall>y.  a \<sharp> (Lam [a].fst y, f3 (fst y) a (snd y)))"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   942
using c f
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   943
apply(auto)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   944
apply(rule_tac x="a" in exI)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   945
apply(auto simp add: abs_fresh fresh_prod)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   946
apply(rule supports_fresh)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   947
apply(rule f3'_supports)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   948
apply(simp add: supp_prod)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   949
apply(simp add: fresh_def)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   950
done
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   951
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   952
lemma fsupp':
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   953
  fixes f1::"('a::pt_name) f1_ty'"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   954
  and   f2::"('a::pt_name) f2_ty'"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   955
  and   f3::"('a::pt_name) f3_ty'"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   956
  assumes f: "finite ((supp (f1,f2,f3))::name set)"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   957
  shows "finite((supp
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   958
          (\<lambda>a. (Var a, f1 a),
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   959
           \<lambda>r1 r2.
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   960
              (App (fst r1) (fst r2),
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   961
               f2 (fst r1) (fst r2) (snd r1) (snd r2)),
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   962
           \<lambda>a r. (Lam [a].fst r, f3 (fst r) a (snd r))))::name set)"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   963
using f
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   964
apply(auto simp add: supp_prod)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   965
apply(rule supports_finite)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   966
apply(rule f1'_supports)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   967
apply(assumption)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   968
apply(rule supports_finite)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   969
apply(rule f2'_supports)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   970
apply(assumption)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   971
apply(rule supports_finite)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   972
apply(rule f3'_supports)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   973
apply(assumption)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   974
done
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   975
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   976
lemma rfun_gen'_fst:
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   977
  fixes f1::"('a::pt_name) f1_ty'"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   978
  and   f2::"('a::pt_name) f2_ty'"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   979
  and   f3::"('a::pt_name) f3_ty'"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   980
  assumes f: "finite ((supp (f1,f2,f3))::name set)" 
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   981
  and     c: "(\<exists>(a::name). a\<sharp>f3 \<and> (\<forall>(y::'a::pt_name) t. a\<sharp>f3 t a y))"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   982
  shows "fst (rfun_gen' f1 f2 f3 t) = t"
18659
2ff0ae57431d changes to make use of the new induction principle proved by
urbanc
parents: 18363
diff changeset
   983
apply(rule lam.induct'[of "\<lambda>_. ((supp (f1,f2,f3))::name set)" "\<lambda>_ t. fst (rfun_gen' f1 f2 f3 t) = t"])
2ff0ae57431d changes to make use of the new induction principle proved by
urbanc
parents: 18363
diff changeset
   984
apply(fold fresh_def)
18106
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   985
apply(simp add: f)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   986
apply(unfold rfun_gen'_def)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   987
apply(simp only: rfun_Var[OF fsupp'[OF f],OF fcb'[OF f, OF c]])
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   988
apply(simp)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   989
apply(simp only: rfun_App[OF fsupp'[OF f],OF fcb'[OF f, OF c]])
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   990
apply(simp)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   991
apply(auto)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   992
apply(rule trans)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   993
apply(rule_tac f="fst" in arg_cong)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   994
apply(rule rfun_Lam[OF fsupp'[OF f],OF fcb'[OF f, OF c]])
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   995
apply(auto simp add: fresh_prod)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   996
apply(rule supports_fresh)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   997
apply(rule f1'_supports)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   998
apply(subgoal_tac "finite ((supp (f1,f2,f3))::name set)")
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   999
apply(simp add: supp_prod)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1000
apply(rule f)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1001
apply(simp add: fresh_def)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1002
apply(rule supports_fresh)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1003
apply(rule f2'_supports)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1004
apply(subgoal_tac "finite ((supp (f1,f2,f3))::name set)")
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1005
apply(simp add: supp_prod)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1006
apply(rule f)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1007
apply(simp add: fresh_def)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1008
apply(rule supports_fresh)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1009
apply(rule f3'_supports)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1010
apply(subgoal_tac "finite ((supp (f1,f2,f3))::name set)")
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1011
apply(simp add: supp_prod)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1012
apply(rule f)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1013
apply(simp add: fresh_def)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1014
done
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1015
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1016
lemma rfun_gen'_Var:
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1017
  fixes f1::"('a::pt_name) f1_ty'"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1018
  and   f2::"('a::pt_name) f2_ty'"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1019
  and   f3::"('a::pt_name) f3_ty'"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1020
  assumes f: "finite ((supp (f1,f2,f3))::name set)"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1021
  and     c: "\<exists>(a::name). a\<sharp>f3 \<and> (\<forall>(y::'a::pt_name) t. a\<sharp>f3 t a y)"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1022
  shows "rfun_gen' f1 f2 f3 (Var c) = (Var c, f1 c)"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1023
apply(simp add: rfun_gen'_def)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1024
apply(simp add: rfun_Var[OF fsupp'[OF f],OF fcb'[OF f, OF c]])
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1025
done
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1026
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1027
lemma rfun_gen'_App:
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1028
  fixes f1::"('a::pt_name) f1_ty'"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1029
  and   f2::"('a::pt_name) f2_ty'"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1030
  and   f3::"('a::pt_name) f3_ty'"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1031
  assumes f: "finite ((supp (f1,f2,f3))::name set)"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1032
  and     c: "\<exists>(a::name). a\<sharp>f3 \<and> (\<forall>(y::'a::pt_name) t. a\<sharp>f3 t a y)"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1033
  shows "rfun_gen' f1 f2 f3 (App t1 t2) = 
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1034
                (App t1 t2, f2 t1 t2 (rfun_gen f1 f2 f3 t1) (rfun_gen f1 f2 f3 t2))"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1035
apply(simp add: rfun_gen'_def)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1036
apply(rule trans)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1037
apply(rule rfun_App[OF fsupp'[OF f],OF fcb'[OF f, OF c]])
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1038
apply(fold rfun_gen'_def)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1039
apply(simp_all add: rfun_gen'_fst[OF f, OF c])
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1040
apply(simp_all add: rfun_gen_def)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1041
done
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1042
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1043
lemma rfun_gen'_Lam:
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1044
  fixes f1::"('a::pt_name) f1_ty'"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1045
  and   f2::"('a::pt_name) f2_ty'"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1046
  and   f3::"('a::pt_name) f3_ty'"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1047
  assumes f: "finite ((supp (f1,f2,f3))::name set)"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1048
  and     c: "\<exists>(a::name). a\<sharp>f3 \<and> (\<forall>(y::'a::pt_name) t. a\<sharp>f3 t a y)"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1049
  and     a: "b\<sharp>(f1,f2,f3)"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1050
  shows "rfun_gen' f1 f2 f3 (Lam [b].t) = (Lam [b].t, f3 t b (rfun_gen f1 f2 f3 t))"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1051
using a f
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1052
apply(simp add: rfun_gen'_def)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1053
apply(rule trans)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1054
apply(rule rfun_Lam[OF fsupp'[OF f],OF fcb'[OF f, OF c]])
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1055
apply(auto simp add: fresh_prod)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1056
apply(rule supports_fresh)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1057
apply(rule f1'_supports)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1058
apply(simp add: supp_prod)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1059
apply(simp add: fresh_def)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1060
apply(rule supports_fresh)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1061
apply(rule f2'_supports)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1062
apply(simp add: supp_prod)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1063
apply(simp add: fresh_def)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1064
apply(rule supports_fresh)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1065
apply(rule f3'_supports)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1066
apply(simp add: supp_prod)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1067
apply(simp add: fresh_def)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1068
apply(fold rfun_gen'_def)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1069
apply(simp_all add: rfun_gen'_fst[OF f, OF c])
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1070
apply(simp_all add: rfun_gen_def)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1071
done
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1072
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1073
lemma rfun_gen_Var:
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1074
  fixes f1::"('a::pt_name) f1_ty'"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1075
  and   f2::"('a::pt_name) f2_ty'"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1076
  and   f3::"('a::pt_name) f3_ty'"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1077
  assumes f: "finite ((supp (f1,f2,f3))::name set)"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1078
  and     c: "\<exists>(a::name). a\<sharp>f3 \<and> (\<forall>(y::'a::pt_name) t. a\<sharp>f3 t a y)"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1079
  shows "rfun_gen f1 f2 f3 (Var c) = f1 c"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1080
apply(unfold rfun_gen_def)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1081
apply(simp add: rfun_gen'_Var[OF f, OF c])
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1082
done
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1083
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1084
lemma rfun_gen_App:
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1085
  fixes f1::"('a::pt_name) f1_ty'"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1086
  and   f2::"('a::pt_name) f2_ty'"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1087
  and   f3::"('a::pt_name) f3_ty'"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1088
  assumes f: "finite ((supp (f1,f2,f3))::name set)"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1089
  and     c: "\<exists>(a::name). a\<sharp>f3 \<and> (\<forall>(y::'a::pt_name) t. a\<sharp>f3 t a y)"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1090
  shows "rfun_gen f1 f2 f3 (App t1 t2) = f2 t1 t2 (rfun_gen f1 f2 f3 t1) (rfun_gen f1 f2 f3 t2)"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1091
apply(unfold rfun_gen_def)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1092
apply(simp add: rfun_gen'_App[OF f, OF c])
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1093
apply(simp add: rfun_gen_def)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1094
done
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1095
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1096
lemma rfun_gen_Lam:
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1097
  fixes f1::"('a::pt_name) f1_ty'"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1098
  and   f2::"('a::pt_name) f2_ty'"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1099
  and   f3::"('a::pt_name) f3_ty'"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1100
  assumes f: "finite ((supp (f1,f2,f3))::name set)"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1101
  and     c: "\<exists>(a::name). a\<sharp>f3 \<and> (\<forall>(y::'a::pt_name) t. a\<sharp>f3 t a y)"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1102
  and     a: "b\<sharp>(f1,f2,f3)"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1103
  shows "rfun_gen f1 f2 f3 (Lam [b].t) = f3 t b (rfun_gen f1 f2 f3 t)"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1104
using a
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1105
apply(unfold rfun_gen_def)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1106
apply(simp add: rfun_gen'_Lam[OF f, OF c])
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1107
apply(simp add: rfun_gen_def)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1108
done
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1109
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1110
constdefs 
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1111
  depth_Var :: "name \<Rightarrow> nat"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1112
  "depth_Var \<equiv> \<lambda>(a::name). 1"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1113
  
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1114
  depth_App :: "nat \<Rightarrow> nat \<Rightarrow> nat"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1115
  "depth_App \<equiv> \<lambda>n1 n2. (max n1 n2)+1"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1116
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1117
  depth_Lam :: "name \<Rightarrow> nat \<Rightarrow> nat"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1118
  "depth_Lam \<equiv> \<lambda>(a::name) n. n+1"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1119
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1120
  depth_lam :: "lam \<Rightarrow> nat"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1121
  "depth_lam \<equiv> rfun depth_Var depth_App depth_Lam"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1122
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1123
lemma supp_depth_Var:
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1124
  shows "((supp depth_Var)::name set)={}"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1125
  apply(simp add: depth_Var_def)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1126
  apply(simp add: supp_def)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1127
  apply(simp add: perm_fun_def)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1128
  apply(simp add: perm_nat_def)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1129
  done
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1130
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1131
lemma supp_depth_App:
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1132
  shows "((supp depth_App)::name set)={}"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1133
  apply(simp add: depth_App_def)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1134
  apply(simp add: supp_def)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1135
  apply(simp add: perm_fun_def)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1136
  apply(simp add: perm_nat_def)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1137
  done
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1138
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1139
lemma supp_depth_Lam:
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1140
  shows "((supp depth_Lam)::name set)={}"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1141
  apply(simp add: depth_Lam_def)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1142
  apply(simp add: supp_def)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1143
  apply(simp add: perm_fun_def)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1144
  apply(simp add: perm_nat_def)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1145
  done
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1146
 
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1147
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1148
lemma fin_supp_depth:
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1149
  shows "finite ((supp (depth_Var,depth_App,depth_Lam))::name set)"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1150
  using supp_depth_Var supp_depth_Lam supp_depth_App
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1151
by (simp add: supp_prod)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1152
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1153
lemma fresh_depth_Lam:
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1154
  shows "\<exists>(a::name). a\<sharp>depth_Lam \<and> (\<forall>n. a\<sharp>depth_Lam a n)"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1155
apply(rule exI)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1156
apply(rule conjI)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1157
apply(simp add: fresh_def supp_depth_Lam)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1158
apply(auto simp add: depth_Lam_def)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1159
apply(unfold fresh_def)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1160
apply(simp add: supp_def)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1161
apply(simp add: perm_nat_def)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1162
done
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1163
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1164
lemma depth_Var:
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1165
  shows "depth_lam (Var c) = 1"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1166
apply(simp add: depth_lam_def)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1167
apply(simp add: rfun_Var[OF fin_supp_depth, OF fresh_depth_Lam])
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1168
apply(simp add: depth_Var_def)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1169
done
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1170
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1171
lemma depth_App:
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1172
  shows "depth_lam (App t1 t2) = (max (depth_lam t1) (depth_lam t2))+1"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1173
apply(simp add: depth_lam_def)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1174
apply(simp add: rfun_App[OF fin_supp_depth, OF fresh_depth_Lam])
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1175
apply(simp add: depth_App_def)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1176
done
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1177
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1178
lemma depth_Lam:
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1179
  shows "depth_lam (Lam [a].t) = (depth_lam t)+1"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1180
apply(simp add: depth_lam_def)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1181
apply(rule trans)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1182
apply(rule rfun_Lam[OF fin_supp_depth, OF fresh_depth_Lam])
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1183
apply(simp add: fresh_def supp_prod supp_depth_Var supp_depth_App supp_depth_Lam)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1184
apply(simp add: depth_Lam_def)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1185
done
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1186
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1187
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1188
(* substitution *)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1189
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1190
constdefs 
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1191
  subst_Var :: "name \<Rightarrow>lam \<Rightarrow> name \<Rightarrow> lam"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1192
  "subst_Var b t \<equiv> \<lambda>a. (if a=b then t else (Var a))"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1193
  
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1194
  subst_App :: "name \<Rightarrow> lam \<Rightarrow> lam \<Rightarrow> lam \<Rightarrow> lam"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1195
  "subst_App b t \<equiv> \<lambda>r1 r2. App r1 r2"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1196
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1197
  subst_Lam :: "name \<Rightarrow> lam \<Rightarrow> name \<Rightarrow> lam \<Rightarrow> lam"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1198
  "subst_Lam b t \<equiv> \<lambda>a r. Lam [a].r"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1199
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1200
  subst_lam :: "name \<Rightarrow> lam \<Rightarrow> lam \<Rightarrow> lam"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1201
  "subst_lam b t \<equiv> rfun (subst_Var b t) (subst_App b t) (subst_Lam b t)"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1202
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1203
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1204
lemma supports_subst_Var:
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1205
  shows "((supp (b,t))::name set) supports (subst_Var b t)"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1206
apply(supports_simp add: subst_Var_def)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1207
apply(rule impI)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1208
apply(drule pt_bij1[OF pt_name_inst, OF at_name_inst])
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1209
apply(simp add: pt_fresh_fresh[OF pt_name_inst, OF at_name_inst])
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1210
done
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1211
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1212
lemma supports_subst_App:
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1213
  shows "((supp (b,t))::name set) supports subst_App b t"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1214
by (supports_simp add: subst_App_def)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1215
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1216
lemma supports_subst_Lam:
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1217
  shows "((supp (b,t))::name set) supports subst_Lam b t"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1218
  by (supports_simp add: subst_Lam_def)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1219
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1220
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1221
lemma fin_supp_subst:
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1222
  shows "finite ((supp (subst_Var b t,subst_App b t,subst_Lam b t))::name set)"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1223
apply(auto simp add: supp_prod)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1224
apply(rule supports_finite)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1225
apply(rule supports_subst_Var)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1226
apply(simp add: fs_name1)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1227
apply(rule supports_finite)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1228
apply(rule supports_subst_App)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1229
apply(simp add: fs_name1)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1230
apply(rule supports_finite)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1231
apply(rule supports_subst_Lam)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1232
apply(simp add: fs_name1)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1233
done
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1234
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1235
lemma fresh_subst_Lam:
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1236
  shows "\<exists>(a::name). a\<sharp>(subst_Lam b t)\<and> (\<forall>y. a\<sharp>(subst_Lam b t) a y)"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1237
apply(subgoal_tac "\<exists>(c::name). c\<sharp>(b,t)")
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1238
apply(auto)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1239
apply(rule_tac x="c" in exI)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1240
apply(auto)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1241
apply(rule supports_fresh)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1242
apply(rule supports_subst_Lam)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1243
apply(simp_all add: fresh_def[symmetric] fs_name1)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1244
apply(simp add: subst_Lam_def)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1245
apply(simp add: abs_fresh)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1246
apply(rule at_exists_fresh[OF at_name_inst])
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1247
apply(simp add: fs_name1)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1248
done
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1249
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1250
lemma subst_Var:
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1251
  shows "subst_lam b t (Var a) = (if a=b then t else (Var a))"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1252
apply(simp add: subst_lam_def)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1253
apply(auto simp add: rfun_Var[OF fin_supp_subst, OF fresh_subst_Lam])
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1254
apply(auto simp add: subst_Var_def)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1255
done
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1256
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1257
lemma subst_App:
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1258
  shows "subst_lam b t (App t1 t2) = App (subst_lam b t t1) (subst_lam b t t2)"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1259
apply(simp add: subst_lam_def)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1260
apply(auto simp add: rfun_App[OF fin_supp_subst, OF fresh_subst_Lam])
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1261
apply(auto simp add: subst_App_def)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1262
done
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1263
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1264
lemma subst_Lam:
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1265
  assumes a: "a\<sharp>(b,t)"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1266
  shows "subst_lam b t (Lam [a].t1) = Lam [a].(subst_lam b t t1)"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1267
using a
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1268
apply(simp add: subst_lam_def)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1269
apply(subgoal_tac "a\<sharp>(subst_Var b t,subst_App b t,subst_Lam b t)")
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1270
apply(auto simp add: rfun_Lam[OF fin_supp_subst, OF fresh_subst_Lam])
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1271
apply(simp (no_asm) add: subst_Lam_def)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1272
apply(auto simp add: fresh_prod)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1273
apply(rule supports_fresh)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1274
apply(rule supports_subst_Var)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1275
apply(simp_all add: fs_name1 fresh_def[symmetric] fresh_prod)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1276
apply(rule supports_fresh)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1277
apply(rule supports_subst_App)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1278
apply(simp_all add: fs_name1 fresh_def[symmetric] fresh_prod)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1279
apply(rule supports_fresh)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1280
apply(rule supports_subst_Lam)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1281
apply(simp_all add: fs_name1 fresh_def[symmetric] fresh_prod)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1282
done
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1283
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1284
lemma subst_Lam':
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1285
  assumes a: "a\<noteq>b"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1286
  and     b: "a\<sharp>t"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1287
  shows "subst_lam b t (Lam [a].t1) = Lam [a].(subst_lam b t t1)"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1288
apply(rule subst_Lam)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1289
apply(simp add: fresh_prod a b fresh_atm)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1290
done
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1291
18300
ca1ac9e81bc8 added one clause for substitution in the lambda-case and
urbanc
parents: 18298
diff changeset
  1292
lemma subst_Lam'':
ca1ac9e81bc8 added one clause for substitution in the lambda-case and
urbanc
parents: 18298
diff changeset
  1293
  assumes a: "a\<sharp>b"
ca1ac9e81bc8 added one clause for substitution in the lambda-case and
urbanc
parents: 18298
diff changeset
  1294
  and     b: "a\<sharp>t"
ca1ac9e81bc8 added one clause for substitution in the lambda-case and
urbanc
parents: 18298
diff changeset
  1295
  shows "subst_lam b t (Lam [a].t1) = Lam [a].(subst_lam b t t1)"
ca1ac9e81bc8 added one clause for substitution in the lambda-case and
urbanc
parents: 18298
diff changeset
  1296
apply(rule subst_Lam)
ca1ac9e81bc8 added one clause for substitution in the lambda-case and
urbanc
parents: 18298
diff changeset
  1297
apply(simp add: fresh_prod a b)
ca1ac9e81bc8 added one clause for substitution in the lambda-case and
urbanc
parents: 18298
diff changeset
  1298
done
ca1ac9e81bc8 added one clause for substitution in the lambda-case and
urbanc
parents: 18298
diff changeset
  1299
18106
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1300
consts
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1301
  subst_syn  :: "lam \<Rightarrow> name \<Rightarrow> lam \<Rightarrow> lam" ("_[_::=_]" [100,100,100] 900)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1302
translations 
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1303
  "t1[a::=t2]" \<rightleftharpoons> "subst_lam a t2 t1"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1304
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1305
declare subst_Var[simp]
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1306
declare subst_App[simp]
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1307
declare subst_Lam[simp]
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1308
declare subst_Lam'[simp]
18300
ca1ac9e81bc8 added one clause for substitution in the lambda-case and
urbanc
parents: 18298
diff changeset
  1309
declare subst_Lam''[simp]
18106
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1310
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1311
lemma subst_eqvt[simp]:
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1312
  fixes pi:: "name prm"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1313
  and   t1:: "lam"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1314
  and   t2:: "lam"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1315
  and   a :: "name"
18301
0c5c3b1a700e fixed the lemma where the new names generated by nominal_induct
urbanc
parents: 18300
diff changeset
  1316
  shows "pi\<bullet>(t1[b::=t2]) = (pi\<bullet>t1)[(pi\<bullet>b)::=(pi\<bullet>t2)]"
18659
2ff0ae57431d changes to make use of the new induction principle proved by
urbanc
parents: 18363
diff changeset
  1317
apply(nominal_induct t1 avoiding: b t2 rule: lam.induct)
18106
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1318
apply(auto simp add: perm_bij fresh_prod fresh_atm)
18659
2ff0ae57431d changes to make use of the new induction principle proved by
urbanc
parents: 18363
diff changeset
  1319
apply(subgoal_tac "(pi\<bullet>name)\<sharp>(pi\<bullet>b,pi\<bullet>t2)")(*A*)
2ff0ae57431d changes to make use of the new induction principle proved by
urbanc
parents: 18363
diff changeset
  1320
apply(simp)
2ff0ae57431d changes to make use of the new induction principle proved by
urbanc
parents: 18363
diff changeset
  1321
(*A*) 
18106
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1322
apply(simp add: perm_bij fresh_prod fresh_atm pt_fresh_bij[OF pt_name_inst, OF at_name_inst]) 
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1323
done
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1324
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1325
lemma subst_supp: "supp(t1[a::=t2])\<subseteq>(((supp(t1)-{a})\<union>supp(t2))::name set)"
18659
2ff0ae57431d changes to make use of the new induction principle proved by
urbanc
parents: 18363
diff changeset
  1326
apply(nominal_induct t1 avoiding: a t2 rule: lam.induct)
18106
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1327
apply(auto simp add: lam.supp supp_atm fresh_prod abs_supp)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1328
apply(blast)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1329
apply(blast)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1330
done
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1331
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1332
(* parallel substitution *)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1333
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1334
consts
18263
7f75925498da cleaned up all examples so that they work with the
urbanc
parents: 18106
diff changeset
  1335
  "domain" :: "(name\<times>lam) list \<Rightarrow> (name list)"
18106
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1336
primrec
18263
7f75925498da cleaned up all examples so that they work with the
urbanc
parents: 18106
diff changeset
  1337
  "domain []    = []"
7f75925498da cleaned up all examples so that they work with the
urbanc
parents: 18106
diff changeset
  1338
  "domain (x#\<theta>) = (fst x)#(domain \<theta>)" 
18106
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1339
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1340
consts
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1341
  "apply_sss"  :: "(name\<times>lam) list \<Rightarrow> name \<Rightarrow> lam" (" _ < _ >" [80,80] 80)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1342
primrec  
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1343
"(x#\<theta>)<a>  = (if (a = fst x) then (snd x) else \<theta><a>)" 
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1344
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1345
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1346
lemma apply_sss_eqvt[rule_format]:
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1347
  fixes pi::"name prm"
18263
7f75925498da cleaned up all examples so that they work with the
urbanc
parents: 18106
diff changeset
  1348
  shows "a\<in>set (domain \<theta>) \<longrightarrow> pi\<bullet>(\<theta><a>) = (pi\<bullet>\<theta>)<pi\<bullet>a>"
18106
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1349
apply(induct_tac \<theta>)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1350
apply(auto)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1351
apply(simp add: pt_bij[OF pt_name_inst, OF at_name_inst])
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1352
done
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1353
18263
7f75925498da cleaned up all examples so that they work with the
urbanc
parents: 18106
diff changeset
  1354
lemma domain_eqvt[rule_format]:
18106
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1355
  fixes pi::"name prm"
18263
7f75925498da cleaned up all examples so that they work with the
urbanc
parents: 18106
diff changeset
  1356
  shows "((pi\<bullet>a)\<in>set (domain \<theta>)) =  (a\<in>set (domain ((rev pi)\<bullet>\<theta>)))"
18106
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1357
apply(induct_tac \<theta>)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1358
apply(auto)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1359
apply(simp_all add: pt_rev_pi[OF pt_name_inst, OF at_name_inst])
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1360
apply(simp_all add: pt_pi_rev[OF pt_name_inst, OF at_name_inst])
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1361
done
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1362
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1363
constdefs 
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1364
  psubst_Var :: "(name\<times>lam) list \<Rightarrow> name \<Rightarrow> lam"
18263
7f75925498da cleaned up all examples so that they work with the
urbanc
parents: 18106
diff changeset
  1365
  "psubst_Var \<theta> \<equiv> \<lambda>a. (if a\<in>set (domain \<theta>) then \<theta><a> else (Var a))"
18106
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1366
  
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1367
  psubst_App :: "(name\<times>lam) list \<Rightarrow> lam \<Rightarrow> lam \<Rightarrow> lam"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1368
  "psubst_App \<theta> \<equiv> \<lambda>r1 r2. App r1 r2"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1369
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1370
  psubst_Lam :: "(name\<times>lam) list \<Rightarrow> name \<Rightarrow> lam \<Rightarrow> lam"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1371
  "psubst_Lam \<theta> \<equiv> \<lambda>a r. Lam [a].r"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1372
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1373
  psubst_lam :: "(name\<times>lam) list \<Rightarrow> lam \<Rightarrow> lam"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1374
  "psubst_lam \<theta> \<equiv> rfun (psubst_Var \<theta>) (psubst_App \<theta>) (psubst_Lam \<theta>)"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1375
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1376
lemma supports_psubst_Var:
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1377
  shows "((supp \<theta>)::name set) supports (psubst_Var \<theta>)"
18263
7f75925498da cleaned up all examples so that they work with the
urbanc
parents: 18106
diff changeset
  1378
  by (supports_simp add: psubst_Var_def apply_sss_eqvt domain_eqvt)
18106
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1379
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1380
lemma supports_psubst_App:
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1381
  shows "((supp \<theta>)::name set) supports psubst_App \<theta>"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1382
  by (supports_simp add: psubst_App_def)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1383
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1384
lemma supports_psubst_Lam:
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1385
  shows "((supp \<theta>)::name set) supports psubst_Lam \<theta>"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1386
  by (supports_simp add: psubst_Lam_def)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1387
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1388
lemma fin_supp_psubst:
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1389
  shows "finite ((supp (psubst_Var \<theta>,psubst_App \<theta>,psubst_Lam \<theta>))::name set)"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1390
apply(auto simp add: supp_prod)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1391
apply(rule supports_finite)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1392
apply(rule supports_psubst_Var)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1393
apply(simp add: fs_name1)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1394
apply(rule supports_finite)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1395
apply(rule supports_psubst_App)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1396
apply(simp add: fs_name1)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1397
apply(rule supports_finite)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1398
apply(rule supports_psubst_Lam)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1399
apply(simp add: fs_name1)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1400
done
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1401
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1402
lemma fresh_psubst_Lam:
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1403
  shows "\<exists>(a::name). a\<sharp>(psubst_Lam \<theta>)\<and> (\<forall>y. a\<sharp>(psubst_Lam \<theta>) a y)"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1404
apply(subgoal_tac "\<exists>(c::name). c\<sharp>\<theta>")
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1405
apply(auto)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1406
apply(rule_tac x="c" in exI)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1407
apply(auto)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1408
apply(rule supports_fresh)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1409
apply(rule supports_psubst_Lam)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1410
apply(simp_all add: fresh_def[symmetric] fs_name1)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1411
apply(simp add: psubst_Lam_def)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1412
apply(simp add: abs_fresh)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1413
apply(rule at_exists_fresh[OF at_name_inst])
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1414
apply(simp add: fs_name1)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1415
done
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1416
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1417
lemma psubst_Var:
18263
7f75925498da cleaned up all examples so that they work with the
urbanc
parents: 18106
diff changeset
  1418
  shows "psubst_lam \<theta> (Var a) = (if a\<in>set (domain \<theta>) then \<theta><a> else (Var a))"
18106
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1419
apply(simp add: psubst_lam_def)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1420
apply(auto simp add: rfun_Var[OF fin_supp_psubst, OF fresh_psubst_Lam])
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1421
apply(auto simp add: psubst_Var_def)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1422
done
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1423
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1424
lemma psubst_App:
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1425
  shows "psubst_lam \<theta> (App t1 t2) = App (psubst_lam \<theta> t1) (psubst_lam \<theta> t2)"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1426
apply(simp add: psubst_lam_def)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1427
apply(auto simp add: rfun_App[OF fin_supp_psubst, OF fresh_psubst_Lam])
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1428
apply(auto simp add: psubst_App_def)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1429
done
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1430
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1431
lemma psubst_Lam:
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1432
  assumes a: "a\<sharp>\<theta>"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1433
  shows "psubst_lam \<theta> (Lam [a].t1) = Lam [a].(psubst_lam \<theta> t1)"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1434
using a
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1435
apply(simp add: psubst_lam_def)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1436
apply(subgoal_tac "a\<sharp>(psubst_Var \<theta>,psubst_App \<theta>,psubst_Lam \<theta>)")
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1437
apply(auto simp add: rfun_Lam[OF fin_supp_psubst, OF fresh_psubst_Lam])
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1438
apply(simp (no_asm) add: psubst_Lam_def)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1439
apply(auto simp add: fresh_prod)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1440
apply(rule supports_fresh)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1441
apply(rule supports_psubst_Var)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1442
apply(simp_all add: fs_name1 fresh_def[symmetric] fresh_prod)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1443
apply(rule supports_fresh)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1444
apply(rule supports_psubst_App)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1445
apply(simp_all add: fs_name1 fresh_def[symmetric] fresh_prod)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1446
apply(rule supports_fresh)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1447
apply(rule supports_psubst_Lam)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1448
apply(simp_all add: fs_name1 fresh_def[symmetric] fresh_prod)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1449
done
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1450
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1451
declare psubst_Var[simp]
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1452
declare psubst_App[simp]
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1453
declare psubst_Lam[simp]
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1454
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1455
consts
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1456
  psubst_syn  :: "lam \<Rightarrow> (name\<times>lam) list \<Rightarrow> lam" ("_[<_>]" [100,100] 900)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1457
translations 
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1458
  "t[<\<theta>>]" \<rightleftharpoons> "psubst_lam \<theta> t"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1459
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
  1460
end