[STATEMENT]
lemma kappa_mu_nu_ni_kappa_mu_nu:
  "kappa_mu_nu_ni f \<longleftrightarrow> kappa_mu_nu f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. kappa_mu_nu_ni f = kappa_mu_nu f
[PROOF STEP]
by (simp add: kappa_mu_nu_def kappa_mu_nu_ni_def ni_def)


[STATEMENT]
lemma n_omega_zero:
  "n(x\<^sup>\<omega>) = bot \<longleftrightarrow> n(x\<^sup>\<star>) = bot \<and> x\<^sup>\<omega> \<le> x\<^sup>\<star> * bot"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (n (x\<^sup>\<omega>) = bot) = (n (x\<^sup>\<star>) = bot \<and> x\<^sup>\<omega> \<le> x\<^sup>\<star> * bot)
[PROOF STEP]
by (metis sup_bot_right order.eq_iff mult_left_zero n_mult_bot n_split_omega star_bot_below_omega)


[STATEMENT]
lemma i_expand_const_NoMsg[simp]: "(\<lambda>n. \<NoMsg>) \<odot>\<^sub>i k = (\<lambda>n. \<NoMsg>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>n. NoMsg) \<odot> k = (\<lambda>n. NoMsg)
[PROOF STEP]
by (simp add: i_expand_def ilist_eq_iff)


[STATEMENT]
lemma decT_decT [simp]: "\<down>\<^sub>\<tau> n k (\<down>\<^sub>\<tau> n' (k + n) T) = \<down>\<^sub>\<tau> (n + n') k T"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<down>\<^sub>\<tau> n k (\<down>\<^sub>\<tau> n' (k + n) T) = \<down>\<^sub>\<tau> (n + n') k T
[PROOF STEP]
by (induct n arbitrary: k T) simp_all


[STATEMENT]
lemma spy_method_via_h_framework_code[code] :
  "spy_method_via_h_framework M m = (let
      tables = (compute_ofsm_tables M (size M - 1));
      distMap = mapping_of (map (\<lambda> (q1,q2) . ((q1,q2), get_distinguishing_sequence_from_ofsm_tables_with_provided_tables tables M q1 q2))
                        (filter (\<lambda> qq . fst qq \<noteq> snd qq) (List.product (states_as_list M) (states_as_list M))));
      distHelper = (\<lambda> q1 q2 . if q1 \<in> states M \<and> q2 \<in> states M \<and> q1 \<noteq> q2 then the (Mapping.lookup distMap (q1,q2)) else get_distinguishing_sequence_from_ofsm_tables M q1 q2);

      hsiMap = mapping_of (map (\<lambda> q . (q,from_list (map (\<lambda>q' . distHelper q q') (filter ((\<noteq>) q) (states_as_list M))))) (states_as_list M));
      distFun = (\<lambda> k q . if q \<in> states M then the (Mapping.lookup hsiMap q) else get_HSI M q)
    in h_framework_static_with_simple_graph M distFun m)"
(is "?f1 = ?f2")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. spy_method_via_h_framework M m = (let tables = compute_ofsm_tables M (FSM.size M - 1); distMap = mapping_of (map (\<lambda>(q1, q2). ((q1, q2), get_distinguishing_sequence_from_ofsm_tables_with_provided_tables tables M q1 q2)) (filter (\<lambda>qq. fst qq \<noteq> snd qq) (List.product (states_as_list M) (states_as_list M)))); distHelper = \<lambda>q1 q2. if q1 \<in> FSM.states M \<and> q2 \<in> FSM.states M \<and> q1 \<noteq> q2 then the (Mapping.lookup distMap (q1, q2)) else get_distinguishing_sequence_from_ofsm_tables M q1 q2; hsiMap = mapping_of (map (\<lambda>q. (q, from_list (map (distHelper q) (filter ((\<noteq>) q) (states_as_list M))))) (states_as_list M)); distFun = \<lambda>k q. if q \<in> FSM.states M then the (Mapping.lookup hsiMap q) else get_HSI M q in h_framework_static_with_simple_graph M distFun m)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. spy_method_via_h_framework M m = (let tables = compute_ofsm_tables M (FSM.size M - 1); distMap = mapping_of (map (\<lambda>(q1, q2). ((q1, q2), get_distinguishing_sequence_from_ofsm_tables_with_provided_tables tables M q1 q2)) (filter (\<lambda>qq. fst qq \<noteq> snd qq) (List.product (states_as_list M) (states_as_list M)))); distHelper = \<lambda>q1 q2. if q1 \<in> FSM.states M \<and> q2 \<in> FSM.states M \<and> q1 \<noteq> q2 then the (Mapping.lookup distMap (q1, q2)) else get_distinguishing_sequence_from_ofsm_tables M q1 q2; hsiMap = mapping_of (map (\<lambda>q. (q, from_list (map (distHelper q) (filter ((\<noteq>) q) (states_as_list M))))) (states_as_list M)); distFun = \<lambda>k q. if q \<in> FSM.states M then the (Mapping.lookup hsiMap q) else get_HSI M q in h_framework_static_with_simple_graph M distFun m)
[PROOF STEP]
define hsiMap' where "hsiMap' = mapping_of (map (\<lambda> q . (q,from_list (map (\<lambda>q' . get_distinguishing_sequence_from_ofsm_tables M q q') (filter ((\<noteq>) q) (states_as_list M))))) (states_as_list M))"
[PROOF STATE]
proof (state)
this:
hsiMap' = mapping_of (map (\<lambda>q. (q, from_list (map (get_distinguishing_sequence_from_ofsm_tables M q) (filter ((\<noteq>) q) (states_as_list M))))) (states_as_list M))

goal (1 subgoal):
 1. spy_method_via_h_framework M m = (let tables = compute_ofsm_tables M (FSM.size M - 1); distMap = mapping_of (map (\<lambda>(q1, q2). ((q1, q2), get_distinguishing_sequence_from_ofsm_tables_with_provided_tables tables M q1 q2)) (filter (\<lambda>qq. fst qq \<noteq> snd qq) (List.product (states_as_list M) (states_as_list M)))); distHelper = \<lambda>q1 q2. if q1 \<in> FSM.states M \<and> q2 \<in> FSM.states M \<and> q1 \<noteq> q2 then the (Mapping.lookup distMap (q1, q2)) else get_distinguishing_sequence_from_ofsm_tables M q1 q2; hsiMap = mapping_of (map (\<lambda>q. (q, from_list (map (distHelper q) (filter ((\<noteq>) q) (states_as_list M))))) (states_as_list M)); distFun = \<lambda>k q. if q \<in> FSM.states M then the (Mapping.lookup hsiMap q) else get_HSI M q in h_framework_static_with_simple_graph M distFun m)
[PROOF STEP]
define distFun' where "distFun' = (\<lambda> M q . if q \<in> states M then the (Mapping.lookup hsiMap' q) else get_HSI M q)"
[PROOF STATE]
proof (state)
this:
distFun' = (\<lambda>M q. if q \<in> FSM.states M then the (Mapping.lookup hsiMap' q) else get_HSI M q)

goal (1 subgoal):
 1. spy_method_via_h_framework M m = (let tables = compute_ofsm_tables M (FSM.size M - 1); distMap = mapping_of (map (\<lambda>(q1, q2). ((q1, q2), get_distinguishing_sequence_from_ofsm_tables_with_provided_tables tables M q1 q2)) (filter (\<lambda>qq. fst qq \<noteq> snd qq) (List.product (states_as_list M) (states_as_list M)))); distHelper = \<lambda>q1 q2. if q1 \<in> FSM.states M \<and> q2 \<in> FSM.states M \<and> q1 \<noteq> q2 then the (Mapping.lookup distMap (q1, q2)) else get_distinguishing_sequence_from_ofsm_tables M q1 q2; hsiMap = mapping_of (map (\<lambda>q. (q, from_list (map (distHelper q) (filter ((\<noteq>) q) (states_as_list M))))) (states_as_list M)); distFun = \<lambda>k q. if q \<in> FSM.states M then the (Mapping.lookup hsiMap q) else get_HSI M q in h_framework_static_with_simple_graph M distFun m)
