text_formalization/general/state_manager.hl

   1 (* ========================================================================== *)
   2 (* FLYSPECK - BOOK FORMALIZATION                                              *)
   3 (*                                                                            *)
   4 (* Chapter: general                                                       *)
   5 (* Author: Thomas C. Hales                                                    *)
   6 (* Date: 2010-02-13                                                           *)
   7 (* ========================================================================== *)
   8
   9
  10 module State_manager:sig
  11   val neutralize_state:unit->unit
  12   end = struct
  13
  14 (*
  15 not neutralized:
  16 set_jrh_lexer;;
  17 installed printers...
  18
  19 binders, infixes, and prefixes add on July 18, 2010.
  20 *)
  21
  22 (*
  23 Bring conversions back to the following state of hol_version 2.20+ 100110:
  24
  25 basic_convs();;
  26 val it : (string * (term * conv)) list =
  27   [("FUN_ONEPATTERN_CONV", (`_FUNCTION (\y z. P y z) x`, <fun>));
  28    ("MATCH_ONEPATTERN_CONV", (`_MATCH x (\y z. P y z)`, <fun>));
  29    ("FUN_SEQPATTERN_CONV", (`_FUNCTION (_SEQPATTERN r s) x`, <fun>));
  30    ("MATCH_SEQPATTERN_CONV", (`_MATCH x (_SEQPATTERN r s)`, <fun>));
  31    ("GEN_BETA_CONV", (`GABS (\a. b) c`, <fun>))]
  32
  33 We cannot restore the list above if someone changes it before this file is read.
  34 The following checking can easily be defeated.  An honor system is in place.  *)
  35
  36
  37   let neutralize_basic_convs =
  38     let bc = basic_convs() in
  39     let msg = "conversions beyond hol_version 2.20+ 100110.  Cannot neutralize state" in
  40     let original=["FUN_ONEPATTERN_CONV"; "MATCH_ONEPATTERN_CONV";
  41                   "FUN_SEQPATTERN_CONV";
  42                   "MATCH_SEQPATTERN_CONV"; "GEN_BETA_CONV"] in
  43     let _ = if not(List.length(bc)=5)   then failwith ("Added "^msg) in
  44     let _ =     if not(map fst bc=original)  then failwith ("Changed "^msg) in
  45       fun () ->    set_basic_convs(bc);;
  46
  47 (*
  48 34 basic rewrites
  49
  50 val rewrites : thm list =
  51   [|- FST (x,y) = x; |- SND (x,y) = y; |- FST x,SND x = x;
  52    |- (if x = x then y else z) = y; |- (if T then t1 else t2) = t1;
  53    |- (if F then t1 else t2) = t2; |- ~ ~t <=> t; |- (@y. y = x) = x;
  54    |- x = x <=> T; |- (T <=> t) <=> t; |- (t <=> T) <=> t;
  55    |- (F <=> t) <=> ~t; |- (t <=> F) <=> ~t; |- ~T <=> F; |- ~F <=> T;
  56    |- T /\ t <=> t; |- t /\ T <=> t; |- F /\ t <=> F; |- t /\ F <=> F;
  57    |- t /\ t <=> t; |- T \/ t <=> T; |- t \/ T <=> T; |- F \/ t <=> t;
  58    |- t \/ F <=> t; |- t \/ t <=> t; |- T ==> t <=> t; |- t ==> T <=> T;
  59    |- F ==> t <=> T; |- t ==> t <=> T; |- t ==> F <=> ~t; |- (!x. t) <=> t;
  60    |- (?x. t) <=> t; |- (\x. f x) y = f y; |- x = x ==> p <=> p]
  61
  62 Again, we do not really check that this list is the one above.
  63 *)
  64
  65   let neutralize_basic_rewrites=
  66     let bw = basic_rewrites() in
  67     let msg = "Added rewrites beyond hol_version 2.20+ 100110.  Cannot neutralize" in
  68     let _ = if not(List.length(bw)=34) then failwith msg in
  69       fun () ->  set_basic_rewrites(bw);;
  70
  71 (*
  72 16 Basic congruences
  73
  74   [|- (!x. ~(x = a) ==> f x = g x)
  75       ==> (((\x. f x) --> l) (at a within s) <=> (g --> l) (at a within s));
  76    |- (!x. ~(x = a) ==> f x = g x)
  77       ==> (((\x. f x) --> l) (at a) <=> (g --> l) (at a));
  78    |- (!x. x IN s ==> f x = g x) ==> product s (\i. f i) = product s g;
  79    |- (!i. a <= i /\ i <= b ==> f i = g i)
  80       ==> product (a..b) (\i. f i) = product (a..b) g;
  81    |- (!x. p x ==> f x = g x)
  82       ==> product {y | p y} (\i. f i) = product {y | p y} g;
  83    |- (!x. x IN s ==> f x = g x) ==> vsum s (\i. f i) = vsum s g;
  84    |- (!i. a <= i /\ i <= b ==> f i = g i)
  85       ==> vsum (a..b) (\i. f i) = vsum (a..b) g;
  86    |- (!x. p x ==> f x = g x) ==> vsum {y | p y} (\i. f i) = vsum {y | p y} g;
  87    |- (!x. x IN s ==> f x = g x) ==> sum s (\i. f i) = sum s g;
  88    |- (!i. a <= i /\ i <= b ==> f i = g i)
  89       ==> sum (a..b) (\i. f i) = sum (a..b) g;
  90    |- (!x. p x ==> f x = g x) ==> sum {y | p y} (\i. f i) = sum {y | p y} g;
  91    |- (!x. x IN s ==> f x = g x) ==> nsum s (\i. f i) = nsum s g;
  92    |- (!i. a <= i /\ i <= b ==> f i = g i)
  93       ==> nsum (a..b) (\i. f i) = nsum (a..b) g;
  94    |- (!x. p x ==> f x = g x) ==> nsum {y | p y} (\i. f i) = nsum {y | p y} g;
  95    |- (g <=> g')
  96       ==> (g' ==> t = t')
  97       ==> (~g' ==> e = e')
  98       ==> (if g then t else e) = (if g' then t' else e');
  99    |- (p <=> p') ==> (p' ==> (q <=> q')) ==> (p ==> q <=> p' ==> q')]
 100
 101
 102 *)
 103
 104   let neutralize_basic_congs=
 105     let bc = basic_congs() in
 106     let msg = "Added "^string_of_int(List.length bc)^
 107       " congruences.  Cannot neutralize. " in
 108     let _ = if not(List.length(bc)=16) then
 109       (let _ = map print_thm bc in failwith msg) in
 110       fun () ->  set_basic_congs(bc);;
 111
 112   let default_overload_skeletons =  (* unchanged since July 31 2009 *)
 113     [("real_interval", `:A`); ("segment", `:A`); ("interval", `:A`);
 114      ("**", `:A->B->C`); ("norm", `:A->real`); ("gcd", `:A#A->A`);
 115      ("coprime", `:A#A->bool`); ("mod", `:A->A->A->bool`);
 116      ("divides", `:A->A->bool`); ("&", `:num->A`); ("min", `:A->A->A`);
 117      ("max", `:A->A->A`); ("abs", `:A->A`); ("inv", `:A->A`);
 118      ("pow", `:A->num->A`); ("--", `:A->A`); (">=", `:A->A->bool`);
 119      (">", `:A->A->bool`); ("<=", `:A->A->bool`); ("<", `:A->A->bool`);
 120      ("/", `:A->A->A`); ("*", `:A->A->A`); ("-", `:A->A->A`);
 121      ("+", `:A->A->A`)];;
 122
 123   let neutralize_overload_skeletons()=
 124     the_overload_skeletons:= default_overload_skeletons;;
 125
 126
 127   let the_default_interface = (* set on Feb 12 2010 *)
 128     [("+", ("real_add", `:real->real->real`));
 129      ("-", ("real_sub", `:real->real->real`));
 130      ("*", ("real_mul", `:real->real->real`));
 131      ("/", ("real_div", `:real->real->real`));
 132      ("<", ("real_lt", `:real->real->bool`));
 133      ("<=", ("real_le", `:real->real->bool`));
 134      (">", ("real_gt", `:real->real->bool`));
 135      (">=", ("real_ge", `:real->real->bool`));
 136      ("--", ("real_neg", `:real->real`));
 137      ("pow", ("real_pow", `:real->num->real`));
 138      ("inv", ("real_inv", `:real->real`));
 139      ("abs", ("real_abs", `:real->real`));
 140      ("max", ("real_max", `:real->real->real`));
 141      ("min", ("real_min", `:real->real->real`));
 142      ("&", ("real_of_num", `:num->real`));
 143      ("mod", ("real_mod", `:real->real->real->bool`));
 144      ("+", ("vector_add", `:real^N->real^N->real^N`));
 145      ("-", ("vector_sub", `:real^N->real^N->real^N`));
 146      ("--", ("vector_neg", `:real^N->real^N`));
 147      ("norm", ("vector_norm", `:real^N->real`));
 148      ("**", ("vector_matrix_mul", `:real^M->real^N^M->real^N`));
 149      ("+", ("+", `:num->num->num`)); ("-", ("-", `:num->num->num`));
 150      ("*", ("*", `:num->num->num`)); ("<", ("<", `:num->num->bool`));
 151      ("<=", ("<=", `:num->num->bool`)); (">", (">", `:num->num->bool`));
 152      (">=", (">=", `:num->num->bool`));
 153      ("divides", ("num_divides", `:num->num->bool`));
 154      ("mod", ("num_mod", `:num->num->num->bool`));
 155      ("coprime", ("num_coprime", `:num#num->bool`));
 156      ("gcd", ("num_gcd", `:num#num->num`));
 157      ("+", ("int_add", `:int->int->int`));
 158      ("-", ("int_sub", `:int->int->int`));
 159      ("*", ("int_mul", `:int->int->int`));
 160      ("<", ("int_lt", `:int->int->bool`));
 161      ("<=", ("int_le", `:int->int->bool`));
 162      (">", ("int_gt", `:int->int->bool`));
 163      (">=", ("int_ge", `:int->int->bool`)); ("--", ("int_neg", `:int->int`));
 164      ("pow", ("int_pow", `:int->num->int`)); ("abs", ("int_abs", `:int->int`));
 165      ("max", ("int_max", `:int->int->int`));
 166      ("min", ("int_min", `:int->int->int`));
 167      ("&", ("int_of_num", `:num->int`));
 168      ("divides", ("int_divides", `:int->int->bool`));
 169      ("mod", ("int_mod", `:int->int->int->bool`));
 170      ("coprime", ("int_coprime", `:int#int->bool`));
 171      ("gcd", ("int_gcd", `:int#int->int`));
 172      ("inv", ("complex_inv", `:real^2->real^2`));
 173      ("pow", ("complex_pow", `:real^2->num->real^2`));
 174      ("/", ("complex_div", `:real^2->real^2->real^2`));
 175      ("*", ("complex_mul", `:real^2->real^2->real^2`));
 176      ("-", ("vector_sub", `:real^2->real^2->real^2`));
 177      ("+", ("vector_add", `:real^2->real^2->real^2`));
 178      ("--", ("vector_neg", `:real^2->real^2`));
 179      ("vol", ("measure", `:(real^3->bool)->real`));
 180      ("NULLSET", ("negligible", `:(real^3->bool)->bool`));
 181      ("real_interval",
 182       ("closed_real_interval", `:(real#real)list->real->bool`));
 183      ("real_interval", ("open_real_interval", `:real#real->real->bool`));
 184      ("segment", ("closed_segment", `:(real^A#real^A)list->real^A->bool`));
 185      ("segment", ("open_segment", `:real^A#real^A->real^A->bool`));
 186      ("interval", ("closed_interval", `:(real^A#real^A)list->real^A->bool`));
 187      ("interval", ("open_interval", `:real^A#real^A->real^A->bool`));
 188      ("**", ("matrix_vector_mul", `:real^N^M->real^N->real^M`));
 189      ("**", ("matrix_mul", `:real^N^M->real^P^N->real^P^M`));
 190      ("-", ("matrix_sub", `:real^N^M->real^N^M->real^N^M`));
 191      ("+", ("matrix_add", `:real^N^M->real^N^M->real^N^M`));
 192      ("--", ("matrix_neg", `:real^N^M->real^N^M`));
 193      ("dist", ("distance", `:real^N#real^N->real`));
 194      ("&", ("hreal_of_num", `:num->hreal`));
 195      ("<=>", ("=", `:bool->bool->bool`))];;
 196
 197   let neutralize_interface()=
 198     the_interface:= the_default_interface;;
 199
 200 let set_parsel f g h xl =
 201    (let _ = map f (h()) in let _ =  map g xl in ());;
 202
 203 let neutralize_binders() =
 204   let bind = ["\\"; "!"; "?"; "?!"; "@"; "minimal"; "lambda"] in
 205   set_parsel unparse_as_binder parse_as_binder binders bind;;
 206
 207 let neutralize_prefixes() =
 208   let pre = ["~"; "--"; "mod"] in
 209   set_parsel unparse_as_prefix parse_as_prefix prefixes pre;;
 210
 211 let neutralize_infixes() =
 212   let inf =   [("<=>", (2, "right")); ("==>", (4, "right")); ("\\/", (6, "right"));
 213    ("/\\", (8, "right")); ("==", (10, "right")); ("===", (10, "right"));
 214    ("treal_eq", (10, "right")); ("IN", (11, "right"));
 215    ("--->", (12, "right")); ("-->", (12, "right")); ("<", (12, "right"));
 216    ("<<", (12, "right"));
 217    ("<<<", (12, "right")); ("<<=", (12, "right")); ("<=", (12, "right"));
 218   ("<=_c", (12, "right"));
 219     ("<_c", (12, "right"));
 220    ("=", (12, "right")); ("=_c", (12, "right")); (">", (12, "right"));
 221   (">=", (12, "right"));
 222   (">=_c", (12, "right"));
 223     (">_c", (12, "right"));
 224    ("HAS_SIZE", (12, "right")); ("PSUBSET", (12, "right"));
 225    ("SUBSET", (12, "right")); ("absolutely_integrable_on", (12, "right"));
 226    ("absolutely_real_integrable_on", (12, "right"));
 227    ("analytic_on", (12, "right")); ("complex_differentiable", (12, "right"));
 228    ("continuous", (12, "right")); ("continuous_on", (12, "right"));
 229    ("convex_on", (12, "right")); ("differentiable", (12, "right"));
 230    ("differentiable_on", (12, "right")); ("divides", (12, "right"));
 231    ("division_of", (12, "right")); ("edge_of", (12, "right"));
 232    ("exposed_face_of", (12, "right")); ("extreme_point_of", (12, "right"));
 233    ("face_of", (12, "right")); ("facet_of", (12, "right"));
 234    ("fine", (12, "right")); ("has_complex_derivative", (12, "right"));
 235    ("has_derivative", (12, "right")); ("has_integral", (12, "right"));
 236    ("has_integral_compact_interval", (12, "right"));
 237    ("has_measure", (12, "right")); ("has_real_derivative", (12, "right"));
 238    ("has_real_integral", (12, "right")); ("has_real_measure", (12, "right"));
 239    ("has_vector_derivative", (12, "right"));
 240    ("holomorphic_on", (12, "right")); ("homeomorphic", (12, "right"));
 241    ("inseg", (12, "right")); ("integrable_on", (12, "right"));
 242    ("limit_point_of", (12, "right")); ("permutes", (12, "right"));
 243    ("real_continuous", (12, "right")); ("real_continuous_on", (12, "right"));
 244    ("real_convex_on", (12, "right")); ("real_differentiable", (12, "right"));
 245    ("real_differentiable_on", (12, "right"));
 246    ("real_integrable_on", (12, "right")); ("real_sums", (12, "right"));
 247    ("real_uniformly_continuous_on", (12, "right"));
 248    ("retract_of", (12, "right")); ("simplex", (12, "right"));
 249    ("sums", (12, "right")); ("tagged_division_of", (12, "right"));
 250    ("tagged_partial_division_of", (12, "right"));
 251    ("treal_le", (12, "right")); ("uniformly_continuous_on", (12, "right"));
 252    (",", (14, "right")); ("in_direction", (14, "right"));
 253    ("within", (14, "right")); ("..", (15, "right")); ("+", (16, "right"));
 254    ("++", (16, "right"));
 255    ("+_c", (16, "right"));  ("UNION", (16, "right"));
 256    ("treal_add", (16, "right")); ("-", (18, "left"));
 257     ("DIFF", (18, "left")); ("*", (20, "right"));
 258    ("**", (20, "right"));
 259    ("*_c", (20, "right")); ("INTER", (20, "right"));
 260    ("cross", (20, "right")); ("dot", (20, "right"));
 261    ("treal_mul", (20, "right")); ("%", (21, "right"));
 262    ("INSERT", (21, "right")); ("DELETE", (21, "left"));
 263    ("hull", (21, "left")); ("CROSS", (22, "right"));
 264     ("/", (22, "left")); ("DIV", (22, "left"));
 265    ("MOD", (22, "left")); ("div", (22, "left")); ("rem", (22, "left"));
 266    ("POWER",(24,"right"));
 267    ("EXP", (24, "left")); ("cpow", (24, "left")); ("pow", (24, "left"));
 268    ("$", (25, "left")); ("o", (26, "right"))]
 269     in
 270   set_parsel (fun (a,_) -> unparse_as_infix a) parse_as_infix infixes inf ;;
 271
 272
 273
 274   (* What we cannot neutralize we destroy *)
 275
 276   let neutralize_axioms() =
 277     if not(List.length(axioms()) =3) then failwith ("Further axioms are not allowed");;
 278
 279
 280   let neutralize_state()=
 281     (
 282       current_goalstack := ([]:goalstack);
 283       neutralize_overload_skeletons();
 284       neutralize_interface();
 285       neutralize_basic_congs();
 286       neutralize_basic_convs();
 287       neutralize_basic_rewrites();
 288       neutralize_binders();
 289       neutralize_prefixes();
 290       neutralize_infixes();
 291       neutralize_axioms();
 292     );;
 293
 294 end;;