Quot/Nominal/LamEx.thy
author Christian Urban <urbanc@in.tum.de>
Thu, 28 Jan 2010 14:20:26 +0100
changeset 983 31b4ac97cfea
parent 981 bc739536b715
child 984 8e2dd0b29466
permissions -rw-r--r--
attempt to prove equivalence between alpha definitions
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
947
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     1
theory LamEx
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     2
imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "../QuotMain" 
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     3
begin
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     4
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     5
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     6
(* lemmas that should be in Nominal \<dots>\<dots>must be cleaned *)
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     7
lemma in_permute_iff:
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     8
  shows "(p \<bullet> x) \<in> (p \<bullet> X) \<longleftrightarrow> x \<in> X"
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     9
apply(unfold mem_def permute_fun_def)[1]
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    10
apply(simp add: permute_bool_def) 
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    11
done
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    12
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    13
lemma fresh_star_permute_iff:
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    14
  shows "(p \<bullet> a) \<sharp>* (p \<bullet> x) \<longleftrightarrow> a \<sharp>* x"
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    15
apply(simp add: fresh_star_def)
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    16
apply(auto)
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    17
apply(drule_tac x="p \<bullet> xa" in bspec)
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    18
apply(unfold mem_def permute_fun_def)[1] 
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    19
apply(simp add: eqvts)
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    20
apply(simp add: fresh_permute_iff)
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    21
apply(rule_tac ?p1="- p" in fresh_permute_iff[THEN iffD1])
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    22
apply(simp)
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    23
apply(drule_tac x="- p \<bullet> xa" in bspec)
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    24
apply(rule_tac ?p1="p" in in_permute_iff[THEN iffD1])
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    25
apply(simp)
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    26
apply(simp)
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    27
done
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    28
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    29
lemma fresh_minus_perm:
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    30
  fixes p::perm
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    31
  shows "a \<sharp> (- p) \<longleftrightarrow> a \<sharp> p"
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    32
  apply(simp add: fresh_def)
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    33
  apply(simp only: supp_minus_perm)
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    34
  done
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    35
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    36
lemma fresh_plus:
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    37
  fixes p q::perm
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    38
  shows "\<lbrakk>a \<sharp> p;  a \<sharp> q\<rbrakk> \<Longrightarrow> a \<sharp> (p + q)"
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    39
unfolding fresh_def
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    40
using supp_plus_perm
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    41
apply(auto)
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    42
done
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    43
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    44
lemma fresh_star_plus:
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    45
  fixes p q::perm
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    46
  shows "\<lbrakk>a \<sharp>* p;  a \<sharp>* q\<rbrakk> \<Longrightarrow> a \<sharp>* (p + q)"
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    47
unfolding fresh_star_def
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    48
by (simp add: fresh_plus)
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    49
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    50
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    51
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    52
atom_decl name
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    53
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    54
datatype rlam =
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    55
  rVar "name"
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    56
| rApp "rlam" "rlam"
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    57
| rLam "name" "rlam"
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    58
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    59
fun
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    60
  rfv :: "rlam \<Rightarrow> atom set"
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    61
where
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    62
  rfv_var: "rfv (rVar a) = {atom a}"
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    63
| rfv_app: "rfv (rApp t1 t2) = (rfv t1) \<union> (rfv t2)"
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    64
| rfv_lam: "rfv (rLam a t) = (rfv t) - {atom a}"
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    65
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    66
instantiation rlam :: pt
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    67
begin
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    68
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    69
primrec
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    70
  permute_rlam
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    71
where
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    72
  "permute_rlam pi (rVar a) = rVar (pi \<bullet> a)"
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    73
| "permute_rlam pi (rApp t1 t2) = rApp (permute_rlam pi t1) (permute_rlam pi t2)"
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    74
| "permute_rlam pi (rLam a t) = rLam (pi \<bullet> a) (permute_rlam pi t)"
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    75
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    76
instance
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    77
apply default
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    78
apply(induct_tac [!] x)
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    79
apply(simp_all)
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    80
done
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    81
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    82
end
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    83
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    84
instantiation rlam :: fs
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    85
begin
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    86
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    87
lemma neg_conj:
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    88
  "\<not>(P \<and> Q) \<longleftrightarrow> (\<not>P) \<or> (\<not>Q)"
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    89
  by simp
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    90
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    91
lemma infinite_Un:
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    92
  "infinite (S \<union> T) \<longleftrightarrow> infinite S \<or> infinite T"
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    93
  by simp
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    94
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    95
instance
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    96
apply default
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    97
apply(induct_tac x)
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    98
(* var case *)
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    99
apply(simp add: supp_def)
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   100
apply(fold supp_def)[1]
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   101
apply(simp add: supp_at_base)
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   102
(* app case *)
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   103
apply(simp only: supp_def)
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   104
apply(simp only: permute_rlam.simps) 
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   105
apply(simp only: rlam.inject) 
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   106
apply(simp only: neg_conj)
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   107
apply(simp only: Collect_disj_eq)
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   108
apply(simp only: infinite_Un)
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   109
apply(simp only: Collect_disj_eq)
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   110
apply(simp)
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   111
(* lam case *)
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   112
apply(simp only: supp_def)
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   113
apply(simp only: permute_rlam.simps) 
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   114
apply(simp only: rlam.inject) 
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   115
apply(simp only: neg_conj)
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   116
apply(simp only: Collect_disj_eq)
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   117
apply(simp only: infinite_Un)
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   118
apply(simp only: Collect_disj_eq)
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   119
apply(simp)
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   120
apply(fold supp_def)[1]
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   121
apply(simp add: supp_at_base)
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   122
done
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   123
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   124
end
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   125
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   126
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   127
(* for the eqvt proof of the alpha-equivalence *)
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   128
declare permute_rlam.simps[eqvt]
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   129
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   130
lemma rfv_eqvt[eqvt]:
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   131
  shows "(pi\<bullet>rfv t) = rfv (pi\<bullet>t)"
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   132
apply(induct t)
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   133
apply(simp_all)
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   134
apply(simp add: permute_set_eq atom_eqvt)
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   135
apply(simp add: union_eqvt)
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   136
apply(simp add: Diff_eqvt)
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   137
apply(simp add: permute_set_eq atom_eqvt)
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   138
done
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   139
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   140
inductive
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   141
    alpha :: "rlam \<Rightarrow> rlam \<Rightarrow> bool" ("_ \<approx> _" [100, 100] 100)
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   142
where
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   143
  a1: "a = b \<Longrightarrow> (rVar a) \<approx> (rVar b)"
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   144
| a2: "\<lbrakk>t1 \<approx> t2; s1 \<approx> s2\<rbrakk> \<Longrightarrow> rApp t1 s1 \<approx> rApp t2 s2"
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   145
| a3: "\<exists>pi. (rfv t - {atom a} = rfv s - {atom b} \<and> (rfv t - {atom a})\<sharp>* pi \<and> (pi \<bullet> t) \<approx> s \<and> (pi \<bullet> a) = b)
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   146
       \<Longrightarrow> rLam a t \<approx> rLam b s"
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   147
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   148
text {* should be automatic with new version of eqvt-machinery *}
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   149
lemma alpha_eqvt:
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   150
  shows "t \<approx> s \<Longrightarrow> (pi \<bullet> t) \<approx> (pi \<bullet> s)"
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   151
apply(induct rule: alpha.induct)
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   152
apply(simp add: a1)
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   153
apply(simp add: a2)
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   154
apply(simp)
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   155
apply(rule a3)
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   156
apply(erule conjE)
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   157
apply(erule exE)
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   158
apply(erule conjE)
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   159
apply(rule_tac x="pi \<bullet> pia" in exI)
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   160
apply(rule conjI)
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   161
apply(rule_tac ?p1="- pi" in permute_eq_iff[THEN iffD1])
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   162
apply(simp add: eqvts atom_eqvt)
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   163
apply(rule conjI)
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   164
apply(rule_tac ?p1="- pi" in fresh_star_permute_iff[THEN iffD1])
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   165
apply(simp add: eqvts atom_eqvt)
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   166
apply(rule conjI)
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   167
apply(subst permute_eqvt[symmetric])
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   168
apply(simp)
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   169
apply(subst permute_eqvt[symmetric])
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   170
apply(simp)
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   171
done
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   172
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   173
lemma alpha_refl:
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   174
  shows "t \<approx> t"
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   175
apply(induct t rule: rlam.induct)
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   176
apply(simp add: a1)
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   177
apply(simp add: a2)
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   178
apply(rule a3)
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   179
apply(rule_tac x="0" in exI)
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   180
apply(simp_all add: fresh_star_def fresh_zero_perm)
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   181
done
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   182
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   183
lemma alpha_sym:
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   184
  shows "t \<approx> s \<Longrightarrow> s \<approx> t"
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   185
apply(induct rule: alpha.induct)
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   186
apply(simp add: a1)
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   187
apply(simp add: a2)
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   188
apply(rule a3)
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   189
apply(erule exE)
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   190
apply(rule_tac x="- pi" in exI)
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   191
apply(simp)
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   192
apply(simp add: fresh_star_def fresh_minus_perm)
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   193
apply(rule conjI)
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   194
apply(erule conjE)+
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   195
apply(rotate_tac 3)
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   196
apply(drule_tac pi="- pi" in alpha_eqvt)
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   197
apply(simp)
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   198
apply(clarify)
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   199
apply(simp)
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   200
done
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   201
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   202
lemma alpha_trans:
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   203
  shows "t1 \<approx> t2 \<Longrightarrow> t2 \<approx> t3 \<Longrightarrow> t1 \<approx> t3"
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   204
apply(induct arbitrary: t3 rule: alpha.induct)
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   205
apply(erule alpha.cases)
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   206
apply(simp_all)
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   207
apply(simp add: a1)
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   208
apply(rotate_tac 4)
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   209
apply(erule alpha.cases)
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   210
apply(simp_all)
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   211
apply(simp add: a2)
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   212
apply(rotate_tac 1)
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   213
apply(erule alpha.cases)
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   214
apply(simp_all)
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   215
apply(erule conjE)+
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   216
apply(erule exE)+
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   217
apply(erule conjE)+
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   218
apply(rule a3)
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   219
apply(rule_tac x="pia + pi" in exI)
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   220
apply(simp add: fresh_star_plus)
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   221
apply(drule_tac x="- pia \<bullet> sa" in spec)
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   222
apply(drule mp)
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   223
apply(rotate_tac 8)
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   224
apply(drule_tac pi="- pia" in alpha_eqvt)
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   225
apply(simp)
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   226
apply(rotate_tac 11)
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   227
apply(drule_tac pi="pia" in alpha_eqvt)
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   228
apply(simp)
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   229
done
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   230
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   231
lemma alpha_equivp:
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   232
  shows "equivp alpha"
