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