src/Pure/goal.ML
changeset 18207 9edbeda7e39a
parent 18180 db712213504d
child 18252 9e2c15ae0e86
     1.1 --- a/src/Pure/goal.ML	Sat Nov 19 14:21:03 2005 +0100
     1.2 +++ b/src/Pure/goal.ML	Sat Nov 19 14:21:04 2005 +0100
     1.3 @@ -18,7 +18,7 @@
     1.4    val conclude: thm -> thm
     1.5    val finish: thm -> thm
     1.6    val norm_hhf: thm -> thm
     1.7 -  val norm_hhf': thm -> thm
     1.8 +  val norm_hhf_protected: thm -> thm
     1.9    val compose_hhf: thm -> int -> thm -> thm Seq.seq
    1.10    val compose_hhf_tac: thm -> int -> tactic
    1.11    val comp_hhf: thm -> thm -> thm
    1.12 @@ -73,23 +73,26 @@
    1.13  
    1.14  (** results **)
    1.15  
    1.16 -(* HHF normal form *)
    1.17 +(* HHF normal form: !! before ==>, outermost !! generalized *)
    1.18 +
    1.19 +local
    1.20  
    1.21 -val norm_hhf_ss =
    1.22 +fun gen_norm_hhf ss =
    1.23 +  (not o Drule.is_norm_hhf o Thm.prop_of) ?
    1.24 +    Drule.fconv_rule (MetaSimplifier.rewrite_cterm (true, false, false) (K (K NONE)) ss)
    1.25 +  #> Thm.adjust_maxidx_thm
    1.26 +  #> Drule.gen_all;
    1.27 +
    1.28 +val ss =
    1.29    MetaSimplifier.theory_context ProtoPure.thy MetaSimplifier.empty_ss
    1.30      addsimps [Drule.norm_hhf_eq];
    1.31  
    1.32 -val norm_hhf_ss' = norm_hhf_ss addeqcongs [Drule.protect_cong];
    1.33 +in
    1.34  
    1.35 -fun gen_norm_hhf protected =
    1.36 -  (not o Drule.is_norm_hhf o Thm.prop_of) ?
    1.37 -    Drule.fconv_rule (MetaSimplifier.rewrite_cterm (true, false, false) (K (K NONE))
    1.38 -      (if protected then norm_hhf_ss else norm_hhf_ss'))
    1.39 -  #> Thm.adjust_maxidx_thm
    1.40 -  #> Drule.gen_all;
    1.41 +val norm_hhf = gen_norm_hhf ss;
    1.42 +val norm_hhf_protected = gen_norm_hhf (ss addeqcongs [Drule.protect_cong]);
    1.43  
    1.44 -val norm_hhf = gen_norm_hhf true;
    1.45 -val norm_hhf' = gen_norm_hhf false;
    1.46 +end;
    1.47  
    1.48  
    1.49  (* composition of normal results *)
    1.50 @@ -171,11 +174,15 @@
    1.51    by making a new state from subgoal i, applying tac to it, and
    1.52    composing the resulting thm with the original state.*)
    1.53  
    1.54 +local
    1.55 +
    1.56  fun SELECT tac i st =
    1.57    init (Thm.adjust_maxidx (Thm.cprem_of st i))
    1.58    |> tac
    1.59    |> Seq.maps (fn st' => Thm.bicompose false (false, conclude st', Thm.nprems_of st') i st);
    1.60  
    1.61 +in
    1.62 +
    1.63  fun SELECT_GOAL tac i st =
    1.64    let val n = Thm.nprems_of st in
    1.65      if 1 <= i andalso i <= n then
    1.66 @@ -185,5 +192,7 @@
    1.67  
    1.68  end;
    1.69  
    1.70 +end;
    1.71 +
    1.72  structure BasicGoal: BASIC_GOAL = Goal;
    1.73  open BasicGoal;