981
bc739536b715 Minor when looking at lam.distinct and lam.inject
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 975
diff changeset
   233
  apply(rule equivpI)
bc739536b715 Minor when looking at lam.distinct and lam.inject
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 975
diff changeset
   234
  unfolding reflp_def symp_def transp_def
bc739536b715 Minor when looking at lam.distinct and lam.inject
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 975
diff changeset
   235
  apply(auto intro: alpha_refl alpha_sym alpha_trans)
bc739536b715 Minor when looking at lam.distinct and lam.inject
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 975
diff changeset
   236
  done
947
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   237
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   238
lemma alpha_rfv:
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   239
  shows "t \<approx> s \<Longrightarrow> rfv t = rfv s"
981
bc739536b715 Minor when looking at lam.distinct and lam.inject
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 975
diff changeset
   240
  apply(induct rule: alpha.induct)
bc739536b715 Minor when looking at lam.distinct and lam.inject
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 975
diff changeset
   241
  apply(simp_all)
bc739536b715 Minor when looking at lam.distinct and lam.inject
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 975
diff changeset
   242
  done
947
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   243
983
31b4ac97cfea attempt to prove equivalence between alpha definitions
Christian Urban <urbanc@in.tum.de>
parents: 981
diff changeset
   244
inductive
31b4ac97cfea attempt to prove equivalence between alpha definitions
Christian Urban <urbanc@in.tum.de>
parents: 981
diff changeset
   245
    alpha2 :: "rlam \<Rightarrow> rlam \<Rightarrow> bool" ("_ \<approx>2 _" [100, 100] 100)
31b4ac97cfea attempt to prove equivalence between alpha definitions
Christian Urban <urbanc@in.tum.de>
parents: 981
diff changeset
   246
