theory StateTranslation_D

lemma transform_intent_isnot_UntypedIntent:
      "(\<not> (\<exists> ui. Some (UntypedIntent ui) = transform_intent label args))
       = ((label \<noteq> GenInvocationLabel UntypedRetype) \<or>
           (label = GenInvocationLabel UntypedRetype \<and> length args < 6) \<or>
           (label = GenInvocationLabel UntypedRetype \<and> length args \<ge> 6 \<and> args ! 0 > 10))" apply(rule iffI) apply(erule contrapos_np) apply(clarsimp) apply(simp add: transform_intent_def) apply(unfold transform_intent_untyped_retype_def) apply (clarsimp split: list.split, safe, simp_all)[1] apply (clarsimp simp: transform_type_def) apply (simp add: unat_arith_simps) apply (simp add: eval_nat_numeral linorder_not_less le_Suc_eq) apply(erule disjE) apply(auto simp: transform_intent_def option_map_def
              split: gen_invocation_labels.split invocation_label.split arch_invocation_label.split
                     option.split_asm)[1] apply (erule disjE) apply (auto simp: transform_intent_def transform_intent_untyped_retype_def
         option_map_def split: invocation_label.split option.split_asm list.split)[1] apply clarsimp apply (clarsimp simp: transform_intent_def transform_type_def transform_intent_untyped_retype_def) apply (clarsimp simp: option_map_def
                  split: invocation_label.splits arch_invocation_label.splits option.splits list.splits) apply (clarsimp simp: transform_type_def split: if_split_asm) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<nexists>ui. Some (UntypedIntent ui) = transform_intent label args) = (label \<noteq> GenInvocationLabel UntypedRetype \<or> label = GenInvocationLabel UntypedRetype \<and> length args < 6 \<or> label = GenInvocationLabel UntypedRetype \<and> 6 \<le> length args \<and> 0xA < args ! 0) proof (prove)
goal (2 subgoals):
 1. \<nexists>ui. Some (UntypedIntent ui) = transform_intent label args \<Longrightarrow> label \<noteq> GenInvocationLabel UntypedRetype \<or> label = GenInvocationLabel UntypedRetype \<and> length args < 6 \<or> label = GenInvocationLabel UntypedRetype \<and> 6 \<le> length args \<and> 0xA < args ! 0
 2. label \<noteq> GenInvocationLabel UntypedRetype \<or> label = GenInvocationLabel UntypedRetype \<and> length args < 6 \<or> label = GenInvocationLabel UntypedRetype \<and> 6 \<le> length args \<and> 0xA < args ! 0 \<Longrightarrow> \<nexists>ui. Some (UntypedIntent ui) = transform_intent label args proof (prove)
goal (2 subgoals):
 1. \<not> (label \<noteq> GenInvocationLabel UntypedRetype \<or> label = GenInvocationLabel UntypedRetype \<and> length args < 6 \<or> label = GenInvocationLabel UntypedRetype \<and> 6 \<le> length args \<and> 0xA < args ! 0) \<Longrightarrow> \<exists>ui. Some (UntypedIntent ui) = transform_intent label args
 2. label \<noteq> GenInvocationLabel UntypedRetype \<or> label = GenInvocationLabel UntypedRetype \<and> length args < 6 \<or> label = GenInvocationLabel UntypedRetype \<and> 6 \<le> length args \<and> 0xA < args ! 0 \<Longrightarrow> \<nexists>ui. Some (UntypedIntent ui) = transform_intent label args proof (prove)
goal (2 subgoals):
 1. \<lbrakk>label = GenInvocationLabel UntypedRetype; \<not> length args < 6; \<not> 0xA < args ! 0\<rbrakk> \<Longrightarrow> \<exists>ui. Some (UntypedIntent ui) = transform_intent (GenInvocationLabel UntypedRetype) args
 2. label \<noteq> GenInvocationLabel UntypedRetype \<or> label = GenInvocationLabel UntypedRetype \<and> length args < 6 \<or> label = GenInvocationLabel UntypedRetype \<and> 6 \<le> length args \<and> 0xA < args ! 0 \<Longrightarrow> \<nexists>ui. Some (UntypedIntent ui) = transform_intent label args proof (prove)
