src/HOL/Nominal/Examples/SN.thy
author urbanc
Mon, 07 Nov 2005 15:19:03 +0100
changeset 18106 836135c8acb2
child 18263 7f75925498da
permissions -rw-r--r--
Initial commit.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
18106
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
     1
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
     2
theory sn
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
     3
imports lam_substs  Accessible_Part
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
     4
begin
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
     5
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
     6
(* Strong normalisation according to the P&T book by Girard et al *)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
     7
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
     8
section {* Beta Reduction *}
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
     9
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
    10
lemma subst_rename[rule_format]: 
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
    11
  fixes  c  :: "name"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
    12
  and    a  :: "name"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
    13
  and    t1 :: "lam"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
    14
  and    t2 :: "lam"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
    15
  shows "c\<sharp>t1 \<longrightarrow> (t1[a::=t2] = ([(c,a)]\<bullet>t1)[c::=t2])"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
    16
apply(nominal_induct t1 rule: lam_induct)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
    17
apply(auto simp add: calc_atm fresh_atm fresh_prod abs_fresh)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
    18
done
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
    19
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
    20
lemma forget[rule_format]: 
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
    21
  shows "a\<sharp>t1 \<longrightarrow> t1[a::=t2] = t1"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
    22
apply (nominal_induct t1 rule: lam_induct)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
    23
apply(auto simp add: abs_fresh fresh_atm fresh_prod)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
    24
done
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
    25
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
    26
lemma fresh_fact[rule_format]: 
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
    27
  fixes   b :: "name"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
    28
  and    a  :: "name"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
    29
  and    t1 :: "lam"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
    30
  and    t2 :: "lam" 
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
    31
  shows "a\<sharp>t1\<longrightarrow>a\<sharp>t2\<longrightarrow>a\<sharp>(t1[b::=t2])"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
    32
apply(nominal_induct t1 rule: lam_induct)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
    33
apply(auto simp add: abs_fresh fresh_prod fresh_atm)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
    34
done
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
    35
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
    36
lemma subs_lemma:  
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
    37
  fixes x::"name"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
    38
  and   y::"name"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
    39
  and   L::"lam"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
    40
  and   M::"lam"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
    41
  and   N::"lam"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
    42
  shows "x\<noteq>y\<longrightarrow>x\<sharp>L\<longrightarrow>M[x::=N][y::=L] = M[y::=L][x::=N[y::=L]]"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
    43
apply(nominal_induct M rule: lam_induct)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
    44
apply(auto simp add: fresh_fact forget fresh_prod fresh_atm)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
    45
done
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
    46
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
    47
lemma id_subs: "t[x::=Var x] = t"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
    48
apply(nominal_induct t rule: lam_induct)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
    49
apply(simp_all add: fresh_atm)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
    50
done
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
    51
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
    52
consts
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
    53
  Beta :: "(lam\<times>lam) set"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
    54
syntax 
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
    55
  "_Beta"       :: "lam\<Rightarrow>lam\<Rightarrow>bool" (" _ \<longrightarrow>\<^isub>\<beta> _" [80,80] 80)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
    56
  "_Beta_star"  :: "lam\<Rightarrow>lam\<Rightarrow>bool" (" _ \<longrightarrow>\<^isub>\<beta>\<^sup>* _" [80,80] 80)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
    57
translations 
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
    58
  "t1 \<longrightarrow>\<^isub>\<beta> t2" \<rightleftharpoons> "(t1,t2) \<in> Beta"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
    59
  "t1 \<longrightarrow>\<^isub>\<beta>\<^sup>* t2" \<rightleftharpoons> "(t1,t2) \<in> Beta\<^sup>*"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
    60
inductive Beta
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
    61
  intros
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
    62
  b1[intro!]: "s1\<longrightarrow>\<^isub>\<beta>s2 \<Longrightarrow> (App s1 t)\<longrightarrow>\<^isub>\<beta>(App s2 t)"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
    63
  b2[intro!]: "s1\<longrightarrow>\<^isub>\<beta>s2 \<Longrightarrow> (App t s1)\<longrightarrow>\<^isub>\<beta>(App t s2)"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
    64
  b3[intro!]: "s1\<longrightarrow>\<^isub>\<beta>s2 \<Longrightarrow> (Lam [a].s1)\<longrightarrow>\<^isub>\<beta> (Lam [(a::name)].s2)"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
    65
  b4[intro!]: "(App (Lam [(a::name)].s1) s2)\<longrightarrow>\<^isub>\<beta>(s1[a::=s2])"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
    66
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
    67
lemma eqvt_beta: 
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
    68
  fixes pi :: "name prm"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
    69
  and   t  :: "lam"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
    70
  and   s  :: "lam"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
    71
  shows "t\<longrightarrow>\<^isub>\<beta>s \<Longrightarrow> (pi\<bullet>t)\<longrightarrow>\<^isub>\<beta>(pi\<bullet>s)"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
    72
  apply(erule Beta.induct)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
    73
  apply(auto)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
    74
  done
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
    75
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
    76
lemma beta_induct_aux[rule_format]:
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
    77
  fixes  P :: "lam \<Rightarrow> lam \<Rightarrow>'a::fs_name\<Rightarrow>bool"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
    78
  and    t :: "lam"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
    79
  and    s :: "lam"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
    80
  assumes a: "t\<longrightarrow>\<^isub>\<beta>s"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
    81
  and a1:    "\<And>x t s1 s2. 
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
    82
              s1\<longrightarrow>\<^isub>\<beta>s2 \<Longrightarrow> (\<forall>z. P s1 s2 z) \<Longrightarrow> P (App s1 t) (App s2 t) x"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
    83
  and a2:    "\<And>x t s1 s2. 
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
    84
              s1\<longrightarrow>\<^isub>\<beta>s2 \<Longrightarrow> (\<forall>z. P s1 s2 z) \<Longrightarrow> P (App t s1) (App t s2) x"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
    85
  and a3:    "\<And>x (a::name) s1 s2. 
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
    86
              a\<sharp>x \<Longrightarrow> s1\<longrightarrow>\<^isub>\<beta>s2 \<Longrightarrow> (\<forall>z. P s1 s2 z) \<Longrightarrow> P (Lam [a].s1) (Lam [a].s2) x"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
    87
  and a4:    "\<And>x (a::name) t1 s1. a\<sharp>(s1,x) \<Longrightarrow> P (App (Lam [a].t1) s1) (t1[a::=s1]) x"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
    88
  shows "\<forall>x (pi::name prm). P (pi\<bullet>t) (pi\<bullet>s) x"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
    89
using a
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
    90
proof (induct)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
    91
  case b1 thus ?case using a1 by (simp, blast intro: eqvt_beta)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
    92
next
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
    93
  case b2 thus ?case using a2 by (simp, blast intro: eqvt_beta)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
    94