where
31b4ac97cfea attempt to prove equivalence between alpha definitions
Christian Urban <urbanc@in.tum.de>
parents: 981
diff changeset
   247
  a1: "a = b \<Longrightarrow> (rVar a) \<approx>2 (rVar b)"
31b4ac97cfea attempt to prove equivalence between alpha definitions
Christian Urban <urbanc@in.tum.de>
parents: 981
diff changeset
   248
| a2: "\<lbrakk>t1 \<approx>2 t2; s1 \<approx>2 s2\<rbrakk> \<Longrightarrow> rApp t1 s1 \<approx>2 rApp t2 s2"
31b4ac97cfea attempt to prove equivalence between alpha definitions
Christian Urban <urbanc@in.tum.de>
parents: 981
diff changeset
   249
| a3: "(a = b \<and> t \<approx>2 s) \<or> (a \<noteq> b \<and> ((a \<leftrightarrow> b) \<bullet> t) \<approx>2 s \<and> atom b \<notin> rfv t)\<Longrightarrow> rLam a t \<approx>2 rLam b s"
31b4ac97cfea attempt to prove equivalence between alpha definitions
Christian Urban <urbanc@in.tum.de>
parents: 981
diff changeset
   250
31b4ac97cfea attempt to prove equivalence between alpha definitions
Christian Urban <urbanc@in.tum.de>
parents: 981
diff changeset
   251
lemma 
31b4ac97cfea attempt to prove equivalence between alpha definitions
Christian Urban <urbanc@in.tum.de>
parents: 981
diff changeset
   252
  assumes a1: "t \<approx>2 s"
31b4ac97cfea attempt to prove equivalence between alpha definitions
Christian Urban <urbanc@in.tum.de>
parents: 981
diff changeset
   253
  shows "t \<approx> s"
31b4ac97cfea attempt to prove equivalence between alpha definitions
Christian Urban <urbanc@in.tum.de>
parents: 981
diff changeset
   254
using a1
31b4ac97cfea attempt to prove equivalence between alpha definitions
Christian Urban <urbanc@in.tum.de>
parents: 981
diff changeset
   255
apply(induct)
31b4ac97cfea attempt to prove equivalence between alpha definitions
Christian Urban <urbanc@in.tum.de>
parents: 981
diff changeset
   256
apply(rule alpha.intros)
31b4ac97cfea attempt to prove equivalence between alpha definitions
Christian Urban <urbanc@in.tum.de>
parents: 981
diff changeset
   257
apply(simp)
31b4ac97cfea attempt to prove equivalence between alpha definitions
Christian Urban <urbanc@in.tum.de>
parents: 981
diff changeset
   258
apply(rule alpha.intros)
31b4ac97cfea attempt to prove equivalence between alpha definitions
Christian Urban <urbanc@in.tum.de>
parents: 981
diff changeset
   259
apply(simp)
31b4ac97cfea attempt to prove equivalence between alpha definitions
Christian Urban <urbanc@in.tum.de>
parents: 981
diff changeset
   260
apply(simp)
31b4ac97cfea attempt to prove equivalence between alpha definitions
Christian Urban <urbanc@in.tum.de>
parents: 981
diff changeset
   261
apply(rule alpha.intros)
31b4ac97cfea attempt to prove equivalence between alpha definitions
Christian Urban <urbanc@in.tum.de>
parents: 981
diff changeset
   262
apply(erule disjE)
31b4ac97cfea attempt to prove equivalence between alpha definitions
Christian Urban <urbanc@in.tum.de>
parents: 981
diff changeset
   263
apply(rule_tac x="0" in exI)
31b4ac97cfea attempt to prove equivalence between alpha definitions
Christian Urban <urbanc@in.tum.de>
parents: 981
diff changeset
   264
apply(simp add: fresh_star_def fresh_zero_perm)
31b4ac97cfea attempt to prove equivalence between alpha definitions
Christian Urban <urbanc@in.tum.de>
parents: 981
diff changeset
   265
apply(erule conjE)+
31b4ac97cfea attempt to prove equivalence between alpha definitions
Christian Urban <urbanc@in.tum.de>
parents: 981
diff changeset
   266
apply(drule alpha_rfv)
31b4ac97cfea attempt to prove equivalence between alpha definitions
Christian Urban <urbanc@in.tum.de>
parents: 981
diff changeset
   267
apply(simp)
31b4ac97cfea attempt to prove equivalence between alpha definitions
Christian Urban <urbanc@in.tum.de>
parents: 981
diff changeset
   268
apply(rule_tac x="(a \<leftrightarrow> b)" in exI)
31b4ac97cfea attempt to prove equivalence between alpha definitions
Christian Urban <urbanc@in.tum.de>
parents: 981
diff changeset
   269
apply(simp)
31b4ac97cfea attempt to prove equivalence between alpha definitions
Christian Urban <urbanc@in.tum.de>
parents: 981
diff changeset
   270
apply(erule conjE)+
31b4ac97cfea attempt to prove equivalence between alpha definitions
Christian Urban <urbanc@in.tum.de>
parents: 981
diff changeset
   271
apply(rule conjI)
31b4ac97cfea attempt to prove equivalence between alpha definitions
Christian Urban <urbanc@in.tum.de>
parents: 981
diff changeset
   272
apply(drule alpha_rfv)
31b4ac97cfea attempt to prove equivalence between alpha definitions
Christian Urban <urbanc@in.tum.de>
parents: 981
diff changeset
   273
apply(drule sym)
31b4ac97cfea attempt to prove equivalence between alpha definitions
Christian Urban <urbanc@in.tum.de>
parents: 981
diff changeset
   274
apply(simp)
31b4ac97cfea attempt to prove equivalence between alpha definitions
Christian Urban <urbanc@in.tum.de>
parents: 981
diff changeset
   275
defer
31b4ac97cfea attempt to prove equivalence between alpha definitions
Christian Urban <urbanc@in.tum.de>
parents: 981
diff changeset
   276
apply(subgoal_tac "atom a \<sharp> (rfv t - {atom a})")
31b4ac97cfea attempt to prove equivalence between alpha definitions
Christian Urban <urbanc@in.tum.de>
parents: 981
diff changeset
   277
apply(subgoal_tac "atom b \<sharp> (rfv t - {atom a})")
31b4ac97cfea attempt to prove equivalence between alpha definitions
Christian Urban <urbanc@in.tum.de>
parents: 981
diff changeset
   278
