1 (* ========================================================================= *)
4 (* Freek Wiedijk, University of Nijmegen *)
5 (* ========================================================================= *)
9 let parse_context_term s env =
10 let ptm,l = (parse_preterm o lex o explode) s in
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";;
16 let goal_frees (asl,w as g) =
17 frees (itlist (curry mk_imp) (map (concl o snd) asl) w);;
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
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
27 (subst [w,ttm; ant,atm; opp,otm]
28 (parse_context_term s ((goal_frees g) @ [ttm; atm; otm]))) in
30 let lhs = lhand (concl (snd (hd asl))) in
31 let itm = mk_var("...",type_of lhs) in
36 (goal -> term) option * int option *
37 (goal -> thm list) * (thm list -> tactic);;
39 type step = (stepinfo -> tactic) * stepinfo;;
41 let TRY' tac thl = TRY (tac thl);;
43 let (then'_) = fun tac1 tac2 thl -> tac1 thl THEN tac2 thl;;
45 let standard_prover = TRY' (REWRITE_TAC THEN' MESON_TAC);;
46 let sketch_prover = K CHEAT_TAC;;
47 let current_prover = ref standard_prover;;
49 let (default_stepinfo: (goal -> term) option -> stepinfo) =
51 (map snd o filter ((=) "=" o fst) o fst),
52 (fun thl -> !current_prover thl);;
54 let ((st'): step -> (goal -> term) -> step) =
55 fun (tac,(t,l,thl,just)) t' -> (tac,(Some t',l,thl,just));;
57 let (st) = fun stp -> (st') stp o parse_mterm;;
59 let (((at)): step -> int -> step) =
60 fun (tac,(t,l,thl,just)) l' -> (tac,(t,Some l',thl,just));;
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 @
68 if l < 0 then snd (el ((n - l - 1) mod n) asl)
69 else assoc (string_of_int l) asl)
73 let so x = fun y -> x y from [-1];;
75 let (((by)): step -> thm list -> step) =
76 fun (tac,(t,l,thl,just)) thl' -> (tac,(t,l,(fun g -> thl g @ thl'),just));;
78 let (((using)): step -> (thm list -> tactic) -> step) =
79 fun (tac,(t,l,thl,just)) just' -> (tac,(t,l,thl,just' THEN' just));;
81 let (step: step -> tactic) = fun (f,x) -> f x;;
83 let (steps: step list -> tactic) =
85 itlist (fun tac1 tac2 -> tac1 THENL [tac2]) (map step stpl) ALL_TAC;;
87 let (tactics: tactic list -> step) =
88 fun tacl -> ((K (itlist ((THEN)) tacl ALL_TAC)),
89 default_stepinfo None);;
91 let (theorem': (goal -> term) -> step list -> thm) =
93 fun t stpl -> prove(t g,steps stpl);;
95 let (((proof)): step -> step list -> step) =
96 fun (tac,(t,l,thl,just)) prf -> (tac,(t,l,thl,K (steps prf)));;
98 let (N_ASSUME_TAC: int option -> thm_tactic) =
99 fun l th (asl,_ as g) ->
101 None -> ASSUME_TAC th g
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;;
106 let (per: step -> step list list -> step) =
108 fun (_,(_,_,thl,just)) cases ->
109 (fun (_,_,thl',just') g ->
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
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));;
122 (fun _ -> failwith "cases"),default_stepinfo None;;
124 let (suppose': (goal -> term) -> step) =
125 fun t -> (fun _ -> failwith "suppose"),default_stepinfo (Some t);;
127 let (consider': (goal -> term) list -> step) =
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
135 None -> failwith "consider"
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')));;
144 let (take': (goal -> term) list -> step) =
146 (fun _ g -> (MAP_EVERY EXISTS_TAC o map (fun t -> t g)) tl g),
147 default_stepinfo None;;
149 let (assume': (goal -> term) -> step) =
151 (fun (t',l,thl,just) g ->
153 None -> failwith "assume"
156 (fun th -> REWRITE_TAC[th] THEN
158 (fun th -> just ((REWRITE_RULE[] th)::(thl g)))
159 (SPEC (t g) EXCLUDED_MIDDLE)) g),
160 default_stepinfo (Some t);;
162 let (have': (goal -> term) -> step) =
164 (fun (t',l,thl,just) g ->
166 None -> failwith "have"
168 (SUBGOAL_THEN (t g) (N_ASSUME_TAC l) THENL
169 [just (thl g); ALL_TAC]) g),
170 default_stepinfo (Some t);;
172 let (thus': (goal -> term) -> step) =
174 (fun (t',l,thl,just) g ->
176 None -> failwith "thus"
178 (SUBGOAL_THEN (t g) ASSUME_TAC THENL
181 N_ASSUME_TAC l th THEN
182 EVERY (map (fun th -> REWRITE_TAC[EQT_INTRO th])
185 default_stepinfo (Some t);;
187 let (fix': (goal -> term) list -> step) =
189 (fun _ g -> (MAP_EVERY X_GEN_TAC o (map (fun t -> t g))) tl g),
190 default_stepinfo None;;
192 let (set': (goal -> term) -> step) =
197 None -> failwith "set"
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];
208 default_stepinfo (Some t) in
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;;
221 let iff prfs = tactics [EQ_TAC THENL map steps prfs];;
223 let (otherwise: ('a -> step) -> ('a -> step)) =
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),
231 let (thesis:mterm) = "thesis";;
232 let (antecedent:mterm) = "antecedent";;
233 let (opposite:mterm) = "opposite";;
234 let (contradiction:mterm) = "F";;
236 let hence = so thus;;
237 let qed = hence thesis;;
239 let h = g o parse_term;;
243 let fp = f o (fun x -> x proof []);;
245 let GOAL_HERE = tactics [GOAL_TAC];;