next
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
    95
  case (b3 a s1 s2)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
    96
  assume j1: "s1 \<longrightarrow>\<^isub>\<beta> s2"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
    97
  assume j2: "\<forall>x (pi::name prm). P (pi\<bullet>s1) (pi\<bullet>s2) x"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
    98
  show ?case 
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
    99
  proof (simp, intro strip)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   100
    fix pi::"name prm" and x::"'a::fs_name"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   101
     have f: "\<exists>c::name. c\<sharp>(pi\<bullet>a,pi\<bullet>s1,pi\<bullet>s2,x)"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   102
      by (rule at_exists_fresh[OF at_name_inst], simp add: fs_name1)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   103
    then obtain c::"name" 
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   104
      where f1: "c\<noteq>(pi\<bullet>a)" and f2: "c\<sharp>x" and f3: "c\<sharp>(pi\<bullet>s1)" and f4: "c\<sharp>(pi\<bullet>s2)"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   105
      by (force simp add: fresh_prod fresh_atm)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   106
    have x: "P (Lam [c].(([(c,pi\<bullet>a)]@pi)\<bullet>s1)) (Lam [c].(([(c,pi\<bullet>a)]@pi)\<bullet>s2)) x"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   107
      using a3 f2 j1 j2 by (simp, blast intro: eqvt_beta)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   108
    have alpha1: "(Lam [c].([(c,pi\<bullet>a)]\<bullet>(pi\<bullet>s1))) = (Lam [(pi\<bullet>a)].(pi\<bullet>s1))" using f1 f3
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   109
      by (simp add: lam.inject alpha)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   110
    have alpha2: "(Lam [c].([(c,pi\<bullet>a)]\<bullet>(pi\<bullet>s2))) = (Lam [(pi\<bullet>a)].(pi\<bullet>s2))" using f1 f3
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   111
      by (simp add: lam.inject alpha)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   112
    show " P (Lam [(pi\<bullet>a)].(pi\<bullet>s1)) (Lam [(pi\<bullet>a)].(pi\<bullet>s2)) x"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   113
      using x alpha1 alpha2 by (simp only: pt_name2)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   114
  qed
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   115
next
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   116
  case (b4 a s1 s2)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   117
  show ?case
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   118
  proof (simp add: subst_eqvt, intro strip)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   119
    fix pi::"name prm" and x::"'a::fs_name" 
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   120
    have f: "\<exists>c::name. c\<sharp>(pi\<bullet>a,pi\<bullet>s1,pi\<bullet>s2,x)"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   121
      by (rule at_exists_fresh[OF at_name_inst], simp add: fs_name1)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   122
    then obtain c::"name" 
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   123
      where f1: "c\<noteq>(pi\<bullet>a)" and f2: "c\<sharp>(pi\<bullet>s2,x)" and f3: "c\<sharp>(pi\<bullet>s1)" and f4: "c\<sharp>(pi\<bullet>s2)"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   124
      by (force simp add: fresh_prod fresh_atm)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   125
    have x: "P (App (Lam [c].(([(c,pi\<bullet>a)]@pi)\<bullet>s1)) (pi\<bullet>s2)) ((([(c,pi\<bullet>a)]@pi)\<bullet>s1)[c::=(pi\<bullet>s2)]) x"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   126
      using a4 f2 by (blast intro!: eqvt_beta)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   127
    have alpha1: "(Lam [c].([(c,pi\<bullet>a)]\<bullet>(pi\<bullet>s1))) = (Lam [(pi\<bullet>a)].(pi\<bullet>s1))" using f1 f3
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   128
      by (simp add: lam.inject alpha)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   129
    have alpha2: "(([(c,pi\<bullet>a)]@pi)\<bullet>s1)[c::=(pi\<bullet>s2)] = (pi\<bullet>s1)[(pi\<bullet>a)::=(pi\<bullet>s2)]"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   130
      using f3 by (simp only: subst_rename[symmetric] pt_name2)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   131
    show "P (App (Lam [(pi\<bullet>a)].(pi\<bullet>s1)) (pi\<bullet>s2)) ((pi\<bullet>s1)[(pi\<bullet>a)::=(pi\<bullet>s2)]) x"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   132
      using x alpha1 alpha2 by (simp only: pt_name2)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   133
  qed
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   134
qed
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   135
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   136
lemma beta_induct[case_names b1 b2 b3 b4]:
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   137
  fixes  P :: "lam \<Rightarrow> lam \<Rightarrow>'a::fs_name\<Rightarrow>bool"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   138
  and    t :: "lam"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   139
  and    s :: "lam"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   140
  and    x :: "'a::fs_name"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   141
  assumes a: "t\<longrightarrow>\<^isub>\<beta>s"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   142
  and a1:    "\<And>x t s1 s2. 
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   143
              s1\<longrightarrow>\<^isub>\<beta>s2 \<Longrightarrow> (\<forall>z. P s1 s2 z) \<Longrightarrow> P (App s1 t) (App s2 t) x"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   144
  and a2:    "\<And>x t s1 s2. 
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   145
              s1\<longrightarrow>\<^isub>\<beta>s2 \<Longrightarrow> (\<forall>z. P s1 s2 z) \<Longrightarrow> P (App t s1) (App t s2) x"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   146
  and a3:    "\<And>x (a::name) s1 s2. 
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   147
              a\<sharp>x \<Longrightarrow> s1\<longrightarrow>\<^isub>\<beta>s2 \<Longrightarrow> (\<forall>z. P s1 s2 z) \<Longrightarrow> P (Lam [a].s1) (Lam [a].s2) x"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   148
  and a4:    "\<And>x (a::name) t1 s1. 
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   149
              a\<sharp>(s1,x) \<Longrightarrow> P (App (Lam [a].t1) s1) (t1[a::=s1]) x"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   150
  shows "P t s x"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   151
