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_ASN_gateway_FT1 =
let
val specialization = (UNDISCH_ALL o REWRITE_RULE[FLAT,MEM] o SPEC_ALL o ISPECL [``p:(α -> bool) # ((α -> bool) -> bool) # ((α -> bool) -> real)``,``5:real``,``FD:'a->extreal``, ``AP:'a->extreal``,`` FF1:'a->extreal``,`` D1:'a->extreal``,`` D4:'a->extreal``,`` D7:'a->extreal``,`` D10:'a->extreal``,`` E1:'a->extreal``,`` E2:'a->extreal``,`` E3:'a->extreal``,`` E4:'a->extreal``, ``E5:'a->extreal``, ``E6:'a->extreal``, ``E7:'a->extreal``, ``E8:'a->extreal``, ``E9:'a->extreal``, ``E10:'a->extreal``, ``E11:'a->extreal``, ``E12:'a->extreal``,
      ``E13:'a->extreal``, ``E14:'a->extreal``, ``E15:'a->extreal``, ``E16:'a->extreal``, ``E17:'a->extreal``, ``E18:'a->extreal``, ``E19:'a->extreal``, ``E20:'a->extreal``, ``E21:'a->extreal``, ``C5:'a->extreal``, ``C6:'a->extreal``, ``C7:'a->extreal``, ``C8:'a->extreal``, ``notshw:'a->extreal``, ``AL:'a->extreal``, ``SL:'a->extreal``, ``PD:'a->extreal``,
      ``Others:'a->extreal``, ``time:'a->extreal``, ``ED:'a->extreal``, ``EQ1:'a->extreal``, ``EN1:'a->extreal``, ``EN2:'a->extreal``, ``EN3:'a->extreal``, ``EN4:'a->extreal``, ``human:'a->extreal``, ``0.5:real``,  ``0.3:real``,  ``0.1:real``,  ``0.4:real``,
       ``0.3:real`` , ``0.8:real`` , ``0.9:real`` , ``0.7:real`` , ``0.8:real`` , ``0.6:real`` , ``0.2:real``, ``0.7:real`` , ``0.3:real`` , ``0.1:real``
      , ``0.5:real`` , ``0.6:real`` , ``0.3:real`` , ``0.1:real``, ``0.1:real`` , ``0.4:real``, ``0.1:real``, ``0.1:real`` , ``0.1:real`` , ``0.1:real`` , ``0.1:real`` , ``0.1:real``
      , ``0.1:real`` , ``0.1:real``, ``0.1:real``  , ``0.1:real`` , ``0.1:real`` , ``0.1:real`` , ``0.1:real`` , ``0.1:real`` , ``0.1:real`` , ``0.1:real`` , ``0.01:real`` , ``0.6:real``
      , ``0.2:real``, ``0.4:real`` , ``0.3:real`` , ``0.1:real`` , ``0.7:real`` , ``0.9:real``, ``0.6:real`` ]) ASN_gateway_thm
val computation =
       ( CONV_RULE(SIMP_CONV real_ss[list_sum_def]) o CONV_RULE(SIMP_CONV list_ss[list_prod_def,one_minus_list_def,exp_func_def,exp_func_list_def,list_prod_def]) o REWRITE_RULE[list_prod_def,one_minus_list_def,exp_func_list_def,one_minus_exp_prod_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 (String.concat (map (fn t => term_to_string t ^ "\n\n") (hyp computation)));
            print "\n\n";
      print (term_to_string (concl computation));
print "\n\n";
print (Real.toString ( value) ^ "\n\n")
end;