app load
 ["bossLib", "metisLib", "realLib", "numLib", "listLib"];

open bossLib metisLib realLib numLib listLib;


(**********************)
fun sml_of_hol_real_op t =
  if t = ``($*):real->real->real`` then Real.*
  else if t = ``($+):real->real->real`` then Real.+
  else if t = ``($/):real->real->real`` then Real./
  else if t = ``($-):real->real->real`` then Real.-
  else failwith "Unrecognized HOL operator";


(************************************)

fun sml_of_hol_real t =
  let val failstring = "Symbolic expression could not be translated in a number" in
    case strip_comb t of 
       (f,[a1,a2]) => sml_of_hol_real_op f (sml_of_hol_real a1,sml_of_hol_real a2)
       | (f,[a]) =>
           if f = ``($&):num -> real``
           then Arbnum.toReal (dest_numeral a)
           else failwith failstring
       | _ => failwith failstring
  end;

(***************************************)
val  auto_solar_RBD_avail =
let
val specialization = (UNDISCH_ALL o REWRITE_RULE[FLAT,MEM]  o SPEC_ALL o ISPECL [``p:(α -> bool) # ((α -> bool) -> bool) # ((α -> bool) -> real)``,``R1:(('a->extreal)#('a->extreal))list``,``R2:(('a->extreal)#('a->extreal))list``,``R3:(('a->extreal)#('a->extreal))list``,``R4:(('a->extreal)#('a->extreal))list``,``R5:(('a->extreal)#('a->extreal))list``,``(0.1,0.3):real#real``,``(0.2,0.5):real#real``,``(0.3,0.4):real#real``,``(0.7,0.8):real#real``,``(0.5,0.5):real#real``]) solar_array_ABD_thm
val computation =
       ( CONV_RULE(SIMP_CONV real_ss[]) o REWRITE_RULE[ REAL_MUL_LZERO,REAL_MUL_RZERO,list_prod_def,one_minus_list_def,steady_state_avail_def,compl_steady_state_avail_def
        ] o BETA_RULE  o REWRITE_RULE[LENGTH,MAP]) specialization
val value = sml_of_hol_real (rhs (concl computation))
in
      print "Under the following assumptions:\n";
      print (term_to_string (concl computation));
      print "\n\n";
print (String.concat (map (fn t => term_to_string t ^ "\n\n") (hyp computation)));
print "\n\n";
print (term_to_string (lhs (concl computation)));
print (Real.toString ( value) ^ "\n\n")
end;

(*-----------------*)