Mizarlight/miz2a.ml

   1 (* ========================================================================= *)
   2 (* Mizar Light II                                                            *)
   3 (*                                                                           *)
   4 (*                   Freek Wiedijk, University of Nijmegen                   *)
   5 (* ========================================================================= *)
   6
   7 type mterm = string;;
   8
   9 let parse_context_term s env =
  10   let ptm,l = (parse_preterm o lex o explode) s in
  11   if l = [] then
  12    (term_of_preterm o retypecheck
  13      (map ((fun (s,ty) -> s,pretype_of_type ty) o dest_var) env)) ptm
  14   else failwith "Unexpected junk after term";;
  15
  16 let goal_frees (asl,w as g) =
  17   frees (itlist (curry mk_imp) (map (concl o snd) asl) w);;
  18
  19 let (parse_mterm: mterm -> goal -> term) =
  20   let ttm = mk_var("thesis",bool_ty) in
  21   let atm = mk_var("antecedent",bool_ty) in
  22   let otm = mk_var("opposite",bool_ty) in
  23   fun s (asl,w as g) ->
  24     let ant = try fst (dest_imp w) with Failure _ -> atm in
  25     let opp = try dest_neg w with Failure _ -> mk_neg w in
  26     let t =
  27      (subst [w,ttm; ant,atm; opp,otm]
  28        (parse_context_term s ((goal_frees g) @ [ttm; atm; otm]))) in
  29     try
  30       let lhs = lhand (concl (snd (hd asl))) in
  31       let itm = mk_var("...",type_of lhs) in
  32       subst [lhs,itm] t
  33     with Failure _ -> t;;
  34
  35 type stepinfo =
  36   (goal -> term) option * int option *
  37   (goal -> thm list) * (thm list -> tactic);;
  38
  39 type step = (stepinfo -> tactic) * stepinfo;;
  40
  41 let TRY' tac thl = TRY (tac thl);;
  42
  43 let (then'_) = fun tac1 tac2 thl -> tac1 thl THEN tac2 thl;;
  44
  45 let standard_prover = TRY' (REWRITE_TAC THEN' MESON_TAC);;
  46 let sketch_prover = K CHEAT_TAC;;
  47 let current_prover = ref standard_prover;;
  48
  49 let (default_stepinfo: (goal -> term) option -> stepinfo) =
  50   fun t -> t,None,
  51     (map snd o filter ((=) "=" o fst) o fst),
  52     (fun thl -> !current_prover thl);;
  53
  54 let ((st'): step -> (goal -> term)  -> step) =
  55   fun (tac,(t,l,thl,just)) t' -> (tac,(Some t',l,thl,just));;
  56
  57 let (st) = fun stp -> (st') stp o parse_mterm;;
  58
  59 let (((at)): step -> int -> step) =
  60   fun (tac,(t,l,thl,just)) l' -> (tac,(t,Some l',thl,just));;
  61
  62 let (((from)): step -> int list -> step) =
  63   fun (tac,(t,l,thl,just)) ll -> (tac,(t,l,
  64     (fun (asl,_ as g) -> thl g @
  65       let n = length asl in
  66       map
  67         (fun l ->
  68           if l < 0 then snd (el ((n - l - 1) mod n) asl)
  69             else assoc (string_of_int l) asl)
  70         ll),
  71     just));;
  72
  73 let so x = fun y -> x y from [-1];;
  74
  75 let (((by)): step -> thm list -> step) =
  76   fun (tac,(t,l,thl,just)) thl' -> (tac,(t,l,(fun g -> thl g @ thl'),just));;
  77
  78 let (((using)): step -> (thm list -> tactic) -> step) =
  79   fun (tac,(t,l,thl,just)) just' -> (tac,(t,l,thl,just' THEN' just));;
  80
  81 let (step: step -> tactic) = fun (f,x) -> f x;;
  82
  83 let (steps: step list -> tactic) =
  84   fun stpl ->
  85     itlist (fun tac1 tac2 -> tac1 THENL [tac2]) (map step stpl) ALL_TAC;;
  86
  87 let (tactics: tactic list -> step) =
  88   fun tacl -> ((K (itlist ((THEN)) tacl ALL_TAC)),
  89     default_stepinfo None);;
  90
  91 let (theorem': (goal -> term) -> step list -> thm) =
  92   let g = ([],`T`) in
  93   fun t stpl -> prove(t g,steps stpl);;
  94
  95 let (((proof)): step -> step list -> step) =
  96   fun (tac,(t,l,thl,just)) prf -> (tac,(t,l,thl,K (steps prf)));;
  97
  98 let (N_ASSUME_TAC: int option -> thm_tactic) =
  99   fun l th (asl,_ as g) ->
 100     match l with
 101       None -> ASSUME_TAC th g
 102     | Some n ->
 103         warn (n >= 0 && length asl <> n) "*** out of sequence label ***";
 104         LABEL_TAC (if n < 0 then "=" else string_of_int n) th g;;
 105
 106 let (per: step -> step list list -> step) =
 107   let F = `F` in
 108   fun (_,(_,_,thl,just)) cases ->
 109     (fun (_,_,thl',just') g ->
 110        let tx (t',_,_,_) =
 111          match t' with None -> failwith "per" | Some t -> t g in
 112        let dj = itlist (curry mk_disj)
 113          (map (tx o snd o hd) cases) F in
 114        (SUBGOAL_THEN dj
 115           (EVERY_TCL (map (fun case -> let _,l,_,_ = snd (hd case) in
 116             (DISJ_CASES_THEN2 (N_ASSUME_TAC l))) cases) CONTR_TAC) THENL
 117         ([(just' THEN' just) ((thl' g) @ (thl g))] @
 118            map (steps o tl) cases)) g),
 119     (None,None,(K []),(K ALL_TAC));;
 120
 121 let (cases: step) =
 122   (fun _ -> failwith "cases"),default_stepinfo None;;
 123
 124 let (suppose': (goal -> term) -> step) =
 125   fun t -> (fun _ -> failwith "suppose"),default_stepinfo (Some t);;
 126
 127 let (consider': (goal -> term) list -> step) =
 128   let T = `T` in
 129   fun tl' ->
 130   (fun (t',l,thl,just) (asl,w as g) ->
 131     let tl = map (fun t' -> t' g) tl' in
 132     let g' = ((asl @ (map (fun t -> ("",REFL t)) tl)),w) in
 133     let ex = itlist (curry mk_exists) tl
 134       (match t' with
 135          None -> failwith "consider"
 136        | Some t -> t g') in
 137     (SUBGOAL_THEN ex
 138        ((EVERY_TCL (map X_CHOOSE_THEN tl)) (N_ASSUME_TAC l)) THENL
 139      [just (thl g); ALL_TAC]) g),
 140   default_stepinfo (Some
 141     (fun g -> end_itlist (curry mk_conj)
 142       (map (fun t' -> let t = t' g in mk_eq(t,t)) tl')));;
 143
 144 let (take': (goal -> term) list -> step) =
 145   fun tl ->
 146     (fun _ g -> (MAP_EVERY EXISTS_TAC o map (fun t -> t g)) tl g),
 147     default_stepinfo None;;
 148
 149 let (assume': (goal -> term) -> step) =
 150   fun t ->
 151     (fun (t',l,thl,just) g ->
 152        match t' with
 153          None -> failwith "assume"
 154        | Some t ->
 155            (DISJ_CASES_THEN2
 156               (fun th -> REWRITE_TAC[th] THEN
 157                  N_ASSUME_TAC l th)
 158               (fun th -> just ((REWRITE_RULE[] th)::(thl g)))
 159             (SPEC (t g) EXCLUDED_MIDDLE)) g),
 160     default_stepinfo (Some t);;
 161
 162 let (have': (goal -> term) -> step) =
 163   fun t ->
 164     (fun (t',l,thl,just) g ->
 165        match t' with
 166          None -> failwith "have"
 167        | Some t ->
 168            (SUBGOAL_THEN (t g) (N_ASSUME_TAC l) THENL
 169             [just (thl g); ALL_TAC]) g),
 170     default_stepinfo (Some t);;
 171
 172 let (thus': (goal -> term) -> step) =
 173   fun t ->
 174     (fun (t',l,thl,just) g ->
 175        match t' with
 176          None -> failwith "thus"
 177        | Some t ->
 178            (SUBGOAL_THEN (t g) ASSUME_TAC THENL
 179             [just (thl g);
 180              POP_ASSUM (fun th ->
 181                N_ASSUME_TAC l th THEN
 182                EVERY (map (fun th -> REWRITE_TAC[EQT_INTRO th])
 183                  (CONJUNCTS th)))])
 184            g),
 185     default_stepinfo (Some t);;
 186
 187 let (fix': (goal -> term) list -> step) =
 188   fun tl ->
 189     (fun _ g -> (MAP_EVERY X_GEN_TAC o (map (fun t -> t g))) tl g),
 190     default_stepinfo None;;
 191
 192 let (set': (goal -> term) -> step) =
 193   fun t ->
 194     let stp =
 195       (fun (t',l,_,_) g ->
 196        match t' with
 197          None -> failwith "set"
 198        | Some t ->
 199            let eq = t g in
 200            let lhs,rhs = dest_eq eq in
 201            let lv,largs = strip_comb lhs in
 202            let rtm = list_mk_abs(largs,rhs) in
 203            let ex = mk_exists(lv,mk_eq(lv,rtm)) in
 204            (SUBGOAL_THEN ex (X_CHOOSE_THEN lv
 205               (fun th -> (N_ASSUME_TAC l) (prove(eq,REWRITE_TAC[th])))) THENL
 206             [REWRITE_TAC[EXISTS_REFL];
 207              ALL_TAC]) g),
 208       default_stepinfo (Some t) in
 209     stp at -1;;
 210
 211 let theorem = theorem' o parse_mterm;;
 212 let suppose = suppose' o parse_mterm;;
 213 let consider = consider' o map parse_mterm;;
 214 let take = take' o map parse_mterm;;
 215 let assume = assume' o parse_mterm;;
 216 let have = have' o parse_mterm;;
 217 let thus = thus' o parse_mterm;;
 218 let fix = fix' o map parse_mterm;;
 219 let set = set' o parse_mterm;;
 220
 221 let iff prfs = tactics [EQ_TAC THENL map steps prfs];;
 222
 223 let (otherwise: ('a -> step) -> ('a -> step)) =
 224   fun stp x ->
 225     let tac,si = stp x in
 226     ((fun (t,l,thl,just) g ->
 227        REFUTE_THEN (fun th ->
 228          tac (t,l,K ([REWRITE_RULE[] th] @ thl g),just)) g),
 229      si);;
 230
 231 let (thesis:mterm) = "thesis";;
 232 let (antecedent:mterm) = "antecedent";;
 233 let (opposite:mterm) = "opposite";;
 234 let (contradiction:mterm) = "F";;
 235
 236 let hence = so thus;;
 237 let qed = hence thesis;;
 238
 239 let h = g o parse_term;;
 240 let f = e o step;;
 241 let ff = e o steps;;
 242 let ee = e o EVERY;;
 243 let fp = f o (fun x -> x proof []);;
 244
 245 let GOAL_HERE = tactics [GOAL_TAC];;