Searched refs:collapse (Results 1 - 25 of 26) sorted by relevance

12

/seL4-l4v-master/HOL4/examples/lambda/other-models/
H A Draw_syntaxScript.sml29 collapse e_1 -->_\beta collapse e_2
35 (Where collapse is written graphically in the paper as the "round
41 The collapse function below has the important property that
43 EQC alpha x y = (collapse x = collapse y)
45 I.e., two raw syntax terms are alpha-equivalent iff they collapse
148 (collapse (var s) = VAR s) /\
149 (collapse (app t u) = collapse
[all...]
/seL4-l4v-master/HOL4/examples/unification/triangular/first-order/
H A DcollapseScript.sml4 val _ = new_theory "collapse";
13 collapse s = FUN_FMAP (\v.walkstar s (Var v)) (FDOM s)`;
17 `wfs s ==> !t.(collapse s ��� t = walkstar s t)`,
27 `wfs s ==> !v.v IN FDOM s ==> (collapse s ' v = walkstar s (Var v))`,
41 `wfs s ==> idempotent (collapse s)`,
46 `idempotent s ��� noids s ==> (collapse s = s)`,
49 `FDOM s = FDOM (collapse s)` by SRW_TAC [][collapse_def,FUN_FMAP_DEF] THEN
56 Cases_on `v IN FDOM (collapse s)` THEN SRW_TAC [][] THEN
76 Q_TAC SUFF_TAC `s = collapse s`
78 `FDOM s = FDOM (collapse
[all...]
H A DsubstScript.sml717 Q.EXISTS_TAC `collapse s` >>
756 `wfs s ==> wfs (collapse s)`,
759 Q_TAC SUFF_TAC `!v u.(vR (collapse s))^+ v u ==> v <> u`
763 Cases_on `u IN FDOM (collapse s)` >>
804 !t.((collapse sx) ��� t = (ss oo s) ��� t)`,
/seL4-l4v-master/HOL4/src/1/
H A DFullUnify.sig23 val collapse : ((hol_type,hol_type)subst * (term,term) subst) Env.EM value
H A DPmatchHeuristics.sig10 collapse_cases : bool, (* collapse cases that lead to same result ? *)
H A DFullUnify.sml176 fun collapse E = SOME(E, collapse0 E) function
H A Dresolve_then.sml135 FullUnify.collapse)
/seL4-l4v-master/isabelle/lib/browser/GraphBrowser/
H A DConsole.java39 gra.collapse(v,"["+d.getName()+"]",d.getCollapsed());
H A DTreeNode.java84 if (unfold) collapse();
91 public void collapse() method in class:TreeNode
96 ((Tree)leaves.elementAt(i)).collapse();
H A DGraphView.java190 if (!v2.isEmpty()) gra.collapse(v2,"[. . . .]",v1);
199 gra.collapse(v,"["+d.getName()+"]",d.getCollapsed());
H A DGraph.java943 /* collapse vertices */
946 public void collapse(Vector vs,String name,Vector inflate) { method in class:Graph
/seL4-l4v-master/l4v/isabelle/lib/browser/GraphBrowser/
H A DConsole.java39 gra.collapse(v,"["+d.getName()+"]",d.getCollapsed());
H A DTreeNode.java84 if (unfold) collapse();
91 public void collapse() method in class:TreeNode
96 ((Tree)leaves.elementAt(i)).collapse();
H A DGraphView.java190 if (!v2.isEmpty()) gra.collapse(v2,"[. . . .]",v1);
199 gra.collapse(v,"["+d.getName()+"]",d.getCollapsed());
H A DGraph.java943 /* collapse vertices */
946 public void collapse(Vector vs,String name,Vector inflate) { method in class:Graph
/seL4-l4v-master/HOL4/polyml/basis/
H A DOS.sml529 fun collapse [] = [] function
530 | collapse (a :: b) =
534 then collapse b
537 case collapse b of
544 val collapsed = collapse arcs
/seL4-l4v-master/isabelle/src/Tools/Metis/src/
H A DUseful.sml299 fun collapse l = (fst (hd l), List.map snd l); function
301 fun groupsByFst l = List.map collapse (groupsBy fstEq l);
/seL4-l4v-master/l4v/isabelle/src/Tools/Metis/src/
H A DUseful.sml299 fun collapse l = (fst (hd l), List.map snd l); function
301 fun groupsByFst l = List.map collapse (groupsBy fstEq l);
/seL4-l4v-master/HOL4/src/transfer/
H A DtransferLib.sml223 case Env.fromEmpty (unify ctys [] (cr_t, h) >> collapse) of
331 collapse)
/seL4-l4v-master/HOL4/src/unwind/
H A DunwindLib.sml528 (* Could use an itlist here again and collapse the maps. *)
/seL4-l4v-master/HOL4/src/pattern_matches/
H A DpatternMatchesLib.sml346 (* try to collapse rows by introducing a catchall at end*)
364 (* really collapse *)
372 (* could we collapse 2 cases? *)
/seL4-l4v-master/HOL4/examples/HolCheck/
H A DcearTools.sml527 (* FIXME: amba_ahb example spends a lot of time here (ctl_grant_always). is ap collapse not working? *)
/seL4-l4v-master/isabelle/src/Doc/Intro/document/
H A Dadvanced.tex695 collapse $nat$ to a trivial type:
/seL4-l4v-master/l4v/isabelle/src/Doc/Intro/document/
H A Dadvanced.tex695 collapse $nat$ to a trivial type:
/seL4-l4v-master/HOL4/examples/algebra/lib/
H A DGaussScript.sml1192 = {{1}, {1}, {1, 2}, {1, 5}} <-- will collapse

Completed in 318 milliseconds

12