defer
31b4ac97cfea attempt to prove equivalence between alpha definitions
Christian Urban <urbanc@in.tum.de>
parents: 981
diff changeset
   279
sorry
31b4ac97cfea attempt to prove equivalence between alpha definitions
Christian Urban <urbanc@in.tum.de>
parents: 981
diff changeset
   280
31b4ac97cfea attempt to prove equivalence between alpha definitions
Christian Urban <urbanc@in.tum.de>
parents: 981
diff changeset
   281
lemma 
31b4ac97cfea attempt to prove equivalence between alpha definitions
Christian Urban <urbanc@in.tum.de>
parents: 981
diff changeset
   282
  assumes a1: "t \<approx> s"
31b4ac97cfea attempt to prove equivalence between alpha definitions
Christian Urban <urbanc@in.tum.de>
parents: 981
diff changeset
   283
  shows "t \<approx>2 s"
31b4ac97cfea attempt to prove equivalence between alpha definitions
Christian Urban <urbanc@in.tum.de>
parents: 981
diff changeset
   284
using a1
31b4ac97cfea attempt to prove equivalence between alpha definitions
Christian Urban <urbanc@in.tum.de>
parents: 981
diff changeset
   285
apply(induct)
31b4ac97cfea attempt to prove equivalence between alpha definitions
Christian Urban <urbanc@in.tum.de>
parents: 981
diff changeset
   286
apply(rule alpha2.intros)
31b4ac97cfea attempt to prove equivalence between alpha definitions
Christian Urban <urbanc@in.tum.de>
parents: 981
diff changeset
   287
apply(simp)
31b4ac97cfea attempt to prove equivalence between alpha definitions
Christian Urban <urbanc@in.tum.de>
parents: 981
diff changeset
   288
apply(rule alpha2.intros)
31b4ac97cfea attempt to prove equivalence between alpha definitions
Christian Urban <urbanc@in.tum.de>
parents: 981
diff changeset
   289
apply(simp)
31b4ac97cfea attempt to prove equivalence between alpha definitions
Christian Urban <urbanc@in.tum.de>
parents: 981
diff changeset
   290
apply(simp)
31b4ac97cfea attempt to prove equivalence between alpha definitions
Christian Urban <urbanc@in.tum.de>
parents: 981
diff changeset
   291
apply(clarify)
31b4ac97cfea attempt to prove equivalence between alpha definitions
Christian Urban <urbanc@in.tum.de>
parents: 981
diff changeset
   292
apply(rule alpha2.intros)
31b4ac97cfea attempt to prove equivalence between alpha definitions
Christian Urban <urbanc@in.tum.de>
parents: 981
diff changeset
   293
apply(frule alpha_rfv)
31b4ac97cfea attempt to prove equivalence between alpha definitions
Christian Urban <urbanc@in.tum.de>
parents: 981
diff changeset
   294
apply(rotate_tac 4)
31b4ac97cfea attempt to prove equivalence between alpha definitions
Christian Urban <urbanc@in.tum.de>
parents: 981
diff changeset
   295
apply(drule sym)
31b4ac97cfea attempt to prove equivalence between alpha definitions
Christian Urban <urbanc@in.tum.de>
parents: 981
diff changeset
   296
apply(simp)
31b4ac97cfea attempt to prove equivalence between alpha definitions
Christian Urban <urbanc@in.tum.de>
parents: 981
diff changeset
   297
apply(drule sym)
31b4ac97cfea attempt to prove equivalence between alpha definitions
Christian Urban <urbanc@in.tum.de>
parents: 981
diff changeset
   298
apply(simp)
31b4ac97cfea attempt to prove equivalence between alpha definitions
Christian Urban <urbanc@in.tum.de>
parents: 981
diff changeset
   299
apply(case_tac "a = pi \<bullet> a")
31b4ac97cfea attempt to prove equivalence between alpha definitions
Christian Urban <urbanc@in.tum.de>
parents: 981
diff changeset
   300
apply(simp)
31b4ac97cfea attempt to prove equivalence between alpha definitions
Christian Urban <urbanc@in.tum.de>
parents: 981
diff changeset
   301
defer
31b4ac97cfea attempt to prove equivalence between alpha definitions
Christian Urban <urbanc@in.tum.de>
parents: 981
diff changeset
   302
apply(simp)
31b4ac97cfea attempt to prove equivalence between alpha definitions
Christian Urban <urbanc@in.tum.de>
parents: 981
diff changeset
   303