[PROOF STEP]
have *: "?f2 = h_framework_static_with_simple_graph M (\<lambda> k q . distFun' M q) m"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (let tables = compute_ofsm_tables M (FSM.size M - 1); distMap = mapping_of (map (\<lambda>(q1, q2). ((q1, q2), get_distinguishing_sequence_from_ofsm_tables_with_provided_tables tables M q1 q2)) (filter (\<lambda>qq. fst qq \<noteq> snd qq) (List.product (states_as_list M) (states_as_list M)))); distHelper = \<lambda>q1 q2. if q1 \<in> FSM.states M \<and> q2 \<in> FSM.states M \<and> q1 \<noteq> q2 then the (Mapping.lookup distMap (q1, q2)) else get_distinguishing_sequence_from_ofsm_tables M q1 q2; hsiMap = mapping_of (map (\<lambda>q. (q, from_list (map (distHelper q) (filter ((\<noteq>) q) (states_as_list M))))) (states_as_list M)); distFun = \<lambda>k q. if q \<in> FSM.states M then the (Mapping.lookup hsiMap q) else get_HSI M q in h_framework_static_with_simple_graph M distFun m) = h_framework_static_with_simple_graph M (\<lambda>k. distFun' M) m
[PROOF STEP]
unfolding distFun'_def hsiMap'_def Let_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. h_framework_static_with_simple_graph M (\<lambda>k q. if q \<in> FSM.states M then the (Mapping.lookup (mapping_of (map (\<lambda>q. (q, from_list (map (\<lambda>q2. if q \<in> FSM.states M \<and> q2 \<in> FSM.states M \<and> q \<noteq> q2 then the (Mapping.lookup (mapping_of (map (\<lambda>(q1, q2). ((q1, q2), get_distinguishing_sequence_from_ofsm_tables_with_provided_tables (compute_ofsm_tables M (FSM.size M - 1)) M q1 q2)) (filter (\<lambda>qq. fst qq \<noteq> snd qq) (List.product (states_as_list M) (states_as_list M))))) (q, q2)) else get_distinguishing_sequence_from_ofsm_tables M q q2) (filter ((\<noteq>) q) (states_as_list M))))) (states_as_list M))) q) else get_HSI M q) m = h_framework_static_with_simple_graph M (\<lambda>k q. if q \<in> FSM.states M then the (Mapping.lookup (mapping_of (map (\<lambda>q. (q, from_list (map (get_distinguishing_sequence_from_ofsm_tables M q) (filter ((\<noteq>) q) (states_as_list M))))) (states_as_list M))) q) else get_HSI M q) m
[PROOF STEP]
apply (subst (2) get_distinguishing_sequence_from_ofsm_tables_precomputed[of M])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. h_framework_static_with_simple_graph M (\<lambda>k q. if q \<in> FSM.states M then the (Mapping.lookup (mapping_of (map (\<lambda>q. (q, from_list (map (\<lambda>q2. if q \<in> FSM.states M \<and> q2 \<in> FSM.states M \<and> q \<noteq> q2 then the (Mapping.lookup (mapping_of (map (\<lambda>(q1, q2). ((q1, q2), get_distinguishing_sequence_from_ofsm_tables_with_provided_tables (compute_ofsm_tables M (FSM.size M - 1)) M q1 q2)) (filter (\<lambda>qq. fst qq \<noteq> snd qq) (List.product (states_as_list M) (states_as_list M))))) (q, q2)) else get_distinguishing_sequence_from_ofsm_tables M q q2) (filter ((\<noteq>) q) (states_as_list M))))) (states_as_list M))) q) else get_HSI M q) m = h_framework_static_with_simple_graph M (\<lambda>k q. if q \<in> FSM.states M then the (Mapping.lookup (mapping_of (map (\<lambda>q. (q, from_list (map ((let tables = compute_ofsm_tables M (FSM.size M - 1); distMap = mapping_of (map (\<lambda>(q1, q2). ((q1, q2), get_distinguishing_sequence_from_ofsm_tables_with_provided_tables tables M q1 q2)) (filter (\<lambda>qq. fst qq \<noteq> snd qq) (List.product (states_as_list M) (states_as_list M)))); distHelper = \<lambda>q1 q2. if q1 \<in> FSM.states M \<and> q2 \<in> FSM.states M \<and> q1 \<noteq> q2 then the (Mapping.lookup distMap (q1, q2)) else get_distinguishing_sequence_from_ofsm_tables M q1 q2 in distHelper) q) (filter ((\<noteq>) q) (states_as_list M))))) (states_as_list M))) q) else get_HSI M q) m
[PROOF STEP]
unfolding Let_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. h_framework_static_with_simple_graph M (\<lambda>k q. if q \<in> FSM.states M then the (Mapping.lookup (mapping_of (map (\<lambda>q. (q, from_list (map (\<lambda>q2. if q \<in> FSM.states M \<and> q2 \<in> FSM.states M \<and> q \<noteq> q2 then the (Mapping.lookup (mapping_of (map (\<lambda>(q1, q2). ((q1, q2), get_distinguishing_sequence_from_ofsm_tables_with_provided_tables (compute_ofsm_tables M (FSM.size M - 1)) M q1 q2)) (filter (\<lambda>qq. fst qq \<noteq> snd qq) (List.product (states_as_list M) (states_as_list M))))) (q, q2)) else get_distinguishing_sequence_from_ofsm_tables M q q2) (filter ((\<noteq>) q) (states_as_list M))))) (states_as_list M))) q) else get_HSI M q) m = h_framework_static_with_simple_graph M (\<lambda>k q. if q \<in> FSM.states M then the (Mapping.lookup (mapping_of (map (\<lambda>q. (q, from_list (map (\<lambda>q2. if q \<in> FSM.states M \<and> q2 \<in> FSM.states M \<and> q \<noteq> q2 then the (Mapping.lookup (mapping_of (map (\<lambda>(q1, q2). ((q1, q2), get_distinguishing_sequence_from_ofsm_tables_with_provided_tables (compute_ofsm_tables M (FSM.size M - 1)) M q1 q2)) (filter (\<lambda>qq. fst qq \<noteq> snd qq) (List.product (states_as_list M) (states_as_list M))))) (q, q2)) else get_distinguishing_sequence_from_ofsm_tables M q q2) (filter ((\<noteq>) q) (states_as_list M))))) (states_as_list M))) q) else get_HSI M q) m
[PROOF STEP]
by presburger
[PROOF STATE]
proof (state)
this:
(let tables = compute_ofsm_tables M (FSM.size M - 1); distMap = mapping_of (map (\<lambda>(q1, q2). ((q1, q2), get_distinguishing_sequence_from_ofsm_tables_with_provided_tables tables M q1 q2)) (filter (\<lambda>qq. fst qq \<noteq> snd qq) (List.product (states_as_list M) (states_as_list M)))); distHelper = \<lambda>q1 q2. if q1 \<in> FSM.states M \<and> q2 \<in> FSM.states M \<and> q1 \<noteq> q2 then the (Mapping.lookup distMap (q1, q2)) else get_distinguishing_sequence_from_ofsm_tables M q1 q2; hsiMap = mapping_of (map (\<lambda>q. (q, from_list (map (distHelper q) (filter ((\<noteq>) q) (states_as_list M))))) (states_as_list M)); distFun = \<lambda>k q. if q \<in> FSM.states M then the (Mapping.lookup hsiMap q) else get_HSI M q in h_framework_static_with_simple_graph M distFun m) = h_framework_static_with_simple_graph M (\<lambda>k. distFun' M) m

goal (1 subgoal):
 1. spy_method_via_h_framework M m = (let tables = compute_ofsm_tables M (FSM.size M - 1); distMap = mapping_of (map (\<lambda>(q1, q2). ((q1, q2), get_distinguishing_sequence_from_ofsm_tables_with_provided_tables tables M q1 q2)) (filter (\<lambda>qq. fst qq \<noteq> snd qq) (List.product (states_as_list M) (states_as_list M)))); distHelper = \<lambda>q1 q2. if q1 \<in> FSM.states M \<and> q2 \<in> FSM.states M \<and> q1 \<noteq> q2 then the (Mapping.lookup distMap (q1, q2)) else get_distinguishing_sequence_from_ofsm_tables M q1 q2; hsiMap = mapping_of (map (\<lambda>q. (q, from_list (map (distHelper q) (filter ((\<noteq>) q) (states_as_list M))))) (states_as_list M)); distFun = \<lambda>k q. if q \<in> FSM.states M then the (Mapping.lookup hsiMap q) else get_HSI M q in h_framework_static_with_simple_graph M distFun m)
[PROOF STEP]
define hsiMap where "hsiMap = map_of (map (\<lambda> q . (q,from_list (map (\<lambda>q' . get_distinguishing_sequence_from_ofsm_tables M q q') (filter ((\<noteq>) q) (states_as_list M))))) (states_as_list M))"
[PROOF STATE]
proof (state)
this:
hsiMap = map_of (map (\<lambda>q. (q, from_list (map (get_distinguishing_sequence_from_ofsm_tables M q) (filter ((\<noteq>) q) (states_as_list M))))) (states_as_list M))

goal (1 subgoal):
 1. spy_method_via_h_framework M m = (let tables = compute_ofsm_tables M (FSM.size M - 1); distMap = mapping_of (map (\<lambda>(q1, q2). ((q1, q2), get_distinguishing_sequence_from_ofsm_tables_with_provided_tables tables M q1 q2)) (filter (\<lambda>qq. fst qq \<noteq> snd qq) (List.product (states_as_list M) (states_as_list M)))); distHelper = \<lambda>q1 q2. if q1 \<in> FSM.states M \<and> q2 \<in> FSM.states M \<and> q1 \<noteq> q2 then the (Mapping.lookup distMap (q1, q2)) else get_distinguishing_sequence_from_ofsm_tables M q1 q2; hsiMap = mapping_of (map (\<lambda>q. (q, from_list (map (distHelper q) (filter ((\<noteq>) q) (states_as_list M))))) (states_as_list M)); distFun = \<lambda>k q. if q \<in> FSM.states M then the (Mapping.lookup hsiMap q) else get_HSI M q in h_framework_static_with_simple_graph M distFun m)
[PROOF STEP]
define distFun where "distFun = (\<lambda> M q . if q \<in> states M then the (hsiMap q) else get_HSI M q)"
[PROOF STATE]
proof (state)
this:
distFun = (\<lambda>M q. if q \<in> FSM.states M then the (hsiMap q) else get_HSI M q)

goal (1 subgoal):
 1. spy_method_via_h_framework M m = (let tables = compute_ofsm_tables M (FSM.size M - 1); distMap = mapping_of (map (\<lambda>(q1, q2). ((q1, q2), get_distinguishing_sequence_from_ofsm_tables_with_provided_tables tables M q1 q2)) (filter (\<lambda>qq. fst qq \<noteq> snd qq) (List.product (states_as_list M) (states_as_list M)))); distHelper = \<lambda>q1 q2. if q1 \<in> FSM.states M \<and> q2 \<in> FSM.states M \<and> q1 \<noteq> q2 then the (Mapping.lookup distMap (q1, q2)) else get_distinguishing_sequence_from_ofsm_tables M q1 q2; hsiMap = mapping_of (map (\<lambda>q. (q, from_list (map (distHelper q) (filter ((\<noteq>) q) (states_as_list M))))) (states_as_list M)); distFun = \<lambda>k q. if q \<in> FSM.states M then the (Mapping.lookup hsiMap q) else get_HSI M q in h_framework_static_with_simple_graph M distFun m)
[PROOF STEP]
have "distinct (map fst (map (\<lambda> q . (q,from_list (map (\<lambda>q' . get_distinguishing_sequence_from_ofsm_tables M q q') (filter ((\<noteq>) q) (states_as_list M))))) (states_as_list M)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. distinct (map fst (map (\<lambda>q. (q, from_list (map (get_distinguishing_sequence_from_ofsm_tables M q) (filter ((\<noteq>) q) (states_as_list M))))) (states_as_list M)))
[PROOF STEP]
using states_as_list_distinct
[PROOF STATE]
proof (prove)
using this:
distinct (states_as_list ?M)

goal (1 subgoal):
 1. distinct (map fst (map (\<lambda>q. (q, from_list (map (get_distinguishing_sequence_from_ofsm_tables M q) (filter ((\<noteq>) q) (states_as_list M))))) (states_as_list M)))
[PROOF STEP]
by (metis map_pair_fst)
[PROOF STATE]
proof (state)
this:
distinct (map fst (map (\<lambda>q. (q, from_list (map (get_distinguishing_sequence_from_ofsm_tables M q) (filter ((\<noteq>) q) (states_as_list M))))) (states_as_list M)))

goal (1 subgoal):
 1. spy_method_via_h_framework M m = (let tables = compute_ofsm_tables M (FSM.size M - 1); distMap = mapping_of (map (\<lambda>(q1, q2). ((q1, q2), get_distinguishing_sequence_from_ofsm_tables_with_provided_tables tables M q1 q2)) (filter (\<lambda>qq. fst qq \<noteq> snd qq) (List.product (states_as_list M) (states_as_list M)))); distHelper = \<lambda>q1 q2. if q1 \<in> FSM.states M \<and> q2 \<in> FSM.states M \<and> q1 \<noteq> q2 then the (Mapping.lookup distMap (q1, q2)) else get_distinguishing_sequence_from_ofsm_tables M q1 q2; hsiMap = mapping_of (map (\<lambda>q. (q, from_list (map (distHelper q) (filter ((\<noteq>) q) (states_as_list M))))) (states_as_list M)); distFun = \<lambda>k q. if q \<in> FSM.states M then the (Mapping.lookup hsiMap q) else get_HSI M q in h_framework_static_with_simple_graph M distFun m)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
distinct (map fst (map (\<lambda>q. (q, from_list (map (get_distinguishing_sequence_from_ofsm_tables M q) (filter ((\<noteq>) q) (states_as_list M))))) (states_as_list M)))
[PROOF STEP]
have "Mapping.lookup hsiMap' = hsiMap"
[PROOF STATE]
proof (prove)
using this:
distinct (map fst (map (\<lambda>q. (q, from_list (map (get_distinguishing_sequence_from_ofsm_tables M q) (filter ((\<noteq>) q) (states_as_list M))))) (states_as_list M)))

goal (1 subgoal):
 1. Mapping.lookup hsiMap' = hsiMap
[PROOF STEP]
unfolding hsiMap_def hsiMap'_def
[PROOF STATE]
proof (prove)
using this:
distinct (map fst (map (\<lambda>q. (q, from_list (map (get_distinguishing_sequence_from_ofsm_tables M q) (filter ((\<noteq>) q) (states_as_list M))))) (states_as_list M)))

goal (1 subgoal):
 1. Mapping.lookup (mapping_of (map (\<lambda>q. (q, from_list (map (get_distinguishing_sequence_from_ofsm_tables M q) (filter ((\<noteq>) q) (states_as_list M))))) (states_as_list M))) = map_of (map (\<lambda>q. (q, from_list (map (get_distinguishing_sequence_from_ofsm_tables M q) (filter ((\<noteq>) q) (states_as_list M))))) (states_as_list M))
[PROOF STEP]
using mapping_of_map_of
[PROOF STATE]
proof (prove)
using this:
distinct (map fst (map (\<lambda>q. (q, from_list (map (get_distinguishing_sequence_from_ofsm_tables M q) (filter ((\<noteq>) q) (states_as_list M))))) (states_as_list M)))
distinct (map fst ?kvs) \<Longrightarrow> Mapping.lookup (mapping_of ?kvs) = map_of ?kvs

goal (1 subgoal):
 1. Mapping.lookup (mapping_of (map (\<lambda>q. (q, from_list (map (get_distinguishing_sequence_from_ofsm_tables M q) (filter ((\<noteq>) q) (states_as_list M))))) (states_as_list M))) = map_of (map (\<lambda>q. (q, from_list (map (get_distinguishing_sequence_from_ofsm_tables M q) (filter ((\<noteq>) q) (states_as_list M))))) (states_as_list M))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Mapping.lookup hsiMap' = hsiMap

goal (1 subgoal):
 1. spy_method_via_h_framework M m = (let tables = compute_ofsm_tables M (FSM.size M - 1); distMap = mapping_of (map (\<lambda>(q1, q2). ((q1, q2), get_distinguishing_sequence_from_ofsm_tables_with_provided_tables tables M q1 q2)) (filter (\<lambda>qq. fst qq \<noteq> snd qq) (List.product (states_as_list M) (states_as_list M)))); distHelper = \<lambda>q1 q2. if q1 \<in> FSM.states M \<and> q2 \<in> FSM.states M \<and> q1 \<noteq> q2 then the (Mapping.lookup distMap (q1, q2)) else get_distinguishing_sequence_from_ofsm_tables M q1 q2; hsiMap = mapping_of (map (\<lambda>q. (q, from_list (map (distHelper q) (filter ((\<noteq>) q) (states_as_list M))))) (states_as_list M)); distFun = \<lambda>k q. if q \<in> FSM.states M then the (Mapping.lookup hsiMap q) else get_HSI M q in h_framework_static_with_simple_graph M distFun m)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Mapping.lookup hsiMap' = hsiMap
[PROOF STEP]
have "distFun' = distFun"
[PROOF STATE]
proof (prove)
using this:
Mapping.lookup hsiMap' = hsiMap

goal (1 subgoal):
 1. distFun' = distFun
[PROOF STEP]
unfolding distFun_def distFun'_def
[PROOF STATE]
proof (prove)
using this:
Mapping.lookup hsiMap' = hsiMap

goal (1 subgoal):
 1. (\<lambda>M q. if q \<in> FSM.states M then the (Mapping.lookup hsiMap' q) else get_HSI M q) = (\<lambda>M q. if q \<in> FSM.states M then the (hsiMap q) else get_HSI M q)
[PROOF STEP]
by meson
[PROOF STATE]
proof (state)
this:
distFun' = distFun

goal (1 subgoal):
 1. spy_method_via_h_framework M m = (let tables = compute_ofsm_tables M (FSM.size M - 1); distMap = mapping_of (map (\<lambda>(q1, q2). ((q1, q2), get_distinguishing_sequence_from_ofsm_tables_with_provided_tables tables M q1 q2)) (filter (\<lambda>qq. fst qq \<noteq> snd qq) (List.product (states_as_list M) (states_as_list M)))); distHelper = \<lambda>q1 q2. if q1 \<in> FSM.states M \<and> q2 \<in> FSM.states M \<and> q1 \<noteq> q2 then the (Mapping.lookup distMap (q1, q2)) else get_distinguishing_sequence_from_ofsm_tables M q1 q2; hsiMap = mapping_of (map (\<lambda>q. (q, from_list (map (distHelper q) (filter ((\<noteq>) q) (states_as_list M))))) (states_as_list M)); distFun = \<lambda>k q. if q \<in> FSM.states M then the (Mapping.lookup hsiMap q) else get_HSI M q in h_framework_static_with_simple_graph M distFun m)
[PROOF STEP]
have **:"distFun M = get_HSI M"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. distFun M = get_HSI M
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. distFun M x = get_HSI M x
[PROOF STEP]
fix q
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. distFun M x = get_HSI M x
[PROOF STEP]
show "distFun M q = get_HSI M q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. distFun M q = get_HSI M q
[PROOF STEP]
proof (cases "q \<in> states M")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. q \<in> FSM.states M \<Longrightarrow> distFun M q = get_HSI M q
 2. q \<notin> FSM.states M \<Longrightarrow> distFun M q = get_HSI M q
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
q \<in> FSM.states M

goal (2 subgoals):
 1. q \<in> FSM.states M \<Longrightarrow> distFun M q = get_HSI M q
 2. q \<notin> FSM.states M \<Longrightarrow> distFun M q = get_HSI M q
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
q \<in> FSM.states M
[PROOF STEP]
have "q \<in> list.set (states_as_list M)"
[PROOF STATE]
proof (prove)
using this:
q \<in> FSM.states M

goal (1 subgoal):
 1. q \<in> list.set (states_as_list M)
[PROOF STEP]
using states_as_list_set
[PROOF STATE]
proof (prove)
using this:
q \<in> FSM.states M
list.set (states_as_list ?M) = FSM.states ?M

goal (1 subgoal):
 1. q \<in> list.set (states_as_list M)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
q \<in> list.set (states_as_list M)

goal (2 subgoals):
 1. q \<in> FSM.states M \<Longrightarrow> distFun M q = get_HSI M q
 2. q \<notin> FSM.states M \<Longrightarrow> distFun M q = get_HSI M q
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
q \<in> list.set (states_as_list M)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
q \<in> list.set (states_as_list M)

goal (1 subgoal):
 1. distFun M q = get_HSI M q
[PROOF STEP]
unfolding distFun_def hsiMap_def map_of_map_pair_entry get_HSI.simps
[PROOF STATE]
proof (prove)
using this:
q \<in> list.set (states_as_list M)

goal (1 subgoal):
 1. (if q \<in> FSM.states M then the (if q \<in> list.set (states_as_list M) then Some (from_list (map (get_distinguishing_sequence_from_ofsm_tables M q) (filter ((\<noteq>) q) (states_as_list M)))) else None) else from_list (map (get_distinguishing_sequence_from_ofsm_tables M q) (filter ((\<noteq>) q) (states_as_list M)))) = from_list (map (get_distinguishing_sequence_from_ofsm_tables M q) (filter ((\<noteq>) q) (states_as_list M)))
[PROOF STEP]
using True
[PROOF STATE]
proof (prove)
using this:
q \<in> list.set (states_as_list M)
q \<in> FSM.states M

goal (1 subgoal):
 1. (if q \<in> FSM.states M then the (if q \<in> list.set (states_as_list M) then Some (from_list (map (get_distinguishing_sequence_from_ofsm_tables M q) (filter ((\<noteq>) q) (states_as_list M)))) else None) else from_list (map (get_distinguishing_sequence_from_ofsm_tables M q) (filter ((\<noteq>) q) (states_as_list M)))) = from_list (map (get_distinguishing_sequence_from_ofsm_tables M q) (filter ((\<noteq>) q) (states_as_list M)))
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
distFun M q = get_HSI M q

goal (1 subgoal):
 1. q \<notin> FSM.states M \<Longrightarrow> distFun M q = get_HSI M q
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. q \<notin> FSM.states M \<Longrightarrow> distFun M q = get_HSI M q
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
q \<notin> FSM.states M

goal (1 subgoal):
 1. q \<notin> FSM.states M \<Longrightarrow> distFun M q = get_HSI M q
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
q \<notin> FSM.states M
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
q \<notin> FSM.states M

goal (1 subgoal):
 1. distFun M q = get_HSI M q
[PROOF STEP]
using distFun_def
[PROOF STATE]
proof (prove)
using this:
q \<notin> FSM.states M
distFun = (\<lambda>M q. if q \<in> FSM.states M then the (hsiMap q) else get_HSI M q)

goal (1 subgoal):
 1. distFun M q = get_HSI M q
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
distFun M q = get_HSI M q

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
distFun M q = get_HSI M q

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
distFun M = get_HSI M

goal (1 subgoal):
 1. spy_method_via_h_framework M m = (let tables = compute_ofsm_tables M (FSM.size M - 1); distMap = mapping_of (map (\<lambda>(q1, q2). ((q1, q2), get_distinguishing_sequence_from_ofsm_tables_with_provided_tables tables M q1 q2)) (filter (\<lambda>qq. fst qq \<noteq> snd qq) (List.product (states_as_list M) (states_as_list M)))); distHelper = \<lambda>q1 q2. if q1 \<in> FSM.states M \<and> q2 \<in> FSM.states M \<and> q1 \<noteq> q2 then the (Mapping.lookup distMap (q1, q2)) else get_distinguishing_sequence_from_ofsm_tables M q1 q2; hsiMap = mapping_of (map (\<lambda>q. (q, from_list (map (distHelper q) (filter ((\<noteq>) q) (states_as_list M))))) (states_as_list M)); distFun = \<lambda>k q. if q \<in> FSM.states M then the (Mapping.lookup hsiMap q) else get_HSI M q in h_framework_static_with_simple_graph M distFun m)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. spy_method_via_h_framework M m = (let tables = compute_ofsm_tables M (FSM.size M - 1); distMap = mapping_of (map (\<lambda>(q1, q2). ((q1, q2), get_distinguishing_sequence_from_ofsm_tables_with_provided_tables tables M q1 q2)) (filter (\<lambda>qq. fst qq \<noteq> snd qq) (List.product (states_as_list M) (states_as_list M)))); distHelper = \<lambda>q1 q2. if q1 \<in> FSM.states M \<and> q2 \<in> FSM.states M \<and> q1 \<noteq> q2 then the (Mapping.lookup distMap (q1, q2)) else get_distinguishing_sequence_from_ofsm_tables M q1 q2; hsiMap = mapping_of (map (\<lambda>q. (q, from_list (map (distHelper q) (filter ((\<noteq>) q) (states_as_list M))))) (states_as_list M)); distFun = \<lambda>k q. if q \<in> FSM.states M then the (Mapping.lookup hsiMap q) else get_HSI M q in h_framework_static_with_simple_graph M distFun m)
[PROOF STEP]
unfolding * ** \<open>distFun' = distFun\<close> spy_method_via_h_framework_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. h_framework_static_with_simple_graph M (\<lambda>k. get_HSI M) m = h_framework_static_with_simple_graph M (\<lambda>k. get_HSI M) m
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
spy_method_via_h_framework M m = (let tables = compute_ofsm_tables M (FSM.size M - 1); distMap = mapping_of (map (\<lambda>(q1, q2). ((q1, q2), get_distinguishing_sequence_from_ofsm_tables_with_provided_tables tables M q1 q2)) (filter (\<lambda>qq. fst qq \<noteq> snd qq) (List.product (states_as_list M) (states_as_list M)))); distHelper = \<lambda>q1 q2. if q1 \<in> FSM.states M \<and> q2 \<in> FSM.states M \<and> q1 \<noteq> q2 then the (Mapping.lookup distMap (q1, q2)) else get_distinguishing_sequence_from_ofsm_tables M q1 q2; hsiMap = mapping_of (map (\<lambda>q. (q, from_list (map (distHelper q) (filter ((\<noteq>) q) (states_as_list M))))) (states_as_list M)); distFun = \<lambda>k q. if q \<in> FSM.states M then the (Mapping.lookup hsiMap q) else get_HSI M q in h_framework_static_with_simple_graph M distFun m)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma allocationProperty:
  "a \<in> possible_allocations_rel G N \<longleftrightarrow>
   runiq a & runiq (a\<inverse>) & (Domain a) partitions G & Range a \<subseteq> N"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (a \<in> possible_allocations_rel G N) = (runiq a \<and> runiq (a\<inverse>) \<and> Domain a partitions G \<and> Range a \<subseteq> N)
[PROOF STEP]
using allocationRightUniqueRangeDomain lm010
[PROOF STATE]
proof (prove)
using this:
?a \<in> possible_allocations_rel ?G ?N \<Longrightarrow> runiq ?a \<and> runiq (?a\<inverse>) \<and> Domain ?a partitions ?G \<and> Range ?a \<subseteq> ?N
\<lbrakk>runiq ?a; runiq (?a\<inverse>); Domain ?a partitions ?G; Range ?a \<subseteq> ?N\<rbrakk> \<Longrightarrow> ?a \<in> possible_allocations_rel ?G ?N

goal (1 subgoal):
 1. (a \<in> possible_allocations_rel G N) = (runiq a \<and> runiq (a\<inverse>) \<and> Domain a partitions G \<and> Range a \<subseteq> N)
[PROOF STEP]
by blast


[STATEMENT]
lemma "i < n \<Longrightarrow> (v \<cdot>\<^sub>v unit_vec n i) $ i = (v::'a::{monoid_mult,times,zero_neq_one})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i < n \<Longrightarrow> (v \<cdot>\<^sub>v unit_vec n i) $ i = v
[PROOF STEP]
by(auto)


[STATEMENT]
lemma finite_FV_FVoption: "finite (FV t) \<and> finite (FVoption s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (FV t) \<and> finite (FVoption s)
[PROOF STEP]
by(induct _ t _ s rule: compat_sterm_sterm_option.induct, simp_all)


[STATEMENT]
lemma not_simple\<^sub>s\<^sub>t\<^sub>p_elim:
  assumes "\<not>simple\<^sub>s\<^sub>t\<^sub>p x"
  shows "(\<exists>ts. x = Send ts \<and> (\<nexists>y. ts = [Var y])) \<or>
         (\<exists>a t t'. x = Equality a t t') \<or>
         (\<exists>X F. x = Inequality X F \<and> (\<nexists>\<I>. ineq_model \<I> X F))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<exists>ts. x = send\<langle>ts\<rangle>\<^sub>s\<^sub>t \<and> (\<nexists>y. ts = [Var y])) \<or> (\<exists>a t t'. x = \<langle>a: t \<doteq> t'\<rangle>\<^sub>s\<^sub>t) \<or> (\<exists>X F. x = \<forall>X\<langle>\<or>\<noteq>: F\<rangle>\<^sub>s\<^sub>t \<and> (\<nexists>\<I>. ineq_model \<I> X F))
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<not> simple\<^sub>s\<^sub>t\<^sub>p x

goal (1 subgoal):
 1. (\<exists>ts. x = send\<langle>ts\<rangle>\<^sub>s\<^sub>t \<and> (\<nexists>y. ts = [Var y])) \<or> (\<exists>a t t'. x = \<langle>a: t \<doteq> t'\<rangle>\<^sub>s\<^sub>t) \<or> (\<exists>X F. x = \<forall>X\<langle>\<or>\<noteq>: F\<rangle>\<^sub>s\<^sub>t \<and> (\<nexists>\<I>. ineq_model \<I> X F))
[PROOF STEP]
by (cases x) (fastforce elim: simple\<^sub>s\<^sub>t\<^sub>p.elims)+


[STATEMENT]
lemma strand_sem_d_if_c: "\<I> \<Turnstile>\<^sub>c \<langle>S,\<theta>\<rangle> \<Longrightarrow> \<I> \<Turnstile> \<langle>S,\<theta>\<rangle>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<I> \<Turnstile>\<^sub>c \<langle>S,\<theta>\<rangle> \<Longrightarrow> \<I> \<Turnstile> \<langle>S,\<theta>\<rangle>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<I> \<Turnstile>\<^sub>c \<langle>S,\<theta>\<rangle> \<Longrightarrow> \<I> \<Turnstile> \<langle>S,\<theta>\<rangle>
[PROOF STEP]
assume *: "\<I> \<Turnstile>\<^sub>c \<langle>S,\<theta>\<rangle>"
[PROOF STATE]
proof (state)
this:
\<I> \<Turnstile>\<^sub>c \<langle>S,\<theta>\<rangle>

goal (1 subgoal):
 1. \<I> \<Turnstile>\<^sub>c \<langle>S,\<theta>\<rangle> \<Longrightarrow> \<I> \<Turnstile> \<langle>S,\<theta>\<rangle>
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
\<I> \<Turnstile>\<^sub>c \<langle>S,\<theta>\<rangle>

goal (1 subgoal):
 1. \<I> \<Turnstile>\<^sub>c \<langle>S,\<theta>\<rangle> \<Longrightarrow> \<I> \<Turnstile> \<langle>S,\<theta>\<rangle>
[PROOF STEP]
fix M
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<I> \<Turnstile>\<^sub>c \<langle>S,\<theta>\<rangle> \<Longrightarrow> \<I> \<Turnstile> \<langle>S,\<theta>\<rangle>
[PROOF STEP]
have "\<lbrakk>M; S\<rbrakk>\<^sub>c \<I> \<Longrightarrow> \<lbrakk>M; S\<rbrakk>\<^sub>d \<I>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>M; S\<rbrakk>\<^sub>c \<I> \<Longrightarrow> \<lbrakk>M; S\<rbrakk>\<^sub>d \<I>
[PROOF STEP]
proof (induction S rule: strand_sem_induct)
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<And>M. \<lbrakk>M; []\<rbrakk>\<^sub>c \<I> \<Longrightarrow> \<lbrakk>M; []\<rbrakk>\<^sub>d \<I>
 2. \<And>M ts S. \<lbrakk>\<And>x. \<lbrakk>M; S\<rbrakk>\<^sub>c \<I> \<Longrightarrow> \<lbrakk>M; S\<rbrakk>\<^sub>d \<I>; \<lbrakk>M; send\<langle>ts\<rangle>\<^sub>s\<^sub>t # S\<rbrakk>\<^sub>c \<I>\<rbrakk> \<Longrightarrow> \<lbrakk>M; send\<langle>ts\<rangle>\<^sub>s\<^sub>t # S\<rbrakk>\<^sub>d \<I>
 3. \<And>M ts S. \<lbrakk>\<And>x. \<lbrakk>(set ts \<cdot>\<^sub>s\<^sub>e\<^sub>t x) \<union> M; S\<rbrakk>\<^sub>c \<I> \<Longrightarrow> \<lbrakk>(set ts \<cdot>\<^sub>s\<^sub>e\<^sub>t x) \<union> M; S\<rbrakk>\<^sub>d \<I>; \<lbrakk>M; receive\<langle>ts\<rangle>\<^sub>s\<^sub>t # S\<rbrakk>\<^sub>c \<I>\<rbrakk> \<Longrightarrow> \<lbrakk>M; receive\<langle>ts\<rangle>\<^sub>s\<^sub>t # S\<rbrakk>\<^sub>d \<I>
 4. \<And>M uu_ t t' S. \<lbrakk>\<And>x. \<lbrakk>M; S\<rbrakk>\<^sub>c \<I> \<Longrightarrow> \<lbrakk>M; S\<rbrakk>\<^sub>d \<I>; \<lbrakk>M; \<langle>uu_: t \<doteq> t'\<rangle>\<^sub>s\<^sub>t # S\<rbrakk>\<^sub>c \<I>\<rbrakk> \<Longrightarrow> \<lbrakk>M; \<langle>uu_: t \<doteq> t'\<rangle>\<^sub>s\<^sub>t # S\<rbrakk>\<^sub>d \<I>
 5. \<And>M X F S. \<lbrakk>\<And>x. \<lbrakk>M; S\<rbrakk>\<^sub>c \<I> \<Longrightarrow> \<lbrakk>M; S\<rbrakk>\<^sub>d \<I>; \<lbrakk>M; \<forall>X\<langle>\<or>\<noteq>: F\<rangle>\<^sub>s\<^sub>t # S\<rbrakk>\<^sub>c \<I>\<rbrakk> \<Longrightarrow> \<lbrakk>M; \<forall>X\<langle>\<or>\<noteq>: F\<rangle>\<^sub>s\<^sub>t # S\<rbrakk>\<^sub>d \<I>
[PROOF STEP]
case (ConsSnd M ts S)
[PROOF STATE]
proof (state)
this:
\<lbrakk>M; S\<rbrakk>\<^sub>c \<I> \<Longrightarrow> \<lbrakk>M; S\<rbrakk>\<^sub>d \<I>
\<lbrakk>M; send\<langle>ts\<rangle>\<^sub>s\<^sub>t # S\<rbrakk>\<^sub>c \<I>

goal (5 subgoals):
 1. \<And>M. \<lbrakk>M; []\<rbrakk>\<^sub>c \<I> \<Longrightarrow> \<lbrakk>M; []\<rbrakk>\<^sub>d \<I>
 2. \<And>M ts S. \<lbrakk>\<And>x. \<lbrakk>M; S\<rbrakk>\<^sub>c \<I> \<Longrightarrow> \<lbrakk>M; S\<rbrakk>\<^sub>d \<I>; \<lbrakk>M; send\<langle>ts\<rangle>\<^sub>s\<^sub>t # S\<rbrakk>\<^sub>c \<I>\<rbrakk> \<Longrightarrow> \<lbrakk>M; send\<langle>ts\<rangle>\<^sub>s\<^sub>t # S\<rbrakk>\<^sub>d \<I>
 3. \<And>M ts S. \<lbrakk>\<And>x. \<lbrakk>(set ts \<cdot>\<^sub>s\<^sub>e\<^sub>t x) \<union> M; S\<rbrakk>\<^sub>c \<I> \<Longrightarrow> \<lbrakk>(set ts \<cdot>\<^sub>s\<^sub>e\<^sub>t x) \<union> M; S\<rbrakk>\<^sub>d \<I>; \<lbrakk>M; receive\<langle>ts\<rangle>\<^sub>s\<^sub>t # S\<rbrakk>\<^sub>c \<I>\<rbrakk> \<Longrightarrow> \<lbrakk>M; receive\<langle>ts\<rangle>\<^sub>s\<^sub>t # S\<rbrakk>\<^sub>d \<I>
 4. \<And>M uu_ t t' S. \<lbrakk>\<And>x. \<lbrakk>M; S\<rbrakk>\<^sub>c \<I> \<Longrightarrow> \<lbrakk>M; S\<rbrakk>\<^sub>d \<I>; \<lbrakk>M; \<langle>uu_: t \<doteq> t'\<rangle>\<^sub>s\<^sub>t # S\<rbrakk>\<^sub>c \<I>\<rbrakk> \<Longrightarrow> \<lbrakk>M; \<langle>uu_: t \<doteq> t'\<rangle>\<^sub>s\<^sub>t # S\<rbrakk>\<^sub>d \<I>
 5. \<And>M X F S. \<lbrakk>\<And>x. \<lbrakk>M; S\<rbrakk>\<^sub>c \<I> \<Longrightarrow> \<lbrakk>M; S\<rbrakk>\<^sub>d \<I>; \<lbrakk>M; \<forall>X\<langle>\<or>\<noteq>: F\<rangle>\<^sub>s\<^sub>t # S\<rbrakk>\<^sub>c \<I>\<rbrakk> \<Longrightarrow> \<lbrakk>M; \<forall>X\<langle>\<or>\<noteq>: F\<rangle>\<^sub>s\<^sub>t # S\<rbrakk>\<^sub>d \<I>
[PROOF STEP]
hence "\<forall>t \<in> set ts. M \<turnstile>\<^sub>c t \<cdot> \<I>" "\<lbrakk>M; S\<rbrakk>\<^sub>d \<I>"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>M; S\<rbrakk>\<^sub>c \<I> \<Longrightarrow> \<lbrakk>M; S\<rbrakk>\<^sub>d \<I>
\<lbrakk>M; send\<langle>ts\<rangle>\<^sub>s\<^sub>t # S\<rbrakk>\<^sub>c \<I>

goal (1 subgoal):
 1. \<forall>t\<in>set ts. M \<turnstile>\<^sub>c t \<cdot> \<I> &&& \<lbrakk>M; S\<rbrakk>\<^sub>d \<I>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>t\<in>set ts. M \<turnstile>\<^sub>c t \<cdot> \<I>
\<lbrakk>M; S\<rbrakk>\<^sub>d \<I>

goal (5 subgoals):
 1. \<And>M. \<lbrakk>M; []\<rbrakk>\<^sub>c \<I> \<Longrightarrow> \<lbrakk>M; []\<rbrakk>\<^sub>d \<I>
 2. \<And>M ts S. \<lbrakk>\<And>x. \<lbrakk>M; S\<rbrakk>\<^sub>c \<I> \<Longrightarrow> \<lbrakk>M; S\<rbrakk>\<^sub>d \<I>; \<lbrakk>M; send\<langle>ts\<rangle>\<^sub>s\<^sub>t # S\<rbrakk>\<^sub>c \<I>\<rbrakk> \<Longrightarrow> \<lbrakk>M; send\<langle>ts\<rangle>\<^sub>s\<^sub>t # S\<rbrakk>\<^sub>d \<I>
 3. \<And>M ts S. \<lbrakk>\<And>x. \<lbrakk>(set ts \<cdot>\<^sub>s\<^sub>e\<^sub>t x) \<union> M; S\<rbrakk>\<^sub>c \<I> \<Longrightarrow> \<lbrakk>(set ts \<cdot>\<^sub>s\<^sub>e\<^sub>t x) \<union> M; S\<rbrakk>\<^sub>d \<I>; \<lbrakk>M; receive\<langle>ts\<rangle>\<^sub>s\<^sub>t # S\<rbrakk>\<^sub>c \<I>\<rbrakk> \<Longrightarrow> \<lbrakk>M; receive\<langle>ts\<rangle>\<^sub>s\<^sub>t # S\<rbrakk>\<^sub>d \<I>
 4. \<And>M uu_ t t' S. \<lbrakk>\<And>x. \<lbrakk>M; S\<rbrakk>\<^sub>c \<I> \<Longrightarrow> \<lbrakk>M; S\<rbrakk>\<^sub>d \<I>; \<lbrakk>M; \<langle>uu_: t \<doteq> t'\<rangle>\<^sub>s\<^sub>t # S\<rbrakk>\<^sub>c \<I>\<rbrakk> \<Longrightarrow> \<lbrakk>M; \<langle>uu_: t \<doteq> t'\<rangle>\<^sub>s\<^sub>t # S\<rbrakk>\<^sub>d \<I>
 5. \<And>M X F S. \<lbrakk>\<And>x. \<lbrakk>M; S\<rbrakk>\<^sub>c \<I> \<Longrightarrow> \<lbrakk>M; S\<rbrakk>\<^sub>d \<I>; \<lbrakk>M; \<forall>X\<langle>\<or>\<noteq>: F\<rangle>\<^sub>s\<^sub>t # S\<rbrakk>\<^sub>c \<I>\<rbrakk> \<Longrightarrow> \<lbrakk>M; \<forall>X\<langle>\<or>\<noteq>: F\<rangle>\<^sub>s\<^sub>t # S\<rbrakk>\<^sub>d \<I>
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
\<forall>t\<in>set ts. M \<turnstile>\<^sub>c t \<cdot> \<I>
\<lbrakk>M; S\<rbrakk>\<^sub>d \<I>

goal (1 subgoal):
 1. \<lbrakk>M; send\<langle>ts\<rangle>\<^sub>s\<^sub>t # S\<rbrakk>\<^sub>d \<I>
[PROOF STEP]
using strand_sem_d.simps(2)[of M _ S]
[PROOF STATE]
proof (prove)
using this:
\<forall>t\<in>set ts. M \<turnstile>\<^sub>c t \<cdot> \<I>
\<lbrakk>M; S\<rbrakk>\<^sub>d \<I>
\<lbrakk>M; send\<langle>?ts\<rangle>\<^sub>s\<^sub>t # S\<rbrakk>\<^sub>d = (\<lambda>\<I>. (\<forall>t\<in>set ?ts. M \<turnstile> t \<cdot> \<I>) \<and> \<lbrakk>M; S\<rbrakk>\<^sub>d \<I>)

goal (1 subgoal):
 1. \<lbrakk>M; send\<langle>ts\<rangle>\<^sub>s\<^sub>t # S\<rbrakk>\<^sub>d \<I>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<lbrakk>M; send\<langle>ts\<rangle>\<^sub>s\<^sub>t # S\<rbrakk>\<^sub>d \<I>

goal (4 subgoals):
 1. \<And>M. \<lbrakk>M; []\<rbrakk>\<^sub>c \<I> \<Longrightarrow> \<lbrakk>M; []\<rbrakk>\<^sub>d \<I>
 2. \<And>M ts S. \<lbrakk>\<And>x. \<lbrakk>(set ts \<cdot>\<^sub>s\<^sub>e\<^sub>t x) \<union> M; S\<rbrakk>\<^sub>c \<I> \<Longrightarrow> \<lbrakk>(set ts \<cdot>\<^sub>s\<^sub>e\<^sub>t x) \<union> M; S\<rbrakk>\<^sub>d \<I>; \<lbrakk>M; receive\<langle>ts\<rangle>\<^sub>s\<^sub>t # S\<rbrakk>\<^sub>c \<I>\<rbrakk> \<Longrightarrow> \<lbrakk>M; receive\<langle>ts\<rangle>\<^sub>s\<^sub>t # S\<rbrakk>\<^sub>d \<I>
 3. \<And>M uu_ t t' S. \<lbrakk>\<And>x. \<lbrakk>M; S\<rbrakk>\<^sub>c \<I> \<Longrightarrow> \<lbrakk>M; S\<rbrakk>\<^sub>d \<I>; \<lbrakk>M; \<langle>uu_: t \<doteq> t'\<rangle>\<^sub>s\<^sub>t # S\<rbrakk>\<^sub>c \<I>\<rbrakk> \<Longrightarrow> \<lbrakk>M; \<langle>uu_: t \<doteq> t'\<rangle>\<^sub>s\<^sub>t # S\<rbrakk>\<^sub>d \<I>
 4. \<And>M X F S. \<lbrakk>\<And>x. \<lbrakk>M; S\<rbrakk>\<^sub>c \<I> \<Longrightarrow> \<lbrakk>M; S\<rbrakk>\<^sub>d \<I>; \<lbrakk>M; \<forall>X\<langle>\<or>\<noteq>: F\<rangle>\<^sub>s\<^sub>t # S\<rbrakk>\<^sub>c \<I>\<rbrakk> \<Longrightarrow> \<lbrakk>M; \<forall>X\<langle>\<or>\<noteq>: F\<rangle>\<^sub>s\<^sub>t # S\<rbrakk>\<^sub>d \<I>
[PROOF STEP]
qed (auto simp add: ineq_model_def)
[PROOF STATE]
proof (state)
this:
\<lbrakk>M; S\<rbrakk>\<^sub>c \<I> \<Longrightarrow> \<lbrakk>M; S\<rbrakk>\<^sub>d \<I>

goal (1 subgoal):
 1. \<I> \<Turnstile>\<^sub>c \<langle>S,\<theta>\<rangle> \<Longrightarrow> \<I> \<Turnstile> \<langle>S,\<theta>\<rangle>
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>?M4; S\<rbrakk>\<^sub>c \<I> \<Longrightarrow> \<lbrakk>?M4; S\<rbrakk>\<^sub>d \<I>

goal (1 subgoal):
 1. \<I> \<Turnstile>\<^sub>c \<langle>S,\<theta>\<rangle> \<Longrightarrow> \<I> \<Turnstile> \<langle>S,\<theta>\<rangle>
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?M4; S\<rbrakk>\<^sub>c \<I> \<Longrightarrow> \<lbrakk>?M4; S\<rbrakk>\<^sub>d \<I>

goal (1 subgoal):
 1. \<I> \<Turnstile> \<langle>S,\<theta>\<rangle>
[PROOF STEP]
using *
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?M4; S\<rbrakk>\<^sub>c \<I> \<Longrightarrow> \<lbrakk>?M4; S\<rbrakk>\<^sub>d \<I>
\<I> \<Turnstile>\<^sub>c \<langle>S,\<theta>\<rangle>

goal (1 subgoal):
 1. \<I> \<Turnstile> \<langle>S,\<theta>\<rangle>
[PROOF STEP]
by (simp add: constr_sem_c_def constr_sem_d_def)
[PROOF STATE]
proof (state)
this:
\<I> \<Turnstile> \<langle>S,\<theta>\<rangle>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma abstract_primitive_in_doubt_deny_Allow2:
    "primitive_matcher_generic \<beta> \<Longrightarrow> normalized_nnf_match m \<Longrightarrow>
      \<not> matches (\<beta>, in_doubt_deny) (abstract_primitive disc m) action.Drop p \<Longrightarrow>
      \<not> matches (\<beta>, in_doubt_deny) m action.Drop p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>primitive_matcher_generic \<beta>; normalized_nnf_match m; \<not> matches (\<beta>, in_doubt_deny) (abstract_primitive disc m) Drop p\<rbrakk> \<Longrightarrow> \<not> matches (\<beta>, in_doubt_deny) m Drop p
[PROOF STEP]
apply(induction disc m rule: abstract_primitive.induct)
[PROOF STATE]
proof (prove)
goal (7 subgoals):
 1. \<And>uu_. \<lbrakk>primitive_matcher_generic \<beta>; normalized_nnf_match MatchAny; \<not> matches (\<beta>, in_doubt_deny) (abstract_primitive uu_ MatchAny) Drop p\<rbrakk> \<Longrightarrow> \<not> matches (\<beta>, in_doubt_deny) MatchAny Drop p
 2. \<And>disc a. \<lbrakk>primitive_matcher_generic \<beta>; normalized_nnf_match (Match a); \<not> matches (\<beta>, in_doubt_deny) (abstract_primitive disc (Match a)) Drop p\<rbrakk> \<Longrightarrow> \<not> matches (\<beta>, in_doubt_deny) (Match a) Drop p
 3. \<And>disc a. \<lbrakk>primitive_matcher_generic \<beta>; normalized_nnf_match (MatchNot (Match a)); \<not> matches (\<beta>, in_doubt_deny) (abstract_primitive disc (MatchNot (Match a))) Drop p\<rbrakk> \<Longrightarrow> \<not> matches (\<beta>, in_doubt_deny) (MatchNot (Match a)) Drop p
 4. \<And>disc v. \<lbrakk>\<lbrakk>primitive_matcher_generic \<beta>; normalized_nnf_match (MatchNot v); \<not> matches (\<beta>, in_doubt_deny) (abstract_primitive disc (MatchNot v)) Drop p\<rbrakk> \<Longrightarrow> \<not> matches (\<beta>, in_doubt_deny) (MatchNot v) Drop p; primitive_matcher_generic \<beta>; normalized_nnf_match (MatchNot (MatchNot v)); \<not> matches (\<beta>, in_doubt_deny) (abstract_primitive disc (MatchNot (MatchNot v))) Drop p\<rbrakk> \<Longrightarrow> \<not> matches (\<beta>, in_doubt_deny) (MatchNot (MatchNot v)) Drop p
 5. \<And>disc v va. \<lbrakk>\<lbrakk>primitive_matcher_generic \<beta>; normalized_nnf_match (MatchAnd v va); \<not> matches (\<beta>, in_doubt_deny) (abstract_primitive disc (MatchAnd v va)) Drop p\<rbrakk> \<Longrightarrow> \<not> matches (\<beta>, in_doubt_deny) (MatchAnd v va) Drop p; primitive_matcher_generic \<beta>; normalized_nnf_match (MatchNot (MatchAnd v va)); \<not> matches (\<beta>, in_doubt_deny) (abstract_primitive disc (MatchNot (MatchAnd v va))) Drop p\<rbrakk> \<Longrightarrow> \<not> matches (\<beta>, in_doubt_deny) (MatchNot (MatchAnd v va)) Drop p
 6. \<And>disc. \<lbrakk>\<lbrakk>primitive_matcher_generic \<beta>; normalized_nnf_match MatchAny; \<not> matches (\<beta>, in_doubt_deny) (abstract_primitive disc MatchAny) Drop p\<rbrakk> \<Longrightarrow> \<not> matches (\<beta>, in_doubt_deny) MatchAny Drop p; primitive_matcher_generic \<beta>; normalized_nnf_match (MatchNot MatchAny); \<not> matches (\<beta>, in_doubt_deny) (abstract_primitive disc (MatchNot MatchAny)) Drop p\<rbrakk> \<Longrightarrow> \<not> matches (\<beta>, in_doubt_deny) (MatchNot MatchAny) Drop p
 7. \<And>disc m1 m2. \<lbrakk>\<lbrakk>primitive_matcher_generic \<beta>; normalized_nnf_match m1; \<not> matches (\<beta>, in_doubt_deny) (abstract_primitive disc m1) Drop p\<rbrakk> \<Longrightarrow> \<not> matches (\<beta>, in_doubt_deny) m1 Drop p; \<lbrakk>primitive_matcher_generic \<beta>; normalized_nnf_match m2; \<not> matches (\<beta>, in_doubt_deny) (abstract_primitive disc m2) Drop p\<rbrakk> \<Longrightarrow> \<not> matches (\<beta>, in_doubt_deny) m2 Drop p; primitive_matcher_generic \<beta>; normalized_nnf_match (MatchAnd m1 m2); \<not> matches (\<beta>, in_doubt_deny) (abstract_primitive disc (MatchAnd m1 m2)) Drop p\<rbrakk> \<Longrightarrow> \<not> matches (\<beta>, in_doubt_deny) (MatchAnd m1 m2) Drop p
[PROOF STEP]
apply (simp_all add: bunch_of_lemmata_about_matches(1))
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>disc a. \<lbrakk>primitive_matcher_generic \<beta>; \<not> matches (\<beta>, in_doubt_deny) (if disc (Pos a) then Match (Extra (common_primitive_toString ipaddr_generic_toString a)) else Match a) Drop p\<rbrakk> \<Longrightarrow> \<not> matches (\<beta>, in_doubt_deny) (Match a) Drop p
 2. \<And>disc a. \<lbrakk>primitive_matcher_generic \<beta>; \<not> matches (\<beta>, in_doubt_deny) (if disc (Neg a) then Match (Extra (''! '' @ common_primitive_toString ipaddr_generic_toString a)) else MatchNot (Match a)) Drop p\<rbrakk> \<Longrightarrow> \<not> matches (\<beta>, in_doubt_deny) (MatchNot (Match a)) Drop p
 3. \<And>disc m1 m2. \<lbrakk>\<not> matches (\<beta>, in_doubt_deny) (abstract_primitive disc m1) Drop p \<Longrightarrow> \<not> matches (\<beta>, in_doubt_deny) m1 Drop p; \<not> matches (\<beta>, in_doubt_deny) (abstract_primitive disc m2) Drop p \<Longrightarrow> \<not> matches (\<beta>, in_doubt_deny) m2 Drop p; primitive_matcher_generic \<beta>; normalized_nnf_match m1 \<and> normalized_nnf_match m2; matches (\<beta>, in_doubt_deny) (abstract_primitive disc m1) Drop p \<longrightarrow> \<not> matches (\<beta>, in_doubt_deny) (abstract_primitive disc m2) Drop p\<rbrakk> \<Longrightarrow> matches (\<beta>, in_doubt_deny) m1 Drop p \<longrightarrow> \<not> matches (\<beta>, in_doubt_deny) m2 Drop p
[PROOF STEP]
apply(auto simp add: primitive_matcher_generic.Extra_single primitive_matcher_generic.Extra_single_not split: if_split_asm)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma between_imp_mod_between: "
  \<lbrakk> b < (m::nat); m * k + a \<le> n; n \<le> m * k + b \<rbrakk> \<Longrightarrow>
  a \<le> n mod m \<and> n mod m \<le> b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>b < m; m * k + a \<le> n; n \<le> m * k + b\<rbrakk> \<Longrightarrow> a \<le> n mod m \<and> n mod m \<le> b
[PROOF STEP]
apply (case_tac "m = 0", simp_all)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>b < m; m * k + a \<le> n; n \<le> m * k + b\<rbrakk> \<Longrightarrow> a \<le> n mod m \<and> n mod m \<le> b
[PROOF STEP]
apply (frule gr_implies_gr0)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>b < m; m * k + a \<le> n; n \<le> m * k + b; 0 < m\<rbrakk> \<Longrightarrow> a \<le> n mod m \<and> n mod m \<le> b
[PROOF STEP]
apply (subgoal_tac "k = n div m")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>b < m; m * k + a \<le> n; n \<le> m * k + b; 0 < m; k = n div m\<rbrakk> \<Longrightarrow> a \<le> n mod m \<and> n mod m \<le> b
 2. \<lbrakk>b < m; m * k + a \<le> n; n \<le> m * k + b; 0 < m\<rbrakk> \<Longrightarrow> k = n div m
[PROOF STEP]
prefer 2
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>b < m; m * k + a \<le> n; n \<le> m * k + b; 0 < m\<rbrakk> \<Longrightarrow> k = n div m
 2. \<lbrakk>b < m; m * k + a \<le> n; n \<le> m * k + b; 0 < m; k = n div m\<rbrakk> \<Longrightarrow> a \<le> n mod m \<and> n mod m \<le> b
[PROOF STEP]
apply (rule sym, rule div_nat_eqI)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>b < m; m * k + a \<le> n; n \<le> m * k + b; 0 < m\<rbrakk> \<Longrightarrow> m * k \<le> n
 2. \<lbrakk>b < m; m * k + a \<le> n; n \<le> m * k + b; 0 < m\<rbrakk> \<Longrightarrow> n < m * Suc k
 3. \<lbrakk>b < m; m * k + a \<le> n; n \<le> m * k + b; 0 < m; k = n div m\<rbrakk> \<Longrightarrow> a \<le> n mod m \<and> n mod m \<le> b
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>b < m; m * k + a \<le> n; n \<le> m * k + b; 0 < m\<rbrakk> \<Longrightarrow> n < m * Suc k
 2. \<lbrakk>b < m; m * k + a \<le> n; n \<le> m * k + b; 0 < m; k = n div m\<rbrakk> \<Longrightarrow> a \<le> n mod m \<and> n mod m \<le> b
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>b < m; m * k + a \<le> n; n \<le> m * k + b; 0 < m; k = n div m\<rbrakk> \<Longrightarrow> a \<le> n mod m \<and> n mod m \<le> b
[PROOF STEP]
apply clarify
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>b < m; m * (n div m) + a \<le> n; n \<le> m * (n div m) + b; 0 < m; k = n div m\<rbrakk> \<Longrightarrow> a \<le> n mod m \<and> n mod m \<le> b
[PROOF STEP]
apply (rule conjI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>b < m; m * (n div m) + a \<le> n; n \<le> m * (n div m) + b; 0 < m; k = n div m\<rbrakk> \<Longrightarrow> a \<le> n mod m
 2. \<lbrakk>b < m; m * (n div m) + a \<le> n; n \<le> m * (n div m) + b; 0 < m; k = n div m\<rbrakk> \<Longrightarrow> n mod m \<le> b
[PROOF STEP]
apply (rule add_le_imp_le_left[where c="m * (n div m)"], simp)+
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma mod_0_imp_div_mult_right_eq: "
  n mod m = (0::nat) \<Longrightarrow> n * k div m = k * (n div m)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n mod m = 0 \<Longrightarrow> n * k div m = k * (n div m)
[PROOF STEP]
by fastforce


[STATEMENT]
lemma fake_monotone [intro]: "G \<subseteq> H \<Longrightarrow> fake T U G \<subseteq> fake T U H"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. G \<subseteq> H \<Longrightarrow> fake T U G \<subseteq> fake T U H
[PROOF STEP]
by (safe, erule fake.cases, auto intro!: fake_intros)


[STATEMENT]
lemma before_conform2I: "before s1 s2 \<Longrightarrow> seq_conform s2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. before s1 s2 \<Longrightarrow> seq_conform s2
[PROOF STEP]
unfolding before_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. seq_conform s1 \<and> seq_conform s2 \<and> set s1 \<inter> set s2 = {} \<and> (\<exists>x\<in>set s1. \<exists>y\<in>set s2. x \<rightarrow>\<^bsub>T\<^esub> y) \<Longrightarrow> seq_conform s2
[PROOF STEP]
by blast


[STATEMENT]
lemma P_denormalize:
  fixes t1 :: "('a list,'b) dtree"
  assumes "wf_dlverts t1"
      and "\<forall>v \<in> dverts t1. distinct v"
      and "hd (Dtree.root t1) = root"
      and "max_deg t1 \<le> 1"
    shows "unique_set_r root (dverts t1) (denormalize t1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. unique_set_r root (dverts t1) (denormalize t1)
[PROOF STEP]
using assms P_denormalize_full
[PROOF STATE]
proof (prove)
using this:
wf_dlverts t1
\<forall>v\<in>dverts t1. distinct v
hd (dtree.root t1) = root
max_deg t1 \<le> 1
\<lbrakk>wf_dlverts ?t1.0; \<forall>v\<in>dverts ?t1.0. distinct v; hd (dtree.root ?t1.0) = root; max_deg ?t1.0 \<le> 1\<rbrakk> \<Longrightarrow> unique_set_r root (dverts ?t1.0) (denormalize (normalize_full ?t1.0))

goal (1 subgoal):
 1. unique_set_r root (dverts t1) (denormalize t1)
[PROOF STEP]
by auto


[STATEMENT]
lemma refl_onPD1: "refl_onP A r ==> r a b ==> a : A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>refl_onP A r; r a b\<rbrakk> \<Longrightarrow> a \<in> A
[PROOF STEP]
by(erule refl_onD1)(simp)


[STATEMENT]
lemma irreflPD: "\<lbrakk> irreflP r; r a a \<rbrakk> \<Longrightarrow> False"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>irreflP r; r a a\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
unfolding irrefl_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>a. (a, a) \<notin> {(x, y). r x y}; r a a\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
by blast


[STATEMENT]
lemma compute_shift_map_keys_pprod [code abstract]:
  "list_of_oalist_ntm (shift_map_keys_pprod t f xs) = map_raw (\<lambda>(k, v). (splus_pprod t k, f v)) (list_of_oalist_ntm xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. list_of_oalist_ntm (shift_map_keys_pprod t f xs) = map_raw (\<lambda>(k, v). (splus_pprod t k, f v)) (list_of_oalist_ntm xs)
[PROOF STEP]
by (simp add: pprod'.list_of_oalist_shift_keys case_prod_beta')


[STATEMENT]
lemma Disj_mono:
  assumes "insert A H \<turnstile> B" "insert C H \<turnstile> D" shows "insert (A OR C) H \<turnstile> B OR D"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. insert (A OR C) H \<turnstile> B OR D
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. insert (A OR C) H \<turnstile> B OR D
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. insert (A OR C) H \<turnstile> B OR D
[PROOF STEP]
fix A B C H
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. insert (A OR C) H \<turnstile> B OR D
[PROOF STEP]
have "insert (A OR C) H \<turnstile> (A IMP B) IMP C OR B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. insert (A OR C) H \<turnstile> (A IMP B) IMP C OR B
[PROOF STEP]
by (metis Bool Hyp MP_same boolean_axioms.DisjConj insertI1)
[PROOF STATE]
proof (state)
this:
insert (A OR C) H \<turnstile> (A IMP B) IMP C OR B

goal (1 subgoal):
 1. insert (A OR C) H \<turnstile> B OR D
[PROOF STEP]
hence "insert A H \<turnstile> B \<Longrightarrow> insert (A OR C) H \<turnstile> C OR B"
[PROOF STATE]
proof (prove)
using this:
insert (A OR C) H \<turnstile> (A IMP B) IMP C OR B

goal (1 subgoal):
 1. insert A H \<turnstile> B \<Longrightarrow> insert (A OR C) H \<turnstile> C OR B
[PROOF STEP]
by (metis MP_same Un_absorb Un_insert_right Imp_I thin_Un)
[PROOF STATE]
proof (state)
this:
insert A H \<turnstile> B \<Longrightarrow> insert (A OR C) H \<turnstile> C OR B

goal (1 subgoal):
 1. insert (A OR C) H \<turnstile> B OR D
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
insert ?Aa2 ?Ha2 \<turnstile> ?Ba2 \<Longrightarrow> insert (?Aa2 OR ?Ca2) ?Ha2 \<turnstile> ?Ca2 OR ?Ba2

goal (1 subgoal):
 1. insert (A OR C) H \<turnstile> B OR D
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
insert ?Aa2 ?Ha2 \<turnstile> ?Ba2 \<Longrightarrow> insert (?Aa2 OR ?Ca2) ?Ha2 \<turnstile> ?Ca2 OR ?Ba2

goal (1 subgoal):
 1. insert (A OR C) H \<turnstile> B OR D
[PROOF STEP]
by (metis cut_same assms thin2)
[PROOF STATE]
proof (state)
this:
insert (A OR C) H \<turnstile> B OR D

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma Neg_Imp_I [intro!]: "H \<turnstile> A \<Longrightarrow> insert B H \<turnstile> Fls \<Longrightarrow> H \<turnstile> Neg (A IMP B)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>H \<turnstile> A; insert B H \<turnstile> Fls\<rbrakk> \<Longrightarrow> H \<turnstile> Neg (A IMP B)
[PROOF STEP]
by (metis NegNeg_I Neg_Disj_I Neg_I)


[STATEMENT]
lemma slp_vp: "n -as\<rightarrow>\<^bsub>sl\<^esub>* n' \<Longrightarrow> n -as\<rightarrow>\<^sub>\<surd>* n'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n -as\<rightarrow>\<^bsub>sl\<^esub>* n' \<Longrightarrow> n -as\<rightarrow>\<^sub>\<surd>* n'
[PROOF STEP]
by(fastforce intro:same_level_path_valid_path simp:slp_def vp_def)


[STATEMENT]
lemma token_is_not_in_sink:
  "token_run x n \<notin> A \<Longrightarrow> token_run x (Suc n) \<in> A \<Longrightarrow> \<not>sink (token_run x n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>token_run x n \<notin> A; token_run x (Suc n) \<in> A\<rbrakk> \<Longrightarrow> \<not> sink (token_run x n)
[PROOF STEP]
by (metis Suc_eq_plus1 token_stays_in_sink)


[STATEMENT]
lemma adds_pp_splus:
  assumes "t adds\<^sub>p v"
  shows "t adds\<^sub>p s \<oplus> v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. t adds\<^sub>p s \<oplus> v
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
t adds\<^sub>p v

goal (1 subgoal):
 1. t adds\<^sub>p s \<oplus> v
[PROOF STEP]
by (simp add: adds_pp_def term_simps)


[STATEMENT]
lemma sfirst_Stream: "sfirst P (s ## x) = (if P (s ## x) then 0 else eSuc (sfirst P x))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sfirst P (s ## x) = (if P (s ## x) then 0 else eSuc (sfirst P x))
[PROOF STEP]
by (subst sfirst.simps) (simp add: HLD_iff)


[STATEMENT]
lemma cp_pre: "cp self' \<Longrightarrow> cp a1' \<Longrightarrow> cp a2'\<Longrightarrow> cp a3'
                  \<Longrightarrow> cp (\<lambda>X. PRE (self' X) (a1' X) (a2' X) (a3' X) )"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cp self'; cp a1'; cp a2'; cp a3'\<rbrakk> \<Longrightarrow> cp (\<lambda>X. PRE (self' X) (a1' X) (a2' X) (a3' X))
[PROOF STEP]
by(rule_tac f=PRE in cpI4, auto intro: cp\<^sub>P\<^sub>R\<^sub>E)


[STATEMENT]
lemma Rep_token_run_af:
  "Rep (token_run x n) \<equiv>\<^sub>P af\<^sub>G \<phi> (w [x \<rightarrow> n])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Rep (token_run x n) \<equiv>\<^sub>P af\<^sub>G \<phi> (w [x \<rightarrow> n])
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Rep (token_run x n) \<equiv>\<^sub>P af\<^sub>G \<phi> (w [x \<rightarrow> n])
[PROOF STEP]
have "token_run x n = Abs (af\<^sub>G \<phi> ((suffix x w) [0 \<rightarrow> (n - x)]))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. token_run x n = Abs (af\<^sub>G \<phi> (prefix (n - x) (suffix x w)))
[PROOF STEP]
by (simp add: subsequence_def run_foldl; metis af_G_abs.f_foldl_abs.abs_eq af_G_abs.f_foldl_abs_alt_def af_G_letter_abs_def)
[PROOF STATE]
proof (state)
this:
token_run x n = Abs (af\<^sub>G \<phi> (prefix (n - x) (suffix x w)))

goal (1 subgoal):
 1. Rep (token_run x n) \<equiv>\<^sub>P af\<^sub>G \<phi> (w [x \<rightarrow> n])
[PROOF STEP]
hence "Rep (token_run x n) \<equiv>\<^sub>P af\<^sub>G \<phi> ((suffix x w) [0 \<rightarrow> (n - x)])"
[PROOF STATE]
proof (prove)
using this:
token_run x n = Abs (af\<^sub>G \<phi> (prefix (n - x) (suffix x w)))

goal (1 subgoal):
 1. Rep (token_run x n) \<equiv>\<^sub>P af\<^sub>G \<phi> (prefix (n - x) (suffix x w))
[PROOF STEP]
using ltl\<^sub>P_abs_rep ltl_prop_equiv_quotient.abs_eq_iff
[PROOF STATE]
proof (prove)
using this:
token_run x n = Abs (af\<^sub>G \<phi> (prefix (n - x) (suffix x w)))
Abs (Rep ?\<phi>) = ?\<phi>
(Abs ?x = Abs ?y) = ?x \<equiv>\<^sub>P ?y

goal (1 subgoal):
 1. Rep (token_run x n) \<equiv>\<^sub>P af\<^sub>G \<phi> (prefix (n - x) (suffix x w))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Rep (token_run x n) \<equiv>\<^sub>P af\<^sub>G \<phi> (prefix (n - x) (suffix x w))

goal (1 subgoal):
 1. Rep (token_run x n) \<equiv>\<^sub>P af\<^sub>G \<phi> (w [x \<rightarrow> n])
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
Rep (token_run x n) \<equiv>\<^sub>P af\<^sub>G \<phi> (prefix (n - x) (suffix x w))

goal (1 subgoal):
 1. Rep (token_run x n) \<equiv>\<^sub>P af\<^sub>G \<phi> (w [x \<rightarrow> n])
[PROOF STEP]
unfolding ltl_prop_equiv_def subsequence_shift
[PROOF STATE]
proof (prove)
using this:
\<forall>\<A>. \<A> \<Turnstile>\<^sub>P Rep (token_run x n) = \<A> \<Turnstile>\<^sub>P af\<^sub>G \<phi> (w [x + 0 \<rightarrow> x + (n - x)])

goal (1 subgoal):
 1. \<forall>\<A>. \<A> \<Turnstile>\<^sub>P Rep (token_run x n) = \<A> \<Turnstile>\<^sub>P af\<^sub>G \<phi> (w [x \<rightarrow> n])
[PROOF STEP]
by (cases "x \<le> n"; simp add: subsequence_def)
[PROOF STATE]
proof (state)
this:
Rep (token_run x n) \<equiv>\<^sub>P af\<^sub>G \<phi> (w [x \<rightarrow> n])

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ltl_to_generalized_rabin_af_wellformed:
  "finite \<Sigma> \<Longrightarrow> range w \<subseteq> \<Sigma> \<Longrightarrow> ltl_to_rabin_af \<Sigma> w"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>finite \<Sigma>; range w \<subseteq> \<Sigma>\<rbrakk> \<Longrightarrow> ltl_to_rabin_af \<Sigma> w
[PROOF STEP]
apply (unfold_locales)
[PROOF STATE]
proof (prove)
goal (8 subgoals):
 1. \<lbrakk>finite \<Sigma>; range w \<subseteq> \<Sigma>\<rbrakk> \<Longrightarrow> finite \<Sigma>
 2. \<lbrakk>finite \<Sigma>; range w \<subseteq> \<Sigma>\<rbrakk> \<Longrightarrow> range w \<subseteq> \<Sigma>
 3. \<And>\<pi> \<pi>'. \<lbrakk>finite \<Sigma>; range w \<subseteq> \<Sigma>; dom \<pi> = dom \<pi>'; \<And>\<chi>. \<chi> \<in> dom \<pi> \<Longrightarrow> the (\<pi> \<chi>) \<le> the (\<pi>' \<chi>)\<rbrakk> \<Longrightarrow> M_fin \<pi> \<subseteq> M_fin \<pi>'
 4. \<And>\<phi>. \<lbrakk>finite \<Sigma>; range w \<subseteq> \<Sigma>\<rbrakk> \<Longrightarrow> finite (reach \<Sigma> \<up>af (Abs \<phi>))
 5. \<And>\<G> \<psi>. \<lbrakk>finite \<Sigma>; range w \<subseteq> \<Sigma>; Only_G \<G>\<rbrakk> \<Longrightarrow> finite \<Sigma>
 6. \<And>\<G> \<psi>. \<lbrakk>finite \<Sigma>; range w \<subseteq> \<Sigma>; Only_G \<G>\<rbrakk> \<Longrightarrow> finite (reach \<Sigma> \<up>af\<^sub>G (Abs \<psi>))
 7. \<And>\<G> \<psi>. \<lbrakk>finite \<Sigma>; range w \<subseteq> \<Sigma>; Only_G \<G>\<rbrakk> \<Longrightarrow> range w \<subseteq> \<Sigma>
 8. \<And>\<G> \<psi> q \<nu>. \<lbrakk>finite \<Sigma>; range w \<subseteq> \<Sigma>; Only_G \<G>; q \<in> {q. \<G> \<up>\<Turnstile>\<^sub>P q}\<rbrakk> \<Longrightarrow> \<up>af\<^sub>G q \<nu> \<in> {q. \<G> \<up>\<Turnstile>\<^sub>P q}
[PROOF STEP]
apply (auto simp add: af_G_letter_sat_core_lifted ltl_prop_entails_abs.rep_eq intro: finite_reach_af)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>\<pi> \<pi>' a b S. \<lbrakk>finite \<Sigma>; range w \<subseteq> \<Sigma>; dom \<pi> = dom \<pi>'; \<And>\<chi>. \<chi> \<in> dom \<pi>' \<Longrightarrow> the (\<pi> \<chi>) \<le> the (\<pi>' \<chi>); \<forall>\<chi>\<in>dom \<pi>'. S \<Turnstile>\<^sub>P \<chi> \<and> (\<forall>q. (\<exists>j\<ge>the (\<pi> \<chi>). the (b \<chi>) q = Some j) \<longrightarrow> S \<Turnstile>\<^sub>P Rep (\<up>eval\<^sub>G (dom \<pi>') q)); \<not> S \<Turnstile>\<^sub>P Rep a\<rbrakk> \<Longrightarrow> \<exists>S. (\<forall>\<chi>\<in>dom \<pi>'. S \<Turnstile>\<^sub>P \<chi> \<and> (\<forall>q. (\<exists>j\<ge>the (\<pi>' \<chi>). the (b \<chi>) q = Some j) \<longrightarrow> S \<Turnstile>\<^sub>P Rep (\<up>eval\<^sub>G (dom \<pi>') q))) \<and> \<not> S \<Turnstile>\<^sub>P Rep a
 2. \<And>\<G> \<psi>. \<lbrakk>finite \<Sigma>; range w \<subseteq> \<Sigma>; Only_G \<G>\<rbrakk> \<Longrightarrow> finite (reach \<Sigma> \<up>af\<^sub>G (Abs \<psi>))
[PROOF STEP]
apply (meson le_trans ltl_semi_mojmir[unfolded semi_mojmir_def])+
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma "ports_toString ''spt: '' (1024,1024) = ''spt: 1024''"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ports_toString ''spt: '' (1024, 1024) = ''spt: 1024''
[PROOF STEP]
by eval


[STATEMENT]
lemma prove_SubstFormP: "{} \<turnstile> SubstFormP \<guillemotleft>Var i\<guillemotright> \<guillemotleft>\<guillemotleft>A\<guillemotright>\<guillemotright> \<guillemotleft>A\<guillemotright> \<guillemotleft>A(i::=\<guillemotleft>A\<guillemotright>)\<guillemotright>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {} \<turnstile> SubstFormP \<guillemotleft>Var i\<guillemotright> \<guillemotleft>\<guillemotleft>A\<guillemotright>\<guillemotright> \<guillemotleft>A\<guillemotright> \<guillemotleft>A(i::=\<guillemotleft>A\<guillemotright>)\<guillemotright>
[PROOF STEP]
by (auto simp: supp_conv_fresh Sigma_fm_imp_thm ground_aux_def SubstForm_quot)


[STATEMENT]
lemma Number_Sign: "Number X \<noteq> Sign  X' Y'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Number X \<noteq> Sign X' Y'
[PROOF STEP]
by transfer auto


[STATEMENT]
lemma subseqs_mem_dbproj:
  assumes "Di \<in> set (subseqs D)" "list_all (\<lambda>d. fst d = i) Di"
  shows "Di \<in> set (subseqs (dbproj i D))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Di \<in> set (subseqs (dbproj i D))
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
Di \<in> set (subseqs D)
list_all (\<lambda>d. fst d = i) Di

goal (1 subgoal):
 1. Di \<in> set (subseqs (dbproj i D))
[PROOF STEP]
proof (induction D arbitrary: Di)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>Di. \<lbrakk>Di \<in> set (subseqs []); list_all (\<lambda>d. fst d = i) Di\<rbrakk> \<Longrightarrow> Di \<in> set (subseqs (dbproj i []))
 2. \<And>a D Di. \<lbrakk>\<And>Di. \<lbrakk>Di \<in> set (subseqs D); list_all (\<lambda>d. fst d = i) Di\<rbrakk> \<Longrightarrow> Di \<in> set (subseqs (dbproj i D)); Di \<in> set (subseqs (a # D)); list_all (\<lambda>d. fst d = i) Di\<rbrakk> \<Longrightarrow> Di \<in> set (subseqs (dbproj i (a # D)))
[PROOF STEP]
case (Cons di D)
[PROOF STATE]
proof (state)
this:
\<lbrakk>?Di \<in> set (subseqs D); list_all (\<lambda>d. fst d = i) ?Di\<rbrakk> \<Longrightarrow> ?Di \<in> set (subseqs (dbproj i D))
Di \<in> set (subseqs (di # D))
list_all (\<lambda>d. fst d = i) Di

goal (2 subgoals):
 1. \<And>Di. \<lbrakk>Di \<in> set (subseqs []); list_all (\<lambda>d. fst d = i) Di\<rbrakk> \<Longrightarrow> Di \<in> set (subseqs (dbproj i []))
 2. \<And>a D Di. \<lbrakk>\<And>Di. \<lbrakk>Di \<in> set (subseqs D); list_all (\<lambda>d. fst d = i) Di\<rbrakk> \<Longrightarrow> Di \<in> set (subseqs (dbproj i D)); Di \<in> set (subseqs (a # D)); list_all (\<lambda>d. fst d = i) Di\<rbrakk> \<Longrightarrow> Di \<in> set (subseqs (dbproj i (a # D)))
[PROOF STEP]
obtain d j where di: "di = (j,d)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>j d. di = (j, d) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis surj_pair)
[PROOF STATE]
proof (state)
this:
di = (j, d)

goal (2 subgoals):
 1. \<And>Di. \<lbrakk>Di \<in> set (subseqs []); list_all (\<lambda>d. fst d = i) Di\<rbrakk> \<Longrightarrow> Di \<in> set (subseqs (dbproj i []))
 2. \<And>a D Di. \<lbrakk>\<And>Di. \<lbrakk>Di \<in> set (subseqs D); list_all (\<lambda>d. fst d = i) Di\<rbrakk> \<Longrightarrow> Di \<in> set (subseqs (dbproj i D)); Di \<in> set (subseqs (a # D)); list_all (\<lambda>d. fst d = i) Di\<rbrakk> \<Longrightarrow> Di \<in> set (subseqs (dbproj i (a # D)))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Di \<in> set (subseqs (dbproj i (di # D)))
[PROOF STEP]
proof (cases "Di \<in> set (subseqs D)")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. Di \<in> set (subseqs D) \<Longrightarrow> Di \<in> set (subseqs (dbproj i (di # D)))
 2. Di \<notin> set (subseqs D) \<Longrightarrow> Di \<in> set (subseqs (dbproj i (di # D)))
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
Di \<in> set (subseqs D)

goal (2 subgoals):
 1. Di \<in> set (subseqs D) \<Longrightarrow> Di \<in> set (subseqs (dbproj i (di # D)))
 2. Di \<notin> set (subseqs D) \<Longrightarrow> Di \<in> set (subseqs (dbproj i (di # D)))
[PROOF STEP]
hence "Di \<in> set (subseqs (dbproj i D))"
[PROOF STATE]
proof (prove)
using this:
Di \<in> set (subseqs D)

goal (1 subgoal):
 1. Di \<in> set (subseqs (dbproj i D))
[PROOF STEP]
using Cons.IH Cons.prems
[PROOF STATE]
proof (prove)
using this:
Di \<in> set (subseqs D)
\<lbrakk>?Di \<in> set (subseqs D); list_all (\<lambda>d. fst d = i) ?Di\<rbrakk> \<Longrightarrow> ?Di \<in> set (subseqs (dbproj i D))
Di \<in> set (subseqs (di # D))
list_all (\<lambda>d. fst d = i) Di

goal (1 subgoal):
 1. Di \<in> set (subseqs (dbproj i D))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Di \<in> set (subseqs (dbproj i D))

goal (2 subgoals):
 1. Di \<in> set (subseqs D) \<Longrightarrow> Di \<in> set (subseqs (dbproj i (di # D)))
 2. Di \<notin> set (subseqs D) \<Longrightarrow> Di \<in> set (subseqs (dbproj i (di # D)))
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
Di \<in> set (subseqs (dbproj i D))

goal (1 subgoal):
 1. Di \<in> set (subseqs (dbproj i (di # D)))
[PROOF STEP]
using subseqs_Cons
[PROOF STATE]
proof (prove)
using this:
Di \<in> set (subseqs (dbproj i D))
?ys \<in> set (subseqs ?xs) \<Longrightarrow> ?ys \<in> set (subseqs (?x # ?xs))

goal (1 subgoal):
 1. Di \<in> set (subseqs (dbproj i (di # D)))
[PROOF STEP]
unfolding dbproj_def
[PROOF STATE]
proof (prove)
using this:
Di \<in> set (subseqs (filter (\<lambda>d. fst d = i) D))
?ys \<in> set (subseqs ?xs) \<Longrightarrow> ?ys \<in> set (subseqs (?x # ?xs))

goal (1 subgoal):
 1. Di \<in> set (subseqs (filter (\<lambda>d. fst d = i) (di # D)))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Di \<in> set (subseqs (dbproj i (di # D)))

goal (1 subgoal):
 1. Di \<notin> set (subseqs D) \<Longrightarrow> Di \<in> set (subseqs (dbproj i (di # D)))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Di \<notin> set (subseqs D) \<Longrightarrow> Di \<in> set (subseqs (dbproj i (di # D)))
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
Di \<notin> set (subseqs D)

goal (1 subgoal):
 1. Di \<notin> set (subseqs D) \<Longrightarrow> Di \<in> set (subseqs (dbproj i (di # D)))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Di \<notin> set (subseqs D)
[PROOF STEP]
obtain Di' where Di': "Di = di#Di'"
[PROOF STATE]
proof (prove)
using this:
Di \<notin> set (subseqs D)

goal (1 subgoal):
 1. (\<And>Di'. Di = di # Di' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using Cons.prems(1)
[PROOF STATE]
proof (prove)
using this:
Di \<notin> set (subseqs D)
Di \<in> set (subseqs (di # D))

goal (1 subgoal):
 1. (\<And>Di'. Di = di # Di' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis (mono_tags, lifting) Un_iff imageE set_append set_map subseqs.simps(2))
[PROOF STATE]
proof (state)
this:
Di = di # Di'

goal (1 subgoal):
 1. Di \<notin> set (subseqs D) \<Longrightarrow> Di \<in> set (subseqs (dbproj i (di # D)))
[PROOF STEP]
hence "Di' \<in> set (subseqs D)"
[PROOF STATE]
proof (prove)
using this:
Di = di # Di'

goal (1 subgoal):
 1. Di' \<in> set (subseqs D)
[PROOF STEP]
using Cons.prems(1) False
[PROOF STATE]
proof (prove)
using this:
Di = di # Di'
Di \<in> set (subseqs (di # D))
Di \<notin> set (subseqs D)

goal (1 subgoal):
 1. Di' \<in> set (subseqs D)
[PROOF STEP]
by (metis (no_types, lifting) UnE imageE list.inject set_append set_map subseqs.simps(2))
[PROOF STATE]
proof (state)
this:
Di' \<in> set (subseqs D)

goal (1 subgoal):
 1. Di \<notin> set (subseqs D) \<Longrightarrow> Di \<in> set (subseqs (dbproj i (di # D)))
[PROOF STEP]
hence "Di' \<in> set (subseqs (dbproj i D))"
[PROOF STATE]
proof (prove)
using this:
Di' \<in> set (subseqs D)

goal (1 subgoal):
 1. Di' \<in> set (subseqs (dbproj i D))
[PROOF STEP]
using Cons.IH Cons.prems Di'
[PROOF STATE]
proof (prove)
using this:
Di' \<in> set (subseqs D)
\<lbrakk>?Di \<in> set (subseqs D); list_all (\<lambda>d. fst d = i) ?Di\<rbrakk> \<Longrightarrow> ?Di \<in> set (subseqs (dbproj i D))
Di \<in> set (subseqs (di # D))
list_all (\<lambda>d. fst d = i) Di
Di = di # Di'

goal (1 subgoal):
 1. Di' \<in> set (subseqs (dbproj i D))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Di' \<in> set (subseqs (dbproj i D))

goal (1 subgoal):
 1. Di \<notin> set (subseqs D) \<Longrightarrow> Di \<in> set (subseqs (dbproj i (di # D)))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
Di' \<in> set (subseqs (dbproj i D))

goal (1 subgoal):
 1. Di \<notin> set (subseqs D) \<Longrightarrow> Di \<in> set (subseqs (dbproj i (di # D)))
[PROOF STEP]
have "i = j"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i = j
[PROOF STEP]
using Di' di Cons.prems(2)
[PROOF STATE]
proof (prove)
using this:
Di = di # Di'
di = (j, d)
list_all (\<lambda>d. fst d = i) Di

goal (1 subgoal):
 1. i = j
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
i = j

goal (1 subgoal):
 1. Di \<notin> set (subseqs D) \<Longrightarrow> Di \<in> set (subseqs (dbproj i (di # D)))
[PROOF STEP]
hence "dbproj i (di#D) = di#dbproj i D"
[PROOF STATE]
proof (prove)
using this:
i = j

goal (1 subgoal):
 1. dbproj i (di # D) = di # dbproj i D
[PROOF STEP]
unfolding dbproj_def
[PROOF STATE]
proof (prove)
using this:
i = j

goal (1 subgoal):
 1. filter (\<lambda>d. fst d = i) (di # D) = di # filter (\<lambda>d. fst d = i) D
[PROOF STEP]
by (simp add: di)
[PROOF STATE]
proof (state)
this:
dbproj i (di # D) = di # dbproj i D

goal (1 subgoal):
 1. Di \<notin> set (subseqs D) \<Longrightarrow> Di \<in> set (subseqs (dbproj i (di # D)))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
Di' \<in> set (subseqs (dbproj i D))
dbproj i (di # D) = di # dbproj i D
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
Di' \<in> set (subseqs (dbproj i D))
dbproj i (di # D) = di # dbproj i D

goal (1 subgoal):
 1. Di \<in> set (subseqs (dbproj i (di # D)))
[PROOF STEP]
using Di'
[PROOF STATE]
proof (prove)
using this:
Di' \<in> set (subseqs (dbproj i D))
dbproj i (di # D) = di # dbproj i D
Di = di # Di'

goal (1 subgoal):
 1. Di \<in> set (subseqs (dbproj i (di # D)))
[PROOF STEP]
by (metis (no_types, lifting) UnCI image_eqI set_append set_map subseqs.simps(2))
[PROOF STATE]
proof (state)
this:
Di \<in> set (subseqs (dbproj i (di # D)))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
Di \<in> set (subseqs (dbproj i (di # D)))

goal (1 subgoal):
 1. \<And>Di. \<lbrakk>Di \<in> set (subseqs []); list_all (\<lambda>d. fst d = i) Di\<rbrakk> \<Longrightarrow> Di \<in> set (subseqs (dbproj i []))
[PROOF STEP]
qed simp


[STATEMENT]
lemma alg_dvd_imp_algebraic_int:
  fixes x y :: "'a :: field_char_0"
  shows "x alg_dvd y \<Longrightarrow> algebraic_int x \<Longrightarrow> algebraic_int y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x alg_dvd y; algebraic_int x\<rbrakk> \<Longrightarrow> algebraic_int y
[PROOF STEP]
using algebraic_int_times[of "y / x" x]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>algebraic_int (y / x); algebraic_int x\<rbrakk> \<Longrightarrow> algebraic_int (y / x * x)

goal (1 subgoal):
 1. \<lbrakk>x alg_dvd y; algebraic_int x\<rbrakk> \<Longrightarrow> algebraic_int y
[PROOF STEP]
by (auto simp: alg_dvd_def)


[STATEMENT]
lemma cIsInvar_distinct_roles: "cIsInvar distinct_roles"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cIsInvar distinct_roles
[PROOF STEP]
apply (cases distinct_roles rule: cIsInvar)
[PROOF STATE]
proof (prove)
goal (8 subgoals):
 1. \<And>s uID p name info email. \<lbrakk>reach s; distinct_roles s; e_createUser s uID p name info email\<rbrakk> \<Longrightarrow> distinct_roles (createUser s uID p name info email)
 2. \<And>s confID uID p name info. \<lbrakk>reach s; distinct_roles s; e_createConf s confID uID p name info\<rbrakk> \<Longrightarrow> distinct_roles (createConf s confID uID p name info)
 3. \<And>s confID uID p uID'. \<lbrakk>reach s; distinct_roles s; e_createPC s confID uID p uID'\<rbrakk> \<Longrightarrow> distinct_roles (createPC s confID uID p uID')
 4. \<And>s confID uID p uID'. \<lbrakk>reach s; distinct_roles s; e_createChair s confID uID p uID'\<rbrakk> \<Longrightarrow> distinct_roles (createChair s confID uID p uID')
 5. \<And>s confID uID p papID name info. \<lbrakk>reach s; distinct_roles s; e_createPaper s confID uID p papID name info\<rbrakk> \<Longrightarrow> distinct_roles (createPaper s confID uID p papID name info)
 6. \<And>s confID uID p papID uID'. \<lbrakk>reach s; distinct_roles s; e_createAuthor s confID uID p papID uID'\<rbrakk> \<Longrightarrow> distinct_roles (createAuthor s confID uID p papID uID')
 7. \<And>s confID uID p papID uID'. \<lbrakk>reach s; distinct_roles s; e_createConflict s confID uID p papID uID'\<rbrakk> \<Longrightarrow> distinct_roles (createConflict s confID uID p papID uID')
 8. \<And>s confID uID p papID uID'. \<lbrakk>reach s; distinct_roles s; e_createReview s confID uID p papID uID'\<rbrakk> \<Longrightarrow> distinct_roles (createReview s confID uID p papID uID')
[PROOF STEP]
by (auto simp: c_defs distinct_roles_def)


[STATEMENT]
lemma invar_isRevNth_geq_revPH: "invar isRevNth_geq_revPH"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. invar isRevNth_geq_revPH
[PROOF STEP]
unfolding invar_cIsInvar_uIsInvar_uuIsInvar
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cIsInvar isRevNth_geq_revPH \<and> uIsInvar isRevNth_geq_revPH \<and> uuIsInvar isRevNth_geq_revPH
[PROOF STEP]
using cIsInvar_isRevNth_geq_revPH uIsInvar_isRevNth_geq_revPH
uuIsInvar_isRevNth_geq_revPH
[PROOF STATE]
proof (prove)
using this:
cIsInvar isRevNth_geq_revPH
uIsInvar isRevNth_geq_revPH
uuIsInvar isRevNth_geq_revPH

goal (1 subgoal):
 1. cIsInvar isRevNth_geq_revPH \<and> uIsInvar isRevNth_geq_revPH \<and> uuIsInvar isRevNth_geq_revPH
[PROOF STEP]
by auto


[STATEMENT]
theorem F'map_comp: "F'map (f1 o g1) (f2 o g2) (f3 o g3) = F'map f1 f2 f3 o F'map g1 g2 g3"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. F'map (f1 \<circ> g1) (f2 \<circ> g2) (f3 \<circ> g3) = F'map f1 f2 f3 \<circ> F'map g1 g2 g3
[PROOF STEP]
by (rule F.map_comp0)


[STATEMENT]
theorem siso0_Atm[simp]:
"siso0 (Atm atm) = compatAtm atm"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. siso0 (Atm atm) = compatAtm atm
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. siso0 (Atm atm) = compatAtm atm
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. siso0 (Atm atm) = compatAtm atm
[PROOF STEP]
fix c
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. siso0 (Atm atm) = compatAtm atm
[PROOF STEP]
have
   "(\<exists> atm. c = Atm atm \<and> compatAtm atm)
    \<Longrightarrow> siso0 c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>atm. c = Atm atm \<and> compatAtm atm \<Longrightarrow> siso0 c
[PROOF STEP]
apply(erule siso0_coind)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>c s c' s'. \<lbrakk>\<exists>atm. c = Atm atm \<and> compatAtm atm; mustT c s; (c, s) \<rightarrow>c (c', s')\<rbrakk> \<Longrightarrow> (\<exists>atm. c' = Atm atm \<and> compatAtm atm) \<or> siso0 c'
 2. \<And>c s t c' s'. \<lbrakk>\<exists>atm. c = Atm atm \<and> compatAtm atm; mustT c s; mustT c t; s \<approx> t; (c, s) \<rightarrow>c (c', s')\<rbrakk> \<Longrightarrow> \<exists>t'. s' \<approx> t' \<and> (c, t) \<rightarrow>c (c', t')
 3. \<And>c s t s'. \<lbrakk>mustT c s; mustT c t; \<exists>atm. c = Atm atm \<and> compatAtm atm; s \<approx> t; (c, s) \<rightarrow>t s'\<rbrakk> \<Longrightarrow> \<exists>t'. s' \<approx> t' \<and> (c, t) \<rightarrow>t t'
[PROOF STEP]
apply (metis Atm_transC_invert)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>c s t c' s'. \<lbrakk>\<exists>atm. c = Atm atm \<and> compatAtm atm; mustT c s; mustT c t; s \<approx> t; (c, s) \<rightarrow>c (c', s')\<rbrakk> \<Longrightarrow> \<exists>t'. s' \<approx> t' \<and> (c, t) \<rightarrow>c (c', t')
 2. \<And>c s t s'. \<lbrakk>mustT c s; mustT c t; \<exists>atm. c = Atm atm \<and> compatAtm atm; s \<approx> t; (c, s) \<rightarrow>t s'\<rbrakk> \<Longrightarrow> \<exists>t'. s' \<approx> t' \<and> (c, t) \<rightarrow>t t'
[PROOF STEP]
apply (metis PL.Atm_transC_invert)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>c s t s'. \<lbrakk>mustT c s; mustT c t; \<exists>atm. c = Atm atm \<and> compatAtm atm; s \<approx> t; (c, s) \<rightarrow>t s'\<rbrakk> \<Longrightarrow> \<exists>t'. s' \<approx> t' \<and> (c, t) \<rightarrow>t t'
[PROOF STEP]
by (metis Atm_transT_invert PL.Atm compatAtm_def)
[PROOF STATE]
proof (state)
this:
\<exists>atm. c = Atm atm \<and> compatAtm atm \<Longrightarrow> siso0 c

goal (1 subgoal):
 1. siso0 (Atm atm) = compatAtm atm
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<exists>atm. ?c3 = Atm atm \<and> compatAtm atm \<Longrightarrow> siso0 ?c3

goal (1 subgoal):
 1. siso0 (Atm atm) = compatAtm atm
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<exists>atm. ?c3 = Atm atm \<and> compatAtm atm \<Longrightarrow> siso0 ?c3

goal (1 subgoal):
 1. siso0 (Atm atm) = compatAtm atm
[PROOF STEP]
have "siso0 (Atm atm) \<Longrightarrow> compatAtm atm"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. siso0 (Atm atm) \<Longrightarrow> compatAtm atm
[PROOF STEP]
unfolding compatAtm_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. siso0 (Atm atm) \<Longrightarrow> \<forall>s t. s \<approx> t \<longrightarrow> aval atm s \<approx> aval atm t
[PROOF STEP]
by (metis Atm Atm_transT_invert siso0_transT mustT_Atm)
[PROOF STATE]
proof (state)
this:
siso0 (Atm atm) \<Longrightarrow> compatAtm atm

goal (1 subgoal):
 1. siso0 (Atm atm) = compatAtm atm
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<exists>atm. ?c3 = Atm atm \<and> compatAtm atm \<Longrightarrow> siso0 ?c3
siso0 (Atm atm) \<Longrightarrow> compatAtm atm
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<exists>atm. ?c3 = Atm atm \<and> compatAtm atm \<Longrightarrow> siso0 ?c3
siso0 (Atm atm) \<Longrightarrow> compatAtm atm

goal (1 subgoal):
 1. siso0 (Atm atm) = compatAtm atm
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
siso0 (Atm atm) = compatAtm atm

goal:
No subgoals!
[PROOF STEP]
qed