Mercurial Mercurial > hg > nominal2 / annotate
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Quot/Nominal/LamEx.thy
author Cezary Kaliszyk <kaliszyk@in.tum.de>
Thu, 11 Feb 2010 14:00:00 +0100 (2010-02-11)
changeset 1129 9a86f0ef6503
parent 1128 17ca92ab4660
child 1139 c4001cda9da3
permissions -rw-r--r--
Notation available locally
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
1129
9a86f0ef6503 Notation available locally
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1128
diff changeset 
     2
 
imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "Abs"
947
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


atom_decl name













fa810f01f7b5
added an LamEx example together with the new nominal infrastructure



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




     6














fa810f01f7b5
added an LamEx example together with the new nominal infrastructure



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




     7


datatype rlam =













fa810f01f7b5
added an LamEx example together with the new nominal infrastructure



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




     8


  rVar "name"













fa810f01f7b5
added an LamEx example together with the new nominal infrastructure



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




     9


| rApp "rlam" "rlam"













fa810f01f7b5
added an LamEx example together with the new nominal infrastructure



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




    10


| rLam "name" "rlam"













fa810f01f7b5
added an LamEx example together with the new nominal infrastructure



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




    11














fa810f01f7b5
added an LamEx example together with the new nominal infrastructure



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




    12


fun













fa810f01f7b5
added an LamEx example together with the new nominal infrastructure



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




    13


  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




    14


where













fa810f01f7b5
added an LamEx example together with the new nominal infrastructure



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




    15


  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




    16


| 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




    17


| 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




    18














fa810f01f7b5
added an LamEx example together with the new nominal infrastructure



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




    19


instantiation rlam :: pt













fa810f01f7b5
added an LamEx example together with the new nominal infrastructure



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




    20


begin













fa810f01f7b5
added an LamEx example together with the new nominal infrastructure



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




    21














fa810f01f7b5
added an LamEx example together with the new nominal infrastructure



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




    22


primrec













fa810f01f7b5
added an LamEx example together with the new nominal infrastructure



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




    23


  permute_rlam













fa810f01f7b5
added an LamEx example together with the new nominal infrastructure



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




    24


where













fa810f01f7b5
added an LamEx example together with the new nominal infrastructure



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




    25


  "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




    26


| "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




    27


| "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




    28














fa810f01f7b5
added an LamEx example together with the new nominal infrastructure



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




    29


instance













fa810f01f7b5
added an LamEx example together with the new nominal infrastructure



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




    30


apply default













fa810f01f7b5
added an LamEx example together with the new nominal infrastructure



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




    31


apply(induct_tac [!] x)













fa810f01f7b5
added an LamEx example together with the new nominal infrastructure



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




    32


apply(simp_all)













fa810f01f7b5
added an LamEx example together with the new nominal infrastructure



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




    33


done













fa810f01f7b5
added an LamEx example together with the new nominal infrastructure



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




    34














fa810f01f7b5
added an LamEx example together with the new nominal infrastructure



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




    35


end













fa810f01f7b5
added an LamEx example together with the new nominal infrastructure



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




    36














fa810f01f7b5
added an LamEx example together with the new nominal infrastructure



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




    37


instantiation rlam :: fs













fa810f01f7b5
added an LamEx example together with the new nominal infrastructure



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




    38


begin













fa810f01f7b5
added an LamEx example together with the new nominal infrastructure



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




    39














fa810f01f7b5
added an LamEx example together with the new nominal infrastructure



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




    40


lemma neg_conj:













fa810f01f7b5
added an LamEx example together with the new nominal infrastructure



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




    41


  "\<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




    42


  by simp













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 infinite_Un:













fa810f01f7b5
added an LamEx example together with the new nominal infrastructure



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




    45


  "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




    46


  by simp













fa810f01f7b5
added an LamEx example together with the new nominal infrastructure



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




    47














fa810f01f7b5
added an LamEx example together with the new nominal infrastructure



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




    48


instance













fa810f01f7b5
added an LamEx example together with the new nominal infrastructure



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




    49


apply default













fa810f01f7b5
added an LamEx example together with the new nominal infrastructure



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




    50


apply(induct_tac x)













fa810f01f7b5
added an LamEx example together with the new nominal infrastructure



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




    51


(* var case *)













fa810f01f7b5
added an LamEx example together with the new nominal infrastructure



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




    52


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




    53


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




    54


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




    55


(* app case *)













fa810f01f7b5
added an LamEx example together with the new nominal infrastructure



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




    56


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




    57


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




    58


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




    59


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




    60


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




    61


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




    62


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




    63


apply(simp)













fa810f01f7b5
added an LamEx example together with the new nominal infrastructure



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




    64


(* lam case *)













fa810f01f7b5
added an LamEx example together with the new nominal infrastructure



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




    65


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




    66


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




    67


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




    68


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




    69


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




    70


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




    71


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




    72


apply(simp)













fa810f01f7b5
added an LamEx example together with the new nominal infrastructure



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




    73


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




    74


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




    75


done













fa810f01f7b5
added an LamEx example together with the new nominal infrastructure



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




    76














fa810f01f7b5
added an LamEx example together with the new nominal infrastructure



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




    77


end













fa810f01f7b5
added an LamEx example together with the new nominal infrastructure



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




    78














fa810f01f7b5
added an LamEx example together with the new nominal infrastructure



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




    79














fa810f01f7b5
added an LamEx example together with the new nominal infrastructure



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




    80


