src/Pure/drule.ML
changeset 9554 1b0f02abbde8
parent 9547 8dad21f06b24
child 9829 bf49c3796599
equal deleted inserted replaced
9553:c2e3773475b6 9554:1b0f02abbde8
    27   val forall_intr_frees : thm -> thm
    27   val forall_intr_frees : thm -> thm
    28   val forall_intr_vars  : thm -> thm
    28   val forall_intr_vars  : thm -> thm
    29   val forall_elim_list  : cterm list -> thm -> thm
    29   val forall_elim_list  : cterm list -> thm -> thm
    30   val forall_elim_var   : int -> thm -> thm
    30   val forall_elim_var   : int -> thm -> thm
    31   val forall_elim_vars  : int -> thm -> thm
    31   val forall_elim_vars  : int -> thm -> thm
       
    32   val forall_elim_vars_safe  : thm -> thm
    32   val freeze_thaw       : thm -> thm * (thm -> thm)
    33   val freeze_thaw       : thm -> thm * (thm -> thm)
    33   val implies_elim_list : thm -> thm list -> thm
    34   val implies_elim_list : thm -> thm list -> thm
    34   val implies_intr_list : cterm list -> thm -> thm
    35   val implies_intr_list : cterm list -> thm -> thm
    35   val instantiate       :
    36   val instantiate       :
    36     (indexname * ctyp) list * (cterm * cterm) list -> thm -> thm
    37     (indexname * ctyp) list * (cterm * cterm) list -> thm -> thm
    97   val tag_assumption    : 'a attribute
    98   val tag_assumption    : 'a attribute
    98   val tag_internal      : 'a attribute
    99   val tag_internal      : 'a attribute
    99   val has_internal	: tag list -> bool
   100   val has_internal	: tag list -> bool
   100   val compose_single    : thm * int * thm -> thm
   101   val compose_single    : thm * int * thm -> thm
   101   val merge_rules	: thm list * thm list -> thm list
   102   val merge_rules	: thm list * thm list -> thm list
       
   103   val norm_hhf_eq	: thm
   102   val triv_goal         : thm
   104   val triv_goal         : thm
   103   val rev_triv_goal     : thm
   105   val rev_triv_goal     : thm
   104   val freeze_all        : thm -> thm
   106   val freeze_all        : thm -> thm
   105   val mk_triv_goal      : cterm -> thm
   107   val mk_triv_goal      : cterm -> thm
   106   val mk_cgoal          : cterm -> cterm
   108   val mk_cgoal          : cterm -> cterm
   281     end;
   283     end;
   282 
   284 
   283 val forall_elim_var = PureThy.forall_elim_var;
   285 val forall_elim_var = PureThy.forall_elim_var;
   284 val forall_elim_vars = PureThy.forall_elim_vars;
   286 val forall_elim_vars = PureThy.forall_elim_vars;
   285 
   287 
       
   288 fun forall_elim_vars_safe th =
       
   289   forall_elim_vars_safe (forall_elim_var (#maxidx (Thm.rep_thm th) + 1) th)
       
   290     handle THM _ => th;
       
   291 
       
   292 
   286 (*Specialization over a list of cterms*)
   293 (*Specialization over a list of cterms*)
   287 fun forall_elim_list cts th = foldr (uncurry forall_elim) (rev cts, th);
   294 fun forall_elim_list cts th = foldr (uncurry forall_elim) (rev cts, th);
   288 
   295 
   289 (* maps [A1,...,An], B   to   [| A1;...;An |] ==> B  *)
   296 (* maps [A1,...,An], B   to   [| A1;...;An |] ==> B  *)
   290 fun implies_intr_list cAs th = foldr (uncurry implies_intr) (cAs,th);
   297 fun implies_intr_list cAs th = foldr (uncurry implies_intr) (cAs,th);
   490 
   497 
   491 (*rewriting conversion*)
   498 (*rewriting conversion*)
   492 fun rew_conv mode prover mss = rewrite_cterm mode mss prover;
   499 fun rew_conv mode prover mss = rewrite_cterm mode mss prover;
   493 
   500 
   494 (*Rewrite a theorem*)
   501 (*Rewrite a theorem*)
   495 fun rewrite_rule_aux _ []   th = th
   502 fun rewrite_rule_aux _ [] = (fn th => th)
   496   | rewrite_rule_aux prover thms th =
   503   | rewrite_rule_aux prover thms =
   497       fconv_rule (rew_conv (true,false,false) prover (Thm.mss_of thms)) th;
   504       fconv_rule (rew_conv (true,false,false) prover (Thm.mss_of thms));
   498 
   505 
   499 fun rewrite_thm mode prover mss = fconv_rule (rew_conv mode prover mss);
   506 fun rewrite_thm mode prover mss = fconv_rule (rew_conv mode prover mss);
   500 fun rewrite_cterm mode prover mss = Thm.rewrite_cterm mode mss prover;
   507 fun rewrite_cterm mode prover mss = Thm.rewrite_cterm mode mss prover;
   501 
   508 
   502 (*Rewrite the subgoals of a proof state (represented by a theorem) *)
   509 (*Rewrite the subgoals of a proof state (represented by a theorem) *)
   575   let val PQ = read_prop "PROP phi ==> PROP psi"
   582   let val PQ = read_prop "PROP phi ==> PROP psi"
   576       and QP = read_prop "PROP psi ==> PROP phi"
   583       and QP = read_prop "PROP psi ==> PROP phi"
   577   in
   584   in
   578     store_standard_thm "equal_intr_rule"
   585     store_standard_thm "equal_intr_rule"
   579       (implies_intr PQ (implies_intr QP (equal_intr (assume PQ) (assume QP))))
   586       (implies_intr PQ (implies_intr QP (equal_intr (assume PQ) (assume QP))))
       
   587   end;
       
   588 
       
   589 
       
   590 (*(PROP ?phi ==> (!!x. PROP ?psi(x))) == (!!x. PROP ?phi ==> PROP ?psi(x))
       
   591   Rewrite rule for HHF normalization.
       
   592 
       
   593   Note: the syntax of ProtoPure is insufficient to handle this
       
   594   statement; storing it would be asking for trouble, e.g. when someone
       
   595   tries to print the theory later.
       
   596 *)
       
   597 
       
   598 val norm_hhf_eq =
       
   599   let
       
   600     val cert = Thm.cterm_of proto_sign;
       
   601     val aT = TFree ("'a", Term.logicS);
       
   602     val all = Term.all aT;
       
   603     val x = Free ("x", aT);
       
   604     val phi = Free ("phi", propT);
       
   605     val psi = Free ("psi", aT --> propT);
       
   606 
       
   607     val cx = cert x;
       
   608     val cphi = cert phi;
       
   609     val lhs = cert (Logic.mk_implies (phi, all $ Abs ("x", aT, psi $ Bound 0)));
       
   610     val rhs = cert (all $ Abs ("x", aT, Logic.mk_implies (phi, psi $ Bound 0)));
       
   611   in
       
   612     Thm.equal_intr
       
   613       (Thm.implies_elim (Thm.assume lhs) (Thm.assume cphi)
       
   614         |> Thm.forall_elim cx
       
   615         |> Thm.implies_intr cphi
       
   616         |> Thm.forall_intr cx
       
   617         |> Thm.implies_intr lhs)
       
   618       (Thm.implies_elim
       
   619           (Thm.assume rhs |> Thm.forall_elim cx) (Thm.assume cphi)
       
   620         |> Thm.forall_intr cx
       
   621         |> Thm.implies_intr cphi
       
   622         |> Thm.implies_intr rhs)
       
   623     |> standard |> curry Thm.name_thm "ProtoPure.norm_hhf_eq"
   580   end;
   624   end;
   581 
   625 
   582 
   626 
   583 (*** Instantiate theorem th, reading instantiations under signature sg ****)
   627 (*** Instantiate theorem th, reading instantiations under signature sg ****)
   584 
   628