development/thales/examples/axiom_example.hl

   1
   2
   3
   4 module My_module = struct
   5
   6 open Pack_concl;;
   7
   8 let concl_list = [GLTVHUM_concl;DUUNHOR_concl;QXSKIIT_concl] ;;
   9
  10 let module_assum = list_mk_conj concl_list;;
  11
  12 (*
  13 frees module_assum;;
  14 type_vars_in_term module_assum;;
  15 *)
  16
  17 axioms();;
  18
  19 let my_assum =  new_definition (mk_eq (`(my_assum:(N#A->bool)) x`,module_assum));;
  20
  21 let my_thm = prove_by_refinement(
  22   `(my_assum ((@) UNIV)) ==> (!x y z. (x = y) ==> (y =x ))`,
  23   (* {{{ proof *)
  24   [
  25   REPEAT STRIP_TAC;
  26   ]);;
  27   (* }}} *)
  28
  29 let INTRO_THEN (axiom,concl) =
  30   FIRST_X_ASSUM (MATCH_MP axom
  31
  32
  33 ;;
  34 help "MATCH_MP";;
  35 INTRO_TAC (my_assum,GLTVHUM_concl);;
  36
  37 let fold_binop f = function
  38    [] -> failwith "fold_binop"
  39   | [a] -> a
  40   | a::xs -> List.fold_left f a xs;;
  41
  42 let make_assumption name concls =
  43   let concl = list_mk_conj concls in
  44   let _ = (frees concl = []) or (failwith "make_assumption: free vars") in
  45   let z = type_vars_in_term concl in
  46   let ty = if (List.length z =0) then `:bool`
  47   else
  48     let f a b = mk_type("prod",[a;b]) in
  49     let C = fold_binop f z in
  50      mk_type("fun",[C;`:bool`]) in
  51   ty;;
  52
  53
  54 mk_type("fun",[`:A`;`:B`]);;
  55 mk_type("prod",[`:A`;`:B`;`:C`]);;
  56 List.fold_left;;
  57 List.fold_right;;
  58 make_assumption "" [`T`];;
  59 concl_list;;
  60 help "mk_type";;
  61 dest_type `:A#B#C`;;
  62 mk_type ("prod",[`:A`;`:B`]);;
  63 help_grep"strip";;
  64 help "mk_list";;
  65 help_grep "mk";;
  66 striplist;;
  67 let GLTVHUM = prove(mk_comb(`GLTVHUM_concl,
  68
  69
  70
  71
  72
  73
  74
  75 end;;