# HG changeset patch
# User wenzelm
# Date 1132159525 -3600
# Node ID cf4b265007bf2d4bdb2cc581ffbf955fbf7ddcfd
# Parent  9e4dfe0315254d2df3fc1e2582b9ec57e2cd4a2b
added protect_cong, cong_mono_thm;
outer_params: Syntax.deskolem;

diff -r 9e4dfe031525 -r cf4b265007bf src/Pure/drule.ML
--- a/src/Pure/drule.ML	Wed Nov 16 17:45:24 2005 +0100
+++ b/src/Pure/drule.ML	Wed Nov 16 17:45:25 2005 +0100
@@ -10,80 +10,80 @@
 
 signature BASIC_DRULE =
 sig
-  val mk_implies        : cterm * cterm -> cterm
-  val list_implies      : cterm list * cterm -> cterm
-  val dest_implies      : cterm -> cterm * cterm
-  val dest_equals       : cterm -> cterm * cterm
-  val strip_imp_prems   : cterm -> cterm list
-  val strip_imp_concl   : cterm -> cterm
-  val cprems_of         : thm -> cterm list
-  val cterm_fun         : (term -> term) -> (cterm -> cterm)
-  val ctyp_fun          : (typ -> typ) -> (ctyp -> ctyp)
-  val read_insts        :
+  val mk_implies: cterm * cterm -> cterm
+  val list_implies: cterm list * cterm -> cterm
+  val dest_implies: cterm -> cterm * cterm
+  val dest_equals: cterm -> cterm * cterm
+  val strip_imp_prems: cterm -> cterm list
+  val strip_imp_concl: cterm -> cterm
+  val cprems_of: thm -> cterm list
+  val cterm_fun: (term -> term) -> (cterm -> cterm)
+  val ctyp_fun: (typ -> typ) -> (ctyp -> ctyp)
+  val read_insts:
           theory -> (indexname -> typ option) * (indexname -> sort option)
                   -> (indexname -> typ option) * (indexname -> sort option)
                   -> string list -> (indexname * string) list
                   -> (ctyp * ctyp) list * (cterm * cterm) list
   val types_sorts: thm -> (indexname-> typ option) * (indexname-> sort option)
-  val strip_shyps_warning : thm -> thm
-  val forall_intr_list  : cterm list -> thm -> thm
-  val forall_intr_frees : thm -> thm
-  val forall_intr_vars  : thm -> thm
-  val forall_elim_list  : cterm list -> thm -> thm
-  val forall_elim_var   : int -> thm -> thm
-  val forall_elim_vars  : int -> thm -> thm
-  val gen_all           : thm -> thm
-  val lift_all          : cterm -> thm -> thm
-  val freeze_thaw       : thm -> thm * (thm -> thm)
+  val strip_shyps_warning: thm -> thm
+  val forall_intr_list: cterm list -> thm -> thm
+  val forall_intr_frees: thm -> thm
+  val forall_intr_vars: thm -> thm
+  val forall_elim_list: cterm list -> thm -> thm
+  val forall_elim_var: int -> thm -> thm
+  val forall_elim_vars: int -> thm -> thm
+  val gen_all: thm -> thm
+  val lift_all: cterm -> thm -> thm
+  val freeze_thaw: thm -> thm * (thm -> thm)
   val freeze_thaw_robust: thm -> thm * (int -> thm -> thm)
-  val implies_elim_list : thm -> thm list -> thm
-  val implies_intr_list : cterm list -> thm -> thm
-  val instantiate       :
+  val implies_elim_list: thm -> thm list -> thm
+  val implies_intr_list: cterm list -> thm -> thm
+  val instantiate:
     (ctyp * ctyp) list * (cterm * cterm) list -> thm -> thm
-  val zero_var_indexes  : thm -> thm
-  val implies_intr_hyps : thm -> thm
-  val standard          : thm -> thm
-  val standard'         : thm -> thm
-  val rotate_prems      : int -> thm -> thm
-  val rearrange_prems   : int list -> thm -> thm
-  val assume_ax         : theory -> string -> thm
-  val RSN               : thm * (int * thm) -> thm
-  val RS                : thm * thm -> thm
-  val RLN               : thm list * (int * thm list) -> thm list
-  val RL                : thm list * thm list -> thm list
-  val MRS               : thm list * thm -> thm
-  val MRL               : thm list list * thm list -> thm list
-  val OF                : thm * thm list -> thm
-  val compose           : thm * int * thm -> thm list
-  val COMP              : thm * thm -> thm
+  val zero_var_indexes: thm -> thm
+  val implies_intr_hyps: thm -> thm
+  val standard: thm -> thm
+  val standard': thm -> thm
+  val rotate_prems: int -> thm -> thm
+  val rearrange_prems: int list -> thm -> thm
+  val assume_ax: theory -> string -> thm
+  val RSN: thm * (int * thm) -> thm
+  val RS: thm * thm -> thm
+  val RLN: thm list * (int * thm list) -> thm list
+  val RL: thm list * thm list -> thm list
+  val MRS: thm list * thm -> thm
+  val MRL: thm list list * thm list -> thm list
+  val OF: thm * thm list -> thm
+  val compose: thm * int * thm -> thm list
+  val COMP: thm * thm -> thm
   val read_instantiate_sg: theory -> (string*string)list -> thm -> thm
