src/HOL/Quickcheck_Benchmark/Needham_Schroeder_Base.thy
author wenzelm
Wed, 29 Oct 2014 11:19:27 +0100
changeset 58813 625d04d4fd2a
parent 58310 91ea607a34d8
child 61952 546958347e05
permissions -rw-r--r--
tuned;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
48243
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
     1
theory Needham_Schroeder_Base
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
     2
imports Main "~~/src/HOL/Library/Predicate_Compile_Quickcheck"
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
     3
begin
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
     4
58310
91ea607a34d8 updated news
blanchet
parents: 58249
diff changeset
     5
datatype agent = Alice | Bob | Spy
48243
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
     6
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
     7
definition agents :: "agent set"
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
     8
where
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
     9
  "agents = {Spy, Alice, Bob}"
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
    10
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
    11
definition bad :: "agent set"
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
    12
where
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
    13
  "bad = {Spy}"
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
    14
58310
91ea607a34d8 updated news
blanchet
parents: 58249
diff changeset
    15
datatype key = pubEK agent | priEK agent
48243
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
    16
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
    17
fun invKey
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
    18
where
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
    19
  "invKey (pubEK A) = priEK A"
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
    20
| "invKey (priEK A) = pubEK A"
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
    21
58310
91ea607a34d8 updated news
blanchet
parents: 58249
diff changeset
    22
datatype
48243
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
    23
     msg = Agent  agent
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
    24
         | Key    key
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
    25
         | Nonce  nat
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
    26
         | MPair  msg msg
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
    27
         | Crypt  key msg
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
    28
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
    29
syntax
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
    30
  "_MTuple"      :: "['a, args] => 'a * 'b"       ("(2{|_,/ _|})")
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
    31
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
    32
syntax (xsymbols)
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
    33
  "_MTuple"      :: "['a, args] => 'a * 'b"       ("(2\<lbrace>_,/ _\<rbrace>)")
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
    34
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
    35
translations
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
    36
  "{|x, y, z|}"   == "{|x, {|y, z|}|}"
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
    37
  "{|x, y|}"      == "CONST MPair x y"
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
    38
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
    39
inductive_set
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
    40
  parts :: "msg set => msg set"
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
    41
  for H :: "msg set"
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
    42
  where
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
    43
    Inj [intro]:               "X \<in> H ==> X \<in> parts H"
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
    44
  | Fst:         "{|X,Y|}   \<in> parts H ==> X \<in> parts H"
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
    45
  | Snd:         "{|X,Y|}   \<in> parts H ==> Y \<in> parts H"
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
    46
  | Body:        "Crypt K X \<in> parts H ==> X \<in> parts H"
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
    47
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
    48
inductive_set
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
    49
  analz :: "msg set => msg set"
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
    50
  for H :: "msg set"
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
    51
  where
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
    52
    Inj [intro,simp] :    "X \<in> H ==> X \<in> analz H"
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
    53
  | Fst:     "{|X,Y|} \<in> analz H ==> X \<in> analz H"
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
    54
  | Snd:     "{|X,Y|} \<in> analz H ==> Y \<in> analz H"
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
    55
  | Decrypt [dest]: 
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
    56
             "[|Crypt K X \<in> analz H; Key(invKey K): analz H|] ==> X \<in> analz H"
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
    57
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
    58
inductive_set
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
    59
  synth :: "msg set => msg set"
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
    60
  for H :: "msg set"
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
    61
  where
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
    62
    Inj    [intro]:   "X \<in> H ==> X \<in> synth H"
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
    63
  | Agent  [intro]:   "Agent agt \<in> synth H"
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
    64
  | MPair  [intro]:   "[|X \<in> synth H;  Y \<in> synth H|] ==> {|X,Y|} \<in> synth H"
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
    65
  | Crypt  [intro]:   "[|X \<in> synth H;  Key(K) \<in> H|] ==> Crypt K X \<in> synth H"
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
    66
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
    67
primrec initState
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
    68
