src/Pure/Isar/object_logic.ML
changeset 16449 d0dc9a301e37
parent 15973 5fd94d84470f
child 17902 7b35ce796a4d
     1.1 --- a/src/Pure/Isar/object_logic.ML	Fri Jun 17 18:33:33 2005 +0200
     1.2 +++ b/src/Pure/Isar/object_logic.ML	Fri Jun 17 18:33:34 2005 +0200
     1.3 @@ -9,16 +9,16 @@
     1.4  sig
     1.5    val add_judgment: bstring * string * mixfix -> theory -> theory
     1.6    val add_judgment_i: bstring * typ * mixfix -> theory -> theory
     1.7 -  val judgment_name: Sign.sg -> string
     1.8 -  val is_judgment: Sign.sg -> term -> bool
     1.9 -  val drop_judgment: Sign.sg -> term -> term
    1.10 -  val fixed_judgment: Sign.sg -> string -> term
    1.11 -  val assert_propT: Sign.sg -> term -> term
    1.12 +  val judgment_name: theory -> string
    1.13 +  val is_judgment: theory -> term -> bool
    1.14 +  val drop_judgment: theory -> term -> term
    1.15 +  val fixed_judgment: theory -> string -> term
    1.16 +  val assert_propT: theory -> term -> term
    1.17    val declare_atomize: theory attribute
    1.18    val declare_rulify: theory attribute
    1.19 -  val atomize_term: Sign.sg -> term -> term
    1.20 +  val atomize_term: theory -> term -> term
    1.21    val atomize_thm: thm -> thm
    1.22 -  val atomize_rule: Sign.sg -> cterm -> thm
    1.23 +  val atomize_rule: theory -> cterm -> thm
    1.24    val atomize_tac: int -> tactic
    1.25    val full_atomize_tac: int -> tactic
    1.26    val atomize_goal: int -> thm -> thm
    1.27 @@ -36,27 +36,26 @@
    1.28  
    1.29  (* data kind 'Pure/object-logic' *)
    1.30  
    1.31 -structure ObjectLogicDataArgs =
    1.32 -struct
    1.33 +structure ObjectLogicData = TheoryDataFun
    1.34 +(struct
    1.35    val name = "Pure/object-logic";
    1.36    type T = string option * (thm list * thm list);
    1.37  
    1.38    val empty = (NONE, ([], [Drule.norm_hhf_eq]));
    1.39    val copy = I;
    1.40 -  val prep_ext = I;
    1.41 +  val extend = I;
    1.42  
    1.43    fun merge_judgment (SOME x, SOME y) =
    1.44          if x = y then SOME x else error "Attempt to merge different object-logics"
    1.45      | merge_judgment (j1, j2) = if is_some j1 then j1 else j2;
    1.46  
    1.47 -  fun merge ((judgment1, (atomize1, rulify1)), (judgment2, (atomize2, rulify2))) =
    1.48 +  fun merge _ ((judgment1, (atomize1, rulify1)), (judgment2, (atomize2, rulify2))) =
    1.49      (merge_judgment (judgment1, judgment2),
    1.50        (Drule.merge_rules (atomize1, atomize2), Drule.merge_rules (rulify1, rulify2)));
    1.51  
    1.52    fun print _ _ = ();
    1.53 -end;
    1.54 +end);
    1.55  
    1.56 -structure ObjectLogicData = TheoryDataFun(ObjectLogicDataArgs);
    1.57  val _ = Context.add_setup [ObjectLogicData.init];
    1.58  
    1.59  
    1.60 @@ -70,23 +69,12 @@
    1.61  fun new_judgment name (NONE, rules) = (SOME name, rules)
    1.62    | new_judgment _ (SOME _, _) = error "Attempt to redeclare object-logic judgment";
    1.63  
    1.64 -fun add_final name thy =
    1.65 -  let
    1.66 -    val typ = case Sign.const_type (sign_of thy) name of
    1.67 -		SOME T => T
    1.68 -	      | NONE => error "Internal error in ObjectLogic.gen_add_judgment";
    1.69 -  in
    1.70 -    Theory.add_finals_i false [Const(name,typ)] thy
    1.71 -  end;
    1.72 -
    1.73 -fun gen_add_judgment add_consts (name, T, syn) thy =
    1.74 -  let
    1.75 -    val fullname = Sign.full_name (Theory.sign_of thy) name;
    1.76 -  in
    1.77 +fun gen_add_judgment add_consts (bname, T, mx) thy =
    1.78 +  let val c = Sign.full_name thy (Syntax.const_name bname mx) in
    1.79      thy
    1.80 -    |> add_consts [(name, T, syn)]
    1.81 -    |> add_final fullname
    1.82 -    |> ObjectLogicData.map (new_judgment fullname)
    1.83 +    |> add_consts [(bname, T, mx)]
    1.84 +    |> (fn thy' => Theory.add_finals_i false [(Const (c, Sign.the_const_type thy' c))] thy')
    1.85 +    |> ObjectLogicData.map (new_judgment c)
    1.86    end;
    1.87  
    1.88  in
    1.89 @@ -99,32 +87,32 @@
    1.90  
    1.91  (* term operations *)
    1.92  
    1.93 -fun judgment_name sg =
    1.94 -  (case ObjectLogicData.get_sg sg of
    1.95 +fun judgment_name thy =
    1.96 +  (case ObjectLogicData.get thy of
    1.97      (SOME name, _) => name
    1.98    | _ => raise TERM ("Unknown object-logic judgment", []));
    1.99  
   1.100 -fun is_judgment sg (Const (c, _) $ _) = c = judgment_name sg
   1.101 +fun is_judgment thy (Const (c, _) $ _) = c = judgment_name thy
   1.102    | is_judgment _ _ = false;
   1.103  
   1.104 -fun drop_judgment sg (Abs (x, T, t)) = Abs (x, T, drop_judgment sg t)
   1.105 -  | drop_judgment sg (tm as (Const (c, _) $ t)) =
   1.106 -      if (c = judgment_name sg handle TERM _ => false) then t else tm
   1.107 +fun drop_judgment thy (Abs (x, T, t)) = Abs (x, T, drop_judgment thy t)
   1.108 +  | drop_judgment thy (tm as (Const (c, _) $ t)) =
   1.109 +      if (c = judgment_name thy handle TERM _ => false) then t else tm
   1.110    | drop_judgment _ tm = tm;
   1.111  
   1.112 -fun fixed_judgment sg x =
   1.113 +fun fixed_judgment thy x =
   1.114    let  (*be robust wrt. low-level errors*)
   1.115 -    val c = judgment_name sg;
   1.116 +    val c = judgment_name thy;
   1.117      val aT = TFree ("'a", []);
   1.118      val T =
   1.119 -      if_none (Sign.const_type sg c) (aT --> propT)
   1.120 +      if_none (Sign.const_type thy c) (aT --> propT)
   1.121        |> Term.map_type_tvar (fn ((x, _), S) => TFree (x, S));
   1.122      val U = Term.domain_type T handle Match => aT;
   1.123    in Const (c, T) $ Free (x, U) end;
   1.124  
   1.125 -fun assert_propT sg t =
   1.126 +fun assert_propT thy t =
   1.127    let val T = Term.fastype_of t
   1.128 -  in if T = propT then t else Const (judgment_name sg, T --> propT) $ t end;
   1.129 +  in if T = propT then t else Const (judgment_name thy, T --> propT) $ t end;
   1.130  
   1.131  
   1.132  
   1.133 @@ -132,8 +120,8 @@
   1.134  
   1.135  (* maintain rules *)
   1.136  
   1.137 -val get_atomize = #1 o #2 o ObjectLogicData.get_sg;
   1.138 -val get_rulify = #2 o #2 o ObjectLogicData.get_sg;
   1.139 +val get_atomize = #1 o #2 o ObjectLogicData.get;
   1.140 +val get_rulify = #2 o #2 o ObjectLogicData.get;
   1.141  
   1.142  val add_atomize = ObjectLogicData.map o Library.apsnd o Library.apfst o Drule.add_rule;
   1.143  val add_rulify = ObjectLogicData.map o Library.apsnd o Library.apsnd o Drule.add_rule;
   1.144 @@ -149,22 +137,22 @@
   1.145      (Drule.forall_conv
   1.146        (Drule.goals_conv (K true) (Tactic.rewrite true rews)))));
   1.147  
   1.148 -fun atomize_term sg =
   1.149 -  drop_judgment sg o MetaSimplifier.rewrite_term sg (get_atomize sg) [];
   1.150 +fun atomize_term thy =
   1.151 +  drop_judgment thy o MetaSimplifier.rewrite_term thy (get_atomize thy) [];
   1.152  
   1.153 -fun atomize_rule sg = Tactic.rewrite true (get_atomize sg);
   1.154 +fun atomize_rule thy = Tactic.rewrite true (get_atomize thy);
   1.155  
   1.156 -(*Convert a natural-deduction rule into a formula (probably in FOL)*)
   1.157 +(*convert a natural-deduction rule into an object-level formula*)
   1.158  fun atomize_thm th =
   1.159 -  rewrite_rule  (get_atomize (Thm.sign_of_thm th)) th;
   1.160 +  rewrite_rule (get_atomize (Thm.theory_of_thm th)) th;
   1.161  
   1.162  fun atomize_tac i st =
   1.163    if Logic.has_meta_prems (Thm.prop_of st) i then
   1.164 -    (rewrite_prems_tac (get_atomize (Thm.sign_of_thm st)) i) st
   1.165 +    (rewrite_prems_tac (get_atomize (Thm.theory_of_thm st)) i) st
   1.166    else all_tac st;
   1.167  
   1.168  fun full_atomize_tac i st =
   1.169 -  rewrite_goal_tac (get_atomize (Thm.sign_of_thm st)) i st;
   1.170 +  rewrite_goal_tac (get_atomize (Thm.theory_of_thm st)) i st;
   1.171  
   1.172  fun atomize_goal i st =
   1.173    (case Seq.pull (atomize_tac i st) of NONE => st | SOME (st', _) => st');
   1.174 @@ -173,7 +161,7 @@
   1.175  (* rulify *)
   1.176  
   1.177  fun gen_rulify full thm =
   1.178 -  Tactic.simplify full (get_rulify (Thm.sign_of_thm thm)) thm
   1.179 +  Tactic.simplify full (get_rulify (Thm.theory_of_thm thm)) thm
   1.180    |> Drule.gen_all |> Drule.strip_shyps_warning |> Drule.zero_var_indexes;
   1.181  
   1.182  val rulify = gen_rulify true;