sorry
947
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   304
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   305
quotient_type lam = rlam / alpha
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   306
  by (rule alpha_equivp)
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   307
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   308
quotient_definition
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   309
  "Var :: name \<Rightarrow> lam"
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   310
as
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   311
  "rVar"
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   312
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   313
quotient_definition
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   314
   "App :: lam \<Rightarrow> lam \<Rightarrow> lam"
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   315
as
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   316
  "rApp"
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   317
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   318
quotient_definition
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   319
  "Lam :: name \<Rightarrow> lam \<Rightarrow> lam"
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   320
as
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   321
  "rLam"
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   322
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   323
quotient_definition
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   324
  "fv :: lam \<Rightarrow> atom set"
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   325
as
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   326
  "rfv"
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   327
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   328
lemma perm_rsp[quot_respect]:
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   329
  "(op = ===> alpha ===> alpha) permute permute"
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   330
  apply(auto)
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   331
  apply(rule alpha_eqvt)
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   332
  apply(simp)
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   333
  done
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   334
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   335
lemma rVar_rsp[quot_respect]:
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   336
  "(op = ===> alpha) rVar rVar"
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   337
  by (auto intro: a1)
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   338
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   339
lemma rApp_rsp[quot_respect]: 
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   340
  "(alpha ===> alpha ===> alpha) rApp rApp"
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   341
  by (auto intro: a2)
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   342
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   343
lemma rLam_rsp[quot_respect]: 
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   344
  "(op = ===> alpha ===> alpha) rLam rLam"
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   345
  apply(auto)
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   346
  apply(rule a3)
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   347
  apply(rule_tac x="0" in exI)
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   348
  unfolding fresh_star_def 
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   349
  apply(simp add: fresh_star_def fresh_zero_perm)
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   350
  apply(simp add: alpha_rfv)
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   351
  done
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   352
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   353
lemma rfv_rsp[quot_respect]: 
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   354
  "(alpha ===> op =) rfv rfv"
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   355
apply(simp add: alpha_rfv)
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   356
done
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   357
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   358
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   359
section {* lifted theorems *}
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   360
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   361
lemma lam_induct:
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   362
  "\<lbrakk>\<And>name. P (Var name);
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   363
    \<And>lam1 lam2. \<lbrakk>P lam1; P lam2\<rbrakk> \<Longrightarrow> P (App lam1 lam2);
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   364
    \<And>name lam. P lam \<Longrightarrow> P (Lam name lam)\<rbrakk> 
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   365
    \<Longrightarrow> P lam"
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   366
  apply (lifting rlam.induct)
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   367
  done
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   368
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   369
instantiation lam :: pt
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   370
begin
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   371
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   372
quotient_definition
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   373
  "permute_lam :: perm \<Rightarrow> lam \<Rightarrow> lam"
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   374
as
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   375
  "permute :: perm \<Rightarrow> rlam \<Rightarrow> rlam"
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   376
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   377
lemma permute_lam [simp]:
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   378
  shows "pi \<bullet> Var a = Var (pi \<bullet> a)"
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   379
  and   "pi \<bullet> App t1 t2 = App (pi \<bullet> t1) (pi \<bullet> t2)"
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   380
  and   "pi \<bullet> Lam a t = Lam (pi \<bullet> a) (pi \<bullet> t)"
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   381
apply(lifting permute_rlam.simps)
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   382
done
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   383
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   384
instance
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   385
apply default
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   386
apply(induct_tac [!] x rule: lam_induct)
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   387
apply(simp_all)
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   388
done
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   389
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   390
end
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   391
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   392
lemma fv_lam [simp]: 
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   393
  shows "fv (Var a) = {atom a}"
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   394
  and   "fv (App t1 t2) = fv t1 \<union> fv t2"
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   395
  and   "fv (Lam a t) = fv t - {atom a}"
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   396
apply(lifting rfv_var rfv_app rfv_lam)
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   397
done
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   398
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   399
lemma a1: 
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   400
  "a = b \<Longrightarrow> Var a = Var b"
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   401
  by  (lifting a1)
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   402
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   403
lemma a2: 
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   404
  "\<lbrakk>x = xa; xb = xc\<rbrakk> \<Longrightarrow> App x xb = App xa xc"
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   405
  by  (lifting a2)
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   406
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   407
lemma a3: 
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   408
  "\<lbrakk>\<exists>pi. (fv t - {atom a} = fv s - {atom b} \<and> (fv t - {atom a})\<sharp>* pi \<and> (pi \<bullet> t) = s \<and> (pi \<bullet> a) = b)\<rbrakk> 
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   409
   \<Longrightarrow> Lam a t = Lam b s"
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   410
  apply  (lifting a3)
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   411
  done
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   412
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   413
lemma alpha_cases: 
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   414
  "\<lbrakk>a1 = a2; \<And>a b. \<lbrakk>a1 = Var a; a2 = Var b; a = b\<rbrakk> \<Longrightarrow> P;
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   415
    \<And>x xa xb xc. \<lbrakk>a1 = App x xb; a2 = App xa xc; x = xa; xb = xc\<rbrakk> \<Longrightarrow> P;
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   416
    \<And>t a s b. \<lbrakk>a1 = Lam a t; a2 = Lam b s; 
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   417
         \<exists>pi. fv t - {atom a} = fv s - {atom b} \<and> (fv t - {atom a}) \<sharp>* pi \<and> (pi \<bullet> t) = s \<and> pi \<bullet> a = b\<rbrakk> 
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   418
   \<Longrightarrow> P\<rbrakk>
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   419
    \<Longrightarrow> P"
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   420
  by (lifting alpha.cases)
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   421
975
513ebe332964 test about supp/freshness for lam (old proofs work in principle - for single binders)
Christian Urban <urbanc@in.tum.de>
parents: 947
diff changeset
   422
(* not sure whether needed *)
947
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   423
lemma alpha_induct: 
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   424
  "\<lbrakk>qx = qxa; \<And>a b. a = b \<Longrightarrow> qxb (Var a) (Var b);
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   425
    \<And>x xa xb xc. \<lbrakk>x = xa; qxb x xa; xb = xc; qxb xb xc\<rbrakk> \<Longrightarrow> qxb (App x xb) (App xa xc);
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   426
     \<And>t a s b.
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   427
        \<lbrakk>\<exists>pi. fv t - {atom a} = fv s - {atom b} \<and>
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   428
         (fv t - {atom a}) \<sharp>* pi \<and> ((pi \<bullet> t) = s \<and> qxb (pi \<bullet> t) s) \<and> pi \<bullet> a = b\<rbrakk> 
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   429
     \<Longrightarrow> qxb (Lam a t) (Lam b s)\<rbrakk>
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   430
    \<Longrightarrow> qxb qx qxa"
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   431
  by (lifting alpha.induct)
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   432
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   433
(* should they lift automatically *)
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   434
lemma lam_inject [simp]: 
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   435
  shows "(Var a = Var b) = (a = b)"
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   436
  and   "(App t1 t2 = App s1 s2) = (t1 = s1 \<and> t2 = s2)"
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   437
apply(lifting rlam.inject(1) rlam.inject(2))
981
bc739536b715 Minor when looking at lam.distinct and lam.inject
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 975
diff changeset
   438
apply(regularize)
bc739536b715 Minor when looking at lam.distinct and lam.inject
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 975
diff changeset
   439
prefer 2
bc739536b715 Minor when looking at lam.distinct and lam.inject
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 975
diff changeset
   440
apply(regularize)
bc739536b715 Minor when looking at lam.distinct and lam.inject
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 975
diff changeset
   441
prefer 2
947
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   442
apply(auto)
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   443
apply(drule alpha.cases)
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   444
apply(simp_all)
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   445
apply(simp add: alpha.a1)
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   446
apply(drule alpha.cases)
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   447
apply(simp_all)
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   448
apply(drule alpha.cases)
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   449
apply(simp_all)
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   450
apply(rule alpha.a2)
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   451
apply(simp_all)
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   452
done
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   453
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   454
lemma rlam_distinct:
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   455
  shows "\<not>(rVar nam \<approx> rApp rlam1' rlam2')"
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   456
  and   "\<not>(rApp rlam1' rlam2' \<approx> rVar nam)"
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   457
  and   "\<not>(rVar nam \<approx> rLam nam' rlam')"
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   458
  and   "\<not>(rLam nam' rlam' \<approx> rVar nam)"
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   459
  and   "\<not>(rApp rlam1 rlam2 \<approx> rLam nam' rlam')"
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   460
  and   "\<not>(rLam nam' rlam' \<approx> rApp rlam1 rlam2)"
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   461
apply auto
981
bc739536b715 Minor when looking at lam.distinct and lam.inject
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 975
diff changeset
   462
