kings-crown/FVELER_Isabelle huggingface dataset:
theory Wellformed_CAMKES

lemma wellformed_composition_ann:
  "wellformed_composition c = (
     \<comment> \<open>This system contains @{text \<open>\<ge> 1\<close>} active component.\<close>
    check_wellformed (wellformed_composition, ''control'', map fst (components c))
                     (\<exists>x \<in> set (components c). control (snd x)) \<and>
     \<comment> \<open>All references resolve.\<close>
    refs_valid_composition c \<and>
     \<comment> \<open>The @{const group_labels} mapping refers to existing ADL names.\<close>
    (\<forall>(comp, group) \<in> set (group_labels c).
        check_wellformed (wellformed_composition, ''group_labels'', comp)
          (comp \<in> (fst ` set (components c) \<union> fst ` set (connections c)))) \<and>
     \<comment> \<open>All connectors and components have distinct names.
        These names will correspond to integrity policy labels.\<close>
    check_wellformed (wellformed_composition, ''distinct'', map fst (components c) @ map fst (connections c))
                     (distinct (map fst (components c) @ map fst (connections c))) \<and>
     \<comment> \<open>All components are valid.\<close>
    (\<forall>x \<in> set (components c). check_wellformed (wellformed_composition, ''component'', fst x)
                                               (wellformed_component (snd x))) \<and>
     \<comment> \<open>All connections are valid.\<close>
    (\<forall>x \<in> set (connections c). check_wellformed (wellformed_composition, ''connection'', fst x)
                                                (wellformed_connection (snd x)))
   )" by (simp only: wellformed_composition_def remove_generic_tag simp_thms)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. wellformed_composition c = (check_wellformed (wellformed_composition, ''control'', map fst (components c)) (\<exists>x\<in>set (components c). control (snd x)) \<and> refs_valid_composition c \<and> (\<forall>(comp, group)\<in>set (group_labels c). check_wellformed (wellformed_composition, ''group_labels'', comp) (comp \<in> fst ` set (components c) \<union> fst ` set (connections c))) \<and> check_wellformed (wellformed_composition, ''distinct'', map fst (components c) @ map fst (connections c)) (distinct (map fst (components c) @ map fst (connections c))) \<and> (\<forall>x\<in>set (components c). check_wellformed (wellformed_composition, ''component'', fst x) (wellformed_component (snd x))) \<and> (\<forall>x\<in>set (connections c). check_wellformed (wellformed_composition, ''connection'', fst x) (wellformed_connection (snd x))))
theory Examples_CAMKES

