(* ========================================================================= *)
(*                              Isabelle Light                               *)
(*   Isabelle/Procedural style additions and other user-friendly shortcuts.  *)
(*                                                                           *)
(*                   Petros Papapanagiotou, Jacques Fleuriot                 *)
(*              Center of Intelligent Systems and their Applications         *)
(*                          University of Edinburgh                          *)
(*                                 2009-2012                                 *)
(* ========================================================================= *)
(* FILE         : meta_rules.ml                                              *)
(* DESCRIPTION  : Meta rules is a formalisation used to accommodate          *)
(*                Isabelle's inference rules in HOL Light.The technical      *)
(*                details are described in the comments that follow.         *)
(*                Isabelle rule application tactics (rule, erule, etc.) have *)
(*                been defined to work with meta rules.                      *)
(*                We have not been able to accommodate first order rules     *)
(*                allI and exE. We also make use of metavariables which are  *)
(*                restricted by the limitations of term_unify                *)
(*                (ie. no HO unification and no type instantiation).         *)
(* LAST MODIFIED: October 2012                                               *)
(* ========================================================================= *)

(* ------------------------------------------------------------------------- *)
(* ----------------------- META-LEVEL IMPLICATION -------------------------- *)
(* ------------------------------------------------------------------------- *)
(* Emulation of meta-level implication at the object level.                  *)
(* This is purely for syntax and parsing purposes. It solves a number of     *)
(* problems when parsing theorems as meta-rules (see below).                 *)
(* It is applied at the logic level only for transparency.                   *)
(* ------------------------------------------------------------------------- *)
(* Thanks to Phil Scott for the suggestion.                                  *)
(* ------------------------------------------------------------------------- *)


(* ------------------------------------------------------------------------- *)
(* Syntax definition.                                                        *)
(* ------------------------------------------------------------------------- *)

parse_as_infix ("===>",(4,"right"));;

let is_mimp = is_binary "===>";;
let dest_mimp = dest_binary "===>";;


(* ------------------------------------------------------------------------- *)
(* Logic definition: Equivalent to object-level implication.                 *)
(* ------------------------------------------------------------------------- *)

let MIMP_DEF = new_basic_definition
  `(===>) = \p q. p ==> q`;;


(* ------------------------------------------------------------------------- *)
(* CONV, RULE and TACTIC to get rid of meta-level implication in proofs.     *)
(* ------------------------------------------------------------------------- *)

let MIMP_TO_IMP_CONV = BETA_RULE o (PURE_REWRITE_CONV [MIMP_DEF]);;
let MIMP_TO_IMP_RULE = BETA_RULE o (PURE_REWRITE_RULE [MIMP_DEF]);;
let MIMP_TAC = (PURE_REWRITE_TAC [MIMP_DEF]) THEN BETA_TAC;;


(* ------------------------------------------------------------------------- *)
(* Equivalent of TAUT after getting rid of meta-level implication.           *)
(* Helps prove simple propositional meta-rules easily.                       *)
(* ------------------------------------------------------------------------- *)

let MTAUT tm =
    let th = MIMP_TO_IMP_CONV tm in
    EQ_MP (SYM th) ((TAUT o snd o dest_iff o concl) th);;


(* ------------------------------------------------------------------------- *)
(* RULE to replace implication by meta-level implication to easily create    *) 
(* meta-theorems from normal theorems.                                       *)
(* ------------------------------------------------------------------------- *)

let MIMP_THM = MTAUT `(p==>q) <=> (p===>q)`;;
let MIMP_RULE = PURE_REWRITE_RULE[MIMP_THM];;


(* ------------------------------------------------------------------------- *)
(* UNDISCH for meta-level implication.                                       *)
(* Also gets rid of meta-level implication in the undischarged term.         *)
(* ------------------------------------------------------------------------- *)

let MUNDISCH th = 
    let mth = BETA_RULE (AP_THM (AP_THM MIMP_DEF `p:bool`) `q:bool`) in 
    let th =  PURE_ONCE_REWRITE_RULE [mth] th in
    try let undisch_tm = (rand o rator o concl) th in
    PROVE_HYP ((UNDISCH o snd o EQ_IMP_RULE o MIMP_TO_IMP_CONV) undisch_tm) (UNDISCH th)
    with Failure _ -> failwith "MUNDISCH";;


(* ------------------------------------------------------------------------- *)
(* -------------------------- HELPFUL FUNCTIONS ---------------------------- *)
(* ------------------------------------------------------------------------- *)

(* ------------------------------------------------------------------------- *)
(* REV_PART_MATCH_I: term list -> (term -> term) -> thm -> term              *)
(*                                                         -> instantiation  *)
(* Does a reverse PART_MATCH and returns the resulting instantiation.        *)
(* Avoids instantiating any of the given variables/constants.                *)
(* Does not apply SPEC_ALL like PART_MATCH does.                             *)
(* ------------------------------------------------------------------------- *)
(* The original PART_MATCH matches a term to part of a theorem so that we can*)
(* instantiate that part with the term.                                      *)
(* The reverse used here, matches the part of the theorem with the term so   *)
(* that the term can be instantiated with the part of the theorem.           *)
(* We use this in cases such as erule where we want (part of) an assumption  *)
(* to match a premise of the rule. We need the instantiation of the rule when*)
(* matched to the assumption (thm) and not the other way around.             *)
(* ------------------------------------------------------------------------- *)

let REV_PART_MATCH_I =
  let rec match_bvs t1 t2 acc =
    try let v1,b1 = dest_abs t1
        and v2,b2 = dest_abs t2 in
        let n1 = fst(dest_var v1) and n2 = fst(dest_var v2) in
        let newacc = if n1 = n2 then acc else insert (n1,n2) acc in
        match_bvs b1 b2 newacc
    with Failure _ -> try
        let l1,r1 = dest_comb t1
        and l2,r2 = dest_comb t2 in
        match_bvs l1 l2 (match_bvs r1 r2 acc)
    with Failure _ -> acc in
  fun avoids partfn th ->
    let bod = concl th in
    let pbod = partfn bod in
    let lconsts = union avoids (intersect (frees (concl th)) (freesl(hyp th))) in
    fun tm ->
      let bvms = match_bvs pbod tm [] in
      let atm = deep_alpha bvms tm in
      term_match lconsts atm (partfn bod) ;; (* whereas in PART_MATCH we do it the other way around *)


(* ------------------------------------------------------------------------- *)
(* term_to_asm_match : term list -> term -> (string * thm) list ->           *)
(*                               (string * thm) list * (thm * instantiation) *)
(* ------------------------------------------------------------------------- *)
(* term_to_asm_match tries to match key to one of the assumptions using      *)
(* REV_PART_MATCH_I. Returns the new assumption list (with the matching      *)
(* assumption removed), the matching assumption and the resulting            *)
(* instantiation used.                                                       *)
(* ------------------------------------------------------------------------- *)
(* It is doubtful that this has practical use outside the Xrule_tac's.       *)
(* It is used in erule, drule and frule to match the major premise to one of *)
(* the assumptions.                                                          *)
(* ------------------------------------------------------------------------- *)

let rec (term_to_asm_match: term list -> term -> (string * thm) list -> (string * thm) list * (thm * instantiation)) =
  fun avoids key asms ->
    if (asms = []) then failwith ("No assumptions match `" ^ (string_of_term key) ^ "`!")
    else try 
      let asm = (snd o hd) asms in
      let i = REV_PART_MATCH_I avoids I asm key in
      (tl asms),(asm,i)
    with Failure _ -> let res,inst = term_to_asm_match avoids key (tl asms) in ((hd asms)::res),inst;;


(* ------------------------------------------------------------------------- *)
(* term_to_asm_n_match : term list -> term -> (string * thm) list -> int ->  *)
(*                               (string * thm) list * (thm * instantiation) *)
(* ------------------------------------------------------------------------- *)
(* Same as term_to_asm_match but only tries to match nth assumption.         *)
(* ------------------------------------------------------------------------- *)
(* It is doubtful that this has practical use outside the Xrulen_tac's.      *)
(* It is used in erulen, drulen and frulen to match the major premise to one *)
(* of the assumptions.                                                       *)
(* ------------------------------------------------------------------------- *)

let rec (term_to_asm_n_match: term list -> term -> (string * thm) list -> int -> (string * thm) list * (thm * instantiation)) =
  fun avoids key asms n ->
    if (asms = []) then failwith "No such assumption found!"
    else try match n with
	0 ->  
	  let asm = (snd o hd) asms in
	  let i = REV_PART_MATCH_I avoids I asm key in
	    (tl asms),(asm,i)
      | _ -> let re_asms,m = term_to_asm_n_match avoids key (tl asms) (n-1) in
	  (hd asms)::re_asms,m
    with Failure _ -> failwith ("Assumption `" ^ ((string_of_term o concl o snd o hd) asms) ^ "` doesn't match `" ^ (string_of_term key) ^ "`!");;



(* gmm is not to be used until qed is updated *)
(* We need a MDISCH for that...               *)

let gmm t =
  let fvs = sort (<) (map (fst o dest_var) (frees t)) in
  (if fvs <> [] then
     let errmsg = end_itlist (fun s t -> s^", "^t) fvs in
     warn true ("Free variables in goal: "^errmsg)
   else ());
  let rec split_mimp = fun tm ->
    if (is_mimp tm) 
    then 
      let (a,b) = dest_mimp tm in
      let (asms, concl) = split_mimp b in
      (a::asms,concl)
    else ([],tm) in
   set_goal (split_mimp t);;


(* ------------------------------------------------------------------------- *)
(* gm : term -> goalstack                                                    *)
(* This is used to set a term containing meta-level implication as a goal.   *)
(* ------------------------------------------------------------------------- *)
(* (+) Uses g to set the goal then MIMP_TAC to get rid of meta-implication.  *)
(* (+) Note that if the goal has normal implication it gets discharged as    *)
(* well. This will be fixed when gmm is fixed.                               *)
(* ------------------------------------------------------------------------- *)

let gm t = g t ; e (MIMP_TAC THEN REPEAT DISCH_TAC);;


(* ------------------------------------------------------------------------- *)
(* Isabelle's natural deduction rules as thms with meta-level implication.   *)
(* ------------------------------------------------------------------------- *)

let conjI = MTAUT `p===>q===>p/\q`;;
let conjunct1 = MTAUT `p/\q===>p`;;
let conjunct2 = MTAUT `p/\q===>q`;;
let conjE = MTAUT `p/\q===>(p===>q===>r)===>r`;; 
let disjI1 = MTAUT `p===>p\/q`;;
let disjI2 = MTAUT `q===>p\/q`;;
let disjE = MTAUT `p\/q===>(p===>r)===>(q===>r)===>r`;;

let impI = MTAUT `(p===>q)===>(p==>q)`;;
let impE = MTAUT `(p==>q)===>p===>(q===>r)===>r`;;
let mp = MTAUT `(p==>q)===>(p===>q)`;;

let iffI = MTAUT `(a===>b)===>(b===>a)===>(a<=>b)`;;
let iffE = MTAUT `(a<=>b)===>((a==>b) ===> (b==>a) ===> r) ===> r`;;

let allE = 
prove( `(!x:A. P x) ===> (P (a:A) ===> (r:bool)) ===> r` ,

                  MIMP_TAC THEN MESON_TAC[]);;
let exI = 
prove (`P (a:A)===> ?x:A. P x`,
 
                          MIMP_TAC THEN
			  DISCH_TAC THEN 
			    (EXISTS_TAC `a:A`) THEN 
			    (FIRST_ASSUM ACCEPT_TAC));;
let notI = MTAUT `(p===>F)===> ~p`;;
let notE = MTAUT `~a ===> a ===> r`;;


(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* ------------------------ META-RULES START HERE!! ------------------------ *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)

(* ------------------------------------------------------------------------- *)
(* meta_rule (type)                                                          *)
(* The representation of an Isabelle inference rule in HOL Light.            *)
(* ------------------------------------------------------------------------- *)
(* term = The conclusion of the inference rule.                              *)
(* goal list = The premises represented as "meta-subgoals".                  *)
(* thm = The representation of the rule as a theorem used for justification. *)
(*                                                                           *)
(* (+) thm must be of the form H1,H2,...,Hn |- G                             *)
(* (+) H1--Hn must be represented as "meta-subgoals" in any order (1)        *)
(* (+) [|P;Q|] ==> R (in Isabelle notation) is translated as "meta-subgoal"  *)
(*     P,Q ?- R and as P==>Q==>R in the justification theorem.               *)
(* (+) The form of the premises (assumption order etc) must be kept in the   *)
(*     justification theorem (see example in (2))                            *)
(* (+) Use "mk_meta_rule" to create proper meta rules from theorems.         *)
(* ------------------------------------------------------------------------- *)
(* (1) Since we use PROVE_HYP instead of MP to justify rule, erule etc, the  *)
(* order of the subgoals is no longer essential.                             *)
(* (2) Example: conjE                                                        *)
(* In Isabelle:     P/\Q  [|P;Q|]==> R                                       *)
(*                  ------------------                                       *)
(*                          R                                                *)
(*                                                                           *)
(* As a meta rule (briefly - see conjEm below for full notation):            *)
(*              `R`,                           - conclusion                  *)
(*              [                              - premises list               *)
(*                [       ], `P/\Q`  ;                                       *)
(*                [`P`;`Q`], `R`                                             *)
(*              ],                                                           *)
(*              `P/\Q, P==>Q==>R |- R`         - justification theorem       *)
(*                                                                           *)
(* The form of the premises must be preserved in the justification theorem.  *)
(* ie. using `P/\Q, Q==>P==>R |- R` or `Q/\P, P==>Q==>R |- R` as a           *)
(* justification theorem would break the justification and result in an      *)
(* "invalid tactic" exception.                                               *)
(* ------------------------------------------------------------------------- *)

type meta_rule = term * goal list * thm;;


let print_meta_rule: meta_rule->unit = 
  fun (c,glist,j) ->
    print_term c ; hd (map (print_newline () ; print_goal) glist) ;
    print_newline () ; print_thm j ; print_newline ();;


(* ------------------------------------------------------------------------- *)
(* inst_meta_rule: instantiation -> meta_rule -> meta_rule                   *)
(* ------------------------------------------------------------------------- *)
(* Instantiates all parts of meta_rules based on an instantiation.           *)
(* ------------------------------------------------------------------------- *)

let inst_meta_rule:instantiation->meta_rule->meta_rule =
  fun inst (c,glist,j) ->
    instantiate inst c,
    map (inst_goal inst) glist,
    INSTANTIATE_ALL inst j;;


(* ------------------------------------------------------------------------- *)
(* meta_rule_frees: meta_rule -> term list                                   *)
(* ------------------------------------------------------------------------- *)
(* Returns the list of free variables (or Isabelle ?metavariables) in a      *)
(* meta_rule.                                                                *)
(* ------------------------------------------------------------------------- *)

let meta_rule_frees: meta_rule -> term list =
  fun (c,glist,l) ->
    itlist (union o gl_frees) glist (union (frees c) (thm_frees l));;


(* ------------------------------------------------------------------------- *)
(* meta_rule_mk_primed_vars_I: term_list -> meta_rule ->                     *)
(*                                            meta_rule * instantiation      *)
(* ------------------------------------------------------------------------- *)
(* Applies mk_primed_var to all the free variables in a meta_rule.           *)
(* Returns the new meta_rule and the instantiation for the variable renaming.*)
(* ------------------------------------------------------------------------- *)

let meta_rule_mk_primed_vars_I: term list -> meta_rule -> meta_rule * instantiation = 
  fun avoids r ->
    let fvars =  meta_rule_frees r in
    let rec mk_primed_l = fun avoids vars ->
      match vars with 
	[] -> null_inst
      | v::rest -> 
	  let new_v = mk_primed_var avoids v in
	  compose_insts (term_match [] v new_v) (mk_primed_l (new_v::avoids) rest)
    in
    let inst = mk_primed_l avoids fvars in
    (inst_meta_rule inst r),inst;;


(* ------------------------------------------------------------------------- *)
(* meta_rule_mk_primed_vars: term_list -> meta_rule -> meta_rule             *)
(* ------------------------------------------------------------------------- *)
(* Applies mk_primed_var to all the free variables in a meta_rule.           *)
(* ------------------------------------------------------------------------- *)

let meta_rule_mk_primed_vars: term list -> meta_rule -> meta_rule = 
  fun avoids r -> fst (meta_rule_mk_primed_vars_I avoids r);;



(* ------------------------------------------------------------------------- *)
(* inst_meta_rule_vars:                                                      *)
(*                 (term * term) list -> meta_rule -> term list -> meta_rule *)
(* ------------------------------------------------------------------------- *)
(* Instantiates the free variables in a meta_rule. Also renames the          *)
(* uninstantiated variables so as to avoid clashes with free variables and   *)
(* constants in the given goal.                                              *)
(* Essentially it prepares the meta_rule for use with any of xrulem_tac.     *)
(* ------------------------------------------------------------------------- *)
(* (+) By instlist we mean the list of variables and instantiation pairs     *)
(* given by the user.                                                        *)
(* (+) First we check the terms given as variables in the instlist. We must  *)
(* check if they are indeed variables and if they are free variables in the  *)
(* given meta_rule.                                                          *)
(* (+) "match_var" is used to compare a variable with a free variable in the *)
(*  meta_rule. *NOTE* that a variable is accepted as long as it can match a  *)
(* free variable in the meta_rule allowing only type instantiation.          *)
(* (+) "mcheck_var" does the is_var check and tries to find a match with the *)
(* meta_rule's free vars (rfrees) using match_var.                           *)
(* (+) "mcheck_gvar" tries to match variables on the rhs of each instlist    *)
(* pair with the free variables in the goal so as to instantiate their types *)
(* properly. This is done to free the user from declaring the variable types.*)
(* (+) Given variables are replaced with the meta_rule variables (effectively*)
(* achieving type instantiation) and later recombined into the instlist.     *)
(* (+) Secondly, we rename all the variables in the meta_rule using          *)
(* "meta_rule_mk_primed_vars_I" so that they don't match any of the free     *)
(* variables in the goal.                                                    *)
(* (+) We use the same instantiation to rename instlist variables so that    *)
(* they properly match the new variables of the meta_rule.                   *)
(* (+) "new_instlist" should contain variables that fully match primed       *)
(* variables in the meta_rule (new_r).                                       *)
(* (+) For each instlist pair, we find the instantiation that allows the     *)
(* variable to be substituted by the given term. *NOTE* that no check is     *)
(* made on that term. It is the user's responsibility to give a sensible,    *)
(* matching and correctly typed term.                                        *)
(* (+) All the instantiations produced by the instlist are composed into one *)
(* which is then applied to new_r to give the result.                        *)
(* ------------------------------------------------------------------------- *)


let inst_meta_rule_vars: (term * term) list -> meta_rule -> term list -> meta_rule =
  fun instlist r gfrees ->
    let rfrees = meta_rule_frees r in
    let vars,subs = List.split instlist in
    
    let match_var = fun tm1 tm2 ->
      let inst = try term_match [] tm1 tm2 with Failure _ -> [],[tm2,tm1],[] in
      match inst with
	[],[],_ -> tm2
      | _  -> failwith "match_var: no match" in
    
    let mcheck_var = fun tm ->
      if (not (is_var tm)) then failwith ("inst_meta_rule_vars: `" ^ string_of_term tm ^ "` is not a variable")
      else try list_match_first (match_var tm) rfrees 
      with Failure _ -> failwith ("inst_meta_rule_vars: `" ^ string_of_term tm ^ "` could not be found in the meta_rule") in

    let mcheck_gvar = fun var ->
      try let mvar = list_match_first (match_var var) gfrees in
      term_match [] var mvar
      with Failure _ ->  
	warn true ("inst_meta_rule_vars: `" ^ string_of_term var ^ "` could not be found in the goal") ;
	null_inst in 

    let new_r,prim_inst = meta_rule_mk_primed_vars_I gfrees r in
    let new_vars = map ((instantiate prim_inst) o mcheck_var) vars in

    let subs_vars = flat (map frees subs) in
    let new_subs_inst = itlist compose_insts (map mcheck_gvar subs_vars) null_inst in
    let new_subs = map (instantiate new_subs_inst) subs in

    let new_instlist = List.combine new_vars new_subs in
    let mk_inst = fun t1,t2 -> term_match [] t1 t2 in
    let inst = itlist compose_insts (map mk_inst new_instlist) null_inst in
    let result_r = inst_meta_rule inst new_r in
    result_r;;



(* ------------------------------------------------------------------------- *)
(* mk_meta_rule: thm -> meta_rule                                            *)
(* Creates a meta_rule out of a theorem.                                     *)
(* Theorem must be of the form |- H1 ===> H2 ===> ...===> Hn ===> C          *)
(* "===>" is the emulation of meta-level implication so this corresponds to  *)
(* [|H1;H2;...;Hn|] ==> C in Isabelle)                                       *)
(* For each Hi that is a meta-level implication, a "meta_subgoal" is created.*)
(* ------------------------------------------------------------------------- *)
(* (+) undisch_premises uses MUNDISCH to handle meta-level implication. All  *)
(* the premises are undischarged. It returns the list of premises paired     *)
(* with the resulting theorem. Note that MUNDISCH also removes meta-level    *)
(* implication from the undischarged premises.                               *)
(* (+) "mk_meta_subgoal" creates a meta_subgoal from a term. If the term is  *)
(* an implication, the lhs is added as an assumption/premise of the          *)
(* meta_subgoal and mk_meta_subgoal is called recursively for the rhs.       *)
(* (+) The conclusion of the undischarged theorem is the first part of the   *)
(* produced meta_rule.                                                       *)
(* (+) mk_meta_subgoal creates the meta_subgoals for all the premises. They  *)
(* form the second part of the meta_rule.                                    *)
(* (+) The theorem itself is used as the justification theorem, after        *)
(* eliminating any remaining meta-level implication in the conclusion.       *)
(* In theory, the conclusion should never have any remaining meta-level      *)
(* implications. We're just making sure because we don't want any meta-level *)
(* implications to appear in our new subgoals.                               *)
(* ------------------------------------------------------------------------- *)

let (mk_meta_rule: thm -> meta_rule) =
  fun thm ->
    let rec undisch_premises th =
        if is_mimp (concl th) 
        then let rest,res_th = undisch_premises (MUNDISCH th) in
             (rand(rator(concl th)))::rest,res_th
        else [],th in
    let (prems,thm) = undisch_premises thm in
    let rec mk_meta_subgoal tm = (
      if (is_mimp(tm)) then 
	let (a,c) = dest_mimp tm in
	let (prems,concl) = mk_meta_subgoal c in
	("",ASSUME a)::prems,concl
     else [],tm
     ) in
    concl thm,map mk_meta_subgoal prems,MIMP_TO_IMP_RULE thm;;
    

(* ------------------------------------------------------------------------- *)
(* mk_meta_rule_old: thm -> meta_rule                                        *)
(* Creates a meta_rule out of a theorem. === DEPRECATED ===                  *)
(* Theorem must be of the form H1,H2,...,Hn |- C                             *)
(* If Hi is of the form Hi1==>Hi2==>...==>Hik==>HiC then it is treated as    *)
(* Hi1,Hi2,...,Hik ?- HiC (or "meta-level" implication                       *)
(* [|Hi1;Hi2;...;Hik|] ==> HiC in Isabelle) and the corresponding            *)
(* meta_subgoal is created.                                                  *)
(* ------------------------------------------------------------------------- *)
(* --As a result you CANNOT have rules with implication in their premises!-- *)
(*  (You'll have to use mk_elim_meta_rule or build the meta_rule yourself.)  *)
(* ------------------------------------------------------------------------- *)
(* (+) The theorem is destroyed to its hypothesis list and its conclusion.   *)
(* The conclusion is the first part of the meta_rule.                        *)
(* (+) "mk_meta_subgoal" creates a meta_subgoal from a term. If the term is  *)
(* an implication, the lhs is added as an assumption/premise of the          *)
(* meta_subgoal and mk_meta_subgoal is called recursively for the rhs.       *)
(* (+) The theorem itself is used as the justification theorem.              *)
(* ------------------------------------------------------------------------- *)
(* Deprecated. New mk_meta_rule uses meta-level implication.                 *)
(* Kept until new mk_meta_rule is tested and stable.                         *)
(* ------------------------------------------------------------------------- *)

let (mk_meta_rule_old: thm -> meta_rule) =
  fun thm ->
    let (hyps,concl) = dest_thm thm in
    let rec mk_meta_subgoal tm = (
      if (is_imp(tm)) then 
	let (a,c) = dest_imp tm in
	let (prems,concl) = mk_meta_subgoal c in
	("",ASSUME a)::prems,concl
     else [],tm
     ) in
    concl,map mk_meta_subgoal hyps,thm;;



(* ------------------------------------------------------------------------- *)
(* mk_elim_meta_rule_old: thm -> meta_rule                                   *)
(* Creates a meta_rule out of a theorem. === DEPRECATED ===                  *)
(* Works like mk_meta_rule but acommodates elimination/destruction rules     *)
(* a little bit better by not breaking the major premise. This effectively   *)
(* allows the major premise to be an implication.                            *)
(* ------------------------------------------------------------------------- *)
(* In an elimination or destruction rule, the first or major premise is      *)
(* matched against one of the assumptions. Therefore, you cannot have a      *)
(* meta_subgoal for a major premise. If there is an implication there we     *)
(* shall leave it intact and not treat it as "meta-level" implication.       *)
(* This still disallows the use of implication in the rest of the premises   *)
(* (by treating it as "meta-level" implication).                             *)
(* ------------------------------------------------------------------------- *)
(* Deprecated. New mk_meta_rule uses meta-level implication.                 *)
(* Kept until new mk_meta_rule is tested and stable.                         *)
(* ------------------------------------------------------------------------- *)

let (mk_elim_meta_rule_old: thm -> meta_rule) =
  fun thm ->
    let (hyps,concl) = dest_thm thm in
    if (hyps = []) then failwith "mk_elim_meta_rule: Invalid rule - no premises!"
	else let major_prem,hyps = ([],hd hyps),tl hyps in
    let rec mk_meta_subgoal tm = (
      if (is_imp(tm)) then 
	let (a,c) = dest_imp tm in
	let (prems,concl) = mk_meta_subgoal c in
	("",ASSUME a)::prems,concl
     else [],tm
     ) in
    concl,major_prem :: (map mk_meta_subgoal hyps),thm;;



(* ------------------------------------------------------------------------- *)
(* Isabelle's natural deduction inference rules as meta_rules.               *)
(* ------------------------------------------------------------------------- *)
(* The trailing 'm' indicates they are represented as meta_rules as opposed  *)
(* to theorems.                                                              *)
(* Use "mk_meta_rule" to create meta_rules from theorems.                    *)
(* Most of the following can be created using mk_meta_rule but are left here *)
(* as examples.                                                              *)
(* ------------------------------------------------------------------------- *)
(* Deprecated. New mk_meta_rule uses meta-level implication so now ALL of    *)
(* these can be represented at the object-level and turned into meta_rules   *)
(* using mk_meta_rule.                                                       *)
(* ------------------------------------------------------------------------- *)

let conjIm:meta_rule =
  (`p/\q`,
   [
   [],`p:bool`;
   [],`q:bool`
  ],
   conjI);;

let conjEm:meta_rule =
  (`r:bool`,
   [
   [],`p/\q`;
   [("",ASSUME `p:bool`);("",ASSUME `q:bool`)],`r:bool`
  ],
  (UNDISCH o UNDISCH o TAUT) `p/\q==>(p==>q==>r)==>r`
);;

let notEm:meta_rule =
  (`r:bool`,
   [
   [],`~a`;
   [],`a:bool`
  ],
  (UNDISCH o UNDISCH o TAUT) `~a==>a==>r`
);;

let disjI1m:meta_rule =
  (`p\/q`,
   [
   [],`p:bool`;
  ],
   UNDISCH ( TAUT `p==>p\/q` ));;

let disjI2m:meta_rule =
  (`p\/q`,
   [
   [],`q:bool`;
  ],
   UNDISCH ( TAUT `q==>p\/q` ));;

let disjEm:meta_rule =
  (`r:bool`,
   [
   [],`p\/q`;
   [("",ASSUME `p:bool`)],`r:bool`;
   [("",ASSUME `q:bool`)],`r:bool`
  ],
   (UNDISCH o UNDISCH o UNDISCH) ( TAUT `p\/q==>(p==>r)==>(q==>r)==>r`)
  );;


let impIm:meta_rule =
  (`p==>q`,
   [
   [("",ASSUME `p:bool`)],`q:bool`
  ],
   UNDISCH (TAUT `(p==>q)==>(p==>q)`)
);;


let impEm:meta_rule =
  (`r:bool`,
   [
    [],`p==>q`;
    [],`p:bool`;
    [("",ASSUME `q:bool`)],`r:bool`
  ],
   (UNDISCH o UNDISCH o UNDISCH o TAUT) `(p==>q)==>p==>(q==>r)==>r`
);;


let mpm:meta_rule =
  (`q:bool`,
   [
    [],`p==>q`;
    [],`p:bool`
  ],
   (UNDISCH o UNDISCH o TAUT) `(p==>q)==>(p==>q)`
);;

(* Note from old mk_meta_rule:                                               *)
(* This one cannot be expressed as a theorem because HOL Light insists on    *)
(* ordering the assumptions of the theorem so the major premise is `p`       *)
(* instead of `~p`.                                                          *)

let notEm:meta_rule =
  (`r:bool`,
   [
   [],`~a`;
   [],`a:bool`
  ],
  (UNDISCH o UNDISCH o TAUT) `~a==>a==>r`
);;
  

(* ------------------------------------------------------------------------- *)
(* rulem_tac: ((term * term) list -> meta_rule -> tactic):                   *)
(* Isabelle's rule as a HOL Light meta_rule tactic.                          *)
(* Uses a rule of the form  H1,H2,...,Hn |- C represented as a meta_rule     *)
(* to solve A1,A2,...,Am ?- G                                                *)
(* Matches C to the goal G, then splits the goal to                          *)
(*          A1,A2,...,Am ?- H1                                               *)
(*          A1,A2,...,Am ?- H2                                               *)
(*          ...                                                              *)
(*          A1,A2,...,Am ?- Hn                                               *)
(* Hi can be of the form Hi1,Hi2,...,Hik ?- HiC then the goal produced is    *)
(*          A1,A2,...,Am,Hi1,Hi2,...,Hik ?- HiC                              *)
(* ------------------------------------------------------------------------- *)
(* (+) "avoids" lists all the free variables in the assumptions and goal so  *)
(* as to avoid instantiating those (as in variable conflicts with the rule   *)
(* or partly instantiated rule in the case of erule)                         *)
(* (+) First we check if C matches G. If it does we keep the resulting       *)
(* instantiation (ins).                                                      *)
(* (+) We instantiate the "meta-subgoals" of the meta_rule using ins.        *)
(* In essence we're instantiating the premises of the rule. (new_hyps)       *)
(* (+) The "create_goal" function creates the new goals by adding the        *)
(* assumption list A1--Am to the instantiated "meta-subgoal".                *)
(* (+) create_goal is mapped on new_hyps to create the new subgoal list.     *)
(* (+) The "create_dischl" function creates the list of the terms involved   *)
(* in the premises of each instantiated meta-subgoal. In order to create the *)
(* justification of the tactic, we need to convert Hi1,Hi2,...,Hik |- HiC    *)
(* into |- Hi1==>Hi2==>...==>Hik==>HiC. That is the only way we can capture  *)
(* the notion of a "subgoal" within a HOL Light object-level theorem.        *)
(* We will then use PROVE_HYP to eliminate each of the proven subgoals from  *)
(* the rule's justification theorem. In order to achieve this conversion we  *)
(* need to keep a list of the instantiated premises of the rule (dischls)    *)
(* for each meta_subgoal so as to avoid discharging the original goal's      *)
(* assumptions or _FALSITY_.                                                 *)
(* (+) "disch_pair" is used for convenience. dishls is combined with the     *)
(* list of proven subgoals so that each subgoal is attached to its           *)
(* corresponding premises list (dischl). disch_pair then does the discharges.*)
(* It also takes care of instantiating the meta-variables in those premises  *)
(* for proper justification.                                                 *)
(* (+) normalfrees is used to calculate the list of metavariables that will  *)
(* end up in the new subgoals. It contains all the free variables in the     *)
(* goal and instlist.                                                        *)
(* (+) The newly introduced metavariables are found by subtracting           *)
(* normalfrees from the set of all free variables in all new goals.          *)
(* ------------------------------------------------------------------------- *)

let (rulem_tac: (term*term) list->meta_rule->tactic) =
  fun instlist r ((asl,w) as g) ->
    let (c,hyps,thm) = inst_meta_rule_vars instlist r (gl_frees g) in

    let ins = try ( term_match [] c w ) with Failure _ -> failwith "Rule doesn't match!" in

    let new_hyps = map (inst_goal ins) hyps in
    let create_goal = fun asms (hs,gl) -> (hs@asms,gl) in
    let new_goals = map (create_goal asl) new_hyps in
    let rec create_dischl = fun (asms,g) -> if (asms = []) then [] else ((concl o snd o hd) asms)::(create_dischl ((tl asms),g)) in
    let dischls = map create_dischl new_hyps in
    let disch_pair = fun i (dischl,thm) -> DISCHL (map (instantiate i) dischl) thm in
    let normalfrees = itlist union (map ( fun (_,y) -> frees y ) instlist ) (gl_frees g) in
    let mvs = subtract (itlist union (map gl_frees new_goals) []) normalfrees in
    (mvs,null_inst),new_goals,fun i l ->  
      List.fold_left (fun t1 t2 -> PROVE_HYP (INSTANTIATE_ALL i t2) t1) (INSTANTIATE_ALL (compose_insts ins i) thm) (map (disch_pair i) (List.combine dischls l));;


(* ------------------------------------------------------------------------- *)
(* erulem_tac: ((term * term) list -> meta_rule -> tactic):                  *)
(* Isabelle's erule as a HOL Light meta_rule tactic.                         *)
(* Works like rulem but also matches the first hypothesis H1 with one of the *)
(* assumptions A1--Am and instantiates accordingly.                          *)
(* A "proper" elimination rule H1 is of the form ?- H1 (ie. has no premises) *)
(* ------------------------------------------------------------------------- *)
(* Same as rulem with some added stuff.                                      *)
(* (+) If there are no "meta_subgoals" (no new subgoals to create) we fail.  *)
(* (+) Otherwise we use the first "meta_subgoal" as our primary hypothesis   *)
(* (the one that will be eliminated - prim_hyp).                             *)
(* (+) If prim_hyp has premises then this is not a "proper" elimination rule.*)
(* (+) Otherwise try to match any of the assumptions with prim_hyp. The      *)
(* resulting instantiation is elim_inst.                                     *)
(* (+) Instantiate all generated meta_subgoals with elim_inst. Retrieve the  *)
(* (now instantiated) prim_hyp and remove it from the new subgoals (it is    *)
(* trivially proven). We get a "pattern-matching is not exhaustive" warning  *)
(* here, but we have already checked that new_hyps is non-empty.             *)
(* (+) prim_thm is a trivial theorem that proves the subgoal corresponding   *)
(* to prim_hyp.                                                              *)
(* (+) Instantiate the justification theorem with elim_thm.                  *)
(* (+) Add prim_hyp to the justification (pretending its a proven subgoal).  *)
(* (+) Use a hack to add the eliminated assumption to the proven subgoals so *)
(* that we pass the validity check properly.                                 *)
(* ------------------------------------------------------------------------- *)

let (erulem_tac: (term * term) list -> meta_rule->tactic) =
  fun instlist r ((asl,w) as g) ->
    let (c,hyps,thm) = inst_meta_rule_vars instlist r (gl_frees g) in

    let ins = try ( term_match [] c w ) 
    with Failure _ -> failwith "Rule doesn't match!" in
    let new_hyps = map (inst_goal ins) hyps in

    let (prems,prim_hyp) = 
      if (new_hyps = []) then failwith "erule: Not a proper elimination rule: no premises!" 
      else hd new_hyps in
    let avoids = gl_frees g in

    let asl,(prim_thm,elim_inst) = 
      if (prems = []) 
      then try term_to_asm_match avoids prim_hyp asl with Failure s -> failwith ("erule: " ^ s) 
      else failwith "erule: Not a proper elimination rule: major premise has assumptions!" in
    let (_,prim_hyp)::new_hyps = map (inst_goal elim_inst) new_hyps in
    let thm = INSTANTIATE_ALL elim_inst thm in
    
    let create_goal = fun asms (hs,gl) -> (hs@asms,gl) in
    let new_goals = map (create_goal asl) new_hyps in
    let rec create_dischl = 
      fun (asms,g) -> 
	if (asms = []) then [] 
	else ((concl o snd o hd) asms)::(create_dischl ((tl asms),g)) in
    let dischls = map create_dischl new_hyps in
    let disch_pair = fun i (dischl,thm) -> DISCHL (map (instantiate i) dischl) thm in

    let normalfrees = itlist union (map ( fun (_,y) -> frees y ) instlist ) (gl_frees g) in
    let mvs = subtract (itlist union (map gl_frees new_goals) []) normalfrees in
    (mvs,null_inst),new_goals,fun i l ->  
      let major_thmi = INSTANTIATE_ALL i prim_thm in
      List.fold_left (fun t1 t2 -> PROVE_HYP (INSTANTIATE_ALL i t2) t1) (INSTANTIATE_ALL (compose_insts ins i) thm) 
	(major_thmi :: map (ADD_HYP major_thmi) (map (disch_pair i) (List.combine dischls l)));;


(* ------------------------------------------------------------------------- *)
(* drulem_tac: ((term * term) list -> meta_rule -> tactic):                  *)
(* Isabelle's drule as a HOL Light meta_rule tactic.                         *)
(* Uses rules as shown in "rule".                                            *)
(* Matches the first hypothesis H1 with one of the                           *)
(* assumptions A1--Am and instantiates accordingly.                          *)
(* The assumption is removed from the list and the trivial goal is proven    *)
(* automatically.                                                            *)
(* A "proper" destructio rule H1 is of the form ?- H1 (ie. has no premises)  *)
(* The goal A1,A2,...,Am,G ?- C is also added.                               *)     
(* ------------------------------------------------------------------------- *)
(* Same as erulem with a few differences.                                    *)
(* [+] Does not try to match the goal c.                                     *)
(* [+] Adds an extra goal c ?- w after instantiating c.                      *)
(* [+] The new goal is treated slightly different in the justification.      *)
(* It is the one whose premises must be proven so as to get to the final     *)
(* goal. So it gets proven using PROVE_HYP by the result of the              *)
(* justification on the original rule.                                       *) 
(* ------------------------------------------------------------------------- *)

let (drulem_tac: (term * term) list -> meta_rule->tactic) =
  fun instlist r ((asl,w) as g) ->
    let (c,hyps,thm) = inst_meta_rule_vars instlist r (gl_frees g) in

    let (prems,major_prem) = 
      if (hyps = []) then failwith "drule: Not a proper destruction rule: no premises!" 
      else hd hyps in
    let avoids = gl_frees g in

    let asl,(major_thm,elim_inst) = 
      if (prems = [])
      then try term_to_asm_match avoids major_prem asl with Failure s -> failwith ("drule: " ^ s) 
      else failwith "drule: not a proper destruction rule: major premise has assumptions!" in
    let (_,major_asm)::new_hyps = map (inst_goal elim_inst) hyps in
    let thm = INSTANTIATE_ALL elim_inst thm in
    let create_goal = fun asms (hs,gl) -> (hs@asms,gl) in
    let new_goals = (map (create_goal asl) new_hyps) @ [create_goal asl (["",ASSUME (instantiate elim_inst c)],w)] in

    let rec create_dischl = 
      fun (asms,g) -> 
	if (asms = []) then [] 
	else ((concl o snd o hd) asms)::(create_dischl ((tl asms),g)) in
    (* We add an empty discharge list at the end for the extra goal. *)
    let dischls = map create_dischl new_hyps @ [[]] in
    let disch_pair = fun i (dischl,thm) -> DISCHL (map (instantiate i) dischl) thm in

    let normalfrees = itlist union (map ( fun (_,y) -> frees y ) instlist ) (gl_frees g) in
    let mvs = subtract (itlist union (map gl_frees new_goals) []) normalfrees in
    (mvs,null_inst),new_goals,fun i l ->  
      let major_thmi = INSTANTIATE_ALL i major_thm in
      let l = (major_thmi :: map (ADD_HYP major_thmi) (map (disch_pair i) (List.combine dischls l))) in
      PROVE_HYP (List.fold_left (fun t1 t2 -> PROVE_HYP (INSTANTIATE_ALL i t2) t1) (INSTANTIATE_ALL i thm) ((butlast) l)) (last l);;


(* ------------------------------------------------------------------------- *)
(* frulem_tac: ((term * term) list -> meta_rule -> tactic):                  *)
(* Isabelle's frule as a HOL Light meta_rule tactic.                         *)
(* Same as drule, but does not remove the matching assumption from the list. *)
(* ------------------------------------------------------------------------- *)
(* Same as drulem only skipping the parts that eat up the assumption and     *)
(* re-add it to the proven subgoals.                                         *)
(* ------------------------------------------------------------------------- *)

let (frulem_tac: (term * term) list -> meta_rule->tactic) =
  fun instlist r ((asl,w) as g) ->
    let (c,hyps,thm) = inst_meta_rule_vars instlist r (gl_frees g) in

    let (prems,major_prem) = 
      if (hyps = []) then failwith "frule: Not a proper destruction rule: no premises!" 
      else hd hyps in
    let avoids = gl_frees g in

    let _,(major_thm,elim_inst) = 
      if (prems = []) 
      then try term_to_asm_match avoids major_prem asl with Failure s -> failwith ("frule: " ^ s) 
      else failwith "frule: Not a proper destruction rule: major premise has assumptions!" in
    let (_,major_asm)::new_hyps = map (inst_goal elim_inst) hyps in
    let thm = INSTANTIATE_ALL elim_inst thm in
    let create_goal = fun asms (hs,gl) -> (hs@asms,gl) in
    let new_goals = (map (create_goal asl) new_hyps) @ [create_goal asl (["",ASSUME (instantiate elim_inst c)],w)] in

    let rec create_dischl = 
      fun (asms,g) -> 
	if (asms = []) then [] 
	else ((concl o snd o hd) asms)::(create_dischl ((tl asms),g)) in
    let dischls = map create_dischl new_hyps @ [[]] in
    let disch_pair = fun i (dischl,thm) -> DISCHL (map (instantiate i) dischl) thm in

    let normalfrees = itlist union (map ( fun (_,y) -> frees y ) instlist ) (gl_frees g) in
    let mvs = subtract (itlist union (map gl_frees new_goals) []) normalfrees in
    (mvs,null_inst),new_goals,fun i l ->  
      let major_thmi = INSTANTIATE_ALL i major_thm in
      let l = (major_thmi :: ((map (disch_pair i)) o (List.combine dischls)) l) in
      PROVE_HYP (List.fold_left (fun t1 t2 -> PROVE_HYP (INSTANTIATE_ALL i t2) t1) (INSTANTIATE_ALL i thm) ((butlast) l)) (last l);;


(* ------------------------------------------------------------------------- *)
(* cutm_tac: ((term * term) list -> meta_rule -> tactic):                    *)
(* Isabelle's cut_tac as a HOL Light meta_rule tactic.                       *)
(* Inserts a theorem in the assumptions.                                     *)
(* ------------------------------------------------------------------------- *)
(* (+) WARNING: It does not introduce metavariables like the other tactics   *)
(* do! In the TODO list...                                                   *)
(* ------------------------------------------------------------------------- *)

let (cutm_tac: (term * term) list -> meta_rule->tactic) =
    fun instlist r g ->
    let (_,_,thm) = inst_meta_rule_vars instlist r (gl_frees g) in
    (ASSUME_TAC thm) g;;


(* ------------------------------------------------------------------------- *)
(* erulenm_tac : (term * term) list -> int -> meta_rule->tactic)             *)
(* drulenm_tac : (term * term) list -> int -> meta_rule->tactic)             *)
(* frulenm_tac : (term * term) list -> int -> meta_rule->tactic)             *)
(* Identical to their counterparts, the only difference being that they try  *)
(* to match a particular assumption given by number.                         *)
(* ------------------------------------------------------------------------- *)

let (erulenm_tac: (term * term) list -> int -> meta_rule->tactic) =
  fun instlist n r ((asl,w) as g) ->
    let (c,hyps,thm) = inst_meta_rule_vars instlist r (gl_frees g) in

    let ins = try ( term_match [] c w ) 
    with Failure _ -> failwith "Rule doesn't match!" in
    let new_hyps = map (inst_goal ins) hyps in

    let (prems,prim_hyp) = 
      if (new_hyps = []) then failwith "erule: Not a proper elimination rule: no premises!" 
      else hd new_hyps in
    let avoids = gl_frees g in

    let asl,(prim_thm,elim_inst) = 
      if (prems = []) 
      then try term_to_asm_n_match avoids prim_hyp (rev asl) n with Failure s -> failwith ("erule: " ^ s) 
      else failwith "erule: Not a proper elimination rule: major premise has assumptions!" in
    let (_,prim_hyp)::new_hyps = map (inst_goal elim_inst) new_hyps in
    let thm = INSTANTIATE_ALL elim_inst thm in
    
    let create_goal = fun asms (hs,gl) -> (hs@asms,gl) in
    let new_goals = map (create_goal asl) new_hyps in
    let rec create_dischl = 
      fun (asms,g) -> 
	if (asms = []) then [] 
	else ((concl o snd o hd) asms)::(create_dischl ((tl asms),g)) in
    let dischls = map create_dischl new_hyps in
    let disch_pair = fun i (dischl,thm) -> DISCHL (map (instantiate i) dischl) thm in

    let normalfrees = itlist union (map ( fun (_,y) -> frees y ) instlist ) (gl_frees g) in
    let mvs = subtract (itlist union (map gl_frees new_goals) []) normalfrees in
    (mvs,null_inst),new_goals,fun i l ->  
      let major_thmi = INSTANTIATE_ALL i prim_thm in
      List.fold_left (fun t1 t2 -> PROVE_HYP (INSTANTIATE_ALL i t2) t1) (INSTANTIATE_ALL (compose_insts ins i) thm) 
	(major_thmi :: map (ADD_HYP major_thmi) (map (disch_pair i) (List.combine dischls l)));;


let (drulenm_tac: (term * term) list -> int -> meta_rule->tactic) =
  fun instlist n r ((asl,w) as g) ->
    let (c,hyps,thm) = inst_meta_rule_vars instlist r (gl_frees g) in

    let (prems,major_prem) = 
      if (hyps = []) then failwith "drule: Not a proper destruction rule: no premises!" 
      else hd hyps in
    let avoids = gl_frees g in

    let asl,(major_thm,elim_inst) = 
      if (prems = [])
      then try term_to_asm_n_match avoids major_prem (rev asl) n with Failure s -> failwith ("drule: " ^ s) 
      else failwith "drule: not a proper destruction rule: major premise has assumptions!" in
    let (_,major_asm)::new_hyps = map (inst_goal elim_inst) hyps in
    let thm = INSTANTIATE_ALL elim_inst thm in
    let create_goal = fun asms (hs,gl) -> (hs@asms,gl) in
    let new_goals = (map (create_goal asl) new_hyps) @ [create_goal asl (["",ASSUME (instantiate elim_inst c)],w)] in

    let rec create_dischl = 
      fun (asms,g) -> 
	if (asms = []) then [] 
	else ((concl o snd o hd) asms)::(create_dischl ((tl asms),g)) in
    (* We add an empty discharge list at the end for the extra goal. *)
    let dischls = map create_dischl new_hyps @ [[]] in
    let disch_pair = fun i (dischl,thm) -> DISCHL (map (instantiate i) dischl) thm in

    let normalfrees = itlist union (map ( fun (_,y) -> frees y ) instlist ) (gl_frees g) in
    let mvs = subtract (itlist union (map gl_frees new_goals) []) normalfrees in
    (mvs,null_inst),new_goals,fun i l ->  
      let major_thmi = INSTANTIATE_ALL i major_thm in
      let l = (major_thmi :: map (ADD_HYP major_thmi) (map (disch_pair i) (List.combine dischls l))) in
      PROVE_HYP (List.fold_left (fun t1 t2 -> PROVE_HYP (INSTANTIATE_ALL i t2) t1) (INSTANTIATE_ALL i thm) ((butlast) l)) (last l);;


let (frulenm_tac: (term * term) list -> int -> meta_rule->tactic) =
  fun instlist n r ((asl,w) as g) ->
    let (c,hyps,thm) = inst_meta_rule_vars instlist r (gl_frees g) in

    let (prems,major_prem) = 
      if (hyps = []) then failwith "frule: Not a proper destruction rule: no premises!" 
      else hd hyps in
    let avoids = gl_frees g in

    let _,(major_thm,elim_inst) = 
      if (prems = []) 
      then try term_to_asm_n_match avoids major_prem (rev asl) n with Failure s -> failwith ("frule: " ^ s) 
      else failwith "frule: Not a proper destruction rule: major premise has assumptions!" in
    let (_,major_asm)::new_hyps = map (inst_goal elim_inst) hyps in
    let thm = INSTANTIATE_ALL elim_inst thm in
    let create_goal = fun asms (hs,gl) -> (hs@asms,gl) in
    let new_goals = (map (create_goal asl) new_hyps) @ [create_goal asl (["",ASSUME (instantiate elim_inst c)],w)] in

    let rec create_dischl = 
      fun (asms,g) -> 
	if (asms = []) then [] 
	else ((concl o snd o hd) asms)::(create_dischl ((tl asms),g)) in
    let dischls = map create_dischl new_hyps @ [[]] in
    let disch_pair = fun i (dischl,thm) -> DISCHL (map (instantiate i) dischl) thm in

    let normalfrees = itlist union (map ( fun (_,y) -> frees y ) instlist ) (gl_frees g) in
    let mvs = subtract (itlist union (map gl_frees new_goals) []) normalfrees in
    (mvs,null_inst),new_goals,fun i l ->  
      let major_thmi = INSTANTIATE_ALL i major_thm in
      let l = (major_thmi :: ((map (disch_pair i)) o (List.combine dischls)) l) in
      PROVE_HYP (List.fold_left (fun t1 t2 -> PROVE_HYP (INSTANTIATE_ALL i t2) t1) (INSTANTIATE_ALL i thm) ((butlast) l)) (last l);;


(* ------------------------------------------------------------------------- *)
(* Xrulem versions for empty instlist.                                       *)
(* ------------------------------------------------------------------------- *)

let rulem: meta_rule -> tactic = rulem_tac [];;
let erulem: meta_rule -> tactic = erulem_tac [];;
let drulem: meta_rule -> tactic = drulem_tac [];;
let frulem: meta_rule -> tactic = frulem_tac [];;

let erulenm: int -> meta_rule -> tactic = erulenm_tac [];;
let drulenm: int -> meta_rule -> tactic = drulenm_tac [];;
let frulenm: int -> meta_rule -> tactic = frulenm_tac [];;

(* For consistency with HOL Light capitalized tactics: *)
let RULEM,ERULEM,DRULEM,FRULEM = rulem,erulem,drulem,frulem;;
let ERULENM,DRULENM,FRULENM = erulenm,drulenm,frulenm;;


(* ------------------------------------------------------------------------- *)
(* Xrule and Xrule_tac using arbitrary inference rules in the form of thms.  *)
(* (see mk_meta_rule and meta_rule type)                                     *)
(* ------------------------------------------------------------------------- *)

let rule_tac: (term * term) list -> thm -> tactic =
  fun instlist thm ->
    rulem_tac instlist (mk_meta_rule thm);;

let erule_tac: (term * term) list -> thm -> tactic =
  fun instlist thm ->
    erulem_tac instlist (mk_meta_rule thm);;

let drule_tac: (term * term) list -> thm -> tactic =
  fun instlist thm ->
    drulem_tac instlist (mk_meta_rule thm);;

let frule_tac: (term * term) list -> thm -> tactic =
  fun instlist thm ->
    frulem_tac instlist (mk_meta_rule thm);;

let cut_tac: (term * term) list -> thm -> tactic =
  fun instlist thm ->
    cutm_tac instlist (mk_meta_rule thm);;

let RULE_TAC,ERULE_TAC,DRULE_TAC,FRULE_TAC,CUT_TAC = rule_tac,erule_tac,drule_tac,frule_tac,cut_tac;;


let erulen_tac: (term * term) list -> int -> thm -> tactic =
  fun instlist n thm ->
    erulenm_tac instlist n (mk_meta_rule thm);;

let drulen_tac: (term * term) list -> int -> thm -> tactic =
  fun instlist n thm ->
    drulenm_tac instlist n (mk_meta_rule thm);;

let frulen_tac: (term * term) list -> int -> thm -> tactic =
  fun instlist n thm ->
    frulenm_tac instlist n (mk_meta_rule thm);;

let ERULEN_TAC,DRULEN_TAC,FRULEN_TAC = erulen_tac,drulen_tac,frulen_tac;;


let rule: (thm -> tactic) = rule_tac [];;
let erule: (thm -> tactic) = erule_tac [];;
let drule: (thm -> tactic) = drule_tac [];;
let frule: (thm -> tactic) = frule_tac [];;

let RULE,ERULE,DRULE,FRULE = rule,erule,drule,frule;;


let erulen: (int -> thm -> tactic) = erulen_tac [];;
let drulen: (int -> thm -> tactic) = drulen_tac [];;
let frulen: (int -> thm -> tactic) = frulen_tac [];;

let ERULEN,DRULEN,FRULEN = erulen,drulen,frulen;;