apply (erule alpha.cases)
bc739536b715 Minor when looking at lam.distinct and lam.inject
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 975
diff changeset
   463
apply (simp_all only: rlam.distinct)
bc739536b715 Minor when looking at lam.distinct and lam.inject
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 975
diff changeset
   464
apply (erule alpha.cases)
bc739536b715 Minor when looking at lam.distinct and lam.inject
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 975
diff changeset
   465
apply (simp_all only: rlam.distinct)
bc739536b715 Minor when looking at lam.distinct and lam.inject
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 975
diff changeset
   466
apply (erule alpha.cases)
bc739536b715 Minor when looking at lam.distinct and lam.inject
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 975
diff changeset
   467
apply (simp_all only: rlam.distinct)
bc739536b715 Minor when looking at lam.distinct and lam.inject
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 975
diff changeset
   468
apply (erule alpha.cases)
bc739536b715 Minor when looking at lam.distinct and lam.inject
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 975
diff changeset
   469
apply (simp_all only: rlam.distinct)
bc739536b715 Minor when looking at lam.distinct and lam.inject
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 975
diff changeset
   470
apply (erule alpha.cases)
bc739536b715 Minor when looking at lam.distinct and lam.inject
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 975
diff changeset
   471
apply (simp_all only: rlam.distinct)
bc739536b715 Minor when looking at lam.distinct and lam.inject
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 975
diff changeset
   472
apply (erule alpha.cases)
bc739536b715 Minor when looking at lam.distinct and lam.inject
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 975
diff changeset
   473
apply (simp_all only: rlam.distinct)
947
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   474
done
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   475
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   476
lemma lam_distinct[simp]:
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   477
  shows "Var nam \<noteq> App lam1' lam2'"
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   478
  and   "App lam1' lam2' \<noteq> Var nam"
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   479
  and   "Var nam \<noteq> Lam nam' lam'"
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   480
  and   "Lam nam' lam' \<noteq> Var nam"
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   481
  and   "App lam1 lam2 \<noteq> Lam nam' lam'"
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   482
  and   "Lam nam' lam' \<noteq> App lam1 lam2"
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   483
apply(lifting rlam_distinct(1) rlam_distinct(2) rlam_distinct(3) rlam_distinct(4) rlam_distinct(5) rlam_distinct(6))
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   484
done
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   485
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   486
lemma var_supp1:
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   487
  shows "(supp (Var a)) = (supp a)"
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   488
  apply (simp add: supp_def)
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   489
  done
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   490
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   491
lemma var_supp:
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   492
  shows "(supp (Var a)) = {a:::name}"
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   493
  using var_supp1 by (simp add: supp_at_base)
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   494
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   495
lemma app_supp:
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   496
  shows "supp (App t1 t2) = (supp t1) \<union> (supp t2)"
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   497
apply(simp only: permute_lam supp_def lam_inject)
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   498
apply(simp add: Collect_imp_eq Collect_neg_eq)
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   499
done
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   500
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   501
(* needs thinking *)
975
513ebe332964 test about supp/freshness for lam (old proofs work in principle - for single binders)
Christian Urban <urbanc@in.tum.de>
parents: 947
diff changeset
   502
lemma lam_supp1:
513ebe332964 test about supp/freshness for lam (old proofs work in principle - for single binders)
Christian Urban <urbanc@in.tum.de>
parents: 947
diff changeset
   503
  shows "(supp (atom x, t)) supports (Lam x t) "
513ebe332964 test about supp/freshness for lam (old proofs work in principle - for single binders)
Christian Urban <urbanc@in.tum.de>
parents: 947
diff changeset
   504
apply(simp add: supports_def)
513ebe332964 test about supp/freshness for lam (old proofs work in principle - for single binders)
Christian Urban <urbanc@in.tum.de>
parents: 947
diff changeset
   505
apply(fold fresh_def)
513ebe332964 test about supp/freshness for lam (old proofs work in principle - for single binders)
Christian Urban <urbanc@in.tum.de>
parents: 947
diff changeset
   506
apply(simp add: fresh_Pair swap_fresh_fresh)
513ebe332964 test about supp/freshness for lam (old proofs work in principle - for single binders)
Christian Urban <urbanc@in.tum.de>
parents: 947
diff changeset
   507
apply(clarify)
513ebe332964 test about supp/freshness for lam (old proofs work in principle - for single binders)
Christian Urban <urbanc@in.tum.de>
parents: 947
diff changeset
   508
apply(subst swap_at_base_simps(3))
513ebe332964 test about supp/freshness for lam (old proofs work in principle - for single binders)
Christian Urban <urbanc@in.tum.de>
parents: 947
diff changeset
   509
apply(simp_all add: fresh_atom)
513ebe332964 test about supp/freshness for lam (old proofs work in principle - for single binders)
Christian Urban <urbanc@in.tum.de>
parents: 947
diff changeset
   510
done
947
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   511
975
513ebe332964 test about supp/freshness for lam (old proofs work in principle - for single binders)
Christian Urban <urbanc@in.tum.de>
parents: 947
diff changeset
   512
lemma lam_fsupp1:
513ebe332964 test about supp/freshness for lam (old proofs work in principle - for single binders)
Christian Urban <urbanc@in.tum.de>
parents: 947
diff changeset
   513
  assumes a: "finite (supp t)"
513ebe332964 test about supp/freshness for lam (old proofs work in principle - for single binders)
Christian Urban <urbanc@in.tum.de>
parents: 947
diff changeset
   514
  shows "finite (supp (Lam x t))"
513ebe332964 test about supp/freshness for lam (old proofs work in principle - for single binders)
Christian Urban <urbanc@in.tum.de>
parents: 947
diff changeset
   515
apply(rule supports_finite)
513ebe332964 test about supp/freshness for lam (old proofs work in principle - for single binders)
Christian Urban <urbanc@in.tum.de>
parents: 947
diff changeset
   516
