1.1 --- a/src/Tools/isac/ProgLang/rewrite.sml Sun Feb 25 10:19:18 2018 +0100
1.2 +++ b/src/Tools/isac/ProgLang/rewrite.sml Sun Feb 25 12:18:47 2018 +0100
1.3 @@ -267,11 +267,12 @@
1.4
1.5 (* Thm.make_thm added to Pure/thm.ML *)
1.6 fun mk_thm thy str =
1.7 - let val t = (Thm.term_of o the o (parse thy)) str
1.8 - val t' = case t of
1.9 - Const ("==>",_) $ _ $ _ => t
1.10 - | _ => Trueprop $ t
1.11 - in Thm.make_thm (Thm.global_cterm_of thy t') end;
1.12 + let
1.13 + val t = (Thm.term_of o the o (parse thy)) str
1.14 + val t' = case t of
1.15 + Const ("Pure.imp", _) $ _ $ _ => t
1.16 + | _ => Trueprop $ t
1.17 + in Thm.make_thm (Thm.global_cterm_of thy t') end;
1.18
1.19 (* "metaview" as seen from programs and from user input (both are parsed like terms presently) *)
1.20 fun convert_metaview_to_thmid thy thmid =
2.1 --- a/test/Tools/isac/ProgLang/rewrite.sml Sun Feb 25 10:19:18 2018 +0100
2.2 +++ b/test/Tools/isac/ProgLang/rewrite.sml Sun Feb 25 12:18:47 2018 +0100
2.3 @@ -592,29 +592,65 @@
2.4 "----------- fun mk_thm ------------------------------------------------------------------------";
2.5 "----------- fun mk_thm ------------------------------------------------------------------------";
2.6 "----------- fun mk_thm ------------------------------------------------------------------------";
2.7 -(*
2.8 - val str = "?r ^^^ 2 = ?r * ?r";
2.9 - val thm = realpow_twoI;
2.10 +val thy = @{theory Isac}
2.11
2.12 - val t1 = (#prop o rep_thm) (num_str thm);
2.13 - val t2 = Trueprop $ ((Thm.term_of o the o (parse thy)) str);
2.14 - t1 = t2;
2.15 -val it = true : bool ... !!!
2.16 - val th1 = (num_str thm);
2.17 - val th2 = ((*num_str*) (mk_thm thy str)) handle e => print_exn e;
2.18 - th1 = th2;
2.19 -ML> val it = false : bool ... HIDDEN DIFFERENCES IRRELEVANT FOR ISAC ?!
2.20 +(*~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~*)
2.21 +val thm = @{thm realpow_twoI};
2.22 +val patt_str = "?r ^^^ 2 = ?r * ?r";
2.23 +val term_str = "r ^^^ 2 = r * r";
2.24 +(*~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~*)
2.25 +case parse_patt thy patt_str of
2.26 + Const ("HOL.eq", _) $ (Const ("Atools.pow", _) $ Var (("r", 0), _) $ Free ("2", _)) $
2.27 + (Const ("Groups.times_class.times", _) $ Var (("r", 0), _) $ Var (("r", 0), _)) => ()
2.28 +| _ => error "parse_patt ?r ^^^ 2 = ?r * ?r changed";
2.29 +case parse thy str of
2.30 + NONE => ()
2.31 +| _ => writeln "parse does NOT take patterns with '?'";
2.32
2.33 -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2.34 - val str = "k ~= 0 ==> m * k / (n * k) = m / n";
2.35 - val thm = real_mult_div_cancel2;
2.36 +val t1 = (#prop o Thm.rep_thm) (num_str thm);
2.37 +if term2str t1 = patt_str then () else error "realpow_twoI (\<rightarrow> string) NOT equal to given string";
2.38
2.39 - val t1 = (#prop o rep_thm) (num_str thm);
2.40 - val t2 = ((Thm.term_of o the o (parse thy)) str);
2.41 - t1 = t2;
2.42 -val it = false : bool ... Var .. Free
2.43 - val th1 = (num_str thm);
2.44 - val th2 = ((*num_str*) (mk_thm thy str)) handle e => print_exn e;
2.45 - th1 = th2;
2.46 -ML> val it = false : bool ... PLUS HIDDEN DIFFERENCES IRRELEVANT FOR ISAC ?!
2.47 -*)
2.48 +val t2 = Trueprop $ (((parse_patt thy)) patt_str) : term;
2.49 +if t1 = t2 then () else error "prop of realpow_twoI NOT equal to parsed string";
2.50 +
2.51 +(mk_thm thy patt_str) handle _ => mk_thm thy "mk_thm = does NOT handle patterns";
2.52 +(*and this*) mk_thm thy term_str (* = "r ^^^ 2 = r * r" [.]: thm
2.53 + gives a strange thm*);
2.54 +(*while this*)
2.55 +val thm_made = Thm.make_thm (Thm.global_cterm_of thy t2) (* = "?r ^^^ 2 = ?r * ?r" [.]: thm
2.56 + gives another strange thm; but it is used and words with rewriting: *);
2.57 +
2.58 +val t1' = (#prop o Thm.rep_thm) (num_str thm_made);
2.59 +if t1 = t1' then () else error "prop of realpow_twoI NOT equal to thm_made from string";
2.60 +
2.61 +(*~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~*)
2.62 +val thm = @{thm real_mult_div_cancel2};
2.63 +val patt_str = "?k \<noteq> 0 \<Longrightarrow> ?m * ?k / (?n * ?k) = ?m / ?n";
2.64 +val term_str = "k \<noteq> 0 \<Longrightarrow> m * k / (n * k) = m / n";
2.65 +(*~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~*)
2.66 +case parse_patt thy patt_str of
2.67 + Const ("Pure.imp", _) $
2.68 + (Const ("HOL.Trueprop", _) $ (Const ("HOL.Not", _) $
2.69 + (Const ("HOL.eq", _) $ Var (("k", 0), _) $ Free ("0", _)))) $
2.70 + (Const ("HOL.Trueprop", _) $
2.71 + (Const ("HOL.eq", _) $ _ $ _ )) => ()
2.72 +| _ => error "parse_patt ?k \<noteq> 0 ==> ?m * ?k / (?n * ?k) = ?m / ?n changed";
2.73 +case parse thy str of
2.74 + NONE => ()
2.75 +| _ => writeln "parse does NOT take patterns with '?'";
2.76 +
2.77 +val t1 = (#prop o Thm.rep_thm) (num_str thm);
2.78 +if term2str t1 = patt_str then () else error "realpow_twoI (\<rightarrow> string) NOT equal to given string";
2.79 +
2.80 +val t2 = (*Trueprop $*) (((parse_patt thy)) patt_str) : term;
2.81 +if t1 = t2 then () else error "prop of realpow_twoI NOT equal to parsed string";
2.82 +
2.83 +(mk_thm thy patt_str) handle _ => mk_thm thy "mk_thm = does NOT handle patterns";
2.84 +(*and this*) mk_thm thy term_str (* = "r ^^^ 2 = r * r" [.]: thm
2.85 + gives a strange thm*);
2.86 +(*while this*)
2.87 +val thm_made = Thm.make_thm (Thm.global_cterm_of thy t2) (* = "?r ^^^ 2 = ?r * ?r" [.]: thm
2.88 + gives another strange thm; but it is used and words with rewriting: *);
2.89 +
2.90 +val t1' = (#prop o Thm.rep_thm) (num_str thm_made);
2.91 +if t1 = t1' then () else error "prop of realpow_twoI NOT equal to thm_made from string";