-  val read_instantiate  : (string*string)list -> thm -> thm
-  val cterm_instantiate : (cterm*cterm)list -> thm -> thm
-  val eq_thm_thy        : thm * thm -> bool
-  val eq_thm_prop	: thm * thm -> bool
-  val weak_eq_thm       : thm * thm -> bool
-  val size_of_thm       : thm -> int
-  val reflexive_thm     : thm
-  val symmetric_thm     : thm
-  val transitive_thm    : thm
-  val symmetric_fun     : thm -> thm
-  val extensional       : thm -> thm
-  val imp_cong          : thm
-  val swap_prems_eq     : thm
-  val equal_abs_elim    : cterm  -> thm -> thm
+  val read_instantiate: (string*string)list -> thm -> thm
+  val cterm_instantiate: (cterm*cterm)list -> thm -> thm
+  val eq_thm_thy: thm * thm -> bool
+  val eq_thm_prop: thm * thm -> bool
+  val weak_eq_thm: thm * thm -> bool
+  val size_of_thm: thm -> int
+  val reflexive_thm: thm
+  val symmetric_thm: thm
+  val transitive_thm: thm
+  val symmetric_fun: thm -> thm
+  val extensional: thm -> thm
+  val imp_cong: thm
+  val swap_prems_eq: thm
+  val equal_abs_elim: cterm  -> thm -> thm
   val equal_abs_elim_list: cterm list -> thm -> thm
-  val asm_rl            : thm
-  val cut_rl            : thm
-  val revcut_rl         : thm
-  val thin_rl           : thm
+  val asm_rl: thm
+  val cut_rl: thm
+  val revcut_rl: thm
+  val thin_rl: thm
   val triv_forall_equality: thm
-  val swap_prems_rl     : thm
-  val equal_intr_rule   : thm
-  val equal_elim_rule1  : thm
-  val inst              : string -> string -> thm -> thm
-  val instantiate'      : ctyp option list -> cterm option list -> thm -> thm
-  val incr_indexes      : thm -> thm -> thm
-  val incr_indexes_wrt  : int list -> ctyp list -> cterm list -> thm list -> thm -> thm
+  val swap_prems_rl: thm
+  val equal_intr_rule: thm
+  val equal_elim_rule1: thm
+  val inst: string -> string -> thm -> thm
+  val instantiate': ctyp option list -> cterm option list -> thm -> thm
+  val incr_indexes: thm -> thm -> thm
+  val incr_indexes_wrt: int list -> ctyp list -> cterm list -> thm list -> thm -> thm
 end;
 
 signature DRULE =
@@ -117,18 +117,19 @@
   val add_rules: thm list -> thm list -> thm list
   val del_rules: thm list -> thm list -> thm list
   val merge_rules: thm list * thm list -> thm list
-  val imp_cong'         : thm -> thm -> thm
+  val imp_cong': thm -> thm -> thm
   val beta_eta_conversion: cterm -> thm
   val eta_long_conversion: cterm -> thm
-  val goals_conv        : (int -> bool) -> (cterm -> thm) -> cterm -> thm
-  val forall_conv       : (cterm -> thm) -> cterm -> thm
-  val fconv_rule        : (cterm -> thm) -> thm -> thm
+  val goals_conv: (int -> bool) -> (cterm -> thm) -> cterm -> thm
+  val forall_conv: (cterm -> thm) -> cterm -> thm
+  val fconv_rule: (cterm -> thm) -> thm -> thm
   val norm_hhf_eq: thm
   val is_norm_hhf: term -> bool
   val norm_hhf: theory -> term -> term
   val protect: cterm -> cterm
   val protectI: thm
   val protectD: thm
+  val protect_cong: thm
   val implies_intr_protected: cterm list -> thm -> thm
   val freeze_all: thm -> thm
   val tvars_of_terms: term list -> (indexname * sort) list
@@ -150,6 +151,7 @@
   val conj_elim_list: thm -> thm list
   val conj_elim_precise: int -> thm -> thm list
   val conj_intr_thm: thm
+  val conj_mono_thm: thm
   val abs_def: thm -> thm
   val read_instantiate_sg': theory -> (indexname * string) list -> thm -> thm
   val read_instantiate': (indexname * string) list -> thm -> thm
