# HG changeset patch
# User Christian Urban <christian dot urban at kcl dot ac dot uk>
# Date 1395675077 0
# Node ID 188826f1ccdb8ca22d9ee22f99e56b42162108b9
# Parent  b33b42211bbf4d085b5b9173c5e0717b2f73e562
updated to massive changes in Isabelle

diff -r b33b42211bbf -r 188826f1ccdb Nominal/Ex/CPS/CPS1_Plotkin.thy
--- a/Nominal/Ex/CPS/CPS1_Plotkin.thy	Thu Mar 13 09:30:26 2014 +0000
+++ b/Nominal/Ex/CPS/CPS1_Plotkin.thy	Mon Mar 24 15:31:17 2014 +0000
@@ -86,7 +86,6 @@
   apply (erule lt.exhaust)
   using [[simproc del: alpha_lst]]
   apply (simp_all)
-  apply blast
   apply (simp add: Abs1_eq_iff CPS.eqvt)
   by blast
 
diff -r b33b42211bbf -r 188826f1ccdb Nominal/Ex/CPS/CPS2_DanvyNielsen.thy
--- a/Nominal/Ex/CPS/CPS2_DanvyNielsen.thy	Thu Mar 13 09:30:26 2014 +0000
+++ b/Nominal/Ex/CPS/CPS2_DanvyNielsen.thy	Mon Mar 24 15:31:17 2014 +0000
@@ -48,7 +48,6 @@
   apply (rule_tac y="a" and c="b" in cpsctxt.strong_exhaust)
   using [[simproc del: alpha_lst]]
   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)
@@ -82,7 +81,6 @@
   apply (rule_tac y="a" in lt.exhaust)
   using [[simproc del: alpha_lst]]
   apply auto
-  apply blast
   apply (rule_tac x="lt" and ?'a="name" in obtain_fresh)
   apply (simp add: Abs1_eq_iff)
   apply blast+
diff -r b33b42211bbf -r 188826f1ccdb Nominal/Ex/CPS/CPS3_DanvyFilinski.thy
--- a/Nominal/Ex/CPS/CPS3_DanvyFilinski.thy	Thu Mar 13 09:30:26 2014 +0000
+++ b/Nominal/Ex/CPS/CPS3_DanvyFilinski.thy	Mon Mar 24 15:31:17 2014 +0000
@@ -26,7 +26,6 @@
   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)
 --"-"
diff -r b33b42211bbf -r 188826f1ccdb Nominal/Ex/CPS/Lt.thy
--- a/Nominal/Ex/CPS/Lt.thy	Thu Mar 13 09:30:26 2014 +0000
+++ b/Nominal/Ex/CPS/Lt.thy	Mon Mar 24 15:31:17 2014 +0000
@@ -24,7 +24,6 @@
   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 add: Abs_fresh_iff)
   apply(simp add: fresh_star_def fresh_Pair)
diff -r b33b42211bbf -r 188826f1ccdb Nominal/Ex/Lambda.thy
--- a/Nominal/Ex/Lambda.thy	Thu Mar 13 09:30:26 2014 +0000
+++ b/Nominal/Ex/Lambda.thy	Mon Mar 24 15:31:17 2014 +0000
@@ -661,12 +661,9 @@
   apply (case_tac a rule: lam.exhaust)
   using [[simproc del: alpha_lst]]
   apply simp_all[3]
-  apply blast
   apply (case_tac b)
   apply (rule_tac y="a" and c="ba" in lam.strong_exhaust)
   apply simp_all[3]
-  apply blast
-  apply blast
   apply (simp add: Abs1_eq_iff fresh_star_def)
   using [[simproc del: alpha_lst]]
   apply(simp_all)
@@ -713,8 +710,6 @@
 apply (rule_tac y="a" in lam.exhaust)
 using [[simproc del: alpha_lst]]
 apply simp_all