using a a1 a2 a3 a4
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   152
by (auto intro!: beta_induct_aux[of "t" "s" "P" "[]" "x", simplified])
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   153
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   154
lemma supp_beta: "t\<longrightarrow>\<^isub>\<beta> s\<Longrightarrow>(supp s)\<subseteq>((supp t)::name set)"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   155
apply(erule Beta.induct)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   156
apply(auto intro!: simp add: abs_supp lam.supp subst_supp)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   157
done
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   158
lemma beta_abs: "Lam [a].t\<longrightarrow>\<^isub>\<beta> t'\<Longrightarrow>\<exists>t''. t'=Lam [a].t'' \<and> t\<longrightarrow>\<^isub>\<beta> t''"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   159
apply(ind_cases "Lam [a].t  \<longrightarrow>\<^isub>\<beta> t'")
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   160
apply(auto simp add: lam.distinct lam.inject)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   161
apply(auto simp add: alpha)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   162
apply(rule_tac x="[(a,aa)]\<bullet>s2" in exI)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   163
apply(rule conjI)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   164
apply(rule sym)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   165
apply(rule pt_bij2[OF pt_name_inst, OF at_name_inst])
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   166
apply(simp)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   167
apply(rule pt_name3)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   168
apply(simp add: at_ds5[OF at_name_inst])
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   169
apply(rule conjI)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   170
apply(simp add: pt_fresh_left[OF pt_name_inst, OF at_name_inst] calc_atm)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   171
apply(force dest!: supp_beta simp add: fresh_def)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   172
apply(force intro!: eqvt_beta)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   173
done
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   174
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   175
lemma beta_subst[rule_format]: 
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   176
  assumes a: "M \<longrightarrow>\<^isub>\<beta> M'"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   177
  shows "M[x::=N]\<longrightarrow>\<^isub>\<beta> M'[x::=N]" 
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   178
using a
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   179
apply(nominal_induct M M' rule: beta_induct)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   180
apply(auto simp add: fresh_prod fresh_atm subs_lemma)
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
instance nat :: fs_name
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   184
apply(intro_classes)   
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   185
apply(simp_all add: supp_def perm_nat_def)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   186
done
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   187
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   188
datatype ty =
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   189
    TVar "string"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   190
  | TArr "ty" "ty" (infix "\<rightarrow>" 200)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   191
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   192
primrec
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   193
 "pi\<bullet>(TVar s) = TVar s"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   194
 "pi\<bullet>(\<tau> \<rightarrow> \<sigma>) = (\<tau> \<rightarrow> \<sigma>)"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   195
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   196
lemma perm_ty[simp]:
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   197
  fixes pi ::"name prm"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   198
  and   \<tau>  ::"ty"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   199
  shows "pi\<bullet>\<tau> = \<tau>"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   200
  by (cases \<tau>, simp_all)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   201
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   202
lemma fresh_ty:
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   203
  fixes a ::"name"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   204
  and   \<tau>  ::"ty"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   205
  shows "a\<sharp>\<tau>"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   206
  by (simp add: fresh_def supp_def)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   207
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   208
instance ty :: pt_name
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   209
apply(intro_classes)   
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   210
apply(simp_all)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   211
done
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   212
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   213
instance ty :: fs_name
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   214
apply(intro_classes)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   215
apply(simp add: supp_def)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   216
done
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   217
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   218
(* valid contexts *)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   219
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   220
consts
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   221
  "dom_ty" :: "(name\<times>ty) list \<Rightarrow> (name list)"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   222
primrec
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   223
  "dom_ty []    = []"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   224
  "dom_ty (x#\<Gamma>) = (fst x)#(dom_ty \<Gamma>)" 
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   225
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   226
consts
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   227
  ctxts :: "((name\<times>ty) list) set" 
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   228
  valid :: "(name\<times>ty) list \<Rightarrow> bool"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   229
translations
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   230
  "valid \<Gamma>" \<rightleftharpoons> "\<Gamma> \<in> ctxts"  
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   231
inductive ctxts
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   232
intros
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   233
v1[intro]: "valid []"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   234
v2[intro]: "\<lbrakk>valid \<Gamma>;a\<sharp>\<Gamma>\<rbrakk>\<Longrightarrow> valid ((a,\<sigma>)#\<Gamma>)"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   235
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   236
lemma valid_eqvt:
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   237
  fixes   pi:: "name prm"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   238
  assumes a: "valid \<Gamma>"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   239
  shows   "valid (pi\<bullet>\<Gamma>)"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   240
using a
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   241
apply(induct)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   242
apply(auto simp add: pt_fresh_bij[OF pt_name_inst, OF at_name_inst])
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   243
done
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   244
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   245
(* typing judgements *)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   246
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   247
lemma fresh_context[rule_format]: 
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   248
  fixes  \<Gamma> :: "(name\<times>ty)list"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   249
  and    a :: "name"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   250
  shows "a\<sharp>\<Gamma>\<longrightarrow>\<not>(\<exists>\<tau>::ty. (a,\<tau>)\<in>set \<Gamma>)"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   251
apply(induct_tac \<Gamma>)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   252
apply(auto simp add: fresh_prod fresh_list_cons fresh_atm)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   253
done
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   254
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   255
lemma valid_elim: 
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   256
  fixes  \<Gamma> :: "(name\<times>ty)list"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   257
  and    pi:: "name prm"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   258
  and    a :: "name"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   259
  and    \<tau> :: "ty"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   260
  shows "valid ((a,\<tau>)#\<Gamma>) \<Longrightarrow> valid \<Gamma> \<and> a\<sharp>\<Gamma>"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   261
apply(ind_cases "valid ((a,\<tau>)#\<Gamma>)", simp)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   262
done
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   263
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   264
lemma valid_unicity[rule_format]: 
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   265
  shows "valid \<Gamma>\<longrightarrow>(c,\<sigma>)\<in>set \<Gamma>\<longrightarrow>(c,\<tau>)\<in>set \<Gamma>\<longrightarrow>\<sigma>=\<tau>" 
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   266
apply(induct_tac \<Gamma>)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   267
apply(auto dest!: valid_elim fresh_context)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   268
done
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   269
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   270
consts
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   271
  typing :: "(((name\<times>ty) list)\<times>lam\<times>ty) set" 
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   272
syntax
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   273
  "_typing_judge" :: "(name\<times>ty) list\<Rightarrow>lam\<Rightarrow>ty\<Rightarrow>bool" (" _ \<turnstile> _ : _ " [80,80,80] 80) 
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   274
translations
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   275
  "\<Gamma> \<turnstile> t : \<tau>" \<rightleftharpoons> "(\<Gamma>,t,\<tau>) \<in> typing"  
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   276
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   277
inductive typing
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   278
intros
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   279
t1[intro]: "\<lbrakk>valid \<Gamma>; (a,\<tau>)\<in>set \<Gamma>\<rbrakk>\<Longrightarrow> \<Gamma> \<turnstile> Var a : \<tau>"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   280
t2[intro]: "\<lbrakk>\<Gamma> \<turnstile> t1 : \<tau>\<rightarrow>\<sigma>; \<Gamma> \<turnstile> t2 : \<tau>\<rbrakk>\<Longrightarrow> \<Gamma> \<turnstile> App t1 t2 : \<sigma>"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   281
t3[intro]: "\<lbrakk>a\<sharp>\<Gamma>;((a,\<tau>)#\<Gamma>) \<turnstile> t : \<sigma>\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> Lam [a].t : \<tau>\<rightarrow>\<sigma>"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   282
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   283
lemma typing_eqvt: 
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   284
  fixes  \<Gamma> :: "(name\<times>ty) list"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   285
  and    t :: "lam"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   286
  and    \<tau> :: "ty"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   287
  and    pi:: "name prm"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   288
  assumes a: "\<Gamma> \<turnstile> t : \<tau>"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   289
  shows "(pi\<bullet>\<Gamma>) \<turnstile> (pi\<bullet>t) : \<tau>"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   290
using a
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   291
proof (induct)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   292
  case (t1 \<Gamma> \<tau> a)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   293
  have "valid (pi\<bullet>\<Gamma>)" by (rule valid_eqvt)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   294
  moreover
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   295
  have "(pi\<bullet>(a,\<tau>))\<in>((pi::name prm)\<bullet>set \<Gamma>)" by (rule pt_set_bij2[OF pt_name_inst, OF at_name_inst])
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   296
  ultimately show "(pi\<bullet>\<Gamma>) \<turnstile> (pi\<bullet>Var a) : \<tau>"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   297
    using typing.intros by (auto simp add: pt_list_set_pi[OF pt_name_inst])
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   298
next 
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   299
  case (t3 \<Gamma> \<sigma> \<tau> a t)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   300
  moreover have "(pi\<bullet>a)\<sharp>(pi\<bullet>\<Gamma>)" by (rule pt_fresh_bij1[OF pt_name_inst, OF at_name_inst])
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   301
  ultimately show "(pi\<bullet>\<Gamma>) \<turnstile> (pi\<bullet>Lam [a].t) : \<tau>\<rightarrow>\<sigma>" 
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   302
    using typing.intros by (force)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   303
qed (auto)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   304
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   305
lemma typing_induct_aux[rule_format]:
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   306
  fixes  P :: "(name\<times>ty) list \<Rightarrow> lam \<Rightarrow> ty \<Rightarrow>'a::fs_name\<Rightarrow>bool"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   307
  and    \<Gamma> :: "(name\<times>ty) list"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   308
  and    t :: "lam"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   309
  and    \<tau> :: "ty"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   310
  assumes a: "\<Gamma> \<turnstile> t : \<tau>"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   311
  and a1:    "\<And>x \<Gamma> (a::name) \<tau>. valid \<Gamma> \<Longrightarrow> (a,\<tau>) \<in> set \<Gamma> \<Longrightarrow> P \<Gamma> (Var a) \<tau> x"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   312
  and a2:    "\<And>x \<Gamma> \<tau> \<sigma> t1 t2. 
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   313
              \<Gamma> \<turnstile> t1 : \<tau>\<rightarrow>\<sigma> \<Longrightarrow> (\<And>z. P \<Gamma> t1 (\<tau>\<rightarrow>\<sigma>) z) \<Longrightarrow> \<Gamma> \<turnstile> t2 : \<tau> \<Longrightarrow> (\<And>z. P \<Gamma> t2 \<tau> z)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   314
              \<Longrightarrow> P \<Gamma> (App t1 t2) \<sigma> x"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   315
  and a3:    "\<And>x (a::name) \<Gamma> \<tau> \<sigma> t. 
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   316
              a\<sharp>x \<Longrightarrow> a\<sharp>\<Gamma> \<Longrightarrow> ((a,\<tau>) # \<Gamma>) \<turnstile> t : \<sigma> \<Longrightarrow> (\<forall>z. P ((a,\<tau>)#\<Gamma>) t \<sigma> z)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   317
              \<Longrightarrow> P \<Gamma> (Lam [a].t) (\<tau>\<rightarrow>\<sigma>) x"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   318
  shows "\<forall>(pi::name prm) (x::'a::fs_name). P (pi\<bullet>\<Gamma>) (pi\<bullet>t) \<tau> x"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   319
using a
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   320
proof (induct)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   321
  case (t1 \<Gamma> \<tau> a)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   322
  assume j1: "valid \<Gamma>"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   323
  assume j2: "(a,\<tau>)\<in>set \<Gamma>"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   324
  show ?case
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   325
  proof (intro strip, simp)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   326
    fix pi::"name prm" and x::"'a::fs_name"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   327
    from j1 have j3: "valid (pi\<bullet>\<Gamma>)" by (rule valid_eqvt)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   328
    from j2 have "pi\<bullet>(a,\<tau>)\<in>pi\<bullet>(set \<Gamma>)" by (simp only: pt_set_bij[OF pt_name_inst, OF at_name_inst])  
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   329
    hence j4: "(pi\<bullet>a,\<tau>)\<in>set (pi\<bullet>\<Gamma>)" by (simp add: pt_list_set_pi[OF pt_name_inst])
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   330
    show "P (pi\<bullet>\<Gamma>) (Var (pi\<bullet>a)) \<tau> x" using a1 j3 j4 by force
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   331
  qed
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   332
next
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   333
  case (t2 \<Gamma> \<sigma> \<tau> t1 t2)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   334
  thus ?case using a2 by (simp, blast intro: typing_eqvt)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   335
next
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   336
  case (t3 \<Gamma> \<sigma> \<tau> a t)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   337
  have k1: "a\<sharp>\<Gamma>" by fact
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   338
  have k2: "((a,\<tau>)#\<Gamma>)\<turnstile>t:\<sigma>" by fact
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   339
  have k3: "\<forall>(pi::name prm) (x::'a::fs_name). P (pi \<bullet> ((a,\<tau>)#\<Gamma>)) (pi\<bullet>t) \<sigma> x" by fact
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   340
  show ?case
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   341
  proof (intro strip, simp)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   342
    fix pi::"name prm" and x::"'a::fs_name"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   343
    have f: "\<exists>c::name. c\<sharp>(pi\<bullet>a,pi\<bullet>t,pi\<bullet>\<Gamma>,x)"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   344
      by (rule at_exists_fresh[OF at_name_inst], simp add: fs_name1)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   345
    then obtain c::"name" 
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   346
      where f1: "c\<noteq>(pi\<bullet>a)" and f2: "c\<sharp>x" and f3: "c\<sharp>(pi\<bullet>t)" and f4: "c\<sharp>(pi\<bullet>\<Gamma>)"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   347
      by (force simp add: fresh_prod fresh_atm)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   348
    from k1 have k1a: "(pi\<bullet>a)\<sharp>(pi\<bullet>\<Gamma>)" 
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   349
      by (simp add: pt_fresh_left[OF pt_name_inst, OF at_name_inst] 
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   350
                    pt_rev_pi[OF pt_name_inst, OF at_name_inst])
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   351
    have l1: "(([(c,pi\<bullet>a)]@pi)\<bullet>\<Gamma>) = (pi\<bullet>\<Gamma>)" using f4 k1a 
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   352
      by (simp only: pt_name2, rule pt_fresh_fresh[OF pt_name_inst, OF at_name_inst])
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   353
    have "\<forall>x. P (([(c,pi\<bullet>a)]@pi)\<bullet>((a,\<tau>)#\<Gamma>)) (([(c,pi\<bullet>a)]@pi)\<bullet>t) \<sigma> x" using k3 by force
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   354
    hence l2: "\<forall>x. P ((c, \<tau>)#(pi\<bullet>\<Gamma>)) (([(c,pi\<bullet>a)]@pi)\<bullet>t) \<sigma> x" using f1 l1
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   355
      by (force simp add: pt_name2  calc_atm split: if_splits)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   356
    have "(([(c,pi\<bullet>a)]@pi)\<bullet>((a,\<tau>)#\<Gamma>)) \<turnstile> (([(c,pi\<bullet>a)]@pi)\<bullet>t) : \<sigma>" using k2 by (rule typing_eqvt)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   357
    hence l3: "((c, \<tau>)#(pi\<bullet>\<Gamma>)) \<turnstile> (([(c,pi\<bullet>a)]@pi)\<bullet>t) : \<sigma>" using l1 f1 
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   358
      by (force simp add: pt_name2 calc_atm split: if_splits)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   359
    have l4: "P (pi\<bullet>\<Gamma>) (Lam [c].(([(c,pi\<bullet>a)]@pi)\<bullet>t)) (\<tau> \<rightarrow> \<sigma>) x" using f2 f4 l2 l3 a3 by auto
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   360
    have alpha: "(Lam [c].([(c,pi\<bullet>a)]\<bullet>(pi\<bullet>t))) = (Lam [(pi\<bullet>a)].(pi\<bullet>t))" using f1 f3
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   361
      by (simp add: lam.inject alpha)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   362
    show "P (pi\<bullet>\<Gamma>) (Lam [(pi\<bullet>a)].(pi\<bullet>t)) (\<tau> \<rightarrow> \<sigma>) x" using l4 alpha 
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   363
      by (simp only: pt_name2)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   364
  qed
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   365
qed
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   366
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   367
lemma typing_induct[case_names t1 t2 t3]:
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   368
  fixes  P :: "(name\<times>ty) list \<Rightarrow> lam \<Rightarrow> ty \<Rightarrow>'a::fs_name\<Rightarrow>bool"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   369
  and    \<Gamma> :: "(name\<times>ty) list"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   370
  and    t :: "lam"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   371
  and    \<tau> :: "ty"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   372
  and    x :: "'a::fs_name"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   373
  assumes a: "\<Gamma> \<turnstile> t : \<tau>"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   374
  and a1:    "\<And>x \<Gamma> (a::name) \<tau>. valid \<Gamma> \<Longrightarrow> (a,\<tau>) \<in> set \<Gamma> \<Longrightarrow> P \<Gamma> (Var a) \<tau> x"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   375
  and a2:    "\<And>x \<Gamma> \<tau> \<sigma> t1 t2. 
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   376
              \<Gamma> \<turnstile> t1 : \<tau>\<rightarrow>\<sigma> \<Longrightarrow> (\<forall>z. P \<Gamma> t1 (\<tau>\<rightarrow>\<sigma>) z) \<Longrightarrow> \<Gamma> \<turnstile> t2 : \<tau> \<Longrightarrow> (\<forall>z. P \<Gamma> t2 \<tau> z)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   377
              \<Longrightarrow> P \<Gamma> (App t1 t2) \<sigma> x"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   378
  and a3:    "\<And>x (a::name) \<Gamma> \<tau> \<sigma> t. 
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   379
              a\<sharp>x \<Longrightarrow> a\<sharp>\<Gamma> \<Longrightarrow> ((a,\<tau>) # \<Gamma>) \<turnstile> t : \<sigma> \<Longrightarrow> (\<forall>z. P ((a,\<tau>)#\<Gamma>) t \<sigma> z)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   380
              \<Longrightarrow> P \<Gamma> (Lam [a].t) (\<tau>\<rightarrow>\<sigma>) x"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   381
  shows "P \<Gamma> t \<tau> x"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   382
using a a1 a2 a3 typing_induct_aux[of "\<Gamma>" "t" "\<tau>" "P" "[]" "x", simplified] by force
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   383
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   384
constdefs
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   385
  "sub" :: "(name\<times>ty) list \<Rightarrow> (name\<times>ty) list \<Rightarrow> bool" (" _ \<lless> _ " [80,80] 80)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   386
  "\<Gamma>1 \<lless> \<Gamma>2 \<equiv> \<forall>a \<sigma>. (a,\<sigma>)\<in>set \<Gamma>1 \<longrightarrow>  (a,\<sigma>)\<in>set \<Gamma>2"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   387
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   388
lemma weakening[rule_format]: 
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   389
  assumes a: "\<Gamma>1 \<turnstile> t : \<sigma>"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   390
  shows "valid \<Gamma>2 \<longrightarrow> \<Gamma>1 \<lless> \<Gamma>2 \<longrightarrow> \<Gamma>2 \<turnstile> t:\<sigma>"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   391
using a
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   392
apply(nominal_induct \<Gamma>1 t \<sigma> rule: typing_induct)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   393
apply(auto simp add: sub_def)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   394
done
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   395
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   396
lemma in_ctxt[rule_format]: "(a,\<tau>)\<in>set \<Gamma> \<longrightarrow> (a\<in>set(dom_ty \<Gamma>))"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   397
apply(induct_tac \<Gamma>)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   398
apply(auto)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   399
done
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   400
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   401
lemma free_vars: 
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   402
  assumes a: "\<Gamma> \<turnstile> t : \<tau>"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   403
  shows " (supp t)\<subseteq>set(dom_ty \<Gamma>)"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   404
using a
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   405
apply(nominal_induct \<Gamma> t \<tau> rule: typing_induct)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   406
apply(auto simp add: lam.supp abs_supp supp_atm in_ctxt)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   407
done
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   408
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   409
lemma t1_elim: "\<Gamma> \<turnstile> Var a : \<tau> \<Longrightarrow> valid \<Gamma> \<and> (a,\<tau>) \<in> set \<Gamma>"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   410
apply(ind_cases "\<Gamma> \<turnstile> Var a : \<tau>")
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   411
apply(auto simp add: lam.inject lam.distinct)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   412
done
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   413
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   414
lemma t2_elim: "\<Gamma> \<turnstile> App t1 t2 : \<sigma> \<Longrightarrow> \<exists>\<tau>. (\<Gamma> \<turnstile> t1 : \<tau>\<rightarrow>\<sigma> \<and> \<Gamma> \<turnstile> t2 : \<tau>)"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   415
apply(ind_cases "\<Gamma> \<turnstile> App t1 t2 : \<sigma>")
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   416
apply(auto simp add: lam.inject lam.distinct)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   417
done
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   418
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   419
lemma t3_elim: "\<lbrakk>\<Gamma> \<turnstile> Lam [a].t : \<sigma>;a\<sharp>\<Gamma>\<rbrakk>\<Longrightarrow> \<exists>\<tau> \<tau>'. \<sigma>=\<tau>\<rightarrow>\<tau>' \<and> ((a,\<tau>)#\<Gamma>) \<turnstile> t : \<tau>'"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   420
apply(ind_cases "\<Gamma> \<turnstile> Lam [a].t : \<sigma>")
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   421
apply(auto simp add: lam.distinct lam.inject alpha) 
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   422
apply(drule_tac pi="[(a,aa)]::name prm" in typing_eqvt)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   423
apply(simp)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   424
apply(subgoal_tac "([(a,aa)]::name prm)\<bullet>\<Gamma> = \<Gamma>")(*A*)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   425
apply(force simp add: calc_atm)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   426
(*A*)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   427
apply(force intro!: pt_fresh_fresh[OF pt_name_inst, OF at_name_inst])
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   428
done
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   429
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   430
lemma typing_valid: 
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   431
  assumes a: "\<Gamma> \<turnstile> t : \<tau>" 
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   432
  shows "valid \<Gamma>"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   433
using a by (induct, auto dest!: valid_elim)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   434
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   435
lemma ty_subs[rule_format]:
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   436
  fixes \<Gamma> ::"(name\<times>ty) list"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   437
  and   t1 ::"lam"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   438
  and   t2 ::"lam"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   439
  and   \<tau>  ::"ty"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   440
  and   \<sigma>  ::"ty" 
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   441
  and   c  ::"name"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   442
  shows  "((c,\<sigma>)#\<Gamma>) \<turnstile> t1:\<tau>\<longrightarrow> \<Gamma>\<turnstile> t2:\<sigma>\<longrightarrow> \<Gamma> \<turnstile> t1[c::=t2]:\<tau>"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   443
proof(nominal_induct t1 rule: lam_induct)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   444
  case (Var \<Gamma> \<sigma> \<tau> c t2 a)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   445
  show ?case
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   446
  proof(intro strip)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   447
    assume a1: "\<Gamma> \<turnstile>t2:\<sigma>"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   448
    assume a2: "((c,\<sigma>)#\<Gamma>) \<turnstile> Var a:\<tau>"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   449
    hence a21: "(a,\<tau>)\<in>set((c,\<sigma>)#\<Gamma>)" and a22: "valid((c,\<sigma>)#\<Gamma>)" by (auto dest: t1_elim)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   450
    from a22 have a23: "valid \<Gamma>" and a24: "c\<sharp>\<Gamma>" by (auto dest: valid_elim) 
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   451
    from a24 have a25: "\<not>(\<exists>\<tau>. (c,\<tau>)\<in>set \<Gamma>)" by (rule fresh_context)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   452
    show "\<Gamma>\<turnstile>(Var a)[c::=t2] : \<tau>"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   453
    proof (cases "a=c", simp_all)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   454
      assume case1: "a=c"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   455
      show "\<Gamma> \<turnstile> t2:\<tau>" using a1
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   456
      proof (cases "\<sigma>=\<tau>")
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   457
	assume "\<sigma>=\<tau>" thus ?thesis using a1 by simp 
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   458
      next
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   459
	assume a3: "\<sigma>\<noteq>\<tau>"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   460
	show ?thesis
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   461
	proof (rule ccontr)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   462
	  from a3 a21 have "(a,\<tau>)\<in>set \<Gamma>" by force
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   463
	  with case1 a25 show False by force 
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   464
	qed
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   465
      qed
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   466
    next
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   467
      assume case2: "a\<noteq>c"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   468
      with a21 have a26: "(a,\<tau>)\<in>set \<Gamma>" by force 
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   469
      from a23 a26 show "\<Gamma> \<turnstile> Var a:\<tau>" by force
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   470
    qed
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   471
  qed
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   472
next
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   473
  case (App \<Gamma> \<sigma> \<tau> c t2 s1 s2)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   474
  show ?case
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   475
  proof (intro strip, simp)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   476
    assume b1: "\<Gamma> \<turnstile>t2:\<sigma>" 
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   477
    assume b2: " ((c,\<sigma>)#\<Gamma>)\<turnstile>App s1 s2 : \<tau>"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   478
    hence "\<exists>\<tau>'. (((c,\<sigma>)#\<Gamma>)\<turnstile>s1:\<tau>'\<rightarrow>\<tau> \<and> ((c,\<sigma>)#\<Gamma>)\<turnstile>s2:\<tau>')" by (rule t2_elim) 
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   479
    then obtain \<tau>' where b3a: "((c,\<sigma>)#\<Gamma>)\<turnstile>s1:\<tau>'\<rightarrow>\<tau>" and b3b: "((c,\<sigma>)#\<Gamma>)\<turnstile>s2:\<tau>'" by force
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   480
    show "\<Gamma> \<turnstile>  App (s1[c::=t2]) (s2[c::=t2]) : \<tau>" 
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   481
      using b1 b3a b3b App by (rule_tac \<tau>="\<tau>'" in t2, auto)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   482
  qed
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   483
next
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   484
  case (Lam \<Gamma> \<sigma> \<tau> c t2 a s)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   485
  assume "a\<sharp>(\<Gamma>,\<sigma>,\<tau>,c,t2)" 
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   486
  hence f1: "a\<sharp>\<Gamma>" and f2: "a\<noteq>c" and f2': "c\<sharp>a" and f3: "a\<sharp>t2" and f4: "a\<sharp>((c,\<sigma>)#\<Gamma>)"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   487
    by (auto simp add: fresh_atm fresh_prod fresh_list_cons)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   488
  show ?case using f2 f3
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   489
  proof(intro strip, simp)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   490
    assume c1: "((c,\<sigma>)#\<Gamma>)\<turnstile>Lam [a].s : \<tau>"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   491
    hence "\<exists>\<tau>1 \<tau>2. \<tau>=\<tau>1\<rightarrow>\<tau>2 \<and> ((a,\<tau>1)#(c,\<sigma>)#\<Gamma>) \<turnstile> s : \<tau>2" using f4 by (auto dest: t3_elim) 
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   492
    then obtain \<tau>1 \<tau>2 where c11: "\<tau>=\<tau>1\<rightarrow>\<tau>2" and c12: "((a,\<tau>1)#(c,\<sigma>)#\<Gamma>) \<turnstile> s : \<tau>2" by force
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   493
    from c12 have "valid ((a,\<tau>1)#(c,\<sigma>)#\<Gamma>)" by (rule typing_valid)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   494
    hence ca: "valid \<Gamma>" and cb: "a\<sharp>\<Gamma>" and cc: "c\<sharp>\<Gamma>" 
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   495
      by (auto dest: valid_elim simp add: fresh_list_cons) 
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   496
    from c12 have c14: "((c,\<sigma>)#(a,\<tau>1)#\<Gamma>) \<turnstile> s : \<tau>2"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   497
    proof -
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   498
      have c2: "((a,\<tau>1)#(c,\<sigma>)#\<Gamma>) \<lless> ((c,\<sigma>)#(a,\<tau>1)#\<Gamma>)" by (force simp add: sub_def)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   499
      have c3: "valid ((c,\<sigma>)#(a,\<tau>1)#\<Gamma>)"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   500
	by (rule v2, rule v2, auto simp add: fresh_list_cons fresh_prod ca cb cc f2' fresh_ty)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   501
      from c12 c2 c3 show ?thesis by (force intro: weakening)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   502
    qed
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   503
    assume c8: "\<Gamma> \<turnstile> t2 : \<sigma>"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   504
    have c81: "((a,\<tau>1)#\<Gamma>)\<turnstile>t2 :\<sigma>"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   505
    proof -
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   506
      have c82: "\<Gamma> \<lless> ((a,\<tau>1)#\<Gamma>)" by (force simp add: sub_def)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   507
      have c83: "valid ((a,\<tau>1)#\<Gamma>)" using f1 ca by force
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   508
      with c8 c82 c83 show ?thesis by (force intro: weakening)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   509
    qed
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   510
    show "\<Gamma> \<turnstile> Lam [a].(s[c::=t2]) : \<tau>"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   511
      using c11 Lam c14 c81 f1 by force
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   512
  qed
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   513
qed
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   514
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   515
lemma subject[rule_format]: 
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   516
  fixes \<Gamma>  ::"(name\<times>ty) list"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   517
  and   t1 ::"lam"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   518
  and   t2 ::"lam"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   519
  and   \<tau>  ::"ty"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   520
  assumes a: "t1\<longrightarrow>\<^isub>\<beta>t2"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   521
  shows "(\<Gamma> \<turnstile> t1:\<tau>) \<longrightarrow> (\<Gamma> \<turnstile> t2:\<tau>)"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   522
using a
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   523
proof (nominal_induct t1 t2 rule: beta_induct, auto)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   524
  case (b1 \<Gamma> \<tau> t s1 s2)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   525
  assume i: "\<forall>\<Gamma> \<tau>. \<Gamma> \<turnstile> s1 : \<tau> \<longrightarrow> \<Gamma> \<turnstile> s2 : \<tau>" 
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   526
  assume "\<Gamma> \<turnstile> App s1 t : \<tau>"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   527
  hence "\<exists>\<sigma>. (\<Gamma> \<turnstile> s1 : \<sigma>\<rightarrow>\<tau> \<and> \<Gamma> \<turnstile> t : \<sigma>)" by (rule t2_elim)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   528
  then obtain \<sigma> where a1: "\<Gamma> \<turnstile> s1 : \<sigma>\<rightarrow>\<tau>" and a2: "\<Gamma> \<turnstile> t : \<sigma>" by force
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   529
  thus "\<Gamma> \<turnstile> App s2 t : \<tau>" using i by force
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   530
next
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   531
  case (b2 \<Gamma> \<tau> t s1 s2)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   532
  assume i: "\<forall>\<Gamma> \<tau>. \<Gamma> \<turnstile> s1 : \<tau> \<longrightarrow> \<Gamma> \<turnstile> s2 : \<tau>" 
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   533
  assume "\<Gamma> \<turnstile> App t s1 : \<tau>"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   534
  hence "\<exists>\<sigma>. (\<Gamma> \<turnstile> t : \<sigma>\<rightarrow>\<tau> \<and> \<Gamma> \<turnstile> s1 : \<sigma>)" by (rule t2_elim)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   535
  then obtain \<sigma> where a1: "\<Gamma> \<turnstile> t : \<sigma>\<rightarrow>\<tau>" and a2: "\<Gamma> \<turnstile> s1 : \<sigma>" by force
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   536
  thus "\<Gamma> \<turnstile> App t s2 : \<tau>" using i by force
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   537
next
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   538
  case (b3 \<Gamma> \<tau> a s1 s2)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   539
  assume "a\<sharp>(\<Gamma>,\<tau>)"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   540
  hence f: "a\<sharp>\<Gamma>" by (simp add: fresh_prod)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   541
  assume i: "\<forall>\<Gamma> \<tau>. \<Gamma> \<turnstile> s1 : \<tau> \<longrightarrow> \<Gamma> \<turnstile> s2 : \<tau>" 
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   542
  assume "\<Gamma> \<turnstile> Lam [a].s1 : \<tau>"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   543
  with f have "\<exists>\<tau>1 \<tau>2. \<tau>=\<tau>1\<rightarrow>\<tau>2 \<and> ((a,\<tau>1)#\<Gamma>) \<turnstile> s1 : \<tau>2" by (force dest: t3_elim)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   544
  then obtain \<tau>1 \<tau>2 where a1: "\<tau>=\<tau>1\<rightarrow>\<tau>2" and a2: "((a,\<tau>1)#\<Gamma>) \<turnstile> s1 : \<tau>2" by force
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   545
  thus "\<Gamma> \<turnstile> Lam [a].s2 : \<tau>" using f i by force 
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   546
next
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   547
  case (b4 \<Gamma> \<tau> a s1 s2)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   548
  have "a\<sharp>(s2,\<Gamma>,\<tau>)" by fact
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   549
  hence f: "a\<sharp>\<Gamma>" by (simp add: fresh_prod)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   550
  assume "\<Gamma> \<turnstile> App (Lam [a].s1) s2 : \<tau>"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   551
  hence "\<exists>\<sigma>. (\<Gamma> \<turnstile> (Lam [a].s1) : \<sigma>\<rightarrow>\<tau> \<and> \<Gamma> \<turnstile> s2 : \<sigma>)" by (rule t2_elim)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   552
  then obtain \<sigma> where a1: "\<Gamma> \<turnstile> (Lam [(a::name)].s1) : \<sigma>\<rightarrow>\<tau>" and a2: "\<Gamma> \<turnstile> s2 : \<sigma>" by force
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   553
  have  "((a,\<sigma>)#\<Gamma>) \<turnstile> s1 : \<tau>" using a1 f by (auto dest!: t3_elim)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   554
  with a2 show "\<Gamma> \<turnstile>  s1[a::=s2] : \<tau>" by (force intro: ty_subs)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   555
qed
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   556
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   557
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   558
lemma subject[rule_format]: 
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   559
  fixes \<Gamma>  ::"(name\<times>ty) list"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   560
  and   t1 ::"lam"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   561
  and   t2 ::"lam"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   562
  and   \<tau>  ::"ty"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   563
  assumes a: "t1\<longrightarrow>\<^isub>\<beta>t2"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   564
  shows "\<Gamma> \<turnstile> t1:\<tau> \<longrightarrow> \<Gamma> \<turnstile> t2:\<tau>"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   565
using a
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   566
apply(nominal_induct t1 t2 rule: beta_induct)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   567
apply(auto dest!: t2_elim t3_elim intro: ty_subs simp add: fresh_prod)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   568
done
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   569
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   570
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   571
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   572
subsection {* some facts about beta *}
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   573
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   574
constdefs
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   575
  "NORMAL" :: "lam \<Rightarrow> bool"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   576
  "NORMAL t \<equiv> \<not>(\<exists>t'. t\<longrightarrow>\<^isub>\<beta> t')"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   577
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   578
constdefs
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   579
  "SN" :: "lam \<Rightarrow> bool"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   580
  "SN t \<equiv> t\<in>termi Beta"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   581
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   582
lemma qq1: "\<lbrakk>SN(t1);t1\<longrightarrow>\<^isub>\<beta> t2\<rbrakk>\<Longrightarrow>SN(t2)"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   583
apply(simp add: SN_def)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   584
apply(drule_tac a="t2" in acc_downward)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   585
apply(auto)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   586
done
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   587
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   588
lemma qq2: "(\<forall>t2. t1\<longrightarrow>\<^isub>\<beta>t2 \<longrightarrow> SN(t2))\<Longrightarrow>SN(t1)"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   589
apply(simp add: SN_def)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   590
apply(rule accI)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   591
apply(auto)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   592
done
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   593
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   594
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   595
section {* Candidates *}
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   596
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   597
consts
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   598
  RED :: "ty \<Rightarrow> lam set"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   599
primrec
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   600
 "RED (TVar X) = {t. SN(t)}"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   601
 "RED (\<tau>\<rightarrow>\<sigma>) =   {t. \<forall>u. (u\<in>RED \<tau> \<longrightarrow> (App t u)\<in>RED \<sigma>)}"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   602
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   603
constdefs
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   604
  NEUT :: "lam \<Rightarrow> bool"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   605
  "NEUT t \<equiv> (\<exists>a. t=Var a)\<or>(\<exists>t1 t2. t=App t1 t2)" 
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   606
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   607
(* a slight hack to get the first element of applications *)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   608
consts
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   609
  FST :: "(lam\<times>lam) set"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   610
syntax 
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   611
  "FST_judge"   :: "lam\<Rightarrow>lam\<Rightarrow>bool" (" _ \<guillemotright> _" [80,80] 80)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   612
translations 
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   613
  "t1 \<guillemotright> t2" \<rightleftharpoons> "(t1,t2) \<in> FST"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   614
inductive FST
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   615
intros
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   616
fst[intro!]:  "(App t s) \<guillemotright> t"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   617
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   618
lemma fst_elim[elim!]: "(App t s) \<guillemotright> t' \<Longrightarrow> t=t'"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   619
apply(ind_cases "App t s \<guillemotright> t'")
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   620
apply(simp add: lam.inject)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   621
done
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   622
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   623
lemma qq3: "SN(App t s)\<Longrightarrow>SN(t)"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   624
apply(simp add: SN_def)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   625
apply(subgoal_tac "\<forall>z. (App t s \<guillemotright> z) \<longrightarrow> z\<in>termi Beta")(*A*)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   626
apply(force)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   627
(*A*)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   628
apply(erule acc_induct)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   629
apply(clarify)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   630
apply(ind_cases "x \<guillemotright> z")
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   631
apply(clarify)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   632
apply(rule accI)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   633
apply(auto intro: b1)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   634
done
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   635
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   636
constdefs
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   637
   "CR1" :: "ty \<Rightarrow> bool"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   638
   "CR1 \<tau> \<equiv> \<forall> t. (t\<in>RED \<tau> \<longrightarrow> SN(t))"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   639
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   640
   "CR2" :: "ty \<Rightarrow> bool"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   641
   "CR2 \<tau> \<equiv> \<forall>t t'. ((t\<in>RED \<tau> \<and> t \<longrightarrow>\<^isub>\<beta> t') \<longrightarrow> t'\<in>RED \<tau>)"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   642
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   643
   "CR3_RED" :: "lam \<Rightarrow> ty \<Rightarrow> bool"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   644
   "CR3_RED t \<tau> \<equiv> \<forall>t'. (t\<longrightarrow>\<^isub>\<beta> t' \<longrightarrow>  t'\<in>RED \<tau>)" 
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   645
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   646
   "CR3" :: "ty \<Rightarrow> bool"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   647
   "CR3 \<tau> \<equiv> \<forall>t. (NEUT t \<and> CR3_RED t \<tau>) \<longrightarrow> t\<in>RED \<tau>"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   648
   
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   649
   "CR4" :: "ty \<Rightarrow> bool"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   650
   "CR4 \<tau> \<equiv> \<forall>t. (NEUT t \<and> NORMAL t) \<longrightarrow>t\<in>RED \<tau>"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   651
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   652
lemma CR3_CR4: "CR3 \<tau> \<Longrightarrow> CR4 \<tau>"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   653
apply(simp (no_asm_use) add: CR3_def CR3_RED_def CR4_def NORMAL_def)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   654
apply(blast)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   655
done
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   656
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   657
lemma sub_ind: 
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   658
  "SN(u)\<Longrightarrow>(u\<in>RED \<tau>\<longrightarrow>(\<forall>t. (NEUT t\<and>CR2 \<tau>\<and>CR3 \<sigma>\<and>CR3_RED t (\<tau>\<rightarrow>\<sigma>))\<longrightarrow>(App t u)\<in>RED \<sigma>))"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   659
apply(simp add: SN_def)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   660
apply(erule acc_induct)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   661
apply(auto)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   662
apply(simp add: CR3_def)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   663
apply(rotate_tac 5)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   664
apply(drule_tac x="App t x" in spec)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   665
apply(drule mp)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   666
apply(rule conjI)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   667
apply(force simp only: NEUT_def)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   668
apply(simp (no_asm) add: CR3_RED_def)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   669
apply(clarify)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   670
apply(ind_cases "App t x \<longrightarrow>\<^isub>\<beta> t'")
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   671
apply(simp_all add: lam.inject)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   672
apply(simp only:  CR3_RED_def)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   673
apply(drule_tac x="s2" in spec)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   674
apply(simp)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   675
apply(drule_tac x="s2" in spec)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   676
apply(simp)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   677
apply(drule mp)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   678
apply(simp (no_asm_use) add: CR2_def)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   679
apply(blast)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   680
apply(drule_tac x="ta" in spec)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   681
apply(force)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   682
apply(auto simp only: NEUT_def lam.inject lam.distinct)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   683
done
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   684
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   685
lemma RED_props: "CR1 \<tau> \<and> CR2 \<tau> \<and> CR3 \<tau>"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   686
apply(induct_tac \<tau>)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   687
apply(auto)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   688
(* atom types *)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   689
(* C1 *)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   690
apply(simp add: CR1_def)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   691
(* C2 *)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   692
apply(simp add: CR2_def)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   693
apply(clarify)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   694
apply(drule_tac ?t2.0="t'" in  qq1)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   695
apply(assumption)+
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   696
(* C3 *)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   697
apply(simp add: CR3_def CR3_RED_def)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   698
apply(clarify)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   699
apply(rule qq2)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   700
apply(assumption)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   701
(* arrow types *)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   702
(* C1 *)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   703
apply(simp (no_asm) add: CR1_def)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   704
apply(clarify)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   705
apply(subgoal_tac "NEUT (Var a)")(*A*)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   706
apply(subgoal_tac "(Var a)\<in>RED ty1")(*C*)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   707
apply(drule_tac x="Var a" in spec)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   708
apply(simp)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   709
apply(simp add: CR1_def)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   710
apply(rotate_tac 1)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   711
apply(drule_tac x="App t (Var a)" in spec)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   712
apply(simp)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   713
apply(drule qq3) 
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   714
apply(assumption)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   715
(*C*)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   716
apply(simp (no_asm_use) add: CR3_def CR3_RED_def)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   717
apply(drule_tac x="Var a" in spec)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   718
apply(drule mp)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   719
apply(clarify)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   720
apply(ind_cases " Var a \<longrightarrow>\<^isub>\<beta> t'")
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   721
apply(simp (no_asm_use) add: lam.distinct)+ 
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   722
(*A*)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   723
apply(simp (no_asm) only: NEUT_def)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   724
apply(rule disjCI)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   725
apply(rule_tac x="a" in exI)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   726
apply(simp (no_asm))
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   727
(* C2 *)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   728
apply(simp (no_asm) add: CR2_def)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   729
apply(clarify)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   730
apply(drule_tac x="u" in spec)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   731
apply(simp)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   732
apply(subgoal_tac "App t u \<longrightarrow>\<^isub>\<beta> App t' u")(*X*)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   733
apply(simp (no_asm_use) only: CR2_def)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   734
apply(blast)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   735
(*X*)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   736
apply(force intro!: b1)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   737
(* C3 *)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   738
apply(unfold CR3_def)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   739
apply(rule allI)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   740
apply(rule impI)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   741
apply(erule conjE)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   742
apply(simp (no_asm))
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   743
apply(rule allI)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   744
apply(rule impI)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   745
apply(subgoal_tac "SN(u)")(*Z*)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   746
apply(fold CR3_def)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   747
apply(drule_tac \<tau>="ty1" and \<sigma>="ty2" in sub_ind)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   748
apply(simp)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   749
(*Z*)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   750
apply(simp add: CR1_def)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   751
done
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   752
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   753
lemma double_acc_aux:
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   754
  assumes a_acc: "a \<in> acc r"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   755
  and b_acc: "b \<in> acc r"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   756
  and hyp: "\<And>x z.
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   757
    (\<And>y. (y, x) \<in> r \<Longrightarrow> y \<in> acc r) \<Longrightarrow>
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   758
    (\<And>y. (y, x) \<in> r \<Longrightarrow> P y z) \<Longrightarrow>
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   759
    (\<And>u. (u, z) \<in> r \<Longrightarrow> u \<in> acc r) \<Longrightarrow>
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   760
    (\<And>u. (u, z) \<in> r \<Longrightarrow> P x u) \<Longrightarrow> P x z"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   761
  shows "P a b"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   762
proof -
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   763
  from a_acc
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   764
  have r: "\<And>b. b \<in> acc r \<Longrightarrow> P a b"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   765
  proof (induct a rule: acc.induct)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   766
    case (accI x)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   767
    note accI' = accI
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   768
    have "b \<in> acc r" .
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   769
    thus ?case
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   770
    proof (induct b rule: acc.induct)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   771
      case (accI y)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   772
      show ?case
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   773
	apply (rule hyp)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   774
	apply (erule accI')
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   775
	apply (erule accI')
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   776
	apply (rule acc.accI)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   777
	apply (erule accI)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   778
	apply (erule accI)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   779
	apply (erule accI)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   780
	done
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   781
    qed
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   782
  qed
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   783
  from b_acc show ?thesis by (rule r)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   784
qed
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   785
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   786
lemma double_acc:
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   787
  "\<lbrakk>a \<in> acc r; b \<in> acc r; \<forall>x z. ((\<forall>y. (y, x)\<in>r\<longrightarrow>P y z)\<and>(\<forall>u. (u, z)\<in>r\<longrightarrow>P x u))\<longrightarrow>P x z\<rbrakk>\<Longrightarrow>P a b"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   788
apply(rule_tac r="r" in double_acc_aux)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   789
apply(assumption)+
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   790
apply(blast)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   791
done
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   792
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   793
lemma abs_RED[rule_format]: "(\<forall>s\<in>RED \<tau>. t[x::=s]\<in>RED \<sigma>)\<longrightarrow>Lam [x].t\<in>RED (\<tau>\<rightarrow>\<sigma>)"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   794
apply(simp)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   795
apply(clarify)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   796
apply(subgoal_tac "t\<in>termi Beta")(*1*)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   797
apply(erule rev_mp)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   798
apply(subgoal_tac "u \<in> RED \<tau>")(*A*)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   799
apply(erule rev_mp)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   800
apply(rule_tac a="t" and b="u" in double_acc)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   801
apply(assumption)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   802
apply(subgoal_tac "CR1 \<tau>")(*A*)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   803
apply(simp add: CR1_def SN_def)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   804
(*A*)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   805
apply(force simp add: RED_props)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   806
apply(simp)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   807
apply(clarify)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   808
apply(subgoal_tac "CR3 \<sigma>")(*B*)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   809
apply(simp add: CR3_def)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   810
apply(rotate_tac 6)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   811
apply(drule_tac x="App(Lam[x].xa ) z" in spec)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   812
apply(drule mp)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   813
apply(rule conjI)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   814
apply(force simp add: NEUT_def)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   815
apply(simp add: CR3_RED_def)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   816
apply(clarify)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   817
apply(ind_cases "App(Lam[x].xa) z \<longrightarrow>\<^isub>\<beta> t'")
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   818
apply(auto simp add: lam.inject lam.distinct)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   819
apply(drule beta_abs)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   820
apply(auto)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   821
apply(drule_tac x="t''" in spec)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   822
apply(simp)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   823
apply(drule mp)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   824
apply(clarify)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   825
apply(drule_tac x="s" in bspec)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   826
apply(assumption)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   827
apply(subgoal_tac "xa [ x ::= s ] \<longrightarrow>\<^isub>\<beta>  t'' [ x ::= s ]")(*B*)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   828
apply(subgoal_tac "CR2 \<sigma>")(*C*)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   829
apply(simp (no_asm_use) add: CR2_def)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   830
apply(blast)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   831
(*C*)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   832
apply(force simp add: RED_props)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   833
(*B*)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   834
apply(force intro!: beta_subst)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   835
apply(assumption)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   836
apply(rotate_tac 3)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   837
apply(drule_tac x="s2" in spec)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   838
apply(subgoal_tac "s2\<in>RED \<tau>")(*D*)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   839
apply(simp)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   840
(*D*)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   841
apply(subgoal_tac "CR2 \<tau>")(*E*)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   842
apply(simp (no_asm_use) add: CR2_def)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   843
apply(blast)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   844
(*E*)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   845
apply(force simp add: RED_props)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   846
apply(simp add: alpha)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   847
apply(erule disjE)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   848
apply(force)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   849
apply(auto)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   850
apply(simp add: subst_rename)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   851
apply(drule_tac x="z" in bspec)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   852
apply(assumption)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   853
(*B*)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   854
apply(force simp add: RED_props)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   855
(*1*)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   856
apply(drule_tac x="Var x" in bspec)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   857
apply(subgoal_tac "CR3 \<tau>")(*2*) 
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   858
apply(drule CR3_CR4)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   859
apply(simp add: CR4_def)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   860
apply(drule_tac x="Var x" in spec)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   861
apply(drule mp)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   862
apply(rule conjI)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   863
apply(force simp add: NEUT_def)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   864
apply(simp add: NORMAL_def)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   865
apply(clarify)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   866
apply(ind_cases "Var x \<longrightarrow>\<^isub>\<beta> t'")
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   867
apply(auto simp add: lam.inject lam.distinct)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   868
apply(force simp add: RED_props)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   869
apply(simp add: id_subs)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   870
apply(subgoal_tac "CR1 \<sigma>")(*3*)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   871
apply(simp add: CR1_def SN_def)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   872
(*3*)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   873
apply(force simp add: RED_props)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   874
done
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   875
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   876
lemma all_RED: 
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   877
 "((\<forall>a \<sigma>. (a,\<sigma>)\<in>set(\<Gamma>)\<longrightarrow>(a\<in>set(dom_sss \<theta>)\<and>\<theta><a>\<in>RED \<sigma>))\<and>\<Gamma>\<turnstile>t:\<tau>) \<longrightarrow> (t[<\<theta>>]\<in>RED \<tau>)"
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   878
apply(nominal_induct t rule: lam_induct)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   879
(* Variables *)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   880
apply(force dest: t1_elim)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   881
(* Applications *)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   882
apply(auto dest!: t2_elim)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   883
apply(drule_tac x="a" in spec)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   884
apply(drule_tac x="a" in spec)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   885
apply(drule_tac x="\<tau>\<rightarrow>aa" in spec)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   886
apply(drule_tac x="\<tau>" in spec)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   887
apply(drule_tac x="b" in spec)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   888
apply(drule_tac x="b" in spec)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   889
apply(force)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   890
(* Abstractions *)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   891
apply(drule t3_elim)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   892
apply(simp add: fresh_prod)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   893
apply(auto)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   894
apply(drule_tac x="((ab,\<tau>)#a)" in spec)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   895
apply(drule_tac x="\<tau>'" in spec)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   896
apply(drule_tac x="b" in spec)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   897
apply(simp)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   898
(* HERE *)
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   899
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   900
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   901
done
836135c8acb2 Initial commit.
urbanc
parents:
diff changeset
   902