moved object_logic.ML to Isar/object_logic.ML;
authorwenzelm
Mon Oct 22 18:07:53 2001 +0200 (2001-10-22)
changeset 11897b9f2028f53bd
parent 11896 1ff33f896720
child 11898 0844573f4518
moved object_logic.ML to Isar/object_logic.ML;
src/Pure/Isar/object_logic.ML
src/Pure/object_logic.ML
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Pure/Isar/object_logic.ML	Mon Oct 22 18:07:53 2001 +0200
     1.3 @@ -0,0 +1,156 @@
     1.4 +(*  Title:      Pure/Isar/object_logic.ML
     1.5 +    ID:         $Id$
     1.6 +    Author:     Markus Wenzel, TU Muenchen
     1.7 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
     1.8 +
     1.9 +Specifics about common object-logics.
    1.10 +*)
    1.11 +
    1.12 +signature OBJECT_LOGIC =
    1.13 +sig
    1.14 +  val add_judgment: bstring * string * mixfix -> theory -> theory
    1.15 +  val add_judgment_i: bstring * typ * mixfix -> theory -> theory
    1.16 +  val judgment_name: Sign.sg -> string
    1.17 +  val is_judgment: Sign.sg -> term -> bool
    1.18 +  val drop_judgment: Sign.sg -> term -> term
    1.19 +  val fixed_judgment: Sign.sg -> string -> term
    1.20 +  val declare_atomize: theory attribute
    1.21 +  val declare_rulify: theory attribute
    1.22 +  val atomize_tac: int -> tactic
    1.23 +  val atomize_goal: int -> thm -> thm
    1.24 +  val rulify: thm -> thm
    1.25 +  val rulify_no_asm: thm -> thm
    1.26 +  val rule_format: 'a attribute
    1.27 +  val rule_format_no_asm: 'a attribute
    1.28 +  val setup: (theory -> theory) list
    1.29 +end;
    1.30 +
    1.31 +structure ObjectLogic: OBJECT_LOGIC =
    1.32 +struct
    1.33 +
    1.34 +
    1.35 +(** object-logic theory data **)
    1.36 +
    1.37 +(* data kind 'Pure/object-logic' *)
    1.38 +
    1.39 +structure ObjectLogicDataArgs =
    1.40 +struct
    1.41 +  val name = "Pure/object-logic";
    1.42 +  type T = string option * (thm list * thm list);
    1.43 +
    1.44 +  val empty = (None, ([], [Drule.norm_hhf_eq]));
    1.45 +  val copy = I;
    1.46 +  val prep_ext = I;
    1.47 +
    1.48 +  fun merge_judgment (Some x, Some y) =
    1.49 +        if x = y then Some x else error "Attempt to merge different object-logics"
    1.50 +    | merge_judgment (j1, j2) = if is_some j1 then j1 else j2;
    1.51 +
    1.52 +  fun merge ((judgment1, (atomize1, rulify1)), (judgment2, (atomize2, rulify2))) =
    1.53 +    (merge_judgment (judgment1, judgment2),
    1.54 +      (Drule.merge_rules (atomize1, atomize2), Drule.merge_rules (rulify1, rulify2)));
    1.55 +
    1.56 +  fun print _ _ = ();
    1.57 +end;
    1.58 +
    1.59 +structure ObjectLogicData = TheoryDataFun(ObjectLogicDataArgs);
    1.60 +
    1.61 +
    1.62 +(** generic treatment of judgments -- with a single argument only **)
    1.63 +
    1.64 +(* add_judgment(_i) *)
    1.65 +
    1.66 +local
    1.67 +
    1.68 +fun new_judgment name (None, rules) = (Some name, rules)
    1.69 +  | new_judgment _ (Some _, _) = error "Attempt to redeclare object-logic judgment";
    1.70 +
    1.71 +fun gen_add_judgment add_consts (name, T, syn) thy =
    1.72 +  thy
    1.73 +  |> add_consts [(name, T, syn)]
    1.74 +  |> ObjectLogicData.map (new_judgment (Sign.full_name (Theory.sign_of thy) name));
    1.75 +
    1.76 +in
    1.77 +
    1.78 +val add_judgment = gen_add_judgment Theory.add_consts;
    1.79 +val add_judgment_i = gen_add_judgment Theory.add_consts_i;
    1.80 +
    1.81 +end;
    1.82 +
    1.83 +
    1.84 +(* term operations *)
    1.85 +
    1.86 +fun judgment_name sg =
    1.87 +  (case ObjectLogicData.get_sg sg of
    1.88 +    (Some name, _) => name
    1.89 +  | _ => raise TERM ("Unknown object-logic judgment", []));
    1.90 +
    1.91 +fun is_judgment sg (Const (c, _) $ _) = c = judgment_name sg
    1.92 +  | is_judgment _ _ = false;
    1.93 +
    1.94 +fun drop_judgment sg (Abs (x, T, t)) = Abs (x, T, drop_judgment sg t)
    1.95 +  | drop_judgment sg (tm as (Const (c, _) $ t)) = if c = judgment_name sg then t else tm
    1.96 +  | drop_judgment _ tm = tm;
    1.97 +
    1.98 +fun fixed_judgment sg x =
    1.99 +  let  (*be robust wrt. low-level errors*)
   1.100 +    val c = judgment_name sg;
   1.101 +    val aT = TFree ("'a", logicS);
   1.102 +    val T =
   1.103 +      if_none (Sign.const_type sg c) (aT --> propT)
   1.104 +      |> Term.map_type_tvar (fn ((x, _), S) => TFree (x, S));
   1.105 +    val U = Term.domain_type T handle Match => aT;
   1.106 +  in Const (c, T) $ Free (x, U) end;
   1.107 +
   1.108 +
   1.109 +
   1.110 +(** treatment of meta-level connectives **)
   1.111 +
   1.112 +(* maintain rules *)
   1.113 +
   1.114 +val get_atomize = #1 o #2 o ObjectLogicData.get_sg;
   1.115 +val get_rulify = #2 o #2 o ObjectLogicData.get_sg;
   1.116 +
   1.117 +val add_atomize = ObjectLogicData.map o Library.apsnd o Library.apfst o Drule.add_rules;
   1.118 +val add_rulify = ObjectLogicData.map o Library.apsnd o Library.apsnd o Drule.add_rules;
   1.119 +
   1.120 +fun declare_atomize (thy, th) = (add_atomize [th] thy, th);
   1.121 +fun declare_rulify (thy, th) = (add_rulify [th] thy, th);
   1.122 +
   1.123 +
   1.124 +(* atomize *)
   1.125 +
   1.126 +fun rewrite_prems_tac rews i = PRIMITIVE (MetaSimplifier.fconv_rule
   1.127 +  (MetaSimplifier.goals_conv (Library.equal i)
   1.128 +    (MetaSimplifier.forall_conv
   1.129 +      (MetaSimplifier.goals_conv (K true) (Tactic.rewrite true rews)))));
   1.130 +
   1.131 +fun atomize_tac i st =
   1.132 +  if Logic.has_meta_prems (#prop (Thm.rep_thm st)) i then
   1.133 +    (rewrite_prems_tac (get_atomize (Thm.sign_of_thm st)) i) st
   1.134 +  else all_tac st;
   1.135 +
   1.136 +fun atomize_goal i st =
   1.137 +  (case Seq.pull (atomize_tac i st) of None => st | Some (st', _) => st');
   1.138 +
   1.139 +
   1.140 +(* rulify *)
   1.141 +
   1.142 +fun gen_rulify full thm =
   1.143 +  Tactic.simplify full (get_rulify (Thm.sign_of_thm thm)) thm
   1.144 +  |> Drule.forall_elim_vars_safe |> Drule.strip_shyps_warning |> Drule.zero_var_indexes;
   1.145 +
   1.146 +val rulify = gen_rulify true;
   1.147 +val rulify_no_asm = gen_rulify false;
   1.148 +
   1.149 +fun rule_format x = Drule.rule_attribute (fn _ => rulify) x;
   1.150 +fun rule_format_no_asm x = Drule.rule_attribute (fn _ => rulify_no_asm) x;
   1.151 +
   1.152 +
   1.153 +
   1.154 +(** theory setup **)
   1.155 +
   1.156 +val setup = [ObjectLogicData.init];
   1.157 +
   1.158 +
   1.159 +end;
     2.1 --- a/src/Pure/object_logic.ML	Mon Oct 22 18:07:30 2001 +0200
     2.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.3 @@ -1,156 +0,0 @@
     2.4 -(*  Title:      Pure/object_logic.ML
     2.5 -    ID:         $Id$
     2.6 -    Author:     Markus Wenzel, TU Muenchen
     2.7 -    License:    GPL (GNU GENERAL PUBLIC LICENSE)
     2.8 -
     2.9 -Specifics about common object-logics.
    2.10 -*)
    2.11 -
    2.12 -signature OBJECT_LOGIC =
    2.13 -sig
    2.14 -  val add_judgment: bstring * string * mixfix -> theory -> theory
    2.15 -  val add_judgment_i: bstring * typ * mixfix -> theory -> theory
    2.16 -  val judgment_name: Sign.sg -> string
    2.17 -  val is_judgment: Sign.sg -> term -> bool
    2.18 -  val drop_judgment: Sign.sg -> term -> term
    2.19 -  val fixed_judgment: Sign.sg -> string -> term
    2.20 -  val declare_atomize: theory attribute
    2.21 -  val declare_rulify: theory attribute
    2.22 -  val atomize_tac: int -> tactic
    2.23 -  val atomize_goal: int -> thm -> thm
    2.24 -  val rulify: thm -> thm
    2.25 -  val rulify_no_asm: thm -> thm
    2.26 -  val rule_format: 'a attribute
    2.27 -  val rule_format_no_asm: 'a attribute
    2.28 -  val setup: (theory -> theory) list
    2.29 -end;
    2.30 -
    2.31 -structure ObjectLogic: OBJECT_LOGIC =
    2.32 -struct
    2.33 -
    2.34 -
    2.35 -(** object-logic theory data **)
    2.36 -
    2.37 -(* data kind 'Pure/object-logic' *)
    2.38 -
    2.39 -structure ObjectLogicDataArgs =
    2.40 -struct
    2.41 -  val name = "Pure/object-logic";
    2.42 -  type T = string option * (thm list * thm list);
    2.43 -
    2.44 -  val empty = (None, ([], [Drule.norm_hhf_eq]));
    2.45 -  val copy = I;
    2.46 -  val prep_ext = I;
    2.47 -
    2.48 -  fun merge_judgment (Some x, Some y) =
    2.49 -        if x = y then Some x else error "Attempt to merge different object-logics"
    2.50 -    | merge_judgment (j1, j2) = if is_some j1 then j1 else j2;
    2.51 -
    2.52 -  fun merge ((judgment1, (atomize1, rulify1)), (judgment2, (atomize2, rulify2))) =
    2.53 -    (merge_judgment (judgment1, judgment2),
    2.54 -      (Drule.merge_rules (atomize1, atomize2), Drule.merge_rules (rulify1, rulify2)));
    2.55 -
    2.56 -  fun print _ _ = ();
    2.57 -end;
    2.58 -
    2.59 -structure ObjectLogicData = TheoryDataFun(ObjectLogicDataArgs);
    2.60 -
    2.61 -
    2.62 -(** generic treatment of judgments -- with a single argument only **)
    2.63 -
    2.64 -(* add_judgment(_i) *)
    2.65 -
    2.66 -local
    2.67 -
    2.68 -fun new_judgment name (None, rules) = (Some name, rules)
    2.69 -  | new_judgment _ (Some _, _) = error "Attempt to redeclare object-logic judgment";
    2.70 -
    2.71 -fun gen_add_judgment add_consts (name, T, syn) thy =
    2.72 -  thy
    2.73 -  |> add_consts [(name, T, syn)]
    2.74 -  |> ObjectLogicData.map (new_judgment (Sign.full_name (Theory.sign_of thy) name));
    2.75 -
    2.76 -in
    2.77 -
    2.78 -val add_judgment = gen_add_judgment Theory.add_consts;
    2.79 -val add_judgment_i = gen_add_judgment Theory.add_consts_i;
    2.80 -
    2.81 -end;
    2.82 -
    2.83 -
    2.84 -(* term operations *)
    2.85 -
    2.86 -fun judgment_name sg =
    2.87 -  (case ObjectLogicData.get_sg sg of
    2.88 -    (Some name, _) => name
    2.89 -  | _ => raise TERM ("Unknown object-logic judgment", []));
    2.90 -
    2.91 -fun is_judgment sg (Const (c, _) $ _) = c = judgment_name sg
    2.92 -  | is_judgment _ _ = false;
    2.93 -
    2.94 -fun drop_judgment sg (Abs (x, T, t)) = Abs (x, T, drop_judgment sg t)
    2.95 -  | drop_judgment sg (tm as (Const (c, _) $ t)) = if c = judgment_name sg then t else tm
    2.96 -  | drop_judgment _ tm = tm;
    2.97 -
    2.98 -fun fixed_judgment sg x =
    2.99 -  let  (*be robust wrt. low-level errors*)
   2.100 -    val c = judgment_name sg;
   2.101 -    val aT = TFree ("'a", logicS);
   2.102 -    val T =
   2.103 -      if_none (Sign.const_type sg c) (aT --> propT)
   2.104 -      |> Term.map_type_tvar (fn ((x, _), S) => TFree (x, S));
   2.105 -    val U = Term.domain_type T handle Match => aT;
   2.106 -  in Const (c, T) $ Free (x, U) end;
   2.107 -
   2.108 -
   2.109 -
   2.110 -(** treatment of meta-level connectives **)
   2.111 -
   2.112 -(* maintain rules *)
   2.113 -
   2.114 -val get_atomize = #1 o #2 o ObjectLogicData.get_sg;
   2.115 -val get_rulify = #2 o #2 o ObjectLogicData.get_sg;
   2.116 -
   2.117 -val add_atomize = ObjectLogicData.map o Library.apsnd o Library.apfst o Drule.add_rules;
   2.118 -val add_rulify = ObjectLogicData.map o Library.apsnd o Library.apsnd o Drule.add_rules;
   2.119 -
   2.120 -fun declare_atomize (thy, th) = (add_atomize [th] thy, th);
   2.121 -fun declare_rulify (thy, th) = (add_rulify [th] thy, th);
   2.122 -
   2.123 -
   2.124 -(* atomize *)
   2.125 -
   2.126 -fun rewrite_prems_tac rews i = PRIMITIVE (MetaSimplifier.fconv_rule
   2.127 -  (MetaSimplifier.goals_conv (Library.equal i)
   2.128 -    (MetaSimplifier.forall_conv
   2.129 -      (MetaSimplifier.goals_conv (K true) (Tactic.rewrite true rews)))));
   2.130 -
   2.131 -fun atomize_tac i st =
   2.132 -  if Logic.has_meta_prems (#prop (Thm.rep_thm st)) i then
   2.133 -    (rewrite_prems_tac (get_atomize (Thm.sign_of_thm st)) i) st
   2.134 -  else all_tac st;
   2.135 -
   2.136 -fun atomize_goal i st =
   2.137 -  (case Seq.pull (atomize_tac i st) of None => st | Some (st', _) => st');
   2.138 -
   2.139 -
   2.140 -(* rulify *)
   2.141 -
   2.142 -fun gen_rulify full thm =
   2.143 -  Tactic.simplify full (get_rulify (Thm.sign_of_thm thm)) thm
   2.144 -  |> Drule.forall_elim_vars_safe |> Drule.strip_shyps_warning |> Drule.zero_var_indexes;
   2.145 -
   2.146 -val rulify = gen_rulify true;
   2.147 -val rulify_no_asm = gen_rulify false;
   2.148 -
   2.149 -fun rule_format x = Drule.rule_attribute (fn _ => rulify) x;
   2.150 -fun rule_format_no_asm x = Drule.rule_attribute (fn _ => rulify_no_asm) x;
   2.151 -
   2.152 -
   2.153 -
   2.154 -(** theory setup **)
   2.155 -
   2.156 -val setup = [ObjectLogicData.init];
   2.157 -
   2.158 -
   2.159 -end;