refine reduction from HOL to HOL-Nat

#Untitled-2#

@@ -0,0 +1 @@
+xckdxcddsc*s

Cook_Levin/IMP-_To_SAS+/.IMP_Minus_Max_Constant_IMP_Minus.thy.marks

@@ -0,0 +1 @@
+!a;4288;4288

Cook_Levin/IMP-_To_SAS+/IMP--_To_SAS++/IMP_Minus_Minus_Subprograms.thy

@@ -2,7 +2,8 @@
 
 section \<open>IMP-- Subprograms\<close>
 
-theory IMP_Minus_Minus_Subprograms imports "../IMP_Minus_Minus_Small_StepT"
+theory IMP_Minus_Minus_Subprograms
+  imports IMP_Minus_Minus_Small_StepT
 begin
 
 text \<open>We give functions that enumerate all subprograms of an IMP-- program, that is, all 

Cook_Levin/IMP-_To_SAS+/IMP--_To_SAS++/IMP_Minus_Minus_To_SAS_Plus_Plus_Correctness.thy

@@ -3,7 +3,7 @@
 section "IMP-- to SAS++ Correctness"
 
 theory IMP_Minus_Minus_To_SAS_Plus_Plus_Correctness 
-  imports IMP_Minus_Minus_To_SAS_Plus_Plus_Reduction "../SAS_Plus_Plus"
+  imports IMP_Minus_Minus_To_SAS_Plus_Plus_Reduction SAS_Plus_Plus
 begin 
 
 text \<open> We show correctness for the IMP-- to SAS++ reduction. \<close>

Cook_Levin/IMP-_To_SAS+/IMP--_To_SAS++/IMP_Minus_Minus_To_SAS_Plus_Plus_Reduction.thy

@@ -19,7 +19,11 @@ type_synonym operator = "(variable, domain_element) sas_plus_operator"
 type_synonym problem = "(variable, domain_element) sas_plus_problem"
 
 definition pc_to_com :: "(variable \<times> domain_element) list \<Rightarrow> com" where
-"pc_to_com l = (case  l ! 0 of (_, PCV x) \<Rightarrow> x)"
+"pc_to_com l = (if l = [] then SKIP else (case  l ! 0 of (_, PCV x) \<Rightarrow> x | t \<Rightarrow> SKIP))"
+
+lemma pc_to_com_def2 :"l \<noteq> [] \<Longrightarrow> pc_to_com l = (case  l ! 0 of (_, PCV x) \<Rightarrow> x | t \<Rightarrow> SKIP)"
+  apply (auto simp add: pc_to_com_def)
+  done
 
 fun com_to_operators :: "com \<Rightarrow> operator list" where
 "com_to_operators (SKIP) = []" |
@@ -144,16 +148,18 @@ lemma map_of_precondition_of_op_PC[simp]: "op \<in> set (com_to_operators c)
 
 lemma pc_to_com_precondition_of_op_PC [simp]: "op \<in> set (com_to_operators c) 
   \<Longrightarrow> pc_to_com (precondition_of op) = c"
-  using PC_of_precondition  
-  by (metis PC_in_effect_precondition domain_element.simps nth_mem old.prod.case pc_to_com_def 
-      precondition_nonempty)
+  using PC_of_precondition  pc_to_com_def2
+  by (metis PC_in_effect_precondition domain_element.simps(6) 
+        length_greater_0_conv nth_mem old.prod.case precondition_nonempty)
+
 
 lemma pc_to_com_effect[simp]: "op \<in> set (com_to_operators c) 
   \<Longrightarrow> (PC, y) \<in> set (effect_of op) \<longleftrightarrow> y = PCV (pc_to_com (effect_of op))"
   using com_to_operators_variables_distinct PC_in_effect_precondition 
-  by (auto simp: pc_to_com_def)
-   (metis domain_element.simps effect_nonempty eq_key_imp_eq_value nth_mem old.prod.case)+
-
+  pc_to_com_def2
+  by (metis domain_element.simps(6) effect_nonempty eq_key_imp_eq_value length_greater_0_conv
+ nth_mem old.prod.case)
+
 lemma PC_of_effect[simp]: "op \<in> set (com_to_operators c) 
   \<Longrightarrow> map_of (effect_of op) PC = Some (PCV (pc_to_com (effect_of op)))"
   using com_to_operators_variables_distinct PC_in_effect_precondition