@@ -215,7 +217,7 @@
   | list_comb (f, t::ts) = list_comb (Thm.capply f t, ts);
 
 (*cterm version of strip_comb: maps  f(t1,...,tn)  to  (f, [t1,...,tn]) *)
-fun strip_comb ct = 
+fun strip_comb ct =
   let
     fun stripc (p as (ct, cts)) =
       let val (ct1, ct2) = Thm.dest_comb ct
@@ -233,7 +235,7 @@
 
 (*Beta-conversion for cterms, where x is an abstraction. Simply returns the rhs
   of the meta-equality returned by the beta_conversion rule.*)
-fun beta_conv x y = 
+fun beta_conv x y =
     #2 (Thm.dest_comb (cprop_of (Thm.beta_conversion false (Thm.capply x y))));
 
 fun plain_prop_of raw_thm =
@@ -300,7 +302,7 @@
 fun types_sorts thm =
     let val {prop, hyps, tpairs, ...} = Thm.rep_thm thm;
         (* bogus term! *)
-        val big = Term.list_comb 
+        val big = Term.list_comb
                     (Term.list_comb (prop, hyps), Thm.terms_of_tpairs tpairs);
         val vars = map dest_Var (term_vars big);
         val frees = map dest_Free (term_frees big);
@@ -406,7 +408,7 @@
 fun outer_params t =
   let
     val vs = Term.strip_all_vars t;
-    val xs = Term.variantlist (map #1 vs, []);
+    val xs = Term.variantlist (map (Syntax.deskolem o #1) vs, []);
   in xs ~~ map #2 vs end;
 
 (*generalize outermost parameters*)
@@ -878,6 +880,8 @@
     |> store_standard_thm_open "norm_hhf_eq"
   end;
 
+val norm_hhf_prop = Logic.dest_equals (Thm.prop_of norm_hhf_eq);
+
 fun is_norm_hhf tm =
   let
     fun is_norm (Const ("==>", _) $ _ $ (Const ("all", _) $ _)) = false
@@ -888,7 +892,8 @@
 
 fun norm_hhf thy t =
   if is_norm_hhf t then t
-  else Pattern.rewrite_term thy [Logic.dest_equals (prop_of norm_hhf_eq)] [] t;
+  else Pattern.rewrite_term thy [norm_hhf_prop] [] t;
+
 
 
 (*** Instantiate theorem th, reading instantiations in theory thy ****)
@@ -926,7 +931,7 @@
 in
 fun cterm_instantiate ctpairs0 th =
   let val (thy,tye,_) = foldr add_types (Thm.theory_of_thm th, Vartab.empty, 0) ctpairs0
-      fun instT(ct,cu) = 
+      fun instT(ct,cu) =
         let val inst = cterm_of thy o Envir.subst_TVars tye o term_of
         in (inst ct, inst cu) end
       fun ctyp2 (ixn, (S, T)) = (ctyp_of thy (TVar (ixn, S)), ctyp_of thy T)
@@ -967,6 +972,7 @@
       (Thm.equal_elim (Thm.symmetric prop_def) (Thm.assume A))));
   val protectD = store_thm "protectD" (kind_rule internalK (standard
       (Thm.equal_elim prop_def (Thm.assume (protect A)))));
+  val protect_cong = store_standard_thm_open "protect_cong" (Thm.reflexive (protect A));
 end;
 
 fun implies_intr_protected asms th =
@@ -1121,7 +1127,11 @@
   val A = read_prop "PROP A";
   val B = read_prop "PROP B";
   val C = read_prop "PROP C";
+  val D = read_prop "PROP D";
+  val AC = read_prop "PROP A ==> PROP C";
+  val BD = read_prop "PROP B ==> PROP D";
   val ABC = read_prop "PROP A ==> PROP B ==> PROP C";
+  val A_B = read_prop "!!X. (PROP A ==> PROP B ==> PROP X) ==> PROP X";
 
   val proj1 =
     forall_intr_list [A, B] (implies_intr_list [A, B] (Thm.assume A))
@@ -1160,6 +1170,13 @@
 val conj_intr_thm = store_standard_thm_open "conjunctionI"
   (implies_intr_list [A, B] (conj_intr (Thm.assume A) (Thm.assume B)));
 
+val conj_mono_thm = store_standard_thm_open "conjunction_mono"
+  (Thm.assume A_B |> conj_elim |> (fn (a, b) =>
+    conj_intr
+      (Thm.implies_elim (Thm.assume AC) a)
+      (Thm.implies_elim (Thm.assume BD) b))
+  |> implies_intr_list [AC, BD, A_B]);
+
 end;
 
 end;