-apply blast
-apply blast
 apply (rule_tac x="(name, lam)" and ?'a="name" in obtain_fresh)
 apply blast
 apply clarify
diff -r b33b42211bbf -r 188826f1ccdb Nominal/Ex/Let.thy
--- a/Nominal/Ex/Let.thy	Thu Mar 13 09:30:26 2014 +0000
+++ b/Nominal/Ex/Let.thy	Mon Mar 24 15:31:17 2014 +0000
@@ -86,7 +86,6 @@
 apply(case_tac x)
 apply(case_tac b rule: trm_assn.exhaust(2))
 apply(simp_all)
-apply(blast)
 done
 
 termination by lexicographic_order
@@ -145,7 +144,6 @@
   apply(case_tac x)
   apply(case_tac b rule: trm_assn.exhaust(2))
   apply(simp_all)
-  apply(blast)
   done
 
 termination by lexicographic_order
diff -r b33b42211bbf -r 188826f1ccdb Nominal/Ex/Multi_Recs2.thy
--- a/Nominal/Ex/Multi_Recs2.thy	Thu Mar 13 09:30:26 2014 +0000
+++ b/Nominal/Ex/Multi_Recs2.thy	Mon Mar 24 15:31:17 2014 +0000
@@ -103,7 +103,6 @@
   apply(raw_tactic {* Induction_Schema.induction_schema_tac @{context} @{thms assms} *})
   apply(rule_tac y="exp" and c="c" in fun_recs.strong_exhaust(1))
   apply(simp_all)[4]
-  apply(blast)
   apply(rule_tac ya="fnclause" and c="c" in fun_recs.strong_exhaust(2))
   apply(blast)
   apply(rule_tac yb="fnclauses" in fun_recs.strong_exhaust(3))
diff -r b33b42211bbf -r 188826f1ccdb Nominal/Ex/Pi.thy
--- a/Nominal/Ex/Pi.thy	Thu Mar 13 09:30:26 2014 +0000
+++ b/Nominal/Ex/Pi.thy	Mon Mar 24 15:31:17 2014 +0000
@@ -172,8 +172,6 @@
   apply(auto simp add: fresh_star_def)[1]
   apply(blast)
   apply(simp)
-  apply(blast)
-  apply(simp)
   apply(case_tac b)
   apply(simp)
   apply(case_tac a)
@@ -192,9 +190,7 @@
   apply(blast)
   using [[simproc del: alpha_lst]]
   apply(auto simp add: fresh_star_def)[1]
-  apply(blast)
   apply(simp)
-  apply(blast)
   --"compatibility"
   apply (simp only: meta_eq_to_obj_eq[OF subs_mix_def, symmetric, unfolded fun_eq_iff])
   apply (subgoal_tac "eqvt_at (\<lambda>(a, b, c). subs_mix a b c) (P, xa, ya)")
diff -r b33b42211bbf -r 188826f1ccdb Nominal/Nominal2.thy
--- a/Nominal/Nominal2.thy	Thu Mar 13 09:30:26 2014 +0000
+++ b/Nominal/Nominal2.thy	Mon Mar 24 15:31:17 2014 +0000
@@ -569,7 +569,7 @@
   (* FIXME: local version *)
   (* val (_, spec_ctxt') = Proof_Context.add_fixes constr_trms spec_ctxt *)
 
-  val thy' = Sign.add_consts_i constr_trms (Proof_Context.theory_of spec_ctxt)
+  val thy' = Sign.add_consts constr_trms (Proof_Context.theory_of spec_ctxt)
 in
   (dts', thy')
 end
@@ -591,7 +591,7 @@
 
 in
   (Local_Theory.exit_global lthy')
-  |> Sign.add_consts_i bn_funs'
+  |> Sign.add_consts bn_funs'
   |> pair (bn_funs', bn_eqs) 
 end 
 *}
diff -r b33b42211bbf -r 188826f1ccdb Nominal/Nominal2_Base.thy
--- a/Nominal/Nominal2_Base.thy	Thu Mar 13 09:30:26 2014 +0000
+++ b/Nominal/Nominal2_Base.thy	Mon Mar 24 15:31:17 2014 +0000
@@ -2167,7 +2167,7 @@
 proof -
   have "(\<Union>{supp x | x. x \<in># M}) = (\<Union>{supp x | x. x \<in> set_of M})" by simp
   also have "... \<subseteq> (\<Union>x \<in> set_of M. supp x)" by auto
-  also have "... = supp (set_of M)" by (simp add: subst supp_of_finite_sets)
+  also have "... = supp (set_of M)" by (simp add: supp_of_finite_sets)
   also have " ... \<subseteq> supp M" by (rule supp_set_of)
   finally show "(\<Union>{supp x | x. x \<in># M}) \<subseteq> supp M" .
 qed
diff -r b33b42211bbf -r 188826f1ccdb Nominal/nominal_function.ML
--- a/Nominal/nominal_function.ML	Thu Mar 13 09:30:26 2014 +0000
+++ b/Nominal/nominal_function.ML	Mon Mar 24 15:31:17 2014 +0000
@@ -205,7 +205,7 @@
   end
 
 val add_nominal_function =
-  gen_add_nominal_function false Specification.check_spec (Type_Infer.anyT HOLogic.typeS)
+  gen_add_nominal_function false Specification.check_spec (Type_Infer.anyT @{sort type})
 fun add_nominal_function_cmd a b c d int = 
   gen_add_nominal_function int Specification.read_spec "_::type" a b c d
 
@@ -220,7 +220,7 @@
   end
 
 val nominal_function =
-  gen_nominal_function false Specification.check_spec (Type_Infer.anyT HOLogic.typeS)
+  gen_nominal_function false Specification.check_spec (Type_Infer.anyT @{sort type})
 fun nominal_function_cmd a b c int = 
   gen_nominal_function int Specification.read_spec "_::type" a b c
 
diff -r b33b42211bbf -r 188826f1ccdb Nominal/nominal_inductive.ML
--- a/Nominal/nominal_inductive.ML	Thu Mar 13 09:30:26 2014 +0000
+++ b/Nominal/nominal_inductive.ML	Mon Mar 24 15:31:17 2014 +0000
@@ -32,8 +32,8 @@
 
 (* fixme: move to nominal_library *)
 fun real_head_of (@{term Trueprop} $ t) = real_head_of t
-  | real_head_of (Const ("==>", _) $ _ $ t) = real_head_of t
-  | real_head_of (Const (@{const_name all}, _) $ Abs (_, _, t)) = real_head_of t
+  | real_head_of (Const (@{const_name Pure.imp}, _) $ _ $ t) = real_head_of t
+  | real_head_of (Const (@{const_name Pure.all}, _) $ Abs (_, _, t)) = real_head_of t
   | real_head_of (Const (@{const_name All}, _) $ Abs (_, _, t)) = real_head_of t
   | real_head_of (Const ("HOL.induct_forall", _) $ Abs (_, _, t)) = real_head_of t
   | real_head_of t = head_of t
diff -r b33b42211bbf -r 188826f1ccdb Nominal/nominal_library.ML
--- a/Nominal/nominal_library.ML	Thu Mar 13 09:30:26 2014 +0000
+++ b/Nominal/nominal_library.ML	Mon Mar 24 15:31:17 2014 +0000
@@ -298,7 +298,8 @@
 (* decompses a formula into params, premises and a conclusion *)
 fun strip_full_horn trm =
   let
-    fun strip_outer_params (Const ("all", _) $ Abs (a, T, t)) = strip_outer_params t |>> cons (a, T)
+    fun strip_outer_params (Const (@{const_name Pure.all}, _) $ Abs (a, T, t)) = 
+      strip_outer_params t |>> cons (a, T)
     | strip_outer_params B = ([], B)
 
     val (params, body) = strip_outer_params trm
diff -r b33b42211bbf -r 188826f1ccdb Nominal/nominal_mutual.ML
--- a/Nominal/nominal_mutual.ML	Thu Mar 13 09:30:26 2014 +0000
+++ b/Nominal/nominal_mutual.ML	Mon Mar 24 15:31:17 2014 +0000
@@ -291,7 +291,7 @@
   end
 
 
-fun forall_elim s (Const ("all", _) $ Abs (_, _, t)) = subst_bound (s, t)
+fun forall_elim s (Const (@{const_name Pure.all}, _) $ Abs (_, _, t)) = subst_bound (s, t)
   | forall_elim _ t = t
 
 val forall_elim_list = fold forall_elim
@@ -316,7 +316,7 @@
     val acc_prems = 
      map prop_of induct_thms
      |> map2 forall_elim_list argss 
-     |> map (strip_qnt_body "all")
+     |> map (strip_qnt_body @{const_name Pure.all})
      |> map (curry Logic.nth_prem 1)
      |> map HOLogic.dest_Trueprop
 
diff -r b33b42211bbf -r 188826f1ccdb Nominal/nominal_thmdecls.ML
--- a/Nominal/nominal_thmdecls.ML	Thu Mar 13 09:30:26 2014 +0000
+++ b/Nominal/nominal_thmdecls.ML	Mon Mar 24 15:31:17 2014 +0000
@@ -112,7 +112,7 @@
          Syntax.string_of_term (Context.proof_of context) (prop_of thm))
   in
     case prop_of thm of
-      Const ("==", _) $ (Const (@{const_name "permute"}, _) $ p $ c) $ c' =>
+      Const ("Pure.eq", _) $ (Const (@{const_name "permute"}, _) $ p $ c) $ c' =>
         if is_Var p andalso is_fixed (Context.proof_of context) c andalso c aconv c' then
           c
         else
@@ -256,7 +256,7 @@
 fun eqvt_transform ctxt thm =
   (case prop_of thm of @{const "Trueprop"} $ _ =>
     thm_4_of_1 ctxt thm
-  | @{const "==>"} $ _ $ _ =>
+  | @{const "Pure.imp"} $ _ $ _ =>
     thm_4_of_1 ctxt (thm_1_of_2 ctxt thm)
   | _ =>
     error msg)
@@ -279,7 +279,7 @@
     in
       (th', thm_4_of_1 ctxt thm)
     end
-  | @{const "==>"} $ _ $ _ =>
+  | @{const "Pure.imp"} $ _ $ _ =>
     let
       val th1 = thm_1_of_2 ctxt thm
     in