goal (2 subgoals):
 1. \<lbrakk>label = GenInvocationLabel UntypedRetype; \<not> length args < 6; \<not> 0xA < args ! 0\<rbrakk> \<Longrightarrow> \<exists>ui. Some (UntypedIntent ui) = map_option UntypedIntent (transform_intent_untyped_retype args)
 2. label \<noteq> GenInvocationLabel UntypedRetype \<or> label = GenInvocationLabel UntypedRetype \<and> length args < 6 \<or> label = GenInvocationLabel UntypedRetype \<and> 6 \<le> length args \<and> 0xA < args ! 0 \<Longrightarrow> \<nexists>ui. Some (UntypedIntent ui) = transform_intent label args proof (prove)
goal (2 subgoals):
 1. \<lbrakk>label = GenInvocationLabel UntypedRetype; \<not> length args < 6; \<not> 0xA < args ! 0\<rbrakk> \<Longrightarrow> \<exists>ui. Some (UntypedIntent ui) = map_option UntypedIntent (case args of [] \<Rightarrow> None | [type] \<Rightarrow> None | [type, size_bits] \<Rightarrow> None | [type, size_bits, index] \<Rightarrow> None | [type, size_bits, index, depth] \<Rightarrow> None | [type, size_bits, index, depth, offset] \<Rightarrow> None | type # size_bits # index # depth # offset # window # xa \<Rightarrow> case transform_type type of None \<Rightarrow> None | Some x \<Rightarrow> Some (UntypedRetypeIntent x size_bits index depth offset window))
 2. label \<noteq> GenInvocationLabel UntypedRetype \<or> label = GenInvocationLabel UntypedRetype \<and> length args < 6 \<or> label = GenInvocationLabel UntypedRetype \<and> 6 \<le> length args \<and> 0xA < args ! 0 \<Longrightarrow> \<nexists>ui. Some (UntypedIntent ui) = transform_intent label args proof (prove)
goal (2 subgoals):
 1. \<And>x21 x21a x21b x21c x21d x21e x22e. \<lbrakk>label = GenInvocationLabel UntypedRetype; \<not> 0xA < x21; args = x21 # x21a # x21b # x21c # x21d # x21e # x22e\<rbrakk> \<Longrightarrow> \<exists>ui. Some (UntypedIntent ui) = map_option UntypedIntent (case transform_type x21 of None \<Rightarrow> None | Some x \<Rightarrow> Some (UntypedRetypeIntent x x21a x21b x21c x21d x21e))
 2. label \<noteq> GenInvocationLabel UntypedRetype \<or> label = GenInvocationLabel UntypedRetype \<and> length args < 6 \<or> label = GenInvocationLabel UntypedRetype \<and> 6 \<le> length args \<and> 0xA < args ! 0 \<Longrightarrow> \<nexists>ui. Some (UntypedIntent ui) = transform_intent label args proof (prove)
goal (2 subgoals):
 1. \<And>x21 x21a x21b x21c x21d x21e x22e. \<lbrakk>label = GenInvocationLabel UntypedRetype; \<not> 0xA < x21; args = x21 # x21a # x21b # x21c # x21d # x21e # x22e; x21 \<noteq> 0xA; x21 \<noteq> 9; x21 \<noteq> 8; x21 \<noteq> 7; x21 \<noteq> 6; x21 \<noteq> 5; x21 \<noteq> 4; x21 \<noteq> 3; x21 \<noteq> 2; x21 \<noteq> 1\<rbrakk> \<Longrightarrow> x21 = 0
 2. label \<noteq> GenInvocationLabel UntypedRetype \<or> label = GenInvocationLabel UntypedRetype \<and> length args < 6 \<or> label = GenInvocationLabel UntypedRetype \<and> 6 \<le> length args \<and> 0xA < args ! 0 \<Longrightarrow> \<nexists>ui. Some (UntypedIntent ui) = transform_intent label args proof (prove)
goal (2 subgoals):
 1. \<And>x21 x21a x21b x21c x21d x21e x22e. \<lbrakk>label = GenInvocationLabel UntypedRetype; \<not> 10 < unat x21; args = x21 # x21a # x21b # x21c # x21d # x21e # x22e; unat x21 \<noteq> 10; unat x21 \<noteq> 9; unat x21 \<noteq> 8; unat x21 \<noteq> 7; unat x21 \<noteq> 6; unat x21 \<noteq> 5; unat x21 \<noteq> 4; unat x21 \<noteq> 3; unat x21 \<noteq> 2; unat x21 \<noteq> Suc 0\<rbrakk> \<Longrightarrow> unat x21 = 0
 2. label \<noteq> GenInvocationLabel UntypedRetype \<or> label = GenInvocationLabel UntypedRetype \<and> length args < 6 \<or> label = GenInvocationLabel UntypedRetype \<and> 6 \<le> length args \<and> 0xA < args ! 0 \<Longrightarrow> \<nexists>ui. Some (UntypedIntent ui) = transform_intent label args proof (prove)
goal (1 subgoal):
 1. label \<noteq> GenInvocationLabel UntypedRetype \<or> label = GenInvocationLabel UntypedRetype \<and> length args < 6 \<or> label = GenInvocationLabel UntypedRetype \<and> 6 \<le> length args \<and> 0xA < args ! 0 \<Longrightarrow> \<nexists>ui. Some (UntypedIntent ui) = transform_intent label args proof (prove)
goal (2 subgoals):
 1. label \<noteq> GenInvocationLabel UntypedRetype \<Longrightarrow> \<nexists>ui. Some (UntypedIntent ui) = transform_intent label args
 2. label = GenInvocationLabel UntypedRetype \<and> length args < 6 \<or> label = GenInvocationLabel UntypedRetype \<and> 6 \<le> length args \<and> 0xA < args ! 0 \<Longrightarrow> \<nexists>ui. Some (UntypedIntent ui) = transform_intent label args proof (prove)
goal (1 subgoal):
 1. label = GenInvocationLabel UntypedRetype \<and> length args < 6 \<or> label = GenInvocationLabel UntypedRetype \<and> 6 \<le> length args \<and> 0xA < args ! 0 \<Longrightarrow> \<nexists>ui. Some (UntypedIntent ui) = transform_intent label args proof (prove)
goal (2 subgoals):
 1. label = GenInvocationLabel UntypedRetype \<and> length args < 6 \<Longrightarrow> \<nexists>ui. Some (UntypedIntent ui) = transform_intent label args
 2. label = GenInvocationLabel UntypedRetype \<and> 6 \<le> length args \<and> 0xA < args ! 0 \<Longrightarrow> \<nexists>ui. Some (UntypedIntent ui) = transform_intent label args proof (prove)
goal (1 subgoal):
 1. label = GenInvocationLabel UntypedRetype \<and> 6 \<le> length args \<and> 0xA < args ! 0 \<Longrightarrow> \<nexists>ui. Some (UntypedIntent ui) = transform_intent label args proof (prove)
goal (1 subgoal):
 1. \<And>ui. \<lbrakk>label = GenInvocationLabel UntypedRetype; 6 \<le> length args; 0xA < args ! 0; Some (UntypedIntent ui) = transform_intent (GenInvocationLabel UntypedRetype) args\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>ui. \<lbrakk>label = GenInvocationLabel UntypedRetype; 6 \<le> length args; 0xA < args ! 0; Some (UntypedIntent ui) = map_option UntypedIntent (case args of [] \<Rightarrow> None | [type] \<Rightarrow> None | [type, size_bits] \<Rightarrow> None | [type, size_bits, index] \<Rightarrow> None | [type, size_bits, index, depth] \<Rightarrow> None | [type, size_bits, index, depth, offset] \<Rightarrow> None | type # size_bits # index # depth # offset # window # x \<Rightarrow> case transform_type type of None \<Rightarrow> None | Some x \<Rightarrow> Some (UntypedRetypeIntent x size_bits index depth offset window))\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>x21 x21a x21b x21c x21d x21e x22e x2a. \<lbrakk>label = GenInvocationLabel UntypedRetype; 0xA < x21; args = x21 # x21a # x21b # x21c # x21d # x21e # x22e; transform_type x21 = Some x2a\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!