1.1 --- a/src/Pure/isac/Isac_Mathengine.thy Fri Jul 23 10:38:58 2010 +0200
1.2 +++ b/src/Pure/isac/Isac_Mathengine.thy Mon Jul 26 15:27:06 2010 +0200
1.3 @@ -8,14 +8,14 @@
1.4 OR tty (unusable: after errors wrong toplevel):
1.5 $ cd "/home/neuper/proto2/isac/src/sml"
1.6 $ isabelle-process HOL HOL-Isac
1.7 -ML> use_thy "Isac_Mathengine";
1.8 +ML> use_thy "Isac_Mathengine";
1.9 *)
1.10
1.11 header {* Loading the isac mathengine *}
1.12
1.13 theory Isac_Mathengine
1.14 -imports Complex_Main
1.15 -(*imports Complex_Main "Scripts/Script" (*ListG, Tools, Script*)*)
1.16 +(*imports Complex_Main*)
1.17 +imports Complex_Main "Scripts/Script" (*ListG, Tools, Script*)
1.18 begin
1.19
1.20 use "library.sml"
1.21 @@ -27,13 +27,8 @@
1.22
1.23 use "Scripts/rewrite.sml"
1.24 use_thy"Scripts/Script"
1.25 +use "Scripts/scrtools.sml"
1.26 (*
1.27 -use "Scripts/ListG.ML"
1.28 -use "Scripts/Tools.ML"
1.29 -use "Scripts/Script.ML"
1.30 -
1.31 -use "Scripts/scrtools.sml"
1.32 -
1.33 use "ME/mstools.sml"
1.34 use "ME/ctree.sml"
1.35 use "ME/ptyps.sml"
2.1 --- a/src/Pure/isac/Scripts/ListG.thy Fri Jul 23 10:38:58 2010 +0200
2.2 +++ b/src/Pure/isac/Scripts/ListG.thy Mon Jul 26 15:27:06 2010 +0200
2.3 @@ -6,6 +6,8 @@
2.4 W.N. 8.01
2.5 attaches identifiers to definition of listfuns,
2.6 for storing them in list_rls
2.7 +
2.8 +WN.29.4.03:
2.9 *)
2.10
2.11 theory ListG
2.12 @@ -14,18 +16,18 @@
2.13 ("Scripts/term_G.sml")("Scripts/calculate.sml")
2.14 ("Scripts/rewrite.sml")
2.15 begin
2.16 -use "library.sml"
2.17 -use "calcelems.sml"
2.18 -use "Scripts/term_G.sml"
2.19 -use "Scripts/calculate.sml"
2.20 -use "Scripts/rewrite.sml"
2.21 +use "library.sml" (*indent,...*)
2.22 +use "calcelems.sml" (*str_of_type, Thm,...*)
2.23 +use "Scripts/term_G.sml" (*num_str,...*)
2.24 +use "Scripts/calculate.sml" (*???*)
2.25 +use "Scripts/rewrite.sml" (*?*** At command "end" (line 205../ListG.thy*)
2.26
2.27 text {* 'nat' in List.thy replaced by 'real' *}
2.28
2.29 primrec length_' :: "'a list => real"
2.30 where
2.31 - length_Nil_': "length_' [] = 0" (*length: 'a list => nat*)
2.32 -| length_Cons_': "length_' (x#xs) = 1 + length_' xs"
2.33 + LENGTH_NIL: "length_' [] = 0" (*length: 'a list => nat*)
2.34 +| LENGTH_CONS: "length_' (x#xs) = 1 + length_' xs"
2.35
2.36 primrec del :: "['a list, 'a] => 'a list"
2.37 where
2.38 @@ -40,14 +42,13 @@
2.39 consts nth_' :: "[real, 'a list] => 'a"
2.40 axioms
2.41 (*** more than one non-variable in pattern in "nth_ 1 [x] = x"--*)
2.42 - nth_Nil_': "nth_' 1 (x#xs) = x"
2.43 -(* nth_Cons_': "nth_' n (x#xs) = nth_' (n+ -1) xs" *)
2.44 + NTH_NIL: "nth_' 1 (x#xs) = x"
2.45 +(* NTH_CONS: "nth_' n (x#xs) = nth_' (n+ -1) xs" *)
2.46
2.47 (*rewriter does not reach base case ...... ;
2.48 the condition involves another rule set (erls, eval_binop in Atools):*)
2.49 - nth_Cons_': "1 < n ==> nth_' n (x#xs) = nth_' (n+ - 1) xs"
2.50 + NTH_CONS: "1 < n ==> nth_' n (x#xs) = nth_' (n+ - 1) xs"
2.51
2.52 -axioms
2.53 (*primrec from Isabelle/src/HOL/List.thy -- def.twice not allowed*)
2.54 (*primrec*)
2.55 hd_thm: "hd(x#xs) = x"
2.56 @@ -58,7 +59,7 @@
2.57 null_Nil: "null([]) = True"
2.58 null_Cons: "null(x#xs) = False"
2.59 (*primrec*)
2.60 - last_thm: "last(x#xs) = (if xs=[] then x else last xs)"
2.61 + LAST: "last(x#xs) = (if xs=[] then x else last xs)"
2.62 (*primrec*)
2.63 butlast_Nil: "butlast [] = []"
2.64 butlast_Cons: "butlast(x#xs) = (if xs=[] then [] else x#butlast xs)"
2.65 @@ -144,18 +145,7 @@
2.66
2.67 (** Lexicographic orderings on lists ...!!!**)
2.68
2.69 -
2.70 -ML{* @{thm o_apply} *}
2.71 -ML{* val list_rls =
2.72 - Rls{id="list_rls",preconds = [], rew_ord = ("dummy_ord",dummy_ord),
2.73 - erls = e_rls, srls = Erls, calc = [], (*asm_thm=[],*)
2.74 - rules = (*8.01: copied from*)
2.75 - [Thm ("refl", num_str refl), (*'a<>b -> FALSE' by fun eval_equal*)
2.76 - Thm ("append_Cons",num_str @{thm append_Cons})
2.77 - ], scr = EmptyScr}:rls;
2.78 - *}
2.79 -(*
2.80 -ML{*
2.81 +ML{* (*the former ListG.ML*)
2.82 (** rule set for evaluating listexpr in scripts **)
2.83 val list_rls =
2.84 Rls{id="list_rls",preconds = [], rew_ord = ("dummy_ord",dummy_ord),
2.85 @@ -164,8 +154,8 @@
2.86 [Thm ("refl", num_str refl), (*'a<>b -> FALSE' by fun eval_equal*)
2.87 Thm ("o_apply", num_str @{thm o_apply}),
2.88
2.89 - Thm ("nth_Cons_",num_str @{thm nth_Cons_}),(*erls for cond. in Atools.ML*)
2.90 - Thm ("nth_Nil_",num_str @{thm nth_Nil_}),
2.91 + Thm ("NTH_CONS",num_str @{thm NTH_CONS}),(*erls for cond. in Atools.ML*)
2.92 + Thm ("NTH_NIL",num_str @{thm NTH_NIL}),
2.93 Thm ("append_Cons",num_str @{thm append_Cons}),
2.94 Thm ("append_Nil",num_str @{thm append_Nil}),
2.95 Thm ("butlast_Cons",num_str @{thm butlast_Cons}),
2.96 @@ -184,9 +174,9 @@
2.97 Thm ("foldr_Cons",num_str @{thm foldr_Cons}),
2.98 Thm ("foldr_Nil",num_str @{thm foldr_Nil}),
2.99 Thm ("hd_thm",num_str @{thm hd_thm}),
2.100 - Thm ("last_thm",num_str @{thm last_thm}),
2.101 - Thm ("length_Cons_",num_str @{thm length_Cons_}),
2.102 - Thm ("length_Nil_",num_str @{thm length_Nil_}),
2.103 + Thm ("LAST",num_str @{thm LAST}),
2.104 + Thm ("LENGTH_CONS",num_str @{thm LENGTH_CONS}),
2.105 + Thm ("LENGTH_NIL",num_str @{thm LENGTH_NIL}),
2.106 Thm ("list_diff_def",num_str @{thm list_diff_def}),
2.107 Thm ("map_Cons",num_str @{thm map_Cons}),
2.108 Thm ("map_Nil",num_str @{thm map_Cons}),
2.109 @@ -205,10 +195,11 @@
2.110 Thm ("zip_Cons",num_str @{thm zip_Cons}),
2.111 Thm ("zip_Nil",num_str @{thm zip_Nil})
2.112 ], scr = EmptyScr}:rls;
2.113 +*}
2.114
2.115 -ruleset' := overwritelthy thy (!ruleset',
2.116 +ML{*
2.117 +ruleset' := overwritelthy @{theory} (!ruleset',
2.118 [("list_rls",list_rls)
2.119 ]);
2.120 *}
2.121 -*)
2.122 end
3.1 --- a/src/Pure/isac/Scripts/Script.thy Fri Jul 23 10:38:58 2010 +0200
3.2 +++ b/src/Pure/isac/Scripts/Script.thy Mon Jul 26 15:27:06 2010 +0200
3.3 @@ -65,6 +65,7 @@
3.4 Repeat :: "['a => 'a, 'a] => 'a"
3.5 Or :: "['a => 'a, 'a => 'a, 'a] => 'a" (infixr "Or" 10)
3.6 While :: "[bool, 'a => 'a, 'a] => 'a" ("((While (_) Do)//(_))" 9)
3.7 +(*WN100723 because of "Error in syntax translation" below...
3.8 (*'b => bool doesn't work with "contains_root _"*)
3.9 Letpar :: "['a, 'a => 'b] => 'b"
3.10 (*--- defined in Isabelle/scr/HOL/HOL.thy:
3.11 @@ -73,8 +74,7 @@
3.12 If :: "[bool, 'a, 'a] => 'a" ("(if (_)/ then (_)/ else (_))" 10)
3.13 %x. P x .. lambda is defined in Isabelles meta logic
3.14 --- *)
3.15 -
3.16 -
3.17 +*)
3.18 failtac :: 'a
3.19 idletac :: 'a
3.20 (*... + RECORD IN 'screxpr' in Script.ML *)
3.21 @@ -133,6 +133,7 @@
3.22 (*... + RECORD IN 'subpbls' in Script.ML *)
3.23 (*SHIFT -> resp.thys ----^^^----------------------------*)
3.24
3.25 +(*Makarius 10.03
3.26 syntax
3.27
3.28 "_Letpar" :: "[letbinds, 'a] => 'a" ("(letpar (_)/ in (_))" 10)
3.29 @@ -141,5 +142,13 @@
3.30
3.31 "_Letpar (_binds b bs) e" == "_Letpar b (_Letpar bs e)"
3.32 "letpar x = a in e" == "Letpar a (%x. e)"
3.33 +*** Error in syntax translation rule: rhs contains extra variables
3.34 +*** ("_Letpar" ("_bind" x a) e) -> (Letpar a ("_abs" x e))
3.35 +*** At command "translations" (line 140 of "/usr/local/isabisac/src/Pure/isac/Scripts/Script.thy").
3.36 +*)
3.37 +
3.38 +ML{* (*the former Script.ML*)
3.39 +
3.40 +*}
3.41
3.42 end
4.1 --- a/src/Pure/isac/Scripts/Tools.thy Fri Jul 23 10:38:58 2010 +0200
4.2 +++ b/src/Pure/isac/Scripts/Tools.thy Mon Jul 26 15:27:06 2010 +0200
4.3 @@ -51,4 +51,182 @@
4.4 Testvar :: "[real, 'a] => bool" (*is a variable in a term: unused 6.5.03*)
4.5 "Testvar v t == v mem (Vars t)" (*by rewriting only,no Calcunused 6.5.03*)
4.6
4.7 +ML {* (*the former Tools.ML*)
4.8 +(* auxiliary functions for scripts WN.9.00*)
4.9 +(*11.02: for equation solving only*)
4.10 +val UniversalList = (term_of o the o (parse @{theory})) "UniversalList";
4.11 +val EmptyList = (term_of o the o (parse @{theory})) "[]::bool list";
4.12 +
4.13 +(*+ for Or_to_List +*)
4.14 +fun or2list (Const ("True",_)) = (writeln"### or2list True";UniversalList)
4.15 + | or2list (Const ("False",_)) = (writeln"### or2list False";EmptyList)
4.16 + | or2list (t as Const ("op =",_) $ _ $ _) =
4.17 + (writeln"### or2list _ = _";list2isalist bool [t])
4.18 + | or2list ors =
4.19 + (writeln"### or2list _ | _";
4.20 + let fun get ls (Const ("op |",_) $ o1 $ o2) =
4.21 + case o2 of
4.22 + Const ("op |",_) $ _ $ _ => get (ls @ [o1]) o2
4.23 + | _ => ls @ [o1, o2]
4.24 + in (((list2isalist bool) o (get [])) ors)
4.25 + handle _ => raise error ("or2list: no ORs= "^(term2str ors)) end
4.26 + );
4.27 +(*>val t = HOLogic.true_const;
4.28 +> val t' = or2list t;
4.29 +> term2str t';
4.30 +"Atools.UniversalList"
4.31 +> val t = HOLogic.false_const;
4.32 +> val t' = or2list t;
4.33 +> term2str t';
4.34 +"[]"
4.35 +> val t=(term_of o the o (parse thy)) "x=3";
4.36 +> val t' = or2list t;
4.37 +> term2str t';
4.38 +"[x = 3]"
4.39 +> val t=(term_of o the o (parse thy))"(x=3) | (x=-3) | (x=0)";
4.40 +> val t' = or2list t;
4.41 +> term2str t';
4.42 +"[x = #3, x = #-3, x = #0]" : string *)
4.43 +
4.44 +
4.45 +(** evaluation on the meta-level **)
4.46 +
4.47 +(*. evaluate the predicate matches (match on whole term only) .*)
4.48 +(*("matches",("Tools.matches",eval_matches "#matches_")):calc*)
4.49 +fun eval_matches (thmid:string) "Tools.matches"
4.50 + (t as Const ("Tools.matches",_) $ pat $ tst) thy =
4.51 + if matches thy tst pat
4.52 + then let val prop = Trueprop $ (mk_equality (t, true_as_term))
4.53 + in SOME (Syntax.string_of_term @{context} prop, prop) end
4.54 + else let val prop = Trueprop $ (mk_equality (t, false_as_term))
4.55 + in SOME (Syntax.string_of_term @{context} prop, prop) end
4.56 + | eval_matches _ _ _ _ = NONE;
4.57 +(*
4.58 +> val t = (term_of o the o (parse thy))
4.59 + "matches (?x = 0) (1 * x ^^^ 2 = 0)";
4.60 +> eval_matches "/thmid/" "/op_/" t thy;
4.61 +val it =
4.62 + SOME
4.63 + ("matches (x = 0) (1 * x ^^^ 2 = 0) = False",
4.64 + Const (#,#) $ (# $ # $ Const #)) : (string * term) option
4.65 +
4.66 +> val t = (term_of o the o (parse thy))
4.67 + "matches (?a = #0) (#1 * x ^^^ #2 = #0)";
4.68 +> eval_matches "/thmid/" "/op_/" t thy;
4.69 +val it =
4.70 + SOME
4.71 + ("matches (?a = #0) (#1 * x ^^^ #2 = #0) = True",
4.72 + Const (#,#) $ (# $ # $ Const #)) : (string * term) option
4.73 +
4.74 +> val t = (term_of o the o (parse thy))
4.75 + "matches (?a * x = #0) (#1 * x ^^^ #2 = #0)";
4.76 +> eval_matches "/thmid/" "/op_/" t thy;
4.77 +val it =
4.78 + SOME
4.79 + ("matches (?a * x = #0) (#1 * x ^^^ #2 = #0) = False",
4.80 + Const (#,#) $ (# $ # $ Const #)) : (string * term) option
4.81 +
4.82 +> val t = (term_of o the o (parse thy))
4.83 + "matches (?a * x ^^^ #2 = #0) (#1 * x ^^^ #2 = #0)";
4.84 +> eval_matches "/thmid/" "/op_/" t thy;
4.85 +val it =
4.86 + SOME
4.87 + ("matches (?a * x ^^^ #2 = #0) (#1 * x ^^^ #2 = #0) = True",
4.88 + Const (#,#) $ (# $ # $ Const #)) : (string * term) option
4.89 +----- before ?patterns ---:
4.90 +> val t = (term_of o the o (parse thy))
4.91 + "matches (a * b^^^#2 = c) (#3 * x^^^#2 = #1)";
4.92 +> eval_matches "/thmid/" "/op_/" t thy;
4.93 +SOME
4.94 + ("matches (a * b ^^^ #2 = c) (#3 * x ^^^ #2 = #1) = True",
4.95 + Const ("Trueprop","bool => prop") $ (Const # $ (# $ #) $ Const (#,#)))
4.96 + : (string * term) option
4.97 +
4.98 +> val t = (term_of o the o (parse thy))
4.99 + "matches (a * b^^^#2 = c) (#3 * x^^^#2222 = #1)";
4.100 +> eval_matches "/thmid/" "/op_/" t thy;
4.101 +SOME ("matches (a * b ^^^ #2 = c) (#3 * x ^^^ #2222 = #1) = False",
4.102 + Const ("Trueprop","bool => prop") $ (Const # $ (# $ #) $ Const (#,#)))
4.103 +
4.104 +> val t = (term_of o the o (parse thy))
4.105 + "matches (a = b) (x + #1 + #-1 * #2 = #0)";
4.106 +> eval_matches "/thmid/" "/op_/" t thy;
4.107 +SOME ("matches (a = b) (x + #1 + #-1 * #2 = #0) = True",Const # $ (# $ #))
4.108 +*)
4.109 +
4.110 +(*.does a pattern match some subterm ?.*)
4.111 +fun matchsub thy t pat =
4.112 + let fun matchs (t as Const _) = matches thy t pat
4.113 + | matchs (t as Free _) = matches thy t pat
4.114 + | matchs (t as Var _) = matches thy t pat
4.115 + | matchs (Bound _) = false
4.116 + | matchs (t as Abs (_, _, body)) =
4.117 + if matches thy t pat then true else matches thy body pat
4.118 + | matchs (t as f1 $ f2) =
4.119 + if matches thy t pat then true
4.120 + else if matchs f1 then true else matchs f2
4.121 + in matchs t end;
4.122 +
4.123 +(*("matchsub",("Tools.matchsub",eval_matchsub "#matchsub_")):calc*)
4.124 +fun eval_matchsub (thmid:string) "Tools.matchsub"
4.125 + (t as Const ("Tools.matchsub",_) $ pat $ tst) thy =
4.126 + if matchsub thy tst pat
4.127 + then let val prop = Trueprop $ (mk_equality (t, true_as_term))
4.128 + in SOME (Syntax.string_of_term @{context} prop, prop) end
4.129 + else let val prop = Trueprop $ (mk_equality (t, false_as_term))
4.130 + in SOME (Syntax.string_of_term @{context} prop, prop) end
4.131 + | eval_matchsub _ _ _ _ = NONE;
4.132 +
4.133 +(*get the variables in an isabelle-term*)
4.134 +(*("Vars" ,("Tools.Vars" ,eval_var "#Vars_")):calc*)
4.135 +fun eval_var (thmid:string) "Tools.Vars"
4.136 + (t as (Const(op0,t0) $ arg)) thy =
4.137 + let
4.138 + val t' = ((list2isalist HOLogic.realT) o vars) t;
4.139 + val thmId = thmid^(Syntax.string_of_term @{context} arg);
4.140 + in SOME (thmId, Trueprop $ (mk_equality (t,t'))) end
4.141 + | eval_var _ _ _ _ = NONE;
4.142 +
4.143 +fun lhs (Const ("op =",_) $ l $ _) = l
4.144 + | lhs t = error("lhs called with (" ^ term2str t ^ ")");
4.145 +(*("lhs" ,("Tools.lhs" ,eval_lhs "")):calc*)
4.146 +fun eval_lhs _ "Tools.lhs"
4.147 + (t as (Const ("Tools.lhs",_) $ (Const ("op =",_) $ l $ _))) _ =
4.148 + SOME ((term2str t) ^ " = " ^ (term2str l),
4.149 + Trueprop $ (mk_equality (t, l)))
4.150 + | eval_lhs _ _ _ _ = NONE;
4.151 +(*
4.152 +> val t = (term_of o the o (parse thy)) "lhs (1 * x ^^^ 2 = 0)";
4.153 +> val SOME (id,t') = eval_lhs 0 0 t 0;
4.154 +val id = "Tools.lhs (1 * x ^^^ 2 = 0) = 1 * x ^^^ 2" : string
4.155 +> term2str t';
4.156 +val it = "Tools.lhs (1 * x ^^^ 2 = 0) = 1 * x ^^^ 2" : string
4.157 +*)
4.158 +
4.159 +fun rhs (Const ("op =",_) $ _ $ r) = r
4.160 + | rhs t = error("rhs called with (" ^ term2str t ^ ")");
4.161 +(*("rhs" ,("Tools.rhs" ,eval_rhs "")):calc*)
4.162 +fun eval_rhs _ "Tools.rhs"
4.163 + (t as (Const ("Tools.rhs",_) $ (Const ("op =",_) $ _ $ r))) _ =
4.164 + SOME ((term2str t) ^ " = " ^ (term2str r),
4.165 + Trueprop $ (mk_equality (t, r)))
4.166 + | eval_rhs _ _ _ _ = NONE;
4.167 +
4.168 +
4.169 +(*for evaluating scripts*)
4.170 +
4.171 +val list_rls = append_rls "list_rls" list_rls
4.172 + [Calc ("Tools.rhs",eval_rhs "")];
4.173 +ruleset' := overwritelthy @{theory} (!ruleset',
4.174 + [("list_rls",list_rls)
4.175 + ]);
4.176 +calclist':= overwritel (!calclist',
4.177 + [("matches",("Tools.matches",eval_matches "#matches_")),
4.178 + ("matchsub",("Tools.matchsub",eval_matchsub "#matchsub_")),
4.179 + ("Vars" ,("Tools.Vars" ,eval_var "#Vars_")),
4.180 + ("lhs" ,("Tools.lhs" ,eval_lhs "")),
4.181 + ("rhs" ,("Tools.rhs" ,eval_rhs ""))
4.182 + ]);
4.183 +
4.184 +*}
4.185 end
5.1 --- a/src/Pure/isac/Scripts/scrtools.sml Fri Jul 23 10:38:58 2010 +0200
5.2 +++ b/src/Pure/isac/Scripts/scrtools.sml Mon Jul 26 15:27:06 2010 +0200
5.3 @@ -122,12 +122,12 @@
5.4 (*make the term 'Subproblem (domID, pblID)' to a formula for frontend;
5.5 needs to be here after def. Subproblem in Script.thy*)
5.6 val t as (subpbl_t $ (pair_t $ Free (domID,_) $ pblID)) =
5.7 - (term_of o the o (parse Script.thy))
5.8 + (term_of o the o (parse @{theory Script}))
5.9 "Subproblem (Isac,[equation,univar])";
5.10 val t as (pbl_t $ _) =
5.11 - (term_of o the o (parse Script.thy))
5.12 + (term_of o the o (parse @{theory Script}))
5.13 "Problem (Isac,[equation,univar])";
5.14 -val Free (_, ID_type) = (term_of o the o (parse Script.thy)) "x::ID";
5.15 +val Free (_, ID_type) = (term_of o the o (parse @{theory Script})) "x::ID";
5.16
5.17
5.18 fun subpbl domID pblID =
5.19 @@ -158,10 +158,10 @@
5.20 v current value, is attached to curried stactics
5.21 stac stactic to be instantiated
5.22 precond:
5.23 - not (a = None) /\ (v = e_term) /\ (stac curried, i.e. without last arg.)
5.24 + not (a = NONE) /\ (v = e_term) /\ (stac curried, i.e. without last arg.)
5.25 this ........................ is the initialization for assy with l=[],
5.26 but the 1st stac is
5.27 - (a) curried: then (a = Some _), or
5.28 + (a) curried: then (a = SOME _), or
5.29 (b) not curried: then the values of the initialization are not used
5.30 .*)
5.31 datatype stacexpr = STac of term | Expr of term
5.32 @@ -182,82 +182,82 @@
5.33 a leaf is either a tactic or an 'exp' in 'let v = expr'
5.34 where 'exp' does not contain a tactic.
5.35 CAUTION: (1) currying with @@ requires 2 patterns for each tactic
5.36 - (2) the non-curried version must return None for a
5.37 + (2) the non-curried version must return NONE for a
5.38 (3) non-matching patterns become an Expr by fall-through.
5.39 WN060906 quick and dirty fix: due to (2) a is returned, too.*)
5.40 fun subst_stacexpr E a v (t as (Const ("Script.Rewrite",_) $ _ $ _ $ _ ))=
5.41 - (None, STac (subst_atomic E t))
5.42 + (NONE, STac (subst_atomic E t))
5.43
5.44 | subst_stacexpr E a v (t as (Const ("Script.Rewrite",_) $ _ $ _ ))=
5.45 - (a, (*in these cases we hope, that a = Some _*)
5.46 - STac (case a of Some a' => (subst_atomic E (t $ a'))
5.47 - | None => ((subst_atomic E t) $ v)))
5.48 + (a, (*in these cases we hope, that a = SOME _*)
5.49 + STac (case a of SOME a' => (subst_atomic E (t $ a'))
5.50 + | NONE => ((subst_atomic E t) $ v)))
5.51
5.52 | subst_stacexpr E a v
5.53 (t as (Const ("Script.Rewrite'_Inst",_) $ _ $ _ $ _ $ _ )) =
5.54 - (None, STac (subst_atomic E t))
5.55 + (NONE, STac (subst_atomic E t))
5.56
5.57 | subst_stacexpr E a v (t as (Const ("Script.Rewrite'_Inst",_) $ _ $ _ $ _))=
5.58 - (a, STac (case a of Some a' => subst_atomic E (t $ a')
5.59 - | None => ((subst_atomic E t) $ v)))
5.60 + (a, STac (case a of SOME a' => subst_atomic E (t $ a')
5.61 + | NONE => ((subst_atomic E t) $ v)))
5.62
5.63 | subst_stacexpr E a v (t as (Const ("Script.Rewrite'_Set",_) $ _ $ _ $ _ ))=
5.64 - (None, STac (subst_atomic E t))
5.65 + (NONE, STac (subst_atomic E t))
5.66
5.67 | subst_stacexpr E a v (t as (Const ("Script.Rewrite'_Set",_) $ _ $ _ )) =
5.68 - (a, STac (case a of Some a' => subst_atomic E (t $ a')
5.69 - | None => ((subst_atomic E t) $ v)))
5.70 + (a, STac (case a of SOME a' => subst_atomic E (t $ a')
5.71 + | NONE => ((subst_atomic E t) $ v)))
5.72
5.73 | subst_stacexpr E a v
5.74 (t as (Const ("Script.Rewrite'_Set'_Inst",_) $ _ $ _ $ _ $ _ )) =
5.75 - (None, STac (subst_atomic E t))
5.76 + (NONE, STac (subst_atomic E t))
5.77
5.78 | subst_stacexpr E a v
5.79 (t as (Const ("Script.Rewrite'_Set'_Inst",_) $ _ $ _ $ _ )) =
5.80 - (a, STac (case a of Some a' => subst_atomic E (t $ a')
5.81 - | None => ((subst_atomic E t) $ v)))
5.82 + (a, STac (case a of SOME a' => subst_atomic E (t $ a')
5.83 + | NONE => ((subst_atomic E t) $ v)))
5.84
5.85 | subst_stacexpr E a v (t as (Const ("Script.Calculate",_) $ _ $ _ )) =
5.86 - (None, STac (subst_atomic E t))
5.87 + (NONE, STac (subst_atomic E t))
5.88
5.89 | subst_stacexpr E a v (t as (Const ("Script.Calculate",_) $ _ )) =
5.90 - (a, STac (case a of Some a' => subst_atomic E (t $ a')
5.91 - | None => ((subst_atomic E t) $ v)))
5.92 + (a, STac (case a of SOME a' => subst_atomic E (t $ a')
5.93 + | NONE => ((subst_atomic E t) $ v)))
5.94
5.95 | subst_stacexpr E a v
5.96 (t as (Const("Script.Check'_elementwise",_) $ _ $ _ )) =
5.97 - (None, STac (subst_atomic E t))
5.98 + (NONE, STac (subst_atomic E t))
5.99
5.100 | subst_stacexpr E a v (t as (Const("Script.Check'_elementwise",_) $ _ )) =
5.101 - (a, STac (case a of Some a' => subst_atomic E (t $ a')
5.102 - | None => ((subst_atomic E t) $ v)))
5.103 + (a, STac (case a of SOME a' => subst_atomic E (t $ a')
5.104 + | NONE => ((subst_atomic E t) $ v)))
5.105
5.106 | subst_stacexpr E a v (t as (Const("Script.Or'_to'_List",_) $ _ )) =
5.107 - (None, STac (subst_atomic E t))
5.108 + (NONE, STac (subst_atomic E t))
5.109
5.110 | subst_stacexpr E a v (t as (Const("Script.Or'_to'_List",_))) = (*t $ v*)
5.111 - (a, STac (case a of Some a' => subst_atomic E (t $ a')
5.112 - | None => ((subst_atomic E t) $ v)))
5.113 + (a, STac (case a of SOME a' => subst_atomic E (t $ a')
5.114 + | NONE => ((subst_atomic E t) $ v)))
5.115
5.116 | subst_stacexpr E a v (t as (Const ("Script.SubProblem",_) $ _ $ _ )) =
5.117 - (None, STac (subst_atomic E t))
5.118 + (NONE, STac (subst_atomic E t))
5.119
5.120 | subst_stacexpr E a v (t as (Const ("Script.Take",_) $ _ )) =
5.121 - (None, STac (subst_atomic E t))
5.122 + (NONE, STac (subst_atomic E t))
5.123
5.124 | subst_stacexpr E a v (t as (Const ("Script.Substitute",_) $ _ $ _ )) =
5.125 - (None, STac (subst_atomic E t))
5.126 + (NONE, STac (subst_atomic E t))
5.127
5.128 | subst_stacexpr E a v (t as (Const ("Script.Substitute",_) $ _ )) =
5.129 - (a, STac (case a of Some a' => subst_atomic E (t $ a')
5.130 - | None => ((subst_atomic E t) $ v)))
5.131 + (a, STac (case a of SOME a' => subst_atomic E (t $ a')
5.132 + | NONE => ((subst_atomic E t) $ v)))
5.133
5.134 (*now all tactics are matched out and this leaf must be without a tactic*)
5.135 | subst_stacexpr E a v t =
5.136 - (a, Expr (subst_atomic (case a of Some a => upd_env E (a,v)
5.137 - | None => E) t));
5.138 + (a, Expr (subst_atomic (case a of SOME a => upd_env E (a,v)
5.139 + | NONE => E) t));
5.140 (*> val t = str2term "SubProblem(Test_, [linear, univariate, equation, test], [Test, solve_linear]) [bool_ e_, real_ v_]";
5.141 -> subst_stacexpr [] None e_term t;*)
5.142 +> subst_stacexpr [] NONE e_term t;*)
5.143
5.144
5.145 fun stacpbls (h $ body) =
5.146 @@ -279,7 +279,7 @@
5.147 (scan ts e1) @ (scan ts e2)
5.148 | scan ts (Const ("Script.Seq",_) $e1 $ e2) =
5.149 (scan ts e1) @ (scan ts e2)
5.150 - | scan ts t = case subst_stacexpr [] None e_term t of
5.151 + | scan ts t = case subst_stacexpr [] NONE e_term t of
5.152 (_, STac _) => [t] | (_, Expr _) => []
5.153 in (distinct o (scan [])) body end;
5.154 (*sc = Solve_root_equation ...
5.155 @@ -301,9 +301,7 @@
5.156 fun op_of_calc (Const ("Script.Calculate",_) $ Free (op_,_)) = op_
5.157 | op_of_calc (Const ("Script.Calculate",_) $ Free (op_,_) $ _) = op_
5.158 | op_of_calc t = raise error ("op_of_calc called with"^term2str t);
5.159 -
5.160 -(*######################################################################
5.161 -
5.162 +(*
5.163 val Script sc = (#scr o rep_rls) Test_simplify;
5.164 val stacs = stacpbls sc;
5.165
5.166 @@ -313,58 +311,74 @@
5.167
5.168 (((map (curry assoc1 (!calclist'))) o (map op_of_calc) o
5.169 (filter is_calc) o stacpbls) sc):calc list;
5.170 -
5.171 -######################################################################*)
5.172 +*)
5.173
5.174 (**.for automatic creation of scripts from rls.**)
5.175 -
5.176 -val ScrStep $ _ $ _ = (*'z not affected by parse: 'a --> real*)
5.177 - ((inst_abs thy) o term_of o the o (parse thy))
5.178 - "Script Stepwise (t_::'z) =\
5.179 +(* naming of identifiers in scripts ???...
5.180 +((inst_abs @{theory}) o term_of o the o (parse @{theory})) "(t::'z) = t";
5.181 +((inst_abs @{theory}) o term_of o (the:cterm option -> cterm) o
5.182 + (parse @{theory})) "(t't::'z) = t't";
5.183 +((inst_abs @{theory}) o term_of o the o (parse @{theory})) "(t_t::'z) = t_t";
5.184 +(* not accepted !!!...*)
5.185 +((inst_abs @{theory}) o term_of o the o (parse @{theory})) "(t_::'z) = t_";
5.186 +((inst_abs @{theory}) o term_of o (the:cterm option -> cterm) o
5.187 + (parse @{theory})) "(_t::'z) = _t";
5.188 +*)
5.189 +((inst_abs @{theory}) o term_of o the o (parse @{theory}))
5.190 +"Script Stepwise (t::'z) =\
5.191 \(Repeat\
5.192 \ ((Try (Repeat (Rewrite real_diff_minus False))) @@ \
5.193 \ (Try (Repeat (Rewrite real_add_commute False))) @@ \
5.194 \ (Try (Repeat (Rewrite real_mult_commute False)))) \
5.195 - \ t_)";
5.196 + \ t)";
5.197 +val ScrStep $ _ $ _ = (*'z not affected by parse: 'a --> real*)
5.198 + ((inst_abs @{theory}) o term_of o the o (parse @{theory}))
5.199 + "Script Stepwise (t::'z) =\
5.200 + \(Repeat\
5.201 + \ ((Try (Repeat (Rewrite real_diff_minus False))) @@ \
5.202 + \ (Try (Repeat (Rewrite real_add_commute False))) @@ \
5.203 + \ (Try (Repeat (Rewrite real_mult_commute False)))) \
5.204 + \ t)";
5.205 (*WN060605 script-arg (t_::'z) and "Free (t_, 'a)" at end of body
5.206 are inconsistent !!!*)
5.207 val ScrStep_inst $ Term $ Bdv $ _=(*'z not affected by parse: 'a --> real*)
5.208 - ((inst_abs thy) o term_of o the o (parse thy))
5.209 - "Script Stepwise_inst (t_::'z) (v_::real) =\
5.210 + ((inst_abs @{theory}) o term_of o the o (parse @{theory}))
5.211 + "Script Stepwise_inst (t::'z) (v::real) =\
5.212 \(Repeat\
5.213 - \ ((Try (Repeat (Rewrite_Inst [(bdv,v_)] real_diff_minus False))) @@ \
5.214 - \ (Try (Repeat (Rewrite_Inst [(bdv,v_)] real_add_commute False))) @@\
5.215 - \ (Try (Repeat (Rewrite_Inst [(bdv,v_)] real_mult_commute False)))) \
5.216 - \ t_)";
5.217 + \ ((Try (Repeat (Rewrite_Inst [(bdv,v)] real_diff_minus False))) @@ \
5.218 + \ (Try (Repeat (Rewrite_Inst [(bdv,v)] real_add_commute False))) @@\
5.219 + \ (Try (Repeat (Rewrite_Inst [(bdv,v)] real_mult_commute False)))) \
5.220 + \ t)";
5.221 val Repeat $ _ =
5.222 - ((inst_abs thy) o term_of o the o (parseN thy))
5.223 - "Repeat (Rewrite real_diff_minus False t_)";
5.224 + ((inst_abs @{theory}) o term_of o the o (parseN @{theory}))
5.225 + "Repeat (Rewrite real_diff_minus False t)";
5.226 val Try $ _ =
5.227 - ((inst_abs thy) o term_of o the o (parseN thy))
5.228 - "Try (Rewrite real_diff_minus False t_)";
5.229 + ((inst_abs @{theory}) o term_of o the o (parseN @{theory}))
5.230 + "Try (Rewrite real_diff_minus False t)";
5.231 +(*
5.232 val Cal $ _ =
5.233 - ((inst_abs thy) o term_of o the o (parseN thy))
5.234 + ((inst_abs @{theory}) o term_of o the o (parseN @{theory}))
5.235 "Calculate plus";
5.236 val Ca1 $ _ =
5.237 - ((inst_abs thy) o term_of o the o (parseN thy))
5.238 + ((inst_abs @{theory}) o term_of o the o (parseN @{theory}))
5.239 "Calculate1 plus";
5.240 -val Rew $ (Free (_,IDtype)) $ _ $ t_ =
5.241 - ((inst_abs thy) o term_of o the o (parseN thy))
5.242 - "Rewrite real_diff_minus False t_";
5.243 +val Rew $ (Free (_,IDtype)) $ _ $ t =
5.244 + ((inst_abs @{theory}) o term_of o the o (parseN @{theory}))
5.245 + "Rewrite real_diff_minus False t";
5.246 val Rew_Inst $ Subs $ _ $ _ =
5.247 - ((inst_abs thy) o term_of o the o (parseN thy))
5.248 - "Rewrite_Inst [(bdv,v_)] real_diff_minus False";
5.249 + ((inst_abs @{theory}) o term_of o the o (parseN @{theory}))
5.250 + "Rewrite_Inst [(bdv,v)] real_diff_minus False";
5.251 val Rew_Set $ _ $ _ =
5.252 - ((inst_abs thy) o term_of o the o (parseN thy))
5.253 + ((inst_abs @{theory}) o term_of o the o (parseN @{theory}))
5.254 "Rewrite_Set real_diff_minus False";
5.255 val Rew_Set_Inst $ _ $ _ $ _ =
5.256 - ((inst_abs thy) o term_of o the o (parseN thy))
5.257 - "Rewrite_Set_Inst [(bdv,v_)] real_diff_minus False";
5.258 + ((inst_abs @{theory}) o term_of o the o (parseN @{theory}))
5.259 + "Rewrite_Set_Inst [(bdv,v)] real_diff_minus False";
5.260 val SEq $ _ $ _ $ _ =
5.261 - ((inst_abs thy) o term_of o the o (parseN thy))
5.262 + ((inst_abs @{theory}) o term_of o the o (parseN @{theory}))
5.263 " ((Try (Repeat (Rewrite real_diff_minus False))) @@ \
5.264 \ (Try (Repeat (Rewrite real_add_commute False))) @@ \
5.265 - \ (Try (Repeat (Rewrite real_mult_commute False)))) t_";
5.266 + \ (Try (Repeat (Rewrite real_mult_commute False)))) t";
5.267
5.268 fun rule2stac _ (Thm (thmID, _)) =
5.269 Try $ (Repeat $ (Rew $ Free (thmID, IDtype) $ HOLogic.false_const))
5.270 @@ -478,3 +492,4 @@
5.271 (writeln o term2str) sc;
5.272 *)
5.273
5.274 +----bootstrapping---*)
6.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
6.2 +++ b/src/Pure/isac/smltest/Pure/General/Basics.thy Mon Jul 26 15:27:06 2010 +0200
6.3 @@ -0,0 +1,38 @@
6.4 +(* Title: ~~~/isac/smltest/Pure/General/Basics.thy
6.5 + Author: Walther Neuper, TU Graz
6.6 +
6.7 +$ cd /usr/local/Isabelle2009-1/src/Pure/isac/smltest/Pure/General
6.8 +$ /usr/local/isabisac/bin/isabelle emacs Scan.thy &
6.9 +*)
6.10 +
6.11 +header {* testing combinators from src/Pure/General/basics
6.12 + see *}
6.13 +
6.14 +theory Basics
6.15 +imports Complex_Main
6.16 +begin
6.17 +
6.18 +ML {* op |> ;
6.19 + 1 |> (fn x => x+10)
6.20 + |> (fn x => 2*x);
6.21 +(*val it = 22 : int*)
6.22 +*}
6.23 +
6.24 +ML {* op |-> ;
6.25 + fun ff c a = a + c;
6.26 + (10, 1) |-> ff
6.27 +(*val it = 11 : int*)
6.28 +*}
6.29 +
6.30 +ML {* op |>> ;
6.31 + (1, "a") |>> (fn x => x+10)
6.32 +(*val it = (11, "a") : int * string*)
6.33 +*}
6.34 +
6.35 +ML {* op ||> ;
6.36 + ("a", 1) ||> (fn x => x+10)
6.37 +(*val it = ("a", 11) : string * int*)
6.38 +*}
6.39 +
6.40 +end
6.41 +