(* 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




    81


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




    82














fa810f01f7b5
added an LamEx example together with the new nominal infrastructure



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




    83


lemma rfv_eqvt[eqvt]:













fa810f01f7b5
added an LamEx example together with the new nominal infrastructure



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




    84


  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




    85


apply(induct t)













fa810f01f7b5
added an LamEx example together with the new nominal infrastructure



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




    86


apply(simp_all)













fa810f01f7b5
added an LamEx example together with the new nominal infrastructure



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




    87


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




    88


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




    89


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




    90


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




    91


done













fa810f01f7b5
added an LamEx example together with the new nominal infrastructure



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




    92














fa810f01f7b5
added an LamEx example together with the new nominal infrastructure



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




    93


inductive













fa810f01f7b5
added an LamEx example together with the new nominal infrastructure



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




    94


    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




    95


where













fa810f01f7b5
added an LamEx example together with the new nominal infrastructure



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




    96


  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




    97


| a2: "\<lbrakk>t1 \<approx> t2; s1 \<approx> s2\<rbrakk> \<Longrightarrow> rApp t1 s1 \<approx> rApp t2 s2"








1011






1dd314a00b0c
Fixed wrong rename.



Cezary Kaliszyk <kaliszyk@in.tum.de>


parents: 
1009

diff
changeset




    98


| a3: "\<exists>pi. (rfv t - {atom a} = rfv s - {atom b} \<and> (rfv t - {atom a})\<sharp>* pi \<and> (pi \<bullet> t) \<approx> s)













1dd314a00b0c
Fixed wrong rename.



Cezary Kaliszyk <kaliszyk@in.tum.de>


parents: 
1009

diff
changeset




    99


       \<Longrightarrow> rLam a t \<approx> rLam b s"








947






fa810f01f7b5
added an LamEx example together with the new nominal infrastructure



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




   100









989






af02b193a19a
the supp of a lambda can now be characterised, *provided* the notion of free variables coincides with support on lambda terms



Christian Urban <urbanc@in.tum.de>


parents: 
984

diff
changeset




   101


lemma a3_inverse:













af02b193a19a
the supp of a lambda can now be characterised, *provided* the notion of free variables coincides with support on lambda terms



Christian Urban <urbanc@in.tum.de>


parents: 
984

diff
changeset




   102


  assumes "rLam a t \<approx> rLam b s"








1011






1dd314a00b0c
Fixed wrong rename.



Cezary Kaliszyk <kaliszyk@in.tum.de>


parents: 
1009

diff
changeset




   103


  shows "\<exists>pi. (rfv t - {atom a} = rfv s - {atom b} \<and> (rfv t - {atom a})\<sharp>* pi \<and> (pi \<bullet> t) \<approx> s)"








989






af02b193a19a
the supp of a lambda can now be characterised, *provided* the notion of free variables coincides with support on lambda terms



Christian Urban <urbanc@in.tum.de>


parents: 
984

diff
changeset




   104


using assms













af02b193a19a
the supp of a lambda can now be characterised, *provided* the notion of free variables coincides with support on lambda terms



Christian Urban <urbanc@in.tum.de>


parents: 
984

diff
changeset




   105


apply(erule_tac alpha.cases)













af02b193a19a
the supp of a lambda can now be characterised, *provided* the notion of free variables coincides with support on lambda terms



Christian Urban <urbanc@in.tum.de>


parents: 
984

diff
changeset




   106


apply(auto)













af02b193a19a
the supp of a lambda can now be characterised, *provided* the notion of free variables coincides with support on lambda terms



Christian Urban <urbanc@in.tum.de>


parents: 
984

diff
changeset




   107


done













af02b193a19a
the supp of a lambda can now be characterised, *provided* the notion of free variables coincides with support on lambda terms



Christian Urban <urbanc@in.tum.de>


parents: 
984

diff
changeset




   108









947






fa810f01f7b5
added an LamEx example together with the new nominal infrastructure



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




   109


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




   110


lemma alpha_eqvt:













fa810f01f7b5
added an LamEx example together with the new nominal infrastructure



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




   111


  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




   112


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




   113


apply(simp add: a1)













fa810f01f7b5
added an LamEx example together with the new nominal infrastructure



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




   114


apply(simp add: a2)













fa810f01f7b5
added an LamEx example together with the new nominal infrastructure



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




   115


apply(simp)













fa810f01f7b5
added an LamEx example together with the new nominal infrastructure



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




   116


apply(rule a3)








1011






1dd314a00b0c
Fixed wrong rename.



Cezary Kaliszyk <kaliszyk@in.tum.de>


parents: 
1009

diff
changeset




   117


apply(erule conjE)








947






fa810f01f7b5
added an LamEx example together with the new nominal infrastructure



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




   118


apply(erule exE)








1011






1dd314a00b0c
Fixed wrong rename.



Cezary Kaliszyk <kaliszyk@in.tum.de>


parents: 
1009

diff
changeset




   119


apply(erule conjE)








947






fa810f01f7b5
added an LamEx example together with the new nominal infrastructure



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




   120


apply(rule_tac x="pi \<bullet> pia" in exI)








1011






1dd314a00b0c
Fixed wrong rename.



Cezary Kaliszyk <kaliszyk@in.tum.de>


parents: 
1009

diff
changeset




   121


apply(rule conjI)








947






fa810f01f7b5
added an LamEx example together with the new nominal infrastructure



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




   122


apply(rule_tac ?p1="- pi" in permute_eq_iff[THEN iffD1])








1087






bb7f4457091a
moved some lemmas to Nominal; updated all files



Christian Urban <urbanc@in.tum.de>


parents: 
1028

diff
changeset




   123


apply(simp only: Diff_eqvt rfv_eqvt insert_eqvt atom_eqvt empty_eqvt)













bb7f4457091a
moved some lemmas to Nominal; updated all files



Christian Urban <urbanc@in.tum.de>


parents: 
1028

diff
changeset




   124


apply(simp)








947






fa810f01f7b5
added an LamEx example together with the new nominal infrastructure



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




   125


apply(rule conjI)













fa810f01f7b5
added an LamEx example together with the new nominal infrastructure



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




   126


apply(rule_tac ?p1="- pi" in fresh_star_permute_iff[THEN iffD1])








1087






bb7f4457091a
moved some lemmas to Nominal; updated all files



Christian Urban <urbanc@in.tum.de>


parents: 
1028

diff
changeset




   127


apply(simp add: Diff_eqvt rfv_eqvt atom_eqvt insert_eqvt empty_eqvt)








947






fa810f01f7b5
added an LamEx example together with the new nominal infrastructure



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




   128


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




   129


apply(simp)













fa810f01f7b5
added an LamEx example together with the new nominal infrastructure



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




   130


done













fa810f01f7b5
added an LamEx example together with the new nominal infrastructure



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




   131














fa810f01f7b5
added an LamEx example together with the new nominal infrastructure



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




   132


lemma alpha_refl:













fa810f01f7b5
added an LamEx example together with the new nominal infrastructure



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




   133


  shows "t \<approx> t"













fa810f01f7b5
added an LamEx example together with the new nominal infrastructure



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




   134


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




   135


apply(simp add: a1)













fa810f01f7b5
added an LamEx example together with the new nominal infrastructure



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




   136


apply(simp add: a2)













fa810f01f7b5
added an LamEx example together with the new nominal infrastructure



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




   137


apply(rule a3)













fa810f01f7b5
added an LamEx example together with the new nominal infrastructure



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




   138


apply(rule_tac x="0" in exI)








1011






1dd314a00b0c
Fixed wrong rename.



Cezary Kaliszyk <kaliszyk@in.tum.de>


parents: 
1009

diff
changeset




   139


apply(simp_all add: fresh_star_def fresh_zero_perm)








947






fa810f01f7b5
added an LamEx example together with the new nominal infrastructure



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




   140


done













fa810f01f7b5
added an LamEx example together with the new nominal infrastructure



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




   141














fa810f01f7b5
added an LamEx example together with the new nominal infrastructure



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




   142


lemma alpha_sym:













fa810f01f7b5
added an LamEx example together with the new nominal infrastructure



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




   143


  shows "t \<approx> s \<Longrightarrow> s \<approx> t"








1011






1dd314a00b0c
Fixed wrong rename.



Cezary Kaliszyk <kaliszyk@in.tum.de>


parents: 
1009

diff
changeset




   144


apply(induct rule: alpha.induct)













1dd314a00b0c
Fixed wrong rename.



Cezary Kaliszyk <kaliszyk@in.tum.de>


parents: 
1009

diff
changeset




   145


apply(simp add: a1)













1dd314a00b0c
Fixed wrong rename.



Cezary Kaliszyk <kaliszyk@in.tum.de>


parents: 
1009

diff
changeset




   146


apply(simp add: a2)













1dd314a00b0c
Fixed wrong rename.



Cezary Kaliszyk <kaliszyk@in.tum.de>


parents: 
1009

diff
changeset




   147


apply(rule a3)













1dd314a00b0c
Fixed wrong rename.



Cezary Kaliszyk <kaliszyk@in.tum.de>


parents: 
1009

diff
changeset




   148


apply(erule exE)













1dd314a00b0c
Fixed wrong rename.



Cezary Kaliszyk <kaliszyk@in.tum.de>


parents: 
1009

diff
changeset




   149


apply(rule_tac x="- pi" in exI)













1dd314a00b0c
Fixed wrong rename.



Cezary Kaliszyk <kaliszyk@in.tum.de>


parents: 
1009

diff
changeset




   150


apply(simp)













1dd314a00b0c
Fixed wrong rename.



Cezary Kaliszyk <kaliszyk@in.tum.de>


parents: 
1009

diff
changeset




   151


apply(simp add: fresh_star_def fresh_minus_perm)













1dd314a00b0c
Fixed wrong rename.



Cezary Kaliszyk <kaliszyk@in.tum.de>


parents: 
1009

diff
changeset




   152


apply(erule conjE)+













1dd314a00b0c
Fixed wrong rename.



Cezary Kaliszyk <kaliszyk@in.tum.de>


parents: 
1009

diff
changeset




   153


apply(rotate_tac 3)













1dd314a00b0c
Fixed wrong rename.



Cezary Kaliszyk <kaliszyk@in.tum.de>


parents: 
1009

diff
changeset




   154


apply(drule_tac pi="- pi" in alpha_eqvt)













1dd314a00b0c
Fixed wrong rename.



Cezary Kaliszyk <kaliszyk@in.tum.de>


parents: 
1009

diff
changeset




   155


apply(simp)













1dd314a00b0c
Fixed wrong rename.



Cezary Kaliszyk <kaliszyk@in.tum.de>


parents: 
1009

diff
changeset




   156


done








947






fa810f01f7b5
added an LamEx example together with the new nominal infrastructure



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




   157














fa810f01f7b5
added an LamEx example together with the new nominal infrastructure



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




   158


lemma alpha_trans:













fa810f01f7b5
added an LamEx example together with the new nominal infrastructure



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




   159


  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




   160


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




   161


apply(erule alpha.cases)













fa810f01f7b5
added an LamEx example together with the new nominal infrastructure



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




   162


apply(simp_all)













fa810f01f7b5
added an LamEx example together with the new nominal infrastructure



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




   163


apply(simp add: a1)













fa810f01f7b5
added an LamEx example together with the new nominal infrastructure



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




   164


apply(rotate_tac 4)













fa810f01f7b5
added an LamEx example together with the new nominal infrastructure



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




   165


apply(erule alpha.cases)













fa810f01f7b5
added an LamEx example together with the new nominal infrastructure



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




   166


apply(simp_all)













fa810f01f7b5
added an LamEx example together with the new nominal infrastructure



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




   167


apply(simp add: a2)













fa810f01f7b5
added an LamEx example together with the new nominal infrastructure



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




   168


apply(rotate_tac 1)













fa810f01f7b5
added an LamEx example together with the new nominal infrastructure



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




   169


apply(erule alpha.cases)













fa810f01f7b5
added an LamEx example together with the new nominal infrastructure



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




   170


apply(simp_all)













fa810f01f7b5
added an LamEx example together with the new nominal infrastructure



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




   171


apply(erule conjE)+













fa810f01f7b5
added an LamEx example together with the new nominal infrastructure



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




   172


apply(erule exE)+













fa810f01f7b5
added an LamEx example together with the new nominal infrastructure



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




   173


apply(erule conjE)+













fa810f01f7b5
added an LamEx example together with the new nominal infrastructure



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




   174


apply(rule a3)













fa810f01f7b5
added an LamEx example together with the new nominal infrastructure



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




   175


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




   176


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




   177


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




   178


apply(drule mp)








989






af02b193a19a
the supp of a lambda can now be characterised, *provided* the notion of free variables coincides with support on lambda terms



Christian Urban <urbanc@in.tum.de>


parents: 
984

diff
changeset




   179


apply(rotate_tac 7)








947






fa810f01f7b5
added an LamEx example together with the new nominal infrastructure



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




   180


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




   181


apply(simp)








989






af02b193a19a
the supp of a lambda can now be characterised, *provided* the notion of free variables coincides with support on lambda terms



Christian Urban <urbanc@in.tum.de>


parents: 
984

diff
changeset




   182


apply(rotate_tac 9)








947






fa810f01f7b5
added an LamEx example together with the new nominal infrastructure



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




   183


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




   184


apply(simp)













fa810f01f7b5
added an LamEx example together with the new nominal infrastructure



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




   185


done













fa810f01f7b5
added an LamEx example together with the new nominal infrastructure



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




   186














fa810f01f7b5
added an LamEx example together with the new nominal infrastructure



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




   187


lemma alpha_equivp:













fa810f01f7b5
added an LamEx example together with the new nominal infrastructure



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




   188


  shows "equivp alpha"








981






bc739536b715
Minor when looking at lam.distinct and lam.inject



Cezary Kaliszyk <kaliszyk@in.tum.de>


parents: 
975

diff
changeset




   189


  apply(rule equivpI)













bc739536b715
Minor when looking at lam.distinct and lam.inject



Cezary Kaliszyk <kaliszyk@in.tum.de>


parents: 
975

diff
changeset




   190


  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




   191


  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




   192


  done








947






fa810f01f7b5
added an LamEx example together with the new nominal infrastructure



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




   193














fa810f01f7b5
added an LamEx example together with the new nominal infrastructure



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




   194


lemma alpha_rfv:













fa810f01f7b5
added an LamEx example together with the new nominal infrastructure



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




   195


  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




   196


  apply(induct rule: alpha.induct)








1011






1dd314a00b0c
Fixed wrong rename.



Cezary Kaliszyk <kaliszyk@in.tum.de>


parents: 
1009

diff
changeset




   197


  apply(simp_all)








981






bc739536b715
Minor when looking at lam.distinct and lam.inject



Cezary Kaliszyk <kaliszyk@in.tum.de>


parents: 
975

diff
changeset




   198


  done








947






fa810f01f7b5
added an LamEx example together with the new nominal infrastructure



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




   199









1011






1dd314a00b0c
Fixed wrong rename.



Cezary Kaliszyk <kaliszyk@in.tum.de>


parents: 
1009

diff
changeset




   200


inductive













1dd314a00b0c
Fixed wrong rename.



Cezary Kaliszyk <kaliszyk@in.tum.de>


parents: 
1009

diff
changeset




   201


    alpha2 :: "rlam \<Rightarrow> rlam \<Rightarrow> bool" ("_ \<approx>2 _" [100, 100] 100)













1dd314a00b0c
Fixed wrong rename.



Cezary Kaliszyk <kaliszyk@in.tum.de>


parents: 
1009

diff
changeset




   202


where













1dd314a00b0c
Fixed wrong rename.



Cezary Kaliszyk <kaliszyk@in.tum.de>


parents: 
1009

diff
changeset




   203


  a21: "a = b \<Longrightarrow> (rVar a) \<approx>2 (rVar b)"













1dd314a00b0c
Fixed wrong rename.



Cezary Kaliszyk <kaliszyk@in.tum.de>


parents: 
1009

diff
changeset




   204


| a22: "\<lbrakk>t1 \<approx>2 t2; s1 \<approx>2 s2\<rbrakk> \<Longrightarrow> rApp t1 s1 \<approx>2 rApp t2 s2"













1dd314a00b0c
Fixed wrong rename.



Cezary Kaliszyk <kaliszyk@in.tum.de>


parents: 
1009

diff
changeset




   205


| a23: "(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"













1dd314a00b0c
Fixed wrong rename.



Cezary Kaliszyk <kaliszyk@in.tum.de>


parents: 
1009

diff
changeset




   206














1dd314a00b0c
Fixed wrong rename.



Cezary Kaliszyk <kaliszyk@in.tum.de>


parents: 
1009

diff
changeset




   207


lemma fv_vars:













1dd314a00b0c
Fixed wrong rename.



Cezary Kaliszyk <kaliszyk@in.tum.de>


parents: 
1009

diff
changeset




   208


  fixes a::name













1dd314a00b0c
Fixed wrong rename.



Cezary Kaliszyk <kaliszyk@in.tum.de>


parents: 
1009

diff
changeset




   209


  assumes a1: "\<forall>x \<in> rfv t - {atom a}. pi \<bullet> x = x"













1dd314a00b0c
Fixed wrong rename.



Cezary Kaliszyk <kaliszyk@in.tum.de>


parents: 
1009

diff
changeset




   210


  shows "(pi \<bullet> t) \<approx>2 ((a \<leftrightarrow> (pi \<bullet> a)) \<bullet> t)"













1dd314a00b0c
Fixed wrong rename.



Cezary Kaliszyk <kaliszyk@in.tum.de>


parents: 
1009

diff
changeset




   211


using a1













1dd314a00b0c
Fixed wrong rename.



Cezary Kaliszyk <kaliszyk@in.tum.de>


parents: 
1009

diff
changeset




   212


apply(induct t)













1dd314a00b0c
Fixed wrong rename.



Cezary Kaliszyk <kaliszyk@in.tum.de>


parents: 
1009

diff
changeset




   213


apply(auto)













1dd314a00b0c
Fixed wrong rename.



Cezary Kaliszyk <kaliszyk@in.tum.de>


parents: 
1009

diff
changeset




   214


apply(rule a21)













1dd314a00b0c
Fixed wrong rename.



Cezary Kaliszyk <kaliszyk@in.tum.de>


parents: 
1009

diff
changeset




   215


apply(case_tac "name = a")













1dd314a00b0c
Fixed wrong rename.



Cezary Kaliszyk <kaliszyk@in.tum.de>


parents: 
1009

diff
changeset




   216


apply(simp)













1dd314a00b0c
Fixed wrong rename.



Cezary Kaliszyk <kaliszyk@in.tum.de>


parents: 
1009

diff
changeset




   217


apply(simp)













1dd314a00b0c
Fixed wrong rename.



Cezary Kaliszyk <kaliszyk@in.tum.de>


parents: 
1009

diff
changeset




   218


defer













1dd314a00b0c
Fixed wrong rename.



Cezary Kaliszyk <kaliszyk@in.tum.de>


parents: 
1009

diff
changeset




   219


apply(rule a22)













1dd314a00b0c
Fixed wrong rename.



Cezary Kaliszyk <kaliszyk@in.tum.de>


parents: 
1009

diff
changeset




   220


apply(simp)













1dd314a00b0c
Fixed wrong rename.



Cezary Kaliszyk <kaliszyk@in.tum.de>


parents: 
1009

diff
changeset




   221


apply(simp)













1dd314a00b0c
Fixed wrong rename.



Cezary Kaliszyk <kaliszyk@in.tum.de>


parents: 
1009

diff
changeset




   222


apply(rule a23)













1dd314a00b0c
Fixed wrong rename.



Cezary Kaliszyk <kaliszyk@in.tum.de>


parents: 
1009

diff
changeset




   223


apply(case_tac "a = name")













1dd314a00b0c
Fixed wrong rename.



Cezary Kaliszyk <kaliszyk@in.tum.de>


parents: 
1009

diff
changeset




   224


apply(simp)













1dd314a00b0c
Fixed wrong rename.



Cezary Kaliszyk <kaliszyk@in.tum.de>


parents: 
1009

diff
changeset




   225


oops













1dd314a00b0c
Fixed wrong rename.



Cezary Kaliszyk <kaliszyk@in.tum.de>


parents: 
1009

diff
changeset




   226














1dd314a00b0c
Fixed wrong rename.



Cezary Kaliszyk <kaliszyk@in.tum.de>


parents: 
1009

diff
changeset




   227














1dd314a00b0c
Fixed wrong rename.



Cezary Kaliszyk <kaliszyk@in.tum.de>


parents: 
1009

diff
changeset




   228


lemma 













1dd314a00b0c
Fixed wrong rename.



Cezary Kaliszyk <kaliszyk@in.tum.de>


parents: 
1009

diff
changeset




   229


  assumes a1: "t \<approx>2 s"













1dd314a00b0c
Fixed wrong rename.



Cezary Kaliszyk <kaliszyk@in.tum.de>


parents: 
1009

diff
changeset




   230


  shows "t \<approx> s"













1dd314a00b0c
Fixed wrong rename.



Cezary Kaliszyk <kaliszyk@in.tum.de>


parents: 
1009

diff
changeset




   231


using a1













1dd314a00b0c
Fixed wrong rename.



Cezary Kaliszyk <kaliszyk@in.tum.de>


parents: 
1009

diff
changeset




   232


apply(induct)













1dd314a00b0c
Fixed wrong rename.



Cezary Kaliszyk <kaliszyk@in.tum.de>


parents: 
1009

diff
changeset




   233


apply(rule alpha.intros)













1dd314a00b0c
Fixed wrong rename.



Cezary Kaliszyk <kaliszyk@in.tum.de>


parents: 
1009

diff
changeset




   234


apply(simp)













1dd314a00b0c
Fixed wrong rename.



Cezary Kaliszyk <kaliszyk@in.tum.de>


parents: 
1009

diff
changeset




   235


apply(rule alpha.intros)













1dd314a00b0c
Fixed wrong rename.



Cezary Kaliszyk <kaliszyk@in.tum.de>


parents: 
1009

diff
changeset




   236


apply(simp)













1dd314a00b0c
Fixed wrong rename.



Cezary Kaliszyk <kaliszyk@in.tum.de>


parents: 
1009

diff
changeset




   237


apply(simp)













1dd314a00b0c
Fixed wrong rename.



Cezary Kaliszyk <kaliszyk@in.tum.de>


parents: 
1009

diff
changeset




   238


apply(rule alpha.intros)













1dd314a00b0c
Fixed wrong rename.



Cezary Kaliszyk <kaliszyk@in.tum.de>


parents: 
1009

diff
changeset




   239


apply(erule disjE)













1dd314a00b0c
Fixed wrong rename.



Cezary Kaliszyk <kaliszyk@in.tum.de>


parents: 
1009

diff
changeset




   240


apply(rule_tac x="0" in exI)













1dd314a00b0c
Fixed wrong rename.



Cezary Kaliszyk <kaliszyk@in.tum.de>


parents: 
1009

diff
changeset




   241


apply(simp add: fresh_star_def fresh_zero_perm)













1dd314a00b0c
Fixed wrong rename.



Cezary Kaliszyk <kaliszyk@in.tum.de>


parents: 
1009

diff
changeset




   242


apply(erule conjE)+













1dd314a00b0c
Fixed wrong rename.



Cezary Kaliszyk <kaliszyk@in.tum.de>


parents: 
1009

diff
changeset




   243


apply(drule alpha_rfv)













1dd314a00b0c
Fixed wrong rename.



Cezary Kaliszyk <kaliszyk@in.tum.de>


parents: 
1009

diff
changeset




   244


apply(simp)













1dd314a00b0c
Fixed wrong rename.



Cezary Kaliszyk <kaliszyk@in.tum.de>


parents: 
1009

diff
changeset




   245


apply(rule_tac x="(a \<leftrightarrow> b)" in exI)













1dd314a00b0c
Fixed wrong rename.



Cezary Kaliszyk <kaliszyk@in.tum.de>


parents: 
1009

diff
changeset




   246


apply(simp)













1dd314a00b0c
Fixed wrong rename.



Cezary Kaliszyk <kaliszyk@in.tum.de>


parents: 
1009

diff
changeset




   247


apply(erule conjE)+













1dd314a00b0c
Fixed wrong rename.



Cezary Kaliszyk <kaliszyk@in.tum.de>


parents: 
1009

diff
changeset




   248


apply(rule conjI)













1dd314a00b0c
Fixed wrong rename.



Cezary Kaliszyk <kaliszyk@in.tum.de>


parents: 
1009

diff
changeset




   249


apply(drule alpha_rfv)













1dd314a00b0c
Fixed wrong rename.



Cezary Kaliszyk <kaliszyk@in.tum.de>


parents: 
1009

diff
changeset




   250


apply(drule sym)













1dd314a00b0c
Fixed wrong rename.



Cezary Kaliszyk <kaliszyk@in.tum.de>


parents: 
1009

diff
changeset




   251


apply(simp)













1dd314a00b0c
Fixed wrong rename.



Cezary Kaliszyk <kaliszyk@in.tum.de>


parents: 
1009

diff
changeset




   252


apply(simp add: rfv_eqvt[symmetric])













1dd314a00b0c
Fixed wrong rename.



Cezary Kaliszyk <kaliszyk@in.tum.de>


parents: 
1009

diff
changeset




   253


defer













1dd314a00b0c
Fixed wrong rename.



Cezary Kaliszyk <kaliszyk@in.tum.de>


parents: 
1009

diff
changeset




   254


apply(subgoal_tac "atom a \<sharp> (rfv t - {atom a})")













1dd314a00b0c
Fixed wrong rename.



Cezary Kaliszyk <kaliszyk@in.tum.de>


parents: 
1009

diff
changeset




   255


apply(subgoal_tac "atom b \<sharp> (rfv t - {atom a})")













1dd314a00b0c
Fixed wrong rename.



Cezary Kaliszyk <kaliszyk@in.tum.de>


parents: 
1009

diff
changeset




   256














1dd314a00b0c
Fixed wrong rename.



Cezary Kaliszyk <kaliszyk@in.tum.de>


parents: 
1009

diff
changeset




   257


defer













1dd314a00b0c
Fixed wrong rename.



Cezary Kaliszyk <kaliszyk@in.tum.de>


parents: 
1009

diff
changeset




   258


sorry













1dd314a00b0c
Fixed wrong rename.



Cezary Kaliszyk <kaliszyk@in.tum.de>


parents: 
1009

diff
changeset




   259














1dd314a00b0c
Fixed wrong rename.



Cezary Kaliszyk <kaliszyk@in.tum.de>


parents: 
1009

diff
changeset




   260


lemma 













1dd314a00b0c
Fixed wrong rename.



Cezary Kaliszyk <kaliszyk@in.tum.de>


parents: 
1009

diff
changeset




   261


  assumes a1: "t \<approx> s"













1dd314a00b0c
Fixed wrong rename.



Cezary Kaliszyk <kaliszyk@in.tum.de>


parents: 
1009

diff
changeset




   262


  shows "t \<approx>2 s"













1dd314a00b0c
Fixed wrong rename.



Cezary Kaliszyk <kaliszyk@in.tum.de>


parents: 
1009

diff
changeset




   263


using a1













1dd314a00b0c
Fixed wrong rename.



Cezary Kaliszyk <kaliszyk@in.tum.de>


parents: 
1009

diff
changeset




   264


apply(induct)













1dd314a00b0c
Fixed wrong rename.



Cezary Kaliszyk <kaliszyk@in.tum.de>


parents: 
1009

diff
changeset




   265


apply(rule alpha2.intros)













1dd314a00b0c
Fixed wrong rename.



Cezary Kaliszyk <kaliszyk@in.tum.de>


parents: 
1009

diff
changeset




   266


apply(simp)













1dd314a00b0c
Fixed wrong rename.



Cezary Kaliszyk <kaliszyk@in.tum.de>


parents: 
1009

diff
changeset




   267


apply(rule alpha2.intros)













1dd314a00b0c
Fixed wrong rename.



Cezary Kaliszyk <kaliszyk@in.tum.de>


parents: 
1009

diff
changeset




   268


apply(simp)













1dd314a00b0c
Fixed wrong rename.



Cezary Kaliszyk <kaliszyk@in.tum.de>


parents: 
1009

diff
changeset




   269


apply(simp)













1dd314a00b0c
Fixed wrong rename.



Cezary Kaliszyk <kaliszyk@in.tum.de>


parents: 
1009

diff
changeset




   270


apply(clarify)













1dd314a00b0c
Fixed wrong rename.



Cezary Kaliszyk <kaliszyk@in.tum.de>


parents: 
1009

diff
changeset




   271


apply(rule alpha2.intros)













1dd314a00b0c
Fixed wrong rename.



Cezary Kaliszyk <kaliszyk@in.tum.de>


parents: 
1009

diff
changeset




   272


apply(frule alpha_rfv)













1dd314a00b0c
Fixed wrong rename.



Cezary Kaliszyk <kaliszyk@in.tum.de>


parents: 
1009

diff
changeset




   273


apply(rotate_tac 4)













1dd314a00b0c
Fixed wrong rename.



Cezary Kaliszyk <kaliszyk@in.tum.de>


parents: 
1009

diff
changeset




   274


apply(drule sym)













1dd314a00b0c
Fixed wrong rename.



Cezary Kaliszyk <kaliszyk@in.tum.de>


parents: 
1009

diff
changeset




   275


apply(simp)













1dd314a00b0c
Fixed wrong rename.



Cezary Kaliszyk <kaliszyk@in.tum.de>


parents: 
1009

diff
changeset




   276


apply(drule sym)













1dd314a00b0c
Fixed wrong rename.



Cezary Kaliszyk <kaliszyk@in.tum.de>


parents: 
1009

diff
changeset




   277


apply(simp)













1dd314a00b0c
Fixed wrong rename.



Cezary Kaliszyk <kaliszyk@in.tum.de>


parents: 
1009

diff
changeset




   278


oops













1dd314a00b0c
Fixed wrong rename.



Cezary Kaliszyk <kaliszyk@in.tum.de>


parents: 
1009

diff
changeset




   279









947






fa810f01f7b5
added an LamEx example together with the new nominal infrastructure



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




   280


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




   281


  by (rule alpha_equivp)













fa810f01f7b5
added an LamEx example together with the new nominal infrastructure



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




   282














fa810f01f7b5
added an LamEx example together with the new nominal infrastructure



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




   283


quotient_definition













fa810f01f7b5
added an LamEx example together with the new nominal infrastructure



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




   284


  "Var :: name \<Rightarrow> lam"













fa810f01f7b5
added an LamEx example together with the new nominal infrastructure



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




   285


as













fa810f01f7b5
added an LamEx example together with the new nominal infrastructure



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




   286


  "rVar"













fa810f01f7b5
added an LamEx example together with the new nominal infrastructure



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




   287














fa810f01f7b5
added an LamEx example together with the new nominal infrastructure



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




   288


quotient_definition













fa810f01f7b5
added an LamEx example together with the new nominal infrastructure



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




   289


   "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




   290


as













fa810f01f7b5
added an LamEx example together with the new nominal infrastructure



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




   291


  "rApp"













fa810f01f7b5
added an LamEx example together with the new nominal infrastructure



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




   292














fa810f01f7b5
added an LamEx example together with the new nominal infrastructure



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




   293


quotient_definition













fa810f01f7b5
added an LamEx example together with the new nominal infrastructure



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




   294


  "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




   295


as













fa810f01f7b5
added an LamEx example together with the new nominal infrastructure



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




   296


  "rLam"













fa810f01f7b5
added an LamEx example together with the new nominal infrastructure



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




   297














fa810f01f7b5
added an LamEx example together with the new nominal infrastructure



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




   298


quotient_definition













fa810f01f7b5
added an LamEx example together with the new nominal infrastructure



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




   299


  "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




   300


as













fa810f01f7b5
added an LamEx example together with the new nominal infrastructure



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




   301


  "rfv"













fa810f01f7b5
added an LamEx example together with the new nominal infrastructure



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




   302














fa810f01f7b5
added an LamEx example together with the new nominal infrastructure



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




   303


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




   304


  "(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




   305


  apply(auto)













fa810f01f7b5
added an LamEx example together with the new nominal infrastructure



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




   306


  apply(rule alpha_eqvt)













fa810f01f7b5
added an LamEx example together with the new nominal infrastructure



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




   307


  apply(simp)













fa810f01f7b5
added an LamEx example together with the new nominal infrastructure



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




   308


  done













fa810f01f7b5
added an LamEx example together with the new nominal infrastructure



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




   309














fa810f01f7b5
added an LamEx example together with the new nominal infrastructure



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




   310


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




   311


  "(op = ===> alpha) rVar rVar"













fa810f01f7b5
added an LamEx example together with the new nominal infrastructure



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




   312


  by (auto intro: a1)













fa810f01f7b5
added an LamEx example together with the new nominal infrastructure



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




   313














fa810f01f7b5
added an LamEx example together with the new nominal infrastructure



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




   314


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




   315


  "(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




   316


  by (auto intro: a2)













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


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




   319


  "(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




   320


  apply(auto)













fa810f01f7b5
added an LamEx example together with the new nominal infrastructure



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




   321


  apply(rule a3)













fa810f01f7b5
added an LamEx example together with the new nominal infrastructure



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




   322


  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




   323


  unfolding fresh_star_def 








1011






1dd314a00b0c
Fixed wrong rename.



Cezary Kaliszyk <kaliszyk@in.tum.de>


parents: 
1009

diff
changeset




   324


  apply(simp add: fresh_star_def fresh_zero_perm)








947






fa810f01f7b5
added an LamEx example together with the new nominal infrastructure



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




   325


  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




   326


  done













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 rfv_rsp[quot_respect]: 













fa810f01f7b5
added an LamEx example together with the new nominal infrastructure



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




   329


  "(alpha ===> op =) rfv rfv"













fa810f01f7b5
added an LamEx example together with the new nominal infrastructure



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




   330


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




   331


done













fa810f01f7b5
added an LamEx example together with the new nominal infrastructure



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




   332














fa810f01f7b5
added an LamEx example together with the new nominal infrastructure



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




   333














fa810f01f7b5
added an LamEx example together with the new nominal infrastructure



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




   334


section {* lifted theorems *}













fa810f01f7b5
added an LamEx example together with the new nominal infrastructure



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




   335














fa810f01f7b5
added an LamEx example together with the new nominal infrastructure



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




   336


lemma lam_induct:













fa810f01f7b5
added an LamEx example together with the new nominal infrastructure



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




   337


  "\<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




   338


    \<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




   339


    \<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




   340


    \<Longrightarrow> P lam"













fa810f01f7b5
added an LamEx example together with the new nominal infrastructure



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




   341


  apply (lifting rlam.induct)













fa810f01f7b5
added an LamEx example together with the new nominal infrastructure



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




   342


  done













fa810f01f7b5
added an LamEx example together with the new nominal infrastructure



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




   343














fa810f01f7b5
added an LamEx example together with the new nominal infrastructure



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




   344


instantiation lam :: pt













fa810f01f7b5
added an LamEx example together with the new nominal infrastructure



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




   345


begin













fa810f01f7b5
added an LamEx example together with the new nominal infrastructure



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




   346














fa810f01f7b5
added an LamEx example together with the new nominal infrastructure



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




   347


quotient_definition













fa810f01f7b5
added an LamEx example together with the new nominal infrastructure



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




   348


  "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




   349


as













fa810f01f7b5
added an LamEx example together with the new nominal infrastructure



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




   350


  "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




   351














fa810f01f7b5
added an LamEx example together with the new nominal infrastructure



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




   352


lemma permute_lam [simp]:













fa810f01f7b5
added an LamEx example together with the new nominal infrastructure



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




   353


  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




   354


  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




   355


  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




   356


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




   357


done













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


instance













fa810f01f7b5
added an LamEx example together with the new nominal infrastructure



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




   360


apply default













fa810f01f7b5
added an LamEx example together with the new nominal infrastructure



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




   361


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




   362


apply(simp_all)













fa810f01f7b5
added an LamEx example together with the new nominal infrastructure



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




   363


done













fa810f01f7b5
added an LamEx example together with the new nominal infrastructure



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




   364














fa810f01f7b5
added an LamEx example together with the new nominal infrastructure



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




   365


end













fa810f01f7b5
added an LamEx example together with the new nominal infrastructure



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




   366














fa810f01f7b5
added an LamEx example together with the new nominal infrastructure



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




   367


lemma fv_lam [simp]: 













fa810f01f7b5
added an LamEx example together with the new nominal infrastructure



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




   368


  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




   369


  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




   370


  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




   371


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




   372


done













fa810f01f7b5
added an LamEx example together with the new nominal infrastructure



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




   373









990






c25ff084868f
now also final step is proved - the supp of lambdas is now completely characterised



Christian Urban <urbanc@in.tum.de>


parents: 
989

diff
changeset




   374


lemma fv_eqvt:













c25ff084868f
now also final step is proved - the supp of lambdas is now completely characterised



Christian Urban <urbanc@in.tum.de>


parents: 
989

diff
changeset




   375


  shows "(p \<bullet> fv t) = fv (p \<bullet> t)"













c25ff084868f
now also final step is proved - the supp of lambdas is now completely characterised



Christian Urban <urbanc@in.tum.de>


parents: 
989

diff
changeset




   376


apply(lifting rfv_eqvt)













c25ff084868f
now also final step is proved - the supp of lambdas is now completely characterised



Christian Urban <urbanc@in.tum.de>


parents: 
989

diff
changeset




   377


done













c25ff084868f
now also final step is proved - the supp of lambdas is now completely characterised



Christian Urban <urbanc@in.tum.de>


parents: 
989

diff
changeset




   378









947






fa810f01f7b5
added an LamEx example together with the new nominal infrastructure



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




   379


lemma a1: 













fa810f01f7b5
added an LamEx example together with the new nominal infrastructure



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




   380


  "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




   381


  by  (lifting a1)













fa810f01f7b5
added an LamEx example together with the new nominal infrastructure



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




   382














fa810f01f7b5
added an LamEx example together with the new nominal infrastructure



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




   383


lemma a2: 













fa810f01f7b5
added an LamEx example together with the new nominal infrastructure



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




   384


  "\<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




   385


  by  (lifting a2)













fa810f01f7b5
added an LamEx example together with the new nominal infrastructure



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




   386









1011






1dd314a00b0c
Fixed wrong rename.



Cezary Kaliszyk <kaliszyk@in.tum.de>


parents: 
1009

diff
changeset




   387


lemma a3: 













1dd314a00b0c
Fixed wrong rename.



Cezary Kaliszyk <kaliszyk@in.tum.de>


parents: 
1009

diff
changeset




   388


  "\<lbrakk>\<exists>pi. (fv t - {atom a} = fv s - {atom b} \<and> (fv t - {atom a})\<sharp>* pi \<and> (pi \<bullet> t) = s)\<rbrakk> 













1dd314a00b0c
Fixed wrong rename.



Cezary Kaliszyk <kaliszyk@in.tum.de>


parents: 
1009

diff
changeset




   389


   \<Longrightarrow> Lam a t = Lam b s"













1dd314a00b0c
Fixed wrong rename.



Cezary Kaliszyk <kaliszyk@in.tum.de>


parents: 
1009

diff
changeset




   390


  apply  (lifting a3)








947






fa810f01f7b5
added an LamEx example together with the new nominal infrastructure



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




   391


  done













fa810f01f7b5
added an LamEx example together with the new nominal infrastructure



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




   392









989






af02b193a19a
the supp of a lambda can now be characterised, *provided* the notion of free variables coincides with support on lambda terms



Christian Urban <urbanc@in.tum.de>


parents: 
984

diff
changeset




   393


lemma a3_inv:













af02b193a19a
the supp of a lambda can now be characterised, *provided* the notion of free variables coincides with support on lambda terms



Christian Urban <urbanc@in.tum.de>


parents: 
984

diff
changeset




   394


  assumes "Lam a t = Lam b s"













af02b193a19a
the supp of a lambda can now be characterised, *provided* the notion of free variables coincides with support on lambda terms



Christian Urban <urbanc@in.tum.de>


parents: 
984

diff
changeset




   395


  shows "\<exists>pi. (fv t - {atom a} = fv s - {atom b} \<and> (fv t - {atom a})\<sharp>* pi \<and> (pi \<bullet> t) = s)"













af02b193a19a
the supp of a lambda can now be characterised, *provided* the notion of free variables coincides with support on lambda terms



Christian Urban <urbanc@in.tum.de>


parents: 
984

diff
changeset




   396


using assms













af02b193a19a
the supp of a lambda can now be characterised, *provided* the notion of free variables coincides with support on lambda terms



Christian Urban <urbanc@in.tum.de>


parents: 
984

diff
changeset




   397


apply(lifting a3_inverse)













af02b193a19a
the supp of a lambda can now be characterised, *provided* the notion of free variables coincides with support on lambda terms



Christian Urban <urbanc@in.tum.de>


parents: 
984

diff
changeset




   398


done













af02b193a19a
the supp of a lambda can now be characterised, *provided* the notion of free variables coincides with support on lambda terms



Christian Urban <urbanc@in.tum.de>


parents: 
984

diff
changeset




   399









947






fa810f01f7b5
added an LamEx example together with the new nominal infrastructure



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




   400


lemma alpha_cases: 













fa810f01f7b5
added an LamEx example together with the new nominal infrastructure



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




   401


  "\<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




   402


    \<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




   403


    \<And>t a s b. \<lbrakk>a1 = Lam a t; a2 = Lam b s; 








989






af02b193a19a
the supp of a lambda can now be characterised, *provided* the notion of free variables coincides with support on lambda terms



Christian Urban <urbanc@in.tum.de>


parents: 
984

diff
changeset




   404


         \<exists>pi. fv t - {atom a} = fv s - {atom b} \<and> (fv t - {atom a}) \<sharp>* pi \<and> (pi \<bullet> t) = s\<rbrakk> 








947






fa810f01f7b5
added an LamEx example together with the new nominal infrastructure



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




   405


   \<Longrightarrow> P\<rbrakk>













fa810f01f7b5
added an LamEx example together with the new nominal infrastructure



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




   406


    \<Longrightarrow> P"













fa810f01f7b5
added an LamEx example together with the new nominal infrastructure



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




   407


  by (lifting alpha.cases)













fa810f01f7b5
added an LamEx example together with the new nominal infrastructure



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




   408









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




   409


(* 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




   410


lemma alpha_induct: 













fa810f01f7b5
added an LamEx example together with the new nominal infrastructure



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




   411


  "\<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




   412


    \<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




   413


     \<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




   414


        \<lbrakk>\<exists>pi. fv t - {atom a} = fv s - {atom b} \<and>








989






af02b193a19a
the supp of a lambda can now be characterised, *provided* the notion of free variables coincides with support on lambda terms



Christian Urban <urbanc@in.tum.de>


parents: 
984

diff
changeset




   415


         (fv t - {atom a}) \<sharp>* pi \<and> ((pi \<bullet> t) = s \<and> qxb (pi \<bullet> t) s)\<rbrakk> 








947






fa810f01f7b5
added an LamEx example together with the new nominal infrastructure



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




   416


     \<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




   417


    \<Longrightarrow> qxb qx qxa"













fa810f01f7b5
added an LamEx example together with the new nominal infrastructure



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




   418


  by (lifting alpha.induct)













fa810f01f7b5
added an LamEx example together with the new nominal infrastructure



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




   419














fa810f01f7b5
added an LamEx example together with the new nominal infrastructure



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




   420


(* should they lift automatically *)













fa810f01f7b5
added an LamEx example together with the new nominal infrastructure



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




   421


lemma lam_inject [simp]: 













fa810f01f7b5
added an LamEx example together with the new nominal infrastructure



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




   422


  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




   423


  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




   424


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




   425


apply(regularize)













bc739536b715
Minor when looking at lam.distinct and lam.inject



Cezary Kaliszyk <kaliszyk@in.tum.de>


parents: 
975

diff
changeset




   426


prefer 2













bc739536b715
Minor when looking at lam.distinct and lam.inject



Cezary Kaliszyk <kaliszyk@in.tum.de>


parents: 
975

diff
changeset




   427


apply(regularize)













bc739536b715
Minor when looking at lam.distinct and lam.inject



Cezary Kaliszyk <kaliszyk@in.tum.de>


parents: 
975

diff
changeset




   428


prefer 2








947






fa810f01f7b5
added an LamEx example together with the new nominal infrastructure



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




   429


apply(auto)













fa810f01f7b5
added an LamEx example together with the new nominal infrastructure



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




   430


apply(drule alpha.cases)













fa810f01f7b5
added an LamEx example together with the new nominal infrastructure



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




   431


apply(simp_all)













fa810f01f7b5
added an LamEx example together with the new nominal infrastructure



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




   432


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




   433


apply(drule alpha.cases)













fa810f01f7b5
added an LamEx example together with the new nominal infrastructure



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




   434


apply(simp_all)













fa810f01f7b5
added an LamEx example together with the new nominal infrastructure



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




   435


apply(drule alpha.cases)













fa810f01f7b5
added an LamEx example together with the new nominal infrastructure



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




   436


apply(simp_all)













fa810f01f7b5
added an LamEx example together with the new nominal infrastructure



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




   437


apply(rule alpha.a2)













fa810f01f7b5
added an LamEx example together with the new nominal infrastructure



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




   438


apply(simp_all)













fa810f01f7b5
added an LamEx example together with the new nominal infrastructure



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




   439


done













fa810f01f7b5
added an LamEx example together with the new nominal infrastructure



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




   440









989






af02b193a19a
the supp of a lambda can now be characterised, *provided* the notion of free variables coincides with support on lambda terms



Christian Urban <urbanc@in.tum.de>


parents: 
984

diff
changeset




   441


lemma Lam_pseudo_inject:













af02b193a19a
the supp of a lambda can now be characterised, *provided* the notion of free variables coincides with support on lambda terms



Christian Urban <urbanc@in.tum.de>


parents: 
984

diff
changeset




   442


  shows "(Lam a t = Lam b s) = 













af02b193a19a
the supp of a lambda can now be characterised, *provided* the notion of free variables coincides with support on lambda terms



Christian Urban <urbanc@in.tum.de>


parents: 
984

diff
changeset




   443


      (\<exists>pi. (fv t - {atom a} = fv s - {atom b} \<and> (fv t - {atom a})\<sharp>* pi \<and> (pi \<bullet> t) = s))"













af02b193a19a
the supp of a lambda can now be characterised, *provided* the notion of free variables coincides with support on lambda terms



Christian Urban <urbanc@in.tum.de>


parents: 
984

diff
changeset




   444


apply(rule iffI)













af02b193a19a
the supp of a lambda can now be characterised, *provided* the notion of free variables coincides with support on lambda terms



Christian Urban <urbanc@in.tum.de>


parents: 
984

diff
changeset




   445


apply(rule a3_inv)













af02b193a19a
the supp of a lambda can now be characterised, *provided* the notion of free variables coincides with support on lambda terms



Christian Urban <urbanc@in.tum.de>


parents: 
984

diff
changeset




   446


apply(assumption)













af02b193a19a
the supp of a lambda can now be characterised, *provided* the notion of free variables coincides with support on lambda terms



Christian Urban <urbanc@in.tum.de>


parents: 
984

diff
changeset




   447


apply(rule a3)













af02b193a19a
the supp of a lambda can now be characterised, *provided* the notion of free variables coincides with support on lambda terms



Christian Urban <urbanc@in.tum.de>


parents: 
984

diff
changeset




   448


apply(assumption)













af02b193a19a
the supp of a lambda can now be characterised, *provided* the notion of free variables coincides with support on lambda terms



Christian Urban <urbanc@in.tum.de>


parents: 
984

diff
changeset




   449


done













af02b193a19a
the supp of a lambda can now be characterised, *provided* the notion of free variables coincides with support on lambda terms



Christian Urban <urbanc@in.tum.de>


parents: 
984

diff
changeset




   450









947






fa810f01f7b5
added an LamEx example together with the new nominal infrastructure



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




   451


lemma rlam_distinct:













fa810f01f7b5
added an LamEx example together with the new nominal infrastructure



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




   452


  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




   453


  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




   454


  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




   455


  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




   456


  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




   457


  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




   458


apply auto








981






bc739536b715
Minor when looking at lam.distinct and lam.inject



Cezary Kaliszyk <kaliszyk@in.tum.de>


parents: 
975

diff
changeset




   459


apply (erule alpha.cases)













bc739536b715
Minor when looking at lam.distinct and lam.inject



Cezary Kaliszyk <kaliszyk@in.tum.de>


parents: 
975

diff
changeset




   460


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




   461


apply (erule alpha.cases)













bc739536b715
Minor when looking at lam.distinct and lam.inject



Cezary Kaliszyk <kaliszyk@in.tum.de>


parents: 
975

diff
changeset




   462


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




   463


apply (erule alpha.cases)













bc739536b715
Minor when looking at lam.distinct and lam.inject



Cezary Kaliszyk <kaliszyk@in.tum.de>


parents: 
975

diff
changeset




   464


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




   465


apply (erule alpha.cases)













bc739536b715
Minor when looking at lam.distinct and lam.inject



Cezary Kaliszyk <kaliszyk@in.tum.de>


parents: 
975

diff
changeset




   466


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




   467


apply (erule alpha.cases)













bc739536b715
Minor when looking at lam.distinct and lam.inject



Cezary Kaliszyk <kaliszyk@in.tum.de>


parents: 
975

diff
changeset




   468


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




   469


apply (erule alpha.cases)













bc739536b715
Minor when looking at lam.distinct and lam.inject



Cezary Kaliszyk <kaliszyk@in.tum.de>


parents: 
975

diff
changeset




   470


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




   471


done













fa810f01f7b5
added an LamEx example together with the new nominal infrastructure



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




   472














fa810f01f7b5
added an LamEx example together with the new nominal infrastructure



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




   473


lemma lam_distinct[simp]:













fa810f01f7b5
added an LamEx example together with the new nominal infrastructure



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




   474


  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




   475


  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




   476


  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




   477


  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




   478


  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




   479


  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




   480


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




   481


done













fa810f01f7b5
added an LamEx example together with the new nominal infrastructure



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




   482














fa810f01f7b5
added an LamEx example together with the new nominal infrastructure



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




   483


lemma var_supp1:













fa810f01f7b5
added an LamEx example together with the new nominal infrastructure



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




   484


  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




   485


  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




   486


  done













fa810f01f7b5
added an LamEx example together with the new nominal infrastructure



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




   487














fa810f01f7b5
added an LamEx example together with the new nominal infrastructure



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




   488


lemma var_supp:













fa810f01f7b5
added an LamEx example together with the new nominal infrastructure



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




   489


  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




   490


  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




   491














fa810f01f7b5
added an LamEx example together with the new nominal infrastructure



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




   492


lemma app_supp:













fa810f01f7b5
added an LamEx example together with the new nominal infrastructure



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




   493


  shows "supp (App t1 t2) = (supp t1) \<union> (supp t2)"








997






b7d259ded92e
Ported LF to the generic lambda and solved the simpler _supp cases.



Cezary Kaliszyk <kaliszyk@in.tum.de>


parents: 
995

diff
changeset




   494


apply(simp only: supp_def lam_inject)








947






fa810f01f7b5
added an LamEx example together with the new nominal infrastructure



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




   495


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




   496


done













fa810f01f7b5
added an LamEx example together with the new nominal infrastructure



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




   497









990






c25ff084868f
now also final step is proved - the supp of lambdas is now completely characterised



Christian Urban <urbanc@in.tum.de>


parents: 
989

diff
changeset




   498


(* supp for lam *)








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




   499


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




   500


  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




   501


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




   502


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




   503


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




   504


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




   505


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




   506


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




   507


done








947






fa810f01f7b5
added an LamEx example together with the new nominal infrastructure



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




   508









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




   509


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




   510


  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




   511


  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




   512


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




   513


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




   514


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




   515


done








947






fa810f01f7b5
added an LamEx example together with the new nominal infrastructure



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




   516














fa810f01f7b5
added an LamEx example together with the new nominal infrastructure



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




   517


instance lam :: fs













fa810f01f7b5
added an LamEx example together with the new nominal infrastructure



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




   518


apply(default)













fa810f01f7b5
added an LamEx example together with the new nominal infrastructure



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




   519


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




   520


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




   521


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




   522


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




   523


done













fa810f01f7b5
added an LamEx example together with the new nominal infrastructure



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




   524









990






c25ff084868f
now also final step is proved - the supp of lambdas is now completely characterised



Christian Urban <urbanc@in.tum.de>


parents: 
989

diff
changeset




   525


lemma supp_fv:













c25ff084868f
now also final step is proved - the supp of lambdas is now completely characterised



Christian Urban <urbanc@in.tum.de>


parents: 
989

diff
changeset




   526


  shows "supp t = fv t"













c25ff084868f
now also final step is proved - the supp of lambdas is now completely characterised



Christian Urban <urbanc@in.tum.de>


parents: 
989

diff
changeset




   527


apply(induct t rule: lam_induct)













c25ff084868f
now also final step is proved - the supp of lambdas is now completely characterised



Christian Urban <urbanc@in.tum.de>


parents: 
989

diff
changeset




   528


apply(simp add: var_supp)













c25ff084868f
now also final step is proved - the supp of lambdas is now completely characterised



Christian Urban <urbanc@in.tum.de>


parents: 
989

diff
changeset




   529


apply(simp add: app_supp)








1016






de8da5b32265
repaired according to changes in Abs.thy



Christian Urban <urbanc@in.tum.de>


parents: 
1011

diff
changeset




   530


apply(subgoal_tac "supp (Lam name lam) = supp (Abs {atom name} lam)")













de8da5b32265
repaired according to changes in Abs.thy



Christian Urban <urbanc@in.tum.de>


parents: 
1011

diff
changeset




   531


apply(simp add: supp_Abs)








990






c25ff084868f
now also final step is proved - the supp of lambdas is now completely characterised



Christian Urban <urbanc@in.tum.de>


parents: 
989

diff
changeset




   532


apply(simp (no_asm) add: supp_def permute_set_eq atom_eqvt)













c25ff084868f
now also final step is proved - the supp of lambdas is now completely characterised



Christian Urban <urbanc@in.tum.de>


parents: 
989

diff
changeset




   533


apply(simp add: Lam_pseudo_inject)








1016






de8da5b32265
repaired according to changes in Abs.thy



Christian Urban <urbanc@in.tum.de>


parents: 
1011

diff
changeset




   534


apply(simp add: Abs_eq_iff alpha_gen)








990






c25ff084868f
now also final step is proved - the supp of lambdas is now completely characterised



Christian Urban <urbanc@in.tum.de>


parents: 
989

diff
changeset




   535


apply(simp add: supp_eqvt[symmetric] fv_eqvt[symmetric])













c25ff084868f
now also final step is proved - the supp of lambdas is now completely characterised



Christian Urban <urbanc@in.tum.de>


parents: 
989

diff
changeset




   536


done













c25ff084868f
now also final step is proved - the supp of lambdas is now completely characterised



Christian Urban <urbanc@in.tum.de>


parents: 
989

diff
changeset




   537









989






af02b193a19a
the supp of a lambda can now be characterised, *provided* the notion of free variables coincides with support on lambda terms



Christian Urban <urbanc@in.tum.de>


parents: 
984

diff
changeset




   538


lemma lam_supp2:








1016






de8da5b32265
repaired according to changes in Abs.thy



Christian Urban <urbanc@in.tum.de>


parents: 
1011

diff
changeset




   539


  shows "supp (Lam x t) = supp (Abs {atom x} t)"








989






af02b193a19a
the supp of a lambda can now be characterised, *provided* the notion of free variables coincides with support on lambda terms



Christian Urban <urbanc@in.tum.de>


parents: 
984

diff
changeset




   540


apply(simp add: supp_def permute_set_eq atom_eqvt)













af02b193a19a
the supp of a lambda can now be characterised, *provided* the notion of free variables coincides with support on lambda terms



Christian Urban <urbanc@in.tum.de>


parents: 
984

diff
changeset




   541


apply(simp add: Lam_pseudo_inject)








1016






de8da5b32265
repaired according to changes in Abs.thy



Christian Urban <urbanc@in.tum.de>


parents: 
1011

diff
changeset




   542


apply(simp add: Abs_eq_iff supp_fv alpha_gen)








995






ee0619b5adff
introduced a generic alpha (but not sure whether it is helpful)



Christian Urban <urbanc@in.tum.de>


parents: 
990

diff
changeset




   543


done








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




   544














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


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




   546


  shows "supp (Lam x t) = ((supp t) - {atom x})"








989






af02b193a19a
the supp of a lambda can now be characterised, *provided* the notion of free variables coincides with support on lambda terms



Christian Urban <urbanc@in.tum.de>


parents: 
984

diff
changeset




   547


apply(simp add: lam_supp2)








1016






de8da5b32265
repaired according to changes in Abs.thy



Christian Urban <urbanc@in.tum.de>


parents: 
1011

diff
changeset




   548


apply(simp add: supp_Abs)








989






af02b193a19a
the supp of a lambda can now be characterised, *provided* the notion of free variables coincides with support on lambda terms



Christian Urban <urbanc@in.tum.de>


parents: 
984

diff
changeset




   549


done








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




   550









947






fa810f01f7b5
added an LamEx example together with the new nominal infrastructure



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




   551


lemma fresh_lam:













fa810f01f7b5
added an LamEx example together with the new nominal infrastructure



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




   552


  "(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




   553


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




   554


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




   555


apply(auto)













fa810f01f7b5
added an LamEx example together with the new nominal infrastructure



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




   556


done













fa810f01f7b5
added an LamEx example together with the new nominal infrastructure



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




   557














fa810f01f7b5
added an LamEx example together with the new nominal infrastructure



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




   558


lemma lam_induct_strong:













fa810f01f7b5
added an LamEx example together with the new nominal infrastructure



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




   559


  fixes a::"'a::fs"













fa810f01f7b5
added an LamEx example together with the new nominal infrastructure



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




   560


  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




   561


  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




   562


  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




   563


  shows "P a lam"













fa810f01f7b5
added an LamEx example together with the new nominal infrastructure



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




   564


proof -













fa810f01f7b5
added an LamEx example together with the new nominal infrastructure



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




   565


  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




   566


  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




   567


    case (1 name pi)













fa810f01f7b5
added an LamEx example together with the new nominal infrastructure



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




   568


    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




   569


      apply (simp)













fa810f01f7b5
added an LamEx example together with the new nominal infrastructure



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




   570


      apply (rule a1)













fa810f01f7b5
added an LamEx example together with the new nominal infrastructure



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




   571


      done













fa810f01f7b5
added an LamEx example together with the new nominal infrastructure



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




   572


  next













fa810f01f7b5
added an LamEx example together with the new nominal infrastructure



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




   573


    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




   574


    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




   575


    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




   576


    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




   577


      apply (simp)













fa810f01f7b5
added an LamEx example together with the new nominal infrastructure



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




   578


      apply (rule a2)













fa810f01f7b5
added an LamEx example together with the new nominal infrastructure



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




   579


      apply (rule b1)













fa810f01f7b5
added an LamEx example together with the new nominal infrastructure



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




   580


      apply (rule b2)













fa810f01f7b5
added an LamEx example together with the new nominal infrastructure



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




   581


      done













fa810f01f7b5
added an LamEx example together with the new nominal infrastructure



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




   582


  next













fa810f01f7b5
added an LamEx example together with the new nominal infrastructure



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




   583


    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




   584


    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




   585


    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




   586


      apply(rule obtain_atom)













fa810f01f7b5
added an LamEx example together with the new nominal infrastructure



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




   587


      apply(auto)













fa810f01f7b5
added an LamEx example together with the new nominal infrastructure



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




   588


      sorry













fa810f01f7b5
added an LamEx example together with the new nominal infrastructure



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




   589


    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




   590


      apply -













fa810f01f7b5
added an LamEx example together with the new nominal infrastructure



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




   591


      apply(rule a3)













fa810f01f7b5
added an LamEx example together with the new nominal infrastructure



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




   592


      apply(blast)













fa810f01f7b5
added an LamEx example together with the new nominal infrastructure



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




   593


      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




   594


      done













fa810f01f7b5
added an LamEx example together with the new nominal infrastructure



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




   595


    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




   596


      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




   597


      using fr













fa810f01f7b5
added an LamEx example together with the new nominal infrastructure



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




   598


      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




   599


      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




   600


      done













fa810f01f7b5
added an LamEx example together with the new nominal infrastructure



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




   601


    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




   602


      apply (simp)













fa810f01f7b5
added an LamEx example together with the new nominal infrastructure



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




   603


      apply(subst eq[symmetric])













fa810f01f7b5
added an LamEx example together with the new nominal infrastructure



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




   604


      using p













fa810f01f7b5
added an LamEx example together with the new nominal infrastructure



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




   605


      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




   606


      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




   607


      done













fa810f01f7b5
added an LamEx example together with the new nominal infrastructure



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




   608


  qed













fa810f01f7b5
added an LamEx example together with the new nominal infrastructure



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




   609


  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




   610


  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




   611


qed













fa810f01f7b5
added an LamEx example together with the new nominal infrastructure



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




   612














fa810f01f7b5
added an LamEx example together with the new nominal infrastructure



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




   613














fa810f01f7b5
added an LamEx example together with the new nominal infrastructure



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




   614


lemma var_fresh:













fa810f01f7b5
added an LamEx example together with the new nominal infrastructure



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




   615


  fixes a::"name"













fa810f01f7b5
added an LamEx example together with the new nominal infrastructure



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




   616


  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




   617


  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




   618


  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




   619


  done













fa810f01f7b5
added an LamEx example together with the new nominal infrastructure



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




   620














fa810f01f7b5
added an LamEx example together with the new nominal infrastructure



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




   621














fa810f01f7b5
added an LamEx example together with the new nominal infrastructure



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




   622









1087






bb7f4457091a
moved some lemmas to Nominal; updated all files



Christian Urban <urbanc@in.tum.de>


parents: 
1028

diff
changeset




   623


end








947






fa810f01f7b5
added an LamEx example together with the new nominal infrastructure



Christian Urban <urbanc@in.tum.de>


parents: 

diff
changeset




   624
















nominal2