# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1336857685 -3600
# Node ID 89715c48f728706725b73dc267b2675b9c1dd842
# Parent  b6873d123f9b647012b8b09ffd008f7818933682
cleaned also examples

diff -r b6873d123f9b -r 89715c48f728 Nominal/Ex/CPS/CPS1_Plotkin.thy
--- a/Nominal/Ex/CPS/CPS1_Plotkin.thy	Sat May 12 21:39:09 2012 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,332 +0,0 @@
-header {* CPS conversion *}
-theory CPS1_Plotkin
-imports Lt
-begin
-
-nominal_primrec
-  CPS :: "lt \<Rightarrow> lt" ("_*" [250] 250)
-where
-  "atom k \<sharp> x \<Longrightarrow> (x~)* = (Lam k ((k~) $ (x~)))"
-| "atom k \<sharp> (x, M) \<Longrightarrow> (Lam x M)* = Lam k (k~ $ Lam x (M*))"
-| "atom k \<sharp> (M, N) \<Longrightarrow> atom m \<sharp> (N, k) \<Longrightarrow> atom n \<sharp> (k, m) \<Longrightarrow>
-    (M $ N)* = Lam k (M* $ Lam m (N* $ Lam n (m~ $ n~ $ k~)))"
-unfolding eqvt_def CPS_graph_def
-apply (rule, perm_simp, rule, rule)
-apply (simp_all add: fresh_Pair_elim)
-apply (rule_tac y="x" in lt.exhaust)
-apply (auto)
-apply (rule_tac x="name" and ?'a="name" in obtain_fresh)
-apply (simp_all add: fresh_at_base)[3]
-apply (rule_tac x="(lt1, lt2)" and ?'a="name" in obtain_fresh)
-apply (rule_tac x="(lt2, a)" and ?'a="name" in obtain_fresh)
-apply (rule_tac x="(a, aa)" and ?'a="name" in obtain_fresh)
-apply (simp add: fresh_Pair_elim fresh_at_base)
-apply (rule_tac x="(name, lt)" and ?'a="name" in obtain_fresh)
-apply (simp add: fresh_Pair_elim fresh_at_base)[2]
-apply (simp add: Abs1_eq_iff lt.fresh fresh_at_base)
---"-"
-apply(rule_tac s="[[atom ka]]lst. ka~ $ Lam x (CPS_sumC M)" in trans)
-apply (case_tac "k = ka")
-apply simp
-apply(simp (no_asm) add: Abs1_eq_iff del:eqvts)
-apply (simp del: eqvts add: lt.fresh fresh_at_base)
-apply (simp only: lt.perm_simps(1) lt.perm_simps(2) flip_def[symmetric] lt.eq_iff)
-apply (subst  flip_at_base_simps(2))
-apply simp
-apply (intro conjI refl)
-apply (rule flip_fresh_fresh[symmetric])
-apply (simp_all add: lt.fresh)
-apply (metis fresh_eqvt_at lt.fsupp)
-apply (case_tac "ka = x")
-apply simp_all[2]
-apply (metis Abs_fresh_iff(3) atom_eq_iff finite_set fresh_Cons fresh_Nil fresh_atom fresh_eqvt_at fresh_finite_atom_set fresh_set lt.fsupp)
-apply (metis Abs_fresh_iff(3) atom_eq_iff finite_set fresh_Cons fresh_Nil fresh_atom fresh_eqvt_at fresh_finite_atom_set fresh_set lt.fsupp)
---"-"
-apply (simp add: Abs1_eq(3))
-apply (erule Abs_lst1_fcb2)
-apply (simp_all add: Abs_fresh_iff fresh_Nil fresh_star_def eqvt_at_def)[4]
---"-"
-apply (rename_tac k' M N m' n')
-apply (subgoal_tac "atom k \<sharp> CPS_sumC M \<and> atom k' \<sharp> CPS_sumC M \<and> atom k \<sharp> CPS_sumC N \<and> atom k' \<sharp> CPS_sumC N \<and>
-                    atom m \<sharp> CPS_sumC N \<and> atom m' \<sharp> CPS_sumC N")
-prefer 2
-apply (intro conjI)
-apply (erule fresh_eqvt_at, simp add: finite_supp, assumption)+
-apply clarify
-apply (case_tac "k = k'", case_tac [!] "m' = k",case_tac [!]"m = k'",case_tac[!] "m = m'")
-apply (simp_all add: Abs1_eq_iff lt.fresh flip_def[symmetric] fresh_at_base flip_fresh_fresh permute_eq_iff)
-by (metis flip_at_base_simps(3) flip_at_simps(2) flip_commute permute_flip_at)+
-
-termination (eqvt) by lexicographic_order
-
-lemmas [simp] = fresh_Pair_elim CPS.simps(2,3)[simplified fresh_Pair_elim]
-
-lemma [simp]: "supp (M*) = supp M"
-  by (induct rule: CPS.induct, simp_all add: lt.supp supp_at_base fresh_at_base fresh_def supp_Pair)
-     (simp_all only: atom_eq_iff[symmetric], blast+)
-
-lemma [simp]: "x \<sharp> M* = x \<sharp> M"
-  unfolding fresh_def by simp
-
-nominal_primrec
-  convert:: "lt => lt" ("_+" [250] 250)
-where
-  "(Var x)+ = Var x"
-| "(Lam x M)+ = Lam x (M*)"
-| "(M $ N)+ = M $ N"
-  unfolding convert_graph_def eqvt_def
-  apply (rule, perm_simp, rule, rule)
-  apply (erule lt.exhaust)
-  apply (simp_all)
-  apply blast
-  apply (simp add: Abs1_eq_iff CPS.eqvt)
-  by blast
-
-termination (eqvt)
-  by (relation "measure size") (simp_all)
-
-lemma convert_supp[simp]:
-  shows "supp (M+) = supp M"
-  by (induct M rule: lt.induct, simp_all add: lt.supp)
-
-lemma convert_fresh[simp]:
-  shows "x \<sharp> (M+) = x \<sharp> M"
-  unfolding fresh_def by simp
-
-lemma [simp]:
-  shows "isValue (p \<bullet> (M::lt)) = isValue M"
-  by (nominal_induct M rule: lt.strong_induct) auto
-
-nominal_primrec
-  Kapply :: "lt \<Rightarrow> lt \<Rightarrow> lt"       (infixl ";" 100)
-where
-  "Kapply (Lam x M) K = K $ (Lam x M)+"
-| "Kapply (Var x) K = K $ Var x"
-| "isValue M \<Longrightarrow> isValue N \<Longrightarrow> Kapply (M $ N) K = M+ $ N+ $ K"
-| "isValue M \<Longrightarrow> \<not>isValue N \<Longrightarrow> atom n \<sharp> M \<Longrightarrow> atom n \<sharp> K \<Longrightarrow>
-    Kapply (M $ N) K = N; (Lam n (M+ $ Var n $ K))"
-| "\<not>isValue M \<Longrightarrow> atom m \<sharp> N \<Longrightarrow> atom m \<sharp> K \<Longrightarrow> atom n \<sharp> m \<Longrightarrow> atom n \<sharp> K \<Longrightarrow>
-    Kapply (M $ N) K = M; (Lam m (N*  $ (Lam n (Var m $ Var n $ K))))"
-  unfolding Kapply_graph_def eqvt_def
-  apply (rule, perm_simp, rule, rule)
-apply (simp_all)
-apply (case_tac x)
-apply (rule_tac y="a" in lt.exhaust)
-apply (auto)
-apply (case_tac "isValue lt1")
-apply (case_tac "isValue lt2")
-apply (auto)[1]
-apply (rule_tac x="(lt1, ba)" and ?'a="name" in obtain_fresh)
-apply (simp add: fresh_Pair_elim fresh_at_base)
-apply (rule_tac x="(lt2, ba)" and ?'a="name" in obtain_fresh)
-apply (rule_tac x="(a, ba)" and ?'a="name" in obtain_fresh)
-apply (simp add: fresh_Pair_elim fresh_at_base)
-apply (auto simp add: Abs1_eq_iff eqvts)[1]
-apply (rename_tac M N u K)
-apply (subgoal_tac "Lam n (M+ $ n~ $ K) =  Lam u (M+ $ u~ $ K)")
-apply (simp only:)
-apply (auto simp add: Abs1_eq_iff flip_def[symmetric] lt.fresh fresh_at_base flip_fresh_fresh[symmetric])[1]
-apply (subgoal_tac "Lam m (Na* $ Lam n (m~ $ n~ $ Ka)) = Lam ma (Na* $ Lam na (ma~ $ na~ $ Ka))")
-apply (simp only:)
-apply (simp add: Abs1_eq_iff flip_def[symmetric] lt.fresh fresh_at_base)
-apply (subgoal_tac "Ka = (n \<leftrightarrow> na) \<bullet> Ka")
-apply (subgoal_tac "Ka = (m \<leftrightarrow> ma) \<bullet> Ka")
-apply (subgoal_tac "Ka = (n \<leftrightarrow> (m \<leftrightarrow> ma) \<bullet> na) \<bullet> Ka")
-apply (case_tac "m = ma")
-apply simp_all
-apply rule
-apply (auto simp add: flip_fresh_fresh[symmetric])
-apply (metis flip_at_base_simps(3) flip_fresh_fresh permute_flip_at)+
-done
-
-termination (eqvt)
-  by (relation "measure (\<lambda>(t, _). size t)") (simp_all)
-
-section{* lemma related to Kapply *}
-
-lemma [simp]: "isValue V \<Longrightarrow> V; K = K $ (V+)"
-  by (nominal_induct V rule: lt.strong_induct) auto
-
-section{* lemma related to CPS conversion *}
-
-lemma value_CPS:
-  assumes "isValue V"
-  and "atom a \<sharp> V"
-  shows "V* = Lam a (a~ $ V+)"
-  using assms
-proof (nominal_induct V avoiding: a rule: lt.strong_induct, simp_all add: lt.fresh)
-  fix name :: name and lt aa
-  assume a: "atom name \<sharp> aa" "\<And>b. \<lbrakk>isValue lt; atom b \<sharp> lt\<rbrakk> \<Longrightarrow> lt* = Lam b (b~ $ lt+)"
-    "atom aa \<sharp> lt \<or> aa = name"
-  obtain ab :: name where b: "atom ab \<sharp> (name, lt, a)" using obtain_fresh by blast
-  show "Lam name lt* = Lam aa (aa~ $ Lam name (lt*))" using a b
-    by (simp add: Abs1_eq_iff fresh_at_base lt.fresh)
-qed
-
-section{* first lemma CPS subst *}
-
-lemma CPS_subst_fv:
-  assumes *:"isValue V"
-  shows "((M[x ::= V])* = (M*)[x ::= V+])"
-using * proof (nominal_induct M avoiding: V x rule: lt.strong_induct)
-  case (Var name)
-  assume *: "isValue V"
-  obtain a :: name where a: "atom a \<sharp> (x, name, V)" using obtain_fresh by blast
-  show "((name~)[x ::= V])* = (name~)*[x ::= V+]" using a
-    by (simp add: fresh_at_base * value_CPS)
-next
-  case (Lam name lt V x)
-  assume *: "atom name \<sharp> V" "atom name \<sharp> x" "\<And>b ba. isValue b \<Longrightarrow> (lt[ba ::= b])* = lt*[ba ::= b+]"
-    "isValue V"
-  obtain a :: name where a: "atom a \<sharp> (name, lt, lt[x ::= V], x, V)" using obtain_fresh by blast
-  show "(Lam name lt[x ::= V])* = Lam name lt*[x ::= V+]" using * a
-    by (simp add: fresh_at_base)
-next
-  case (App lt1 lt2 V x)
-  assume *: "\<And>b ba. isValue b \<Longrightarrow> (lt1[ba ::= b])* = lt1*[ba ::= b+]" "\<And>b ba. isValue b \<Longrightarrow> (lt2[ba ::= b])* = lt2*[ba ::= b+]"
-    "isValue V"
-  obtain a :: name where a: "atom a \<sharp> (lt1[x ::= V], lt1, lt2[x ::= V], lt2, V, x)" using obtain_fresh by blast
-  obtain b :: name where b: "atom b \<sharp> (lt2[x ::= V], lt2, a, V, x)" using obtain_fresh by blast
-  obtain c :: name where c: "atom c \<sharp> (a, b, V, x)" using obtain_fresh by blast
-  show "((lt1 $ lt2)[x ::= V])* = (lt1 $ lt2)*[x ::= V+]" using * a b c
-    by (simp add: fresh_at_base)
-qed
-
-lemma [simp]: "isValue V \<Longrightarrow> isValue (V+)"
-  by (nominal_induct V rule: lt.strong_induct, auto)
-
-lemma CPS_eval_Kapply:
-  assumes a: "isValue K"
-  shows "(M* $ K) \<longrightarrow>\<^isub>\<beta>\<^sup>* (M ; K)"
-  using a
-proof (nominal_induct M avoiding: K rule: lt.strong_induct, simp_all)
-  case (Var name K)
-  assume *: "isValue K"
-  obtain a :: name where a: "atom a \<sharp> (name, K)" using obtain_fresh by blast
-  show "(name~)* $ K \<longrightarrow>\<^isub>\<beta>\<^sup>* K $ name~" using * a
-    by simp (rule evbeta', simp_all add: fresh_at_base)
-next
-  fix name :: name and lt K
-  assume *: "atom name \<sharp> K" "\<And>b. isValue b \<Longrightarrow> lt* $ b \<longrightarrow>\<^isub>\<beta>\<^sup>* lt ; b" "isValue K"
-  obtain a :: name where a: "atom a \<sharp> (name, K, lt)" using obtain_fresh by blast
-  then have b: "atom name \<sharp> a" using fresh_PairD(1) fresh_at_base atom_eq_iff by metis
-  show "Lam name lt* $ K \<longrightarrow>\<^isub>\<beta>\<^sup>* K $ Lam name (lt*)" using * a b
-    by simp (rule evbeta', simp_all)
-next
-  fix lt1 lt2 K
-  assume *: "\<And>b. isValue b \<Longrightarrow>  lt1* $ b \<longrightarrow>\<^isub>\<beta>\<^sup>* lt1 ; b" "\<And>b. isValue b \<Longrightarrow>  lt2* $ b \<longrightarrow>\<^isub>\<beta>\<^sup>* lt2 ; b" "isValue K"
-  obtain a :: name where a: "atom a \<sharp> (lt1, lt2, K)" using obtain_fresh by blast
-  obtain b :: name where b: "atom b \<sharp> (lt1, lt2, K, a)" using obtain_fresh by blast
-  obtain c :: name where c: "atom c \<sharp> (lt1, lt2, K, a, b)" using obtain_fresh by blast
-  have d: "atom a \<sharp> lt1" "atom a \<sharp> lt2" "atom a \<sharp> K" "atom b \<sharp> lt1" "atom b \<sharp> lt2" "atom b \<sharp> K" "atom b \<sharp> a"
-    "atom c \<sharp> lt1" "atom c \<sharp> lt2" "atom c \<sharp> K" "atom c \<sharp> a" "atom c \<sharp> b" using fresh_Pair a b c by simp_all
-  have "(lt1 $ lt2)* $ K \<longrightarrow>\<^isub>\<beta>\<^sup>* lt1* $ Lam b (lt2* $ Lam c (b~ $ c~ $ K))" using * d
-    by (simp add: fresh_at_base) (rule evbeta', simp_all add: fresh_at_base)
-  also have "... \<longrightarrow>\<^isub>\<beta>\<^sup>* lt1 $ lt2 ; K" proof (cases "isValue lt1")
-    assume e: "isValue lt1"
-    have "lt1* $ Lam b (lt2* $ Lam c (b~ $ c~ $ K)) \<longrightarrow>\<^isub>\<beta>\<^sup>* Lam b (lt2* $ Lam c (b~ $ c~ $ K)) $ lt1+"
-      using * d e by simp
-    also have "... \<longrightarrow>\<^isub>\<beta>\<^sup>* lt2* $ Lam c (lt1+ $ c~ $ K)"
-      by (rule evbeta', simp_all add: * d e, metis d(12) fresh_at_base)
-    also have "... \<longrightarrow>\<^isub>\<beta>\<^sup>* lt1 $ lt2 ; K" proof (cases "isValue lt2")
-      assume f: "isValue lt2"
-      have "lt2* $ Lam c (lt1+ $ c~ $ K) \<longrightarrow>\<^isub>\<beta>\<^sup>* Lam c (lt1+ $ c~ $ K) $ lt2+" using * d e f by simp
-      also have "... \<longrightarrow>\<^isub>\<beta>\<^sup>* lt1+ $ lt2+ $ K"
-        by (rule evbeta', simp_all add: d e f)
-      finally show ?thesis using * d e f by simp
-    next
-      assume f: "\<not> isValue lt2"
-      have "lt2* $ Lam c (lt1+ $ c~ $ K) \<longrightarrow>\<^isub>\<beta>\<^sup>* lt2 ; Lam c (lt1+ $ c~ $ K)" using * d e f by simp
-      also have "... \<longrightarrow>\<^isub>\<beta>\<^sup>* lt2 ; Lam a (lt1+ $ a~ $ K)" using Kapply.simps(4) d e evs1 f by metis
-      finally show ?thesis using * d e f by simp
-    qed
-    finally show ?thesis .
-  qed (metis Kapply.simps(5) isValue.simps(2) * d)
-  finally show "(lt1 $ lt2)* $ K \<longrightarrow>\<^isub>\<beta>\<^sup>* lt1 $ lt2 ; K" .
-qed
-
-lemma Kapply_eval:
-  assumes a: "M \<longrightarrow>\<^isub>\<beta> N" "isValue K"
-  shows "(M; K) \<longrightarrow>\<^isub>\<beta>\<^sup>*  (N; K)"
-  using assms
-proof (induct arbitrary: K rule: eval.induct)
-  case (evbeta x V M)
-  fix K
-  assume a: "isValue K" "isValue V" "atom x \<sharp> V"
-  have "Lam x (M*) $ V+ $ K \<longrightarrow>\<^isub>\<beta>\<^sup>* (((M*)[x ::= V+]) $ K)"
-    by (rule evs2,rule ev2,rule Lt.evbeta) (simp_all add: fresh_def a[simplified fresh_def] evs1)
-  also have "... = ((M[x ::= V])* $ K)" by (simp add: CPS_subst_fv a)
-  also have "... \<longrightarrow>\<^isub>\<beta>\<^sup>* ((M[x ::= V]) ; K)" by (rule CPS_eval_Kapply, simp_all add: a)
-  finally show "(Lam x M $ V ; K) \<longrightarrow>\<^isub>\<beta>\<^sup>*  ((M[x ::= V]) ; K)" using a by simp
-next
-  case (ev1 V M N)
-  fix V M N K
-  assume a: "isValue V" "M \<longrightarrow>\<^isub>\<beta> N" "\<And>K. isValue K \<Longrightarrow> M ; K \<longrightarrow>\<^isub>\<beta>\<^sup>* N ; K" "isValue K"
-  obtain a :: name where b: "atom a \<sharp> (V, K, M, N)" using obtain_fresh by blast
-  show "V $ M ; K \<longrightarrow>\<^isub>\<beta>\<^sup>* V $ N ; K" proof (cases "isValue N")
-    assume "\<not> isValue N"
-    then show "V $ M ; K \<longrightarrow>\<^isub>\<beta>\<^sup>* V $ N ; K" using a b by simp
-  next
-    assume n: "isValue N"
-    have c: "M; Lam a (V+ $ a~ $ K) \<longrightarrow>\<^isub>\<beta>\<^sup>* Lam a (V+ $ a~ $ K) $ N+" using a b by (simp add: n)
-    also have d: "... \<longrightarrow>\<^isub>\<beta>\<^sup>* V+ $ N+ $ K" by (rule evbeta') (simp_all add: a b n)
-    finally show "V $ M ; K \<longrightarrow>\<^isub>\<beta>\<^sup>* V $ N ; K" using a b by (simp add: n)
-  qed
-next
-  case (ev2 M M' N)
-  assume *: "M \<longrightarrow>\<^isub>\<beta> M'" "\<And>K. isValue K \<Longrightarrow>  M ; K \<longrightarrow>\<^isub>\<beta>\<^sup>* M' ; K" "isValue K"
-  obtain a :: name where a: "atom a \<sharp> (K, M, N, M')" using obtain_fresh by blast
-  obtain b :: name where b: "atom b \<sharp> (a, K, M, N, M', N+)" using obtain_fresh by blast
-  have d: "atom a \<sharp> K" "atom a \<sharp> M" "atom a \<sharp> N" "atom a \<sharp> M'" "atom b \<sharp> a" "atom b \<sharp> K"
-    "atom b \<sharp> M" "atom b \<sharp> N" "atom b \<sharp> M'" using a b fresh_Pair by simp_all
-  have "M $ N ; K  \<longrightarrow>\<^isub>\<beta>\<^sup>* M' ; Lam a (N* $ Lam b (a~ $ b~ $ K))" using * d by simp
-  also have "... \<longrightarrow>\<^isub>\<beta>\<^sup>* M' $ N ; K" proof (cases "isValue M'")
-    assume "\<not> isValue M'"
-    then show ?thesis using * d by (simp_all add: evs1)
-  next
-    assume e: "isValue M'"
-    then have "M' ; Lam a (N* $ Lam b (a~ $ b~ $ K)) = Lam a (N* $ Lam b (a~ $ b~ $ K)) $ M'+" by simp
-    also have "... \<longrightarrow>\<^isub>\<beta>\<^sup>* (N* $ Lam b (a~ $ b~ $ K))[a ::= M'+]"
-      by (rule evbeta') (simp_all add: fresh_at_base e d)
-    also have "... = N* $ Lam b (M'+ $ b~ $ K)" using * d by (simp add: fresh_at_base)
-    also have "... \<longrightarrow>\<^isub>\<beta>\<^sup>* M' $ N ; K" proof (cases "isValue N")
-      assume f: "isValue N"
-      have "N* $ Lam b (M'+ $ b~ $ K) \<longrightarrow>\<^isub>\<beta>\<^sup>* Lam b (M'+ $ b~ $ K) $ N+"
-        by (rule eval_trans, rule CPS_eval_Kapply) (simp_all add: d e f * evs1)
-      also have "... \<longrightarrow>\<^isub>\<beta>\<^sup>* M' $ N ; K" by (rule evbeta') (simp_all add: d e f evs1)
-      finally show ?thesis .
-    next
-      assume "\<not> isValue N"
-      then show ?thesis using d e
-        by (metis CPS_eval_Kapply Kapply.simps(4) isValue.simps(2))
-    qed
-    finally show ?thesis .
-  qed
-  finally show ?case .
-qed
-
-lemma Kapply_eval_rtrancl:
-  assumes H: "M \<longrightarrow>\<^isub>\<beta>\<^sup>*  N" and "isValue K"
-  shows "(M;K) \<longrightarrow>\<^isub>\<beta>\<^sup>* (N;K)"
-  using H
-  by (induct) (metis Kapply_eval assms(2) eval_trans evs1)+
-
-lemma
-  assumes "isValue V" "M \<longrightarrow>\<^isub>\<beta>\<^sup>* V"
-  shows "M* $ (Lam x (x~)) \<longrightarrow>\<^isub>\<beta>\<^sup>* V+"
-proof-
-  obtain y::name where *: "atom y \<sharp> V" using obtain_fresh by blast
-  have e: "Lam x (x~) = Lam y (y~)"
-    by (simp add: Abs1_eq_iff lt.fresh fresh_at_base)
-  have "M* $ Lam x (x~) \<longrightarrow>\<^isub>\<beta>\<^sup>* M ; Lam x (x~)"
-    by(rule CPS_eval_Kapply,simp_all add: assms)
-  also have "... \<longrightarrow>\<^isub>\<beta>\<^sup>* (V ; Lam x (x~))" by (rule Kapply_eval_rtrancl, simp_all add: assms)
-  also have "... = V ; Lam y (y~)" using e by (simp only:)
-  also have "... \<longrightarrow>\<^isub>\<beta>\<^sup>* (V+)" by (simp add: assms, rule evbeta') (simp_all add: assms *)
-  finally show "M* $ (Lam x (x~)) \<longrightarrow>\<^isub>\<beta>\<^sup>* (V+)" .
-qed
-
-end
-
-
-
diff -r b6873d123f9b -r 89715c48f728 Nominal/Ex/CPS/CPS2_DanvyNielsen.thy
--- a/Nominal/Ex/CPS/CPS2_DanvyNielsen.thy	Sat May 12 21:39:09 2012 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,114 +0,0 @@
-header {* CPS transformation of Danvy and Nielsen *}
-theory CPS2_DanvyNielsen
-imports Lt
-begin
-
-nominal_datatype cpsctxt =
-  Hole
-| CFun cpsctxt lt
-| CArg lt cpsctxt
-| CAbs x::name c::cpsctxt binds x in c
-
-nominal_primrec
-  fill   :: "cpsctxt \<Rightarrow> lt \<Rightarrow> lt"         ("_<_>" [200, 200] 100)
-where
-  fill_hole : "Hole<M> = M"
-| fill_fun  : "(CFun C N)<M> = (C<M>) $ N"
-| fill_arg  : "(CArg N C)<M> = N $ (C<M>)"
-| fill_abs  : "atom x \<sharp> M \<Longrightarrow> (CAbs x C)<M> = Lam x (C<M>)"
-  unfolding eqvt_def fill_graph_def
-  apply perm_simp
-  apply auto
-  apply (rule_tac y="a" and c="b" in cpsctxt.strong_exhaust)
-  apply (auto simp add: fresh_star_def)
-  apply (erule Abs_lst1_fcb)
-  apply (simp_all add: Abs_fresh_iff)
-  apply (erule fresh_eqvt_at)
-  apply (simp add: finite_supp)
-  apply (simp add: fresh_Pair)
-  apply (simp add: eqvt_at_def swap_fresh_fresh)
-  done
-
-termination (eqvt) by lexicographic_order
-
-nominal_primrec
-  ccomp :: "cpsctxt => cpsctxt => cpsctxt"
-where
-  "ccomp Hole C  = C"
-| "atom x \<sharp> C' \<Longrightarrow> ccomp (CAbs x C) C' = CAbs x (ccomp C C')"
-| "ccomp (CArg N C) C' = CArg N (ccomp C C')"
-| "ccomp (CFun C N) C'  = CFun (ccomp C C') N"
-  unfolding eqvt_def ccomp_graph_def
-  apply perm_simp
-  apply auto
-  apply (rule_tac y="a" and c="b" in cpsctxt.strong_exhaust)
-  apply (auto simp add: fresh_star_def)
-  apply blast+
-  apply (erule Abs_lst1_fcb)
-  apply (simp_all add: Abs_fresh_iff)
-  apply (erule fresh_eqvt_at)
-  apply (simp add: finite_supp)
-  apply (simp add: fresh_Pair)
-  apply (simp add: eqvt_at_def swap_fresh_fresh)
-  done
-
-termination (eqvt) by lexicographic_order
-
-nominal_primrec
-    CPSv :: "lt => lt"
-and CPS :: "lt => cpsctxt" where
-  "CPSv (Var x) = x~"
-| "CPS (Var x) = CFun Hole (x~)"
-| "atom b \<sharp> M \<Longrightarrow> CPSv (Lam y M) = Lam y (Lam b ((CPS M)<Var b>))"
-| "atom b \<sharp> M \<Longrightarrow> CPS (Lam y M) = CFun Hole (Lam y (Lam b ((CPS M)<Var b>)))"
-| "CPSv (M $ N) = Lam x (Var x)"
-| "isValue M \<Longrightarrow> isValue N \<Longrightarrow> CPS (M $ N) = CArg (CPSv M $ CPSv N) Hole"
-| "isValue M \<Longrightarrow> ~isValue N \<Longrightarrow> atom a \<sharp> M \<Longrightarrow> CPS (M $ N) =
-     ccomp (CPS N) (CAbs a (CArg (CPSv M $ Var a) Hole))"
-| "~isValue M \<Longrightarrow> isValue N \<Longrightarrow> atom a \<sharp> N \<Longrightarrow> CPS (M $ N) =
-     ccomp (CPS M) (CAbs a (CArg (Var a $ (CPSv N)) Hole))"
-| "~isValue M \<Longrightarrow> ~isValue N \<Longrightarrow> atom a \<sharp> (N, b) \<Longrightarrow> CPS (M $ N) =
-     ccomp (CPS M) (CAbs a (ccomp (CPS N) (CAbs b (CArg (Var a $ Var b) Hole))))"
-  apply auto
-  defer
-  apply (case_tac x)
-  apply (rule_tac y="a" in lt.exhaust)
-  apply auto
-  apply blast
-  apply (rule_tac x="lt" and ?'a="name" in obtain_fresh)
-  apply (simp add: Abs1_eq_iff)
-  apply blast+
-  apply (rule_tac y="b" in lt.exhaust)
-  apply auto
-  apply (rule_tac ?'a="name" in obtain_fresh)
-  apply (rule_tac x="(lt1, lt2, a)" and ?'a="name" in obtain_fresh)
-  apply (simp add: fresh_Pair_elim)
-  apply (case_tac "isValue lt1", case_tac [!] "isValue lt2")[1]
-  apply (simp_all add: fresh_Pair)[4]
-  apply (rule_tac x="lt" and ?'a="name" in obtain_fresh)
-  apply (simp add: Abs1_eq_iff)
-  apply blast
---""
-  apply (rule_tac x="(y, ya, b, ba, M, Ma)" and ?'a="name" in obtain_fresh)
-  apply (subgoal_tac "Lam b (Sum_Type.Projr (CPSv_CPS_sumC (Inr M))<(b~)>) = Lam a (Sum_Type.Projr (CPSv_CPS_sumC (Inr M))<(a~)>)")
-  apply (subgoal_tac "Lam ba (Sum_Type.Projr (CPSv_CPS_sumC (Inr Ma))<(ba~)>) = Lam a (Sum_Type.Projr (CPSv_CPS_sumC (Inr Ma))<(a~)>)")
-  apply (simp only:)
-  apply (erule Abs_lst1_fcb)
-  apply (simp add: Abs_fresh_iff)
-  apply (simp_all add: Abs_fresh_iff lt.fresh fresh_Pair_elim fresh_at_base swap_fresh_fresh)[2]
-  (* need an invariant to get eqvt_at (Proj) *)
-  defer defer
-  apply simp
-  apply (simp_all add: Abs1_eq_iff fresh_Pair_elim fresh_at_base)[2]
-  defer defer
-  defer
-  apply (simp add: Abs1_eq_iff fresh_at_base lt.fresh)
-  apply (rule arg_cong) back
-  defer
-  apply (rule arg_cong) back
-  defer
-  apply (rule arg_cong) back
-  defer
-  oops --"The goals seem reasonable"
-
-end
diff -r b6873d123f9b -r 89715c48f728 Nominal/Ex/CPS/CPS3_DanvyFilinski.thy
--- a/Nominal/Ex/CPS/CPS3_DanvyFilinski.thy	Sat May 12 21:39:09 2012 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,252 +0,0 @@
-header {* CPS transformation of Danvy and Filinski *}
-theory CPS3_DanvyFilinski imports Lt begin
-
-nominal_primrec
-  CPS1 :: "lt \<Rightarrow> (lt \<Rightarrow> lt) \<Rightarrow> lt" ("_*_"  [100,100] 100)
-and
-  CPS2 :: "lt \<Rightarrow> lt \<Rightarrow> lt" ("_^_" [100,100] 100)
-where
-  "eqvt k \<Longrightarrow> (x~)*k = k (x~)"
-| "eqvt k \<Longrightarrow> (M$N)*k = M*(%m. (N*(%n.((m $ n) $ (Lam c (k (c~)))))))"
-| "eqvt k \<Longrightarrow> atom c \<sharp> (x, M) \<Longrightarrow> (Lam x M)*k = k (Lam x (Lam c (M^(c~))))"
-| "\<not>eqvt k \<Longrightarrow> (CPS1 t k) = t"
-| "(x~)^l = l $ (x~)"
-| "(M$N)^l = M*(%m. (N*(%n.((m $ n) $ l))))"
-| "atom c \<sharp> (x, M) \<Longrightarrow> (Lam x M)^l = l $ (Lam x (Lam c (M^(c~))))"
-  apply (simp only: eqvt_def CPS1_CPS2_graph_def)
-  apply (rule, perm_simp, rule)
-  apply auto
-  apply (case_tac x)
-  apply (case_tac a)
-  apply (case_tac "eqvt b")
-  apply (rule_tac y="aa" in lt.strong_exhaust)
-  apply auto[4]
-  apply (rule_tac x="(name, lt)" and ?'a="name" in obtain_fresh)
-  apply (simp add: fresh_at_base Abs1_eq_iff)
-  apply (case_tac b)
-  apply (rule_tac y="a" in lt.strong_exhaust)
-  apply auto[3]
-  apply blast+
-  apply (rule_tac x="(name, lt)" and ?'a="name" in obtain_fresh) 
-  apply (simp add: fresh_at_base Abs1_eq_iff)
---"-"
-  apply (subgoal_tac "Lam c (ka (c~)) = Lam ca (ka (ca~))")
-  apply (simp only:)
-  apply (simp add: Abs1_eq_iff)
-  apply (case_tac "c=ca")
-  apply simp_all[2]
-  apply rule
-  apply (perm_simp)
-  apply (simp add: eqvt_def)
-  apply (simp add: fresh_def)
-  apply (rule contra_subsetD[OF supp_fun_app])
-  back
-  apply (simp add: supp_fun_eqvt lt.supp supp_at_base)
---"-"
-  apply (rule arg_cong)
-  back
-  apply simp
-  apply (thin_tac "eqvt ka")
-  apply (rule_tac x="(c, ca, x, xa, M, Ma)" and ?'a="name" in obtain_fresh)
-  apply (subgoal_tac "Lam c (CPS1_CPS2_sumC (Inr (M, c~))) = Lam a (CPS1_CPS2_sumC (Inr (M, a~)))")
-  prefer 2
-  apply (simp add: Abs1_eq_iff')
-  apply (case_tac "c = a")
-  apply simp_all[2]
-  apply rule
-  apply (simp add: eqvt_at_def)
-  apply (simp add: swap_fresh_fresh fresh_Pair_elim)
-  apply (erule fresh_eqvt_at)
-  apply (simp add: supp_Inr finite_supp)
-  apply (simp add: fresh_Inr fresh_Pair lt.fresh fresh_at_base)
-  apply (subgoal_tac "Lam ca (CPS1_CPS2_sumC (Inr (Ma, ca~))) = Lam a (CPS1_CPS2_sumC (Inr (Ma, a~)))")
-  prefer 2
-  apply (simp add: Abs1_eq_iff')
-  apply (case_tac "ca = a")
-  apply simp_all[2]
-  apply rule
-  apply (simp add: eqvt_at_def)
-  apply (simp add: swap_fresh_fresh fresh_Pair_elim)
-  apply (erule fresh_eqvt_at)
-  apply (simp add: supp_Inr finite_supp)
-  apply (simp add: fresh_Inr fresh_Pair lt.fresh fresh_at_base)
-  apply (simp only: )
-  apply (erule Abs_lst1_fcb)
-  apply (simp add: Abs_fresh_iff)
-  apply (drule sym)
-  apply (simp only:)
-  apply (simp add: Abs_fresh_iff lt.fresh)
-  apply clarify
-  apply (erule fresh_eqvt_at)
-  apply (simp add: supp_Inr finite_supp)
-  apply (simp add: fresh_Inr fresh_Pair lt.fresh fresh_at_base)
-  apply (drule sym)
-  apply (drule sym)
-  apply (drule sym)
-  apply (simp only:)
-  apply (thin_tac "Lam a (CPS1_CPS2_sumC (Inr (M, a~))) = Lam c (CPS1_CPS2_sumC (Inr (M, c~)))")
-  apply (thin_tac "Lam a (CPS1_CPS2_sumC (Inr (Ma, a~))) = Lam ca (CPS1_CPS2_sumC (Inr (Ma, ca~)))")
-  apply (thin_tac "atom a \<sharp> (c, ca, x, xa, M, Ma)")
-  apply (simp add: fresh_Pair_elim)
-  apply (subst iffD1[OF meta_eq_to_obj_eq[OF eqvt_at_def]])
-  back
-  back
-  back
-  apply assumption
-  apply (simp add: Abs1_eq_iff' fresh_Pair_elim fresh_at_base swap_fresh_fresh lt.fresh)
-  apply (case_tac "(atom x \<rightleftharpoons> atom xa) \<bullet> c = ca")
-  apply simp_all[3]
-  apply rule
-  apply (case_tac "c = xa")
-  apply simp_all[2]
-  apply (rotate_tac 1)
-  apply (drule_tac q="(atom ca \<rightleftharpoons> atom x)" in eqvt_at_perm)
-  apply (simp add: swap_fresh_fresh)
-  apply (simp add: eqvt_at_def swap_fresh_fresh)
-  apply (thin_tac "eqvt_at CPS1_CPS2_sumC (Inr (M, c~))")
-  apply (simp add: eqvt_at_def)
-  apply (drule_tac x="(atom ca \<rightleftharpoons> atom c)" in spec)
-  apply simp
-  apply (metis (no_types) atom_eq_iff fresh_permute_iff permute_swap_cancel swap_atom_simps(3) swap_fresh_fresh)
-  apply (case_tac "c = xa")
-  apply simp
-  apply (subgoal_tac "((ca \<leftrightarrow> x) \<bullet> (atom x)) \<sharp> (ca \<leftrightarrow> x) \<bullet> CPS1_CPS2_sumC (Inr (Ma, ca~))")
-  apply (simp add: atom_eqvt eqvt_at_def)
-  apply (simp add: flip_fresh_fresh)
-  apply (subst fresh_permute_iff)
-  apply (erule fresh_eqvt_at)
-  apply (simp add: supp_Inr finite_supp)
-  apply (simp add: fresh_Inr lt.fresh fresh_at_base fresh_Pair)
-  apply simp
-  apply clarify
-  apply (subgoal_tac "atom ca \<sharp> (atom x \<rightleftharpoons> atom xa) \<bullet> CPS1_CPS2_sumC (Inr (M, c~))")
-  apply (simp add: eqvt_at_def)
-  apply (subgoal_tac "(atom x \<rightleftharpoons> atom xa) \<bullet> atom ca \<sharp> CPS1_CPS2_sumC (Inr (M, c~))")
-  apply (metis Nominal2_Base.swap_commute fresh_permute_iff permute_swap_cancel2)
-  apply (erule fresh_eqvt_at)
-  apply (simp add: finite_supp supp_Inr)
-  apply (simp add: fresh_Inr fresh_Pair lt.fresh)
-  apply rule
-  apply (metis Nominal2_Base.swap_commute fresh_permute_iff permute_swap_cancel2)
-  apply (simp add: fresh_def supp_at_base)
-  apply (metis atom_eq_iff permute_swap_cancel2 swap_atom_simps(3))
---"-"
-  apply (rule_tac x="(c, ca, x, xa, M, Ma)" and ?'a="name" in obtain_fresh)
-  apply (subgoal_tac "Lam c (CPS1_CPS2_sumC (Inr (M, c~))) = Lam a (CPS1_CPS2_sumC (Inr (M, a~)))")
-  prefer 2
-  apply (simp add: Abs1_eq_iff')
-  apply (case_tac "c = a")
-  apply simp_all[2]
-  apply rule
-  apply (simp add: eqvt_at_def)
-  apply (simp add: swap_fresh_fresh fresh_Pair_elim)
-  apply (erule fresh_eqvt_at)
-  apply (simp add: supp_Inr finite_supp)
-  apply (simp add: fresh_Inr fresh_Pair lt.fresh fresh_at_base)
-  apply (subgoal_tac "Lam ca (CPS1_CPS2_sumC (Inr (Ma, ca~))) = Lam a (CPS1_CPS2_sumC (Inr (Ma, a~)))")
-  prefer 2
-  apply (simp add: Abs1_eq_iff')
-  apply (case_tac "ca = a")
-  apply simp_all[2]
-  apply rule
-  apply (simp add: eqvt_at_def)
-  apply (simp add: swap_fresh_fresh fresh_Pair_elim)
-  apply (erule fresh_eqvt_at)
-  apply (simp add: supp_Inr finite_supp)
-  apply (simp add: fresh_Inr fresh_Pair lt.fresh fresh_at_base)
-  apply (simp only: )
-  apply (erule Abs_lst1_fcb)
-  apply (simp add: Abs_fresh_iff)
-  apply (drule sym)
-  apply (simp only:)
-  apply (simp add: Abs_fresh_iff lt.fresh)
-  apply clarify
-  apply (erule fresh_eqvt_at)
-  apply (simp add: supp_Inr finite_supp) (* TODO put sum of fs into fs typeclass *)
-  apply (simp add: fresh_Inr fresh_Pair lt.fresh fresh_at_base)
-  apply (drule sym)
-  apply (drule sym)
-  apply (drule sym)
-  apply (simp only:)
-  apply (thin_tac "Lam a (CPS1_CPS2_sumC (Inr (M, a~))) = Lam c (CPS1_CPS2_sumC (Inr (M, c~)))")
-  apply (thin_tac "Lam a (CPS1_CPS2_sumC (Inr (Ma, a~))) = Lam ca (CPS1_CPS2_sumC (Inr (Ma, ca~)))")
-  apply (thin_tac "atom a \<sharp> (c, ca, x, xa, M, Ma)")
-  apply (simp add: fresh_Pair_elim)
-  apply (subst iffD1[OF meta_eq_to_obj_eq[OF eqvt_at_def]])
-  back
-  back
-  back
-  apply assumption
-  apply (simp add: Abs1_eq_iff' fresh_Pair_elim fresh_at_base swap_fresh_fresh lt.fresh)
-  apply (case_tac "(atom x \<rightleftharpoons> atom xa) \<bullet> c = ca")
-  apply simp_all[3]
-  apply rule
-  apply (case_tac "c = xa")
-  apply simp_all[2]
-  apply (rotate_tac 1)
-  apply (drule_tac q="(atom ca \<rightleftharpoons> atom x)" in eqvt_at_perm)
-  apply (simp add: swap_fresh_fresh)
-  apply (simp add: eqvt_at_def swap_fresh_fresh)
-  apply (thin_tac "eqvt_at CPS1_CPS2_sumC (Inr (M, c~))")
-  apply (simp add: eqvt_at_def)
-  apply (drule_tac x="(atom ca \<rightleftharpoons> atom c)" in spec)
-  apply simp
-  apply (metis (no_types) atom_eq_iff fresh_permute_iff permute_swap_cancel swap_atom_simps(3) swap_fresh_fresh)
-  apply (case_tac "c = xa")
-  apply simp
-  apply (subgoal_tac "((ca \<leftrightarrow> x) \<bullet> (atom x)) \<sharp> (ca \<leftrightarrow> x) \<bullet> CPS1_CPS2_sumC (Inr (Ma, ca~))")
-  apply (simp add: atom_eqvt eqvt_at_def)
-  apply (simp add: flip_fresh_fresh)
-  apply (subst fresh_permute_iff)
-  apply (erule fresh_eqvt_at)
-  apply (simp add: supp_Inr finite_supp)
-  apply (simp add: fresh_Inr lt.fresh fresh_at_base fresh_Pair)
-  apply simp
-  apply clarify
-  apply (subgoal_tac "atom ca \<sharp> (atom x \<rightleftharpoons> atom xa) \<bullet> CPS1_CPS2_sumC (Inr (M, c~))")
-  apply (simp add: eqvt_at_def)
-  apply (subgoal_tac "(atom x \<rightleftharpoons> atom xa) \<bullet> atom ca \<sharp> CPS1_CPS2_sumC (Inr (M, c~))")
-  apply (metis Nominal2_Base.swap_commute fresh_permute_iff permute_swap_cancel2)
-  apply (erule fresh_eqvt_at)
-  apply (simp add: finite_supp supp_Inr)
-  apply (simp add: fresh_Inr fresh_Pair lt.fresh)
-  apply rule
-  apply (metis Nominal2_Base.swap_commute fresh_permute_iff permute_swap_cancel2)
-  apply (simp add: fresh_def supp_at_base)
-  apply (metis atom_eq_iff permute_swap_cancel2 swap_atom_simps(3))
-  done
-
-termination (eqvt)
-  by lexicographic_order
-
-definition psi:: "lt => lt"
-  where [simp]: "psi V == V*(\<lambda>x. x)"
-
-section {* Simple consequence of CPS *}
-
-lemma [simp]: "eqvt (\<lambda>x\<Colon>lt. x)"
-  by (simp add: eqvt_def eqvt_bound eqvt_lambda)
-
-lemma value_eq1 : "isValue V \<Longrightarrow> eqvt k \<Longrightarrow> V*k = k (psi V)"
-  apply (cases V rule: lt.exhaust)
-  apply simp_all
-  apply (rule_tac x="(name, lt)" and ?'a="name" in obtain_fresh)
-  apply simp
-  done
-
-lemma value_eq2 : "isValue V \<Longrightarrow> V^K = K $ (psi V)"
-  apply (cases V rule: lt.exhaust)
-  apply simp_all
-  apply (rule_tac x="(name, lt)" and ?'a="name" in obtain_fresh)
-  apply simp
-  done
-
-lemma value_eq3' : "~isValue M \<Longrightarrow> eqvt k \<Longrightarrow> M*k = (M^(Lam n (k (Var n))))"
-  by (cases M rule: lt.exhaust) auto
-
-
-
-end
-
-
-
diff -r b6873d123f9b -r 89715c48f728 Nominal/Ex/CPS/CPS3_DanvyFilinski_FCB2.thy
--- a/Nominal/Ex/CPS/CPS3_DanvyFilinski_FCB2.thy	Sat May 12 21:39:09 2012 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,83 +0,0 @@
-header {* CPS transformation of Danvy and Filinski *}
-theory CPS3_DanvyFilinski imports Lt begin
-
-nominal_primrec
-  CPS1 :: "lt \<Rightarrow> (lt \<Rightarrow> lt) \<Rightarrow> lt" ("_*_"  [100,100] 100)
-and
-  CPS2 :: "lt \<Rightarrow> lt \<Rightarrow> lt" ("_^_" [100,100] 100)
-where
-  "eqvt k \<Longrightarrow> (x~)*k = k (x~)"
-| "eqvt k \<Longrightarrow> (M$N)*k = M*(%m. (N*(%n.((m $ n) $ (Lam c (k (c~)))))))"
-| "eqvt k \<Longrightarrow> atom c \<sharp> (x, M) \<Longrightarrow> (Lam x M)*k = k (Lam x (Lam c (M^(c~))))"
-| "\<not>eqvt k \<Longrightarrow> (CPS1 t k) = t"
-| "(x~)^l = l $ (x~)"
-| "(M$N)^l = M*(%m. (N*(%n.((m $ n) $ l))))"
-| "atom c \<sharp> (x, M) \<Longrightarrow> (Lam x M)^l = l $ (Lam x (Lam c (M^(c~))))"
-  apply (simp only: eqvt_def CPS1_CPS2_graph_def)
-  apply (rule, perm_simp, rule)
-  apply auto
-  apply (case_tac x)
-  apply (case_tac a)
-  apply (case_tac "eqvt b")
-  apply (rule_tac y="aa" in lt.strong_exhaust)
-  apply auto[4]
-  apply (rule_tac x="(name, lt)" and ?'a="name" in obtain_fresh)
-  apply (simp add: fresh_at_base Abs1_eq_iff)
-  apply (case_tac b)
-  apply (rule_tac y="a" in lt.strong_exhaust)
-  apply auto[3]
-  apply blast
-  apply (rule_tac x="(name, lt)" and ?'a="name" in obtain_fresh) 
-  apply (simp add: fresh_at_base Abs1_eq_iff)
-  apply blast
---"-"
-  apply (subgoal_tac "Lam c (ka (c~)) = Lam ca (ka (ca~))")
-  apply (simp only:)
-  apply (simp add: Abs1_eq_iff)
-  apply (case_tac "c=ca")
-  apply simp_all[2]
-  apply rule
-  apply (perm_simp)
-  apply (simp add: eqvt_def)
-  apply (simp add: fresh_def)
-  apply (rule contra_subsetD[OF supp_fun_app])
-  back
-  apply (simp add: supp_fun_eqvt lt.supp supp_at_base)
---"-"
-  apply (rule arg_cong)
-  back
-  apply (thin_tac "eqvt ka")
-  apply (rule_tac x="(c, ca, x, xa, M, Ma)" and ?'a="name" in obtain_fresh)
-  apply (subgoal_tac "Lam c (CPS1_CPS2_sumC (Inr (M, c~))) = Lam a (CPS1_CPS2_sumC (Inr (M, a~)))")
-  prefer 2
-  apply (simp add: Abs1_eq_iff')
-  apply (case_tac "c = a")
-  apply simp_all[2]
-  apply rule
-  apply (simp add: eqvt_at_def)
-  apply (simp add: swap_fresh_fresh fresh_Pair_elim)
-  apply (erule fresh_eqvt_at)
-  apply (simp add: supp_Inr finite_supp)
-  apply (simp add: fresh_Inr fresh_Pair lt.fresh fresh_at_base)
-  apply (subgoal_tac "Lam ca (CPS1_CPS2_sumC (Inr (Ma, ca~))) = Lam a (CPS1_CPS2_sumC (Inr (Ma, a~)))")
-  prefer 2
-  apply (simp add: Abs1_eq_iff')
-  apply (case_tac "ca = a")
-  apply simp_all[2]
-  apply rule
-  apply (simp add: eqvt_at_def)
-  apply (simp add: swap_fresh_fresh fresh_Pair_elim)
-  apply (erule fresh_eqvt_at)
-  apply (simp add: supp_Inr finite_supp)
-  apply (simp add: fresh_Inr fresh_Pair lt.fresh fresh_at_base)
-  apply (simp only:)
-  apply (simp (no_asm))
-  apply (erule_tac c="a" in Abs_lst1_fcb2')
-  apply (simp add: Abs_fresh_iff lt.fresh)
-  apply (simp add: fresh_star_def fresh_Pair_elim lt.fresh fresh_at_base)
-  oops
-
-end
-
-
-
diff -r b6873d123f9b -r 89715c48f728 Nominal/Ex/CPS/Lt.thy
--- a/Nominal/Ex/CPS/Lt.thy	Sat May 12 21:39:09 2012 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,117 +0,0 @@
-header {* The Call-by-Value Lambda Calculus *}
-theory Lt
-imports "../../Nominal2"
-begin
-
-atom_decl name
-
-nominal_datatype lt =
-    Var name       ("_~"  [150] 149)
-  | App lt lt         (infixl "$" 100)
-  | Lam x::"name" t::"lt"  binds  x in t
-
-nominal_primrec
-  subst :: "lt \<Rightarrow> name \<Rightarrow> lt \<Rightarrow> lt"  ("_ [_ ::= _]" [90, 90, 90] 90)
-where
-  "(Var x)[y ::= s] = (if x = y then s else (Var x))"
-| "(App t1 t2)[y ::= s] = App (t1[y ::= s]) (t2[y ::= s])"
-| "atom x \<sharp> (y, s) \<Longrightarrow> (Lam x t)[y ::= s] = Lam x (t[y ::= s])"
-  unfolding eqvt_def subst_graph_def
-  apply (rule, perm_simp, rule)
-  apply(rule TrueI)
-  apply(auto simp add: lt.distinct lt.eq_iff)
-  apply(rule_tac y="a" and c="(aa, b)" in lt.strong_exhaust)
-  apply blast
-  apply(simp_all add: fresh_star_def fresh_Pair_elim)
-  apply blast
-  apply (erule_tac c="(ya,sa)" in Abs_lst1_fcb2)
-  apply(simp_all add: Abs_fresh_iff)
-  apply(simp add: fresh_star_def fresh_Pair)
-  apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)+
-done
-
-termination (eqvt) by lexicographic_order
-
-lemma forget[simp]:
-  shows "atom x \<sharp> M \<Longrightarrow> M[x ::= s] = M"
-  by (nominal_induct M avoiding: x s rule: lt.strong_induct)
-     (auto simp add: lt.fresh fresh_at_base)
-
-lemma [simp]: "supp (M[x ::= V]) <= (supp(M) - {atom x}) Un (supp V)"
-  by (nominal_induct M avoiding: x V rule: lt.strong_induct)
-     (auto simp add: lt.supp supp_at_base, blast, blast)
-
-nominal_primrec
-  isValue:: "lt => bool"
-where
-  "isValue (Var x) = True"
-| "isValue (Lam y N) = True"
-| "isValue (A $ B) = False"
-  unfolding eqvt_def isValue_graph_def
-  by (perm_simp, auto)
-     (erule lt.exhaust, auto)
-
-termination (eqvt)
-  by (relation "measure size") (simp_all)
-
-inductive
-  eval :: "[lt, lt] \<Rightarrow> bool" (" _ \<longrightarrow>\<^isub>\<beta> _" [80,80] 80)
-  where
-   evbeta: "\<lbrakk>atom x\<sharp>V; isValue V\<rbrakk> \<Longrightarrow> ((Lam x M) $ V) \<longrightarrow>\<^isub>\<beta> (M[x ::= V])"
-|  ev1: "\<lbrakk>isValue V; M \<longrightarrow>\<^isub>\<beta> M' \<rbrakk> \<Longrightarrow> (V $ M) \<longrightarrow>\<^isub>\<beta> (V $ M')"
-|  ev2: "M \<longrightarrow>\<^isub>\<beta> M' \<Longrightarrow> (M $ N) \<longrightarrow>\<^isub>\<beta> (M' $ N)"
-
-equivariance eval
-
-nominal_inductive eval
-done
-
-(*lemmas [simp] = lt.supp(2)*)
-
-lemma closedev1: assumes "s \<longrightarrow>\<^isub>\<beta> t"
-  shows "supp t <= supp s"
-  using assms
-    by (induct, auto simp add: lt.supp)
-
-
-lemma [simp]: "~ ((Lam x M) \<longrightarrow>\<^isub>\<beta> N)"
-by (rule, erule eval.cases, simp_all)
-
-lemma [simp]: assumes "M \<longrightarrow>\<^isub>\<beta> N" shows "~ isValue M"
-using assms
-by (cases, auto)
-
-
-inductive
-  eval_star :: "[lt, lt] \<Rightarrow> bool" (" _ \<longrightarrow>\<^isub>\<beta>\<^sup>* _" [80,80] 80)
-  where
-   evs1: "M \<longrightarrow>\<^isub>\<beta>\<^sup>* M"
-|  evs2: "\<lbrakk>M \<longrightarrow>\<^isub>\<beta> M'; M' \<longrightarrow>\<^isub>\<beta>\<^sup>*  M'' \<rbrakk> \<Longrightarrow> M \<longrightarrow>\<^isub>\<beta>\<^sup>*  M''"
-
-lemma eval_evs: assumes *: "M \<longrightarrow>\<^isub>\<beta> M'" shows "M \<longrightarrow>\<^isub>\<beta>\<^sup>* M'"
-by (rule evs2, rule *, rule evs1)
-
-lemma eval_trans[trans]:
-  assumes "M1  \<longrightarrow>\<^isub>\<beta>\<^sup>* M2"
-      and "M2  \<longrightarrow>\<^isub>\<beta>\<^sup>*  M3"
-  shows "M1  \<longrightarrow>\<^isub>\<beta>\<^sup>* M3"
-  using assms
-  by (induct, auto intro: evs2)
-
-lemma evs3[rule_format]: assumes "M1  \<longrightarrow>\<^isub>\<beta>\<^sup>* M2"
-  shows "M2  \<longrightarrow>\<^isub>\<beta> M3 \<longrightarrow> M1  \<longrightarrow>\<^isub>\<beta>\<^sup>* M3"
-  using assms
-    by (induct, auto intro: eval_evs evs2)
-
-equivariance eval_star
-
-lemma evbeta':
-  fixes x :: name
-  assumes "isValue V" and "atom x\<sharp>V" and "N = (M[x ::= V])"
-  shows "((Lam x M) $ V) \<longrightarrow>\<^isub>\<beta>\<^sup>* N"
-  using assms by simp (rule evs2, rule evbeta, simp_all add: evs1)
-
-end
-
-
-
diff -r b6873d123f9b -r 89715c48f728 Nominal/Ex/FiniteType.thy
--- a/Nominal/Ex/FiniteType.thy	Sat May 12 21:39:09 2012 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,19 +0,0 @@
-theory FiniteType
-imports "../Nominal2"
-begin
-
-typedef ('a::pt, 'b::fs) ffun = "{f::'a => 'b. finite (supp f)}"
-apply(rule_tac x="\<lambda>_. undefined::'b::fs" in exI)
-apply(auto)
-apply(rule_tac S="supp (undefined::'b::fs)" in supports_finite)
-apply(simp add: supports_def)
-apply(perm_simp)
-apply(simp add: fresh_def[symmetric])
-apply(simp add: swap_fresh_fresh)
-apply(simp add: finite_supp)
-done
-
-
-
-
-end
\ No newline at end of file
diff -r b6873d123f9b -r 89715c48f728 Nominal/Ex/Finite_Alpha.thy
--- a/Nominal/Ex/Finite_Alpha.thy	Sat May 12 21:39:09 2012 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,124 +0,0 @@
-theory Finite_Alpha
-imports "../Nominal2"
-begin
-
-lemma
-  assumes "(supp x - as) \<sharp>* p"
-      and "p \<bullet> x = y"
-      and "p \<bullet> as = bs"
-    shows "(as, x) \<approx>set (op =) supp p (bs, y)"
-  using assms unfolding alphas
-  apply(simp)
-  apply(clarify)
-  apply(simp only: Diff_eqvt[symmetric] supp_eqvt[symmetric])
-  apply(simp only: atom_set_perm_eq)
-  done
-
-
-lemma
-  assumes "(supp x - set as) \<sharp>* p"
-      and "p \<bullet> x = y"
-      and "p \<bullet> as = bs"
-    shows "(as, x) \<approx>lst (op =) supp p (bs, y)"
-  using assms unfolding alphas
-  apply(simp)
-  apply(clarify)
-  apply(simp only: set_eqvt[symmetric] Diff_eqvt[symmetric] supp_eqvt[symmetric])
-  apply(simp only: atom_set_perm_eq)
-  done
-
-lemma
-  assumes "(supp x - as) \<sharp>* p"
-      and "p \<bullet> x = y"
-      and "p \<bullet> (as \<inter> supp x) = bs \<inter> supp y"
-      and "finite (supp x)"
-  shows "(as, x) \<approx>res (op =) supp p (bs, y)"
-  using assms
-  unfolding alpha_res_alpha_set
-  unfolding alphas
-  apply simp
-  apply rule
-  apply (rule trans)
-  apply (rule supp_perm_eq[symmetric, of _ p])
-  apply (simp add: supp_finite_atom_set fresh_star_def)
-  apply(auto)[1]
-  apply(simp only: Diff_eqvt inter_eqvt supp_eqvt)
-  apply (simp add: fresh_star_def)
-  apply blast
-  done
-
-lemma
-  assumes "(as, x) \<approx>res (op =) supp p (bs, y)"
-  shows "(supp x - as) \<sharp>* p"
-    and "p \<bullet> (as \<inter> supp x) = bs \<inter> supp y"
-    and "p \<bullet> x = y"
-  using assms
-  apply -
-  prefer 3
-  apply (auto simp add: alphas)[2]
-  unfolding alpha_res_alpha_set
-  unfolding alphas
-  by blast
-
-(* On the raw level *)
-
-atom_decl name
-
-nominal_datatype lam =
-  Var "name"
-| App "lam" "lam"
-| Lam x::"name" l::"lam"  binds x in l ("Lam [_]. _" [100, 100] 100)
-
-thm alpha_lam_raw.intros(3)[unfolded alphas, simplified]
-
-lemma alpha_fv: "alpha_lam_raw l r \<Longrightarrow> fv_lam_raw l = fv_lam_raw r"
-  by (induct rule: alpha_lam_raw.induct) (simp_all add: alphas)
-
-lemma finite_fv_raw: "finite (fv_lam_raw l)"
-  by (induct rule: lam_raw.induct) (simp_all add: supp_at_base)
-
-lemma "(fv_lam_raw l - {atom n}) \<sharp>* p \<Longrightarrow> alpha_lam_raw (p \<bullet> l) r \<Longrightarrow>
-  fv_lam_raw l - {atom n} = fv_lam_raw r - {atom (p \<bullet> n)}"
-  apply (rule trans)
-  apply (rule supp_perm_eq[symmetric])
-  apply (subst supp_finite_atom_set)
-  apply (rule finite_Diff)
-  apply (rule finite_fv_raw)
-  apply assumption
-  apply (simp add: eqvts)
-  apply (subst alpha_fv)
-  apply assumption
-  apply (rule)
-  done
-
-(* For the res binding *)
-
-nominal_datatype ty2 =
-  Var2 "name"
-| Fun2 "ty2" "ty2"
-
-nominal_datatype tys2 =
-  All2 xs::"name fset" ty::"ty2" binds (set+) xs in ty
-
-lemma alpha_fv': "alpha_tys2_raw l r \<Longrightarrow> fv_tys2_raw l = fv_tys2_raw r"
-  by (induct rule: alpha_tys2_raw.induct) (simp_all add: alphas)
-
-lemma finite_fv_raw': "finite (fv_tys2_raw l)"
-  by (induct rule: tys2_raw.induct) (simp_all add: supp_at_base finite_supp)
-
-thm alpha_tys2_raw.intros[unfolded alphas, simplified]
-
-lemma "(supp x - atom ` (fset as)) \<sharp>* p \<Longrightarrow> p \<bullet> (x :: tys2) = y \<Longrightarrow>
-  p \<bullet> (atom ` (fset as) \<inter> supp x) = atom ` (fset bs) \<inter> supp y \<Longrightarrow>
-  supp x - atom ` (fset as) = supp y - atom ` (fset bs)"
-  apply (rule trans)
-  apply (rule supp_perm_eq[symmetric])
-  apply (subst supp_finite_atom_set)
-  apply (rule finite_Diff)
-  apply (rule finite_supp)
-  apply assumption
-  apply (simp add: eqvts)
-  apply blast
-  done
-
-end
diff -r b6873d123f9b -r 89715c48f728 Nominal/Ex/LamTest.thy
--- a/Nominal/Ex/LamTest.thy	Sat May 12 21:39:09 2012 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,1894 +0,0 @@
-theory LamTest
-imports "../Nominal2" 
-begin
-
-atom_decl name
-
-nominal_datatype lam =
-  Var "name"
-| App "lam" "lam"
-| Lam x::"name" l::"lam"  bind x in l
-
-
-ML {*
-
-val trace = Unsynchronized.ref false
-fun trace_msg msg = if ! trace then tracing (msg ()) else ()
-
-val boolT = HOLogic.boolT
-val mk_eq = HOLogic.mk_eq
-
-open Function_Lib
-open Function_Common
-
-datatype globals = Globals of
- {fvar: term,
-  domT: typ,
-  ranT: typ,
-  h: term,
-  y: term,
-  x: term,
-  z: term,
-  a: term,
-  P: term,
-  D: term,
-  Pbool:term}
-
-datatype rec_call_info = RCInfo of
- {RIvs: (string * typ) list,  (* Call context: fixes and assumes *)
-  CCas: thm list,
-  rcarg: term,                 (* The recursive argument *)
-  llRI: thm,
-  h_assum: term}
-
-
-datatype clause_context = ClauseContext of
- {ctxt : Proof.context,
-  qs : term list,
-  gs : term list,
-  lhs: term,
-  rhs: term,
-  cqs: cterm list,
-  ags: thm list,
-  case_hyp : thm}
-
-
-fun transfer_clause_ctx thy (ClauseContext { ctxt, qs, gs, lhs, rhs, cqs, ags, case_hyp }) =
-  ClauseContext { ctxt = ProofContext.transfer thy ctxt,
-    qs = qs, gs = gs, lhs = lhs, rhs = rhs, cqs = cqs, ags = ags, case_hyp = case_hyp }
-
-
-datatype clause_info = ClauseInfo of
- {no: int,
-  qglr : ((string * typ) list * term list * term * term),
-  cdata : clause_context,
-  tree: Function_Ctx_Tree.ctx_tree,
-  lGI: thm,
-  RCs: rec_call_info list}
-*}
-
-thm accp_induct_rule
-
-ML {*
-(* Theory dependencies. *)
-val acc_induct_rule = @{thm accp_induct_rule}
-
-val ex1_implies_ex = @{thm FunDef.fundef_ex1_existence}
-val ex1_implies_un = @{thm FunDef.fundef_ex1_uniqueness}
-val ex1_implies_iff = @{thm FunDef.fundef_ex1_iff}
-
-val acc_downward = @{thm accp_downward}
-val accI = @{thm accp.accI}
-val case_split = @{thm HOL.case_split}
-val fundef_default_value = @{thm FunDef.fundef_default_value}
-val not_acc_down = @{thm not_accp_down}
-*}
-
-
-ML {*
-fun find_calls tree =
-  let
-    fun add_Ri (fixes,assumes) (_ $ arg) _ (_, xs) =
-      ([], (fixes, assumes, arg) :: xs)
-      | add_Ri _ _ _ _ = raise Match
-  in
-    rev (Function_Ctx_Tree.traverse_tree add_Ri tree [])
-  end
-*}
-
-ML {*
-fun mk_eqvt_at (f_trm, arg_trm) =
-  let
-    val f_ty = fastype_of f_trm
-    val arg_ty = domain_type f_ty
-  in
-    Const (@{const_name eqvt_at}, [f_ty, arg_ty] ---> @{typ bool}) $ f_trm $ arg_trm
-    |> HOLogic.mk_Trueprop
-  end
-*}
-
-ML {*
-fun find_calls2 f t = 
-  let
-    fun aux (g $ arg) = aux g #> aux arg #> (if f = g then cons ((g, arg)) else I)
-      | aux (Abs (_, _, t)) = aux t 
-      | aux _ = I
-  in
-    aux t []
-  end 
-*}
-
-
-ML {*
-(** building proof obligations *)
-
-fun mk_compat_proof_obligations domT ranT fvar f glrs =
-  let
-    fun mk_impl ((qs, gs, lhs, rhs), (qs', gs', lhs', rhs')) =
-      let
-        val shift = incr_boundvars (length qs')
-
-        val RCs_rhs  = find_calls2 fvar rhs
-        val RCs_rhs' = find_calls2 fvar rhs'
-      in
-        Logic.mk_implies
-          (HOLogic.mk_Trueprop (HOLogic.eq_const domT $ shift lhs $ lhs'),
-            HOLogic.mk_Trueprop (HOLogic.eq_const ranT $ shift rhs $ rhs'))
-        |> fold_rev (curry Logic.mk_implies) (map shift gs @ gs')
-        |> fold_rev (curry Logic.mk_implies) (map (shift o mk_eqvt_at) RCs_rhs) (* HERE *) 
-        (*|> fold_rev (curry Logic.mk_implies) (map mk_eqvt_at RCs_rhs')*) (* HERE *) 
-        |> fold_rev (fn (n,T) => fn b => Term.all T $ Abs(n,T,b)) (qs @ qs')
-        |> curry abstract_over fvar
-        |> curry subst_bound f
-      end
-  in
-    map mk_impl (unordered_pairs glrs)
-  end
-*}
-
-ML {*
-fun mk_completeness (Globals {x, Pbool, ...}) clauses qglrs =
-  let
-    fun mk_case (ClauseContext {qs, gs, lhs, ...}, (oqs, _, _, _)) =
-      HOLogic.mk_Trueprop Pbool
-      |> curry Logic.mk_implies (HOLogic.mk_Trueprop (mk_eq (x, lhs)))
-      |> fold_rev (curry Logic.mk_implies) gs
-      |> fold_rev mk_forall_rename (map fst oqs ~~ qs)
-  in
-    HOLogic.mk_Trueprop Pbool
-    |> fold_rev (curry Logic.mk_implies o mk_case) (clauses ~~ qglrs)
-    |> mk_forall_rename ("x", x)
-    |> mk_forall_rename ("P", Pbool)
-  end
-*}
-
-(** making a context with it's own local bindings **)
-ML {*
-
-fun mk_clause_context x ctxt (pre_qs,pre_gs,pre_lhs,pre_rhs) =
-  let
-    val (qs, ctxt') = Variable.variant_fixes (map fst pre_qs) ctxt
-      |>> map2 (fn (_, T) => fn n => Free (n, T)) pre_qs
-
-    val thy = ProofContext.theory_of ctxt'
-
-    fun inst t = subst_bounds (rev qs, t)
-    val gs = map inst pre_gs
-    val lhs = inst pre_lhs
-    val rhs = inst pre_rhs
-
-    val cqs = map (cterm_of thy) qs
-    val ags = map (Thm.assume o cterm_of thy) gs
-
-    val case_hyp = Thm.assume (cterm_of thy (HOLogic.mk_Trueprop (mk_eq (x, lhs))))
-  in
-    ClauseContext { ctxt = ctxt', qs = qs, gs = gs, lhs = lhs, rhs = rhs,
-      cqs = cqs, ags = ags, case_hyp = case_hyp }
-  end
-*}
-
-ML {*
-(* lowlevel term function. FIXME: remove *)
-fun abstract_over_list vs body =
-  let
-    fun abs lev v tm =
-      if v aconv tm then Bound lev
-      else
-        (case tm of
-          Abs (a, T, t) => Abs (a, T, abs (lev + 1) v t)
-        | t $ u => abs lev v t $ abs lev v u
-        | t => t)
-  in
-    fold_index (fn (i, v) => fn t => abs i v t) vs body
-  end
-
-
-
-fun mk_clause_info globals G f no cdata qglr tree RCs GIntro_thm RIntro_thms =
-  let
-    val Globals {h, ...} = globals
-
-    val ClauseContext { ctxt, qs, cqs, ags, ... } = cdata
-    val cert = Thm.cterm_of (ProofContext.theory_of ctxt)
-
-    (* Instantiate the GIntro thm with "f" and import into the clause context. *)
-    val lGI = GIntro_thm
-      |> Thm.forall_elim (cert f)
-      |> fold Thm.forall_elim cqs
-      |> fold Thm.elim_implies ags
-
-    fun mk_call_info (rcfix, rcassm, rcarg) RI =
-      let
-        val llRI = RI
-          |> fold Thm.forall_elim cqs
-          |> fold (Thm.forall_elim o cert o Free) rcfix
-          |> fold Thm.elim_implies ags
-          |> fold Thm.elim_implies rcassm
-
-        val h_assum =
-          HOLogic.mk_Trueprop (G $ rcarg $ (h $ rcarg))
-          |> fold_rev (curry Logic.mk_implies o prop_of) rcassm
-          |> fold_rev (Logic.all o Free) rcfix
-          |> Pattern.rewrite_term (ProofContext.theory_of ctxt) [(f, h)] []
-          |> abstract_over_list (rev qs)
-      in
-        RCInfo {RIvs=rcfix, rcarg=rcarg, CCas=rcassm, llRI=llRI, h_assum=h_assum}
-      end
-
-    val RC_infos = map2 mk_call_info RCs RIntro_thms
-  in
-    ClauseInfo {no=no, cdata=cdata, qglr=qglr, lGI=lGI, RCs=RC_infos,
-      tree=tree}
-  end
-*}
-
-ML {*
-fun store_compat_thms 0 thms = []
-  | store_compat_thms n thms =
-  let
-    val (thms1, thms2) = chop n thms
-  in
-    (thms1 :: store_compat_thms (n - 1) thms2)
-  end
-*}
-
-ML {*
-(* expects i <= j *)
-fun lookup_compat_thm i j cts =
-  nth (nth cts (i - 1)) (j - i)
-
-(* Returns "Gsi, Gsj, lhs_i = lhs_j |-- rhs_j_f = rhs_i_f" *)
-(* if j < i, then turn around *)
-fun get_compat_thm thy cts eqvtsi eqvtsj i j ctxi ctxj =
-  let
-    val ClauseContext {cqs=cqsi,ags=agsi,lhs=lhsi,...} = ctxi
-    val ClauseContext {cqs=cqsj,ags=agsj,lhs=lhsj,...} = ctxj
-
-    val lhsi_eq_lhsj = cterm_of thy (HOLogic.mk_Trueprop (mk_eq (lhsi, lhsj)))
-  in if j < i then
-    let
-      val compat = lookup_compat_thm j i cts
-    in
-      compat         (* "!!qj qi. Gsj => Gsi => lhsj = lhsi ==> rhsj = rhsi" *)
-      |> fold Thm.forall_elim (cqsj @ cqsi) (* "Gsj => Gsi => lhsj = lhsi ==> rhsj = rhsi" *)
-      |> fold Thm.elim_implies (rev eqvtsj) (* HERE *)
-      |> fold Thm.elim_implies agsj
-      |> fold Thm.elim_implies agsi
-      |> Thm.elim_implies ((Thm.assume lhsi_eq_lhsj) RS sym) (* "Gsj, Gsi, lhsi = lhsj |-- rhsj = rhsi" *)
-    end
-    else
-    let
-      val compat = lookup_compat_thm i j cts
-    in
-      compat        (* "!!qi qj. Gsi => Gsj => lhsi = lhsj ==> rhsi = rhsj" *)
-      |> fold Thm.forall_elim (cqsi @ cqsj) (* "Gsi => Gsj => lhsi = lhsj ==> rhsi = rhsj" *)
-      |> fold Thm.elim_implies (rev eqvtsi)  (* HERE *)
-      |> fold Thm.elim_implies agsi
-      |> fold Thm.elim_implies agsj
-      |> Thm.elim_implies (Thm.assume lhsi_eq_lhsj)
-      |> (fn thm => thm RS sym) (* "Gsi, Gsj, lhsi = lhsj |-- rhsj = rhsi" *)
-    end
-  end
-*}
-
-
-ML {*
-(* Generates the replacement lemma in fully quantified form. *)
-fun mk_replacement_lemma thy h ih_elim clause =
-  let
-    val ClauseInfo {cdata=ClauseContext {qs, cqs, ags, case_hyp, ...},
-      RCs, tree, ...} = clause
-    local open Conv in
-      val ih_conv = arg1_conv o arg_conv o arg_conv
-    end
-
-    val ih_elim_case =
-      Conv.fconv_rule (ih_conv (K (case_hyp RS eq_reflection))) ih_elim
-
-    val Ris = map (fn RCInfo {llRI, ...} => llRI) RCs
-    val h_assums = map (fn RCInfo {h_assum, ...} =>
-      Thm.assume (cterm_of thy (subst_bounds (rev qs, h_assum)))) RCs
-
-    val (eql, _) =
-      Function_Ctx_Tree.rewrite_by_tree thy h ih_elim_case (Ris ~~ h_assums) tree
-
-    val replace_lemma = (eql RS meta_eq_to_obj_eq)
-      |> Thm.implies_intr (cprop_of case_hyp)
-      |> fold_rev (Thm.implies_intr o cprop_of) h_assums
-      |> fold_rev (Thm.implies_intr o cprop_of) ags
-      |> fold_rev Thm.forall_intr cqs
-      |> Thm.close_derivation
-  in
-    replace_lemma
-  end
-*}
-
-ML {*
-fun mk_eqvt_lemma thy ih_eqvt clause =
-  let
-    val ClauseInfo {cdata=ClauseContext {cqs, ags, case_hyp, ...}, RCs, ...} = clause
-
-    local open Conv in
-      val ih_conv = arg1_conv o arg_conv o arg_conv
-    end
-
-    val ih_eqvt_case =
-      Conv.fconv_rule (ih_conv (K (case_hyp RS eq_reflection))) ih_eqvt
-
-    fun prep_eqvt (RCInfo {llRI, RIvs, CCas, ...}) = 
-        (llRI RS ih_eqvt_case)
-        |> fold_rev (Thm.implies_intr o cprop_of) CCas
-        |> fold_rev (Thm.forall_intr o cterm_of thy o Free) RIvs
-  in
-    map prep_eqvt RCs
-    |> map (fold_rev (Thm.implies_intr o cprop_of) ags)
-    |> map (Thm.implies_intr (cprop_of case_hyp))
-    |> map (fold_rev Thm.forall_intr cqs)
-    |> map (Thm.close_derivation) 
-  end
-*}
-
-ML {*
-fun mk_uniqueness_clause thy globals compat_store eqvts clausei clausej RLj =
-  let
-    val Globals {h, y, x, fvar, ...} = globals
-    val ClauseInfo {no=i, cdata=cctxi as ClauseContext {ctxt=ctxti, lhs=lhsi, case_hyp, cqs = cqsi, 
-      ags = agsi, ...}, ...} = clausei
-    val ClauseInfo {no=j, qglr=cdescj, RCs=RCsj, ...} = clausej
-
-    val cctxj as ClauseContext {ags = agsj', lhs = lhsj', rhs = rhsj', qs = qsj', cqs = cqsj', ...} =
-      mk_clause_context x ctxti cdescj 
-
-    val rhsj'h = Pattern.rewrite_term thy [(fvar,h)] [] rhsj'
-
-    val Ghsj' = map 
-      (fn RCInfo {h_assum, ...} => Thm.assume (cterm_of thy (subst_bounds (rev qsj', h_assum)))) RCsj
-
-    val y_eq_rhsj'h = Thm.assume (cterm_of thy (HOLogic.mk_Trueprop (mk_eq (y, rhsj'h))))
-    val lhsi_eq_lhsj' = Thm.assume (cterm_of thy (HOLogic.mk_Trueprop (mk_eq (lhsi, lhsj'))))
-       (* lhs_i = lhs_j' |-- lhs_i = lhs_j' *) 
-
-    val case_hypj' = trans OF [case_hyp, lhsi_eq_lhsj']
-
-    val RLj_import = RLj
-      |> fold Thm.forall_elim cqsj'
-      |> fold Thm.elim_implies agsj'
-      |> fold Thm.elim_implies Ghsj'
-
-    val eqvtsi = nth eqvts (i - 1)
-      |> map (fold Thm.forall_elim cqsi)
-      |> map (fold Thm.elim_implies [case_hyp])
-      |> map (fold Thm.elim_implies agsi)
-
-    val eqvtsj = nth eqvts (j - 1)
-      |> map (fold Thm.forall_elim cqsj')
-      |> map (fold Thm.elim_implies [case_hypj'])
-      |> map (fold Thm.elim_implies agsj')
-
-    val compat = get_compat_thm thy compat_store eqvtsi eqvtsj i j cctxi cctxj
-
-  in
-    (trans OF [case_hyp, lhsi_eq_lhsj']) (* lhs_i = lhs_j' |-- x = lhs_j' *)
-    |> Thm.implies_elim RLj_import
-      (* Rj1' ... Rjk', lhs_i = lhs_j' |-- rhs_j'_h = rhs_j'_f *)
-    |> (fn it => trans OF [it, compat])
-      (* lhs_i = lhs_j', Gj', Rj1' ... Rjk' |-- rhs_j'_h = rhs_i_f *)
-    |> (fn it => trans OF [y_eq_rhsj'h, it])
-      (* lhs_i = lhs_j', Gj', Rj1' ... Rjk', y = rhs_j_h' |-- y = rhs_i_f *)
-    |> fold_rev (Thm.implies_intr o cprop_of) Ghsj'
-    |> fold_rev (Thm.implies_intr o cprop_of) agsj'
-      (* lhs_i = lhs_j' , y = rhs_j_h' |-- Gj', Rj1'...Rjk' ==> y = rhs_i_f *)
-    |> Thm.implies_intr (cprop_of y_eq_rhsj'h)
-    |> Thm.implies_intr (cprop_of lhsi_eq_lhsj')
-    |> fold_rev Thm.forall_intr (cterm_of thy h :: cqsj')
-  end
-*}
-
-
-ML {*
-fun mk_uniqueness_case thy globals G f ihyp ih_intro G_cases compat_store clauses replems eqvtlems clausei =
-  let
-    val Globals {x, y, ranT, fvar, ...} = globals
-    val ClauseInfo {cdata = ClauseContext {lhs, rhs, cqs, ags, case_hyp, ...}, lGI, RCs, ...} = clausei
-    val rhsC = Pattern.rewrite_term thy [(fvar, f)] [] rhs
-
-    val ih_intro_case = full_simplify (HOL_basic_ss addsimps [case_hyp]) ih_intro
-
-    fun prep_RC (RCInfo {llRI, RIvs, CCas, ...}) = 
-        (llRI RS ih_intro_case)
-        |> fold_rev (Thm.implies_intr o cprop_of) CCas
-        |> fold_rev (Thm.forall_intr o cterm_of thy o Free) RIvs
-
-    val existence = fold (curry op COMP o prep_RC) RCs lGI
-
-    val P = cterm_of thy (mk_eq (y, rhsC))
-    val G_lhs_y = Thm.assume (cterm_of thy (HOLogic.mk_Trueprop (G $ lhs $ y)))
-
-    val unique_clauses =
-      map2 (mk_uniqueness_clause thy globals compat_store eqvtlems clausei) clauses replems
-
-    fun elim_implies_eta A AB =
-      Thm.compose_no_flatten true (A, 0) 1 AB |> Seq.list_of |> the_single
-
-    val uniqueness = G_cases
-      |> Thm.forall_elim (cterm_of thy lhs)
-      |> Thm.forall_elim (cterm_of thy y)
-      |> Thm.forall_elim P
-      |> Thm.elim_implies G_lhs_y
-      |> fold elim_implies_eta unique_clauses
-      |> Thm.implies_intr (cprop_of G_lhs_y)
-      |> Thm.forall_intr (cterm_of thy y)
-
-    val P2 = cterm_of thy (lambda y (G $ lhs $ y)) (* P2 y := (lhs, y): G *)
-
-    val exactly_one =
-      ex1I |> instantiate' [SOME (ctyp_of thy ranT)] [SOME P2, SOME (cterm_of thy rhsC)]
-      |> curry (op COMP) existence
-      |> curry (op COMP) uniqueness
-      |> simplify (HOL_basic_ss addsimps [case_hyp RS sym])
-      |> Thm.implies_intr (cprop_of case_hyp)
-      |> fold_rev (Thm.implies_intr o cprop_of) ags
-      |> fold_rev Thm.forall_intr cqs
-
-    val function_value =
-      existence
-      |> Thm.implies_intr ihyp
-      |> Thm.implies_intr (cprop_of case_hyp)
-      |> Thm.forall_intr (cterm_of thy x)
-      |> Thm.forall_elim (cterm_of thy lhs)
-      |> curry (op RS) refl
-  in
-    (exactly_one, function_value)
-  end
-*}
-
-
-ML {*
-fun prove_stuff ctxt globals G f R clauses complete compat compat_store G_elim G_eqvt f_def =
-  let
-    val Globals {h, domT, ranT, x, ...} = globals
-    val thy = ProofContext.theory_of ctxt
-
-    (* Inductive Hypothesis: !!z. (z,x):R ==> EX!y. (z,y):G *)
-    val ihyp = Term.all domT $ Abs ("z", domT,
-      Logic.mk_implies (HOLogic.mk_Trueprop (R $ Bound 0 $ x),
-        HOLogic.mk_Trueprop (Const (@{const_name Ex1}, (ranT --> boolT) --> boolT) $
-          Abs ("y", ranT, G $ Bound 1 $ Bound 0))))
-      |> cterm_of thy
-
-    val ihyp_thm = Thm.assume ihyp |> Thm.forall_elim_vars 0
-    val ih_intro = ihyp_thm RS (f_def RS ex1_implies_ex)
-    val ih_elim = ihyp_thm RS (f_def RS ex1_implies_un)
-      |> instantiate' [] [NONE, SOME (cterm_of thy h)]
-    val ih_eqvt = ihyp_thm RS (G_eqvt RS (f_def RS @{thm fundef_ex1_eqvt_at}))
-
-    val _ = trace_msg (K "Proving Replacement lemmas...")
-    val repLemmas = map (mk_replacement_lemma thy h ih_elim) clauses
-
-    val _ = trace_msg (K "Proving Equivariance lemmas...")
-    val eqvtLemmas = map (mk_eqvt_lemma thy ih_eqvt) clauses
-
-    val _ = trace_msg (K "Proving cases for unique existence...")
-    val (ex1s, values) =
-      split_list (map (mk_uniqueness_case thy globals G f 
-        ihyp ih_intro G_elim compat_store clauses repLemmas eqvtLemmas) clauses)
-     
-    val _ = trace_msg (K "Proving: Graph is a function")
-    val graph_is_function = complete
-      |> Thm.forall_elim_vars 0
-      |> fold (curry op COMP) ex1s
-      |> Thm.implies_intr (ihyp)
-      |> Thm.implies_intr (cterm_of thy (HOLogic.mk_Trueprop (mk_acc domT R $ x)))
-      |> Thm.forall_intr (cterm_of thy x)
-      |> (fn it => Drule.compose_single (it, 2, acc_induct_rule)) (* "EX! y. (?x,y):G" *)
-      |> (fn it => fold (Thm.forall_intr o cterm_of thy o Var) (Term.add_vars (prop_of it) []) it)
-
-    val goalstate =  Conjunction.intr graph_is_function complete
-      |> Thm.close_derivation
-      |> Goal.protect
-      |> fold_rev (Thm.implies_intr o cprop_of) compat
-      |> Thm.implies_intr (cprop_of complete)
-  in
-    (goalstate, values)
-  end
-*}
-
-
-ML {*
-(* wrapper -- restores quantifiers in rule specifications *)
-fun inductive_def eqvt_flag (binding as ((R, T), _)) intrs lthy =
-  let
-    val ({intrs = intrs_gen, elims = [elim_gen], preds = [ Rdef ], induct, raw_induct, ...}, lthy) =
-      lthy
-      |> Local_Theory.conceal 
-      |> Inductive.add_inductive_i
-          {quiet_mode = true,
-            verbose = ! trace,
-            alt_name = Binding.empty,
-            coind = false,
-            no_elim = false,
-            no_ind = false,
-            skip_mono = true,
-            fork_mono = false}
-          [binding] (* relation *)
-          [] (* no parameters *)
-          (map (fn t => (Attrib.empty_binding, t)) intrs) (* intro rules *)
-          [] (* no special monos *)
-      ||> Local_Theory.restore_naming lthy
-
-    val eqvt_thm' = 
-      if eqvt_flag = false then NONE
-      else 
-        let
-          val ([eqvt_thm], lthy) = Nominal_Eqvt.raw_equivariance false [Rdef] raw_induct intrs_gen lthy
-        in
-          SOME ((Nominal_ThmDecls.eqvt_transform lthy eqvt_thm) RS @{thm eqvtI})
-        end
-
-    val cert = cterm_of (ProofContext.theory_of lthy)
-    fun requantify orig_intro thm =
-      let
-        val (qs, t) = dest_all_all orig_intro
-        val frees = frees_in_term lthy t |> remove (op =) (Binding.name_of R, T)
-        val vars = Term.add_vars (prop_of thm) [] |> rev
-        val varmap = AList.lookup (op =) (frees ~~ map fst vars)
-          #> the_default ("",0)
-      in
-        fold_rev (fn Free (n, T) =>
-          forall_intr_rename (n, cert (Var (varmap (n, T), T)))) qs thm
-      end
-  in
-    ((Rdef, map2 requantify intrs intrs_gen, forall_intr_vars elim_gen, induct, eqvt_thm'), lthy)
-  end
-*}
-
-ML {*
-fun define_graph Gname fvar domT ranT clauses RCss lthy =
-  let
-    val GT = domT --> ranT --> boolT
-    val (Gvar as (n, T)) = singleton (Variable.variant_frees lthy []) (Gname, GT)
-
-    fun mk_GIntro (ClauseContext {qs, gs, lhs, rhs, ...}) RCs =
-      let
-        fun mk_h_assm (rcfix, rcassm, rcarg) =
-          HOLogic.mk_Trueprop (Free Gvar $ rcarg $ (fvar $ rcarg))
-          |> fold_rev (curry Logic.mk_implies o prop_of) rcassm
-          |> fold_rev (Logic.all o Free) rcfix
-      in
-        HOLogic.mk_Trueprop (Free Gvar $ lhs $ rhs)
-        |> fold_rev (curry Logic.mk_implies o mk_h_assm) RCs
-        |> fold_rev (curry Logic.mk_implies) gs
-        |> fold_rev Logic.all (fvar :: qs)
-      end
-
-    val G_intros = map2 mk_GIntro clauses RCss
-  in
-    inductive_def true ((Binding.name n, T), NoSyn) G_intros lthy
-  end
-*}
-
-ML {*
-fun define_function fdefname (fname, mixfix) domT ranT G default lthy =
-  let
-    val f_def =
-      Abs ("x", domT, Const (@{const_name FunDef.THE_default}, ranT --> (ranT --> boolT) --> ranT) 
-        $ (default $ Bound 0) $ Abs ("y", ranT, G $ Bound 1 $ Bound 0))
-      |> Syntax.check_term lthy
-  in
-    Local_Theory.define
-      ((Binding.name (function_name fname), mixfix),
-        ((Binding.conceal (Binding.name fdefname), []), f_def)) lthy
-  end
-
-fun define_recursion_relation Rname domT qglrs clauses RCss lthy =
-  let
-    val RT = domT --> domT --> boolT
-    val (Rvar as (n, T)) = singleton (Variable.variant_frees lthy []) (Rname, RT)
-
-    fun mk_RIntro (ClauseContext {qs, gs, lhs, ...}, (oqs, _, _, _)) (rcfix, rcassm, rcarg) =
-      HOLogic.mk_Trueprop (Free Rvar $ rcarg $ lhs)
-      |> fold_rev (curry Logic.mk_implies o prop_of) rcassm
-      |> fold_rev (curry Logic.mk_implies) gs
-      |> fold_rev (Logic.all o Free) rcfix
-      |> fold_rev mk_forall_rename (map fst oqs ~~ qs)
-      (* "!!qs xs. CS ==> G => (r, lhs) : R" *)
-
-    val R_intross = map2 (map o mk_RIntro) (clauses ~~ qglrs) RCss
-
-    val ((R, RIntro_thms, R_elim, _, _), lthy) =
-      inductive_def false ((Binding.name n, T), NoSyn) (flat R_intross) lthy
-  in
-    ((R, Library.unflat R_intross RIntro_thms, R_elim), lthy)
-  end
-
-
-fun fix_globals domT ranT fvar ctxt =
-  let
-    val ([h, y, x, z, a, D, P, Pbool],ctxt') = Variable.variant_fixes
-      ["h_fd", "y_fd", "x_fd", "z_fd", "a_fd", "D_fd", "P_fd", "Pb_fd"] ctxt
-  in
-    (Globals {h = Free (h, domT --> ranT),
-      y = Free (y, ranT),
-      x = Free (x, domT),
-      z = Free (z, domT),
-      a = Free (a, domT),
-      D = Free (D, domT --> boolT),
-      P = Free (P, domT --> boolT),
-      Pbool = Free (Pbool, boolT),
-      fvar = fvar,
-      domT = domT,
-      ranT = ranT},
-    ctxt')
-  end
-
-fun inst_RC thy fvar f (rcfix, rcassm, rcarg) =
-  let
-    fun inst_term t = subst_bound(f, abstract_over (fvar, t))
-  in
-    (rcfix, map (Thm.assume o cterm_of thy o inst_term o prop_of) rcassm, inst_term rcarg)
-  end
-
-
-
-(**********************************************************
- *                   PROVING THE RULES
- **********************************************************)
-
-fun mk_psimps thy globals R clauses valthms f_iff graph_is_function =
-  let
-    val Globals {domT, z, ...} = globals
-
-    fun mk_psimp (ClauseInfo {qglr = (oqs, _, _, _), cdata = ClauseContext {cqs, lhs, ags, ...}, ...}) valthm =
-      let
-        val lhs_acc = cterm_of thy (HOLogic.mk_Trueprop (mk_acc domT R $ lhs)) (* "acc R lhs" *)
-        val z_smaller = cterm_of thy (HOLogic.mk_Trueprop (R $ z $ lhs)) (* "R z lhs" *)
-      in
-        ((Thm.assume z_smaller) RS ((Thm.assume lhs_acc) RS acc_downward))
-        |> (fn it => it COMP graph_is_function)
-        |> Thm.implies_intr z_smaller
-        |> Thm.forall_intr (cterm_of thy z)
-        |> (fn it => it COMP valthm)
-        |> Thm.implies_intr lhs_acc
-        |> asm_simplify (HOL_basic_ss addsimps [f_iff])
-        |> fold_rev (Thm.implies_intr o cprop_of) ags
-        |> fold_rev forall_intr_rename (map fst oqs ~~ cqs)
-      end
-  in
-    map2 mk_psimp clauses valthms
-  end
-
-
-(** Induction rule **)
-
-
-val acc_subset_induct = @{thm predicate1I} RS @{thm accp_subset_induct}
-
-
-fun mk_partial_induct_rule thy globals R complete_thm clauses =
-  let
-    val Globals {domT, x, z, a, P, D, ...} = globals
-    val acc_R = mk_acc domT R
-
-    val x_D = Thm.assume (cterm_of thy (HOLogic.mk_Trueprop (D $ x)))
-    val a_D = cterm_of thy (HOLogic.mk_Trueprop (D $ a))
-
-    val D_subset = cterm_of thy (Logic.all x
-      (Logic.mk_implies (HOLogic.mk_Trueprop (D $ x), HOLogic.mk_Trueprop (acc_R $ x))))
-
-    val D_dcl = (* "!!x z. [| x: D; (z,x):R |] ==> z:D" *)
-      Logic.all x (Logic.all z (Logic.mk_implies (HOLogic.mk_Trueprop (D $ x),
-        Logic.mk_implies (HOLogic.mk_Trueprop (R $ z $ x),
-          HOLogic.mk_Trueprop (D $ z)))))
-      |> cterm_of thy
-
-    (* Inductive Hypothesis: !!z. (z,x):R ==> P z *)
-    val ihyp = Term.all domT $ Abs ("z", domT,
-      Logic.mk_implies (HOLogic.mk_Trueprop (R $ Bound 0 $ x),
-        HOLogic.mk_Trueprop (P $ Bound 0)))
-      |> cterm_of thy
-
-    val aihyp = Thm.assume ihyp
-
-    fun prove_case clause =
-      let
-        val ClauseInfo {cdata = ClauseContext {ctxt, qs, cqs, ags, gs, lhs, case_hyp, ...},
-          RCs, qglr = (oqs, _, _, _), ...} = clause
-
-        val case_hyp_conv = K (case_hyp RS eq_reflection)
-        local open Conv in
-          val lhs_D = fconv_rule (arg_conv (arg_conv (case_hyp_conv))) x_D
-          val sih =
-            fconv_rule (Conv.binder_conv
-              (K (arg1_conv (arg_conv (arg_conv case_hyp_conv)))) ctxt) aihyp
-        end
-
-        fun mk_Prec (RCInfo {llRI, RIvs, CCas, rcarg, ...}) = sih
-          |> Thm.forall_elim (cterm_of thy rcarg)
-          |> Thm.elim_implies llRI
-          |> fold_rev (Thm.implies_intr o cprop_of) CCas
-          |> fold_rev (Thm.forall_intr o cterm_of thy o Free) RIvs
-
-        val P_recs = map mk_Prec RCs   (*  [P rec1, P rec2, ... ]  *)
-
-        val step = HOLogic.mk_Trueprop (P $ lhs)
-          |> fold_rev (curry Logic.mk_implies o prop_of) P_recs
-          |> fold_rev (curry Logic.mk_implies) gs
-          |> curry Logic.mk_implies (HOLogic.mk_Trueprop (D $ lhs))
-          |> fold_rev mk_forall_rename (map fst oqs ~~ qs)
-          |> cterm_of thy
-
-        val P_lhs = Thm.assume step
-          |> fold Thm.forall_elim cqs
-          |> Thm.elim_implies lhs_D
-          |> fold Thm.elim_implies ags
-          |> fold Thm.elim_implies P_recs
-
-        val res = cterm_of thy (HOLogic.mk_Trueprop (P $ x))
-          |> Conv.arg_conv (Conv.arg_conv case_hyp_conv)
-          |> Thm.symmetric (* P lhs == P x *)
-          |> (fn eql => Thm.equal_elim eql P_lhs) (* "P x" *)
-          |> Thm.implies_intr (cprop_of case_hyp)
-          |> fold_rev (Thm.implies_intr o cprop_of) ags
-          |> fold_rev Thm.forall_intr cqs
-      in
-        (res, step)
-      end
-
-    val (cases, steps) = split_list (map prove_case clauses)
-
-    val istep = complete_thm
-      |> Thm.forall_elim_vars 0
-      |> fold (curry op COMP) cases (*  P x  *)
-      |> Thm.implies_intr ihyp
-      |> Thm.implies_intr (cprop_of x_D)
-      |> Thm.forall_intr (cterm_of thy x)
-
-    val subset_induct_rule =
-      acc_subset_induct
-      |> (curry op COMP) (Thm.assume D_subset)
-      |> (curry op COMP) (Thm.assume D_dcl)
-      |> (curry op COMP) (Thm.assume a_D)
-      |> (curry op COMP) istep
-      |> fold_rev Thm.implies_intr steps
-      |> Thm.implies_intr a_D
-      |> Thm.implies_intr D_dcl
-      |> Thm.implies_intr D_subset
-
-    val simple_induct_rule =
-      subset_induct_rule
-      |> Thm.forall_intr (cterm_of thy D)
-      |> Thm.forall_elim (cterm_of thy acc_R)
-      |> assume_tac 1 |> Seq.hd
-      |> (curry op COMP) (acc_downward
-        |> (instantiate' [SOME (ctyp_of thy domT)]
-             (map (SOME o cterm_of thy) [R, x, z]))
-        |> Thm.forall_intr (cterm_of thy z)
-        |> Thm.forall_intr (cterm_of thy x))
-      |> Thm.forall_intr (cterm_of thy a)
-      |> Thm.forall_intr (cterm_of thy P)
-  in
-    simple_induct_rule
-  end
-
-
-(* FIXME: broken by design *)
-fun mk_domain_intro ctxt (Globals {domT, ...}) R R_cases clause =
-  let
-    val thy = ProofContext.theory_of ctxt
-    val ClauseInfo {cdata = ClauseContext {gs, lhs, cqs, ...},
-      qglr = (oqs, _, _, _), ...} = clause
-    val goal = HOLogic.mk_Trueprop (mk_acc domT R $ lhs)
-      |> fold_rev (curry Logic.mk_implies) gs
-      |> cterm_of thy
-  in
-    Goal.init goal
-    |> (SINGLE (resolve_tac [accI] 1)) |> the
-    |> (SINGLE (eresolve_tac [Thm.forall_elim_vars 0 R_cases] 1))  |> the
-    |> (SINGLE (auto_tac (clasimpset_of ctxt))) |> the
-    |> Goal.conclude
-    |> fold_rev forall_intr_rename (map fst oqs ~~ cqs)
-  end
-
-
-
-(** Termination rule **)
-
-val wf_induct_rule = @{thm Wellfounded.wfP_induct_rule}
-val wf_in_rel = @{thm FunDef.wf_in_rel}
-val in_rel_def = @{thm FunDef.in_rel_def}
-
-fun mk_nest_term_case thy globals R' ihyp clause =
-  let
-    val Globals {z, ...} = globals
-    val ClauseInfo {cdata = ClauseContext {qs, cqs, ags, lhs, case_hyp, ...}, tree,
-      qglr=(oqs, _, _, _), ...} = clause
-
-    val ih_case = full_simplify (HOL_basic_ss addsimps [case_hyp]) ihyp
-
-    fun step (fixes, assumes) (_ $ arg) u (sub,(hyps,thms)) =
-      let
-        val used = (u @ sub)
-          |> map (fn (ctx,thm) => Function_Ctx_Tree.export_thm thy ctx thm)
-
-        val hyp = HOLogic.mk_Trueprop (R' $ arg $ lhs)
-          |> fold_rev (curry Logic.mk_implies o prop_of) used (* additional hyps *)
-          |> Function_Ctx_Tree.export_term (fixes, assumes)
-          |> fold_rev (curry Logic.mk_implies o prop_of) ags
-          |> fold_rev mk_forall_rename (map fst oqs ~~ qs)
-          |> cterm_of thy
-
-        val thm = Thm.assume hyp
-          |> fold Thm.forall_elim cqs
-          |> fold Thm.elim_implies ags
-          |> Function_Ctx_Tree.import_thm thy (fixes, assumes)
-          |> fold Thm.elim_implies used (*  "(arg, lhs) : R'"  *)
-
-        val z_eq_arg = HOLogic.mk_Trueprop (mk_eq (z, arg))
-          |> cterm_of thy |> Thm.assume
-
-        val acc = thm COMP ih_case
-        val z_acc_local = acc
-          |> Conv.fconv_rule
-              (Conv.arg_conv (Conv.arg_conv (K (Thm.symmetric (z_eq_arg RS eq_reflection)))))
-
-        val ethm = z_acc_local
-          |> Function_Ctx_Tree.export_thm thy (fixes,
-               z_eq_arg :: case_hyp :: ags @ assumes)
-          |> fold_rev forall_intr_rename (map fst oqs ~~ cqs)
-
-        val sub' = sub @ [(([],[]), acc)]
-      in
-        (sub', (hyp :: hyps, ethm :: thms))
-      end
-      | step _ _ _ _ = raise Match
-  in
-    Function_Ctx_Tree.traverse_tree step tree
-  end
-
-
-fun mk_nest_term_rule thy globals R R_cases clauses =
-  let
-    val Globals { domT, x, z, ... } = globals
-    val acc_R = mk_acc domT R
-
-    val R' = Free ("R", fastype_of R)
-
-    val Rrel = Free ("R", HOLogic.mk_setT (HOLogic.mk_prodT (domT, domT)))
-    val inrel_R = Const (@{const_name FunDef.in_rel},
-      HOLogic.mk_setT (HOLogic.mk_prodT (domT, domT)) --> fastype_of R) $ Rrel
-
-    val wfR' = HOLogic.mk_Trueprop (Const (@{const_name Wellfounded.wfP},
-      (domT --> domT --> boolT) --> boolT) $ R')
-      |> cterm_of thy (* "wf R'" *)
-
-    (* Inductive Hypothesis: !!z. (z,x):R' ==> z : acc R *)
-    val ihyp = Term.all domT $ Abs ("z", domT,
-      Logic.mk_implies (HOLogic.mk_Trueprop (R' $ Bound 0 $ x),
-        HOLogic.mk_Trueprop (acc_R $ Bound 0)))
-      |> cterm_of thy
-
-    val ihyp_a = Thm.assume ihyp |> Thm.forall_elim_vars 0
-
-    val R_z_x = cterm_of thy (HOLogic.mk_Trueprop (R $ z $ x))
-
-    val (hyps, cases) = fold (mk_nest_term_case thy globals R' ihyp_a) clauses ([], [])
-  in
-    R_cases
-    |> Thm.forall_elim (cterm_of thy z)
-    |> Thm.forall_elim (cterm_of thy x)
-    |> Thm.forall_elim (cterm_of thy (acc_R $ z))
-    |> curry op COMP (Thm.assume R_z_x)
-    |> fold_rev (curry op COMP) cases
-    |> Thm.implies_intr R_z_x
-    |> Thm.forall_intr (cterm_of thy z)
-    |> (fn it => it COMP accI)
-    |> Thm.implies_intr ihyp
-    |> Thm.forall_intr (cterm_of thy x)
-    |> (fn it => Drule.compose_single(it,2,wf_induct_rule))
-    |> curry op RS (Thm.assume wfR')
-    |> forall_intr_vars
-    |> (fn it => it COMP allI)
-    |> fold Thm.implies_intr hyps
-    |> Thm.implies_intr wfR'
-    |> Thm.forall_intr (cterm_of thy R')
-    |> Thm.forall_elim (cterm_of thy (inrel_R))
-    |> curry op RS wf_in_rel
-    |> full_simplify (HOL_basic_ss addsimps [in_rel_def])
-    |> Thm.forall_intr (cterm_of thy Rrel)
-  end
-
-
-
-(* Tail recursion (probably very fragile)
- *
- * FIXME:
- * - Need to do forall_elim_vars on psimps: Unneccesary, if psimps would be taken from the same context.
- * - Must we really replace the fvar by f here?
- * - Splitting is not configured automatically: Problems with case?
- *)
-fun mk_trsimps octxt globals f G R f_def R_cases G_induct clauses psimps =
-  let
-    val Globals {domT, ranT, fvar, ...} = globals
-
-    val R_cases = Thm.forall_elim_vars 0 R_cases (* FIXME: Should be already in standard form. *)
-
-    val graph_implies_dom = (* "G ?x ?y ==> dom ?x"  *)
-      Goal.prove octxt ["x", "y"] [HOLogic.mk_Trueprop (G $ Free ("x", domT) $ Free ("y", ranT))]
-        (HOLogic.mk_Trueprop (mk_acc domT R $ Free ("x", domT)))
-        (fn {prems=[a], ...} =>
-          ((rtac (G_induct OF [a]))
-          THEN_ALL_NEW rtac accI
-          THEN_ALL_NEW etac R_cases
-          THEN_ALL_NEW asm_full_simp_tac (simpset_of octxt)) 1)
-
-    val default_thm =
-      forall_intr_vars graph_implies_dom COMP (f_def COMP fundef_default_value)
-
-    fun mk_trsimp clause psimp =
-      let
-        val ClauseInfo {qglr = (oqs, _, _, _), cdata =
-          ClauseContext {ctxt, cqs, gs, lhs, rhs, ...}, ...} = clause
-        val thy = ProofContext.theory_of ctxt
-        val rhs_f = Pattern.rewrite_term thy [(fvar, f)] [] rhs
-
-        val trsimp = Logic.list_implies(gs,
-          HOLogic.mk_Trueprop (HOLogic.mk_eq(f $ lhs, rhs_f))) (* "f lhs = rhs" *)
-        val lhs_acc = (mk_acc domT R $ lhs) (* "acc R lhs" *)
-        fun simp_default_tac ss =
-          asm_full_simp_tac (ss addsimps [default_thm, Let_def])
-      in
-        Goal.prove ctxt [] [] trsimp (fn _ =>
-          rtac (instantiate' [] [SOME (cterm_of thy lhs_acc)] case_split) 1
-          THEN (rtac (Thm.forall_elim_vars 0 psimp) THEN_ALL_NEW assume_tac) 1
-          THEN (simp_default_tac (simpset_of ctxt) 1)
-          THEN TRY ((etac not_acc_down 1)
-            THEN ((etac R_cases)
-              THEN_ALL_NEW (simp_default_tac (simpset_of ctxt))) 1))
-        |> fold_rev forall_intr_rename (map fst oqs ~~ cqs)
-      end
-  in
-    map2 mk_trsimp clauses psimps
-  end
-*}
-
-ML {*
-fun prepare_function config defname [((fname, fT), mixfix)] abstract_qglrs lthy =
-  let
-    val FunctionConfig {domintros, tailrec, default=default_opt, ...} = config
-
-    val default_str = the_default "%x. undefined" default_opt (*FIXME dynamic scoping*)
-    val fvar = Free (fname, fT)
-    val domT = domain_type fT
-    val ranT = range_type fT
-
-    val default = Syntax.parse_term lthy default_str
-      |> Type.constraint fT |> Syntax.check_term lthy
-
-    val (globals, ctxt') = fix_globals domT ranT fvar lthy
-
-    val Globals { x, h, ... } = globals
-
-    val clauses = map (mk_clause_context x ctxt') abstract_qglrs
-
-    val n = length abstract_qglrs
-
-    fun build_tree (ClauseContext { ctxt, rhs, ...}) =
-       Function_Ctx_Tree.mk_tree (fname, fT) h ctxt rhs
-
-    val trees = map build_tree clauses
-    val RCss = map find_calls trees
-
-    val ((G, GIntro_thms, G_elim, G_induct, SOME G_eqvt), lthy) =
-      PROFILE "def_graph" (define_graph (graph_name defname) fvar domT ranT clauses RCss) lthy
-
-    val ((f, (_, f_defthm)), lthy) =
-      PROFILE "def_fun" (define_function (defname ^ "_sumC_def") (fname, mixfix) domT ranT G default) lthy
-
-    val RCss = map (map (inst_RC (ProofContext.theory_of lthy) fvar f)) RCss
-    val trees = map (Function_Ctx_Tree.inst_tree (ProofContext.theory_of lthy) fvar f) trees
-
-    val ((R, RIntro_thmss, R_elim), lthy) =
-      PROFILE "def_rel" (define_recursion_relation (rel_name defname) domT abstract_qglrs clauses RCss) lthy
-
-    val (_, lthy) =
-      Local_Theory.abbrev Syntax.mode_default ((Binding.name (dom_name defname), NoSyn), mk_acc domT R) lthy
-
-    val newthy = ProofContext.theory_of lthy
-    val clauses = map (transfer_clause_ctx newthy) clauses
-
-    val cert = cterm_of (ProofContext.theory_of lthy)
-
-    val xclauses = PROFILE "xclauses"
-      (map7 (mk_clause_info globals G f) (1 upto n) clauses abstract_qglrs trees
-        RCss GIntro_thms) RIntro_thmss
-
-    val complete =
-      mk_completeness globals clauses abstract_qglrs |> cert |> Thm.assume
-
-    val compat =
-      mk_compat_proof_obligations domT ranT fvar f abstract_qglrs 
-      |> map (cert #> Thm.assume)
-
-    val compat_store = store_compat_thms n compat
-
-    val (goalstate, values) = PROFILE "prove_stuff"
-      (prove_stuff lthy globals G f R xclauses complete compat
-         compat_store G_elim G_eqvt) f_defthm
-     
-    val mk_trsimps =
-      mk_trsimps lthy globals f G R f_defthm R_elim G_induct xclauses
-
-    fun mk_partial_rules provedgoal =
-      let
-        val newthy = theory_of_thm provedgoal (*FIXME*)
-
-        val (graph_is_function, complete_thm) =
-          provedgoal
-          |> Conjunction.elim
-          |> apfst (Thm.forall_elim_vars 0)
-
-        val f_iff = graph_is_function RS (f_defthm RS ex1_implies_iff)
-
-        val psimps = PROFILE "Proving simplification rules"
-          (mk_psimps newthy globals R xclauses values f_iff) graph_is_function
-
-        val simple_pinduct = PROFILE "Proving partial induction rule"
-          (mk_partial_induct_rule newthy globals R complete_thm) xclauses
-
-        val total_intro = PROFILE "Proving nested termination rule"
-          (mk_nest_term_rule newthy globals R R_elim) xclauses
-
-        val dom_intros =
-          if domintros then SOME (PROFILE "Proving domain introduction rules"
-             (map (mk_domain_intro lthy globals R R_elim)) xclauses)
-           else NONE
-        val trsimps = if tailrec then SOME (mk_trsimps psimps) else NONE
-
-      in
-        FunctionResult {fs=[f], G=G, R=R, cases=complete_thm,
-          psimps=psimps, simple_pinducts=[simple_pinduct],
-          termination=total_intro, trsimps=trsimps,
-          domintros=dom_intros}
-      end
-  in
-    ((f, goalstate, mk_partial_rules), lthy)
-  end
-*}
-
-ML {*
-open Function_Lib
-open Function_Common
-
-type qgar = string * (string * typ) list * term list * term list * term
-
-datatype mutual_part = MutualPart of
- {i : int,
-  i' : int,
-  fvar : string * typ,
-  cargTs: typ list,
-  f_def: term,
-
-  f: term option,
-  f_defthm : thm option}
-
-datatype mutual_info = Mutual of
- {n : int,
-  n' : int,
-  fsum_var : string * typ,
-
-  ST: typ,
-  RST: typ,
-
-  parts: mutual_part list,
-  fqgars: qgar list,
-  qglrs: ((string * typ) list * term list * term * term) list,
-
-  fsum : term option}
-
-fun mutual_induct_Pnames n =
-  if n < 5 then fst (chop n ["P","Q","R","S"])
-  else map (fn i => "P" ^ string_of_int i) (1 upto n)
-
-fun get_part fname =
-  the o find_first (fn (MutualPart {fvar=(n,_), ...}) => n = fname)
-
-(* FIXME *)
-fun mk_prod_abs e (t1, t2) =
-  let
-    val bTs = rev (map snd e)
-    val T1 = fastype_of1 (bTs, t1)
-    val T2 = fastype_of1 (bTs, t2)
-  in
-    HOLogic.pair_const T1 T2 $ t1 $ t2
-  end
-
-fun analyze_eqs ctxt defname fs eqs =
-  let
-    val num = length fs
-    val fqgars = map (split_def ctxt (K true)) eqs
-    val arity_of = map (fn (fname,_,_,args,_) => (fname, length args)) fqgars
-      |> AList.lookup (op =) #> the
-
-    fun curried_types (fname, fT) =
-      let
-        val (caTs, uaTs) = chop (arity_of fname) (binder_types fT)
-      in
-        (caTs, uaTs ---> body_type fT)
-      end
-
-    val (caTss, resultTs) = split_list (map curried_types fs)
-    val argTs = map (foldr1 HOLogic.mk_prodT) caTss
-
-    val dresultTs = distinct (op =) resultTs
-    val n' = length dresultTs
-
-    val RST = Balanced_Tree.make (uncurry SumTree.mk_sumT) dresultTs
-    val ST = Balanced_Tree.make (uncurry SumTree.mk_sumT) argTs
-
-    val fsum_type = ST --> RST
-
-    val ([fsum_var_name], _) = Variable.add_fixes [ defname ^ "_sum" ] ctxt
-    val fsum_var = (fsum_var_name, fsum_type)
-
-    fun define (fvar as (n, _)) caTs resultT i =
-      let
-        val vars = map_index (fn (j,T) => Free ("x" ^ string_of_int j, T)) caTs (* FIXME: Bind xs properly *)
-        val i' = find_index (fn Ta => Ta = resultT) dresultTs + 1
-
-        val f_exp = SumTree.mk_proj RST n' i' 
-          (Free fsum_var $ SumTree.mk_inj ST num i (foldr1 HOLogic.mk_prod vars))
-        
-        val def = Term.abstract_over (Free fsum_var, fold_rev lambda vars f_exp)
-
-        val rew = (n, fold_rev lambda vars f_exp)
-      in
-        (MutualPart {i=i, i'=i', fvar=fvar,cargTs=caTs,f_def=def,f=NONE,f_defthm=NONE}, rew)
-      end
-
-    val (parts, rews) = split_list (map4 define fs caTss resultTs (1 upto num))
-
-    fun convert_eqs (f, qs, gs, args, rhs) =
-      let
-        val MutualPart {i, i', ...} = get_part f parts
-      in
-        (qs, gs, SumTree.mk_inj ST num i (foldr1 (mk_prod_abs qs) args),
-         SumTree.mk_inj RST n' i' (replace_frees rews rhs)
-         |> Envir.beta_norm)
-      end
-
-    val qglrs = map convert_eqs fqgars
-  in
-    Mutual {n=num, n'=n', fsum_var=fsum_var, ST=ST, RST=RST,
-      parts=parts, fqgars=fqgars, qglrs=qglrs, fsum=NONE}
-  end
-*}
-
-ML {*
-fun define_projections fixes mutual fsum lthy =
-  let
-    fun def ((MutualPart {i=i, i'=i', fvar=(fname, fT), cargTs, f_def, ...}), (_, mixfix)) lthy =
-      let
-        val ((f, (_, f_defthm)), lthy') =
-          Local_Theory.define
-            ((Binding.name fname, mixfix),
-              ((Binding.conceal (Binding.name (fname ^ "_def")), []),
-              Term.subst_bound (fsum, f_def))) lthy
-      in
-        (MutualPart {i=i, i'=i', fvar=(fname, fT), cargTs=cargTs, f_def=f_def,
-           f=SOME f, f_defthm=SOME f_defthm },
-         lthy')
-      end
-
-    val Mutual { n, n', fsum_var, ST, RST, parts, fqgars, qglrs, ... } = mutual
-    val (parts', lthy') = fold_map def (parts ~~ fixes) lthy
-  in
-    (Mutual { n=n, n'=n', fsum_var=fsum_var, ST=ST, RST=RST, parts=parts',
-       fqgars=fqgars, qglrs=qglrs, fsum=SOME fsum },
-     lthy')
-  end
-
-fun in_context ctxt (f, pre_qs, pre_gs, pre_args, pre_rhs) F =
-  let
-    val thy = ProofContext.theory_of ctxt
-
-    val oqnames = map fst pre_qs
-    val (qs, _) = Variable.variant_fixes oqnames ctxt
-      |>> map2 (fn (_, T) => fn n => Free (n, T)) pre_qs
-
-    fun inst t = subst_bounds (rev qs, t)
-    val gs = map inst pre_gs
-    val args = map inst pre_args
-    val rhs = inst pre_rhs
-
-    val cqs = map (cterm_of thy) qs
-    val ags = map (Thm.assume o cterm_of thy) gs
-
-    val import = fold Thm.forall_elim cqs
-      #> fold Thm.elim_implies ags
-
-    val export = fold_rev (Thm.implies_intr o cprop_of) ags
-      #> fold_rev forall_intr_rename (oqnames ~~ cqs)
-  in
-    F ctxt (f, qs, gs, args, rhs) import export
-  end
-
-fun recover_mutual_psimp all_orig_fdefs parts ctxt (fname, _, _, args, rhs)
-  import (export : thm -> thm) sum_psimp_eq =
-  let
-    val (MutualPart {f=SOME f, ...}) = get_part fname parts
-
-    val psimp = import sum_psimp_eq
-    val (simp, restore_cond) =
-      case cprems_of psimp of
-        [] => (psimp, I)
-      | [cond] => (Thm.implies_elim psimp (Thm.assume cond), Thm.implies_intr cond)
-      | _ => raise General.Fail "Too many conditions"
-
-  in
-    Goal.prove ctxt [] []
-      (HOLogic.Trueprop $ HOLogic.mk_eq (list_comb (f, args), rhs))
-      (fn _ => (Local_Defs.unfold_tac ctxt all_orig_fdefs)
-         THEN EqSubst.eqsubst_tac ctxt [0] [simp] 1
-         THEN (simp_tac (simpset_of ctxt)) 1) (* FIXME: global simpset?!! *)
-    |> restore_cond
-    |> export
-  end
-
-fun mk_applied_form ctxt caTs thm =
-  let
-    val thy = ProofContext.theory_of ctxt
-    val xs = map_index (fn (i,T) => cterm_of thy (Free ("x" ^ string_of_int i, T))) caTs (* FIXME: Bind xs properly *)
-  in
-    fold (fn x => fn thm => Thm.combination thm (Thm.reflexive x)) xs thm
-    |> Conv.fconv_rule (Thm.beta_conversion true)
-    |> fold_rev Thm.forall_intr xs
-    |> Thm.forall_elim_vars 0
-  end
-
-fun mutual_induct_rules lthy induct all_f_defs (Mutual {n, ST, parts, ...}) =
-  let
-    val cert = cterm_of (ProofContext.theory_of lthy)
-    val newPs =
-      map2 (fn Pname => fn MutualPart {cargTs, ...} =>
-          Free (Pname, cargTs ---> HOLogic.boolT))
-        (mutual_induct_Pnames (length parts)) parts
-
-    fun mk_P (MutualPart {cargTs, ...}) P =
-      let
-        val avars = map_index (fn (i,T) => Var (("a", i), T)) cargTs
-        val atup = foldr1 HOLogic.mk_prod avars
-      in
-        HOLogic.tupled_lambda atup (list_comb (P, avars))
-      end
-
-    val Ps = map2 mk_P parts newPs
-    val case_exp = SumTree.mk_sumcases HOLogic.boolT Ps
-
-    val induct_inst =
-      Thm.forall_elim (cert case_exp) induct
-      |> full_simplify SumTree.sumcase_split_ss
-      |> full_simplify (HOL_basic_ss addsimps all_f_defs)
-
-    fun project rule (MutualPart {cargTs, i, ...}) k =
-      let
-        val afs = map_index (fn (j,T) => Free ("a" ^ string_of_int (j + k), T)) cargTs (* FIXME! *)
-        val inj = SumTree.mk_inj ST n i (foldr1 HOLogic.mk_prod afs)
-      in
-        (rule
-         |> Thm.forall_elim (cert inj)
-         |> full_simplify SumTree.sumcase_split_ss
-         |> fold_rev (Thm.forall_intr o cert) (afs @ newPs),
-         k + length cargTs)
-      end
-  in
-    fst (fold_map (project induct_inst) parts 0)
-  end
-
-fun mk_partial_rules_mutual lthy inner_cont (m as Mutual {parts, fqgars, ...}) proof =
-  let
-    val result = inner_cont proof
-    val FunctionResult {G, R, cases, psimps, trsimps, simple_pinducts=[simple_pinduct],
-      termination, domintros, ...} = result
-
-    val (all_f_defs, fs) =
-      map (fn MutualPart {f_defthm = SOME f_def, f = SOME f, cargTs, ...} =>
-        (mk_applied_form lthy cargTs (Thm.symmetric f_def), f))
-      parts
-      |> split_list
-
-    val all_orig_fdefs =
-      map (fn MutualPart {f_defthm = SOME f_def, ...} => f_def) parts
-
-    fun mk_mpsimp fqgar sum_psimp =
-      in_context lthy fqgar (recover_mutual_psimp all_orig_fdefs parts) sum_psimp
-
-    val rew_ss = HOL_basic_ss addsimps all_f_defs
-    val mpsimps = map2 mk_mpsimp fqgars psimps
-    val mtrsimps = Option.map (map2 mk_mpsimp fqgars) trsimps
-    val minducts = mutual_induct_rules lthy simple_pinduct all_f_defs m
-    val mtermination = full_simplify rew_ss termination
-    val mdomintros = Option.map (map (full_simplify rew_ss)) domintros
-  in
-    FunctionResult { fs=fs, G=G, R=R,
-      psimps=mpsimps, simple_pinducts=minducts,
-      cases=cases, termination=mtermination,
-      domintros=mdomintros, trsimps=mtrsimps}
-  end
-
-fun prepare_function_mutual config defname fixes eqss lthy =
-  let
-    val mutual as Mutual {fsum_var=(n, T), qglrs, ...} =
-      analyze_eqs lthy defname (map fst fixes) (map Envir.beta_eta_contract eqss)
-
-    val ((fsum, goalstate, cont), lthy') =
-      prepare_function config defname [((n, T), NoSyn)] qglrs lthy
-
-    val (mutual', lthy'') = define_projections fixes mutual fsum lthy'
-
-    val mutual_cont = mk_partial_rules_mutual lthy'' cont mutual'
-  in
-    ((goalstate, mutual_cont), lthy'')
-  end
-
-*}
-
-
-ML {*
-
-open Function_Lib
-open Function_Common
-
-val simp_attribs = map (Attrib.internal o K)
-  [Simplifier.simp_add,
-   Code.add_default_eqn_attribute,
-   Nitpick_Simps.add]
-
-val psimp_attribs = map (Attrib.internal o K)
-  [Nitpick_Psimps.add]
-
-fun mk_defname fixes = fixes |> map (fst o fst) |> space_implode "_"
-
-fun add_simps fnames post sort extra_qualify label mod_binding moreatts
-  simps lthy =
-  let
-    val spec = post simps
-      |> map (apfst (apsnd (fn ats => moreatts @ ats)))
-      |> map (apfst (apfst extra_qualify))
-
-    val (saved_spec_simps, lthy) =
-      fold_map Local_Theory.note spec lthy
-
-    val saved_simps = maps snd saved_spec_simps
-    val simps_by_f = sort saved_simps
-
-    fun add_for_f fname simps =
-      Local_Theory.note
-        ((mod_binding (Binding.qualify true fname (Binding.name label)), []), simps)
-      #> snd
-  in
-    (saved_simps, fold2 add_for_f fnames simps_by_f lthy)
-  end
-
-fun prepare_function is_external prep default_constraint fixspec eqns config lthy =
-  let
-    val constrn_fxs = map (fn (b, T, mx) => (b, SOME (the_default default_constraint T), mx))
-    val ((fixes0, spec0), ctxt') = prep (constrn_fxs fixspec) eqns lthy
-    val fixes = map (apfst (apfst Binding.name_of)) fixes0;
-    val spec = map (fn (bnd, prop) => (bnd, [prop])) spec0;
-    val (eqs, post, sort_cont, cnames) = get_preproc lthy config ctxt' fixes spec
-
-    val defname = mk_defname fixes
-    val FunctionConfig {partials, tailrec, default, ...} = config
-    val _ =
-      if tailrec then Output.legacy_feature
-        "'function (tailrec)' command. Use 'partial_function (tailrec)'."
-      else ()
-    val _ =
-      if is_some default then Output.legacy_feature
-        "'function (default)'. Use 'partial_function'."
-      else ()
-
-    val ((goal_state, cont), lthy') =
-      prepare_function_mutual config defname fixes eqs lthy
-
-    fun afterqed [[proof]] lthy =
-      let
-        val FunctionResult {fs, R, psimps, trsimps, simple_pinducts,
-          termination, domintros, cases, ...} =
-          cont (Thm.close_derivation proof)
-
-        val fnames = map (fst o fst) fixes
-        fun qualify n = Binding.name n
-          |> Binding.qualify true defname
-        val conceal_partial = if partials then I else Binding.conceal
-
-        val addsmps = add_simps fnames post sort_cont
-
-        val (((psimps', pinducts'), (_, [termination'])), lthy) =
-          lthy
-          |> addsmps (conceal_partial o Binding.qualify false "partial")
-               "psimps" conceal_partial psimp_attribs psimps
-          ||> (case trsimps of NONE => I | SOME thms =>
-                   addsmps I "simps" I simp_attribs thms #> snd
-                   #> Spec_Rules.add Spec_Rules.Equational (fs, thms))
-          ||>> Local_Theory.note ((conceal_partial (qualify "pinduct"),
-                 [Attrib.internal (K (Rule_Cases.case_names cnames)),
-                  Attrib.internal (K (Rule_Cases.consumes 1)),
-                  Attrib.internal (K (Induct.induct_pred ""))]), simple_pinducts)
-          ||>> Local_Theory.note ((Binding.conceal (qualify "termination"), []), [termination])
-          ||> (snd o Local_Theory.note ((qualify "cases",
-                 [Attrib.internal (K (Rule_Cases.case_names cnames))]), [cases]))
-          ||> (case domintros of NONE => I | SOME thms => 
-                   Local_Theory.note ((qualify "domintros", []), thms) #> snd)
-
-        val info = { add_simps=addsmps, case_names=cnames, psimps=psimps',
-          pinducts=snd pinducts', simps=NONE, inducts=NONE, termination=termination',
-          fs=fs, R=R, defname=defname, is_partial=true }
-
-        val _ =
-          if not is_external then ()
-          else Specification.print_consts lthy (K false) (map fst fixes)
-      in
-        (info, 
-         lthy |> Local_Theory.declaration false (add_function_data o morph_function_data info))
-      end
-  in
-    ((goal_state, afterqed), lthy')
-  end
-
-*}
-
-ML {*
-fun gen_function is_external prep default_constraint fixspec eqns config lthy =
-  let
-    val ((goal_state, afterqed), lthy') =
-      prepare_function is_external prep default_constraint fixspec eqns config lthy
-  in
-    lthy'
-    |> Proof.theorem NONE (snd oo afterqed) [[(Logic.unprotect (concl_of goal_state), [])]]
-    |> Proof.refine (Method.primitive_text (K goal_state)) 
-    |> Seq.hd
-  end
-*}
-
-
-ML {*
-val function = gen_function false Specification.check_spec (Type_Infer.anyT HOLogic.typeS)
-val function_cmd = gen_function true Specification.read_spec "_::type"
-
-fun add_case_cong n thy =
-  let
-    val cong = #case_cong (Datatype.the_info thy n)
-      |> safe_mk_meta_eq
-  in
-    Context.theory_map
-      (Function_Ctx_Tree.map_function_congs (Thm.add_thm cong)) thy
-  end
-
-val setup_case_cong = Datatype.interpretation (K (fold add_case_cong))
-
-
-(* setup *)
-
-val setup =
-  Attrib.setup @{binding fundef_cong}
-    (Attrib.add_del Function_Ctx_Tree.cong_add Function_Ctx_Tree.cong_del)
-    "declaration of congruence rule for function definitions"
-  #> setup_case_cong
-  #> Function_Relation.setup
-  #> Function_Common.Termination_Simps.setup
-
-val get_congs = Function_Ctx_Tree.get_function_congs
-
-fun get_info ctxt t = Item_Net.retrieve (get_function ctxt) t
-  |> the_single |> snd
-
-
-(* outer syntax *)
-
-val _ =
-  Outer_Syntax.local_theory_to_proof "nominal_primrec" "define recursive functions for nominal types"
-  Keyword.thy_goal
-  (function_parser default_config
-     >> (fn ((config, fixes), statements) => function_cmd fixes statements config))
-*}
-
-ML {* trace := true *}
-
-lemma test:
-  assumes a: "[[x]]lst. t = [[x]]lst. t'"
-  shows "t = t'"
-using a
-apply(simp add: Abs_eq_iff)
-apply(erule exE)
-apply(simp only: alphas)
-apply(erule conjE)+
-apply(rule sym)
-apply(clarify)
-apply(rule supp_perm_eq)
-apply(subgoal_tac "set [x] \<sharp>* p")
-apply(auto simp add: fresh_star_def)[1]
-apply(simp)
-apply(simp add: fresh_star_def)
-apply(simp add: fresh_perm)
-done
-
-lemma test2:
-  assumes "a \<sharp> x" "c \<sharp> x" "b \<sharp> y" "c \<sharp> y"
-  and "(a \<rightleftharpoons> c) \<bullet> x = (b \<rightleftharpoons> c) \<bullet> y"
-  shows "x = y"
-using assms by (simp add: swap_fresh_fresh)
-
-lemma test3:
-  assumes "x = y"
-  and "a \<sharp> x" "c \<sharp> x" "b \<sharp> y" "c \<sharp> y"
-  shows "(a \<rightleftharpoons> c) \<bullet> x = (b \<rightleftharpoons> c) \<bullet> y"
-using assms by (simp add: swap_fresh_fresh)
-
-nominal_primrec
-  depth :: "lam \<Rightarrow> nat"
-where
-  "depth (Var x) = 1"
-| "depth (App t1 t2) = (max (depth t1) (depth t2)) + 1"
-| "depth (Lam x t) = (depth t) + 1"
-apply(rule_tac y="x" in lam.exhaust)
-apply(simp_all)[3]
-apply(simp_all only: lam.distinct)
-apply(simp add: lam.eq_iff)
-apply(simp add: lam.eq_iff)
-apply(subst (asm) Abs_eq_iff)
-apply(erule exE)
-apply(simp add: alphas)
-apply(clarify)
-oops
-
-lemma removeAll_eqvt[eqvt]:
-  shows "p \<bullet> (removeAll x xs) = removeAll (p \<bullet> x) (p \<bullet> xs)"
-by (induct xs) (auto)
-
-nominal_primrec 
-  frees_lst :: "lam \<Rightarrow> atom list"
-where
-  "frees_lst (Var x) = [atom x]"
-| "frees_lst (App t1 t2) = (frees_lst t1) @ (frees_lst t2)"
-| "frees_lst (Lam x t) = removeAll (atom x) (frees_lst t)"
-apply(rule_tac y="x" in lam.exhaust)
-apply(simp_all)[3]
-apply(simp_all only: lam.distinct)
-apply(simp add: lam.eq_iff)
-apply(simp add: lam.eq_iff)
-apply(simp add: lam.eq_iff)
-apply(simp add: Abs_eq_iff)
-apply(erule exE)
-apply(simp add: alphas)
-apply(simp add: atom_eqvt)
-apply(clarify)
-oops
-
-nominal_primrec
-  subst :: "lam \<Rightarrow> name \<Rightarrow> lam \<Rightarrow> lam"  ("_ [_ ::= _]" [100,100,100] 100)
-where
-  "(Var x)[y ::= s] = (if x=y then s else (Var x))"
-| "(App t\<^isub>1 t\<^isub>2)[y ::= s] = App (t\<^isub>1[y ::= s]) (t\<^isub>2[y ::= s])"
-| "atom x \<sharp> (y, s) \<Longrightarrow> (Lam x t)[y ::= s] = Lam x (t[y ::= s])"
-apply(case_tac x)
-apply(simp)
-apply(rule_tac y="a" and c="(b, c)" in lam.strong_exhaust)
-apply(simp add: lam.eq_iff lam.distinct)
-apply(auto)[1]
-apply(simp add: lam.eq_iff lam.distinct)
-apply(auto)[1]
-apply(simp add: fresh_star_def lam.eq_iff lam.distinct)
-apply(simp_all add: lam.distinct)[5]
-apply(simp add: lam.eq_iff)
-apply(simp add: lam.eq_iff)
-apply(simp add: lam.eq_iff)
-apply(erule conjE)+
-oops
-
-
-
-nominal_primrec
-  depth :: "lam \<Rightarrow> nat"
-where
-  "depth (Var x) = 1"
-| "depth (App t1 t2) = (max (depth t1) (depth t2)) + 1"
-| "depth (Lam x t) = (depth t) + 1"
-apply(rule_tac y="x" in lam.exhaust)
-apply(simp_all)[3]
-apply(simp_all only: lam.distinct)
-apply(simp add: lam.eq_iff)
-apply(simp add: lam.eq_iff)
-(*
-apply(subst (asm) Abs_eq_iff)
-apply(erule exE)
-apply(simp add: alphas)
-apply(clarify)
-*)
-apply(subgoal_tac "finite (supp (x, xa, t, ta, depth_sumC t, depth_sumC ta))")
-apply(erule_tac ?'a="name" in obtain_at_base)
-unfolding fresh_def[symmetric]
-apply(drule_tac a="atom x" and b="atom xa" and c="atom a" in test3)
-apply(simp add: Abs_fresh_iff)
-apply(simp add: Abs_fresh_iff)
-apply(simp add: Abs_fresh_iff)
-apply(simp add: Abs_fresh_iff)
-apply(rule_tac a="atom x" and b="atom xa" and c="atom a" in test2)
-apply(simp add: pure_fresh)
-apply(simp add: pure_fresh)
-apply(simp add: pure_fresh)
-apply(simp add: pure_fresh)
-apply(simp add: eqvt_at_def)
-apply(drule test)
-apply(simp)
-apply(simp add: finite_supp)
-done
-
-termination depth
-  apply(relation "measure size")
-  apply(auto simp add: lam.size)
-  done
-
-thm depth.psimps
-thm depth.simps
-
-
-lemma swap_set_not_in_at:
-  fixes a b::"'a::at"
-  and   S::"'a::at set"
-  assumes a: "a \<notin> S" "b \<notin> S"
-  shows "(a \<leftrightarrow> b) \<bullet> S = S"
-  unfolding permute_set_def
-  using a by (auto simp add: permute_flip_at)
-
-lemma removeAll_eqvt[eqvt]:
-  shows "p \<bullet> (removeAll x xs) = removeAll (p \<bullet> x) (p \<bullet> xs)"
-by (induct xs) (auto)
-
-nominal_primrec 
-  frees_lst :: "lam \<Rightarrow> atom list"
-where
-  "frees_lst (Var x) = [atom x]"
-| "frees_lst (App t1 t2) = (frees_lst t1) @ (frees_lst t2)"
-| "frees_lst (Lam x t) = removeAll (atom x) (frees_lst t)"
-apply(rule_tac y="x" in lam.exhaust)
-apply(simp_all)[3]
-apply(simp_all only: lam.distinct)
-apply(simp add: lam.eq_iff)
-apply(simp add: lam.eq_iff)
-apply(simp add: lam.eq_iff)
-apply(simp add: Abs_eq_iff)
-apply(erule exE)
-apply(simp add: alphas)
-apply(simp add: atom_eqvt)
-apply(clarify)
-apply(rule trans)
-apply(rule sym)
-apply(rule_tac p="p" in supp_perm_eq)
-oops
-
-nominal_primrec 
-  frees :: "lam \<Rightarrow> name set"
-where
-  "frees (Var x) = {x}"
-| "frees (App t1 t2) = (frees t1) \<union> (frees t2)"
-| "frees (Lam x t) = (frees t) - {x}"
-apply(rule_tac y="x" in lam.exhaust)
-apply(simp_all)[3]
-apply(simp_all only: lam.distinct)
-apply(simp add: lam.eq_iff)
-apply(simp add: lam.eq_iff)
-apply(simp add: lam.eq_iff)
-apply(subgoal_tac "finite (supp (x, xa, t, ta, frees_sumC t, frees_sumC ta))")
-apply(erule_tac ?'a="name" in obtain_at_base)
-unfolding fresh_def[symmetric]
-apply(drule_tac a="atom x" and b="atom xa" and c="atom a" in test3)
-apply(simp add: Abs_fresh_iff)
-apply(simp add: Abs_fresh_iff)
-apply(simp add: Abs_fresh_iff)
-apply(simp add: Abs_fresh_iff)
-apply(simp)
-apply(drule test)
-apply(rule_tac t="frees_sumC t - {x}" and s="(x \<leftrightarrow> a) \<bullet> (frees_sumC t - {x})" in subst)
-oops
-
-thm Abs_eq_iff[simplified alphas]
-
-lemma Abs_set_eq_iff2:
-  fixes x y::"'a::fs"
-  shows "[bs]set. x = [cs]set. y \<longleftrightarrow>
-    (\<exists>p. supp ([bs]set. x) = supp ([cs]set. y) \<and>
-         supp ([bs]set. x) \<sharp>* p \<and>
-         p \<bullet> x = y \<and> p \<bullet> bs = cs)"
-unfolding Abs_eq_iff
-unfolding alphas
-unfolding supp_Abs
-by simp
-
-lemma Abs_set_eq_iff3:
-  fixes x y::"'a::fs"
-  assumes a: "finite bs" "finite cs"
-  shows "[bs]set. x = [cs]set. y \<longleftrightarrow>
-    (\<exists>p. supp ([bs]set. x) = supp ([cs]set. y) \<and>
-         supp ([bs]set. x) \<sharp>* p \<and>
-         p \<bullet> x = y \<and> p \<bullet> bs = cs \<and>
-         supp p \<subseteq> bs \<union> cs)"
-unfolding Abs_eq_iff
-unfolding alphas
-unfolding supp_Abs
-apply(auto)
-using set_renaming_perm
-sorry
-
-lemma Abs_eq_iff2:
-  fixes x y::"'a::fs"
-  shows "[bs]lst. x = [cs]lst. y \<longleftrightarrow>
-    (\<exists>p. supp ([bs]lst. x) = supp ([cs]lst. y) \<and>
-         supp ([bs]lst. x) \<sharp>* p \<and>
-         p \<bullet> x = y \<and> p \<bullet> bs = cs)"
-unfolding Abs_eq_iff
-unfolding alphas
-unfolding supp_Abs
-by simp
-
-lemma Abs_eq_iff3:
-  fixes x y::"'a::fs"
-  shows "[bs]lst. x = [cs]lst. y \<longleftrightarrow>
-    (\<exists>p. supp ([bs]lst. x) = supp ([cs]lst. y) \<and>
-         supp ([bs]lst. x) \<sharp>* p \<and>
-         p \<bullet> x = y \<and> p \<bullet> bs = cs \<and>
-         supp p \<subseteq> set bs \<union> set cs)"
-unfolding Abs_eq_iff
-unfolding alphas
-unfolding supp_Abs
-apply(auto)
-using list_renaming_perm
-apply -
-apply(drule_tac x="bs" in meta_spec)
-apply(drule_tac x="p" in meta_spec)
-apply(erule exE)
-apply(rule_tac x="q" in exI)
-apply(simp add: set_eqvt)
-sorry
-
-nominal_primrec
-  subst :: "lam \<Rightarrow> name \<Rightarrow> lam \<Rightarrow> lam"  ("_ [_ ::= _]" [100,100,100] 100)
-where
-  "(Var x)[y ::= s] = (if x=y then s else (Var x))"
-| "(App t\<^isub>1 t\<^isub>2)[y ::= s] = App (t\<^isub>1[y ::= s]) (t\<^isub>2[y ::= s])"
-| "atom x \<sharp> (y, s) \<Longrightarrow> (Lam x t)[y ::= s] = Lam x (t[y ::= s])"
-apply(case_tac x)
-apply(simp)
-apply(rule_tac y="a" and c="(b, c)" in lam.strong_exhaust)
-apply(simp add: lam.eq_iff lam.distinct)
-apply(auto)[1]
-apply(simp add: lam.eq_iff lam.distinct)
-apply(auto)[1]
-apply(simp add: fresh_star_def lam.eq_iff lam.distinct)
-apply(simp_all add: lam.distinct)[5]
-apply(simp add: lam.eq_iff)
-apply(simp add: lam.eq_iff)
-apply(simp add: lam.eq_iff)
-apply(erule conjE)+
-apply(subst (asm) Abs_eq_iff3) 
-apply(erule exE)
-apply(erule conjE)+
-apply(clarify)
-apply(perm_simp)
-apply(simp)
-apply(rule trans)
-apply(rule sym)
-apply(rule_tac p="p" in supp_perm_eq)
-apply(rule fresh_star_supp_conv)
-apply(drule fresh_star_supp_conv)
-apply(simp add: Abs_fresh_star_iff)
-thm fresh_eqvt_at
-apply(rule_tac f="subst_sumC" in fresh_eqvt_at)
-apply(assumption)
-apply(simp add: finite_supp)
-prefer 2
-apply(simp)
-apply(simp add: eqvt_at_def)
-apply(perm_simp)
-apply(subgoal_tac "p \<bullet> ya = ya")
-apply(subgoal_tac "p \<bullet> sa = sa")
-apply(simp)
-apply(rule supp_perm_eq)
-apply(rule fresh_star_supp_conv)
-apply(auto simp add: fresh_star_def fresh_Pair)[1]
-apply(rule supp_perm_eq)
-apply(rule fresh_star_supp_conv)
-apply(auto simp add: fresh_star_def fresh_Pair)[1]
-
-
-
-nominal_primrec
-  subst :: "lam \<Rightarrow> name \<Rightarrow> lam \<Rightarrow> lam"  ("_ [_ ::= _]" [100,100,100] 100)
-where
-  "(Var x)[y ::= s] = (if x=y then s else (Var x))"
-| "(App t\<^isub>1 t\<^isub>2)[y ::= s] = App (t\<^isub>1[y ::= s]) (t\<^isub>2[y ::= s])"
-| "atom x \<sharp> (y, s) \<Longrightarrow> (Lam x t)[y ::= s] = Lam x (t[y ::= s])"
-apply(case_tac x)
-apply(simp)
-apply(rule_tac y="a" and c="(b, c)" in lam.strong_exhaust)
-apply(simp add: lam.eq_iff lam.distinct)
-apply(auto)[1]
-apply(simp add: lam.eq_iff lam.distinct)
-apply(auto)[1]
-apply(simp add: fresh_star_def lam.eq_iff lam.distinct)
-apply(simp_all add: lam.distinct)[5]
-apply(simp add: lam.eq_iff)
-apply(simp add: lam.eq_iff)
-apply(simp add: lam.eq_iff)
-apply(subgoal_tac "finite (supp (ya, sa, x, xa, t, ta, subst_sumC (t, ya, sa), subst_sumC (ta, ya, sa)))")
-apply(erule_tac ?'a="name" in obtain_at_base)
-unfolding fresh_def[symmetric]
-apply(rule_tac a="atom x" and b="atom xa" and c="atom a" in test2)
-apply(simp add: Abs_fresh_iff)
-apply(simp add: Abs_fresh_iff)
-apply(simp add: Abs_fresh_iff)
-apply(simp add: Abs_fresh_iff)
-apply(erule conjE)+
-apply(drule_tac a="atom x" and b="atom xa" and c="atom a" in test3)
-apply(simp add: Abs_fresh_iff)
-apply(simp add: Abs_fresh_iff)
-apply(simp add: Abs_fresh_iff)
-apply(simp add: Abs_fresh_iff)
-apply(simp add: eqvt_at_def)
-apply(drule test)
-apply(simp)
-apply(subst (2) swap_fresh_fresh)
-apply(simp)
-apply(simp)
-apply(subst (2) swap_fresh_fresh)
-apply(simp)
-apply(simp)
-apply(subst (3) swap_fresh_fresh)
-apply(simp)
-apply(simp)
-apply(subst (3) swap_fresh_fresh)
-apply(simp)
-apply(simp)
-apply(simp)
-apply(simp add: finite_supp)
-done
-
-(* this should not work *)
-nominal_primrec 
-  bnds :: "lam \<Rightarrow> name set"
-where
-  "bnds (Var x) = {}"
-| "bnds (App t1 t2) = (bnds t1) \<union> (bnds t2)"
-| "bnds (Lam x t) = (bnds t) \<union> {x}"
-apply(rule_tac y="x" in lam.exhaust)
-apply(simp_all)[3]
-apply(simp_all only: lam.distinct)
-apply(simp add: lam.eq_iff)
-apply(simp add: lam.eq_iff)
-apply(simp add: lam.eq_iff)
-sorry
-
-end
-
-
-
diff -r b6873d123f9b -r 89715c48f728 Nominal/Ex/Lambda_F_T.thy
--- a/Nominal/Ex/Lambda_F_T.thy	Sat May 12 21:39:09 2012 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,183 +0,0 @@
-theory Lambda
-imports "../Nominal2" 
-begin
-
-atom_decl name
-
-nominal_datatype lam =
-  Var "name"
-| App "lam" "lam"
-| Lam x::"name" l::"lam"  binds x in l ("Lam [_]. _" [100, 100] 100)
-
-lemma fresh_fun_eqvt_app3:
-  assumes a: "eqvt f"
-  and b: "a \<sharp> x" "a \<sharp> y" "a \<sharp> z"
-  shows "a \<sharp> f x y z"
-  using fresh_fun_eqvt_app[OF a b(1)] a b
-  by (metis fresh_fun_app)
-
-lemma fresh_fun_eqvt_app4:
-  assumes a: "eqvt f"
-  and b: "a \<sharp> x" "a \<sharp> y" "a \<sharp> z" "a \<sharp> w"
-  shows "a \<sharp> f x y z w"
-  using fresh_fun_eqvt_app[OF a b(1)] a b
-  by (metis fresh_fun_app)
-
-lemma the_default_pty:
-  assumes f_def: "f == (\<lambda>x::'a. THE_default d (G x))"
-  and unique: "\<exists>!y. G x y"
-  and pty: "\<And>x y. G x y \<Longrightarrow> P x y"
-  shows "P x (f x)"
-  apply(subst f_def)
-  apply (rule ex1E[OF unique])
-  apply (subst THE_default1_equality[OF unique])
-  apply assumption
-  apply (rule pty)
-  apply assumption
-  done
-
-locale test =
-  fixes f1::"name \<Rightarrow> name list \<Rightarrow> ('a::pt)"
-    and f2::"lam \<Rightarrow> lam \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> name list \<Rightarrow> ('a::pt)"
-    and f3::"name \<Rightarrow> lam \<Rightarrow> 'a \<Rightarrow> name list \<Rightarrow> ('a::pt)"
-  assumes fs: "finite (supp (f1, f2, f3))"
-    and eq: "eqvt f1" "eqvt f2" "eqvt f3"
-    and fcb1: "\<And>l n. atom ` set l \<sharp>* f1 n l"
-    and fcb2: "\<And>l t1 t2 r1 r2. atom ` set l \<sharp>* (r1, r2) \<Longrightarrow> atom ` set l \<sharp>* f2 t1 t2 r1 r2 l"
-    and fcb3: "\<And>t l r. atom ` set (x # l) \<sharp>* r \<Longrightarrow> atom ` set (x # l) \<sharp>* f3 x t r l"
-begin
-
-nominal_primrec (invariant "\<lambda>(x, l) y. atom ` set l \<sharp>* y")
-  f
-where
-  "f (Var x) l = f1 x l"
-| "f (App t1 t2) l = f2 t1 t2 (f t1 l) (f t2 l) l"
-| "atom x \<sharp> l \<Longrightarrow> (f (Lam [x].t) l) = f3 x t (f t (x # l)) l"
-  apply (simp add: eqvt_def f_graph_def)
-  apply (rule, perm_simp)
-  apply (simp only: eq[unfolded eqvt_def])
-  apply (erule f_graph.induct)
-  apply (simp add: fcb1)
-  apply (simp add: fcb2 fresh_star_Pair)
-  apply simp
-  apply (subgoal_tac "atom ` set (xa # l) \<sharp>* f3 xa t (f_sum (t, xa # l)) l")
-  apply (simp add: fresh_star_def)
-  apply (rule fcb3)
-  apply (simp add: fresh_star_def fresh_def)
-  apply simp_all
-  apply(case_tac x)
-  apply(rule_tac y="a" and c="b" in lam.strong_exhaust)
-  apply(auto simp add: fresh_star_def)
-  apply(erule Abs_lst1_fcb)
-  apply (subgoal_tac "atom ` set (x # la) \<sharp>* f3 x t (f_sumC (t, x # la)) la")
-  apply (simp add: fresh_star_def)
-  apply (rule fcb3)
-  apply (simp add: fresh_star_def)
-  apply (rule fresh_fun_eqvt_app4[OF eq(3)])
-  apply (simp add: fresh_at_base)
-  apply assumption
-  apply (erule fresh_eqvt_at)
-  apply (simp add: finite_supp)
-  apply (simp add: fresh_Pair fresh_Cons fresh_at_base)
-  apply assumption
-  apply (subgoal_tac "\<And>p y r l. p \<bullet> (f3 x y r l) = f3 (p \<bullet> x) (p \<bullet> y) (p \<bullet> r) (p \<bullet> l)")
-  apply (subgoal_tac "(atom x \<rightleftharpoons> atom xa) \<bullet> la = la")
-  apply (simp add: eqvt_at_def)
-  apply (simp add: swap_fresh_fresh)
-  apply (simp add: permute_fun_app_eq eq[unfolded eqvt_def])
-  apply simp
-  done
-
-termination
-  by (relation "measure (\<lambda>(x,_). size x)") (auto simp add: lam.size)
-
-end
-
-section {* Locally Nameless Terms *}
-
-nominal_datatype ln = 
-  LNBnd nat
-| LNVar name
-| LNApp ln ln
-| LNLam ln
-
-fun
-  lookup :: "name list \<Rightarrow> nat \<Rightarrow> name \<Rightarrow> ln" 
-where
-  "lookup [] n x = LNVar x"
-| "lookup (y # ys) n x = (if x = y then LNBnd n else (lookup ys (n + 1) x))"
-
-lemma lookup_eqvt[eqvt]:
-  shows "(p \<bullet> lookup xs n x) = lookup (p \<bullet> xs) (p \<bullet> n) (p \<bullet> x)"
-  by (induct xs arbitrary: n) (simp_all add: permute_pure)
-
-lemma fresh_at_list: "atom x \<sharp> xs \<longleftrightarrow> x \<notin> set xs"
-  unfolding fresh_def supp_set[symmetric]
-  apply (induct xs)
-  apply (simp add: supp_set_empty)
-  apply simp
-  apply auto
-  apply (simp_all add: insert_absorb UnI2 finite_set supp_of_finite_insert supp_at_base)
-  done
-
-interpretation trans: test
-  "%x l. lookup l 0 x"
-  "%t1 t2 r1 r2 l. LNApp r1 r2"
-  "%n t r l. LNLam r"
-  apply default
-  apply (auto simp add: pure_fresh supp_Pair)
-  apply (simp_all add: fresh_def supp_def permute_fun_def permute_pure lookup_eqvt)[3]
-  apply (simp_all add: eqvt_def permute_fun_def permute_pure lookup_eqvt)
-  apply (simp add: fresh_star_def)
-  apply (rule_tac x="0 :: nat" in spec)
-  apply (induct_tac l)
-  apply (simp add: ln.fresh pure_fresh)
-  apply (auto simp add: ln.fresh pure_fresh)[1]
-  apply (case_tac "a \<in> set list")
-  apply simp
-  apply (rule_tac f="lookup" in fresh_fun_eqvt_app3)
-  unfolding eqvt_def
-  apply rule
-  using eqvts_raw(35)
-  apply auto[1]
-  apply (simp add: fresh_at_list)
-  apply (simp add: pure_fresh)
-  apply (simp add: fresh_at_base)
-  apply (simp add: fresh_star_Pair fresh_star_def ln.fresh)
-  apply (simp add: fresh_star_def ln.fresh)
-  done
-
-thm trans.f.simps
-
-lemma lam_strong_exhaust2:
-  "\<lbrakk>\<And>name. y = Var name \<Longrightarrow> P; 
-    \<And>lam1 lam2. y = App lam1 lam2 \<Longrightarrow> P;
-    \<And>name lam. \<lbrakk>{atom name} \<sharp>* c; y = Lam [name]. lam\<rbrakk> \<Longrightarrow> P;
-    finite (supp c)\<rbrakk>
-    \<Longrightarrow> P"
-sorry
-
-nominal_primrec
-  g
-where
-  "(~finite (supp (g1, g2, g3))) \<Longrightarrow> g g1 g2 g3 t = t"
-| "finite (supp (g1, g2, g3)) \<Longrightarrow> g g1 g2 g3 (Var x) = g1 x"
-| "finite (supp (g1, g2, g3)) \<Longrightarrow> g g1 g2 g3 (App t1 t2) = g2 t1 t2 (g g1 g2 g3 t1) (g g1 g2 g3 t2)"
-| "finite (supp (g1, g2, g3)) \<Longrightarrow> atom x \<sharp> (g1,g2,g3) \<Longrightarrow> (g g1 g2 g3 (Lam [x].t)) = g3 x t (g g1 g2 g3 t)"
-  apply (simp add: eqvt_def g_graph_def)
-  apply (rule, perm_simp, rule)
-  apply simp_all
-  apply (case_tac x)
-  apply (case_tac "finite (supp (a, b, c))")
-  prefer 2
-  apply simp
-  apply(rule_tac y="d" and c="(a,b,c)" in lam_strong_exhaust2)
-  apply auto
-  apply blast
-  apply (simp add: Abs1_eq_iff fresh_star_def)
-  sorry
-
-termination
-  by (relation "measure (\<lambda>(_,_,_,t). size t)") (simp_all add: lam.size)
-
-end
diff -r b6873d123f9b -r 89715c48f728 Nominal/Ex/Lambda_F_T_FCB2.thy
--- a/Nominal/Ex/Lambda_F_T_FCB2.thy	Sat May 12 21:39:09 2012 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,270 +0,0 @@
-theory Lambda
-imports "../Nominal2" 
-begin
-
-atom_decl name
-
-nominal_datatype lam =
-  Var "name"
-| App "lam" "lam"
-| Lam x::"name" l::"lam"  bind x in l ("Lam [_]. _" [100, 100] 100)
-
-lemma fresh_fun_eqvt_app3:
-  assumes a: "eqvt f"
-  and b: "a \<sharp> x" "a \<sharp> y" "a \<sharp> z"
-  shows "a \<sharp> f x y z"
-  using fresh_fun_eqvt_app[OF a b(1)] a b
-  by (metis fresh_fun_app)
-
-lemma fresh_fun_eqvt_app4:
-  assumes a: "eqvt f"
-  and b: "a \<sharp> x" "a \<sharp> y" "a \<sharp> z" "a \<sharp> w"
-  shows "a \<sharp> f x y z w"
-  using fresh_fun_eqvt_app[OF a b(1)] a b
-  by (metis fresh_fun_app)
-
-lemma the_default_pty:
-  assumes f_def: "f == (\<lambda>x::'a. THE_default d (G x))"
-  and unique: "\<exists>!y. G x y"
-  and pty: "\<And>x y. G x y \<Longrightarrow> P x y"
-  shows "P x (f x)"
-  apply(subst f_def)
-  apply (rule ex1E[OF unique])
-  apply (subst THE_default1_equality[OF unique])
-  apply assumption
-  apply (rule pty)
-  apply assumption
-  done
-
-lemma Abs_lst1_fcb2:
-  fixes a b :: "'a :: at"
-    and S T :: "'b :: fs"
-    and c::"'c::fs"
-  assumes e: "(Abs_lst [atom a] T) = (Abs_lst [atom b] S)"
-  and fcb: "\<And>a T. atom a \<sharp> f a T c"
-  and fresh: "{atom a, atom b} \<sharp>* c"
-  and perm1: "\<And>p. supp p \<sharp>* c \<Longrightarrow> p \<bullet> (f a T c) = f (p \<bullet> a) (p \<bullet> T) c"
-  and perm2: "\<And>p. supp p \<sharp>* c \<Longrightarrow> p \<bullet> (f b S c) = f (p \<bullet> b) (p \<bullet> S) c"
-  shows "f a T c = f b S c"
-proof -
-  have fin1: "finite (supp (f a T c))"
-    apply(rule_tac S="supp (a, T, c)" in supports_finite)
-    apply(simp add: supports_def)
-    apply(simp add: fresh_def[symmetric])
-    apply(clarify)
-    apply(subst perm1)
-    apply(simp add: supp_swap fresh_star_def)
-    apply(simp add: swap_fresh_fresh fresh_Pair)
-    apply(simp add: finite_supp)
-    done
-  have fin2: "finite (supp (f b S c))"
-    apply(rule_tac S="supp (b, S, c)" in supports_finite)
-    apply(simp add: supports_def)
-    apply(simp add: fresh_def[symmetric])
-    apply(clarify)
-    apply(subst perm2)
-    apply(simp add: supp_swap fresh_star_def)
-    apply(simp add: swap_fresh_fresh fresh_Pair)
-    apply(simp add: finite_supp)
-    done
-  obtain d::"'a::at" where fr: "atom d \<sharp> (a, b, S, T, c, f a T c, f b S c)" 
-    using obtain_fresh'[where x="(a, b, S, T, c, f a T c, f b S c)"]
-    apply(auto simp add: finite_supp supp_Pair fin1 fin2)
-    done
-  have "(a \<leftrightarrow> d) \<bullet> (Abs_lst [atom a] T) = (b \<leftrightarrow> d) \<bullet> (Abs_lst [atom b] S)" 
-    apply(simp (no_asm_use) only: flip_def)
-    apply(subst swap_fresh_fresh)
-    apply(simp add: Abs_fresh_iff)
-    using fr
-    apply(simp add: Abs_fresh_iff)
-    apply(subst swap_fresh_fresh)
-    apply(simp add: Abs_fresh_iff)
-    using fr
-    apply(simp add: Abs_fresh_iff)
-    apply(rule e)
-    done
-  then have "Abs_lst [atom d] ((a \<leftrightarrow> d) \<bullet> T) = Abs_lst [atom d] ((b \<leftrightarrow> d) \<bullet> S)"
-    apply (simp add: swap_atom flip_def)
-    done
-  then have eq: "(a \<leftrightarrow> d) \<bullet> T = (b \<leftrightarrow> d) \<bullet> S"
-    by (simp add: Abs1_eq_iff)
-  have "f a T c = (a \<leftrightarrow> d) \<bullet> f a T c"
-    unfolding flip_def
-    apply(rule sym)
-    apply(rule swap_fresh_fresh)
-    using fcb[where a="a"] 
-    apply(simp)
-    using fr
-    apply(simp add: fresh_Pair)
-    done
-  also have "... = f d ((a \<leftrightarrow> d) \<bullet> T) c"
-    unfolding flip_def
-    apply(subst perm1)
-    using fresh fr
-    apply(simp add: supp_swap fresh_star_def fresh_Pair)
-    apply(simp)
-    done
-  also have "... = f d ((b \<leftrightarrow> d) \<bullet> S) c" using eq by simp
-  also have "... = (b \<leftrightarrow> d) \<bullet> f b S c"
-    unfolding flip_def
-    apply(subst perm2)
-    using fresh fr
-    apply(simp add: supp_swap fresh_star_def fresh_Pair)
-    apply(simp)
-    done
-  also have "... = f b S c"   
-    apply(rule flip_fresh_fresh)
-    using fcb[where a="b"] 
-    apply(simp)
-    using fr
-    apply(simp add: fresh_Pair)
-    done
-  finally show ?thesis by simp
-qed
-
-locale test =
-  fixes f1::"name \<Rightarrow> name list \<Rightarrow> ('a::pt)"
-    and f2::"lam \<Rightarrow> lam \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> name list \<Rightarrow> ('a::pt)"
-    and f3::"name \<Rightarrow> lam \<Rightarrow> 'a \<Rightarrow> name list \<Rightarrow> ('a::pt)"
-  assumes fs: "finite (supp (f1, f2, f3))"
-    and eq: "eqvt f1" "eqvt f2" "eqvt f3"
-    and fcb1: "\<And>l n. atom ` set l \<sharp>* f1 n l"
-    and fcb2: "\<And>l t1 t2 r1 r2. atom ` set l \<sharp>* (r1, r2) \<Longrightarrow> atom ` set l \<sharp>* f2 t1 t2 r1 r2 l"
-    and fcb3: "\<And>t l r. atom ` set (x # l) \<sharp>* r \<Longrightarrow> atom ` set (x # l) \<sharp>* f3 x t r l"
-begin
-
-nominal_primrec (invariant "\<lambda>(x, l) y. atom ` set l \<sharp>* y")
-  f
-where
-  "f (Var x) l = f1 x l"
-| "f (App t1 t2) l = f2 t1 t2 (f t1 l) (f t2 l) l"
-| "atom x \<sharp> l \<Longrightarrow> (f (Lam [x].t) l) = f3 x t (f t (x # l)) l"
-  apply (simp add: eqvt_def f_graph_def)
-  apply (rule, perm_simp)
-  apply (simp only: eq[unfolded eqvt_def])
-  apply (erule f_graph.induct)
-  apply (simp add: fcb1)
-  apply (simp add: fcb2 fresh_star_Pair)
-  apply simp
-  apply (subgoal_tac "atom ` set (xa # l) \<sharp>* f3 xa t (f_sum (t, xa # l)) l")
-  apply (simp add: fresh_star_def)
-  apply (rule fcb3)
-  apply (simp add: fresh_star_def fresh_def)
-  apply simp_all
-  apply(case_tac x)
-  apply(rule_tac y="a" and c="b" in lam.strong_exhaust)
-  apply(auto simp add: fresh_star_def)
-  apply(erule_tac Abs_lst1_fcb2)
---"?"
-  apply (subgoal_tac "atom ` set (a # la) \<sharp>* f3 a T (f_sumC (T, a # la)) la")
-  apply (simp add: fresh_star_def)
-  apply (rule fcb3)
-  apply (simp add: fresh_star_def)
-  apply (rule fresh_fun_eqvt_app4[OF eq(3)])
-  apply (simp add: fresh_at_base)
-  apply assumption
-  apply (erule fresh_eqvt_at)
-  apply (simp add: finite_supp)
-  apply (simp add: fresh_Pair fresh_Cons fresh_at_base)
-  apply assumption
-  apply (subgoal_tac "\<And>p y r l. p \<bullet> (f3 x y r l) = f3 (p \<bullet> x) (p \<bullet> y) (p \<bullet> r) (p \<bullet> l)")
-  apply (subgoal_tac "(atom x \<rightleftharpoons> atom xa) \<bullet> la = la")
-  apply (simp add: eqvt_at_def)
-  apply (simp add: swap_fresh_fresh)
-  apply (simp add: permute_fun_app_eq eq[unfolded eqvt_def])
-  apply simp
-  done
-
-termination
-  by (relation "measure (\<lambda>(x,_). size x)") (auto simp add: lam.size)
-
-end
-
-section {* Locally Nameless Terms *}
-
-nominal_datatype ln = 
-  LNBnd nat
-| LNVar name
-| LNApp ln ln
-| LNLam ln
-
-fun
-  lookup :: "name list \<Rightarrow> nat \<Rightarrow> name \<Rightarrow> ln" 
-where
-  "lookup [] n x = LNVar x"
-| "lookup (y # ys) n x = (if x = y then LNBnd n else (lookup ys (n + 1) x))"
-
-lemma lookup_eqvt[eqvt]:
-  shows "(p \<bullet> lookup xs n x) = lookup (p \<bullet> xs) (p \<bullet> n) (p \<bullet> x)"
-  by (induct xs arbitrary: n) (simp_all add: permute_pure)
-
-lemma fresh_at_list: "atom x \<sharp> xs \<longleftrightarrow> x \<notin> set xs"
-  unfolding fresh_def supp_set[symmetric]
-  apply (induct xs)
-  apply (simp add: supp_set_empty)
-  apply simp
-  apply auto
-  apply (simp_all add: insert_absorb UnI2 finite_set supp_of_finite_insert supp_at_base)
-  done
-
-interpretation trans: test
-  "%x l. lookup l 0 x"
-  "%t1 t2 r1 r2 l. LNApp r1 r2"
-  "%n t r l. LNLam r"
-  apply default
-  apply (auto simp add: pure_fresh supp_Pair)
-  apply (simp_all add: fresh_def supp_def permute_fun_def permute_pure lookup_eqvt)[3]
-  apply (simp_all add: eqvt_def permute_fun_def permute_pure lookup_eqvt)
-  apply (simp add: fresh_star_def)
-  apply (rule_tac x="0 :: nat" in spec)
-  apply (induct_tac l)
-  apply (simp add: ln.fresh pure_fresh)
-  apply (auto simp add: ln.fresh pure_fresh)[1]
-  apply (case_tac "a \<in> set list")
-  apply simp
-  apply (rule_tac f="lookup" in fresh_fun_eqvt_app3)
-  unfolding eqvt_def
-  apply rule
-  using eqvts_raw(35)
-  apply auto[1]
-  apply (simp add: fresh_at_list)
-  apply (simp add: pure_fresh)
-  apply (simp add: fresh_at_base)
-  apply (simp add: fresh_star_Pair fresh_star_def ln.fresh)
-  apply (simp add: fresh_star_def ln.fresh)
-  done
-
-thm trans.f.simps
-
-lemma lam_strong_exhaust2:
-  "\<lbrakk>\<And>name. y = Var name \<Longrightarrow> P; 
-    \<And>lam1 lam2. y = App lam1 lam2 \<Longrightarrow> P;
-    \<And>name lam. \<lbrakk>{atom name} \<sharp>* c; y = Lam [name]. lam\<rbrakk> \<Longrightarrow> P;
-    finite (supp c)\<rbrakk>
-    \<Longrightarrow> P"
-sorry
-
-nominal_primrec
-  g
-where
-  "(~finite (supp (g1, g2, g3))) \<Longrightarrow> g g1 g2 g3 t = t"
-| "finite (supp (g1, g2, g3)) \<Longrightarrow> g g1 g2 g3 (Var x) = g1 x"
-| "finite (supp (g1, g2, g3)) \<Longrightarrow> g g1 g2 g3 (App t1 t2) = g2 t1 t2 (g g1 g2 g3 t1) (g g1 g2 g3 t2)"
-| "finite (supp (g1, g2, g3)) \<Longrightarrow> atom x \<sharp> (g1,g2,g3) \<Longrightarrow> (g g1 g2 g3 (Lam [x].t)) = g3 x t (g g1 g2 g3 t)"
-  apply (simp add: eqvt_def g_graph_def)
-  apply (rule, perm_simp, rule)
-  apply simp_all
-  apply (case_tac x)
-  apply (case_tac "finite (supp (a, b, c))")
-  prefer 2
-  apply simp
-  apply(rule_tac y="d" and c="(a,b,c)" in lam_strong_exhaust2)
-  apply auto
-  apply blast
-  apply (simp add: Abs1_eq_iff fresh_star_def)
-  sorry
-
-termination
-  by (relation "measure (\<lambda>(_,_,_,t). size t)") (simp_all add: lam.size)
-
-end
diff -r b6873d123f9b -r 89715c48f728 Nominal/Ex/LetRecFunNo.thy
--- a/Nominal/Ex/LetRecFunNo.thy	Sat May 12 21:39:09 2012 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,299 +0,0 @@
-theory Let
-imports "../Nominal2"
-begin
-
-atom_decl name
-
-nominal_datatype trm =
-  Var "name"
-| App "trm" "trm"
-| Let as::"assn" t::"trm"   binds "bn as" in as t
-and assn =
-  ANil
-| ACons "name" "trm" "assn"
-binder
-  bn
-where
-  "bn ANil = []"
-| "bn (ACons x t as) = (atom x) # (bn as)"
-
-nominal_primrec substrec where
-  "substrec fa fl fd y z (Var x) = (if (y = x) then z else (Var x))"
-| "substrec fa fl fd y z (App l r) = fa l r"
-| "(set (bn as) \<sharp>* (Let as t, y, z) \<and> (\<forall>bs s. set (bn bs) \<sharp>* (Let bs s, y, z) \<longrightarrow> Let as t = Let bs s \<longrightarrow> fl as t = fl bs s)) \<Longrightarrow>
-   substrec fa fl fd y z (Let as t) = fl as t"
-| "(set (bn as) \<sharp>* (Let as t, y, z) \<and> \<not>(\<forall>bs s. set (bn bs) \<sharp>* (Let bs s, y, z) \<longrightarrow> Let as t = Let bs s \<longrightarrow> fl as t = fl bs s)) \<Longrightarrow>
-   substrec fa fl fd y z (Let as t) = fd"
-  unfolding eqvt_def substrec_graph_def
-  apply (rule, perm_simp, rule, rule)
-  apply (case_tac x)
-  apply (rule_tac y="f" and c="(f, d, e)" in trm_assn.strong_exhaust(1))
-  apply metis
-  apply metis
-  apply (thin_tac "\<And>fa fl fd y z xa. x = (fa, fl, fd, y, z, Var xa) \<Longrightarrow> P")
-  apply (thin_tac "\<And>fa fl fd y z l r. x = (fa, fl, fd, y, z, App l r) \<Longrightarrow> P")
-  apply (drule_tac x="assn" in meta_spec)+
-  apply (drule_tac x="trm" in meta_spec)+
-  apply (drule_tac x="d" in meta_spec)+
-  apply (drule_tac x="e" in meta_spec)+
-  apply (drule_tac x="b" in meta_spec)+
-  apply (drule_tac x="a" in meta_spec)+
-  apply (drule_tac x="c" in meta_spec)+
-  apply (case_tac "(\<forall>bs s.
-             set (bn bs) \<sharp>* (Let bs s, d, e) \<longrightarrow>
-             Let.Let assn trm = Let.Let bs s \<longrightarrow> b assn trm = b bs s)")
-  apply simp
-  apply (thin_tac "set (bn assn) \<sharp>* (Let assn trm, d, e) \<and>
-         (\<forall>bs s.
-             set (bn bs) \<sharp>* (Let bs s, d, e) \<longrightarrow>
-             Let.Let assn trm = Let.Let bs s \<longrightarrow> b assn trm = b bs s) \<Longrightarrow>
-         x = (a, b, c, d, e, Let.Let assn trm) \<Longrightarrow> P")
-  apply simp
-  apply simp_all
-  apply clarify
-  apply metis
-  done
-termination (eqvt) by lexicographic_order
-
-nominal_primrec substarec :: "(name \<Rightarrow> trm \<Rightarrow> assn \<Rightarrow> assn) \<Rightarrow> assn \<Rightarrow> assn" where
-  "substarec fac ANil = ANil"
-| "substarec fac (ACons x t as) = fac x t as"
-  unfolding eqvt_def substarec_graph_def
-  apply (rule, perm_simp, rule, rule)
-  apply (case_tac x)
-  apply (rule_tac y="b" in trm_assn.exhaust(2))
-  apply auto
-  done
-termination (eqvt) by lexicographic_order
-
-lemma [fundef_cong]:
- "(\<And>t1 t2. t = App t1 t2 \<Longrightarrow> fa t1 t2 = fa' t1 t2) \<Longrightarrow>
-  (\<And>as s. t = Let as s \<Longrightarrow> fl as s = fl' as s) \<Longrightarrow>
-  substrec fa fl fd y z t = substrec fa' fl' fd y z t"
-  apply (rule_tac y="t" and c="(t, y, z)" in trm_assn.strong_exhaust(1))
-  apply auto
-  apply (case_tac "(\<forall>bs s. set (bn bs) \<sharp>* (Let bs s, y, z) \<longrightarrow> Let assn trm = Let bs s \<longrightarrow> fl assn trm = fl bs s)")
-  apply (subst substrec.simps(3)) apply simp
-  apply (subst substrec.simps(3)) apply simp
-  apply metis
-  apply (subst substrec.simps(4)) apply simp
-  apply (subst substrec.simps(4)) apply simp_all
-  done
-
-lemma [fundef_cong]:
- "(\<And>x s as. t = ACons x s as \<Longrightarrow> fac x s as = fac' x s as) \<Longrightarrow>
-  substarec fac t = substarec fac' t"
-  by (rule_tac y="t" in trm_assn.exhaust(2)) simp_all
-
-function
-    subst  :: "name \<Rightarrow> trm \<Rightarrow> trm \<Rightarrow> trm"
-and substa :: "name \<Rightarrow> trm \<Rightarrow> assn \<Rightarrow> assn"
-where
-  [simp del]: "subst y z t = substrec
-     (\<lambda>l r. App (subst y z l) (subst y z r))
-     (\<lambda>as t. Let (substa y z as) (subst y z t))
-     (Let (ACons y (Var y) ANil) (Var y)) y z t"
-| [simp del]: "substa y z t = substarec
-     (\<lambda>x t as. ACons x (subst y z t) (substa y z as)) t"
-  by pat_completeness auto
-
-termination by lexicographic_order
-
-lemma testl:
-  assumes a: "\<exists>y. f x = Inl y"
-  shows "(p \<bullet> (Sum_Type.Projl (f x))) = Sum_Type.Projl ((p \<bullet> f) (p \<bullet> x))"
-using a
-apply clarify
-apply(frule_tac p="p" in permute_boolI)
-apply(simp (no_asm_use) only: eqvts)
-apply(subst (asm) permute_fun_app_eq)
-back
-apply(simp)
-done
-
-lemma testr:
-  assumes a: "\<exists>y. f x = Inr y"
-  shows "(p \<bullet> (Sum_Type.Projr (f x))) = Sum_Type.Projr ((p \<bullet> f) (p \<bullet> x))"
-using a
-apply clarify
-apply(frule_tac p="p" in permute_boolI)
-apply(simp (no_asm_use) only: eqvts)
-apply(subst (asm) permute_fun_app_eq)
-back
-apply(simp)
-done
-
-lemma permute_move: "p \<bullet> x = y \<longleftrightarrow> x = -p \<bullet> y"
-  by (metis eqvt_bound unpermute_def)
-
-lemma "subst_substa_graph x t \<Longrightarrow> subst_substa_graph (p \<bullet> x) (p \<bullet> t)"
-proof (induct arbitrary: p rule: subst_substa_graph.induct)
-fix f y z t p
-assume a: "\<And>t1 t2 p. t = App t1 t2 \<Longrightarrow> subst_substa_graph (p \<bullet> Inl (y, z, t1)) (p \<bullet> f (Inl (y, z, t1)))"
-   and b: "\<And>t1 t2 p. t = App t1 t2 \<Longrightarrow> subst_substa_graph (p \<bullet> Inl (y, z, t2)) (p \<bullet> f (Inl (y, z, t2)))"
-   and c: "\<And>as s p. t = Let.Let as s \<Longrightarrow> subst_substa_graph (p \<bullet> Inr (y, z, as)) (p \<bullet> f (Inr (y, z, as)))"
-   and d: "\<And>as s p. t = Let.Let as s \<Longrightarrow> subst_substa_graph (p \<bullet> Inl (y, z, s)) (p \<bullet> f (Inl (y, z, s)))"
-   then show "subst_substa_graph (p \<bullet> Inl (y, z, t))
-           (p \<bullet> Inl (substrec
-                      (\<lambda>l r. App (Sum_Type.Projl (f (Inl (y, z, l))))
-                              (Sum_Type.Projl (f (Inl (y, z, r)))))
-                      (\<lambda>as t. Let.Let (Sum_Type.Projr (f (Inr (y, z, as))))
-                               (Sum_Type.Projl (f (Inl (y, z, t)))))
-                      (Let.Let (ACons y (Var y) ANil) (Var y)) y z t))"
-     proof (rule_tac y="t" and c="(t, y, z)" in trm_assn.strong_exhaust(1))
-       fix name
-       assume "t = Var name"
-       then show ?thesis
-         apply (simp add: eqvts split del: if_splits)
-         apply (simp only:  trm_assn.perm_simps)
-         apply (rule subst_substa_graph.intros(1)[of "Var (p \<bullet> name)" "p \<bullet> y" "p \<bullet> z", simplified])
-         by simp_all
-     next
-       fix trm1 trm2
-       assume e: "t = App trm1 trm2"
-       then show ?thesis
-         apply (simp add: eqvts)
-         apply (subst testl) back
-         apply (rule subst_substa_graph.cases[OF a[OF e, of 0, simplified]])
-         apply metis apply simp
-         apply (subst testl) back
-         apply (rule subst_substa_graph.cases[OF b[OF e, of 0, simplified]])
-         apply metis apply (simp add: eqvts)
-         apply (simp only: Inl_eqvt) apply simp
-         apply (rule subst_substa_graph.intros(1)[of "App (p \<bullet> trm1) (p \<bullet> trm2)" "p \<bullet> y" "p \<bullet> z", simplified])
-         apply simp_all apply clarify
-         using a[OF e, simplified Inl_eqvt, simplified]
-         apply (metis (lifting) Inl_eqvt permute_fun_app_eq permute_prod.simps)
-         apply clarify
-         using b[OF e, simplified Inl_eqvt, simplified]
-         by (metis (lifting) Inl_eqvt permute_fun_app_eq permute_prod.simps)
-     next
-       fix assn trm
-       assume e: "t = Let.Let assn trm" and f: "set (bn assn) \<sharp>* (t, y, z)"
-       then show ?thesis
-         apply (simp add: eqvts)
-         apply (simp only: permute_fun_def)
-         apply (simp only: eqvts permute_minus_cancel)
-         apply (case_tac "(\<forall>bs s. set (bn bs) \<sharp>* (Let.Let bs s, p \<bullet> y, p \<bullet> z) \<longrightarrow>
-                 Let.Let (p \<bullet> assn) (p \<bullet> trm) = Let.Let bs s \<longrightarrow>
-                 Let.Let (p \<bullet> Sum_Type.Projr (f (Inr (y, z, - p \<bullet> p \<bullet> assn))))
-                  (p \<bullet> Sum_Type.Projl (f (Inl (y, z, - p \<bullet> p \<bullet> trm)))) =
-                 Let.Let (p \<bullet> Sum_Type.Projr (f (Inr (y, z, - p \<bullet> bs))))
-                  (p \<bullet> Sum_Type.Projl (f (Inl (y, z, - p \<bullet> s)))))")
-         prefer 2
-         apply (subst substrec.simps(4))
-         apply rule
-         apply (simp add: fresh_star_Pair)
-         apply (intro conjI)
-         apply (metis fresh_star_permute_iff set_eqvt trm_assn.fv_bn_eqvt(4) trm_assn.perm_simps(3))
-         apply (metis (lifting) fresh_star_permute_iff set_eqvt trm_assn.fv_bn_eqvt(4))
-         apply (metis (lifting) fresh_star_permute_iff set_eqvt trm_assn.fv_bn_eqvt(4))
-         apply assumption
-         prefer 2
-         apply (subst substrec.simps(3))
-         apply rule
-         apply (simp add: fresh_star_Pair)
-         apply (intro conjI)
-         apply (metis fresh_star_permute_iff set_eqvt trm_assn.fv_bn_eqvt(4) trm_assn.perm_simps(3))
-         apply (metis (lifting) fresh_star_permute_iff set_eqvt trm_assn.fv_bn_eqvt(4))
-         apply (metis (lifting) fresh_star_permute_iff set_eqvt trm_assn.fv_bn_eqvt(4))
-         apply assumption
-(*       The following subgoal is motivated by:
-   thm subst_substa_graph.intros(1)[of "Let (p \<bullet> assn) (p \<bullet> trm)" "p \<bullet> y" "p \<bullet> z" "(p \<bullet> f)", simplified]*)
-         apply (subgoal_tac "subst_substa_graph (Inl (p \<bullet> y, p \<bullet> z, Let.Let (p \<bullet> assn) (p \<bullet> trm)))
-           (Inl (substrec
-           (\<lambda>l r. App (Sum_Type.Projl ((p \<bullet> f) (Inl (p \<bullet> y, p \<bullet> z, l))))
-                   (Sum_Type.Projl ((p \<bullet> f) (Inl (p \<bullet> y, p \<bullet> z, r)))))
-           (\<lambda>as t. Let.Let (Sum_Type.Projr ((p \<bullet> f) (Inr (p \<bullet> y, p \<bullet> z, as))))
-                    (Sum_Type.Projl ((p \<bullet> f) (Inl (p \<bullet> y, p \<bullet> z, t)))))
-           (Let.Let (ACons (p \<bullet> y) (Var (p \<bullet> y)) ANil) (Var (p \<bullet> y))) (p \<bullet> y) (p \<bullet> z)
-           (Let.Let (p \<bullet> assn) (p \<bullet> trm))))")
-         apply (subst (asm) substrec.simps(3))
-         apply rule
-         apply (simp add: fresh_star_Pair)
-         apply (intro conjI)
-         apply (metis fresh_star_permute_iff set_eqvt trm_assn.fv_bn_eqvt(4) trm_assn.perm_simps(3))
-         apply (metis (lifting) fresh_star_permute_iff set_eqvt trm_assn.fv_bn_eqvt(4))
-         apply (metis (lifting) fresh_star_permute_iff set_eqvt trm_assn.fv_bn_eqvt(4))
-         (* We don't have equivariance of Projl/Projr at the arbitrary 'bs' point *)
-         defer
-         apply (subst testr) back
-         apply (rule subst_substa_graph.cases[OF c[OF e, of 0, simplified]])
-         apply simp apply simp
-         apply (subst testl) back
-         apply (rule subst_substa_graph.cases[OF d[OF e, of 0, simplified]])
-         apply simp apply simp apply simp
-         apply (rule subst_substa_graph.intros(1)[of "Let (p \<bullet> assn) (p \<bullet> trm)" "p \<bullet> y" "p \<bullet> z" "(p \<bullet> f)", simplified])
-         apply simp apply simp (* These two should follow by d for arbitrary 'as' point *)
-         defer defer
-         sorry
-     qed
-   next
-     fix f y z t p
-     show "subst_substa_graph (p \<bullet> Inr (y, z, t)) (p \<bullet> Inr (substarec (\<lambda>x t as. ACons
-       x (Sum_Type.Projl (f (Inl (y, z, t)))) (Sum_Type.Projr (f (Inr (y, z, as))))) t))"
-       sorry
-   qed
-
-(* Will follow from above and accp *)
-lemma [eqvt]:
-  "p \<bullet> (subst y z t) = subst (p \<bullet> y) (p \<bullet> z) (p \<bullet> t)"
-  "p \<bullet> (substa y z t2) = substa (p \<bullet> y) (p \<bullet> z) (p \<bullet> t2)"
-  sorry
-
-lemma substa_simps[simp]:
-  "substa y z ANil = ANil"
-  "substa y z (ACons x t as) = ACons x (subst y z t) (substa y z as)"
-  apply (subst substa.simps) apply (subst substarec.simps) apply rule
-  apply (subst substa.simps) apply (subst substarec.simps) apply rule
-  done
-
-lemma bn_substa: "bn (substa y z t) = bn t"
-  by (induct t rule: trm_assn.inducts(2)) (simp_all add: trm_assn.bn_defs)
-
-lemma fresh_fun_eqvt_app3:
-  assumes e: "eqvt f"
-  shows "\<lbrakk>a \<sharp> x; a \<sharp> y; a \<sharp> z\<rbrakk> \<Longrightarrow> a \<sharp> f x y z"
-  using fresh_fun_eqvt_app[OF e] fresh_fun_app by (metis (lifting, full_types))
-
-lemma
-  "subst y z (Var x) = (if (y = x) then z else (Var x))"
-  "subst y z (App l r) = App (subst y z l) (subst y z r)"
-  "set (bn as) \<sharp>* (Let as t, y, z) \<Longrightarrow> subst y z (Let as t) = Let (substa y z as) (subst y z t)"
-  apply (subst subst.simps) apply (subst substrec.simps) apply rule
-  apply (subst subst.simps) apply (subst substrec.simps) apply rule
-  apply (subst subst.simps) apply (subst substrec.simps) apply auto
-  apply (subst (asm) Abs_eq_iff2)
-  apply clarify
-  apply (simp add: alphas bn_substa)
-  apply (rule_tac s="p \<bullet> ([bn as]lst. (substa y z as, subst y z t))" in trans)
-  apply (rule sym)
-  defer
-  apply (simp add: eqvts)
-  apply (subgoal_tac "supp p \<sharp>* y")
-  apply (subgoal_tac "supp p \<sharp>* z")
-  apply (simp add: perm_supp_eq)
-  apply (simp add: fresh_Pair fresh_star_def)
-  apply blast
-  apply (simp add: fresh_Pair fresh_star_def)
-  apply blast
-  apply (rule perm_supp_eq)
-  apply (simp add: fresh_star_Pair)
-  apply (simp add: fresh_star_def Abs_fresh_iff)
-  apply (auto)
-  apply (simp add: bn_substa fresh_Pair)
-  apply (rule)
-  apply (rule fresh_fun_eqvt_app3[of substa])
-  apply (simp add: eqvt_def eqvts_raw)
-  apply (metis (lifting) Diff_partition Un_iff)
-  apply (metis (lifting) Diff_partition Un_iff)
-  apply (simp add: fresh_def trm_assn.supp)
-  apply (metis (lifting) DiffI UnI1 supp_Pair)
-  apply (rule fresh_fun_eqvt_app3[of subst])
-  apply (simp add: eqvt_def eqvts_raw)
-  apply (metis (lifting) Diff_partition Un_iff)
-  apply (metis (lifting) Diff_partition Un_iff)
-  apply (simp add: fresh_def trm_assn.supp)
-  by (metis Diff_iff Un_iff supp_Pair)
-
-end
diff -r b6873d123f9b -r 89715c48f728 Nominal/Ex/Let_ExhaustIssue.thy
--- a/Nominal/Ex/Let_ExhaustIssue.thy	Sat May 12 21:39:09 2012 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,130 +0,0 @@
-theory Let
-imports "../Nominal2" 
-begin
-
-
-atom_decl name
-
-nominal_datatype trm =
-  Var "name"
-| App "trm" "trm"
-| Lam x::"name" t::"trm"  binds  x in t
-| Let as::"assn" t::"trm"   binds "bn as" in t
-and assn =
-  ANil
-| ACons "name" "trm" "assn"
-binder
-  bn
-where
-  "bn ANil = []"
-| "bn (ACons x t as) = (atom x) # (bn as)"
-
-lemma alpha_bn_inducts_raw:
-  "\<lbrakk>alpha_bn_raw a b; P3 ANil_raw ANil_raw;
- \<And>trm_raw trm_rawa assn_raw assn_rawa name namea.
-    \<lbrakk>alpha_trm_raw trm_raw trm_rawa; alpha_bn_raw assn_raw assn_rawa;
-     P3 assn_raw assn_rawa\<rbrakk>
-    \<Longrightarrow> P3 (ACons_raw name trm_raw assn_raw)
-        (ACons_raw namea trm_rawa assn_rawa)\<rbrakk> \<Longrightarrow> P3 a b"
-  by (erule alpha_trm_raw_alpha_assn_raw_alpha_bn_raw.inducts(3)[of _ _ "\<lambda>x y. True" _ "\<lambda>x y. True", simplified]) auto
-
-lemmas alpha_bn_inducts = alpha_bn_inducts_raw[quot_lifted]
-
-lemma alpha_bn_refl: "alpha_bn x x"
-  by (induct x rule: trm_assn.inducts(2))
-     (rule TrueI, auto simp add: trm_assn.eq_iff)
-
-lemma max_eqvt[eqvt]: "p \<bullet> (max (a :: _ :: pure) b) = max (p \<bullet> a) (p \<bullet> b)"
-  by (simp add: permute_pure)
-
-lemma what_we_would_like:
-  assumes a: "alpha_bn as asa"
-  shows "\<forall>p. set (bn as) \<sharp>* fv_bn as \<and> set (bn asa) \<sharp>* fv_bn asa \<and>
-   p \<bullet> bn as = bn asa \<and> supp p \<subseteq> set (bn as) \<union> set (bn asa) \<longrightarrow> p \<bullet> as = asa"
-  apply (rule alpha_bn_inducts[OF a])
-  apply
- (simp_all add: trm_assn.bn_defs trm_assn.perm_bn_simps trm_assn.supp)
- apply clarify
- apply simp
- apply (simp add: atom_eqvt)
- apply (case_tac "name = namea")
- sorry
-
-lemma Abs_lst_fcb2:
-  fixes as bs :: "'a :: fs"
-    and x y :: "'b :: fs"
-    and c::"'c::fs"
-  assumes eq: "[ba as]lst. x = [ba bs]lst. y"
-  and fcb1: "set (ba as) \<sharp>* f as x c"
-  and fresh1: "set (ba as) \<sharp>* c"
-  and fresh2: "set (ba bs) \<sharp>* c"
-  and perm1: "\<And>p. supp p \<sharp>* c \<Longrightarrow> p \<bullet> (f as x c) = f (p \<bullet> as) (p \<bullet> x) c"
-  and perm2: "\<And>p. supp p \<sharp>* c \<Longrightarrow> p \<bullet> (f bs y c) = f (p \<bullet> bs) (p \<bullet> y) c"
-  and ba_inj: "\<And>q r. q \<bullet> ba as = r \<bullet> ba bs \<Longrightarrow> q \<bullet> as = r \<bullet> bs"
-  shows "f as x c = f bs y c"
-sorry
-
-nominal_primrec
-    height_trm :: "trm \<Rightarrow> nat"
-and height_assn :: "assn \<Rightarrow> nat"
-where
-  "height_trm (Var x) = 1"
-| "height_trm (App l r) = max (height_trm l) (height_trm r)"
-| "height_trm (Lam v b) = 1 + (height_trm b)"
-| "set (bn as) \<sharp>* fv_bn as \<Longrightarrow> height_trm (Let as b) = max (height_assn as) (height_trm b)"
-| "height_assn ANil = 0"
-| "height_assn (ACons v t as) = max (height_trm t) (height_assn as)"
-  apply (simp only: eqvt_def height_trm_height_assn_graph_def)
-  apply (rule, perm_simp, rule, rule TrueI)
-  apply (case_tac x)
-  apply (rule_tac y="a" in trm_assn.strong_exhaust(1))
-  apply (auto)[4]
-  apply (drule_tac x="assn" in meta_spec)
-  apply (drule_tac x="trm" in meta_spec)
-  apply (simp add: alpha_bn_refl)
---"HERE"
-  defer
-  apply (case_tac b rule: trm_assn.exhaust(2))
-  apply (auto)[2]
-  apply(simp_all)
-  apply (erule_tac c="()" in Abs_lst_fcb2)
-  apply (simp_all add: pure_fresh fresh_star_def)[3]
-  apply (simp add: eqvt_at_def)
-  apply (simp add: eqvt_at_def)
-  apply assumption
-  apply(erule conjE)
-  apply (simp add: meta_eq_to_obj_eq[OF height_trm_def, symmetric, unfolded fun_eq_iff])
-  apply (simp add: meta_eq_to_obj_eq[OF height_assn_def, symmetric, unfolded fun_eq_iff])
-  apply (subgoal_tac "eqvt_at height_assn as")
-  apply (subgoal_tac "eqvt_at height_assn asa")
-  apply (subgoal_tac "eqvt_at height_trm b")
-  apply (subgoal_tac "eqvt_at height_trm ba")
-  apply (thin_tac "eqvt_at height_trm_height_assn_sumC (Inr as)")
-  apply (thin_tac "eqvt_at height_trm_height_assn_sumC (Inr asa)")
-  apply (thin_tac "eqvt_at height_trm_height_assn_sumC (Inl b)")
-  apply (thin_tac "eqvt_at height_trm_height_assn_sumC (Inl ba)")
-  defer
-  apply (simp add: eqvt_at_def height_trm_def)
-  apply (simp add: eqvt_at_def height_trm_def)
-  apply (simp add: eqvt_at_def height_assn_def)
-  apply (simp add: eqvt_at_def height_assn_def)
-  defer
-  apply (subgoal_tac "height_assn as = height_assn asa")
-  apply (subgoal_tac "height_trm b = height_trm ba")
-  apply simp
-  apply (erule_tac c="()" in Abs_lst_fcb2)
-  apply (simp_all add: pure_fresh fresh_star_def)[3]
-  apply (simp_all add: eqvt_at_def)[2]
-  apply assumption
-  apply (erule_tac Abs_lst_fcb)
-  apply (simp_all add: pure_fresh fresh_star_def)[2]
-  apply (drule what_we_would_like)
-  apply (drule_tac x="p" in spec)
-  apply simp
-  apply (simp add: eqvt_at_def)
-  oops
-
-end
-
-
-
diff -r b6873d123f9b -r 89715c48f728 Nominal/Ex/NBE.thy
--- a/Nominal/Ex/NBE.thy	Sat May 12 21:39:09 2012 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,546 +0,0 @@
-theory Lambda
-imports 
-  "../Nominal2"
-begin
-
-
-atom_decl name
-
-nominal_datatype lam =
-  Var "name"
-| App "lam" "lam"
-| Lam x::"name" l::"lam"  binds x in l ("Lam [_]. _" [100, 100] 100)
-
-nominal_datatype sem =
-  L e::"env" x::"name" l::"lam" binds x "bn e" in l
-| N "neu"
-and neu = 
-  V "name"
-| A "neu" "sem"
-and env =
-  ENil
-| ECons "env" "name" "sem"
-binder
-  bn
-where
-  "bn ENil = []"
-| "bn (ECons env x v) = (atom x) # (bn env)"
-
-thm sem_neu_env.supp
-
-lemma [simp]:
-  shows "finite (fv_bn env)"
-apply(induct env rule: sem_neu_env.inducts(3))
-apply(rule TrueI)+
-apply(auto simp add: sem_neu_env.supp finite_supp)
-done
-
-lemma test1:
-  shows "supp p \<sharp>* (fv_bn env) \<Longrightarrow> (p \<bullet> env) = permute_bn p env"
-apply(induct env rule: sem_neu_env.inducts(3))
-apply(rule TrueI)+
-apply(auto simp add: sem_neu_env.perm_bn_simps sem_neu_env.supp)
-apply(drule meta_mp)
-apply(drule fresh_star_supp_conv)
-apply(subst (asm) supp_finite_atom_set)
-apply(simp add: finite_supp)
-apply(simp add: fresh_star_Un)
-apply(rule fresh_star_supp_conv)
-apply(subst supp_finite_atom_set)
-apply(simp)
-apply(simp)
-apply(simp)
-apply(rule perm_supp_eq)
-apply(drule fresh_star_supp_conv)
-apply(subst (asm) supp_finite_atom_set)
-apply(simp add: finite_supp)
-apply(simp add: fresh_star_Un)
-apply(rule fresh_star_supp_conv)
-apply(simp)
-done
-
-thm alpha_sem_raw_alpha_neu_raw_alpha_env_raw_alpha_bn_raw.inducts(4)[no_vars]
-
-lemma alpha_bn_inducts_raw[consumes 1]:
-  "\<lbrakk>alpha_bn_raw x7 x8;
-  P4 ENil_raw ENil_raw;
- \<And>env_raw env_rawa sem_raw sem_rawa name namea.
-    \<lbrakk>alpha_bn_raw env_raw env_rawa; P4 env_raw env_rawa; alpha_sem_raw sem_raw sem_rawa\<rbrakk>
-    \<Longrightarrow> P4 (ECons_raw env_raw name sem_raw) (ECons_raw env_rawa namea sem_rawa)\<rbrakk>
-\<Longrightarrow> P4 x7 x8"
-apply(induct rule: alpha_sem_raw_alpha_neu_raw_alpha_env_raw_alpha_bn_raw.inducts(4))
-apply(rule TrueI)+
-apply(auto)
-done
-
-lemmas alpha_bn_inducts[consumes 1] = alpha_bn_inducts_raw[quot_lifted]
-
-lemma test2:
-  shows "alpha_bn env1 env2 \<Longrightarrow> p \<bullet> (bn env1) = q \<bullet> (bn env2) \<Longrightarrow> permute_bn p env1 = permute_bn q env2"
-apply(induct rule: alpha_bn_inducts)
-apply(auto simp add: sem_neu_env.perm_bn_simps sem_neu_env.bn_defs)
-apply(simp add: atom_eqvt)
-done
-
-lemma fresh_star_Union:
-  assumes "as \<subseteq> bs" "bs \<sharp>* x"
-  shows "as \<sharp>* x"
-using assms by (auto simp add: fresh_star_def)
-  
-
-nominal_primrec  (invariant "\<lambda>x y. case x of Inl (x1, y1) \<Rightarrow> 
-  supp y \<subseteq> (supp y1 - set (bn x1)) \<union> (fv_bn x1) | Inr (x2, y2) \<Rightarrow> supp y \<subseteq> supp x2 \<union> supp y2")
-  evals :: "env \<Rightarrow> lam \<Rightarrow> sem" and
-  evals_aux :: "sem \<Rightarrow> sem \<Rightarrow> sem"
-where
-  "evals ENil (Var x) = N (V x)"
-| "evals (ECons tail y v) (Var x) = (if x = y then v else evals tail (Var x))" 
-| "atom x \<sharp> env \<Longrightarrow> evals env (Lam [x]. t) = L env x t"
-| "evals env (App t1 t2) = evals_aux (evals env t1) (evals env t2)"
-| "set (atom x # bn env) \<sharp>* (fv_bn env, t') \<Longrightarrow> evals_aux (L env x t) t' = evals (ECons env x t') t"
-| "evals_aux (N n) t' = N (A n t')"
-apply(simp add: eqvt_def  evals_evals_aux_graph_def)
-apply(perm_simp)
-apply(simp)
-apply(erule evals_evals_aux_graph.induct)
-apply(simp add: sem_neu_env.supp lam.supp sem_neu_env.bn_defs)
-apply(simp add: sem_neu_env.supp lam.supp sem_neu_env.bn_defs)
-apply(rule conjI)
-apply(rule impI)
-apply(blast)
-apply(rule impI)
-apply(simp add: supp_at_base)
-apply(blast)
-apply(simp add: sem_neu_env.supp lam.supp sem_neu_env.bn_defs)
-apply(blast)
-apply(simp add: sem_neu_env.supp lam.supp sem_neu_env.bn_defs)
-apply(blast)
-apply(simp add: sem_neu_env.supp lam.supp sem_neu_env.bn_defs)
-apply(blast)
-apply(simp add: sem_neu_env.supp lam.supp sem_neu_env.bn_defs)
---"completeness"
-apply(case_tac x)
-apply(simp)
-apply(case_tac a)
-apply(simp)
-apply(case_tac aa rule: sem_neu_env.exhaust(3))
-apply(simp add: sem_neu_env.fresh)
-apply(case_tac b rule: lam.exhaust)
-apply(metis)+
-apply(case_tac aa rule: sem_neu_env.exhaust(3))
-apply(rule_tac y="b" and c="env" in lam.strong_exhaust)
-apply(metis)+
-apply(simp add: fresh_star_def)
-apply(simp)
-apply(rule_tac y="b" and c="ECons env name sem" in lam.strong_exhaust)
-apply(metis)+
-apply(simp add: fresh_star_def)
-apply(simp)
-apply(case_tac b)
-apply(simp)
-apply(rule_tac y="a" and c="(a, ba)" in sem_neu_env.strong_exhaust(1))
-apply(simp)
-apply(rotate_tac 4)
-apply(drule_tac x="name" in meta_spec)
-apply(drule_tac x="env" in meta_spec)
-apply(drule_tac x="ba" in meta_spec)
-apply(drule_tac x="lam" in meta_spec)
-apply(simp add:  sem_neu_env.alpha_refl)
-apply(rotate_tac 9)
-apply(drule_tac meta_mp)
-apply(simp (no_asm_use) add: fresh_star_def sem_neu_env.fresh fresh_Pair)
-apply(simp)
-apply(subst fresh_finite_atom_set)
-defer
-apply(simp)
-apply(subst fresh_finite_atom_set)
-defer
-apply(simp)
-apply(metis)+
---"compatibility"
-apply(all_trivials)
-apply(simp)
-apply(simp)
-defer
-apply(simp)
-apply(simp)
-apply (simp add: meta_eq_to_obj_eq[OF evals_def, symmetric, unfolded fun_eq_iff])
-apply (subgoal_tac "eqvt_at (\<lambda>(a, b). evals a b) (ECons env x t'a, t)")
-apply (subgoal_tac "eqvt_at (\<lambda>(a, b). evals a b) (ECons enva xa t'a, ta)")
-apply (thin_tac "eqvt_at evals_evals_aux_sumC (Inl (ECons env x t'a, t))")
-apply (thin_tac "eqvt_at evals_evals_aux_sumC (Inl (ECons enva xa t'a, ta))")
-apply(erule conjE)+
-defer
-apply (simp_all add: eqvt_at_def evals_def)[3]
-defer
-defer
-apply(simp add: sem_neu_env.alpha_refl)
-apply(erule conjE)+
-apply(erule_tac c="(env, enva)" in Abs_lst1_fcb2)
-apply(simp add: Abs_fresh_iff)
-apply(simp add: fresh_star_def)
-apply(perm_simp)
-apply(simp add: fresh_star_Pair perm_supp_eq)
-apply(perm_simp)
-apply(simp add: fresh_star_Pair perm_supp_eq)
-apply(simp add: sem_neu_env.bn_defs sem_neu_env.supp)
-using at_set_avoiding3
-apply -
-apply(drule_tac x="set (atom x # bn env)" in meta_spec)
-apply(drule_tac x="(fv_bn env, fv_bn enva, env, enva, x, xa, t, ta, t'a)" in meta_spec)
-apply(drule_tac x="[atom x # bn env]lst. t" in meta_spec)
-apply(simp (no_asm_use) add: finite_supp Abs_fresh_star_iff)
-apply(drule meta_mp)
-apply(simp add: supp_Pair finite_supp supp_finite_atom_set)
-apply(drule meta_mp)
-apply(simp add: fresh_star_def)
-apply(erule exE)
-apply(erule conjE)+
-apply(rule trans)
-apply(rule sym)
-apply(rule_tac p="p" in perm_supp_eq)
-apply(simp)
-apply(perm_simp)
-apply(simp add: fresh_star_Un fresh_star_insert)
-apply(rule conjI)
-apply(simp (no_asm_use) add: fresh_star_def fresh_Pair)
-apply(simp add: fresh_def)
-apply(simp add: supp_finite_atom_set)
-apply(blast)
-apply(rule conjI)
-apply(simp (no_asm_use) add: fresh_star_def fresh_Pair)
-apply(simp add: fresh_def)
-apply(simp add: supp_finite_atom_set)
-apply(blast)
-apply(rule conjI)
-apply(simp (no_asm_use) add: fresh_star_def fresh_Pair)
-apply(simp add: fresh_def)
-apply(simp add: supp_finite_atom_set)
-apply(blast)
-apply(simp (no_asm_use) add: fresh_star_def fresh_Pair)
-apply(simp add: fresh_def)
-apply(simp add: supp_finite_atom_set)
-apply(blast)
-apply(simp add: eqvt_at_def perm_supp_eq)
-apply(subst (3) perm_supp_eq)
-apply(simp)
-apply(simp add: fresh_star_def fresh_Pair)
-apply(auto)[1]
-apply(rotate_tac 6)
-apply(drule sym)
-apply(simp)
-apply(rotate_tac 11)
-apply(drule trans)
-apply(rule sym)
-apply(rule_tac p="p" in supp_perm_eq)
-apply(assumption)
-apply(rotate_tac 11)
-apply(rule sym)
-apply(simp add: atom_eqvt)
-apply(simp (no_asm_use) add: Abs_eq_iff2 alphas)
-apply(erule conjE | erule exE)+
-apply(rule trans)
-apply(rule sym)
-apply(rule_tac p="pa" in perm_supp_eq)
-apply(erule fresh_star_Union)
-apply(simp (no_asm_use) add: fresh_star_insert fresh_star_Un)
-apply(rule conjI)
-apply(perm_simp)
-apply(simp add: fresh_star_insert fresh_star_Un)
-apply(simp add: fresh_Pair)
-apply(simp add: fresh_def)
-apply(simp add: supp_finite_atom_set)
-apply(blast)
-apply(rule conjI)
-apply(perm_simp)
-apply(simp add: fresh_star_insert fresh_star_Un)
-apply(simp add: fresh_Pair)
-apply(simp add: fresh_def)
-apply(simp add: supp_finite_atom_set)
-apply(blast)
-apply(rule conjI)
-apply(perm_simp)
-defer
-apply(perm_simp)
-apply(simp add: fresh_star_insert fresh_star_Un)
-apply(simp add: fresh_star_Pair)
-apply(simp add: fresh_star_def fresh_def)
-apply(simp add: supp_finite_atom_set)
-apply(blast)
-apply(simp)
-apply(perm_simp)
-apply(subst (3) perm_supp_eq)
-apply(erule fresh_star_Union)
-apply(simp add: fresh_star_insert fresh_star_Un)
-apply(simp add: fresh_star_def fresh_Pair)
-apply(subgoal_tac "pa \<bullet> enva = p \<bullet> env")
-apply(simp)
-defer
-apply(simp (no_asm_use) add: fresh_star_insert fresh_star_Un)
-apply(simp (no_asm_use) add: fresh_star_def)
-apply(rule ballI)
-apply(subgoal_tac "a \<notin> supp ta - insert (atom xa) (set (bn enva)) \<union> (fv_bn enva \<union> supp t'a)")
-apply(simp only: fresh_def)
-apply(blast)
-apply(simp (no_asm_use))
-apply(rule conjI)
-apply(blast)
-apply(simp add: fresh_Pair)
-apply(simp add: fresh_star_def fresh_def)
-apply(simp add: supp_finite_atom_set)
-apply(subst test1)
-apply(erule fresh_star_Union)
-apply(simp add: fresh_star_insert fresh_star_Un)
-apply(simp add: fresh_star_def fresh_Pair)
-apply(subst test1)
-apply(simp)
-apply(simp add: fresh_star_insert fresh_star_Un)
-apply(simp add: fresh_star_def fresh_Pair)
-apply(rule sym)
-apply(erule test2)
-apply(perm_simp)
-apply(simp)
-done
-
-
-
-
-text {* can probably not proved by a trivial size argument *}
-termination (* apply(lexicographic_order) *)
-sorry
-
-lemma [eqvt]:
-  shows "(p \<bullet> evals env t) = evals (p \<bullet> env) (p \<bullet> t)"
-  and "(p \<bullet> evals_aux v s) = evals_aux (p \<bullet> v) (p \<bullet> s)"
-sorry
-
-(* fixme: should be a provided lemma *)
-lemma fv_bn_finite:
-  shows "finite (fv_bn env)"
-apply(induct env rule: sem_neu_env.inducts(3))
-apply(auto simp add: sem_neu_env.supp finite_supp)
-done
-
-lemma test:
-  fixes env::"env"
-  shows "supp (evals env t) \<subseteq> (supp t - set (bn env)) \<union> (fv_bn env)"
-  and "supp (evals_aux s v) \<subseteq> (supp s) \<union> (supp v)"
-apply(induct env t and s v rule: evals_evals_aux.induct)
-apply(simp add: sem_neu_env.supp lam.supp supp_Nil sem_neu_env.bn_defs)
-apply(simp add: sem_neu_env.supp lam.supp supp_Nil supp_Cons sem_neu_env.bn_defs)
-apply(rule conjI)
-apply(auto)[1]
-apply(rule impI)
-apply(simp)
-apply(simp add: supp_at_base)
-apply(blast)
-apply(simp)
-apply(subst sem_neu_env.supp)
-apply(simp add: sem_neu_env.supp lam.supp)
-apply(auto)[1]
-apply(simp add: lam.supp sem_neu_env.supp)
-apply(blast)
-apply(simp add: sem_neu_env.supp sem_neu_env.bn_defs)
-apply(blast)
-apply(simp add: sem_neu_env.supp)
-done
-
-
-nominal_primrec
-  reify :: "sem \<Rightarrow> lam" and
-  reifyn :: "neu \<Rightarrow> lam"
-where
-  "atom x \<sharp> (env, y, t) \<Longrightarrow> reify (L env y t) = Lam [x]. (reify (evals (ECons env y (N (V x))) t))"
-| "reify (N n) = reifyn n"
-| "reifyn (V x) = Var x"
-| "reifyn (A n d) = App (reifyn n) (reify d)"
-apply(subgoal_tac "\<And>p x y. reify_reifyn_graph x y \<Longrightarrow> reify_reifyn_graph (p \<bullet> x) (p \<bullet> y)")
-apply(simp add: eqvt_def)
-apply(simp add: permute_fun_def)
-apply(rule allI)
-apply(rule ext)
-apply(rule ext)
-apply(rule iffI)
-apply(drule_tac x="p" in meta_spec)
-apply(drule_tac x="- p \<bullet> x" in meta_spec)
-apply(drule_tac x="- p \<bullet> xa" in meta_spec)
-apply(simp add: permute_bool_def)
-apply(simp add: permute_bool_def)
-apply(erule reify_reifyn_graph.induct)
-apply(perm_simp)
-apply(rule reify_reifyn_graph.intros)
-apply(rule_tac p="-p" in permute_boolE)
-apply(perm_simp add: permute_minus_cancel)
-apply(simp)
-apply(simp)
-apply(perm_simp)
-apply(rule reify_reifyn_graph.intros)
-apply(simp)
-apply(perm_simp)
-apply(rule reify_reifyn_graph.intros)
-apply(perm_simp)
-apply(rule reify_reifyn_graph.intros)
-apply(simp)
-apply(simp)
-apply(rule TrueI)
---"completeness"
-apply(case_tac x)
-apply(simp)
-apply(case_tac a rule: sem_neu_env.exhaust(1))
-apply(subgoal_tac "\<exists>x::name. atom x \<sharp> (env, name, lam)")
-apply(metis)
-apply(rule obtain_fresh)
-apply(blast)
-apply(blast)
-apply(case_tac b rule: sem_neu_env.exhaust(2))
-apply(simp)
-apply(simp)
-apply(metis)
---"compatibility"
-apply(all_trivials)
-defer
-apply(simp)
-apply(simp)
-apply(simp)
-apply(erule conjE)
-apply (simp add: meta_eq_to_obj_eq[OF reify_def, symmetric, unfolded fun_eq_iff])
-apply (subgoal_tac "eqvt_at (\<lambda>t. reify t) (evals (ECons env y (N (V x))) t)")
-apply (subgoal_tac "eqvt_at (\<lambda>t. reify t) (evals (ECons enva ya (N (V xa))) ta)")
-apply (thin_tac "eqvt_at reify_reifyn_sumC (Inl (evals (ECons env y (N (V x))) t))")
-apply (thin_tac "eqvt_at reify_reifyn_sumC (Inl (evals (ECons enva ya (N (V xa))) ta))")
-defer
-apply (simp_all add: eqvt_at_def reify_def)[2]
-apply(subgoal_tac "\<exists>c::name. atom c \<sharp> (x, xa, env, enva, y, ya, t, ta)")
-prefer 2
-apply(rule obtain_fresh)
-apply(blast)
-apply(erule exE)
-apply(rule trans)
-apply(rule sym)
-apply(rule_tac a="x" and b="c" in flip_fresh_fresh)
-apply(simp add: Abs_fresh_iff)
-apply(simp add: Abs_fresh_iff fresh_Pair)
-apply(auto)[1]
-apply(rule fresh_eqvt_at)
-back
-apply(assumption)
-apply(simp add: finite_supp)
-apply(rule_tac S="supp (env, y, x, t)" in supports_fresh)
-apply(simp add: supports_def fresh_def[symmetric])
-apply(perm_simp)
-apply(simp add: swap_fresh_fresh fresh_Pair)
-apply(simp add: finite_supp)
-apply(simp add: fresh_def[symmetric])
-apply(simp add: eqvt_at_def)
-apply(simp add: eqvt_at_def[symmetric])
-apply(perm_simp)
-apply(simp add: flip_fresh_fresh)
-apply(rule sym)
-apply(rule trans)
-apply(rule sym)
-apply(rule_tac a="xa" and b="c" in flip_fresh_fresh)
-apply(simp add: Abs_fresh_iff)
-apply(simp add: Abs_fresh_iff fresh_Pair)
-apply(auto)[1]
-apply(rule fresh_eqvt_at)
-back
-apply(assumption)
-apply(simp add: finite_supp)
-apply(rule_tac S="supp (enva, ya, xa, ta)" in supports_fresh)
-apply(simp add: supports_def fresh_def[symmetric])
-apply(perm_simp)
-apply(simp add: swap_fresh_fresh fresh_Pair)
-apply(simp add: finite_supp)
-apply(simp add: fresh_def[symmetric])
-apply(simp add: eqvt_at_def)
-apply(simp add: eqvt_at_def[symmetric])
-apply(perm_simp)
-apply(simp add: flip_fresh_fresh)
-apply(simp (no_asm) add: Abs1_eq_iff)
-(* HERE *)
-thm at_set_avoiding3
-using at_set_avoiding3
-apply -
-apply(drule_tac x="set (atom y # bn env)" in meta_spec)
-apply(drule_tac x="(env, enva)" in meta_spec)
-apply(drule_tac x="[atom y # bn env]lst. t" in meta_spec)
-apply(simp (no_asm_use) add: finite_supp)
-apply(drule meta_mp)
-apply(rule Abs_fresh_star)
-apply(auto)[1]
-apply(erule exE)
-apply(erule conjE)+
-apply(drule_tac q="(x \<leftrightarrow> c)" in eqvt_at_perm)
-apply(perm_simp)
-apply(simp add: flip_fresh_fresh fresh_Pair)
-apply(drule_tac q="(xa \<leftrightarrow> c)" in eqvt_at_perm)
-apply(perm_simp)
-apply(simp add: flip_fresh_fresh fresh_Pair)
-apply(drule sym)
-(* HERE *)
-apply(rotate_tac 9)
-apply(drule sym)
-apply(rotate_tac 9)
-apply(drule trans)
-apply(rule sym)
-apply(rule_tac p="p" in supp_perm_eq)
-apply(assumption)
-apply(simp)
-apply(perm_simp)
-apply(simp (no_asm_use) add: Abs_eq_iff2 alphas)
-apply(erule conjE | erule exE)+
-apply(clarify)
-apply(rule trans)
-apply(rule sym)
-apply(rule_tac p="pa" in perm_supp_eq)
-defer
-apply(rule sym)
-apply(rule trans)
-apply(rule sym)
-apply(rule_tac p="p" in perm_supp_eq)
-defer
-apply(simp add: atom_eqvt)
-apply(drule_tac q="(x \<leftrightarrow> c)" in eqvt_at_perm)
-apply(perm_simp)
-apply(simp add: flip_fresh_fresh fresh_Pair)
-
-apply(rule sym)
-apply(erule_tac Abs_lst1_fcb2')
-apply(rule fresh_eqvt_at)
-back
-apply(drule_tac q="(c \<leftrightarrow> x)" in eqvt_at_perm)
-apply(perm_simp)
-apply(simp add: flip_fresh_fresh)
-apply(simp add: finite_supp)
-apply(rule supports_fresh)
-apply(rule_tac S="supp (enva, ya, xa, ta)" in supports_fresh)
-apply(simp add: supports_def fresh_def[symmetric])
-apply(perm_simp)
-apply(simp add: swap_fresh_fresh fresh_Pair)
-apply(simp add: finite_supp)
-apply(simp add: fresh_def[symmetric])
-apply(simp add: eqvt_at_def)
-apply(simp add: eqvt_at_def[symmetric])
-apply(perm_simp)
-apply(rule fresh_eqvt_at)
-back
-apply(drule_tac q="(c \<leftrightarrow> x)" in eqvt_at_perm)
-apply(perm_simp)
-apply(simp add: flip_fresh_fresh)
-apply(assumption)
-apply(simp add: finite_supp)
-sorry
-
-termination sorry
-
-definition
-  eval :: "lam \<Rightarrow> sem"
-where
-  "eval t = evals ENil t"
-
-definition
-  normalize :: "lam \<Rightarrow> lam"
-where
-  "normalize t = reify (eval t)"
-
-end
\ No newline at end of file
diff -r b6873d123f9b -r 89715c48f728 Nominal/Ex/PaperTest.thy
--- a/Nominal/Ex/PaperTest.thy	Sat May 12 21:39:09 2012 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,303 +0,0 @@
-theory PaperTest
-imports "../Nominal2"
-begin
-
-atom_decl name 
-
-datatype trm = 
-  Const "string"
-| Var "name"
-| App "trm" "trm"
-| Lam "name" "trm"  ("Lam [_]. _" [100, 100] 100)
-
-fun
-  subst :: "trm \<Rightarrow> name \<Rightarrow> name \<Rightarrow> trm"  ("_[_::=_]" [100,100,100] 100)
-where
-  "(Var x)[y::=p] = (if x=y then (App (App (Const ''unpermute'') (Var p)) (Var x)) else (Var x))"
-| "(App t\<^isub>1 t\<^isub>2)[y::=p] = App (t\<^isub>1[y::=p]) (t\<^isub>2[y::=p])"
-| "(Lam [x].t)[y::=p] = (if x=y then (Lam [x].t) else Lam [x].(t[y::=p]))"
-| "(Const n)[y::=p] = Const n"
-
-datatype utrm = 
-  UConst "string"
-| UnPermute "name" "name"
-| UVar "name"
-| UApp "utrm" "utrm"
-| ULam "name" "utrm"  ("ULam [_]. _" [100, 100] 100)
-
-fun
-  usubst :: "utrm \<Rightarrow> name \<Rightarrow> name \<Rightarrow> utrm"  ("_[_:::=_]" [100,100,100] 100)
-where
-  "(UVar x)[y:::=p] = (if x=y then UnPermute p x else (UVar x))"
-| "(UApp t\<^isub>1 t\<^isub>2)[y:::=p] = UApp (t\<^isub>1[y:::=p]) (t\<^isub>2[y:::=p])"
-| "(ULam [x].t)[y:::=p] = (if x=y then (ULam [x].t) else ULam [x].(t[y:::=p]))"
-| "(UConst n)[y:::=p] = UConst n"
-| "(UnPermute x q)[y:::=p] = UnPermute x q"
-
-function
-  ss :: "trm \<Rightarrow> nat"
-where
-  "ss (Var x) = 1"
-| "ss (Const s) = 1"
-| "ss (Lam [x].t) = 1 + ss t"
-| "ss (App (App (Const ''unpermute'') (Var p)) (Var x)) = 1"
-| "\<not>(\<exists>p x. t1 = App (Const ''unpermute'') (Var p) \<and> t2 = (Var x)) \<Longrightarrow> ss (App t1 t2) = 1 + ss t1 + ss t2"
-defer
-apply(simp_all)
-apply(auto)[1]
-apply(case_tac x)
-apply(simp_all)
-apply(auto)
-apply(blast)
-done
-
-termination
-  apply(relation "measure (\<lambda>t. size t)")
-  apply(simp_all)
-  done
-
-fun
-  uss :: "utrm \<Rightarrow> nat"
-where
-  "uss (UVar x) = 1"
-| "uss (UConst s) = 1"
-| "uss (ULam [x].t) = 1 + uss t"
-| "uss (UnPermute x y) = 1"
-| "uss (UApp t1 t2) = 1 + uss t1 + uss t2"
-
-lemma trm_uss:
-  shows "uss (t[x:::=p]) = uss t"
-apply(induct rule: uss.induct)
-apply(simp_all)
-done
-
-inductive
-  ufree :: "utrm \<Rightarrow> bool"
-where
-  "ufree (UVar x)"
-| "s \<noteq> ''unpermute'' \<Longrightarrow> ufree (UConst s)"
-| "ufree t \<Longrightarrow> ufree (ULam [x].t)"
-| "ufree (UnPermute x y)"
-| "\<lbrakk>ufree t1; ufree t2\<rbrakk> \<Longrightarrow> ufree (UApp t1 t2)"
-
-fun
-  trans :: "utrm \<Rightarrow> trm" ("\<parallel>_\<parallel>" [100] 100)
-where
-  "\<parallel>(UVar x)\<parallel> = Var x"
-| "\<parallel>(UConst x)\<parallel> = Const x"
-| "\<parallel>(UnPermute p x)\<parallel> = (App (App (Const ''unpermute'') (Var p)) (Var x))"
-| "\<parallel>(ULam [x].t)\<parallel> = Lam [x].(\<parallel>t\<parallel>)"
-| "\<parallel>(UApp t1 t2)\<parallel> = App (\<parallel>t1\<parallel>) (\<parallel>t2\<parallel>)"
-
-function
-  utrans :: "trm \<Rightarrow> utrm" ("\<lparr>_\<rparr>" [90] 100)
-where
-  "\<lparr>Var x\<rparr> = UVar x"
-| "\<lparr>Const x\<rparr> = UConst x"
-| "\<lparr>Lam [x].t\<rparr> = ULam [x].\<lparr>t\<rparr>"
-| "\<lparr>App (App (Const ''unpermute'') (Var p)) (Var x)\<rparr> = UnPermute p x"
-| "\<not>(\<exists>p x. t1 = App (Const ''unpermute'') (Var p) \<and> t2 = (Var x)) \<Longrightarrow> \<lparr>App t1 t2\<rparr> = UApp (\<lparr>t1\<rparr>) (\<lparr>t2\<rparr>)"
-defer
-apply(simp_all)
-apply(auto)[1]
-apply(case_tac x)
-apply(simp_all)
-apply(auto)
-apply(blast)
-done
-
-termination
-  apply(relation "measure (\<lambda>t. size t)")
-  apply(simp_all)
-  done
-
-
-lemma elim1:
-  "ufree t \<Longrightarrow> \<parallel>t\<parallel> \<noteq>(Const ''unpermute'')"
-apply(erule ufree.induct)
-apply(auto)
-done
-
-lemma elim2:
-  "ufree t \<Longrightarrow> \<not>(\<exists>p. \<parallel>t\<parallel> = App (Const ''unpermute'') (Var p))"
-apply(erule ufree.induct)
-apply(auto dest: elim1)
-done
-
-lemma ss1:
-  "ufree t \<Longrightarrow> uss t = ss (\<parallel>t\<parallel>)"
-apply(erule ufree.induct)
-apply(simp_all)
-apply(subst ss.simps)
-apply(auto)
-apply(drule elim2)
-apply(auto)
-done
-
-lemma trans1:
-  shows "\<parallel>\<lparr>t\<rparr>\<parallel> = t"
-apply(induct t)
-apply(simp)
-apply(simp)
-prefer 2
-apply(simp)
-apply(case_tac "(\<exists>p x. t1 = App (Const ''unpermute'') (Var p) \<and> t2 = (Var x))")
-apply(erule exE)+
-apply(simp)
-apply(simp)
-done
-
-lemma trans_subst:
-  shows "\<lparr>t[x ::= p]\<rparr> = \<lparr>t\<rparr>[x :::= p]"
-apply(induct rule: subst.induct)
-apply(simp)
-defer
-apply(simp)
-apply(simp)
-apply(simp)
-apply(case_tac "(t1 = App (Const ''unpermute'') (Var p) \<and> t2 = (Var x))")
-apply(erule exE)+
-apply(simp only:)
-apply(subst utrans.simps)
-apply(subst usubst.simps)
-apply(case_tac "xa = x")
-apply(subst (asm) subst.simps)
-apply(simp only:)
-apply(subst (asm) utrans.simps)
-apply(simp only: usubst.simps)
-apply(simp)
-apply(auto)[1]
-apply(case_tac "pa = x")
-apply(simp)
-prefer 2
-apply(simp)
-apply(simp)
-done
-
-lemma 
-  "ss (t[x ::= p]) = ss t"
-apply(subst (2) trans1[symmetric])
-apply(subst ss1[symmetric])
-
-
-fun
-  fr :: "trm \<Rightarrow> name set"
-where
-  "fr (Var x) = {x}"
-| "fr (Const s) = {}"
-| "fr (Lam [x].t) = fr t - {x}"
-| "fr (App t1 t2) = fr t1 \<union> fr t2"
-
-function
-  sfr :: "trm \<Rightarrow> name set"
-where
-  "sfr (Var x) = {}"
-| "sfr (Const s) = {}"
-| "sfr (Lam [x].t) = sfr t - {x}"
-| "sfr (App (App (Const ''unpermute'') (Var p)) (Var x)) = {p, x}"
-| "\<not>(\<exists>p x. t1 = App (Const ''unpermute'') (Var p) \<and> t2 = (Var x)) \<Longrightarrow> sfr (App t1 t2) = sfr t1 \<union> sfr t2"
-defer
-apply(simp_all)
-apply(auto)[1]
-apply(case_tac x)
-apply(simp_all)
-apply(auto)
-apply(blast)
-done
-
-termination
-  apply(relation "measure (\<lambda>t. size t)")
-  apply(simp_all)
-  done
-
-function
-  ss :: "trm \<Rightarrow> nat"
-where
-  "ss (Var x) = 1"
-| "ss (Const s) = 1"
-| "ss (Lam [x].t) = 1 + ss t"
-| "ss (App (App (Const ''unpermute'') (Var p)) (Var x)) = 1"
-| "\<not>(\<exists>p x. t1 = App (Const ''unpermute'') (Var p) \<and> t2 = (Var x)) \<Longrightarrow> ss (App t1 t2) = 1 + ss t1 + ss t2"
-defer
-apply(simp_all)
-apply(auto)[1]
-apply(case_tac x)
-apply(simp_all)
-apply(auto)
-apply(blast)
-done 
-
-termination
-  apply(relation "measure (\<lambda>t. size t)")
-  apply(simp_all)
-  done
-
-inductive
-  improper :: "trm \<Rightarrow> bool"
-where
-  "improper (App (App (Const ''unpermute'') (Var p)) (Var x))"
-| "improper p x t \<Longrightarrow> improper p x (Lam [y].t)"
-| "\<lbrakk>improper p x t1; improper p x t2\<rbrakk> \<Longrightarrow> improper p x (App t1 t2)"
-
-lemma trm_ss:
-  shows "\<not>improper p x t \<Longrightarrow> ss (t[x::= p]) = ss t"
-apply(induct rule: ss.induct)
-apply(simp)
-apply(simp)
-apply(simp)
-apply(auto)[1]
-apply(case_tac "improper p x t")
-apply(drule improper.intros(2))
-apply(blast)
-apply(simp)
-using improper.intros(1)
-apply(blast)
-apply(erule contrapos_pn)
-thm contrapos_np
-apply(simp)
-apply(auto)[1]
-apply(simp)
-apply(erule disjE)
-apply(erule conjE)+
-apply(subst ss.simps)
-apply(simp)
-apply(rule disjI1)
-apply(rule allI)
-apply(rule notI)
-
-apply(simp del: ss.simps)
-apply(erule disjE)
-apply(subst ss.simps)
-apply(simp)
-apply(simp only: subst.simps)
-apply(subst ss.simps)
-apply(simp del: ss.simps)
-apply(rule conjI)
-apply(rule impI)
-apply(erule conjE)
-apply(erule exE)+
-apply(subst ss.simps)
-apply(simp)
-apply(auto)[1]
-apply(simp add: if_splits)
-apply()
-
-function
-  simp :: "name \<Rightarrow> trm \<Rightarrow> trm"
-where
-  "simp p (Const c) = (Const c)"
-| "simp p (Var x) = App (App (Const ''permute'') (Var p)) (Var x)"
-| "simp p (App t1 t2) = (if ((\<exists>x. t1 = App (Const ''unpermute'') (Var p) \<and> t2 = (Var x))) 
-                         then t2
-                         else App (simp p t1) (simp p t2))"
-| "simp p (Lam [x].t) = Lam [x]. (simp p (t[x ::= p]))"
-apply(pat_completeness)
-apply(simp_all)
-apply(auto)
-done
-
-termination
-apply(relation "measure (\<lambda>(_, t). size t)")
-apply(simp_all)
-
-end
\ No newline at end of file
diff -r b6873d123f9b -r 89715c48f728 Nominal/Ex/QuotientSet.thy
--- a/Nominal/Ex/QuotientSet.thy	Sat May 12 21:39:09 2012 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,91 +0,0 @@
-theory QuotientSet
-imports 
-  "../Nominal2"
-begin
-
-lemma supp_quot:
-  "(supp (R, x)) supports (R `` {x})"
-unfolding supports_def
-unfolding fresh_def[symmetric]
-apply(perm_simp)
-apply(simp add: swap_fresh_fresh)
-done
-
-lemma
-  assumes "equiv UNIV R"
-  and "(x, y) \<in> R"
-  shows "R `` {x} = R `` {y}"
-using assms
-by (rule equiv_class_eq)
-
-lemma s1:
-  assumes "equiv UNIV R"
-  and "(x, y) \<in> R"
-  shows "a \<sharp> (R `` {x}) \<longleftrightarrow> a \<sharp> (R `` {y})"
-using assms
-apply(subst equiv_class_eq)
-apply(auto)
-done
-
-lemma s2:
-  fixes x::"'a::fs"
-  assumes "equiv UNIV R"
-  and     "supp R = {}"
-  shows "\<Inter>{supp y | y. (x, y) \<in> R} supports (R `` {x})"
-unfolding supports_def
-apply(rule allI)+
-apply(rule impI)
-apply(rule swap_fresh_fresh)
-apply(drule conjunct1)
-apply(auto)[1]
-apply(subst s1)
-apply(rule assms)
-apply(assumption)
-apply(rule supports_fresh)
-apply(rule supp_quot)
-apply(simp add: supp_Pair finite_supp assms)
-apply(simp add: supp_Pair assms)
-apply(drule conjunct2)
-apply(auto)[1]
-apply(subst s1)
-apply(rule assms)
-apply(assumption)
-apply(rule supports_fresh)
-apply(rule supp_quot)
-apply(simp add: supp_Pair finite_supp assms)
-apply(simp add: supp_Pair assms)
-done
-
-lemma s3:
-  fixes S::"'a::fs set"
-  assumes "finite S"
-  and "S \<noteq> {}"
-  and "a \<sharp> S"
-  shows "\<exists>x \<in> S. a \<sharp> x"
-using assms
-apply(auto simp add: fresh_def)
-apply(subst (asm) supp_of_finite_sets)
-apply(auto)
-done
-
-(*
-lemma supp_inter:
-  fixes x::"'a::fs"
-  assumes "equiv UNIV R"
-  and     "supp R = {}"
-  shows "supp (R `` {x}) = \<Inter>{supp y | y. (x, y) \<in> R}"
-apply(rule finite_supp_unique)
-apply(rule s2)
-apply(rule assms)
-apply(rule assms)
-apply(metis (lam_lifting, no_types) at_base_infinite finite_UNIV)
-*)
-
-  
-
-
-
-end
-
-
-
diff -r b6873d123f9b -r 89715c48f728 Nominal/Ex/SFT/Consts.thy
--- a/Nominal/Ex/SFT/Consts.thy	Sat May 12 21:39:09 2012 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,294 +0,0 @@
-header {* Constant definitions *}
-
-theory Consts imports Utils begin
-
-fun Umn :: "nat \<Rightarrow> nat \<Rightarrow> lam"
-where
-  [simp del]: "Umn 0 n = \<integral>(cn 0). Var (cn n)"
-| [simp del]: "Umn (Suc m) n = \<integral>(cn (Suc m)). Umn m n"
-
-lemma [simp]: "2 = Suc 1"
-  by auto
-
-lemma split_lemma:
-  "(a = b \<and> X) \<or> (a \<noteq> b \<and> Y) \<longleftrightarrow> (a = b \<longrightarrow> X) \<and> (a \<noteq> b \<longrightarrow> Y)"
-  by blast
-
-lemma Lam_U:
-  assumes "x \<noteq> y" "y \<noteq> z" "x \<noteq> z"
-  shows "Umn 2 0 = \<integral>x. \<integral>y. \<integral>z. Var z"
-        "Umn 2 1 = \<integral>x. \<integral>y. \<integral>z. Var y"
-        "Umn 2 2 = \<integral>x. \<integral>y. \<integral>z. Var x"
-  apply (simp_all add: Umn.simps Abs1_eq_iff lam.fresh fresh_at_base flip_def[symmetric] Umn.simps cnd permute_flip_at assms assms[symmetric] split_lemma)
-  apply (intro impI conjI)
-  apply (metis assms)+
-  done
-
-lemma supp_U1: "n \<le> m \<Longrightarrow> atom (cn n) \<notin> supp (Umn m n)"
-  by (induct m)
-     (auto simp add: lam.supp supp_at_base Umn.simps le_Suc_eq)
-
-lemma supp_U2: "supp (Umn m n) \<subseteq> {atom (cn n)}"
-  by (induct m) (auto simp add: lam.supp supp_at_base Umn.simps)
-
-lemma supp_U[simp]: "n \<le> m \<Longrightarrow> supp (Umn m n) = {}"
-  using supp_U1 supp_U2
-  by blast
-
-lemma U_eqvt:
-  "n \<le> m \<Longrightarrow> p \<bullet> (Umn m n) = Umn m n"
-  by (rule_tac [!] perm_supp_eq) (simp_all add: fresh_star_def fresh_def)
-
-definition VAR where "VAR \<equiv> \<integral>cx. \<integral>cy. (Var cy \<cdot> (Umn 2 2) \<cdot> Var cx \<cdot> Var cy)"
-definition "APP \<equiv> \<integral>cx. \<integral>cy. \<integral>cz. (Var cz \<cdot> Umn 2 1 \<cdot> Var cx \<cdot> Var cy \<cdot> Var cz)"
-definition "Abs \<equiv> \<integral>cx. \<integral>cy. (Var cy \<cdot> Umn 2 0 \<cdot> Var cx \<cdot> Var cy)"
-
-lemma VAR_APP_Abs:
-  "x \<noteq> e \<Longrightarrow> VAR = \<integral>x. \<integral>e. (Var e \<cdot> Umn 2 2 \<cdot> Var x \<cdot> Var e)"
-  "e \<noteq> x \<Longrightarrow> e \<noteq> y \<Longrightarrow> x \<noteq> y \<Longrightarrow> APP = \<integral>x. \<integral>y. \<integral>e. (Var e \<cdot> Umn 2 1 \<cdot> Var x \<cdot> Var y \<cdot> Var e)"
-  "x \<noteq> e \<Longrightarrow> Abs = \<integral>x. \<integral>e. (Var e \<cdot> Umn 2 0 \<cdot> Var x \<cdot> Var e)"
-  unfolding VAR_def APP_def Abs_def
-  by (simp_all add: Abs1_eq_iff lam.fresh flip_def[symmetric] U_eqvt fresh_def lam.supp supp_at_base split_lemma permute_flip_at)
-     (auto simp only: cx_cy_cz cx_cy_cz[symmetric])
-
-lemma VAR_app:
-  "VAR \<cdot> x \<cdot> e \<approx> e \<cdot> Umn 2 2 \<cdot> x \<cdot> e"
-  by (rule lam2_fast_app[OF VAR_APP_Abs(1)]) simp_all
-
-lemma APP_app:
-  "APP \<cdot> x \<cdot> y \<cdot> e \<approx> e \<cdot> Umn 2 1 \<cdot> x \<cdot> y \<cdot> e"
-  by (rule lam3_fast_app[OF VAR_APP_Abs(2)]) (simp_all)
-
-lemma Abs_app:
-  "Abs \<cdot> x \<cdot> e \<approx> e \<cdot> Umn 2 0 \<cdot> x \<cdot> e"
-  by (rule lam2_fast_app[OF VAR_APP_Abs(3)]) simp_all
-
-lemma supp_VAR_APP_Abs[simp]:
-  "supp VAR = {}" "supp APP = {}" "supp Abs = {}"
-  by (simp_all add: VAR_def APP_def Abs_def lam.supp supp_at_base) blast+
-
-lemma VAR_APP_Abs_eqvt[eqvt]:
-  "p \<bullet> VAR = VAR" "p \<bullet> APP = APP" "p \<bullet> Abs = Abs"
-  by (rule_tac [!] perm_supp_eq) (simp_all add: fresh_star_def fresh_def)
-
-nominal_primrec
-  Numeral :: "lam \<Rightarrow> lam" ("\<lbrace>_\<rbrace>" 1000)
-where
-  "\<lbrace>Var x\<rbrace> = VAR \<cdot> (Var x)"
-| Ap: "\<lbrace>M \<cdot> N\<rbrace> = APP \<cdot> \<lbrace>M\<rbrace> \<cdot> \<lbrace>N\<rbrace>"
-| "\<lbrace>\<integral>x. M\<rbrace> = Abs \<cdot> (\<integral>x. \<lbrace>M\<rbrace>)"
-proof auto
-  fix x :: lam and P
-  assume "\<And>xa. x = Var xa \<Longrightarrow> P" "\<And>M N. x = M \<cdot> N \<Longrightarrow> P" "\<And>xa M. x = \<integral> xa. M \<Longrightarrow> P"
-  then show "P"
-    by (rule_tac y="x" and c="0 :: perm" in lam.strong_exhaust)
-       (auto simp add: Abs1_eq_iff fresh_star_def)[3]
-next
-  fix x :: name and M and xa :: name and Ma
-  assume "[[atom x]]lst. M = [[atom xa]]lst. Ma"
-    "eqvt_at Numeral_sumC M"
-  then show "[[atom x]]lst. Numeral_sumC M = [[atom xa]]lst. Numeral_sumC Ma"
-    apply -
-    apply (erule Abs_lst1_fcb)
-    apply (simp_all add: Abs_fresh_iff)
-    apply (erule fresh_eqvt_at)
-    apply (simp_all add: finite_supp Abs1_eq_iff eqvt_at_def)
-    done
-next
-  show "eqvt Numeral_graph" unfolding eqvt_def Numeral_graph_def
-    by (rule, perm_simp, rule)
-qed
-
-termination (eqvt) by lexicographic_order
-
-lemma supp_numeral[simp]:
-  "supp \<lbrace>x\<rbrace> = supp x"
-  by (induct x rule: lam.induct)
-     (simp_all add: lam.supp)
-
-lemma fresh_numeral[simp]:
-  "x \<sharp> \<lbrace>y\<rbrace> = x \<sharp> y"
-  unfolding fresh_def by simp
-
-fun app_lst :: "name \<Rightarrow> lam list \<Rightarrow> lam" where
-  "app_lst n [] = Var n"
-| "app_lst n (h # t) = (app_lst n t) \<cdot> h"
-
-lemma app_lst_eqvt[eqvt]: "p \<bullet> (app_lst t ts) = app_lst (p \<bullet> t) (p \<bullet> ts)"
-  by (induct ts arbitrary: t p) (simp_all add: eqvts)
-
-lemma supp_app_lst: "supp (app_lst x l) = {atom x} \<union> supp l"
-  apply (induct l)
-  apply (simp_all add: supp_Nil lam.supp supp_at_base supp_Cons)
-  by blast
-
-lemma app_lst_eq_iff: "app_lst n M = app_lst n N \<Longrightarrow> M = N"
-  by (induct M N rule: list_induct2') simp_all
-
-lemma app_lst_rev_eq_iff: "app_lst n (rev M) = app_lst n (rev N) \<Longrightarrow> M = N"
-  by (drule app_lst_eq_iff) simp
-
-nominal_primrec
-  Ltgt :: "lam list \<Rightarrow> lam" ("\<guillemotleft>_\<guillemotright>" 1000)
-where
-  [simp del]: "atom x \<sharp> l \<Longrightarrow> \<guillemotleft>l\<guillemotright> = \<integral>x. (app_lst x (rev l))"
-  unfolding eqvt_def Ltgt_graph_def
-  apply (rule, perm_simp, rule, rule)
-  apply (rule_tac x="x" and ?'a="name" in obtain_fresh)
-  apply (simp_all add: Abs1_eq_iff lam.fresh swap_fresh_fresh fresh_at_base)
-  apply (simp add: eqvts swap_fresh_fresh)
-  apply (case_tac "x = xa")
-  apply simp_all
-  apply (subgoal_tac "eqvt app_lst")
-  apply (erule fresh_fun_eqvt_app2)
-  apply (simp_all add: fresh_at_base lam.fresh eqvt_def eqvts_raw fresh_rev)
-  done
-
-termination (eqvt) by lexicographic_order
-
-lemma ltgt_eq_iff[simp]:
-  "\<guillemotleft>M\<guillemotright> = \<guillemotleft>N\<guillemotright> \<longleftrightarrow> M = N"
-proof auto
-  obtain x :: name where "atom x \<sharp> (M, N)" using obtain_fresh by auto
-  then have *: "atom x \<sharp> M" "atom x \<sharp> N" using fresh_Pair by simp_all
-  then show "(\<guillemotleft>M\<guillemotright> = \<guillemotleft>N\<guillemotright>) \<Longrightarrow> (M = N)" by (simp add: Abs1_eq_iff app_lst_rev_eq_iff Ltgt.simps)
-qed
-
-lemma Ltgt1_app: "\<guillemotleft>[M]\<guillemotright> \<cdot> N \<approx> N \<cdot> M"
-proof -
-  obtain x :: name where "atom x \<sharp> (M, N)" using obtain_fresh by auto
-  then have "atom x \<sharp> M" "atom x \<sharp> N" using fresh_Pair by simp_all
-  then show ?thesis
-  apply (subst Ltgt.simps)
-  apply (simp add: fresh_Cons fresh_Nil)
-  apply (rule b3, rule bI, simp add: b1)
-  done
-qed
-
-lemma Ltgt3_app: "\<guillemotleft>[M,N,P]\<guillemotright> \<cdot> R \<approx> R \<cdot> M \<cdot> N \<cdot> P"
-proof -
-  obtain x :: name where "atom x \<sharp> (M, N, P, R)" using obtain_fresh by auto
-  then have *: "atom x \<sharp> (M,N,P)" "atom x \<sharp> R" using fresh_Pair by simp_all
-  then have s: "Var x \<cdot> M \<cdot> N \<cdot> P [x ::= R] \<approx> R \<cdot> M \<cdot> N \<cdot> P" using b1 by simp
-  show ?thesis using *
-    apply (subst Ltgt.simps)
-  apply (simp add: fresh_Cons fresh_Nil fresh_Pair_elim)
-  apply auto[1]
-  apply (rule b3, rule bI, simp add: b1)
-  done
-qed
-
-lemma supp_ltgt[simp]:
-  "supp \<guillemotleft>t\<guillemotright> = supp t"
-proof -
-  obtain x :: name where *:"atom x \<sharp> t" using obtain_fresh by auto
-  show ?thesis using *
-  by (simp_all add: Ltgt.simps lam.supp supp_at_base supp_Nil supp_app_lst supp_rev fresh_def)
-qed
-
-lemma fresh_ltgt[simp]:
-  "x \<sharp> \<guillemotleft>[y]\<guillemotright> = x \<sharp> y"
-  "x \<sharp> \<guillemotleft>[t,r,s]\<guillemotright> = x \<sharp> (t,r,s)"
-  by (simp_all add: fresh_def supp_Cons supp_Nil supp_Pair)
-
-lemma Ltgt1_subst[simp]:
-  "\<guillemotleft>[M]\<guillemotright> [y ::= A] = \<guillemotleft>[M [y ::= A]]\<guillemotright>"
-proof -
-  obtain x :: name where a: "atom x \<sharp> (M, A, y, M [y ::= A])" using obtain_fresh by blast
-  have "x \<noteq> y" using a[simplified fresh_Pair fresh_at_base] by simp
-  then show ?thesis
-    apply (subst Ltgt.simps)
-    using a apply (simp add: fresh_Nil fresh_Cons fresh_Pair_elim)
-    apply (subst Ltgt.simps)
-    using a apply (simp add: fresh_Pair_elim fresh_Nil fresh_Cons)
-    apply (simp add: a)
-    done
-qed
-
-lemma U_app:
-  "\<guillemotleft>[A,B,C]\<guillemotright> \<cdot> Umn 2 2 \<approx> A" "\<guillemotleft>[A,B,C]\<guillemotright> \<cdot> Umn 2 1 \<approx> B" "\<guillemotleft>[A,B,C]\<guillemotright> \<cdot> Umn 2 0 \<approx> C"
-  by (rule b3, rule Ltgt3_app, rule lam3_fast_app, rule Lam_U, simp_all)
-     (rule b3, rule Ltgt3_app, rule lam3_fast_app, rule Lam_U[simplified], simp_all)+
-
-definition "F1 \<equiv> \<integral>cx. (APP \<cdot> \<lbrace>VAR\<rbrace> \<cdot> (VAR \<cdot> Var cx))"
-definition "F2 \<equiv> \<integral>cx. \<integral>cy. \<integral>cz. ((APP \<cdot> (APP \<cdot> \<lbrace>APP\<rbrace> \<cdot> (Var cz \<cdot> Var cx))) \<cdot> (Var cz \<cdot> Var cy))"
-definition "F3 \<equiv> \<integral>cx. \<integral>cy. (APP \<cdot> \<lbrace>Abs\<rbrace> \<cdot> (Abs \<cdot> (\<integral>cz. (Var cy \<cdot> (Var cx \<cdot> Var cz)))))"
-
-
-lemma Lam_F:
-  "F1 = \<integral>x. (APP \<cdot> \<lbrace>VAR\<rbrace> \<cdot> (VAR \<cdot> Var x))"
-  "a \<noteq> b \<Longrightarrow> a \<noteq> c \<Longrightarrow> c \<noteq> b \<Longrightarrow> F2 = \<integral>a. \<integral>b. \<integral>c. ((APP \<cdot> (APP \<cdot> \<lbrace>APP\<rbrace> \<cdot> (Var c \<cdot> Var a))) \<cdot> (Var c \<cdot> Var b))"
-  "a \<noteq> b \<Longrightarrow> a \<noteq> x \<Longrightarrow> x \<noteq> b \<Longrightarrow> F3 = \<integral>a. \<integral>b. (APP \<cdot> \<lbrace>Abs\<rbrace> \<cdot> (Abs \<cdot> (\<integral>x. (Var b \<cdot> (Var a \<cdot> Var x)))))"
-  by (simp_all add: F1_def F2_def F3_def Abs1_eq_iff lam.fresh supp_at_base VAR_APP_Abs_eqvt Numeral.eqvt flip_def[symmetric] fresh_at_base split_lemma permute_flip_at)
-     (auto simp add: cx_cy_cz cx_cy_cz[symmetric])
-
-lemma supp_F[simp]:
-  "supp F1 = {}" "supp F2 = {}" "supp F3 = {}"
-  by (simp_all add: F1_def F2_def F3_def lam.supp supp_at_base)
-     blast+
-
-lemma F_eqvt[eqvt]:
-  "p \<bullet> F1 = F1" "p \<bullet> F2 = F2" "p \<bullet> F3 = F3"
-  by (rule_tac [!] perm_supp_eq)
-     (simp_all add: fresh_star_def fresh_def)
-
-lemma F_app:
-  "F1 \<cdot> A \<approx> APP \<cdot> \<lbrace>VAR\<rbrace> \<cdot> (VAR \<cdot> A)"
-  "F2 \<cdot> A \<cdot> B \<cdot> C \<approx> (APP \<cdot> (APP \<cdot> \<lbrace>APP\<rbrace> \<cdot> (C \<cdot> A))) \<cdot> (C \<cdot> B)"
-  by (rule lam1_fast_app, rule Lam_F, simp_all)
-     (rule lam3_fast_app, rule Lam_F, simp_all)
-
-lemma F3_app:
-  assumes f: "atom x \<sharp> A" "atom x \<sharp> B" (* or A and B have empty support *)
-  shows "F3 \<cdot> A \<cdot> B \<approx> APP \<cdot> \<lbrace>Abs\<rbrace> \<cdot> (Abs \<cdot> (\<integral>x. (B \<cdot> (A \<cdot> Var x))))"
-proof -
-  obtain y :: name where b: "atom y \<sharp> (x, A, B)" using obtain_fresh by blast
-  obtain z :: name where c: "atom z \<sharp> (x, y, A, B)" using obtain_fresh by blast
-  have *: "x \<noteq> z" "x \<noteq> y" "y \<noteq> z"
-    using b c by (simp_all add: fresh_Pair fresh_at_base) blast+
-  have **:
-    "atom y \<sharp> z" "atom x \<sharp> z" "atom y \<sharp> x"
-    "atom z \<sharp> y" "atom z \<sharp> x" "atom x \<sharp> y"
-    "atom x \<sharp> A" "atom y \<sharp> A" "atom z \<sharp> A"
-    "atom x \<sharp> B" "atom y \<sharp> B" "atom z \<sharp> B"
-    using b c f by (simp_all add: fresh_Pair fresh_at_base) blast+
-  show ?thesis
-    apply (simp add: Lam_F(3)[of y z x] * *[symmetric])
-    apply (rule b3) apply (rule b5) apply (rule bI)
-    apply (simp add: ** fresh_Pair * *[symmetric])
-    apply (rule b3) apply (rule bI)
-    apply (simp add: ** fresh_Pair * *[symmetric])
-    apply (rule b1)
-    done
-qed
-
-definition Lam_A1_pre : "A1 \<equiv> \<integral>cx. \<integral>cy. (F1 \<cdot> Var cx)"
-definition Lam_A2_pre : "A2 \<equiv> \<integral>cx. \<integral>cy. \<integral>cz. (F2 \<cdot> Var cx \<cdot> Var cy \<cdot> \<guillemotleft>[Var cz]\<guillemotright>)"
-definition Lam_A3_pre : "A3 \<equiv> \<integral>cx. \<integral>cy. (F3 \<cdot> Var cx \<cdot> \<guillemotleft>[Var cy]\<guillemotright>)"
-lemma Lam_A:
-  "x \<noteq> y \<Longrightarrow> A1 = \<integral>x. \<integral>y. (F1 \<cdot> Var x)"
-  "a \<noteq> b \<Longrightarrow> a \<noteq> c \<Longrightarrow> c \<noteq> b \<Longrightarrow> A2 = \<integral>a. \<integral>b. \<integral>c. (F2 \<cdot> Var a \<cdot> Var b \<cdot> \<guillemotleft>[Var c]\<guillemotright>)"
-  "a \<noteq> b \<Longrightarrow> A3 = \<integral>a. \<integral>b. (F3 \<cdot> Var a \<cdot> \<guillemotleft>[Var b]\<guillemotright>)"
-  by (simp_all add: Lam_A1_pre Lam_A2_pre Lam_A3_pre Abs1_eq_iff lam.fresh supp_at_base VAR_APP_Abs_eqvt Numeral.eqvt flip_def[symmetric] fresh_at_base F_eqvt Ltgt.eqvt split_lemma permute_flip_at cx_cy_cz cx_cy_cz[symmetric])
-     auto
-
-lemma supp_A[simp]:
-  "supp A1 = {}" "supp A2 = {}" "supp A3 = {}"
-  by (auto simp add: Lam_A1_pre Lam_A2_pre Lam_A3_pre lam.supp supp_at_base supp_Cons supp_Nil)
-
-lemma A_app:
-  "A1 \<cdot> A \<cdot> B \<approx> F1 \<cdot> A"
-  "A2 \<cdot> A \<cdot> B \<cdot> C \<approx> F2 \<cdot> A \<cdot> B \<cdot> \<guillemotleft>[C]\<guillemotright>"
-  "A3 \<cdot> A \<cdot> B \<approx> F3 \<cdot> A \<cdot> \<guillemotleft>[B]\<guillemotright>"
-  apply (rule lam2_fast_app, rule Lam_A, simp_all)
-  apply (rule lam3_fast_app, rule Lam_A, simp_all)
-  apply (rule lam2_fast_app, rule Lam_A, simp_all)
-  done
-
-definition "Num \<equiv> \<guillemotleft>[\<guillemotleft>[A1,A2,A3]\<guillemotright>]\<guillemotright>"
-
-lemma supp_Num[simp]:
-  "supp Num = {}"
-  by (auto simp only: Num_def supp_ltgt supp_Pair supp_A supp_Cons supp_Nil)
-
-end
diff -r b6873d123f9b -r 89715c48f728 Nominal/Ex/SFT/LambdaTerms.thy
--- a/Nominal/Ex/SFT/LambdaTerms.thy	Sat May 12 21:39:09 2012 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,83 +0,0 @@
-header {* Definition of Lambda terms and convertibility *}
-
-theory LambdaTerms imports "../../Nominal2" begin
-
-lemma [simp]: "supp x = {} \<Longrightarrow> y \<sharp> x"
-  unfolding fresh_def by blast
-
-atom_decl name
-
-nominal_datatype lam =
-  Var "name"
-| App "lam" "lam"
-| Lam x::"name" l::"lam"  binds x in l ("Lam [_]. _" [100, 100] 100)
-
-notation
-  App (infixl "\<cdot>" 98) and
-  Lam ("\<integral> _. _" [97, 97] 99)
-
-nominal_primrec
-  subst :: "lam \<Rightarrow> name \<Rightarrow> lam \<Rightarrow> lam"  ("_ [_ ::= _]" [90, 90, 90] 90)
-where
-  "(Var x)[y ::= s] = (if x = y then s else (Var x))"
-| "(t1 \<cdot> t2)[y ::= s] = (t1[y ::= s]) \<cdot> (t2[y ::= s])"
-| "atom x \<sharp> (y, s) \<Longrightarrow> (\<integral>x. t)[y ::= s] = \<integral>x.(t[y ::= s])"
-proof auto
-  fix a b :: lam and aa :: name and P
-  assume "\<And>x y s. a = Var x \<and> aa = y \<and> b = s \<Longrightarrow> P"
-    "\<And>t1 t2 y s. a = t1 \<cdot> t2 \<and> aa = y \<and> b = s \<Longrightarrow> P"
-    "\<And>x y s t. \<lbrakk>atom x \<sharp> (y, s); a = \<integral> x. t \<and> aa = y \<and> b = s\<rbrakk> \<Longrightarrow> P"
-  then show "P"
-    by (rule_tac y="a" and c="(aa, b)" in lam.strong_exhaust)
-       (blast, blast, simp add: fresh_star_def)
-next
-  fix x :: name and t and xa :: name and ya sa ta
-  assume *: "eqvt_at subst_sumC (t, ya, sa)"
-    "atom x \<sharp> (ya, sa)" "atom xa \<sharp> (ya, sa)"
-    "[[atom x]]lst. t = [[atom xa]]lst. ta"
-  then show "[[atom x]]lst. subst_sumC (t, ya, sa) = [[atom xa]]lst. subst_sumC (ta, ya, sa)"
-    apply -
-    apply (erule Abs_lst1_fcb)
-    apply(simp (no_asm) add: Abs_fresh_iff)
-    apply(drule_tac a="atom xa" in fresh_eqvt_at)
-    apply(simp add: finite_supp)
-    apply(simp_all add: fresh_Pair_elim Abs_fresh_iff Abs1_eq_iff)
-    apply(subgoal_tac "(atom x \<rightleftharpoons> atom xa) \<bullet> ya = ya")
-    apply(subgoal_tac "(atom x \<rightleftharpoons> atom xa) \<bullet> sa = sa")
-    apply(simp add: atom_eqvt eqvt_at_def)
-    apply(rule perm_supp_eq, simp add: supp_swap fresh_star_def fresh_Pair)+
-    done
-next
-  show "eqvt subst_graph" unfolding eqvt_def subst_graph_def
-    by (rule, perm_simp, rule)
-qed
-
-termination (eqvt) by lexicographic_order
-
-lemma forget[simp]:
-  shows "atom x \<sharp> t \<Longrightarrow> t[x ::= s] = t"
-  by (nominal_induct t avoiding: x s rule: lam.strong_induct)
-     (auto simp add: lam.fresh fresh_at_base)
-
-lemma forget_closed[simp]: "supp t = {} \<Longrightarrow> t[x ::= s] = t"
-  by (simp add: fresh_def)
-
-lemma subst_id[simp]: "M [x ::= Var x] = M"
-  by (rule_tac lam="M" and c="x" in lam.strong_induct)
-     (simp_all add: fresh_star_def lam.fresh fresh_Pair)
-
-inductive
-  beta :: "lam \<Rightarrow> lam \<Rightarrow> bool" (infix "\<approx>" 80)
-where
-  bI: "(\<integral>x. M) \<cdot> N \<approx> M[x ::= N]"
-| b1: "M \<approx> M"
-| b2: "M \<approx> N \<Longrightarrow> N \<approx> M"
-| b3: "M \<approx> N \<Longrightarrow> N \<approx> L \<Longrightarrow> M \<approx> L"
-| b4: "M \<approx> N \<Longrightarrow> Z \<cdot> M \<approx> Z \<cdot> N"
-| b5: "M \<approx> N \<Longrightarrow> M \<cdot> Z \<approx> N \<cdot> Z"
-| b6: "M \<approx> N \<Longrightarrow> \<integral>x. M \<approx> \<integral>x. N"
-
-lemmas [trans] = b3
-equivariance beta
-
-end
diff -r b6873d123f9b -r 89715c48f728 Nominal/Ex/SFT/Theorem.thy
--- a/Nominal/Ex/SFT/Theorem.thy	Sat May 12 21:39:09 2012 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,70 +0,0 @@
-header {* The main lemma about Num and the Second Fixed Point Theorem *}
-
-theory Theorem imports Consts begin
-
-lemmas [simp] = b3[OF bI] b1 b4 b5 supp_Num[unfolded Num_def supp_ltgt] Num_def lam.fresh[unfolded fresh_def] fresh_def b6
-lemmas app = Ltgt1_app
-
-lemma Num:
-  shows "Num \<cdot> \<lbrace>M\<rbrace> \<approx> \<lbrace>\<lbrace>M\<rbrace>\<rbrace>"
-proof (induct M rule: lam.induct)
-  case (Var n)
-  have "Num \<cdot> \<lbrace>Var n\<rbrace> = Num \<cdot> (VAR \<cdot> Var n)" by simp
-  also have "... = \<guillemotleft>[\<guillemotleft>[A1,A2,A3]\<guillemotright>]\<guillemotright> \<cdot> (VAR \<cdot> Var n)" by simp
-  also have "... \<approx> VAR \<cdot> Var n \<cdot> \<guillemotleft>[A1,A2,A3]\<guillemotright>" using app .
-  also have "... \<approx> \<guillemotleft>[A1,A2,A3]\<guillemotright> \<cdot> Umn 2 2 \<cdot> Var n \<cdot> \<guillemotleft>[A1,A2,A3]\<guillemotright>" using VAR_app .
-  also have "... \<approx> A1 \<cdot> Var n \<cdot> \<guillemotleft>[A1,A2,A3]\<guillemotright>" using U_app by simp
-  also have "... \<approx> F1 \<cdot> Var n" using A_app(1) .
-  also have "... \<approx> APP \<cdot> \<lbrace>VAR\<rbrace> \<cdot> (VAR \<cdot> Var n)" using F_app(1) .
-  also have "... = \<lbrace>\<lbrace>Var n\<rbrace>\<rbrace>" by simp
-  finally show "Num \<cdot> \<lbrace>Var n\<rbrace> \<approx> \<lbrace>\<lbrace>Var n\<rbrace>\<rbrace>".
-next
-  case (App M N)
-  assume IH: "Num \<cdot> \<lbrace>M\<rbrace> \<approx> \<lbrace>\<lbrace>M\<rbrace>\<rbrace>" "Num \<cdot> \<lbrace>N\<rbrace> \<approx> \<lbrace>\<lbrace>N\<rbrace>\<rbrace>"
-  have "Num \<cdot> \<lbrace>M \<cdot> N\<rbrace> = Num \<cdot> (APP \<cdot> \<lbrace>M\<rbrace> \<cdot> \<lbrace>N\<rbrace>)" by simp
-  also have "... = \<guillemotleft>[\<guillemotleft>[A1,A2,A3]\<guillemotright>]\<guillemotright> \<cdot> (APP \<cdot> \<lbrace>M\<rbrace> \<cdot> \<lbrace>N\<rbrace>)" by simp
-  also have "... \<approx> APP \<cdot> \<lbrace>M\<rbrace> \<cdot> \<lbrace>N\<rbrace> \<cdot> \<guillemotleft>[A1,A2,A3]\<guillemotright>" using app .
-  also have "... \<approx> \<guillemotleft>[A1,A2,A3]\<guillemotright> \<cdot> Umn 2 1 \<cdot> \<lbrace>M\<rbrace> \<cdot> \<lbrace>N\<rbrace> \<cdot> \<guillemotleft>[A1,A2,A3]\<guillemotright>" using APP_app .
-  also have "... \<approx> A2 \<cdot> \<lbrace>M\<rbrace> \<cdot> \<lbrace>N\<rbrace> \<cdot> \<guillemotleft>[A1,A2,A3]\<guillemotright>" using U_app by simp
-  also have "... \<approx> F2 \<cdot> \<lbrace>M\<rbrace> \<cdot> \<lbrace>N\<rbrace> \<cdot> Num" using A_app(2) by simp
-  also have "... \<approx> APP \<cdot> (APP \<cdot> \<lbrace>APP\<rbrace> \<cdot> (Num \<cdot> \<lbrace>M\<rbrace>)) \<cdot> (Num \<cdot> \<lbrace>N\<rbrace>)" using F_app(2) .
-  also have "... \<approx> APP \<cdot> (APP \<cdot> \<lbrace>APP\<rbrace> \<cdot> (\<lbrace>\<lbrace>M\<rbrace>\<rbrace>)) \<cdot> (Num \<cdot> \<lbrace>N\<rbrace>)" using IH by simp
-  also have "... \<approx> \<lbrace>\<lbrace>M \<cdot> N\<rbrace>\<rbrace>" using IH by simp
-  finally show "Num \<cdot> \<lbrace>M \<cdot> N\<rbrace> \<approx> \<lbrace>\<lbrace>M \<cdot> N\<rbrace>\<rbrace>".
-next
-  case (Lam x P)
-  assume IH: "Num \<cdot> \<lbrace>P\<rbrace> \<approx> \<lbrace>\<lbrace>P\<rbrace>\<rbrace>"
-  have "Num \<cdot> \<lbrace>\<integral> x. P\<rbrace> = Num \<cdot> (Abs \<cdot> \<integral> x. \<lbrace>P\<rbrace>)" by simp
-  also have "... = \<guillemotleft>[\<guillemotleft>[A1,A2,A3]\<guillemotright>]\<guillemotright> \<cdot> (Abs \<cdot> \<integral> x. \<lbrace>P\<rbrace>)" by simp
-  also have "... \<approx> Abs \<cdot> (\<integral> x. \<lbrace>P\<rbrace>) \<cdot> \<guillemotleft>[A1,A2,A3]\<guillemotright>" using app .
-  also have "... \<approx> \<guillemotleft>[A1,A2,A3]\<guillemotright> \<cdot> Umn 2 0 \<cdot> (\<integral> x. \<lbrace>P\<rbrace>) \<cdot> \<guillemotleft>[A1,A2,A3]\<guillemotright>" using Abs_app .
-  also have "... \<approx> A3 \<cdot> (\<integral> x. \<lbrace>P\<rbrace>) \<cdot> \<guillemotleft>[A1,A2,A3]\<guillemotright>" using U_app by simp
-  also have "... \<approx> F3 \<cdot> (\<integral> x. \<lbrace>P\<rbrace>) \<cdot> \<guillemotleft>[\<guillemotleft>[A1,A2,A3]\<guillemotright>]\<guillemotright>" using A_app(3) .
-  also have "... = F3 \<cdot> (\<integral> x. \<lbrace>P\<rbrace>) \<cdot> Num" by simp
-  also have "... \<approx> APP \<cdot> \<lbrace>Abs\<rbrace> \<cdot> (Abs \<cdot> \<integral> x. (Num \<cdot> ((\<integral> x. \<lbrace>P\<rbrace>) \<cdot> Var x)))" by (rule F3_app) simp_all
-  also have "... \<approx> APP \<cdot> \<lbrace>Abs\<rbrace> \<cdot> (Abs \<cdot> \<integral> x. (Num \<cdot> \<lbrace>P\<rbrace>))" using beta_app by simp
-  also have "... \<approx> APP \<cdot> \<lbrace>Abs\<rbrace> \<cdot> (Abs \<cdot> \<integral> x. \<lbrace>\<lbrace>P\<rbrace>\<rbrace>)" using IH by simp
-  also have "... = \<lbrace>\<lbrace>\<integral> x. P\<rbrace>\<rbrace>" by simp
-  finally show "Num \<cdot> \<lbrace>\<integral> x. P\<rbrace> \<approx> \<lbrace>\<lbrace>\<integral> x. P\<rbrace>\<rbrace>" .
-qed
-
-lemmas [simp] = Ap Num
-lemmas [simp del] = fresh_def Num_def
-
-theorem SFP:
-  fixes F :: lam
-  shows "\<exists>X. X \<approx> F \<cdot> \<lbrace>X\<rbrace>"
-proof -
-  obtain x :: name where [simp]:"atom x \<sharp> F" using obtain_fresh by blast
-  def W \<equiv> "\<integral>x. (F \<cdot> (APP \<cdot> Var x \<cdot> (Num \<cdot> Var x)))"
-  def X \<equiv> "W \<cdot> \<lbrace>W\<rbrace>"
-  have a: "X = W \<cdot> \<lbrace>W\<rbrace>" unfolding X_def ..
-  also have "... = (\<integral>x. (F \<cdot> (APP \<cdot> Var x \<cdot> (Num \<cdot> Var x)))) \<cdot> \<lbrace>W\<rbrace>" unfolding W_def ..
-  also have "... \<approx> F \<cdot> (APP \<cdot> \<lbrace>W\<rbrace> \<cdot> (Num \<cdot> \<lbrace>W\<rbrace>))" by simp
-  also have "... \<approx> F \<cdot> (APP \<cdot> \<lbrace>W\<rbrace> \<cdot> \<lbrace>\<lbrace>W\<rbrace>\<rbrace>)" by simp
-  also have "... \<approx> F \<cdot> \<lbrace>W \<cdot> \<lbrace>W\<rbrace>\<rbrace>" by simp
-  also have "... = F \<cdot> \<lbrace>X\<rbrace>" unfolding X_def ..
-  finally show ?thesis by blast
-qed
-
-end
diff -r b6873d123f9b -r 89715c48f728 Nominal/Ex/SFT/Utils.thy
--- a/Nominal/Ex/SFT/Utils.thy	Sat May 12 21:39:09 2012 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,102 +0,0 @@
-header {* Utilities for defining constants and functions *}
-
-theory Utils imports LambdaTerms begin
-
-lemma beta_app:
-  "(\<integral> x. M) \<cdot> Var x \<approx> M"
-  by (rule b3, rule bI)
-     (simp add: b1)
-
-lemma lam1_fast_app:
-  assumes leq: "\<And>a. (L = \<integral> a. (F (V a)))"
-      and su: "\<And>x. atom x \<sharp> A \<Longrightarrow> F (V x) [x ::= A] = F A"
-  shows "L \<cdot> A \<approx> F A"
-proof -
-  obtain x :: name where a: "atom x \<sharp> A" using obtain_fresh by blast
-  show ?thesis
-    by (simp add: leq[of x], rule b3, rule bI, simp add: su b1 a)
-qed
-
-lemma lam2_fast_app:
-  assumes leq: "\<And>a b. a \<noteq> b \<Longrightarrow> L = \<integral> a. \<integral> b. (F (V a) (V b))"
-     and su: "\<And>x y. atom x \<sharp> A \<Longrightarrow> atom y \<sharp> A \<Longrightarrow> atom x \<sharp> B \<Longrightarrow> atom y \<sharp> B \<Longrightarrow>
-       x \<noteq> y \<Longrightarrow> F (V x) (V y) [x ::= A] [y ::= B] = F A B"
-  shows "L \<cdot> A \<cdot> B \<approx> F A B"
-proof -
-  obtain x :: name where a: "atom x \<sharp> (A, B)" using obtain_fresh by blast
-  obtain y :: name where b: "atom y \<sharp> (x, A, B)" using obtain_fresh by blast
-  obtain z :: name where c: "atom z \<sharp> (x, y, A, B)" using obtain_fresh by blast
-  have *: "x \<noteq> y" "x \<noteq> z" "y \<noteq> z"
-    using a b c by (simp_all add: fresh_Pair fresh_at_base) blast+
-  have ** : "atom y \<sharp> z" "atom x \<sharp> z" "atom y \<sharp> x"
-            "atom z \<sharp> y" "atom z \<sharp> x" "atom x \<sharp> y"
-            "atom x \<sharp> A" "atom y \<sharp> A" "atom z \<sharp> A"
-            "atom x \<sharp> B" "atom y \<sharp> B" "atom z \<sharp> B"
-    using a b c by (simp_all add: fresh_Pair fresh_at_base) blast+
-  show ?thesis
-    apply (simp add: leq[OF *(1)])
-    apply (rule b3) apply (rule b5) apply (rule bI)
-    apply (simp add: ** fresh_Pair)
-    apply (rule b3) apply (rule bI) apply (simp add: su b1 ** *)
-    done
-  qed
-
-lemma lam3_fast_app:
-  assumes leq: "\<And>a b c. a \<noteq> b \<Longrightarrow> b \<noteq> c \<Longrightarrow> c \<noteq> a \<Longrightarrow>
-       L = \<integral> a. \<integral> b. \<integral> c. (F (V a) (V b) (V c))"
-     and su: "\<And>x y z. atom x \<sharp> A \<Longrightarrow> atom y \<sharp> A \<Longrightarrow> atom z \<sharp> A \<Longrightarrow>
-                     atom x \<sharp> B \<Longrightarrow> atom y \<sharp> B \<Longrightarrow> atom z \<sharp> B \<Longrightarrow>
-                     atom y \<sharp> B \<Longrightarrow> atom y \<sharp> B \<Longrightarrow> atom z \<sharp> B \<Longrightarrow>
-                     x \<noteq> y \<Longrightarrow> y \<noteq> z \<Longrightarrow> z \<noteq> x \<Longrightarrow>
-      ((F (V x) (V y) (V z))[x ::= A] [y ::= B] [z ::= C] = F A B C)"
-  shows "L \<cdot> A \<cdot> B \<cdot> C \<approx> F A B C"
-proof -
-  obtain x :: name where a: "atom x \<sharp> (A, B, C)" using obtain_fresh by blast
-  obtain y :: name where b: "atom y \<sharp> (x, A, B, C)" using obtain_fresh by blast
-  obtain z :: name where c: "atom z \<sharp> (x, y, A, B, C)" using obtain_fresh by blast
-  have *: "x \<noteq> y" "y \<noteq> z" "z \<noteq> x"
-    using a b c by (simp_all add: fresh_Pair fresh_at_base) blast+
-  have ** : "atom y \<sharp> z" "atom x \<sharp> z" "atom y \<sharp> x"
-            "atom z \<sharp> y" "atom z \<sharp> x" "atom x \<sharp> y"
-            "atom x \<sharp> A" "atom y \<sharp> A" "atom z \<sharp> A"
-            "atom x \<sharp> B" "atom y \<sharp> B" "atom z \<sharp> B"
-            "atom x \<sharp> C" "atom y \<sharp> C" "atom z \<sharp> C"
-    using a b c by (simp_all add: fresh_Pair fresh_at_base) blast+
-  show ?thesis
-    apply (simp add: leq[OF *(1) *(2) *(3)])
-    apply (rule b3) apply (rule b5) apply (rule b5) apply (rule bI)
-    apply (simp add: ** fresh_Pair)
-    apply (rule b3) apply (rule b5) apply (rule bI)
-    apply (simp add: ** fresh_Pair)
-    apply (rule b3) apply (rule bI) apply (simp add: su b1 ** *)
-    done
-  qed
-
-definition cn :: "nat \<Rightarrow> name" where "cn n \<equiv> Abs_name (Atom (Sort ''LambdaTerms.name'' []) n)"
-
-lemma cnd[simp]: "m \<noteq> n \<Longrightarrow> cn m \<noteq> cn n"
-  unfolding cn_def using Abs_name_inject by simp
-
-definition cx :: name where "cx \<equiv> cn 0"
-definition cy :: name where "cy \<equiv> cn 1"
-definition cz :: name where "cz \<equiv> cn 2"
-
-lemma cx_cy_cz[simp]:
-  "cx \<noteq> cy" "cx \<noteq> cz" "cz \<noteq> cy"
-  unfolding cx_def cy_def cz_def
-  by simp_all
-
-lemma noteq_fresh: "atom x \<sharp> y = (x \<noteq> y)"
-  by (simp add: fresh_at_base(2))
-
-lemma fresh_fun_eqvt_app2:
-  assumes a: "eqvt f"
-  and b: "a \<sharp> x" "a \<sharp> y"
-  shows "a \<sharp> f x y"
-  using fresh_fun_eqvt_app[OF a b(1)] a b
-  by (metis fresh_fun_app)
-
-end
-
-
-
diff -r b6873d123f9b -r 89715c48f728 Nominal/Ex/SubstNoFcb.thy
--- a/Nominal/Ex/SubstNoFcb.thy	Sat May 12 21:39:09 2012 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,84 +0,0 @@
-theory Lambda imports "../Nominal2" begin
-
-atom_decl name
-
-nominal_datatype lam =
-  Var "name"
-| App "lam" "lam"
-| Lam x::"name" l::"lam"  binds x in l ("Lam [_]. _" [100, 100] 100)
-
-nominal_primrec lam_rec ::
-  "(name \<Rightarrow> 'a :: pt) \<Rightarrow> (lam \<Rightarrow> lam \<Rightarrow> 'a) \<Rightarrow> (name \<Rightarrow> lam \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'b :: fs \<Rightarrow> lam \<Rightarrow> 'a"
-where
-  "lam_rec fv fa fl fd P (Var n) = fv n"
-| "lam_rec fv fa fl fd P (App l r) = fa l r"
-| "(atom x \<sharp> P \<and> (\<forall>y s. atom y \<sharp> P \<longrightarrow> Lam [x]. t = Lam [y]. s \<longrightarrow> fl x t = fl y s)) \<Longrightarrow>
-     lam_rec fv fa fl fd P (Lam [x]. t) = fl x t"
-| "(atom x \<sharp> P \<and> \<not>(\<forall>y s. atom y \<sharp> P \<longrightarrow> Lam [x]. t = Lam [y]. s \<longrightarrow> fl x t = fl y s)) \<Longrightarrow>
-     lam_rec fv fa fl fd P (Lam [x]. t) = fd"
-  apply (simp add: eqvt_def lam_rec_graph_def)
-  apply (rule, perm_simp, rule, rule)
-  apply (case_tac x)
-  apply (rule_tac y="f" and c="e" in lam.strong_exhaust)
-  apply metis
-  apply metis
-  unfolding fresh_star_def
-  apply simp
-  apply metis
-  apply simp_all[2]
-  apply (metis (no_types) Pair_inject lam.distinct)+
-  apply simp
-  apply (metis (no_types) Pair_inject lam.distinct)+
-  done
-
-termination (eqvt) by lexicographic_order
-
-lemma lam_rec_cong[fundef_cong]:
-  " (\<And>v. l = Var v \<Longrightarrow> fv v = fv' v) \<Longrightarrow>
-    (\<And>t1 t2. l = App t1 t2 \<Longrightarrow> fa t1 t2 = fa' t1 t2) \<Longrightarrow>
-    (\<And>n t. l = Lam [n]. t \<Longrightarrow> fl n t = fl' n t) \<Longrightarrow>
-  lam_rec fv fa fl fd P l = lam_rec fv' fa' fl' fd P l"
-  apply (rule_tac y="l" and c="P" in lam.strong_exhaust)
-  apply auto
-  apply (case_tac "(\<forall>y s. atom y \<sharp> P \<longrightarrow> Lam [name]. lam = Lam [y]. s \<longrightarrow> fl name lam = fl y s)")
-  apply (subst lam_rec.simps) apply (simp add: fresh_star_def)
-  apply (subst lam_rec.simps) apply (simp add: fresh_star_def)
-  using Abs1_eq_iff lam.eq_iff apply metis
-  apply (subst lam_rec.simps(4)) apply (simp add: fresh_star_def)
-  apply (subst lam_rec.simps(4)) apply (simp add: fresh_star_def)
-  using Abs1_eq_iff lam.eq_iff apply metis
-  done
-
-nominal_primrec substr where
-[simp del]: "substr l y s = lam_rec
-  (%x. if x = y then s else (Var x))
-  (%t1 t2. App (substr t1 y s) (substr t2 y s))
-  (%x t. Lam [x]. (substr t y s)) (Lam [y]. Var y) (y, s) l"
-unfolding eqvt_def substr_graph_def
-apply (rule, perm_simp, rule, rule)
-by pat_completeness auto
-
-termination (eqvt) by lexicographic_order
-
-lemma fresh_fun_eqvt_app3:
-  assumes e: "eqvt f"
-  shows "\<lbrakk>a \<sharp> x; a \<sharp> y; a \<sharp> z\<rbrakk> \<Longrightarrow> a \<sharp> f x y z"
-  using fresh_fun_eqvt_app[OF e] fresh_fun_app by (metis (lifting, full_types))
-
-lemma substr_simps:
-  "substr (Var x) y s = (if x = y then s else (Var x))"
-  "substr (App t1 t2) y s = App (substr t1 y s) (substr t2 y s)"
-  "atom x \<sharp> (y, s) \<Longrightarrow> substr (Lam [x]. t) y s = Lam [x]. (substr t y s)"
-  apply (subst substr.simps) apply (simp only: lam_rec.simps)
-  apply (subst substr.simps) apply (simp only: lam_rec.simps)
-  apply (subst substr.simps) apply (subst lam_rec.simps)
-  apply (auto simp add: Abs1_eq_iff substr.eqvt swap_fresh_fresh)
-  apply (rule fresh_fun_eqvt_app3[of substr])
-  apply (simp add: eqvt_def eqvts_raw)
-  apply (simp_all add: fresh_Pair)
-  done
-
-end
-
-
-
diff -r b6873d123f9b -r 89715c48f728 Nominal/Ex/TypeVarsTest.thy
--- a/Nominal/Ex/TypeVarsTest.thy	Sat May 12 21:39:09 2012 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,59 +0,0 @@
-theory TypeVarsTest
-imports "../Nominal2" 
-begin
-
-(* a nominal datatype with type variables and sorts *)
-
-
-(* the sort constraints need to be attached to the  *)
-(* first occurence of the type variables on the     *)
-(* right-hand side                                  *)
-
-atom_decl name
-
-class s1
-class s2
-
-instance nat :: s1 ..
-instance int :: s2 .. 
-
-nominal_datatype ('a::s1, 'b::s2, 'c::at) lam =
-  Var "name"
-| App "('a, 'b, 'c) lam" "('a, 'b, 'c) lam"
-| Lam x::"name" l::"('a, 'b, 'c) lam"  binds x in l
-| Foo "'a" "'b"
-| Bar x::"'c" l::"('a, 'b, 'c) lam"  binds x in l   (* Bar binds a polymorphic atom *)
-
-term Foo
-term Bar
-
-thm lam.distinct
-thm lam.induct
-thm lam.exhaust 
-thm lam.strong_exhaust
-thm lam.fv_defs
-thm lam.bn_defs
-thm lam.perm_simps
-thm lam.eq_iff
-thm lam.fv_bn_eqvt
-thm lam.size_eqvt
-
-
-nominal_datatype ('alpha, 'beta, 'gamma) psi =
-  PsiNil
-| Output "'alpha" "'alpha" "('alpha, 'beta, 'gamma) psi" 
-
-
-nominal_datatype 'a foo = 
-  Node x::"name" f::"'a foo" binds x in f
-| Leaf "'a"
-
-term "Leaf"
-
-
-
-
-end
-
-
-
diff -r b6873d123f9b -r 89715c48f728 Nominal/ROOT.ML
--- a/Nominal/ROOT.ML	Sat May 12 21:39:09 2012 +0100
+++ b/Nominal/ROOT.ML	Sat May 12 22:21:25 2012 +0100
@@ -18,12 +18,12 @@
     "Ex/LetRec2",
     "Ex/LetFun",
     "Ex/Modules",
+
     "Ex/SingleLet",
     "Ex/Shallow",
     "Ex/SystemFOmega",
     "Ex/TypeSchemes1",
     "Ex/TypeSchemes2",
-    "Ex/TypeVarsTest",
     "Ex/Foo1",
     "Ex/Foo2",
     "Ex/CoreHaskell",