--- a/src/HOL/Auth/Guard/Guard_NS_Public.thy Sun Jul 15 22:56:49 2012 +0200
+++ b/src/HOL/Auth/Guard/Guard_NS_Public.thy Sun Jul 15 22:58:52 2012 +0200
@@ -158,7 +158,10 @@
apply (case_tac "NBa=NB", clarify)
apply (drule Guard_Nonce_analz, simp+)
apply (drule Says_imp_knows_Spy)+
-by (drule_tac A=Aa and A'=A in NB_is_uniq, auto)
+apply (drule_tac A=Aa and A'=A in NB_is_uniq)
+apply auto[1]
+apply (auto simp add: guard.No_Nonce)
+done
subsection{*Agents' Authentication*}
--- a/src/HOL/Auth/Guard/Guard_Public.thy Sun Jul 15 22:56:49 2012 +0200
+++ b/src/HOL/Auth/Guard/Guard_Public.thy Sun Jul 15 22:58:52 2012 +0200
@@ -5,7 +5,7 @@
Lemmas on guarded messages for public protocols.
*)
-theory Guard_Public imports Guard Public Extensions begin
+theory Guard_Public imports Guard "../Public" Extensions begin
subsection{*Extensions to Theory @{text Public}*}
--- a/src/HOL/Bali/AxExample.thy Sun Jul 15 22:56:49 2012 +0200
+++ b/src/HOL/Bali/AxExample.thy Sun Jul 15 22:58:52 2012 +0200
@@ -83,7 +83,7 @@
apply (tactic "ax_tac 1" (* AVar *))
prefer 2
apply (rule ax_subst_Val_allI)
-apply (tactic {* inst1_tac @{context} "P'" "\<lambda>u a. Normal (?PP a\<leftarrow>?x) u" *})
+apply (tactic {* inst1_tac @{context} "P'" "\<lambda>a. Normal (?PP a\<leftarrow>?x)" *})
apply (simp del: avar_def2 peek_and_def2)
apply (tactic "ax_tac 1")
apply (tactic "ax_tac 1")
@@ -137,7 +137,7 @@
prefer 4
apply (rule ax_derivs.Done [THEN conseq1],force)
apply (rule ax_subst_Val_allI)
-apply (tactic {* inst1_tac @{context} "P'" "\<lambda>u a. Normal (?PP a\<leftarrow>?x) u" *})
+apply (tactic {* inst1_tac @{context} "P'" "\<lambda>a. Normal (?PP a\<leftarrow>?x)" *})
apply (simp (no_asm) del: peek_and_def2 heap_free_def2 normal_def2 o_apply)
apply (tactic "ax_tac 1")
prefer 2
@@ -161,7 +161,7 @@
apply (tactic "ax_tac 1")
defer
apply (rule ax_subst_Var_allI)
-apply (tactic {* inst1_tac @{context} "P'" "\<lambda>u vf. Normal (?PP vf \<and>. ?p) u" *})
+apply (tactic {* inst1_tac @{context} "P'" "\<lambda>vf. Normal (?PP vf \<and>. ?p)" *})
apply (simp (no_asm) del: split_paired_All peek_and_def2 initd_def2 heap_free_def2 normal_def2)
apply (tactic "ax_tac 1" (* NewC *))
apply (tactic "ax_tac 1" (* ax_Alloc *))
--- a/src/Pure/search.ML Sun Jul 15 22:56:49 2012 +0200
+++ b/src/Pure/search.ML Sun Jul 15 22:58:52 2012 +0200
@@ -255,9 +255,9 @@
*)
(*Insertion into priority queue of states, marked with level *)
-fun insert_with_level (lnth: int*int*thm, []) = [lnth]
- | insert_with_level ((l,m,th), (l',n,th')::nths) =
- if n<m then (l',n,th') :: insert_with_level ((l,m,th), nths)
+fun insert_with_level (lnth: int*int*thm) [] = [lnth]
+ | insert_with_level (l,m,th) ((l',n,th') :: nths) =
+ if n<m then (l',n,th') :: insert_with_level (l,m,th) nths
else if n=m andalso Thm.eq_thm(th,th')
then (l',n,th')::nths
else (l,m,th)::(l',n,th')::nths;
@@ -274,7 +274,7 @@
let fun cost thm = (level, costf level thm, thm)
in (case List.partition satp news of
([],nonsats)
- => next (List.foldr insert_with_level nprfs (map cost nonsats))
+ => next (fold_rev (insert_with_level o cost) nonsats nprfs)
| (sats,_) => some_of_list sats)
end and
next [] = NONE
--- a/src/Pure/term.ML Sun Jul 15 22:56:49 2012 +0200
+++ b/src/Pure/term.ML Sun Jul 15 22:58:52 2012 +0200
@@ -147,7 +147,7 @@
val aconv_untyped: term * term -> bool
val could_unify: term * term -> bool
val strip_abs_eta: int -> term -> (string * typ) list * term
- val match_bvars: (term * term) * (string * string) list -> (string * string) list
+ val match_bvars: (term * term) -> (string * string) list -> (string * string) list
val map_abs_vars: (string -> string) -> term -> term
val rename_abs: term -> term -> term -> term option
val is_open: term -> bool
@@ -611,7 +611,7 @@
| match_bvs(_,_,al) = al;
(* strip abstractions created by parameters *)
-fun match_bvars((s,t),al) = match_bvs(strip_abs_body s, strip_abs_body t, al);
+fun match_bvars (s,t) al = match_bvs(strip_abs_body s, strip_abs_body t, al);
fun map_abs_vars f (t $ u) = map_abs_vars f t $ map_abs_vars f u
| map_abs_vars f (Abs (a, T, t)) = Abs (f a, T, map_abs_vars f t)
--- a/src/Pure/thm.ML Sun Jul 15 22:56:49 2012 +0200
+++ b/src/Pure/thm.ML Sun Jul 15 22:58:52 2012 +0200
@@ -1562,7 +1562,7 @@
(*Function to rename bounds/unknowns in the argument, lifted over B*)
fun rename_bvars dpairs =
- rename_bvs (List.foldr Term.match_bvars [] dpairs) dpairs;
+ rename_bvs (fold_rev Term.match_bvars dpairs []) dpairs;
(*** RESOLUTION ***)
--- a/src/Pure/unify.ML Sun Jul 15 22:56:49 2012 +0200
+++ b/src/Pure/unify.ML Sun Jul 15 22:58:52 2012 +0200
@@ -273,11 +273,11 @@
Does not even identify Vars in dpairs such as ?a =?= ?b; an attempt to
do so caused numerous problems with no compensating advantage.
*)
-fun SIMPL0 thy (dp0, (env,flexflex,flexrigid)) : Envir.env * dpair list * dpair list =
+fun SIMPL0 thy dp0 (env,flexflex,flexrigid) : Envir.env * dpair list * dpair list =
let
val (dp as (rbinder, t, u), env) = head_norm_dpair thy (env, dp0);
fun SIMRANDS (f $ t, g $ u, env) =
- SIMPL0 thy ((rbinder, t, u), SIMRANDS (f, g, env))
+ SIMPL0 thy (rbinder, t, u) (SIMRANDS (f, g, env))
| SIMRANDS (t as _$_, _, _) =
raise TERM ("SIMPL: operands mismatch", [t, u])
| SIMRANDS (t, u as _ $ _, _) =
@@ -318,7 +318,7 @@
Clever would be to re-do just the affected dpairs*)
fun SIMPL thy (env,dpairs) : Envir.env * dpair list * dpair list =
let
- val all as (env', flexflex, flexrigid) = List.foldr (SIMPL0 thy) (env, [], []) dpairs;
+ val all as (env', flexflex, flexrigid) = fold_rev (SIMPL0 thy) dpairs (env, [], []);
val dps = flexrigid @ flexflex;
in
if exists (fn (_, t, u) => changed (env', t) orelse changed (env', u)) dps
@@ -496,15 +496,24 @@
in change 0 end;
(*Change indices, delete the argument if it contains a banned Bound*)
-fun change_arg banned ({j, t, T}, args) : flarg list =
+fun change_arg banned {j, t, T} args : flarg list =
if rigid_bound (0, banned) t then args (*delete argument!*)
else {j = j, t = change_bnos banned t, T = T} :: args;
(*Sort the arguments to create assignments if possible:
- create eta-terms like ?g(B.1,B.0) *)
-fun arg_less ({t = Bound i1, ...}, {t = Bound i2, ...}) = (i2 < i1)
- | arg_less (_: flarg, _: flarg) = false;
+ create eta-terms like ?g B.1 B.0*)
+local
+ fun less_arg ({t = Bound i1, ...}, {t = Bound i2, ...}) = (i2 < i1)
+ | less_arg (_: flarg, _: flarg) = false;
+
+ fun ins_arg x [] = [x]
+ | ins_arg x (y :: ys) =
+ if less_arg (y, x) then y :: ins_arg x ys else x :: y :: ys;
+in
+ fun sort_args [] = []
+ | sort_args (x :: xs) = ins_arg x (sort_args xs);
+end;
(*Test whether the new term would be eta-equivalent to a variable --
if so then there is no point in creating a new variable*)
@@ -519,7 +528,7 @@
val (Var (v, T), ts) = strip_comb t;
val (Ts, U) = strip_type env T
and js = length ts - 1 downto 0;
- val args = sort (make_ord arg_less) (List.foldr (change_arg banned) [] (flexargs (js, ts, Ts)))
+ val args = sort_args (fold_rev (change_arg banned) (flexargs (js, ts, Ts)) [])
val ts' = map #t args;
in
if decreasing (length Ts) args then (env, (list_comb (Var (v, T), ts')))
@@ -570,7 +579,7 @@
eliminates trivial tpairs like t=t, as well as repeated ones
trivial tpairs can easily escape SIMPL: ?A=t, ?A=?B, ?B=t gives t=t
Resulting tpairs MAY NOT be in normal form: assignments may occur here.*)
-fun add_ffpair thy ((rbinder,t0,u0), (env,tpairs)) : Envir.env * (term * term) list =
+fun add_ffpair thy (rbinder,t0,u0) (env,tpairs) : Envir.env * (term * term) list =
let
val t = Envir.norm_term env t0
and u = Envir.norm_term env u0;
@@ -618,7 +627,7 @@
SIMPL thy (env, dpairs));
in
(case flexrigid of
- [] => SOME (List.foldr (add_ffpair thy) (env', []) flexflex, reseq)
+ [] => SOME (fold_rev (add_ffpair thy) flexflex (env', []), reseq)
| dp :: frigid' =>
if tdepth > search_bnd then
(warning "Unification bound exceeded"; Seq.pull reseq)
@@ -655,7 +664,7 @@
Unlike Huet (1975), does not smash together all variables of same type --
requires more work yet gives a less general unifier (fewer variables).
Handles ?f(t1...rm) with ?f(u1...um) to avoid multiple updates. *)
-fun smash_flexflex1 ((t, u), env) : Envir.env =
+fun smash_flexflex1 (t, u) env : Envir.env =
let
val vT as (v, T) = var_head_of (env, t)
and wU as (w, U) = var_head_of (env, u);
@@ -669,7 +678,7 @@
(*Smash all flex-flexpairs. Should allow selection of pairs by a predicate?*)
fun smash_flexflex (env, tpairs) : Envir.env =
- List.foldr smash_flexflex1 env tpairs;
+ fold_rev smash_flexflex1 tpairs env;
(*Returns unifiers with no remaining disagreement pairs*)
fun smash_unifiers thy tus env =