src/Pure/drule.ML
changeset 11975 129c6679e8c4
parent 11960 58ffa8bec4da
child 11997 402ae1a172ae
     1.1 --- a/src/Pure/drule.ML	Sun Oct 28 19:44:26 2001 +0100
     1.2 +++ b/src/Pure/drule.ML	Sun Oct 28 19:44:58 2001 +0100
     1.3 @@ -84,38 +84,42 @@
     1.4  signature DRULE =
     1.5  sig
     1.6    include BASIC_DRULE
     1.7 -  val rule_attribute    : ('a -> thm -> thm) -> 'a attribute
     1.8 -  val tag_rule          : tag -> thm -> thm
     1.9 -  val untag_rule        : string -> thm -> thm
    1.10 -  val tag               : tag -> 'a attribute
    1.11 -  val untag             : string -> 'a attribute
    1.12 -  val get_kind          : thm -> string
    1.13 -  val kind              : string -> 'a attribute
    1.14 -  val theoremK          : string
    1.15 -  val lemmaK            : string
    1.16 -  val corollaryK        : string
    1.17 -  val internalK         : string
    1.18 -  val kind_internal     : 'a attribute
    1.19 -  val has_internal      : tag list -> bool
    1.20 -  val impose_hyps       : cterm list -> thm -> thm
    1.21 -  val close_derivation  : thm -> thm
    1.22 -  val compose_single    : thm * int * thm -> thm
    1.23 -  val add_rules         : thm list -> thm list -> thm list
    1.24 -  val del_rules         : thm list -> thm list -> thm list
    1.25 -  val merge_rules       : thm list * thm list -> thm list
    1.26 -  val norm_hhf_eq       : thm
    1.27 -  val triv_goal         : thm
    1.28 -  val rev_triv_goal     : thm
    1.29 +  val rule_attribute: ('a -> thm -> thm) -> 'a attribute
    1.30 +  val tag_rule: tag -> thm -> thm
    1.31 +  val untag_rule: string -> thm -> thm
    1.32 +  val tag: tag -> 'a attribute
    1.33 +  val untag: string -> 'a attribute
    1.34 +  val get_kind: thm -> string
    1.35 +  val kind: string -> 'a attribute
    1.36 +  val theoremK: string
    1.37 +  val lemmaK: string
    1.38 +  val corollaryK: string
    1.39 +  val internalK: string
    1.40 +  val kind_internal: 'a attribute
    1.41 +  val has_internal: tag list -> bool
    1.42 +  val impose_hyps: cterm list -> thm -> thm
    1.43 +  val close_derivation: thm -> thm
    1.44 +  val compose_single: thm * int * thm -> thm
    1.45 +  val add_rules: thm list -> thm list -> thm list
    1.46 +  val del_rules: thm list -> thm list -> thm list
    1.47 +  val merge_rules: thm list * thm list -> thm list
    1.48 +  val norm_hhf_eq: thm
    1.49 +  val triv_goal: thm
    1.50 +  val rev_triv_goal: thm
    1.51    val implies_intr_goals: cterm list -> thm -> thm
    1.52 -  val freeze_all        : thm -> thm
    1.53 -  val mk_triv_goal      : cterm -> thm
    1.54 -  val tvars_of_terms    : term list -> (indexname * sort) list
    1.55 -  val vars_of_terms     : term list -> (indexname * typ) list
    1.56 -  val tvars_of          : thm -> (indexname * sort) list
    1.57 -  val vars_of           : thm -> (indexname * typ) list
    1.58 -  val unvarifyT         : thm -> thm
    1.59 -  val unvarify          : thm -> thm
    1.60 -  val tvars_intr_list   : string list -> thm -> thm
    1.61 +  val freeze_all: thm -> thm
    1.62 +  val mk_triv_goal: cterm -> thm
    1.63 +  val tvars_of_terms: term list -> (indexname * sort) list
    1.64 +  val vars_of_terms: term list -> (indexname * typ) list
    1.65 +  val tvars_of: thm -> (indexname * sort) list
    1.66 +  val vars_of: thm -> (indexname * typ) list
    1.67 +  val unvarifyT: thm -> thm
    1.68 +  val unvarify: thm -> thm
    1.69 +  val tvars_intr_list: string list -> thm -> thm
    1.70 +  val conj_intr: thm -> thm -> thm
    1.71 +  val conj_intr_list: thm list -> thm
    1.72 +  val conj_elim: thm -> thm * thm
    1.73 +  val conj_elim_list: thm -> thm list
    1.74  end;
    1.75  
    1.76  structure Drule: DRULE =
    1.77 @@ -875,8 +879,47 @@
    1.78  (*make an initial proof state, "PROP A ==> (PROP A)" *)
    1.79  fun mk_triv_goal ct = instantiate' [] [Some ct] triv_goal;
    1.80  
    1.81 +
    1.82 +
    1.83 +(** meta-level conjunction **)
    1.84 +
    1.85 +local
    1.86 +  val A = read_prop "PROP A";
    1.87 +  val B = read_prop "PROP B";
    1.88 +  val C = read_prop "PROP C";
    1.89 +  val ABC = read_prop "PROP A ==> PROP B ==> PROP C";
    1.90 +
    1.91 +  val proj1 =
    1.92 +    forall_intr_list [A, B] (implies_intr_list [A, B] (Thm.assume A))
    1.93 +    |> forall_elim_vars 0;
    1.94 +
    1.95 +  val proj2 =
    1.96 +    forall_intr_list [A, B] (implies_intr_list [A, B] (Thm.assume B))
    1.97 +    |> forall_elim_vars 0;
    1.98 +
    1.99 +  val conj_intr_rule =
   1.100 +    forall_intr_list [A, B] (implies_intr_list [A, B]
   1.101 +      (Thm.forall_intr C (Thm.implies_intr ABC
   1.102 +        (implies_elim_list (Thm.assume ABC) [Thm.assume A, Thm.assume B]))))
   1.103 +    |> forall_elim_vars 0;
   1.104 +
   1.105 +  val incr = incr_indexes_wrt [] [] [];
   1.106 +in
   1.107 +
   1.108 +fun conj_intr tha thb = thb COMP (tha COMP incr [tha, thb] conj_intr_rule);
   1.109 +val conj_intr_list = foldr1 (uncurry conj_intr);
   1.110 +
   1.111 +fun conj_elim th =
   1.112 +  let val th' = forall_elim_var (#maxidx (Thm.rep_thm th) + 1) th
   1.113 +  in (incr [th'] proj1 COMP th', incr [th'] proj2 COMP th') end;
   1.114 +
   1.115 +fun conj_elim_list th =
   1.116 +  let val (th1, th2) = conj_elim th
   1.117 +  in conj_elim_list th1 @ conj_elim_list th2 end handle THM _ => [th];
   1.118 +
   1.119  end;
   1.120  
   1.121 +end;
   1.122  
   1.123  structure BasicDrule: BASIC_DRULE = Drule;
   1.124  open BasicDrule;