wneuper/isa: src/Tools/isac/BaseDefinitions/BaseDefinitions.thy@02102eaa2021

     1 (* Title:  "BaseDefinitions/BaseDefinitions.thy"

     2    Author: Walther Neuper 190823

     3    (c) due to copyright terms

     5 Know_Store holds Theory_Data (problems, methods, etc) and requires respective definitions.

     6 *)

     7 theory BaseDefinitions imports Know_Store

     8 begin

     9   ML_file termC.sml

    10   ML_file substitution.sml

    11   ML_file contextC.sml

    12   ML_file environment.sml

    14 ML \<open>

    15 \<close> ML \<open>

    16 \<close> text \<open>

    17 fun string_of_atom (t as Const ("Num.numeral_class.numeral", _) $ _) = dest_numeral' t

    18 (*

    19   | string_of_atom (t as Const ("Groups.one_class.one", _)) = HOLogic.dest_numeral t

    20   | string_of_atom (t as Const ("Groups.zero_class.zero", _)) = HOLogic.dest_numeral t

    21   | string_of_atom (Const (str, _)) = str

    22   | string_of_atom (Free _) = true

    23   | string_of_atom (Var _) = true

    24   | string_of_atom _ = false;

    25 *)

    26 \<close> ML \<open>

    27 \<close> ML \<open>

    28 \<close> ML \<open>

    29 \<close> ML \<open>

    30 \<close> ML \<open>

    31 \<close> ML \<open>

    32 @{term 3}(* = Const ("Num.numeral_class.numeral", _) $ *)

    33 \<close> ML \<open>

    34 fun mk_num_op_num T1 T2 (op_, Top) n1 n2 =

    35   Const (op_, Top) $ HOLogic.mk_number T1 n1 $ HOLogic.mk_number T2 n2;

    36 \<close> ML \<open>

    37 mk_num_op_num: typ -> typ -> string * typ -> int -> int -> term

    38 \<close> ML \<open>

    39 \<close> ML \<open>

    40 (* this function only accepts the most simple monoms  vvvvvvvvvv *)

    41 fun ist_monom (Free _) = true                                                   (* 2,   a   *)

    42   | ist_monom (Const ("Groups.times_class.times", _) $

    43       (Const ("Num.numeral_class.numeral", _) $ _) $ Free _) = true

    44   | ist_monom (Const ("Groups.times_class.times", _) $                          (* 2*a, a*b *)

    45       Free _ $ (Const ("Num.numeral_class.numeral", _) $ _)) = false

    46   | ist_monom (Const ("Groups.times_class.times", _) $                          (* 3*a*b    *)

    47 		  (Const ("Groups.times_class.times", _) $

    48 			  (Const ("Num.numeral_class.numeral", _) $ _) $ Free _) $ Free _) = true

    49   | ist_monom (Const ("Transcendental.powr", _) $                               (* a^2      *)

    50       Free _ $ (Const ("Num.numeral_class.numeral", _) $ _)) = true

    51   | ist_monom (Const ("Groups.times_class.times", _) $                          (* 3*a^2    *)

    52       (Const ("Num.numeral_class.numeral", _) $ _) $

    53 		     (Const ("Transcendental.powr", _) $ Free _ $ Free _)) = true

    54   | ist_monom _ = false;

    55 \<close> ML \<open>

    56 fun varids (Const ("Num.numeral_class.numeral", _) $ _) = []

    57   | varids (Const (s, Type (_,[]))) = [strip_thy s]

    58   | varids (Free (s, Type (_,[]))) = [strip_thy s]

    59   | varids (Var((s, _),Type (_,[]))) = [strip_thy s]

    60 (*| varids (_      (s,"?DUMMY"   )) =   ..ML-error *)

    61   | varids((Const ("Bin.integ_of_bin",_)) $ _)= [](*8.01: superfluous?*)

    62   | varids (Abs (a, _, t)) = union op = [a] (varids t)

    63   | varids (t1 $ t2) = union op = (varids t1) (varids t2)

    64   | varids _ = [];

    65 \<close> ML \<open>

    66 \<close> ML \<open>

    67 \<close> ML \<open>

    68 \<close> ML \<open>

    69 \<close> ML \<open>

    70 \<close> ML \<open>

    71 \<close> ML \<open>

    72 \<close> ML \<open>

    73 \<close> ML \<open>

    74 \<close> ML \<open>

    75 \<close>

    76 end

author	wneuper <walther.neuper@jku.at>
	Tue, 13 Jul 2021 08:52:35 +0200
changeset 60320	02102eaa2021
parent 60317	638d02a9a96a
child 60322	2220bafba61f
permissions	-rw-r--r--