where
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
    69
  initState_Alice:
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
    70
    "initState Alice = {Key (priEK Alice)} \<union> (Key ` pubEK ` agents)"
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
    71
| initState_Bob:
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
    72
    "initState Bob = {Key (priEK Bob)} \<union> (Key ` pubEK ` agents)"
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
    73
| initState_Spy:
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
    74
    "initState Spy        =  (Key ` priEK ` bad) \<union> (Key ` pubEK ` agents)"
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
    75
58310
91ea607a34d8 updated news
blanchet
parents: 58249
diff changeset
    76
datatype
48243
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
    77
  event = Says  agent agent msg
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
    78
        | Gets  agent       msg
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
    79
        | Notes agent       msg
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
    80
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
    81
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
    82
primrec knows :: "agent => event list => msg set"
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
    83
where
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
    84
  knows_Nil:   "knows A [] = initState A"
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
    85
| knows_Cons:
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
    86
    "knows A (ev # evs) =
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
    87
       (if A = Spy then 
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
    88
        (case ev of
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
    89
           Says A' B X => insert X (knows Spy evs)
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
    90
         | Gets A' X => knows Spy evs
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
    91
         | Notes A' X  => 
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
    92
             if A' \<in> bad then insert X (knows Spy evs) else knows Spy evs)
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
    93
        else
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
    94
        (case ev of
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
    95
           Says A' B X => 
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
    96
             if A'=A then insert X (knows A evs) else knows A evs
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
    97
         | Gets A' X    => 
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
    98
             if A'=A then insert X (knows A evs) else knows A evs
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
    99
         | Notes A' X    => 
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
   100
             if A'=A then insert X (knows A evs) else knows A evs))"
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
   101
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
   102
abbreviation (input)
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
   103
  spies  :: "event list => msg set" where
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
   104
  "spies == knows Spy"
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
   105
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
   106
primrec used :: "event list => msg set"
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
   107
where
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
   108
  used_Nil:   "used []         = Union (parts ` initState ` agents)"
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
   109
| used_Cons:  "used (ev # evs) =
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
   110
                     (case ev of
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
   111
                        Says A B X => parts {X} \<union> used evs
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
   112
                      | Gets A X   => used evs
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
   113
                      | Notes A X  => parts {X} \<union> used evs)"
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
   114
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
   115
subsection {* Preparations for sets *}
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
   116
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
   117
fun find_first :: "('a => 'b option) => 'a list => 'b option"
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
   118
where
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
   119
  "find_first f [] = None"
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
   120
| "find_first f (x # xs) = (case f x of Some y => Some y | None => find_first f xs)"
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
   121
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
   122
consts cps_of_set :: "'a set => ('a => term list option) => term list option"
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
   123
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
   124
lemma
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
   125
  [code]: "cps_of_set (set xs) f = find_first f xs"
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
   126
sorry
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
   127
51143
0a2371e7ced3 two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents: 48618
diff changeset
   128
consts pos_cps_of_set :: "'a set => ('a => (bool * term list) option) => natural => (bool * term list) option"
0a2371e7ced3 two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents: 48618
diff changeset
   129
consts neg_cps_of_set :: "'a set => ('a Quickcheck_Exhaustive.unknown => term list Quickcheck_Exhaustive.three_valued) => natural => term list Quickcheck_Exhaustive.three_valued"
48243
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
   130
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
   131
lemma
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
   132
  [code]: "pos_cps_of_set (set xs) f i = find_first f xs"
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
   133
sorry
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
   134
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
   135
consts find_first' :: "('b Quickcheck_Exhaustive.unknown => 'a Quickcheck_Exhaustive.three_valued)
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
   136
    => 'b list => 'a Quickcheck_Exhaustive.three_valued"
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
   137
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
   138
lemma [code]:
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
   139
  "find_first' f [] = Quickcheck_Exhaustive.No_value"
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
   140
  "find_first' f (x # xs) = (case f (Quickcheck_Exhaustive.Known x) of Quickcheck_Exhaustive.No_value => find_first' f xs | Quickcheck_Exhaustive.Value x => Quickcheck_Exhaustive.Value x | Quickcheck_Exhaustive.Unknown_value => (case find_first' f xs of Quickcheck_Exhaustive.Value x => Quickcheck_Exhaustive.Value x | _ => Quickcheck_Exhaustive.Unknown_value))"
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
   141
sorry
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
   142
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
   143
lemma
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
   144
  [code]: "neg_cps_of_set (set xs) f i = find_first' f xs"
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
   145
sorry
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
   146
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
   147
setup {*
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
   148
let
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
   149
  val Fun = Predicate_Compile_Aux.Fun
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
   150
  val Input = Predicate_Compile_Aux.Input
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
   151
  val Output = Predicate_Compile_Aux.Output
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
   152
  val Bool = Predicate_Compile_Aux.Bool
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
   153
  val oi = Fun (Output, Fun (Input, Bool))
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
   154
  val ii = Fun (Input, Fun (Input, Bool))
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
   155
  fun of_set compfuns (Type ("fun", [T, _])) =
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
   156
    case body_type (Predicate_Compile_Aux.mk_monadT compfuns T) of
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
   157
      Type ("Quickcheck_Exhaustive.three_valued", _) => 
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
   158
        Const(@{const_name neg_cps_of_set}, HOLogic.mk_setT T --> (Predicate_Compile_Aux.mk_monadT compfuns T))
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
   159
    | Type ("Predicate.pred", _) => Const(@{const_name pred_of_set}, HOLogic.mk_setT T --> Predicate_Compile_Aux.mk_monadT compfuns T)
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
   160
    | _ => Const(@{const_name pos_cps_of_set}, HOLogic.mk_setT T --> (Predicate_Compile_Aux.mk_monadT compfuns T))
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
   161
  fun member compfuns (U as Type ("fun", [T, _])) =
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
   162
    (absdummy T (absdummy (HOLogic.mk_setT T) (Predicate_Compile_Aux.mk_if compfuns
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
   163
      (Const (@{const_name "Set.member"}, T --> HOLogic.mk_setT T --> @{typ bool}) $ Bound 1 $ Bound 0))))
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
   164
 
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
   165
in
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
   166
  Core_Data.force_modes_and_compilations @{const_name Set.member}
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
   167
    [(oi, (of_set, false)), (ii, (member, false))]
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
   168
end
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
   169
*}
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
   170
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
   171
subsection {* Derived equations for analz, parts and synth *}
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
   172
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
   173
lemma [code]:
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
   174
  "analz H = (let
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
   175
     H' = H \<union> (Union ((%m. case m of {|X, Y|} => {X, Y} | Crypt K X => if Key (invKey K) : H then {X} else {} | _ => {}) ` H))
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
   176
   in if H' = H then H else analz H')"
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
   177
sorry
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
   178
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
   179
lemma [code]:
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
   180
  "parts H = (let
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
   181
     H' = H \<union> (Union ((%m. case m of {|X, Y|} => {X, Y} | Crypt K X => {X} | _ => {}) ` H))
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
   182
   in if H' = H then H else parts H')"
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
   183
sorry
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
   184
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
   185
definition synth' :: "msg set => msg => bool"
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
   186
where
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
   187
  "synth' H m = (m : synth H)"
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
   188
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
   189
lemmas [code_pred_intro] = synth.intros[folded synth'_def]
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
   190
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
   191
code_pred [generator_cps] synth' unfolding synth'_def by (rule synth.cases) fastforce+
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
   192
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
   193
setup {* Predicate_Compile_Data.ignore_consts [@{const_name analz}, @{const_name knows}] *}
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
   194
declare ListMem_iff[symmetric, code_pred_inline]
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
   195
declare [[quickcheck_timing]]
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
   196
58813
wenzelm
parents: 58310
diff changeset
   197
setup Exhaustive_Generators.setup_exhaustive_datatype_interpretation
48243
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
   198
declare [[quickcheck_full_support = false]]
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
   199
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
   200
end