lemma "wellformed_assembly system" by (simp add: wellformed_CAMKES_simps system_def echo_def client_def simple_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. wellformed_assembly system
theory Examples_CAMKES

lemma "wellformed_assembly event_system" by (simp add: wellformed_CAMKES_simps event_system_def emitter_def consumer_def signal_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. wellformed_assembly event_system
theory Examples_CAMKES

lemma "wellformed_assembly terminal" by (simp add: wellformed_CAMKES_simps refs_valid_connection_def
                terminal_def comp_def manager_def terminal_client_def display_def
                channel1_def channel2_def conf_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. wellformed_assembly terminal
theory Examples_CAMKES

lemma "\<not>wellformed_assembly \<lparr> composition = \<lparr>
    components = [(''foo'', undefined), (''foo'', undefined)],
    connections = undefined,
    group_labels = undefined
  \<rparr>, configuration = undefined,
     policy_extra = {} \<rparr>" by (simp add:wellformed_assembly_def wellformed_composition_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<not> wellformed_assembly \<lparr>composition = \<lparr>components = [(''foo'', undefined), (''foo'', undefined)], connections = undefined, group_labels = undefined\<rparr>, configuration = undefined, policy_extra = {}\<rparr>
theory Examples_CAMKES

lemma "\<not>wellformed_assembly \<lparr> composition = \<lparr>
    components = undefined,
    connections = [(''foo'', undefined), (''foo'', undefined)],
    group_labels = undefined
  \<rparr>, configuration = undefined,
     policy_extra = {} \<rparr>" by (simp add:wellformed_assembly_def wellformed_composition_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<not> wellformed_assembly \<lparr>composition = \<lparr>components = undefined, connections = [(''foo'', undefined), (''foo'', undefined)], group_labels = undefined\<rparr>, configuration = undefined, policy_extra = {}\<rparr>
theory Examples_CAMKES

lemma "\<not>wellformed_assembly \<lparr> composition = \<lparr>
    components = [(''foo'', undefined)],
    connections = [(''foo'', undefined)],
    group_labels = undefined
  \<rparr>, configuration = undefined,
     policy_extra = {} \<rparr>" by (simp add:wellformed_assembly_def wellformed_composition_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<not> wellformed_assembly \<lparr>composition = \<lparr>components = [(''foo'', undefined)], connections = [(''foo'', undefined)], group_labels = undefined\<rparr>, configuration = undefined, policy_extra = {}\<rparr>
theory Examples_CAMKES

lemma "\<not>wellformed_assembly \<lparr> composition = \<lparr>
    components = [(''foo'', \<lparr>
      control = undefined,
      hardware = undefined,
      requires = [(''bar'', (InterfaceRequired, [undefined]))],
      provides = undefined,
      dataports = undefined,
      emits = undefined,
      consumes = undefined,
      attributes = undefined \<rparr>)],
    connections = [
      (''dup1'', \<lparr>
        conn_type = undefined,
        conn_from = [(''foo'', ''bar'')],
        conn_to = undefined \<rparr>),
      (''dup2'', \<lparr>
        conn_type = undefined,
        conn_from = [(''foo'', ''bar'')],
        conn_to = undefined \<rparr>)],
    group_labels = undefined
  \<rparr>, configuration = undefined,
     policy_extra = {} \<rparr>" by (simp add: wellformed_assembly_def wellformed_composition_def refs_valid_components_def
                refs_valid_composition_def refs_valid_procedures_def
                ex_one_def
           split: prod.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<not> wellformed_assembly \<lparr>composition = \<lparr>components = [(''foo'', \<lparr>control = undefined, hardware = undefined, requires = [(''bar'', InterfaceRequired, [undefined])], provides = undefined, dataports = undefined, emits = undefined, consumes = undefined, attributes = undefined\<rparr>)], connections = [(''dup1'', \<lparr>conn_type = undefined, conn_from = [(''foo'', ''bar'')], conn_to = undefined\<rparr>), (''dup2'', \<lparr>conn_type = undefined, conn_from = [(''foo'', ''bar'')], conn_to = undefined\<rparr>)], group_labels = undefined\<rparr>, configuration = undefined, policy_extra = {}\<rparr>
theory FastMap

lemma lookup_tree_valid_simps':
  "lookup_tree_valid key Leaf = (True, None)"
  "lookup_tree_valid key (Node k v Leaf Leaf) = (True, Some (k, k))"
  "\<lbrakk> lookup_tree_valid key (Node lk lv llt lrt) = (True, Some (llow, lhigh));
     key lhigh < key k
   \<rbrakk> \<Longrightarrow> lookup_tree_valid key (Node k v (Node lk lv llt lrt) Leaf) =
           (True, Some (llow, k))"
  "\<lbrakk> lookup_tree_valid key (Node rk rv rlt rrt) = (True, Some (rlow, rhigh));
     key k < key rlow
   \<rbrakk> \<Longrightarrow> lookup_tree_valid key (Node k v Leaf (Node rk rv rlt rrt)) =
           (True, Some (k, rhigh))"
  "\<lbrakk> lookup_tree_valid key (Node lk lv llt lrt) = (True, Some (llow, lhigh));
     lookup_tree_valid key (Node rk rv rlt rrt) = (True, Some (rlow, rhigh));
     key lhigh < key k;
     key k < key rlow
   \<rbrakk> \<Longrightarrow> lookup_tree_valid key (Node k v (Node lk lv llt lrt) (Node rk rv rlt rrt)) =
           (True, Some (llow, rhigh))" by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (lookup_tree_valid key Leaf = (True, None) &&& lookup_tree_valid key (Node k v Leaf Leaf) = (True, Some (k, k))) &&& (\<lbrakk>lookup_tree_valid key (Node lk lv llt lrt) = (True, Some (llow, lhigh)); key lhigh < key k\<rbrakk> \<Longrightarrow> lookup_tree_valid key (Node k v (Node lk lv llt lrt) Leaf) = (True, Some (llow, k))) &&& (\<lbrakk>lookup_tree_valid key (Node rk rv rlt rrt) = (True, Some (rlow, rhigh)); key k < key rlow\<rbrakk> \<Longrightarrow> lookup_tree_valid key (Node k v Leaf (Node rk rv rlt rrt)) = (True, Some (k, rhigh))) &&& (\<lbrakk>lookup_tree_valid key (Node lk lv llt lrt) = (True, Some (llow, lhigh)); lookup_tree_valid key (Node rk rv rlt rrt) = (True, Some (rlow, rhigh)); key lhigh < key k; key k < key rlow\<rbrakk> \<Longrightarrow> lookup_tree_valid key (Node k v (Node lk lv llt lrt) (Node rk rv rlt rrt)) = (True, Some (llow, rhigh)))
theory FastMap

lemma lookup_tree_valid_empty:
  "lookup_tree_valid key tree = (True, None) \<Longrightarrow> tree = Leaf" apply (induct tree) apply simp apply (fastforce split: prod.splits option.splits if_splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. lookup_tree_valid key tree = (True, None) \<Longrightarrow> tree = Leaf proof (prove)
goal (2 subgoals):
 1. lookup_tree_valid key Leaf = (True, None) \<Longrightarrow> Leaf = Leaf
 2. \<And>x1 x2 tree1 tree2. \<lbrakk>lookup_tree_valid key tree1 = (True, None) \<Longrightarrow> tree1 = Leaf; lookup_tree_valid key tree2 = (True, None) \<Longrightarrow> tree2 = Leaf; lookup_tree_valid key (Node x1 x2 tree1 tree2) = (True, None)\<rbrakk> \<Longrightarrow> Node x1 x2 tree1 tree2 = Leaf proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2 tree1 tree2. \<lbrakk>lookup_tree_valid key tree1 = (True, None) \<Longrightarrow> tree1 = Leaf; lookup_tree_valid key tree2 = (True, None) \<Longrightarrow> tree2 = Leaf; lookup_tree_valid key (Node x1 x2 tree1 tree2) = (True, None)\<rbrakk> \<Longrightarrow> Node x1 x2 tree1 tree2 = Leaf proof (prove)
goal:
No subgoals!
theory FastMap

lemma lookup_tree_valid_in_range:
  "lookup_tree_valid key tree = (True, Some (low, high)) \<Longrightarrow>
   lookup_tree key tree k = Some v \<Longrightarrow>
   key k \<in> {key low .. key high}" apply (induct tree arbitrary: k v low high) apply simp apply (fastforce split: prod.splits option.splits if_split_asm
                   dest: lookup_tree_valid_empty lookup_tree_valid_range) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>lookup_tree_valid key tree = (True, Some (low, high)); lookup_tree key tree k = Some v\<rbrakk> \<Longrightarrow> key k \<in> {key low..key high} proof (prove)
goal (2 subgoals):
 1. \<And>k v low high. \<lbrakk>lookup_tree_valid key Leaf = (True, Some (low, high)); lookup_tree key Leaf k = Some v\<rbrakk> \<Longrightarrow> key k \<in> {key low..key high}
 2. \<And>x1 x2 tree1 tree2 k v low high. \<lbrakk>\<And>k v low high. \<lbrakk>lookup_tree_valid key tree1 = (True, Some (low, high)); lookup_tree key tree1 k = Some v\<rbrakk> \<Longrightarrow> key k \<in> {key low..key high}; \<And>k v low high. \<lbrakk>lookup_tree_valid key tree2 = (True, Some (low, high)); lookup_tree key tree2 k = Some v\<rbrakk> \<Longrightarrow> key k \<in> {key low..key high}; lookup_tree_valid key (Node x1 x2 tree1 tree2) = (True, Some (low, high)); lookup_tree key (Node x1 x2 tree1 tree2) k = Some v\<rbrakk> \<Longrightarrow> key k \<in> {key low..key high} proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2 tree1 tree2 k v low high. \<lbrakk>\<And>k v low high. \<lbrakk>lookup_tree_valid key tree1 = (True, Some (low, high)); lookup_tree key tree1 k = Some v\<rbrakk> \<Longrightarrow> key k \<in> {key low..key high}; \<And>k v low high. \<lbrakk>lookup_tree_valid key tree2 = (True, Some (low, high)); lookup_tree key tree2 k = Some v\<rbrakk> \<Longrightarrow> key k \<in> {key low..key high}; lookup_tree_valid key (Node x1 x2 tree1 tree2) = (True, Some (low, high)); lookup_tree key (Node x1 x2 tree1 tree2) k = Some v\<rbrakk> \<Longrightarrow> key k \<in> {key low..key high} proof (prove)
goal:
No subgoals!
theory FastMap

lemma lookup_tree_valid_in_range_None:
  "lookup_tree_valid key tree = (True, Some (low, high)) \<Longrightarrow>
   key k \<notin> {key low .. key high} \<Longrightarrow>
   lookup_tree key tree k = None" using lookup_tree_valid_in_range by fastforce

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>lookup_tree_valid key tree = (True, Some (low, high)); key k \<notin> {key low..key high}\<rbrakk> \<Longrightarrow> lookup_tree key tree k = None proof (prove)
using this:
\<lbrakk>lookup_tree_valid ?key ?tree = (True, Some (?low, ?high)); lookup_tree ?key ?tree ?k = Some ?v\<rbrakk> \<Longrightarrow> ?key ?k \<in> {?key ?low..?key ?high}

goal (1 subgoal):
 1. \<lbrakk>lookup_tree_valid key tree = (True, Some (low, high)); key k \<notin> {key low..key high}\<rbrakk> \<Longrightarrow> lookup_tree key tree k = None
theory FastMap

lemma lookup_tree_to_list_range:
  "lookup_tree_valid key tree = (True, Some (low, high)) \<Longrightarrow>
   (k, v) \<in> set (lookup_tree_to_list tree) \<Longrightarrow>
   key k \<in> {key low .. key high}" apply (induct tree arbitrary: k v low high) apply simp apply (fastforce split: prod.splits option.splits if_split_asm
                   dest: lookup_tree_valid_empty lookup_tree_valid_range) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>lookup_tree_valid key tree = (True, Some (low, high)); (k, v) \<in> set (lookup_tree_to_list tree)\<rbrakk> \<Longrightarrow> key k \<in> {key low..key high} proof (prove)
goal (2 subgoals):
 1. \<And>k v low high. \<lbrakk>lookup_tree_valid key Leaf = (True, Some (low, high)); (k, v) \<in> set (lookup_tree_to_list Leaf)\<rbrakk> \<Longrightarrow> key k \<in> {key low..key high}
 2. \<And>x1 x2 tree1 tree2 k v low high. \<lbrakk>\<And>k v low high. \<lbrakk>lookup_tree_valid key tree1 = (True, Some (low, high)); (k, v) \<in> set (lookup_tree_to_list tree1)\<rbrakk> \<Longrightarrow> key k \<in> {key low..key high}; \<And>k v low high. \<lbrakk>lookup_tree_valid key tree2 = (True, Some (low, high)); (k, v) \<in> set (lookup_tree_to_list tree2)\<rbrakk> \<Longrightarrow> key k \<in> {key low..key high}; lookup_tree_valid key (Node x1 x2 tree1 tree2) = (True, Some (low, high)); (k, v) \<in> set (lookup_tree_to_list (Node x1 x2 tree1 tree2))\<rbrakk> \<Longrightarrow> key k \<in> {key low..key high} proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2 tree1 tree2 k v low high. \<lbrakk>\<And>k v low high. \<lbrakk>lookup_tree_valid key tree1 = (True, Some (low, high)); (k, v) \<in> set (lookup_tree_to_list tree1)\<rbrakk> \<Longrightarrow> key k \<in> {key low..key high}; \<And>k v low high. \<lbrakk>lookup_tree_valid key tree2 = (True, Some (low, high)); (k, v) \<in> set (lookup_tree_to_list tree2)\<rbrakk> \<Longrightarrow> key k \<in> {key low..key high}; lookup_tree_valid key (Node x1 x2 tree1 tree2) = (True, Some (low, high)); (k, v) \<in> set (lookup_tree_to_list (Node x1 x2 tree1 tree2))\<rbrakk> \<Longrightarrow> key k \<in> {key low..key high} proof (prove)
goal:
No subgoals!
theory FastMap

lemma lookup_tree_dom_distinct_sorted_:
  "fst (lookup_tree_valid key tree) \<Longrightarrow>
   distinct (lookup_tree_to_list tree) \<and> sorted (map (key o fst) (lookup_tree_to_list tree))" apply (induct tree) apply simp apply (fastforce simp: sorted_append
                   split: prod.splits option.splits if_splits
                   dest: lookup_tree_valid_empty lookup_tree_valid_range
                         lookup_tree_valid_in_range lookup_tree_to_list_range
                   elim: lookup_tree_valid_in_range_None) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. fst (lookup_tree_valid key tree) \<Longrightarrow> distinct (lookup_tree_to_list tree) \<and> sorted (map (key \<circ> fst) (lookup_tree_to_list tree)) proof (prove)
goal (2 subgoals):
 1. fst (lookup_tree_valid key Leaf) \<Longrightarrow> distinct (lookup_tree_to_list Leaf) \<and> sorted (map (key \<circ> fst) (lookup_tree_to_list Leaf))
 2. \<And>x1 x2 tree1 tree2. \<lbrakk>fst (lookup_tree_valid key tree1) \<Longrightarrow> distinct (lookup_tree_to_list tree1) \<and> sorted (map (key \<circ> fst) (lookup_tree_to_list tree1)); fst (lookup_tree_valid key tree2) \<Longrightarrow> distinct (lookup_tree_to_list tree2) \<and> sorted (map (key \<circ> fst) (lookup_tree_to_list tree2)); fst (lookup_tree_valid key (Node x1 x2 tree1 tree2))\<rbrakk> \<Longrightarrow> distinct (lookup_tree_to_list (Node x1 x2 tree1 tree2)) \<and> sorted (map (key \<circ> fst) (lookup_tree_to_list (Node x1 x2 tree1 tree2))) proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2 tree1 tree2. \<lbrakk>fst (lookup_tree_valid key tree1) \<Longrightarrow> distinct (lookup_tree_to_list tree1) \<and> sorted (map (key \<circ> fst) (lookup_tree_to_list tree1)); fst (lookup_tree_valid key tree2) \<Longrightarrow> distinct (lookup_tree_to_list tree2) \<and> sorted (map (key \<circ> fst) (lookup_tree_to_list tree2)); fst (lookup_tree_valid key (Node x1 x2 tree1 tree2))\<rbrakk> \<Longrightarrow> distinct (lookup_tree_to_list (Node x1 x2 tree1 tree2)) \<and> sorted (map (key \<circ> fst) (lookup_tree_to_list (Node x1 x2 tree1 tree2))) proof (prove)
goal:
No subgoals!
theory FastMap

lemma lookup_tree_to_list_of_:
  "fst (lookup_tree_valid key tree) \<Longrightarrow>
   map_of (map (apfst key) (lookup_tree_to_list tree)) (key k) = lookup_tree key tree k" apply (induct tree arbitrary: k) apply simp 
  (* this big blob just does case distinctions of both subtrees and
     all possible lookup results within each, then solves *)
  (* slow 10s *)
   by (fastforce simp: apfst_def map_prod_def map_add_def
                split: prod.splits option.splits if_splits
                dest: lookup_tree_valid_empty lookup_tree_valid_range lookup_tree_valid_in_range
                elim: lookup_tree_valid_in_range_None)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. fst (lookup_tree_valid key tree) \<Longrightarrow> map_of (map (apfst key) (lookup_tree_to_list tree)) (key k) = lookup_tree key tree k proof (prove)
goal (2 subgoals):
 1. \<And>k. fst (lookup_tree_valid key Leaf) \<Longrightarrow> map_of (map (apfst key) (lookup_tree_to_list Leaf)) (key k) = lookup_tree key Leaf k
 2. \<And>x1 x2 tree1 tree2 k. \<lbrakk>\<And>k. fst (lookup_tree_valid key tree1) \<Longrightarrow> map_of (map (apfst key) (lookup_tree_to_list tree1)) (key k) = lookup_tree key tree1 k; \<And>k. fst (lookup_tree_valid key tree2) \<Longrightarrow> map_of (map (apfst key) (lookup_tree_to_list tree2)) (key k) = lookup_tree key tree2 k; fst (lookup_tree_valid key (Node x1 x2 tree1 tree2))\<rbrakk> \<Longrightarrow> map_of (map (apfst key) (lookup_tree_to_list (Node x1 x2 tree1 tree2))) (key k) = lookup_tree key (Node x1 x2 tree1 tree2) k proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2 tree1 tree2 k. \<lbrakk>\<And>k. fst (lookup_tree_valid key tree1) \<Longrightarrow> map_of (map (apfst key) (lookup_tree_to_list tree1)) (key k) = lookup_tree key tree1 k; \<And>k. fst (lookup_tree_valid key tree2) \<Longrightarrow> map_of (map (apfst key) (lookup_tree_to_list tree2)) (key k) = lookup_tree key tree2 k; fst (lookup_tree_valid key (Node x1 x2 tree1 tree2))\<rbrakk> \<Longrightarrow> map_of (map (apfst key) (lookup_tree_to_list (Node x1 x2 tree1 tree2))) (key k) = lookup_tree key (Node x1 x2 tree1 tree2) k proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2 tree1 tree2 k. \<lbrakk>\<And>k. fst (lookup_tree_valid key tree1) \<Longrightarrow> map_of (map (apfst key) (lookup_tree_to_list tree1)) (key k) = lookup_tree key tree1 k; \<And>k. fst (lookup_tree_valid key tree2) \<Longrightarrow> map_of (map (apfst key) (lookup_tree_to_list tree2)) (key k) = lookup_tree key tree2 k; fst (lookup_tree_valid key (Node x1 x2 tree1 tree2))\<rbrakk> \<Longrightarrow> map_of (map (apfst key) (lookup_tree_to_list (Node x1 x2 tree1 tree2))) (key k) = lookup_tree key (Node x1 x2 tree1 tree2) k
theory FastMap

lemma lookup_tree_to_list_of:
  "fst (lookup_tree_valid key tree) \<Longrightarrow>
   lookup_tree key tree = map_of (map (apfst key) (lookup_tree_to_list tree)) o key" apply (rule ext) apply (simp add: lookup_tree_to_list_of_) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. fst (lookup_tree_valid key tree) \<Longrightarrow> lookup_tree key tree = map_of (map (apfst key) (lookup_tree_to_list tree)) \<circ> key proof (prove)
goal (1 subgoal):
 1. \<And>x. fst (lookup_tree_valid key tree) \<Longrightarrow> lookup_tree key tree x = (map_of (map (apfst key) (lookup_tree_to_list tree)) \<circ> key) x proof (prove)
goal:
No subgoals!
theory FastMap

lemma map_of_key:
  "inj key \<Longrightarrow> map_of (map (apfst key) binds) o key = map_of binds" apply (rule ext) apply (induct binds) apply simp apply (clarsimp simp: inj_def dom_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. inj key \<Longrightarrow> map_of (map (apfst key) binds) \<circ> key = map_of binds proof (prove)
goal (1 subgoal):
 1. \<And>x. inj key \<Longrightarrow> (map_of (map (apfst key) binds) \<circ> key) x = map_of binds x proof (prove)
goal (2 subgoals):
 1. \<And>x. inj key \<Longrightarrow> (map_of (map (apfst key) []) \<circ> key) x = map_of [] x
 2. \<And>a binds x. \<lbrakk>\<And>x. inj key \<Longrightarrow> (map_of (map (apfst key) binds) \<circ> key) x = map_of binds x; inj key\<rbrakk> \<Longrightarrow> (map_of (map (apfst key) (a # binds)) \<circ> key) x = map_of (a # binds) x proof (prove)
goal (1 subgoal):
 1. \<And>a binds x. \<lbrakk>\<And>x. inj key \<Longrightarrow> (map_of (map (apfst key) binds) \<circ> key) x = map_of binds x; inj key\<rbrakk> \<Longrightarrow> (map_of (map (apfst key) (a # binds)) \<circ> key) x = map_of (a # binds) x proof (prove)
goal:
No subgoals!
theory FastMap

lemma lookup_tree_to_list_of_gen:
  "\<lbrakk> inj key;
     fst (lookup_tree_valid key tree);
     lookup_tree_to_list tree = binds
   \<rbrakk> \<Longrightarrow> lookup_tree key tree = map_of binds \<and> distinct (map fst binds)" using lookup_tree_to_list_of apply (fastforce intro: lookup_tree_to_list_of_distinct
                   simp: map_of_key distinct_inj) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>inj key; fst (lookup_tree_valid key tree); lookup_tree_to_list tree = binds\<rbrakk> \<Longrightarrow> lookup_tree key tree = map_of binds \<and> distinct (map fst binds) proof (prove)
using this:
fst (lookup_tree_valid ?key ?tree) \<Longrightarrow> lookup_tree ?key ?tree = map_of (map (apfst ?key) (lookup_tree_to_list ?tree)) \<circ> ?key

goal (1 subgoal):
 1. \<lbrakk>inj key; fst (lookup_tree_valid key tree); lookup_tree_to_list tree = binds\<rbrakk> \<Longrightarrow> lookup_tree key tree = map_of binds \<and> distinct (map fst binds) proof (prove)
goal:
No subgoals!
theory FastMap

lemma dom_map_of_conv_list:
  "dom (map_of xs) = set (map fst xs)" by (simp add: dom_map_of_conv_image_fst)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. dom (map_of xs) = set (map fst xs)
theory FastMap

lemma ran_map_of_conv_list:
  "distinct (map fst xs) \<Longrightarrow> ran (map_of xs) = set (map snd xs)" by (erule distinct_map_via_ran)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. distinct (map fst xs) \<Longrightarrow> ran (map_of xs) = set (map snd xs)