apply(rule lam_supp1)
513ebe332964 test about supp/freshness for lam (old proofs work in principle - for single binders)
Christian Urban <urbanc@in.tum.de>
parents: 947
diff changeset
   517
apply(simp add: a supp_Pair supp_atom)
513ebe332964 test about supp/freshness for lam (old proofs work in principle - for single binders)
Christian Urban <urbanc@in.tum.de>
parents: 947
diff changeset
   518
done
947
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   519
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   520
instance lam :: fs
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   521
apply(default)
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   522
apply(induct_tac x rule: lam_induct)
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   523
apply(simp add: var_supp)
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   524
apply(simp add: app_supp)
975
513ebe332964 test about supp/freshness for lam (old proofs work in principle - for single binders)
Christian Urban <urbanc@in.tum.de>
parents: 947
diff changeset
   525
apply(simp add: lam_fsupp1)
947
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   526
done
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   527
975
513ebe332964 test about supp/freshness for lam (old proofs work in principle - for single binders)
Christian Urban <urbanc@in.tum.de>
parents: 947
diff changeset
   528
lemma lam_fresh1:
513ebe332964 test about supp/freshness for lam (old proofs work in principle - for single binders)
Christian Urban <urbanc@in.tum.de>
parents: 947
diff changeset
   529
  assumes f: "finite (supp t)"
513ebe332964 test about supp/freshness for lam (old proofs work in principle - for single binders)
Christian Urban <urbanc@in.tum.de>
parents: 947
diff changeset
   530
  and a1: "b \<sharp> t" 
513ebe332964 test about supp/freshness for lam (old proofs work in principle - for single binders)
Christian Urban <urbanc@in.tum.de>
parents: 947
diff changeset
   531
  and a2: "atom a \<noteq> b"
513ebe332964 test about supp/freshness for lam (old proofs work in principle - for single binders)
Christian Urban <urbanc@in.tum.de>
parents: 947
diff changeset
   532
  shows "b \<sharp> Lam a t"
513ebe332964 test about supp/freshness for lam (old proofs work in principle - for single binders)
Christian Urban <urbanc@in.tum.de>
parents: 947
diff changeset
   533
  proof -
513ebe332964 test about supp/freshness for lam (old proofs work in principle - for single binders)
Christian Urban <urbanc@in.tum.de>
parents: 947
diff changeset
   534
    have "\<exists>c. c \<sharp> (b, a ,t, Lam a t)" sorry
513ebe332964 test about supp/freshness for lam (old proofs work in principle - for single binders)
Christian Urban <urbanc@in.tum.de>
parents: 947
diff changeset
   535
    then obtain c where fr1: "c \<noteq> b"
513ebe332964 test about supp/freshness for lam (old proofs work in principle - for single binders)
Christian Urban <urbanc@in.tum.de>
parents: 947
diff changeset
   536
                  and   fr2: "c \<noteq> atom a"
513ebe332964 test about supp/freshness for lam (old proofs work in principle - for single binders)
Christian Urban <urbanc@in.tum.de>
parents: 947
diff changeset
   537
                  and   fr3: "c \<sharp> t"
513ebe332964 test about supp/freshness for lam (old proofs work in principle - for single binders)
Christian Urban <urbanc@in.tum.de>
parents: 947
diff changeset
   538
                  and   fr4: "c \<sharp> Lam a t"
513ebe332964 test about supp/freshness for lam (old proofs work in principle - for single binders)
Christian Urban <urbanc@in.tum.de>
parents: 947
diff changeset
   539
                  and   fr5: "sort_of b = sort_of c"  
513ebe332964 test about supp/freshness for lam (old proofs work in principle - for single binders)
Christian Urban <urbanc@in.tum.de>
parents: 947
diff changeset
   540
                  apply(auto simp add: fresh_Pair fresh_atom)
513ebe332964 test about supp/freshness for lam (old proofs work in principle - for single binders)
Christian Urban <urbanc@in.tum.de>
parents: 947
diff changeset
   541
                  sorry
513ebe332964 test about supp/freshness for lam (old proofs work in principle - for single binders)
Christian Urban <urbanc@in.tum.de>
parents: 947
diff changeset
   542
    have e: "(c \<rightleftharpoons> b) \<bullet> (Lam a t) = Lam a ((c \<rightleftharpoons> b) \<bullet> t)" using a2 fr1 fr2
513ebe332964 test about supp/freshness for lam (old proofs work in principle - for single binders)
Christian Urban <urbanc@in.tum.de>
parents: 947
diff changeset
   543
      by simp
513ebe332964 test about supp/freshness for lam (old proofs work in principle - for single binders)
Christian Urban <urbanc@in.tum.de>
parents: 947
diff changeset
   544
    from fr4 have "((c \<rightleftharpoons> b) \<bullet>c) \<sharp> ((c \<rightleftharpoons> b) \<bullet>(Lam a t))"
513ebe332964 test about supp/freshness for lam (old proofs work in principle - for single binders)
Christian Urban <urbanc@in.tum.de>
parents: 947
diff changeset
   545
      by (simp only: fresh_permute_iff)
513ebe332964 test about supp/freshness for lam (old proofs work in principle - for single binders)
Christian Urban <urbanc@in.tum.de>
parents: 947
diff changeset
   546
    then have "b \<sharp> (Lam a ((c \<rightleftharpoons> b) \<bullet> t))" using fr1 fr2 fr5 e
513ebe332964 test about supp/freshness for lam (old proofs work in principle - for single binders)
Christian Urban <urbanc@in.tum.de>
parents: 947
diff changeset
   547
      by simp
513ebe332964 test about supp/freshness for lam (old proofs work in principle - for single binders)
Christian Urban <urbanc@in.tum.de>
parents: 947
diff changeset
   548
    then show ?thesis using a1 fr3 
513ebe332964 test about supp/freshness for lam (old proofs work in principle - for single binders)
Christian Urban <urbanc@in.tum.de>
parents: 947
diff changeset
   549
      by (simp only: swap_fresh_fresh)
513ebe332964 test about supp/freshness for lam (old proofs work in principle - for single binders)
Christian Urban <urbanc@in.tum.de>
parents: 947
diff changeset
   550
qed
513ebe332964 test about supp/freshness for lam (old proofs work in principle - for single binders)
Christian Urban <urbanc@in.tum.de>
parents: 947
diff changeset
   551
