isar-keywords.el
authorurbanc
Thu Apr 27 01:41:30 2006 +0200 (2006-04-27)
changeset 19477a95176d0f0dd
parent 19476 816f519f8b72
child 19478 25778eacbe21
isar-keywords.el
- I am not sure what has changed here

nominal.thy
- includes a number of new lemmas (including freshness
and perm_aux things)

nominal_atoms.ML
- no particular changes here

nominal_permeq.ML
- a new version of the decision procedure using
for permutation composition the constant perm_aux

examples
- various adjustments
src/HOL/Nominal/Examples/CR.thy
src/HOL/Nominal/Examples/Class.thy
src/HOL/Nominal/Examples/Iteration.thy
src/HOL/Nominal/Nominal.thy
src/HOL/Nominal/nominal_atoms.ML
src/HOL/Nominal/nominal_permeq.ML
     1.1 --- a/src/HOL/Nominal/Examples/CR.thy	Wed Apr 26 22:40:46 2006 +0200
     1.2 +++ b/src/HOL/Nominal/Examples/CR.thy	Thu Apr 27 01:41:30 2006 +0200
     1.3 @@ -32,7 +32,7 @@
     1.4    assumes asm: "a\<sharp>t\<^isub>1"
     1.5    shows "t\<^isub>1[a::=t\<^isub>2] = t\<^isub>1"
     1.6    using asm by (nominal_induct t\<^isub>1 avoiding: a t\<^isub>2 rule: lam.induct)
     1.7 -             (auto simp add: abs_fresh fresh_atm)
     1.8 +               (auto simp add: abs_fresh fresh_atm)
     1.9  
    1.10  lemma fresh_fact: 
    1.11    fixes a :: "name"
    1.12 @@ -108,7 +108,7 @@
    1.13    have ih: "\<And>x y N L. \<lbrakk>x\<noteq>y; x\<sharp>L\<rbrakk> \<Longrightarrow> M1[x::=N][y::=L] = M1[y::=L][x::=N[y::=L]]" by fact
    1.14    have "x\<noteq>y" by fact
    1.15    have "x\<sharp>L" by fact
    1.16 -  have "z\<sharp>x" "z\<sharp>y" "z\<sharp>N" "z\<sharp>L" by fact
    1.17 +  have fs: "z\<sharp>x" "z\<sharp>y" "z\<sharp>N" "z\<sharp>L" by fact
    1.18    hence "z\<sharp>N[y::=L]" by (simp add: fresh_fact)
    1.19    show "(Lam [z].M1)[x::=N][y::=L] = (Lam [z].M1)[y::=L][x::=N[y::=L]]" (is "?LHS=?RHS") 
    1.20    proof -
     2.1 --- a/src/HOL/Nominal/Examples/Class.thy	Wed Apr 26 22:40:46 2006 +0200
     2.2 +++ b/src/HOL/Nominal/Examples/Class.thy	Thu Apr 27 01:41:30 2006 +0200
     2.3 @@ -176,6 +176,31 @@
     2.4  apply(assumption, rule at_prm_eq_append'[OF at_name_inst], assumption)
     2.5  done
     2.6  
     2.7 +lemma rec_fin_supp: 
     2.8 +assumes f: "finite ((supp (f1,f2,f3,f3,f4,f5,f6,f7,f8,f9,f10,f11,f12))::name set)"
     2.9 +  and   c: "\<exists>(a::name). a\<sharp>f3 \<and> (\<forall>t (r::'a::pt_name). a\<sharp>f3 a t r)"
    2.10 +  and   a: "(t,r) \<in> trm_rec_set f1 f2 f3"
    2.11 +  shows "finite ((supp r)::name set)"
    2.12 +using a 
    2.13 +proof (induct)
    2.14 +  case goal1 thus ?case using f by (finite_guess add: supp_prod fs_name1)
    2.15 +next
    2.16 +  case goal2 thus ?case using f by (finite_guess add: supp_prod fs_name1)
    2.17 +next
    2.18 +  case (goal3 c t r)
    2.19 +  have ih: "finite ((supp r)::name set)" by fact
    2.20 +  let ?g' = "\<lambda>pi a'. f3 a' ((pi@[(c,a')])\<bullet>t) (r (pi@[(c,a')]))"     --"helper function"
    2.21 +  have fact1: "\<forall>pi. finite ((supp (?g' pi))::name set)" using f ih
    2.22 +    by (rule_tac allI, finite_guess add: perm_append supp_prod fs_name1)
    2.23 +  have fact2: "\<forall>pi. \<exists>(a''::name). a''\<sharp>(?g' pi) \<and> a''\<sharp>((?g' pi) a'')" 
    2.24 +  proof 
    2.25 +    fix pi::"name prm"
    2.26 +    show "\<exists>(a''::name). a''\<sharp>(?g' pi) \<and> a''\<sharp>((?g' pi) a'')" using f c ih 
    2.27 +      by (rule_tac f3_freshness_conditions_simple, simp_all add: supp_prod)
    2.28 +  qed
    2.29 +  show ?case using fact1 fact2 ih f by (finite_guess add: fresh_fun_eqvt perm_append supp_prod fs_name1)
    2.30 +qed 
    2.31 +
    2.32  text {* Induction principles *}
    2.33  
    2.34  thm trm.induct_weak --"weak"
     3.1 --- a/src/HOL/Nominal/Examples/Iteration.thy	Wed Apr 26 22:40:46 2006 +0200
     3.2 +++ b/src/HOL/Nominal/Examples/Iteration.thy	Thu Apr 27 01:41:30 2006 +0200
     3.3 @@ -264,7 +264,7 @@
     3.4    and     a: "(t,r) \<in> it f1 f2 f3"
     3.5    shows "(pi\<bullet>t,pi\<bullet>r) \<in> it (pi\<bullet>f1) (pi\<bullet>f2) (pi\<bullet>f3)"
     3.6  using a proof(induct)
     3.7 -  case it1 show ?case by (perm_simp add: it.intros)
     3.8 +  case it1 show ?case by (perm_simp add: it.intros perm_compose')
     3.9  next
    3.10    case it2 thus ?case by (perm_simp add: it.intros)
    3.11  next
    3.12 @@ -375,8 +375,9 @@
    3.13    have fin_g: "finite ((supp ?g)::name set)" 
    3.14      using f by (finite_guess add: itfun'_eqvt[OF f, OF c] supp_prod fs_name1)
    3.15    have fr_g: "\<exists>(a''::name). a''\<sharp>?g \<and> a''\<sharp>(?g a'')" using f c 
    3.16 -    by (rule_tac f3_freshness_conditions_simple, auto simp add: supp_prod, 
    3.17 -        finite_guess add: itfun'_eqvt[OF f, OF c] supp_prod fs_name1)
    3.18 +    apply (rule_tac f3_freshness_conditions_simple, auto simp add: supp_prod, 
    3.19 +           finite_guess add: itfun'_eqvt[OF f, OF c] supp_prod fs_name1)
    3.20 +    done
    3.21    have fresh_b: "b\<sharp>?g" 
    3.22    proof -
    3.23      have "finite ((supp (a,t,f1,f2,f3))::name set)" using f by (simp add: supp_prod fs_name1)
     4.1 --- a/src/HOL/Nominal/Nominal.thy	Wed Apr 26 22:40:46 2006 +0200
     4.2 +++ b/src/HOL/Nominal/Nominal.thy	Thu Apr 27 01:41:30 2006 +0200
     4.3 @@ -17,11 +17,16 @@
     4.4  types 
     4.5    'x prm = "('x \<times> 'x) list"
     4.6  
     4.7 -(* polymorphic operations for permutation and swapping*)
     4.8 +(* polymorphic operations for permutation and swapping *)
     4.9  consts 
    4.10    perm :: "'x prm \<Rightarrow> 'a \<Rightarrow> 'a"     (infixr "\<bullet>" 80)
    4.11    swap :: "('x \<times> 'x) \<Rightarrow> 'x \<Rightarrow> 'x"
    4.12  
    4.13 +(* for the decision procedure involving permutations *)
    4.14 +(* (to make the perm-composition to be terminating   *)
    4.15 +constdefs
    4.16 +  "perm_aux pi x \<equiv> pi\<bullet>x"
    4.17 +
    4.18  (* permutation on sets *)
    4.19  defs (overloaded)
    4.20    perm_set_def:  "pi\<bullet>(X::'a set) \<equiv> {pi\<bullet>a | a. a\<in>X}"
    4.21 @@ -1556,15 +1561,13 @@
    4.22    and      at: "at TYPE ('x)"
    4.23    and      a1: "S supports x"
    4.24    and      a2: "finite S"
    4.25 -  and      a3: "\<forall>S'. (finite S' \<and> S' supports x) \<longrightarrow> S\<subseteq>S'"
    4.26 +  and      a3: "\<forall>S'. (S' supports x) \<longrightarrow> S\<subseteq>S'"
    4.27    shows "S = (supp x)"
    4.28  proof (rule equalityI)
    4.29    show "((supp x)::'x set)\<subseteq>S" using a1 a2 by (rule supp_is_subset)
    4.30  next
    4.31 -  have s1: "((supp x)::'x set) supports x" by (rule supp_supports[OF pt, OF at])
    4.32 -  have "((supp x)::'x set)\<subseteq>S" using a1 a2 by (rule supp_is_subset)
    4.33 -  hence "finite ((supp x)::'x set)" using a2 by (simp add: finite_subset)
    4.34 -  with s1 a3 show "S\<subseteq>supp x" by force
    4.35 +  have "((supp x)::'x set) supports x" by (rule supp_supports[OF pt, OF at])
    4.36 +  with a3 show "S\<subseteq>supp x" by force
    4.37  qed
    4.38  
    4.39  lemma supports_set:
    4.40 @@ -1620,10 +1623,8 @@
    4.41    and     fs: "finite X"
    4.42    shows "(supp X) = X"
    4.43  proof (rule subset_antisym)
    4.44 -  case goal1 
    4.45    show "(supp X) \<subseteq> X" using at_fin_set_supports[OF at] using fs by (simp add: supp_is_subset)
    4.46  next
    4.47 -  case goal2
    4.48    have inf: "infinite (UNIV-X)" using at4[OF at] fs by (auto simp add: Diff_infinite_finite)
    4.49    { fix a::"'x"
    4.50      assume asm: "a\<in>X"
    4.51 @@ -1679,12 +1680,12 @@
    4.52    show "?LHS"
    4.53    proof (rule ccontr)
    4.54      assume "(pi\<bullet>f) \<noteq> f"
    4.55 -    hence "\<exists>c. (pi\<bullet>f) c \<noteq> f c" by (simp add: expand_fun_eq)
    4.56 -    then obtain c where b1: "(pi\<bullet>f) c \<noteq> f c" by force
    4.57 -    from b have "pi\<bullet>(f ((rev pi)\<bullet>c)) = f (pi\<bullet>((rev pi)\<bullet>c))" by force
    4.58 -    hence "(pi\<bullet>f)(pi\<bullet>((rev pi)\<bullet>c)) = f (pi\<bullet>((rev pi)\<bullet>c))" 
    4.59 +    hence "\<exists>x. (pi\<bullet>f) x \<noteq> f x" by (simp add: expand_fun_eq)
    4.60 +    then obtain x where b1: "(pi\<bullet>f) x \<noteq> f x" by force
    4.61 +    from b have "pi\<bullet>(f ((rev pi)\<bullet>x)) = f (pi\<bullet>((rev pi)\<bullet>x))" by force
    4.62 +    hence "(pi\<bullet>f)(pi\<bullet>((rev pi)\<bullet>x)) = f (pi\<bullet>((rev pi)\<bullet>x))" 
    4.63        by (simp add: pt_fun_app_eq[OF pt, OF at])
    4.64 -    hence "(pi\<bullet>f) c = f c" by (simp add: pt_pi_rev[OF pt, OF at])
    4.65 +    hence "(pi\<bullet>f) x = f x" by (simp add: pt_pi_rev[OF pt, OF at])
    4.66      with b1 show "False" by simp
    4.67    qed
    4.68  qed
    4.69 @@ -2056,6 +2057,116 @@
    4.70    shows "a\<sharp>(set xs) = a\<sharp>xs"
    4.71  by (simp add: fresh_def pt_list_set_supp[OF pt, OF at, OF fs])
    4.72   
    4.73 +section {* disjointness properties *}
    4.74 +(*=================================*)
    4.75 +lemma dj_perm_forget:
    4.76 +  fixes pi::"'y prm"
    4.77 +  and   x ::"'x"
    4.78 +  assumes dj: "disjoint TYPE('x) TYPE('y)"
    4.79 +  shows "pi\<bullet>x=x"
    4.80 +  using dj by (simp add: disjoint_def)
    4.81 +
    4.82 +lemma dj_perm_perm_forget:
    4.83 +  fixes pi1::"'x prm"
    4.84 +  and   pi2::"'y prm"
    4.85 +  assumes dj: "disjoint TYPE('x) TYPE('y)"
    4.86 +  shows "pi2\<bullet>pi1=pi1"
    4.87 +  using dj by (induct pi1, auto simp add: disjoint_def)
    4.88 +
    4.89 +lemma dj_cp:
    4.90 +  fixes pi1::"'x prm"
    4.91 +  and   pi2::"'y prm"
    4.92 +  and   x  ::"'a"
    4.93 +  assumes cp: "cp TYPE ('a) TYPE('x) TYPE('y)"
    4.94 +  and     dj: "disjoint TYPE('y) TYPE('x)"
    4.95 +  shows "pi1\<bullet>(pi2\<bullet>x) = (pi2)\<bullet>(pi1\<bullet>x)"
    4.96 +  by (simp add: cp1[OF cp] dj_perm_perm_forget[OF dj])
    4.97 +
    4.98 +lemma dj_supp:
    4.99 +  fixes a::"'x"
   4.100 +  assumes dj: "disjoint TYPE('x) TYPE('y)"
   4.101 +  shows "(supp a) = ({}::'y set)"
   4.102 +apply(simp add: supp_def dj_perm_forget[OF dj])
   4.103 +done
   4.104 +
   4.105 +section {* composition instances *}
   4.106 +(* ============================= *)
   4.107 +
   4.108 +lemma cp_list_inst:
   4.109 +  assumes c1: "cp TYPE ('a) TYPE('x) TYPE('y)"
   4.110 +  shows "cp TYPE ('a list) TYPE('x) TYPE('y)"
   4.111 +using c1
   4.112 +apply(simp add: cp_def)
   4.113 +apply(auto)
   4.114 +apply(induct_tac x)
   4.115 +apply(auto)
   4.116 +done
   4.117 +
   4.118 +lemma cp_set_inst:
   4.119 +  assumes c1: "cp TYPE ('a) TYPE('x) TYPE('y)"
   4.120 +  shows "cp TYPE ('a set) TYPE('x) TYPE('y)"
   4.121 +using c1
   4.122 +apply(simp add: cp_def)
   4.123 +apply(auto)
   4.124 +apply(auto simp add: perm_set_def)
   4.125 +apply(rule_tac x="pi2\<bullet>aa" in exI)
   4.126 +apply(auto)
   4.127 +done
   4.128 +
   4.129 +lemma cp_option_inst:
   4.130 +  assumes c1: "cp TYPE ('a) TYPE('x) TYPE('y)"
   4.131 +  shows "cp TYPE ('a option) TYPE('x) TYPE('y)"
   4.132 +using c1
   4.133 +apply(simp add: cp_def)
   4.134 +apply(auto)
   4.135 +apply(case_tac x)
   4.136 +apply(auto)
   4.137 +done
   4.138 +
   4.139 +lemma cp_noption_inst:
   4.140 +  assumes c1: "cp TYPE ('a) TYPE('x) TYPE('y)"
   4.141 +  shows "cp TYPE ('a noption) TYPE('x) TYPE('y)"
   4.142 +using c1
   4.143 +apply(simp add: cp_def)
   4.144 +apply(auto)
   4.145 +apply(case_tac x)
   4.146 +apply(auto)
   4.147 +done
   4.148 +
   4.149 +lemma cp_unit_inst:
   4.150 +  shows "cp TYPE (unit) TYPE('x) TYPE('y)"
   4.151 +apply(simp add: cp_def)
   4.152 +done
   4.153 +
   4.154 +lemma cp_bool_inst:
   4.155 +  shows "cp TYPE (bool) TYPE('x) TYPE('y)"
   4.156 +apply(simp add: cp_def)
   4.157 +apply(rule allI)+
   4.158 +apply(induct_tac x)
   4.159 +apply(simp_all)
   4.160 +done
   4.161 +
   4.162 +lemma cp_prod_inst:
   4.163 +  assumes c1: "cp TYPE ('a) TYPE('x) TYPE('y)"
   4.164 +  and     c2: "cp TYPE ('b) TYPE('x) TYPE('y)"
   4.165 +  shows "cp TYPE ('a\<times>'b) TYPE('x) TYPE('y)"
   4.166 +using c1 c2
   4.167 +apply(simp add: cp_def)
   4.168 +done
   4.169 +
   4.170 +lemma cp_fun_inst:
   4.171 +  assumes c1: "cp TYPE ('a) TYPE('x) TYPE('y)"
   4.172 +  and     c2: "cp TYPE ('b) TYPE('x) TYPE('y)"
   4.173 +  and     pt: "pt TYPE ('y) TYPE('x)"
   4.174 +  and     at: "at TYPE ('x)"
   4.175 +  shows "cp TYPE ('a\<Rightarrow>'b) TYPE('x) TYPE('y)"
   4.176 +using c1 c2
   4.177 +apply(auto simp add: cp_def perm_fun_def expand_fun_eq)
   4.178 +apply(simp add: perm_rev[symmetric])
   4.179 +apply(simp add: pt_rev_pi[OF pt_list_inst[OF pt_prod_inst[OF pt, OF pt]], OF at])
   4.180 +done
   4.181 +
   4.182 +
   4.183  section {* Andy's freshness lemma *}
   4.184  (*================================*)
   4.185  
   4.186 @@ -2149,6 +2260,47 @@
   4.187    with b show "fr = h a" by force
   4.188  qed
   4.189  
   4.190 +lemma fresh_fun_equiv_ineq:
   4.191 +  fixes h :: "'y\<Rightarrow>'a"
   4.192 +  and   pi:: "'x prm"
   4.193 +  assumes pta: "pt TYPE('a) TYPE('x)"
   4.194 +  and     ptb: "pt TYPE('y) TYPE('x)"
   4.195 +  and     ptb':"pt TYPE('a) TYPE('y)"
   4.196 +  and     at:  "at TYPE('x)" 
   4.197 +  and     at': "at TYPE('y)"
   4.198 +  and     cpa: "cp TYPE('a) TYPE('x) TYPE('y)"
   4.199 +  and     cpb: "cp TYPE('y) TYPE('x) TYPE('y)"
   4.200 +  and     f1: "finite ((supp h)::'y set)"
   4.201 +  and     a1: "\<exists>(a::'y). (a\<sharp>h \<and> a\<sharp>(h a))"
   4.202 +  shows "pi\<bullet>(fresh_fun h) = fresh_fun(pi\<bullet>h)" (is "?LHS = ?RHS")
   4.203 +proof -
   4.204 +  have ptd: "pt TYPE('y) TYPE('y)" by (simp add: at_pt_inst[OF at']) 
   4.205 +  have ptc: "pt TYPE('y\<Rightarrow>'a) TYPE('x)" by (simp add: pt_fun_inst[OF ptb, OF pta, OF at]) 
   4.206 +  have cpc: "cp TYPE('y\<Rightarrow>'a) TYPE ('x) TYPE ('y)" by (rule cp_fun_inst[OF cpb,OF cpa])
   4.207 +  have f2: "finite ((supp (pi\<bullet>h))::'y set)"
   4.208 +  proof -
   4.209 +    from f1 have "finite (pi\<bullet>((supp h)::'y set))"
   4.210 +      by (simp add: pt_set_finite_ineq[OF ptb, OF at])
   4.211 +    thus ?thesis
   4.212 +      by (simp add: pt_perm_supp_ineq[OF ptc, OF ptb, OF at, OF cpc])
   4.213 +  qed
   4.214 +  from a1 obtain a' where c0: "a'\<sharp>h \<and> a'\<sharp>(h a')" by force
   4.215 +  hence c1: "a'\<sharp>h" and c2: "a'\<sharp>(h a')" by simp_all
   4.216 +  have c3: "(pi\<bullet>a')\<sharp>(pi\<bullet>h)" using c1
   4.217 +  by (simp add: pt_fresh_bij_ineq[OF ptc, OF ptb, OF at, OF cpc])
   4.218 +  have c4: "(pi\<bullet>a')\<sharp>(pi\<bullet>h) (pi\<bullet>a')"
   4.219 +  proof -
   4.220 +    from c2 have "(pi\<bullet>a')\<sharp>(pi\<bullet>(h a'))"
   4.221 +      by (simp add: pt_fresh_bij_ineq[OF pta, OF ptb, OF at,OF cpa])
   4.222 +    thus ?thesis by (simp add: pt_fun_app_eq[OF ptb, OF at])
   4.223 +  qed
   4.224 +  have a2: "\<exists>(a::'y). (a\<sharp>(pi\<bullet>h) \<and> a\<sharp>((pi\<bullet>h) a))" using c3 c4 by force
   4.225 +  have d1: "?LHS = pi\<bullet>(h a')" using c1 a1 by (simp add: fresh_fun_app[OF ptb', OF at', OF f1])
   4.226 +  have d2: "?RHS = (pi\<bullet>h) (pi\<bullet>a')" using c3 a2 
   4.227 +    by (simp add: fresh_fun_app[OF ptb', OF at', OF f2])
   4.228 +  show ?thesis using d1 d2 by (simp add: pt_fun_app_eq[OF ptb, OF at])
   4.229 +qed
   4.230 +
   4.231  lemma fresh_fun_equiv:
   4.232    fixes h :: "'x\<Rightarrow>'a"
   4.233    and   pi:: "'x prm"
   4.234 @@ -2192,117 +2344,6 @@
   4.235    apply(simp add: pt_fresh_fresh[OF pt_fun_inst[OF at_pt_inst[OF at], OF pt], OF at, OF at])
   4.236    done
   4.237    
   4.238 -section {* disjointness properties *}
   4.239 -(*=================================*)
   4.240 -lemma dj_perm_forget:
   4.241 -  fixes pi::"'y prm"
   4.242 -  and   x ::"'x"
   4.243 -  assumes dj: "disjoint TYPE('x) TYPE('y)"
   4.244 -  shows "pi\<bullet>x=x"
   4.245 -  using dj by (simp add: disjoint_def)
   4.246 -
   4.247 -lemma dj_perm_perm_forget:
   4.248 -  fixes pi1::"'x prm"
   4.249 -  and   pi2::"'y prm"
   4.250 -  assumes dj: "disjoint TYPE('x) TYPE('y)"
   4.251 -  shows "pi2\<bullet>pi1=pi1"
   4.252 -  using dj by (induct pi1, auto simp add: disjoint_def)
   4.253 -
   4.254 -lemma dj_cp:
   4.255 -  fixes pi1::"'x prm"
   4.256 -  and   pi2::"'y prm"
   4.257 -  and   x  ::"'a"
   4.258 -  assumes cp: "cp TYPE ('a) TYPE('x) TYPE('y)"
   4.259 -  and     dj: "disjoint TYPE('y) TYPE('x)"
   4.260 -  shows "pi1\<bullet>(pi2\<bullet>x) = (pi2)\<bullet>(pi1\<bullet>x)"
   4.261 -  by (simp add: cp1[OF cp] dj_perm_perm_forget[OF dj])
   4.262 -
   4.263 -lemma dj_supp:
   4.264 -  fixes a::"'x"
   4.265 -  assumes dj: "disjoint TYPE('x) TYPE('y)"
   4.266 -  shows "(supp a) = ({}::'y set)"
   4.267 -apply(simp add: supp_def dj_perm_forget[OF dj])
   4.268 -done
   4.269 -
   4.270 -
   4.271 -section {* composition instances *}
   4.272 -(* ============================= *)
   4.273 -
   4.274 -lemma cp_list_inst:
   4.275 -  assumes c1: "cp TYPE ('a) TYPE('x) TYPE('y)"
   4.276 -  shows "cp TYPE ('a list) TYPE('x) TYPE('y)"
   4.277 -using c1
   4.278 -apply(simp add: cp_def)
   4.279 -apply(auto)
   4.280 -apply(induct_tac x)
   4.281 -apply(auto)
   4.282 -done
   4.283 -
   4.284 -lemma cp_set_inst:
   4.285 -  assumes c1: "cp TYPE ('a) TYPE('x) TYPE('y)"
   4.286 -  shows "cp TYPE ('a set) TYPE('x) TYPE('y)"
   4.287 -using c1
   4.288 -apply(simp add: cp_def)
   4.289 -apply(auto)
   4.290 -apply(auto simp add: perm_set_def)
   4.291 -apply(rule_tac x="pi2\<bullet>aa" in exI)
   4.292 -apply(auto)
   4.293 -done
   4.294 -
   4.295 -lemma cp_option_inst:
   4.296 -  assumes c1: "cp TYPE ('a) TYPE('x) TYPE('y)"
   4.297 -  shows "cp TYPE ('a option) TYPE('x) TYPE('y)"
   4.298 -using c1
   4.299 -apply(simp add: cp_def)
   4.300 -apply(auto)
   4.301 -apply(case_tac x)
   4.302 -apply(auto)
   4.303 -done
   4.304 -
   4.305 -lemma cp_noption_inst:
   4.306 -  assumes c1: "cp TYPE ('a) TYPE('x) TYPE('y)"
   4.307 -  shows "cp TYPE ('a noption) TYPE('x) TYPE('y)"
   4.308 -using c1
   4.309 -apply(simp add: cp_def)
   4.310 -apply(auto)
   4.311 -apply(case_tac x)
   4.312 -apply(auto)
   4.313 -done
   4.314 -
   4.315 -lemma cp_unit_inst:
   4.316 -  shows "cp TYPE (unit) TYPE('x) TYPE('y)"
   4.317 -apply(simp add: cp_def)
   4.318 -done
   4.319 -
   4.320 -lemma cp_bool_inst:
   4.321 -  shows "cp TYPE (bool) TYPE('x) TYPE('y)"
   4.322 -apply(simp add: cp_def)
   4.323 -apply(rule allI)+
   4.324 -apply(induct_tac x)
   4.325 -apply(simp_all)
   4.326 -done
   4.327 -
   4.328 -lemma cp_prod_inst:
   4.329 -  assumes c1: "cp TYPE ('a) TYPE('x) TYPE('y)"
   4.330 -  and     c2: "cp TYPE ('b) TYPE('x) TYPE('y)"
   4.331 -  shows "cp TYPE ('a\<times>'b) TYPE('x) TYPE('y)"
   4.332 -using c1 c2
   4.333 -apply(simp add: cp_def)
   4.334 -done
   4.335 -
   4.336 -lemma cp_fun_inst:
   4.337 -  assumes c1: "cp TYPE ('a) TYPE('x) TYPE('y)"
   4.338 -  and     c2: "cp TYPE ('b) TYPE('x) TYPE('y)"
   4.339 -  and     pt: "pt TYPE ('y) TYPE('x)"
   4.340 -  and     at: "at TYPE ('x)"
   4.341 -  shows "cp TYPE ('a\<Rightarrow>'b) TYPE('x) TYPE('y)"
   4.342 -using c1 c2
   4.343 -apply(auto simp add: cp_def perm_fun_def expand_fun_eq)
   4.344 -apply(simp add: perm_rev[symmetric])
   4.345 -apply(simp add: pt_rev_pi[OF pt_list_inst[OF pt_prod_inst[OF pt, OF pt]], OF at])
   4.346 -done
   4.347 -
   4.348 -
   4.349  section {* Abstraction function *}
   4.350  (*==============================*)
   4.351  
   4.352 @@ -2680,6 +2721,30 @@
   4.353  section {* lemmas for deciding permutation equations *}
   4.354  (*===================================================*)
   4.355  
   4.356 +lemma perm_aux_fold:
   4.357 +  shows "perm_aux pi x = pi\<bullet>x" by (simp only: perm_aux_def)
   4.358 +
   4.359 +lemma pt_perm_compose_aux:
   4.360 +  fixes pi1 :: "'x prm"
   4.361 +  and   pi2 :: "'x prm"
   4.362 +  and   x  :: "'a"
   4.363 +  assumes pt: "pt TYPE('a) TYPE('x)"
   4.364 +  and     at: "at TYPE('x)"
   4.365 +  shows "pi2\<bullet>(pi1\<bullet>x) = perm_aux (pi2\<bullet>pi1) (pi2\<bullet>x)" 
   4.366 +proof -
   4.367 +  have "(pi2@pi1) \<triangleq> ((pi2\<bullet>pi1)@pi2)" by (rule at_ds8)
   4.368 +  hence "(pi2@pi1)\<bullet>x = ((pi2\<bullet>pi1)@pi2)\<bullet>x" by (rule pt3[OF pt])
   4.369 +  thus ?thesis by (simp add: pt2[OF pt] perm_aux_def)
   4.370 +qed  
   4.371 +
   4.372 +lemma cp1_aux:
   4.373 +  fixes pi1::"'x prm"
   4.374 +  and   pi2::"'y prm"
   4.375 +  and   x  ::"'a"
   4.376 +  assumes cp: "cp TYPE ('a) TYPE('x) TYPE('y)"
   4.377 +  shows "pi1\<bullet>(pi2\<bullet>x) = perm_aux (pi1\<bullet>pi2) (pi1\<bullet>x)"
   4.378 +  using cp by (simp add: cp_def perm_aux_def)
   4.379 +
   4.380  lemma perm_eq_app:
   4.381    fixes f  :: "'a\<Rightarrow>'b"
   4.382    and   x  :: "'a"
   4.383 @@ -2696,7 +2761,6 @@
   4.384    shows "((pi\<bullet>(\<lambda>x. f x))=y) = ((\<lambda>x. (pi\<bullet>(f ((rev pi)\<bullet>x))))=y)"
   4.385    by (simp add: perm_fun_def)
   4.386  
   4.387 -
   4.388  section {* test *}
   4.389  lemma at_prm_eq_compose:
   4.390    fixes pi1 :: "'x prm"
   4.391 @@ -2745,10 +2809,18 @@
   4.392  
   4.393  method_setup perm_simp =
   4.394    {* perm_eq_meth *}
   4.395 -  {* tactic for deciding equalities involving permutations *}
   4.396 +  {* simp rules and simprocs for analysing permutations *}
   4.397  
   4.398  method_setup perm_simp_debug =
   4.399    {* perm_eq_meth_debug *}
   4.400 +  {* simp rules and simprocs for analysing permutations including debuging facilities *}
   4.401 +
   4.402 +method_setup perm_full_simp =
   4.403 +  {* perm_full_eq_meth *}
   4.404 +  {* tactic for deciding equalities involving permutations *}
   4.405 +
   4.406 +method_setup perm_full_simp_debug =
   4.407 +  {* perm_full_eq_meth_debug *}
   4.408    {* tactic for deciding equalities involving permutations including debuging facilities *}
   4.409  
   4.410  method_setup supports_simp =
     5.1 --- a/src/HOL/Nominal/nominal_atoms.ML	Wed Apr 26 22:40:46 2006 +0200
     5.2 +++ b/src/HOL/Nominal/nominal_atoms.ML	Thu Apr 27 01:41:30 2006 +0200
     5.3 @@ -520,6 +520,7 @@
     5.4         val cp_option_inst  = thm "cp_option_inst";
     5.5         val cp_noption_inst = thm "cp_noption_inst";
     5.6         val pt_perm_compose = thm "pt_perm_compose";
     5.7 +       
     5.8         val dj_pp_forget    = thm "dj_perm_perm_forget";
     5.9  
    5.10         (* shows that <aj> is an instance of cp_<ak>_<ai>  *)
    5.11 @@ -645,32 +646,32 @@
    5.12  
    5.13         (* abbreviations for some lemmas *)
    5.14         (*===============================*)
    5.15 -       val abs_fun_pi        = thm "nominal.abs_fun_pi";
    5.16 -       val abs_fun_pi_ineq   = thm "nominal.abs_fun_pi_ineq";
    5.17 -       val abs_fun_eq        = thm "nominal.abs_fun_eq";
    5.18 -       val dj_perm_forget    = thm "nominal.dj_perm_forget";
    5.19 -       val dj_pp_forget      = thm "nominal.dj_perm_perm_forget";
    5.20 -       val fresh_iff         = thm "nominal.fresh_abs_fun_iff";
    5.21 -       val fresh_iff_ineq    = thm "nominal.fresh_abs_fun_iff_ineq";
    5.22 -       val abs_fun_supp      = thm "nominal.abs_fun_supp";
    5.23 -       val abs_fun_supp_ineq = thm "nominal.abs_fun_supp_ineq";
    5.24 -       val pt_swap_bij       = thm "nominal.pt_swap_bij";
    5.25 -       val pt_fresh_fresh    = thm "nominal.pt_fresh_fresh";
    5.26 -       val pt_bij            = thm "nominal.pt_bij";
    5.27 -       val pt_perm_compose   = thm "nominal.pt_perm_compose";
    5.28 -       val pt_perm_compose'  = thm "nominal.pt_perm_compose'";
    5.29 -       val perm_app          = thm "nominal.pt_fun_app_eq";
    5.30 -       val at_fresh          = thm "nominal.at_fresh";
    5.31 -       val at_calc           = thms "nominal.at_calc";
    5.32 -       val at_supp           = thm "nominal.at_supp";
    5.33 -       val dj_supp           = thm "nominal.dj_supp";
    5.34 -       val fresh_left_ineq   = thm "nominal.pt_fresh_left_ineq";
    5.35 -       val fresh_left        = thm "nominal.pt_fresh_left";
    5.36 -       val fresh_bij_ineq    = thm "nominal.pt_fresh_bij_ineq";
    5.37 -       val fresh_bij         = thm "nominal.pt_fresh_bij";
    5.38 -       val pt_pi_rev         = thm "nominal.pt_pi_rev";
    5.39 -       val pt_rev_pi         = thm "nominal.pt_rev_pi";
    5.40 -       val fresh_fun_eqvt    = thm "nominal.fresh_fun_equiv";
    5.41 +       val abs_fun_pi          = thm "nominal.abs_fun_pi";
    5.42 +       val abs_fun_pi_ineq     = thm "nominal.abs_fun_pi_ineq";
    5.43 +       val abs_fun_eq          = thm "nominal.abs_fun_eq";
    5.44 +       val dj_perm_forget      = thm "nominal.dj_perm_forget";
    5.45 +       val dj_pp_forget        = thm "nominal.dj_perm_perm_forget";
    5.46 +       val fresh_iff           = thm "nominal.fresh_abs_fun_iff";
    5.47 +       val fresh_iff_ineq      = thm "nominal.fresh_abs_fun_iff_ineq";
    5.48 +       val abs_fun_supp        = thm "nominal.abs_fun_supp";
    5.49 +       val abs_fun_supp_ineq   = thm "nominal.abs_fun_supp_ineq";
    5.50 +       val pt_swap_bij         = thm "nominal.pt_swap_bij";
    5.51 +       val pt_fresh_fresh      = thm "nominal.pt_fresh_fresh";
    5.52 +       val pt_bij              = thm "nominal.pt_bij";
    5.53 +       val pt_perm_compose     = thm "nominal.pt_perm_compose";
    5.54 +       val pt_perm_compose'    = thm "nominal.pt_perm_compose'";
    5.55 +       val perm_app            = thm "nominal.pt_fun_app_eq";
    5.56 +       val at_fresh            = thm "nominal.at_fresh";
    5.57 +       val at_calc             = thms "nominal.at_calc";
    5.58 +       val at_supp             = thm "nominal.at_supp";
    5.59 +       val dj_supp             = thm "nominal.dj_supp";
    5.60 +       val fresh_left_ineq     = thm "nominal.pt_fresh_left_ineq";
    5.61 +       val fresh_left          = thm "nominal.pt_fresh_left";
    5.62 +       val fresh_bij_ineq      = thm "nominal.pt_fresh_bij_ineq";
    5.63 +       val fresh_bij           = thm "nominal.pt_fresh_bij";
    5.64 +       val pt_pi_rev           = thm "nominal.pt_pi_rev";
    5.65 +       val pt_rev_pi           = thm "nominal.pt_rev_pi";
    5.66 +       val fresh_fun_eqvt      = thm "nominal.fresh_fun_equiv";
    5.67  
    5.68         (* Now we collect and instantiate some lemmas w.r.t. all atom      *)
    5.69         (* types; this allows for example to use abs_perm (which is a      *)
     6.1 --- a/src/HOL/Nominal/nominal_permeq.ML	Wed Apr 26 22:40:46 2006 +0200
     6.2 +++ b/src/HOL/Nominal/nominal_permeq.ML	Thu Apr 27 01:41:30 2006 +0200
     6.3 @@ -1,22 +1,23 @@
     6.4  (* $Id$ *)
     6.5  
     6.6 -(* METHOD FOR ANALYSING EQUATION INVOLVING PERMUTATION *)
     6.7 +(* METHODS FOR SIMPLIFYING PERMUTATIONS AND     *)
     6.8 +(* FOR ANALYSING EQUATION INVOLVING PERMUTATION *)
     6.9  
    6.10  local
    6.11  
    6.12  (* pulls out dynamically a thm via the simpset *)
    6.13 -fun dynamic_thms ss name = 
    6.14 -    ProofContext.get_thms (Simplifier.the_context ss) (Name name);
    6.15 -fun dynamic_thm ss name = 
    6.16 -    ProofContext.get_thm (Simplifier.the_context ss) (Name name);
    6.17 +fun dynamic_thms ss name = ProofContext.get_thms (Simplifier.the_context ss) (Name name);
    6.18 +fun dynamic_thm ss name = ProofContext.get_thm (Simplifier.the_context ss) (Name name);
    6.19  
    6.20 -(* initial simplification step in the tactic *)
    6.21 +(* a tactic simplyfying permutations *)
    6.22 +val perm_fun_def = thm "nominal.perm_fun_def"
    6.23 +val perm_eq_app = thm "nominal.pt_fun_app_eq"
    6.24 +
    6.25  fun perm_eval_tac ss i =
    6.26      let
    6.27          fun perm_eval_simproc sg ss redex =
    6.28          let 
    6.29 -	   
    6.30 -           (* the "application" case below is only applicable when the head   *)
    6.31 +	   (* the "application" case below is only applicable when the head   *)
    6.32             (* of f is not a constant  or when it is a permuattion with two or *) 
    6.33             (* more arguments                                                  *)
    6.34             fun applicable t = 
    6.35 @@ -38,14 +39,10 @@
    6.36  		    val name = Sign.base_name n
    6.37  		    val at_inst     = dynamic_thm ss ("at_"^name^"_inst")
    6.38  		    val pt_inst     = dynamic_thm ss ("pt_"^name^"_inst")  
    6.39 -		    val perm_eq_app = thm "nominal.pt_fun_app_eq"	  
    6.40  		in SOME ((at_inst RS (pt_inst RS perm_eq_app)) RS eq_reflection) end)
    6.41  
    6.42          (* case pi o (%x. f x) == (%x. pi o (f ((rev pi)o x))) *)
    6.43 -        | (Const("nominal.perm",_) $ pi $ (Abs _)) => 
    6.44 -           let 
    6.45 -               val perm_fun_def = thm "nominal.perm_fun_def"
    6.46 -           in SOME (perm_fun_def) end
    6.47 +        | (Const("nominal.perm",_) $ pi $ (Abs _)) => SOME (perm_fun_def)
    6.48  
    6.49          (* no redex otherwise *) 
    6.50          | _ => NONE) end
    6.51 @@ -54,112 +51,137 @@
    6.52  	    Simplifier.simproc (Theory.sign_of (the_context ())) "perm_eval" 
    6.53  	    ["nominal.perm pi x"] perm_eval_simproc;
    6.54  
    6.55 -      (* applies the pt_perm_compose lemma              *)
    6.56 -      (*                                                *)
    6.57 -      (*     pi1 o (pi2 o x) = (pi1 o pi2) o (pi1 o x)  *)
    6.58 -      (*                                                *)
    6.59 -      (* in the restricted case where pi1 is a swapping *)
    6.60 -      (* (a b) coming from a "supports problem"; in     *)
    6.61 -      (* this rule would cause loops in the simplifier  *) 
    6.62 -      val pt_perm_compose = thm "pt_perm_compose";
    6.63 -	  
    6.64 -      fun perm_compose_simproc i sg ss redex =
    6.65 -      (case redex of
    6.66 -        (Const ("nominal.perm", _) $ (pi1 as Const ("List.list.Cons", _) $
    6.67 -         (Const ("Pair", _) $ Free (a as (_, T as Type (tname, _))) $ Free b) $ 
    6.68 -           Const ("List.list.Nil", _)) $ (Const ("nominal.perm", 
    6.69 -            Type ("fun", [Type ("List.list", [Type ("*", [U, _])]), _])) $ pi2 $ t)) =>
    6.70 +      (* these lemmas are created dynamically according to the atom types *) 
    6.71 +      val perm_swap        = dynamic_thms ss "perm_swap"
    6.72 +      val perm_fresh       = dynamic_thms ss "perm_fresh_fresh"
    6.73 +      val perm_bij         = dynamic_thms ss "perm_bij"
    6.74 +      val perm_pi_simp     = dynamic_thms ss "perm_pi_simp"
    6.75 +      val ss' = ss addsimps (perm_swap@perm_fresh@perm_bij@perm_pi_simp)
    6.76 +    in
    6.77 +	("general simplification step", asm_full_simp_tac (ss' addsimprocs [perm_eval]) i)
    6.78 +    end;
    6.79 +
    6.80 +(* applies the perm_compose rule such that                             *)
    6.81 +(*                                                                     *)
    6.82 +(*   pi o (pi' o lhs) = rhs                                            *)
    6.83 +(*                                                                     *)
    6.84 +(* is transformed to                                                   *) 
    6.85 +(*                                                                     *)
    6.86 +(*  (pi o pi') o (pi' o lhs) = rhs                                     *)
    6.87 +(*                                                                     *)
    6.88 +(* this rule would loop in the simplifier, so some trick is used with  *)
    6.89 +(* generating perm_aux'es for the outermost permutation and then un-   *)
    6.90 +(* folding the definition                                              *)
    6.91 +val pt_perm_compose_aux = thm "pt_perm_compose_aux";
    6.92 +val cp1_aux             = thm "cp1_aux";
    6.93 +val perm_aux_fold       = thm "perm_aux_fold"; 
    6.94 +
    6.95 +fun perm_compose_tac ss i = 
    6.96 +    let
    6.97 +	fun perm_compose_simproc sg ss redex =
    6.98 +	(case redex of
    6.99 +           (Const ("nominal.perm", Type ("fun", [Type ("List.list", 
   6.100 +             [Type ("*", [T as Type (tname,_),_])]),_])) $ pi1 $ (Const ("nominal.perm", 
   6.101 +               Type ("fun", [Type ("List.list", [Type ("*", [U as Type (uname,_),_])]),_])) $ 
   6.102 +                pi2 $ t)) =>
   6.103          let
   6.104 -            val ({bounds = (_, xs), ...}, _) = rep_ss ss
   6.105 -            val ai = find_index (fn (x, _) => x = a) xs
   6.106 -	    val bi = find_index (fn (x, _) => x = b) xs
   6.107  	    val tname' = Sign.base_name tname
   6.108 +            val uname' = Sign.base_name uname
   6.109          in
   6.110 -            if ai = length xs - i - 1 andalso 
   6.111 -               bi = length xs - i - 2 andalso 
   6.112 -               T = U andalso pi1 <> pi2 then
   6.113 +            if pi1 <> pi2 then  (* only apply the composition rule in this case *)
   6.114 +               if T = U then    
   6.115                  SOME (Drule.instantiate'
   6.116  	              [SOME (ctyp_of sg (fastype_of t))]
   6.117  		      [SOME (cterm_of sg pi1), SOME (cterm_of sg pi2), SOME (cterm_of sg t)]
   6.118  		      (mk_meta_eq ([PureThy.get_thm sg (Name ("pt_"^tname'^"_inst")),
   6.119 -	               PureThy.get_thm sg (Name ("at_"^tname'^"_inst"))] MRS pt_perm_compose)))
   6.120 +	               PureThy.get_thm sg (Name ("at_"^tname'^"_inst"))] MRS pt_perm_compose_aux)))
   6.121 +               else
   6.122 +                SOME (Drule.instantiate'
   6.123 +	              [SOME (ctyp_of sg (fastype_of t))]
   6.124 +		      [SOME (cterm_of sg pi1), SOME (cterm_of sg pi2), SOME (cterm_of sg t)]
   6.125 +		      (mk_meta_eq (PureThy.get_thm sg (Name ("cp_"^tname'^"_"^uname'^"_inst")) RS 
   6.126 +                       cp1_aux)))
   6.127              else NONE
   6.128          end
   6.129         | _ => NONE);
   6.130 -
   6.131 -      fun perm_compose i =
   6.132 +	  
   6.133 +      val perm_compose  =
   6.134  	Simplifier.simproc (the_context()) "perm_compose" 
   6.135 -	["nominal.perm [(a, b)] (nominal.perm pi t)"] (perm_compose_simproc i);
   6.136 -         
   6.137 -      (* these lemmas are created dynamically according to the atom types *) 
   6.138 -      val perm_swap     = dynamic_thms ss "perm_swap"
   6.139 -      val perm_fresh    = dynamic_thms ss "perm_fresh_fresh"
   6.140 -      val perm_bij      = dynamic_thms ss "perm_bij"
   6.141 -      val perm_pi_simp  = dynamic_thms ss "perm_pi_simp"
   6.142 -      val ss' = ss addsimps (perm_swap@perm_fresh@perm_bij@perm_pi_simp)
   6.143 +	["nominal.perm pi1 (nominal.perm pi2 t)"] perm_compose_simproc;
   6.144 +
   6.145 +      val ss' = Simplifier.theory_context (the_context ()) empty_ss	  
   6.146 +
   6.147      in
   6.148 -      ("general simplification step", 
   6.149 -        FIRST [rtac conjI i, 
   6.150 -               SUBGOAL (fn (g, i) => asm_full_simp_tac 
   6.151 -                 (ss' addsimprocs [perm_eval,perm_compose (length (Logic.strip_params g)-2)]) i) i])
   6.152 -    end;
   6.153 -
   6.154 -(* applies the perm_compose rule - this rule would loop in the simplifier     *)
   6.155 -(* in case there are more atom-types we have to check every possible instance *)
   6.156 -(* of perm_compose                                                            *)
   6.157 -fun apply_perm_compose_tac ss i = 
   6.158 -    let
   6.159 -	val perm_compose = dynamic_thms ss "perm_compose"; 
   6.160 -        val tacs = map (fn thm => (rtac (thm RS trans) i)) perm_compose
   6.161 -    in
   6.162 -	("analysing permutation compositions on the lhs",FIRST (tacs))
   6.163 +	("analysing permutation compositions on the lhs",
   6.164 +         EVERY [rtac trans i,
   6.165 +                asm_full_simp_tac (ss' addsimprocs [perm_compose]) i,
   6.166 +                asm_full_simp_tac (HOL_basic_ss addsimps [perm_aux_fold]) i])
   6.167      end
   6.168  
   6.169  (* applying Stefan's smart congruence tac *)
   6.170  fun apply_cong_tac i = 
   6.171      ("application of congruence",
   6.172 -     (fn st => DatatypeAux.cong_tac  i st handle Subscript => no_tac st));
   6.173 +     (fn st => DatatypeAux.cong_tac i st handle Subscript => no_tac st));
   6.174  
   6.175 -(* unfolds the definition of permutations applied to functions *)
   6.176 +(* unfolds the definition of permutations     *)
   6.177 +(* applied to functions such that             *)
   6.178 +(*                                            *)
   6.179 +(*   pi o f = rhs                             *)  
   6.180 +(*                                            *)
   6.181 +(* is transformed to                          *)
   6.182 +(*                                            *)
   6.183 +(*   %x. pi o (f ((rev pi) o x)) = rhs        *)
   6.184  fun unfold_perm_fun_def_tac i = 
   6.185      let
   6.186  	val perm_fun_def = thm "nominal.perm_fun_def"
   6.187      in
   6.188  	("unfolding of permutations on functions", 
   6.189 -	 simp_tac (HOL_basic_ss addsimps [perm_fun_def]) i)
   6.190 +         rtac (perm_fun_def RS meta_eq_to_obj_eq RS trans) i)
   6.191      end
   6.192  
   6.193 -(* applies the expand_fun_eq rule to the first goal and strips off all universal quantifiers *)
   6.194 -fun expand_fun_eq_tac i =    
   6.195 -    ("extensionality expansion of functions",
   6.196 -    EVERY [simp_tac (HOL_basic_ss addsimps [expand_fun_eq]) i, REPEAT_DETERM (rtac allI i)]);
   6.197 +(* applies the ext-rule such that      *)
   6.198 +(*                                     *)
   6.199 +(*    f = g    goes to /\x. f x = g x  *)
   6.200 +fun ext_fun_tac i = ("extensionality expansion of functions", rtac ext i);
   6.201  
   6.202 +(* FIXME FIXME FIXME *)
   6.203 +(* should be able to analyse pi o fresh_fun () = fresh_fun instances *) 
   6.204 +fun fresh_fun_eqvt_tac i =
   6.205 +    let
   6.206 +	val fresh_fun_equiv = thm "nominal.fresh_fun_equiv_ineq"
   6.207 +    in
   6.208 +	("fresh_fun equivariance", rtac (fresh_fun_equiv RS trans) i)
   6.209 +    end		       
   6.210 +		       
   6.211  (* debugging *)
   6.212  fun DEBUG_tac (msg,tac) = 
   6.213      CHANGED (EVERY [tac, print_tac ("after "^msg)]); 
   6.214  fun NO_DEBUG_tac (_,tac) = CHANGED tac; 
   6.215  
   6.216 -(* Main Tactic *)
   6.217 -
   6.218 +(* Main Tactics *)
   6.219  fun perm_simp_tac tactical ss i = 
   6.220      DETERM (tactical (perm_eval_tac ss i));
   6.221  
   6.222 +(* perm_full_simp_tac is perm_simp_tac plus additional tactics    *)
   6.223 +(* to decide equation that come from support problems             *)
   6.224 +(* since it contains looping rules the "recursion" - depth is set *)
   6.225 +(* to 10 - this seems to be sufficient in most cases              *)
   6.226 +fun perm_full_simp_tac tactical ss =
   6.227 +  let fun perm_full_simp_tac_aux tactical ss n = 
   6.228 +	  if n=0 then K all_tac
   6.229 +	  else DETERM o 
   6.230 +	       (FIRST'[fn i => tactical ("splitting conjunctions on the rhs", rtac conjI i),
   6.231 +                       fn i => tactical (perm_eval_tac ss i),
   6.232 +		       fn i => tactical (perm_compose_tac ss i),
   6.233 +		       fn i => tactical (apply_cong_tac i), 
   6.234 +                       fn i => tactical (unfold_perm_fun_def_tac i),
   6.235 +                       fn i => tactical (ext_fun_tac i), 
   6.236 +                       fn i => tactical (fresh_fun_eqvt_tac i)]
   6.237 +		      THEN_ALL_NEW (TRY o (perm_full_simp_tac_aux tactical ss (n-1))))
   6.238 +  in perm_full_simp_tac_aux tactical ss 10 end;
   6.239  
   6.240 -(* perm_simp_tac plus additional tactics to decide            *)
   6.241 -(* support problems                                           *)
   6.242 -(* the "recursion"-depth is set to 10 - this seems sufficient *)
   6.243 -fun perm_supports_tac tactical ss n = 
   6.244 -    if n=0 then K all_tac
   6.245 -    else DETERM o 
   6.246 -         (FIRST'[fn i => tactical (perm_eval_tac ss i),
   6.247 -                 (*fn i => tactical (apply_perm_compose_tac ss i),*)
   6.248 -		 fn i => tactical (apply_cong_tac i), 
   6.249 -                 fn i => tactical (unfold_perm_fun_def_tac i),
   6.250 -		 fn i => tactical (expand_fun_eq_tac i)]
   6.251 -         THEN_ALL_NEW (TRY o (perm_supports_tac tactical ss (n-1))));
   6.252 -
   6.253 -(* tactic that first unfolds the support definition          *)
   6.254 -(* and strips off the intros, then applies perm_supports_tac *)
   6.255 +(* tactic that first unfolds the support definition           *)
   6.256 +(* and strips off the intros, then applies perm_full_simp_tac *)
   6.257  fun supports_tac tactical ss i =
   6.258    let 
   6.259        val supports_def = thm "nominal.op supports_def";
   6.260 @@ -167,16 +189,19 @@
   6.261        val fresh_prod   = thm "nominal.fresh_prod";
   6.262        val simps        = [supports_def,symmetric fresh_def,fresh_prod]
   6.263    in
   6.264 -      EVERY [tactical ("unfolding of supports ", simp_tac (HOL_basic_ss addsimps simps) i),
   6.265 -             tactical ("stripping of foralls  ", REPEAT_DETERM (rtac allI i)),
   6.266 -             tactical ("geting rid of the imps", rtac impI i),
   6.267 -             tactical ("eliminating conjuncts ", REPEAT_DETERM (etac  conjE i)),
   6.268 -             tactical ("applying perm_simp    ", perm_supports_tac tactical ss 10 i)]
   6.269 +      EVERY [tactical ("unfolding of supports   ", simp_tac (HOL_basic_ss addsimps simps) i),
   6.270 +             tactical ("stripping of foralls    ", REPEAT_DETERM (rtac allI i)),
   6.271 +             tactical ("geting rid of the imps  ", rtac impI i),
   6.272 +             tactical ("eliminating conjuncts   ", REPEAT_DETERM (etac  conjE i)),
   6.273 +             tactical ("applying perm_full_simp ", perm_full_simp_tac tactical ss i
   6.274 +                                                   (*perm_simp_tac tactical ss i*))]
   6.275    end;
   6.276  
   6.277  
   6.278 -(* tactic that guesses the finite-support of a goal *)
   6.279 -
   6.280 +(* tactic that guesses the finite-support of a goal       *)
   6.281 +(* it collects all free variables and tries to show       *)
   6.282 +(* that the support of these free variables (op supports) *)
   6.283 +(* the goal                                               *)
   6.284  fun collect_vars i (Bound j) vs = if j < i then vs else Bound (j - i) ins vs
   6.285    | collect_vars i (v as Free _) vs = v ins vs
   6.286    | collect_vars i (v as Var _) vs = v ins vs
   6.287 @@ -219,17 +244,18 @@
   6.288  
   6.289  in             
   6.290  
   6.291 -
   6.292  fun simp_meth_setup tac =
   6.293    Method.only_sectioned_args (Simplifier.simp_modifiers' @ Splitter.split_modifiers)
   6.294    (Method.SIMPLE_METHOD' HEADGOAL o tac o local_simpset_of);
   6.295  
   6.296 -val perm_eq_meth         = simp_meth_setup (perm_simp_tac NO_DEBUG_tac);
   6.297 -val perm_eq_meth_debug   = simp_meth_setup (perm_simp_tac DEBUG_tac);
   6.298 -val supports_meth        = simp_meth_setup (supports_tac NO_DEBUG_tac);
   6.299 -val supports_meth_debug  = simp_meth_setup (supports_tac DEBUG_tac);
   6.300 -val finite_gs_meth       = simp_meth_setup (finite_guess_tac NO_DEBUG_tac);
   6.301 -val finite_gs_meth_debug = simp_meth_setup (finite_guess_tac DEBUG_tac);
   6.302 +val perm_eq_meth            = simp_meth_setup (perm_simp_tac NO_DEBUG_tac);
   6.303 +val perm_eq_meth_debug      = simp_meth_setup (perm_simp_tac DEBUG_tac);
   6.304 +val perm_full_eq_meth       = simp_meth_setup (perm_full_simp_tac NO_DEBUG_tac);
   6.305 +val perm_full_eq_meth_debug = simp_meth_setup (perm_full_simp_tac DEBUG_tac);
   6.306 +val supports_meth           = simp_meth_setup (supports_tac NO_DEBUG_tac);
   6.307 +val supports_meth_debug     = simp_meth_setup (supports_tac DEBUG_tac);
   6.308 +val finite_gs_meth          = simp_meth_setup (finite_guess_tac NO_DEBUG_tac);
   6.309 +val finite_gs_meth_debug    = simp_meth_setup (finite_guess_tac DEBUG_tac);
   6.310  
   6.311  end
   6.312