scyther-proof-0.3.0: data/isabelle/src/ESPLogic/espl_definitions.ML
(*****************************************************************************
* ESPL --- an embedded security protocol logic
* http://people.inf.ethz.ch/meiersi/espl/
*
* Copyright (c) 2009-2011, Simon Meier, ETH Zurich, Switzerland
*
* Extension to compromising adversaries:
*
* Copyright (c) 2010-2011, Martin Schaub, ETH Zurich, Switzerland
*
* All rights reserved. See file LICENCE for more information.
******************************************************************************)
(*
Commands for role and protocols definitions in the ESPLogic.
Side effect: registers the two definitional commands "role" and "protocol".
*)
signature ESPL_DEFINITIONS =
sig
(* Additional Utilities *)
val unnamed_caseN: string
datatype steptyp = Recv | Send
val mk_rolestep: steptyp * term * term -> term
val dest_rolestep: term -> steptyp * term * term
val dest_role: term -> (steptyp * term * term) list
val dest_variable_store_lookup: term -> term * (term * term)
val dest_non_refl_eq: typ -> term -> term * term
val get_unfold_thms: Proof.context -> term -> thm list
val get_rolestep_msg: Proof.context -> string -> term
(* Role Definitions *)
val define_rolestep_cmd
: string -> Args.src list -> steptyp * term * term -> local_theory ->
((term * thm) * (term * thm)) * local_theory
val define_role_cmd
: binding * ((binding * Args.src list) * string) -> local_theory ->
((term * thm) * ((term * thm) * (term * thm)) list) * local_theory
(* Protocol Definitions *)
val define_proto_cmd
: binding * ((binding * Args.src list) * string) -> local_theory ->
(term * thm) * local_theory
(* Managing the Chain Rule and Its Expansion with Named Cases *)
structure TypeElimRulesData : GENERIC_DATA
val lookup_type_elim_rules: Proof.context -> TypeElimRulesData.T
val insert_case_names: Proof.context -> thm -> thm
val source_case_names: thm -> string list
val refine_knows_cases
: Proof.context -> term option -> thm -> thm
val prepare_sources_elim: Proof.context -> thm -> term -> thm
structure KnowsCasesCache : NAMED_THMS
val precompute_source_elim_rules
: thm -> Proof.context -> (string * thm list) list * local_theory
(* Type Invariant Definitions Combined With Chain Rule Expansion *)
val type_invariant_cmd
: (binding * string) * ((binding * Args.src list) * string) ->
local_theory -> local_theory
end;
structure ESPL_Definitions: ESPL_DEFINITIONS =
struct
open ESPL_Utils;
(******************************************************************************
** Additional Utilities
******************************************************************************)
datatype steptyp = Recv | Send | Note of term;
fun mk_rolestep (Send, lbl, msg) = @{const Send} $ lbl $ msg
| mk_rolestep (Recv, lbl, msg) = @{const Recv} $ lbl $ msg
| mk_rolestep (Note nTy, lbl, msg) = @{const Note} $ lbl $ nTy $ msg
fun dest_rolestep (Const (@{const_name Send},_) $ lbl $ msg) = (Send, lbl, msg)
| dest_rolestep (Const (@{const_name Recv},_) $ lbl $ msg) = (Recv, lbl, msg)
| dest_rolestep (Const (@{const_name Note},_) $ lbl $ nTy $ msg) = (Note nTy, lbl, msg)
| dest_rolestep t = raise TERM ("dest_rolestep", [t])
val dest_role = map dest_rolestep o HOLogic.dest_list
(* Destruct a symbolic representation of the contents
of a protocol variable.
*)
fun dest_variable_store_lookup (t as (s $ lv)) =
if (Term.fastype_of s = @{typ "store"})
then (case HOLogic.strip_tuple lv of
[v,tid] => (s, (v,tid))
| _ =>
raise TERM ("dest_variable_store_lookup: wrong arity",[t]))
else raise TERM ("dest_variable_store_lookup: wrong type",[t])
| dest_variable_store_lookup t =
raise TERM ("dest_variable_store_lookup",[t]);
(* Destruct an non-reflexive equality *)
fun dest_non_refl_eq ty t =
case HOLogic.dest_eq t of
eq as (lhs,rhs) =>
if lhs = rhs
then raise TERM ("dest_non_refl_eq: reflexive",[t])
else
if Term.fastype_of lhs = ty
then eq
else raise TYPE ("dest_non_refl_eq:",[ty],[t]);
(* Retrieves the unfold theorems for a constent that were previously stored as
const_name.unfold. This is not very stable but works for our defintions.
TODO: Check if there is a more stable machinery for that purpose.
*)
fun get_unfold_thms ctxt (Const (c,_)) = ProofContext.get_thms ctxt (c ^ ".unfold")
| get_unfold_thms ctxt (Free (c,_)) = ProofContext.get_thms ctxt (c ^ ".unfold")
| get_unfold_thms _ t = raise TERM ("get_unfold_thms", [t])
(* Lookup the term of the message of a role step *)
fun get_rolestep_msg ctxt step_name =
ProofContext.get_thm ctxt (Thm.def_name (step_name ^ "_pt"))
|> Thm.prop_of
|> dest_HOL_def
|> snd
(* Extract identifiers of message variables in a pattern *)
fun pat_msgvars (Const (@{const_name "PEnc"},_) $ m $ k) =
OrdList.union fast_string_ord (pat_msgvars m) (pat_msgvars k)
| pat_msgvars (Const (@{const_name "PTup"},_) $ x $ y) =
OrdList.union fast_string_ord (pat_msgvars x) (pat_msgvars y)
| pat_msgvars (Const (@{const_name "PHash"},_) $ x) =
pat_msgvars x
| pat_msgvars (Const (@{const_name "PSymK"},_) $ a $ b) =
OrdList.union fast_string_ord (pat_msgvars a) (pat_msgvars b)
| pat_msgvars (Const (@{const_name "PAsymPK"},_) $ a) =
pat_msgvars a
| pat_msgvars (Const (@{const_name "PAsymSK"},_) $ a) =
pat_msgvars a
| pat_msgvars (Const (@{const_name "PFresh"},_) $ _) =
[]
| pat_msgvars (Const (@{const_name "PConst"},_) $ _) =
[]
| pat_msgvars (Const (@{const_name "PVar"},_) $ v) =
(case v of
(Const (@{const_name AVar},_) $ _) => []
| (Const (@{const_name MVar},_) $ i) => [HOLogic.dest_string i]
| _ => []
)
| pat_msgvars _ = []
(******************************************************************************
** Role Definitions
******************************************************************************)
(*
The "role" definition command defines constants for every message and step of
the role specification and the role specification itself. Furthermore
wellformedness of the role and several expansion theorems are proven
automatically. The theorems "role.unfold" can be used if all these
intermediate definitions need to be simplified away.
*)
(* proves and notes all the theorems associated to a rolestep *)
fun setup_rolestep mk_binding ann_defs lthy =
let
val ((msg_const,msg_def),(step_const,step_def)) = ann_defs;
val ss_step = Simplifier.simpset_of lthy addsimps [step_def];
val ss_full = ss_step addsimps [msg_def];
val sendStep_t = @{const sendStep} $ step_const;
val noteStep_t = @{const noteStep} $ step_const;
val stepPat_t = @{const stepPat} $ step_const;
val noteType_t = @{const noteType} $ step_const;
val inst_t = @{term "inst s i"} $ msg_const;
val FV_t = @{term "FV"} $ msg_const;
val FMV_t = @{term "FMV"} $ msg_const;
val FAV_t = @{term "FAV"} $ msg_const;
in
lthy
(* unfold theorems *)
|> #2 o Local_Theory.note (mk_binding "unfold", [msg_def,step_def])
(* step expansions *)
|> #2 o notes_expansion ss_step
[ (mk_binding "sendStep_conv", [([sendStep_t],[att_iff_add])])
, (mk_binding "noteStep_conv", [([noteStep_t],[att_iff_add])])
, (mk_binding "stepPat_conv", [([stepPat_t],[att_simp_add])])
, (mk_binding "noteType_conv", [([noteType_t],[att_simp_add])])
]
(* full expansions *)
|> notes_expansion ss_full
[ (mk_binding "inst_conv", [([inst_t], [att_simp_add])])
, (mk_binding "FV_conv", [([FV_t], [att_simp_add])])
, (mk_binding "FMV_conv", [([FMV_t], [att_simp_add])])
, (mk_binding "FAV_conv", [([FAV_t], [att_simp_add])])
]
(* restore original annotated definitions *)
|>> K ann_defs
end
(* defines the constants needed for a rolestep and setups the associated
theorems using setup_rolestep
*)
fun define_rolestep_cmd prefix srcs (stepty, lbl, msg) lthy =
let
val lbl_str = HOLogic.dest_string lbl;
val step_name = prefix ^ "_" ^ lbl_str;
val step_const_bind = Binding.name step_name;
val step_def_bind = (Binding.suffix_name "_def" step_const_bind, srcs);
val msg_name = step_name ^ "_pt";
val msg_const_bind = Binding.name msg_name;
val msg_def_bind = (Binding.suffix_name "_def" msg_const_bind, srcs);
val msg_def_eq = Logic.mk_equals (Free (msg_name, @{typ pattern}), msg);
in
lthy
|> Specification.definition
( SOME (msg_const_bind, SOME @{typ pattern}, NoSyn)
, (msg_def_bind, msg_def_eq) )
|-> (fn (msg_const, (_, msg_def)) =>
Specification.definition
( SOME (step_const_bind, SOME @{typ rolestep}, NoSyn)
, ( step_def_bind
, Logic.mk_equals (Free (step_name, @{typ rolestep}),
mk_rolestep (stepty, lbl, msg_const))
)
)
#>> (fn (step_const, (_, step_def)) =>
((msg_const, msg_def), (step_const, step_def))
)
)
|-> setup_rolestep (fn n => (Binding.qualify true step_name (Binding.name n), srcs))
end
(* proves and notes all theorems associated to a role *)
fun setup_role mk_binding (defs as ((role_const, role_def), steps)) ctxt =
let
val in_set_t = HOLogic.mk_mem (@{term "step :: rolestep"},
@{term "set :: role => rolestep set"} $ role_const);
val zip_t =
@{term "zip :: role => 'a list => (rolestep * 'a) list"}
$ role_const $ @{term "xs :: 'a list"}
val splits_t =
@{term "splits :: role => (role * role) list"} $ role_const
val pat_defs = map (snd o fst) steps;
val step_defs = map (snd o snd) steps;
val step_consts = map (fst o snd) steps;
val ss_role = Simplifier.simpset_of ctxt addsimps [role_def,
@{thm prefixClose_def}, @{thm weakly_atomic_def}];
val ss_full = ss_role addsimps (pat_defs @ step_defs @
@{thms wf_role_def distinct_list_def wf_role_axioms_def});
val simp_tactic = K (FIRSTGOAL (Simplifier.full_simp_tac ss_full));
val distinct_steps_thms = prove_distinctness ctxt simp_tactic step_consts;
val wf_goal = HOLogic.mk_Trueprop (@{const wf_role} $ role_const);
val avars_t = @{const aVars}$ role_const;
val lastComStep_t = @{const lastComStep} $ role_const;
val firstComStep_t = @{const firstComStep} $ role_const;
val ss_prefixClose = ss_role addsimps distinct_steps_thms;
fun mk_prefixClose_thm step_def =
let
val step = step_def |> Thm.prop_of |> dest_HOL_def |> #1;
val t = @{const prefixClose} $ (Free ("s", @{typ store})) $
(Free ("t", @{typ explicit_trace})) $
role_const $ step $ (Free ("i", @{typ tid}));
in expand_term ss_prefixClose t end
fun pat_def_msgvars pat_def =
pat_def |> Thm.prop_of |> dest_HOL_def |> #2 |> pat_msgvars;
val msgvars = Library.foldl
(fn (vs,def) => OrdList.union fast_string_ord vs (pat_def_msgvars def))
([],pat_defs);
fun mk_weakly_atomic_thm v = expand_term ss_role
( @{const weakly_atomic} $ HOLogic.mk_tuple [role_const, HOLogic.mk_string v] );
in
ctxt
(* unfold theorems *)
|> #2 o Local_Theory.note (mk_binding "unfold", role_def :: step_defs @ pat_defs)
(* wellformed role *)
|> #2 o notes_proven simp_tactic
[ (mk_binding "wf_role", [([wf_goal],[att_iff_add])]) ]
(* distinct steps and prefixClose expansions *)
|> #2 o Local_Theory.notes
[ (mk_binding "distinct_steps", [(distinct_steps_thms,[att_iff_add])])
, (mk_binding "prefixClose_convs",
[(map mk_prefixClose_thm step_defs, [att_iff_add])])
, (mk_binding "weakly_atomic_convs",
[(map mk_weakly_atomic_thm msgvars, [att_iff_add])])
]
(* expansions *)
|> notes_expansion ss_role
[ (mk_binding "in_set_conv", [([in_set_t],[att_iff_add])])
, (mk_binding "zip_conv", [([zip_t],[att_simp_add])])
, (mk_binding "splits_conv", [([splits_t],[att_simp_add])])
, (mk_binding "avars_conv", [([avars_t],[att_simp_add])])
, (mk_binding "lastComStep_conv", [([lastComStep_t],[att_simp_add])])
, (mk_binding "firstComStep_conv", [([firstComStep_t],[att_simp_add])])
]
(* restore definitions *)
|>> K defs
end
(* defines a role and setups all associated theorems using setup_role *)
fun define_role_cmd (raw_bind, raw_spec as ((_,srcs),_)) params_ctxt =
let
val (([((_,role_ty),_)],[(role_def_bind, role_eq)]), _) =
Specification.read_free_spec [(raw_bind, SOME "Protocol.role", NoSyn)]
[raw_spec] params_ctxt;
val steps = role_eq |> dest_HOL_def |> #2 |> dest_role;
fun mk_definition ann_step_defs =
let
val role_eq = Logic.mk_equals (role_eq |> dest_HOL_def |> #1,
HOLogic.mk_list @{typ rolestep} (map (fst o snd) ann_step_defs));
in
Specification.definition
( SOME (raw_bind, SOME role_ty, NoSyn)
, (role_def_bind, role_eq) )
#>> (fn (role_const,(_,role_def)) => ((role_const,role_def),ann_step_defs))
end
val prefix = Binding.name_of raw_bind;
fun mk_rel_binding name = (Binding.qualify true prefix (Binding.name name), srcs);
in
params_ctxt
|> fold_map (define_rolestep_cmd prefix srcs) steps
|-> mk_definition
|-> setup_role mk_rel_binding
end
(* registering the role definition command as an outer keyword *)
local structure P = OuterParse and K = OuterKeyword in
val roledef_parser =
P.binding --| P.where_ -- (SpecParse.opt_thm_name ":" -- P.prop);
val _ =
OuterSyntax.local_theory "role" "security protocol role definition"
K.thy_decl (roledef_parser >> (fn spec => define_role_cmd spec #> snd));
end;
(******************************************************************************
** Protocol Definitions
******************************************************************************)
(* proves and notes all theorems associated to a protocol definition *)
fun setup_proto mk_binding (ann_def as (proto_const, proto_def)) ctxt =
let
val role_consts = proto_def |> Thm.prop_of
|> dest_HOL_def |> #2 |> HOLogic.dest_set;
val role_unfolds = flat (map (get_unfold_thms ctxt) role_consts);
val proto_ss = Simplifier.simpset_of ctxt addsimps
(proto_def :: @{thms wf_proto_def});
val full_ss = proto_ss addsimps role_unfolds;
fun simp_tactic ss = K (FIRSTGOAL (Simplifier.full_simp_tac ss));
val wf_proto_thm = prove_prop ctxt (simp_tactic proto_ss)
(HOLogic.mk_Trueprop (@{const wf_proto} $ proto_const));
val distinct_roles_thms =
prove_distinctness ctxt (simp_tactic full_ss) role_consts;
val in_set_t = HOLogic.mk_mem (@{term "R :: role"}, proto_const);
in
ctxt
(* unfolds, distinct roles, and wf_proto *)
|> #2 o Local_Theory.notes
[ (mk_binding "unfold", [(proto_def :: role_unfolds, [])])
, (mk_binding "distinct_roles", [(distinct_roles_thms,[att_iff_add])])
, (mk_binding "wf_proto", [([wf_proto_thm], [att_iff_add])])
]
(* expansions *)
|> #2 o notes_expansion proto_ss
[ (mk_binding "in_set_conv", [([in_set_t],[att_iff_add])])
]
(* restore annotated definition *)
|> pair ann_def
end;
fun define_proto_cmd (raw_bind, raw_spec as ((_,srcs),_)) params_ctxt =
let
val ((proto_const, (_, proto_def)), spec_ctxt) = params_ctxt
|> Specification.definition_cmd
(SOME (raw_bind, SOME "Protocol.proto", NoSyn), raw_spec);
val proto_name = Binding.name_of raw_bind;
fun mk_rel_binding name =
(Binding.qualify true proto_name (Binding.name name), srcs);
in
setup_proto mk_rel_binding (proto_const, proto_def) spec_ctxt
|> apsnd (Local_Theory.theory (fn thy =>
let
val locale_b = Binding.name (proto_name ^ "_state");
val _ = Output.writeln ("\nlocale\n " ^ (Binding.name_of locale_b));
(* HACK as I didn't know how to get a hand of the right constant *)
val proto_t = Syntax.read_term_global thy proto_name;
val (_,lthy) =
add_simple_locale locale_b "reachable_state" [SOME proto_t] thy;
in
lthy |> Local_Theory.exit_global
end))
end;
(* registering the protocol definition command *)
local structure P = OuterParse and K = OuterKeyword in
val protodef_parser =
P.binding --| P.where_ -- (SpecParse.opt_thm_name ":" -- P.prop);
val _ =
OuterSyntax.local_theory "protocol" "security protocol definition"
K.thy_decl (protodef_parser >> (fn spec => define_proto_cmd spec #> #2));
end;
(******************************************************************************
** Sources Case Name Computation
******************************************************************************)
val unnamed_caseN = "unnamed"
(* Given a list of premises, it extracts the content of the first premise being
a "case_name" hint.
*)
fun extract_case_name prems =
case Hints.gather_by_name "case_name" prems of
(name :: _) => HOLogic.dest_string name
| [] => raise TERM ("extract_case_name", prems);
(* Given a list of case premises, it extracts the rolestep constant name
whose specification message was the start for this case.
*)
fun extract_rolestep_name prems =
case Hints.gather_by_name "decrChainFrom" prems of
(data :: _) =>
(case HOLogic.strip_tuple data of
(_ :: _ :: Const (step_name,_) :: _) => step_name
| _ => raise TERM ("extract_rolestep_name", prems)
)
| _ => raise TERM ("extract_rolestep_name", prems)
(* Name the variable constructors *)
fun var_name (Const (@{const_name "AVar"},_) $ i) = HOLogic.dest_string i
| var_name (Const (@{const_name "MVar"},_) $ i) = HOLogic.dest_string i
| var_name _ = "var"
(* Name the execution literal constructors *)
fun msg_lit_name (Const (@{const_name "ENonce"},_) $ n $ _) = HOLogic.dest_string n
| msg_lit_name (Const (@{const_name "EConst"},_) $ c) = HOLogic.dest_string c
| msg_lit_name _ = "lit";
(* Name the pattern constructors *)
fun msg_name (Const (@{const_name "Enc"},_) $ _ $ _) = "enc"
| msg_name (Const (@{const_name "Tup"},_) $ _ $ _) = "tup"
| msg_name (Const (@{const_name "Hash"},_) $ _) = "hash"
| msg_name (Const (@{const_name "K"},_) $ _ $ _) = "K"
| msg_name (Const (@{const_name "PK"},_) $ _) = "PK"
| msg_name (Const (@{const_name "SK"},_) $ _) = "SK"
| msg_name (Const (@{const_name "Lit"},_) $ l) = msg_lit_name l
| msg_name _ = "msg"
(* extract all non-reflexive equalities,
if there is a lhs with a substitution then use this name
else use the name of the first rhs
*)
fun extract_msg_name prems =
let
val dest_msg_eq = dest_non_refl_eq @{typ execmsg};
val subst_var = var_name o
#1 o #2 o dest_variable_store_lookup o
#1 o dest_msg_eq;
val fixed_msg = msg_name o #2 o dest_msg_eq;
val subst = try hd (ESPL_Utils.gather_props subst_var prems);
val fixed = try hd (ESPL_Utils.gather_props fixed_msg prems);
in
if is_none subst andalso is_none fixed then
NONE
else
if subst = fixed then
SOME (the_default "" subst)
else
SOME (
(the_default "" subst) ^
(if is_some subst andalso is_some fixed then "_" else "") ^
(the_default "" fixed)
)
end
(* get the case name from a term representing an implication *)
fun get_case_name t =
let
val prems = Logic.strip_imp_prems (Term.strip_all_body t);
in
case try extract_case_name prems of
SOME "decrypt" =>
(let
val step_name = extract_rolestep_name prems;
val opt_name = extract_msg_name prems;
in
(List.last (space_explode "." step_name)) ^
(case opt_name of
SOME m => "_" ^ m
| NONE => "")
end
handle _ => "decrypt")
| SOME name => name
| NONE => unnamed_caseN
end;
(* Compute the case names for the given theorem being a case distinction in
eleminitation form gained from spezializing the knows_cases theorem.
*)
fun source_case_names th =
th |> Thm.prop_of
|> Logic.strip_imp_prems
|> map get_case_name
|> blank_zero_numbers (op =)
|> map (append_optional_number "_")
fun mk_case_name_hint thy name =
Hints.mk_hint_thm thy "case_name" (HOLogic.mk_string name);
(* Insert the case names into a theorem *)
fun insert_case_names ctxt th =
let
val thy = ProofContext.theory_of ctxt;
val cases = source_case_names th;
val case_hint = Hints.mk_hint_thm thy "case_name" o HOLogic.mk_string o nth cases;
fun ins_tac (_,i) = Method.insert_tac [case_hint (i-1)] i;
in
HOL_Ext.refine_rule ctxt
(K (ALLGOALS (Hints.remove_all_hints_tac THEN' SUBGOAL ins_tac))) th
end
(******************************************************************************
** Chain Rule Expansion
******************************************************************************)
(* FIXME: Not sure if there isn't some additional setup needed.
For NamedThms it is..
*)
(* Storing the rules used for eliminating the type information *)
structure TypeElimRulesData = Generic_Data
(
type T = Thm.thm list;
val empty = [];
val extend = I;
fun merge (ths1, ths2) = distinct Thm.eq_thm (ths1 @ ths2)
);
val lookup_type_elim_rules = TypeElimRulesData.get o Context.Proof;
(* Reorder the bound variables introduced by the expansion of a ticket.
The argument is premise of the form !! x1..xn. A1 ==> ... An ==> B
The result is a conversion justifying the permutation of x1...xn
according to their left-to-right occurrence in the first equality
of the form
s(MV v tid) = msg
*)
fun reorder_bound_conv ctxt ct =
let
val t = Thm.term_of ct;
val dest_subst_eq =
apfst (dest_variable_store_lookup) o dest_non_refl_eq @{typ execmsg};
in
case
t |> Term.strip_all_body
|> Logic.strip_imp_prems
|> ESPL_Utils.gather_props dest_subst_eq
|> try hd
of
SOME ((_, (_, tidt)), rhst) =>
let
val n = length (Term.strip_all_vars t);
val p = [] |> fold HOL_Ext.add_bound_list [tidt, rhst]
|> distinct (op =)
|> map (fn i => n - i - 1);
in
HOL_Ext.forall_permute_conv ctxt p ct
end
| NONE => Conv.all_conv ct
end;
(* reorders the bound variables of the premises according to
reorder_bound_conv
*)
fun reorder_bound_vars ctxt th =
HOL_Ext.lift_ground_thm_mod ctxt
(Conv.fconv_rule o
Conv.prems_conv (Thm.nprems_of th) o reorder_bound_conv)
th;
(* Eliminates the remaining decryption chains starting from symbolically
instantiated protocol variables using their type assertions.
*)
fun type_elim_tac ctxt ty_elim_ths =
let
fun mk_elim_tac ty_elim_th =
EVERY'
[ etac ty_elim_th
, assume_tac
, TRY o full_simp_tac (simpset_of ctxt)
, TRY o (REPEAT o etac @{thm conjE})
, TRY o Orders.order_tac ctxt []
]
in
(FIRST' (map mk_elim_tac ty_elim_ths)) THEN'
(TRY o Clasimp.clarsimp_tac (clasimpset_of ctxt))
end;
fun expand_knows_cases_tac ctxt ty_elim_ths =
REPEAT_DETERM1 (
FIRST [ safe_tac (claset_of ctxt)
, CHANGED_PROP (TRYALL (full_simp_tac (simpset_of ctxt)))
, CHANGED_PROP (TRYALL (type_elim_tac ctxt ty_elim_ths))
]
);
(* Convert a knows_cases theorem to its elimination form with
all premises named with the corresponding case name.
Optionally, changes to the given message term are traced.
*)
fun refine_knows_cases ctxt opt_msg_t case_th =
let
(* don't track changes to first subgoal "m : knows t" *)
fun mk_track_tac th (_,i) = Method.insert_tac [th] i;
val ((track_tac, untrack), ctxt') =
case opt_msg_t of
SOME msg_t => apfst (apfst mk_track_tac)
(HOL_Ext.track_HOL_term ctxt msg_t)
| NONE => ((K all_tac, I), ctxt);
val ty_elim_ths = lookup_type_elim_rules ctxt';
fun tac lthy =
(ALLGOALS (SUBGOAL track_tac) THEN
expand_knows_cases_tac lthy ty_elim_ths);
in
HOL_Ext.refine_rule ctxt' tac case_th
|> untrack
|> insert_case_names ctxt
|> reorder_bound_vars ctxt
end;
(* A more convenient interface to refine_knows_cases
FIXME: Why can't it be merged with refine_knows_cases?
*)
fun prepare_sources_elim ctxt case_th msg_t =
let
val lthy = Variable.auto_fixes msg_t ctxt;
val knows_ct =
HOLogic.mk_mem (msg_t, @{term "knows t"})
|> HOLogic.mk_Trueprop
|> Thm.cterm_of (ProofContext.theory_of lthy);
val knows_th = Thm.assume knows_ct;
in
(knows_th RS case_th)
|> HOL_Ext.make_HOL_elim
|> refine_knows_cases lthy (SOME msg_t)
|> Thm.implies_intr knows_ct
|> singleton (ProofContext.export lthy ctxt)
|> Drule.zero_var_indexes
end;
(*** Precomputing and storing chain rule expansion in the actual theory ***)
structure KnowsCasesCache = Named_Thms
(val name ="knows_cases_cache"
val description = "Cache of protocol and message specific specializations of the knows_cases theorem")
(* shorthand for attributes modifying the knowledge cases *)
val att_knows_cases_cache_add = Attrib.internal (K KnowsCasesCache.add);
val att_knows_cases_cache_del = Attrib.internal (K KnowsCasesCache.del);
(* Precompute and register the standard chain rule expansions
*)
fun precompute_source_elim_rules case_th ctxt =
let
val _ = Output.writeln "\n precomputed sources for:"
fun precompute (msg_t, desc) =
let
val b = Binding.name ("knows_cases_" ^ desc)
val _ = Output.writeln (" " ^ Binding.name_of b);
in
(b, prepare_sources_elim ctxt case_th msg_t)
end;
val prec_ths = Par_List.map precompute
[ (@{term "LN n i :: execmsg"}, "Nonce")
, (@{term "Hash m :: execmsg"}, "Hash")
, (@{term "Enc m k :: execmsg"}, "Enc")
, (@{term "SK a :: execmsg"}, "SK")
, (@{term "K a b :: execmsg"}, "K")
, (@{term "KShr A :: execmsg"}, "KShr")
]
fun prep_note (b,th) = ((b,[]),[([th],[att_knows_cases_cache_add])]);
in
ctxt
(* |> Local_Theory.target (add_sources_rules (map snd prec_ths)) *)
|> Local_Theory.notes (map prep_note prec_ths)
end;
(******************************************************************************
** Type Invariant Definitions
******************************************************************************)
(* Check if a definition reads like: def = weakly_atomic *)
val is_weakly_atomic_typing =
the_default false o try
(curry (op =) @{const weakly_atomic} o
#2 o ESPL_Utils.dest_HOL_def o Thm.prop_of);
(* Destruct a mk_typing constructor *)
fun dest_mk_typing (Const (@{const_name mk_typing},_) $ typ) =
typ |> HOLogic.dest_list |> map HOLogic.dest_prod
| dest_mk_typing t = raise TERM ("dest_mk_typing", [t]);
(* proves and notes all the theorems associated to a typing *)
fun setup_typing mk_binding ann_def ctxt =
let
val (typ_const,typ_def) = ann_def;
val cs = Classical.claset_of ctxt;
val ss = Simplifier.simpset_of ctxt
addsimps [typ_def];
val ss_full = ss addsimps @{thms mk_typing_def};
val vars = typ_def |> Thm.prop_of
|> ESPL_Utils.dest_HOL_def |> snd |> dest_mk_typing |> map fst;
val typ_calls = map (curry (op $) typ_const) vars;
val mono_typ_th = (@{const monoTyp} $ typ_const)
|> HOLogic.mk_Trueprop
|> Thm.cterm_of (ProofContext.theory_of ctxt)
|> (fn ct => Goal.prove_internal [] ct
(K (auto_tac (cs, ss)))
);
in
ctxt
(* expansions for 'calling' the typing with defined variable *)
|> #2 o ESPL_Utils.notes_expansion ss_full
[ (mk_binding "defined_vars", [(typ_calls, [att_iff_add])]) ]
(* monotonicity theorem *)
|> Local_Theory.note (mk_binding "monoTyp", [mono_typ_th])
(* restore original annotated definition *)
|>> K ann_def
end;
(* Defines and setups a typing defined using 'mk_typing'. *)
fun define_typing_cmd ((b,proto_name), ((att,srcs),raw_def)) params_ctxt =
let
fun mk_rel_binding name =
(Binding.qualify true (Binding.name_of b) (Binding.name name), srcs);
val ((typ_const, (_, typ_def)), spec_ctxt) = params_ctxt
|> Specification.definition_cmd
(SOME (b, SOME "WeakTyping.typing", NoSyn)
, ((att,srcs), raw_def));
in
if is_weakly_atomic_typing typ_def then
( (typ_const, typ_def)
, spec_ctxt
|> Local_Theory.notes
[( mk_rel_binding "unfold_def"
, [([typ_def], [ESPL_Utils.att_simp_add])]
)]
|> #2
)
else
setup_typing mk_rel_binding (typ_const, typ_def) spec_ctxt
end;
(* Add the locale corresponding to the type invariant being defined
*)
fun add_type_invariant_locale (b,(typ_t, proto_t)) =
add_simple_locale b "typed_state"
[SOME proto_t, NONE, NONE, NONE, SOME typ_t];
(* Defines and setups a typing as well as its corresponding
chain rule expansions.
*)
fun type_invariant_cmd (spec as ((typing_b,proto_name),_)) lthy =
lthy
|> #2 o define_typing_cmd spec
|> Local_Theory.theory (fn thy =>
let
val typ_name = Binding.name_of typing_b;
val typ_t = Syntax.read_term_global thy typ_name;
val proto_t = Syntax.read_term_global thy proto_name;
val locale_b = Binding.name (typ_name ^ "_state");
val _ = Output.writeln ("\nlocale\n " ^ (Binding.name_of locale_b));
val (_,lthy) =
add_type_invariant_locale (locale_b, (typ_t, proto_t)) thy;
val case_th = ProofContext.get_thm lthy "knows_cases";
in
lthy
|> #2 o precompute_source_elim_rules case_th
|> Local_Theory.exit_global
end
);
(* register the type invariant definition command *)
local structure P = OuterParse and K = OuterKeyword in
val for_proto = P.$$$ "for" |-- P.term;
val type_invariant_parser =
P.binding -- for_proto --| P.where_ -- (SpecParse.opt_thm_name ":" -- P.prop);
val _ =
OuterSyntax.local_theory "type_invariant" "type invariant definition"
K.thy_decl (type_invariant_parser >> type_invariant_cmd);
end;
end;