513ebe332964 test about supp/freshness for lam (old proofs work in principle - for single binders)
Christian Urban <urbanc@in.tum.de>
parents: 947
diff changeset
   552
lemma lam_fresh2:
513ebe332964 test about supp/freshness for lam (old proofs work in principle - for single binders)
Christian Urban <urbanc@in.tum.de>
parents: 947
diff changeset
   553
  assumes f: "finite (supp t)"
513ebe332964 test about supp/freshness for lam (old proofs work in principle - for single binders)
Christian Urban <urbanc@in.tum.de>
parents: 947
diff changeset
   554
  shows "(atom a) \<sharp> Lam a t"
513ebe332964 test about supp/freshness for lam (old proofs work in principle - for single binders)
Christian Urban <urbanc@in.tum.de>
parents: 947
diff changeset
   555
sorry
513ebe332964 test about supp/freshness for lam (old proofs work in principle - for single binders)
Christian Urban <urbanc@in.tum.de>
parents: 947
diff changeset
   556
513ebe332964 test about supp/freshness for lam (old proofs work in principle - for single binders)
Christian Urban <urbanc@in.tum.de>
parents: 947
diff changeset
   557
513ebe332964 test about supp/freshness for lam (old proofs work in principle - for single binders)
Christian Urban <urbanc@in.tum.de>
parents: 947
diff changeset
   558
lemma lam_supp:
513ebe332964 test about supp/freshness for lam (old proofs work in principle - for single binders)
Christian Urban <urbanc@in.tum.de>
parents: 947
diff changeset
   559
  shows "supp (Lam x t) = ((supp t) - {atom x})"
513ebe332964 test about supp/freshness for lam (old proofs work in principle - for single binders)
Christian Urban <urbanc@in.tum.de>
parents: 947
diff changeset
   560
apply(default)
513ebe332964 test about supp/freshness for lam (old proofs work in principle - for single binders)
Christian Urban <urbanc@in.tum.de>
parents: 947
diff changeset
   561
apply(simp_all add: supp_conv_fresh)
513ebe332964 test about supp/freshness for lam (old proofs work in principle - for single binders)
Christian Urban <urbanc@in.tum.de>
parents: 947
diff changeset
   562
apply(auto)
513ebe332964 test about supp/freshness for lam (old proofs work in principle - for single binders)
Christian Urban <urbanc@in.tum.de>
parents: 947
diff changeset
   563
sorry
513ebe332964 test about supp/freshness for lam (old proofs work in principle - for single binders)
Christian Urban <urbanc@in.tum.de>
parents: 947
diff changeset
   564
947
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   565
lemma fresh_lam:
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   566
  "(atom a \<sharp> Lam b t) \<longleftrightarrow> (a = b) \<or> (a \<noteq> b \<and> atom a \<sharp> t)"
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   567
apply(simp add: fresh_def)
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   568
apply(simp add: lam_supp)
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   569
apply(auto)
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   570
done
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   571
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   572
lemma lam_induct_strong:
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   573
  fixes a::"'a::fs"
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   574
  assumes a1: "\<And>name b. P b (Var name)"
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   575
  and     a2: "\<And>lam1 lam2 b. \<lbrakk>\<And>c. P c lam1; \<And>c. P c lam2\<rbrakk> \<Longrightarrow> P b (App lam1 lam2)"
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   576
  and     a3: "\<And>name lam b. \<lbrakk>\<And>c. P c lam; (atom name) \<sharp> b\<rbrakk> \<Longrightarrow> P b (Lam name lam)"
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   577
  shows "P a lam"
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   578
proof -
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   579
  have "\<And>pi a. P a (pi \<bullet> lam)" 
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   580
  proof (induct lam rule: lam_induct)
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   581
    case (1 name pi)
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   582
    show "P a (pi \<bullet> Var name)"
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   583
      apply (simp)
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   584
      apply (rule a1)
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   585
      done
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   586
  next
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   587
    case (2 lam1 lam2 pi)
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   588
    have b1: "\<And>pi a. P a (pi \<bullet> lam1)" by fact
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   589
    have b2: "\<And>pi a. P a (pi \<bullet> lam2)" by fact
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   590
    show "P a (pi \<bullet> App lam1 lam2)"
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   591
      apply (simp)
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   592
      apply (rule a2)
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   593
      apply (rule b1)
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   594
      apply (rule b2)
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   595
      done
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   596
  next
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   597
    case (3 name lam pi a)
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   598
    have b: "\<And>pi a. P a (pi \<bullet> lam)" by fact
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   599
    obtain c::name where fr: "atom c\<sharp>(a, pi\<bullet>name, pi\<bullet>lam)"
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   600
      apply(rule obtain_atom)
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   601
      apply(auto)
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   602
      sorry
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   603
    from b fr have p: "P a (Lam c (((c \<leftrightarrow> (pi \<bullet> name)) + pi)\<bullet>lam))" 
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   604
      apply -
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   605
      apply(rule a3)
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   606
      apply(blast)
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   607
      apply(simp add: fresh_Pair)
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   608
      done
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   609
    have eq: "(atom c \<rightleftharpoons> atom (pi\<bullet>name)) \<bullet> Lam (pi \<bullet> name) (pi \<bullet> lam) = Lam (pi \<bullet> name) (pi \<bullet> lam)"
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   610
      apply(rule swap_fresh_fresh)
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   611
      using fr
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   612
      apply(simp add: fresh_lam fresh_Pair)
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   613
      apply(simp add: fresh_lam fresh_Pair)
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   614
      done
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   615
    show "P a (pi \<bullet> Lam name lam)" 
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   616
      apply (simp)
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   617
      apply(subst eq[symmetric])
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   618
      using p
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   619
      apply(simp only: permute_lam)
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   620
      apply(simp add: flip_def)
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   621
      done
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   622
  qed
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   623
  then have "P a (0 \<bullet> lam)" by blast
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   624
  then show "P a lam" by simp 
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   625
qed
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   626
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   627
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   628
lemma var_fresh:
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   629
  fixes a::"name"
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   630
  shows "(atom a \<sharp> (Var b)) = (atom a \<sharp> b)"
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   631
  apply(simp add: fresh_def)
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   632
  apply(simp add: var_supp1)
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   633
  done
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   634
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   635
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   636
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   637
end
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   638