renamed Thm.cgoal_of to Thm.cprem_of;
authorwenzelm
Thu Nov 10 20:57:11 2005 +0100 (2005-11-10)
changeset 181456757627acf59
parent 18144 4edcb5fdc3b0
child 18146 47463b1825c6
renamed Thm.cgoal_of to Thm.cprem_of;
NEWS
src/HOL/Tools/datatype_aux.ML
src/HOL/Tools/record_package.ML
src/HOLCF/adm_tac.ML
src/Provers/splitter.ML
src/Pure/Isar/method.ML
src/Pure/goal.ML
src/Pure/tactic.ML
src/Pure/thm.ML
     1.1 --- a/NEWS	Thu Nov 10 17:33:14 2005 +0100
     1.2 +++ b/NEWS	Thu Nov 10 20:57:11 2005 +0100
     1.3 @@ -107,7 +107,7 @@
     1.4  Note that fold_index starts counting at index 0, not 1 like foldln used to.
     1.5  
     1.6  * Pure: primitive rule lift_rule now takes goal cterm instead of an
     1.7 -actual goal state (thm).  Use Thm.lift_rule (Thm.cgoal_of st i) to
     1.8 +actual goal state (thm).  Use Thm.lift_rule (Thm.cprem_of st i) to
     1.9  achieve the old behaviour.
    1.10  
    1.11  * Pure: the "Goal" constant is now called "prop", supporting a
     2.1 --- a/src/HOL/Tools/datatype_aux.ML	Thu Nov 10 17:33:14 2005 +0100
     2.2 +++ b/src/HOL/Tools/datatype_aux.ML	Thu Nov 10 20:57:11 2005 +0100
     2.3 @@ -115,7 +115,7 @@
     2.4    (List.nth (prems_of st, i - 1)) of
     2.5      _ $ (_ $ (f $ x) $ (g $ y)) =>
     2.6        let
     2.7 -        val cong' = Thm.lift_rule (Thm.cgoal_of st i) cong;
     2.8 +        val cong' = Thm.lift_rule (Thm.cprem_of st i) cong;
     2.9          val _ $ (_ $ (f' $ x') $ (g' $ y')) =
    2.10            Logic.strip_assums_concl (prop_of cong');
    2.11          val insts = map (pairself (cterm_of (#sign (rep_thm st))) o
    2.12 @@ -155,7 +155,7 @@
    2.13      val prem = List.nth (prems_of state, i - 1);
    2.14      val params = Logic.strip_params prem;
    2.15      val (_, Type (tname, _)) = hd (rev params);
    2.16 -    val exhaustion = Thm.lift_rule (Thm.cgoal_of state i) (exh_thm_of tname);
    2.17 +    val exhaustion = Thm.lift_rule (Thm.cprem_of state i) (exh_thm_of tname);
    2.18      val prem' = hd (prems_of exhaustion);
    2.19      val _ $ (_ $ lhs $ _) = hd (rev (Logic.strip_assums_hyp prem'));
    2.20      val exhaustion' = cterm_instantiate [(cterm_of sg (head_of lhs),
     3.1 --- a/src/HOL/Tools/record_package.ML	Thu Nov 10 17:33:14 2005 +0100
     3.2 +++ b/src/HOL/Tools/record_package.ML	Thu Nov 10 20:57:11 2005 +0100
     3.3 @@ -1234,7 +1234,7 @@
     3.4      val g = nth (prems_of st) (i - 1);
     3.5      val params = Logic.strip_params g;
     3.6      val concl = HOLogic.dest_Trueprop (Logic.strip_assums_concl g);
     3.7 -    val rule' = Thm.lift_rule (Thm.cgoal_of st i) rule;
     3.8 +    val rule' = Thm.lift_rule (Thm.cprem_of st i) rule;
     3.9      val (P, ys) = strip_comb (HOLogic.dest_Trueprop
    3.10        (Logic.strip_assums_concl (prop_of rule')));
    3.11      (* ca indicates if rule is a case analysis or induction rule *)
    3.12 @@ -1260,7 +1260,7 @@
    3.13      val sg = sign_of_thm st;
    3.14      val g = nth (prems_of st) (i - 1);
    3.15      val params = Logic.strip_params g;
    3.16 -    val exI' = Thm.lift_rule (Thm.cgoal_of st i) exI;
    3.17 +    val exI' = Thm.lift_rule (Thm.cprem_of st i) exI;
    3.18      val (_$(_$x)) = Logic.strip_assums_concl (hd (prems_of exI'));
    3.19      val cx = cterm_of sg (fst (strip_comb x));
    3.20  
     4.1 --- a/src/HOLCF/adm_tac.ML	Thu Nov 10 17:33:14 2005 +0100
     4.2 +++ b/src/HOLCF/adm_tac.ML	Thu Nov 10 20:57:11 2005 +0100
     4.3 @@ -113,7 +113,7 @@
     4.4    let val {sign, maxidx, ...} = rep_thm state;
     4.5        val j = maxidx+1;
     4.6        val parTs = map snd (rev params);
     4.7 -      val rule = Thm.lift_rule (Thm.cgoal_of state i) adm_subst;
     4.8 +      val rule = Thm.lift_rule (Thm.cprem_of state i) adm_subst;
     4.9        val types = valOf o (fst (types_sorts rule));
    4.10        val tT = types ("t", j);
    4.11        val PT = types ("P", j);
     5.1 --- a/src/Provers/splitter.ML	Thu Nov 10 17:33:14 2005 +0100
     5.2 +++ b/src/Provers/splitter.ML	Thu Nov 10 20:57:11 2005 +0100
     5.3 @@ -302,7 +302,7 @@
     5.4  
     5.5  fun inst_split Ts t tt thm TB state i =
     5.6    let
     5.7 -    val thm' = Thm.lift_rule (Thm.cgoal_of state i) thm;
     5.8 +    val thm' = Thm.lift_rule (Thm.cprem_of state i) thm;
     5.9      val (P, _) = strip_comb (fst (Logic.dest_equals
    5.10        (Logic.strip_assums_concl (#prop (rep_thm thm')))));
    5.11      val cert = cterm_of (sign_of_thm state);
     6.1 --- a/src/Pure/Isar/method.ML	Thu Nov 10 17:33:14 2005 +0100
     6.2 +++ b/src/Pure/Isar/method.ML	Thu Nov 10 20:57:11 2005 +0100
     6.3 @@ -435,7 +435,7 @@
     6.4          val lifttvar = pairself (ctyp_of thy o Logic.incr_tvar inc);
     6.5          val rule = Drule.instantiate
     6.6                (map lifttvar envT', map liftpair cenv)
     6.7 -              (Thm.lift_rule (Thm.cgoal_of st i) thm)
     6.8 +              (Thm.lift_rule (Thm.cprem_of st i) thm)
     6.9        in
    6.10          if i > nprems_of st then no_tac st
    6.11          else st |>
     7.1 --- a/src/Pure/goal.ML	Thu Nov 10 17:33:14 2005 +0100
     7.2 +++ b/src/Pure/goal.ML	Thu Nov 10 20:57:11 2005 +0100
     7.3 @@ -84,7 +84,7 @@
     7.4  (* composition of normal results *)
     7.5  
     7.6  fun compose_hhf tha i thb =
     7.7 -  Thm.bicompose false (false, Drule.lift_all (Thm.cgoal_of thb i) tha, 0) i thb;
     7.8 +  Thm.bicompose false (false, Drule.lift_all (Thm.cprem_of thb i) tha, 0) i thb;
     7.9  
    7.10  fun compose_hhf_tac th i = PRIMSEQ (compose_hhf th i);
    7.11  
    7.12 @@ -161,7 +161,7 @@
    7.13    composing the resulting thm with the original state.*)
    7.14  
    7.15  fun SELECT tac i st =
    7.16 -  init (Thm.adjust_maxidx (List.nth (Drule.cprems_of st, i - 1)))
    7.17 +  init (Thm.adjust_maxidx (Thm.cprem_of st i))
    7.18    |> tac
    7.19    |> Seq.maps (fn st' => Thm.bicompose false (false, conclude st', Thm.nprems_of st') i st);
    7.20  
     8.1 --- a/src/Pure/tactic.ML	Thu Nov 10 17:33:14 2005 +0100
     8.2 +++ b/src/Pure/tactic.ML	Thu Nov 10 20:57:11 2005 +0100
     8.3 @@ -253,7 +253,7 @@
     8.4      fun liftpair (cv,ct) = (cterm_fun liftvar cv, cterm_fun liftterm ct)
     8.5      val lifttvar = pairself (ctyp_fun (Logic.incr_tvar inc))
     8.6  in Drule.instantiate (map lifttvar Tinsts, map liftpair insts)
     8.7 -                     (Thm.lift_rule (Thm.cgoal_of st i) rule)
     8.8 +                     (Thm.lift_rule (Thm.cprem_of st i) rule)
     8.9  end;
    8.10  
    8.11  fun lift_inst_rule (st, i, sinsts, rule) = lift_inst_rule'
    8.12 @@ -285,7 +285,7 @@
    8.13        (ctyp_of thy (TVar ((a, i + inc), S)),
    8.14         ctyp_of thy (Logic.incr_tvar inc T))
    8.15  in Drule.instantiate (map liftTpair Tinsts, map liftpair insts)
    8.16 -                     (Thm.lift_rule (Thm.cgoal_of st i) rule)
    8.17 +                     (Thm.lift_rule (Thm.cprem_of st i) rule)
    8.18  end;
    8.19  
    8.20  (*** Resolve after lifting and instantation; may refer to parameters of the
     9.1 --- a/src/Pure/thm.ML	Thu Nov 10 17:33:14 2005 +0100
     9.2 +++ b/src/Pure/thm.ML	Thu Nov 10 20:57:11 2005 +0100
     9.3 @@ -83,7 +83,7 @@
     9.4    val prems_of: thm -> term list
     9.5    val nprems_of: thm -> int
     9.6    val cprop_of: thm -> cterm
     9.7 -  val cgoal_of: thm -> int -> cterm
     9.8 +  val cprem_of: thm -> int -> cterm
     9.9    val transfer: theory -> thm -> thm
    9.10    val weaken: cterm -> thm -> thm
    9.11    val extra_shyps: thm -> sort list
    9.12 @@ -451,9 +451,9 @@
    9.13  fun cprop_of (Thm {thy_ref, maxidx, shyps, prop, ...}) =
    9.14    Cterm {thy_ref = thy_ref, maxidx = maxidx, T = propT, t = prop, sorts = shyps};
    9.15  
    9.16 -fun cgoal_of (th as Thm {thy_ref, maxidx, shyps, prop, ...}) i =
    9.17 +fun cprem_of (th as Thm {thy_ref, maxidx, shyps, prop, ...}) i =
    9.18    Cterm {thy_ref = thy_ref, maxidx = maxidx, T = propT, sorts = shyps,
    9.19 -    t = Logic.nth_prem (i, prop) handle TERM _ => raise THM ("cgoal_of", i, [th])};
    9.20 +    t = Logic.nth_prem (i, prop) handle TERM _ => raise THM ("cprem_of", i, [th])};
    9.21  
    9.22  (*explicit transfer to a super theory*)
    9.23  fun transfer thy' thm =
    9.24 @@ -1472,7 +1472,7 @@
    9.25    Puts the rule above:  rule/state.  Renames vars in the rules. *)
    9.26  fun biresolution match brules i state =
    9.27      let val (stpairs, Bs, Bi, C) = dest_state(state,i);
    9.28 -        val lift = lift_rule (cgoal_of state i);
    9.29 +        val lift = lift_rule (cprem_of state i);
    9.30          val B = Logic.strip_assums_concl Bi;
    9.31          val Hs = Logic.strip_assums_hyp Bi;
    9.32          val comp = bicompose_aux match (state, (stpairs, Bs, Bi, C), true);